17 #ifndef _cvc3__search__decision_engine_mbtf_h_
18 #define _cvc3__search__decision_engine_mbtf_h_
Data structure of expressions in CVC3.
virtual bool isBetter(const Expr &e1, const Expr &e2)
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
virtual void goalSatisfied()
Search should call this when it derives 'false'.
DecisionEngineMBTF(TheoryCore *core, SearchImplBase *se)
virtual ~DecisionEngineMBTF()
virtual Expr findSplitter(const Expr &e)
Finds a splitter inside a non const expression. The expression passed in must not be a boolean consta...
std::vector< CacheEntry > d_cache
API to to a generic proof search engine (a.k.a. SAT solver)