CVC3
2.4.1
|
Implementation of the simple search engine. More...
#include <search_simple.h>
Public Member Functions | |
SearchSimple (TheoryCore *core) | |
Constructor. | |
~SearchSimple () | |
Destructor. | |
const std::string & | getName () |
Name of this search engine. | |
QueryResult | checkValidInternal (const Expr &e) |
Checks the validity of a formula in the current context. | |
QueryResult | restartInternal (const Expr &e) |
Reruns last check with e as an additional assumption. | |
void | addLiteralFact (const Theorem &thm) |
Notify the search engine about a new literal fact. | |
void | addNonLiteralFact (const Theorem &thm) |
Notify the search engine about a new non-literal fact. | |
![]() | |
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 | checkValid (const Expr &e, Theorem &result) |
Similar to checkValidInternal(), only returns Theorem(e) or Null. | |
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. | |
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. |
Private Member Functions | |
QueryResult | checkValidRec (Theorem &thm) |
Recursive DPLL algorithm used by checkValid. | |
QueryResult | checkValidMain (const Expr &e2) |
Private helper function for checkValid and restart. |
Private Attributes | |
std::string | d_name |
Name. | |
DecisionEngine * | d_decisionEngine |
Decision Engine. | |
CDO< Theorem > | d_goal |
Formula being checked. | |
CDO< Theorem > | d_nonLiterals |
Non-literals generated by DP's. | |
CDO< Theorem > | d_simplifiedThm |
Theorem which records simplification of the last query. |
Additional Inherited Members | |
![]() | |
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') | |
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) | |
![]() | |
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) | |
CDMap< Expr, bool > | d_enqueueCNFCache |
Cache for enqueueCNF() | |
CDMap< Expr, bool > | d_applyCNFRulesCache |
Cache for applyCNFRules() | |
CDMap< Expr, Theorem > | d_replaceITECache |
Cache for replaceITE() |
Implementation of the simple search engine.
Definition at line 41 of file search_simple.h.