API to to a generic proof search engine (a.k.a. SAT solver) More...
#include <search_impl_base.h>
Inherits CVC3::SearchEngine.
Inherited by CVC3::SearchEngineFast, and CVC3::SearchSimple.
Collaboration diagram for CVC3::SearchImplBase:
Classes | |
| class | Splitter |
| Representation of a DP-suggested splitter. More... | |
Public Member Functions | |
| int | getBottomScope () |
| bool | isClause (const Expr &e) |
| Check if e is a clause (a literal, or a disjunction of literals) | |
| bool | isPropClause (const Expr &e) |
| Check if e is a propositional clause. | |
| bool | isCNFVar (const Expr &e) |
| Check whether e is a fresh variable introduced by the CNF converter. | |
| bool | isGoodSplitter (const Expr &e) |
| Check if a splitter is required for completeness. | |
| SearchImplBase (TheoryCore *core) | |
| Constructor. | |
| virtual | ~SearchImplBase () |
| Destructor. | |
| virtual void | registerAtom (const Expr &e) |
| Register an atomic formula of interest. | |
| virtual Theorem | getImpliedLiteral () |
| Return next literal implied by last assertion. Null Expr if none. | |
| virtual void | push () |
| Push a checkpoint. | |
| virtual void | pop () |
| Restore last checkpoint. | |
| virtual QueryResult | checkValidInternal (const Expr &e)=0 |
| Checks the validity of a formula in the current context. | |
| virtual QueryResult | checkValid (const Expr &e, Theorem &result) |
| Similar to checkValidInternal(), only returns Theorem(e) or Null. | |
| virtual QueryResult | restartInternal (const Expr &e)=0 |
| Reruns last check with e as an additional assumption. | |
| virtual QueryResult | restart (const Expr &e, Theorem &result) |
| Reruns last check with e as an additional assumption. | |
| void | returnFromCheck () |
| Returns to context immediately before last call to checkValid. | |
| virtual Theorem | lastThm () |
| Returns the result of the most recent valid theorem. | |
| Theorem | newUserAssumption (const Expr &e) |
| Generate and add a new assertion to the set of assertions in the current context. This should only be used by class VCL in assertFormula(). | |
| virtual Theorem | newIntAssumption (const Expr &e) |
| Add a new internal asserion. | |
| void | newIntAssumption (const Theorem &thm) |
| Helper for above function. | |
| void | getUserAssumptions (std::vector< Expr > &assumptions) |
| Get all assumptions made in this and all previous contexts. | |
| void | getInternalAssumptions (std::vector< Expr > &assumptions) |
| Get assumptions made internally in this and all previous contexts. | |
| virtual void | getAssumptions (std::vector< Expr > &assumptions) |
| Get all assumptions made in this and all previous contexts. | |
| virtual bool | isAssumption (const Expr &e) |
| Check if the formula has been assumed. | |
| void | addFact (const Theorem &thm) |
| Add a new fact to the search engine from the core. | |
| virtual void | addSplitter (const Expr &e, int priority) |
| Suggest a splitter to the SearchEngine. | |
| virtual void | getCounterExample (std::vector< Expr > &assertions, bool inOrder=true) |
| Will return the set of assertions which make the queried formula false. | |
| virtual Proof | getProof () |
| Returns the proof term for the last proven query. | |
| virtual const Assumptions & | getAssumptionsUsed () |
| Returns the set of assumptions used in the proof. It should be a subset of getAssumptions(). | |
| void | processResult (const Theorem &res, const Expr &e) |
| Process result of checkValid. | |
| virtual FormulaValue | getValue (const CVC3::Expr &e) |
 Public Member Functions inherited from CVC3::SearchEngine | |
