21 #ifndef _cvc3__search__decision_engine_dfs_h_
22 #define _cvc3__search__decision_engine_dfs_h_
virtual ~DecisionEngineDFS()
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Decision Engine for use with the Search EngineAuthor: Clark Barrett.
virtual bool isBetter(const Expr &e1, const Expr &e2)
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)
DecisionEngineDFS(TheoryCore *core, SearchImplBase *se)
Constructor.