CVC3
2.4.1
|
API to to a generic proof search engine (a.k.a. SAT solver) More...
#include <search_impl_base.h>
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) |
![]() | |
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) | |
![]() | |
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() | |
![]() | |
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 |
API to to a generic proof search engine (a.k.a. SAT solver)
Definition at line 37 of file search_impl_base.h.
|
friend |
Definition at line 38 of file search_impl_base.h.