| SearchEngine (TheoryCore *core) | |
| Constructor. | |
| virtual | ~SearchEngine () |
| Destructor. | |
| virtual const std::string & | getName ()=0 |
| Name of this search engine. | |
| CommonProofRules * | getCommonRules () |
| Accessor for common rules. | |
| TheoryCore * | theoryCore () |
| Accessor for TheoryCore. | |
| void | getConcreteModel (ExprMap< Expr > &m) |
| Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. | |
| bool | tryModelGeneration (Theorem &thm) |
| Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent. | |
Protected Member Functions | |
| Literal | newLiteral (const Expr &e) |
| Construct a Literal out of an Expr or return an existing one. | |
| Theorem | simplify (const Theorem &e) |
| Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e') | |
| virtual void | addLiteralFact (const Theorem &thm)=0 |
| Notify the search engine about a new literal fact. | |
| virtual void | addNonLiteralFact (const Theorem &thm)=0 |
| Notify the search engine about a new non-literal fact. | |
| void | addCNFFact (const Theorem &thm, bool fromCore=false) |
| Add a new fact to the search engine bypassing CNF converter. | |
| int | scopeLevel () |
| Return the current scope level (for convenience) | |
| Protected Member Functions inherited from CVC3::SearchEngine | |
| SearchEngineRules * | createRules () |
| Create the trusted component. | |
| SearchEngineRules * | createRules (SearchEngine *s_eng) |
Protected Attributes | |
| VariableManager * | d_vm |
| Variable manager for classes Variable and Literal. | |
| CDO< int > | d_bottomScope |
| The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid). | |
| TheoryCore::CoreSatAPI * | d_coreSatAPI_implBase |
| CDList< Splitter > | d_dpSplitters |
| Backtracking ordered set of DP-suggested splitters. | |
| Theorem | d_lastValid |
| Theorem from the last successful checkValid call. It is used by getProof and getAssumptions. | |
| ExprHashMap< bool > | d_lastCounterExample |
| Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample. | |
| CDMap< Expr, Theorem > | d_assumptions |
| Maintain the list of current assumptions (user asserts and splitters) for getAssumptions(). | |
| CDMap< Expr, Theorem > | d_cnfCache |
| Backtracking cache for the CNF generator. | |
| CDMap< Expr, bool > | d_cnfVars |
| Backtracking set of new variables generated by CNF translator. | |
| const bool * | d_cnfOption |
| Command line flag whether to convert to CNF. | |
| const bool * | d_ifLiftOption |
| Flag: whether to convert term ITEs into CNF. | |
| const bool * | d_ignoreCnfVarsOption |
| Flag: ignore auxiliary CNF variables when searching for a splitter. | |
| const bool * | d_origFormulaOption |
| Flag: Preserve the original formula with +cnf (for splitter heuristics) | |
CNF Caches | |
These caches are for subexpressions of the translated formula phi, to avoid expanding phi into a tree. We cannot use d_cnfCache for that, since it is effectively non-backtracking, and we do not know if a subexpression of phi was translated at the current level, or at some other (inactive) branch of the decision tree. | |
| CDMap< Expr, bool > | d_enqueueCNFCache |
| Cache for enqueueCNF() | |
| CDMap< Expr, bool > | d_applyCNFRulesCache |
| Cache for applyCNFRules() | |
| CDMap< Expr, Theorem > | d_replaceITECache |
| Cache for replaceITE() | |
| Protected Attributes inherited from CVC3::SearchEngine | |
| TheoryCore * | d_core |
| Access to theory reasoning. | |
| CommonProofRules * | d_commonRules |
| Common proof rules. | |
| SearchEngineRules * | d_rules |
| Proof rules for the search engine. | |
Private Member Functions | |
| void | enqueueCNF (const Theorem &theta) |
| Translate theta to CNF and enqueue the new clauses. | |
| void | enqueueCNFrec (const Theorem &theta) |
| Recursive version of enqueueCNF() | |
| void | applyCNFRules (const Theorem &e) |
| FIXME: write a comment. | |
| void | addToCNFCache (const Theorem &thm) |
| Cache a theorem phi <=> v by phi, where v is a literal. | |
| Theorem | findInCNFCache (const Expr &e) |
| Find a theorem phi <=> v by phi, where v is a literal. | |
| Theorem | replaceITE (const Expr &e) |
| Replaces ITE subexpressions in e with variables. | |
Friends | |
| class | DecisionEngine |
Detailed Description
API to to a generic proof search engine (a.k.a. SAT solver)
Definition at line 37 of file search_impl_base.h.
Friends And Related Function Documentation
|
friend |
Definition at line 38 of file search_impl_base.h.
The documentation for this class was generated from the following files:
