33 : d_core(core), d_se(se),
34 d_splitters(core->getCM()->getCurrentContext()),
35 d_splitterCount(core->getStatistics().counter(
"splitters"))
79 vector<int> order(e.
arity());
94 for (
int k = 0; k < e.
arity(); ++k)
100 for (
int k = 0; k < e.
arity(); k++)
130 string stCase = whichCase ?
"TRUE" :
"FALSE";
133 TRACE(
"search trace",
"Asserting splitter("+stCase+
"): ", splitter,
"");
134 TRACE(
"search",
"Asserting splitter("+stCase+
"): ", splitter,
"");
137 splitter = splitter.
negate();
bool isAtomic() const
Test if e is atomic.
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.
iterator find(const Expr &e)
ExprMap< Expr > d_visited
Visited cache for findSplitterRec traversal.
Expr lastSplitter()
Return the last known splitter.
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
virtual bool isBetter(const Expr &e1, const Expr &e2)=0
T & push_back(const T &data, int scope=-1)
SearchImplBase * d_se
Pointer to search engine.
size_t count(const Expr &e) const
void pushDecision(Expr splitter, bool whichCase=true)
Push context and record the splitter.
virtual Theorem newIntAssumption(const Expr &e)
Add a new internal asserion.
bool isGoodSplitter(const Expr &e)
Check if a splitter is required for completeness.
virtual void addLiteralFact(const Theorem &thm)=0
Notify the search engine about a new literal fact.
Expr findExpr(const Expr &e)
Return the find of e, or e if it has no find.
void popTo(int dl)
Pop to given scope.
TheoryCore * d_core
Pointer to core theory.
ContextManager * getCM() const
ExprMap< Expr > d_bestByExpr
CDList< Expr > d_splitters
List of currently active splitters.
void popDecision()
Pop last decision (and context)
API to to a generic proof search engine (a.k.a. SAT solver)
bool isAbsLiteral() const
Test if e is an abstract literal.
StatCounter d_splitterCount
Total number of splitters.
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...