32 bool DecisionEngineDFS::isBetter(
const Expr& e1,
const Expr& e2)
68 TRACE(
"splitters verbose",
"findSplitter(", e,
") {");
81 debugger.counter(
"splitters from decision engine")++;)
83 TRACE(
"splitters verbose",
"findSplitter => ", splitter,
" }");
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Expr findSplitterRec(const Expr &e)
Abstract API to the proof search engine.
ExprMap< Expr > d_visited
Visited cache for findSplitterRec traversal.
virtual void goalSatisfied()
Search should call this when it derives 'false'.
virtual Expr findSplitter(const Expr &e)
Find the next splitter.
API to to a generic proof search engine (a.k.a. SAT solver)