CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | List of all members
CVC3::SearchSimple Class Reference

Implementation of the simple search engine. More...

#include <search_simple.h>

Inheritance diagram for CVC3::SearchSimple:
CVC3::SearchImplBase CVC3::SearchEngine

Public Member Functions

 SearchSimple (TheoryCore *core)
 Constructor. More...
 
 ~SearchSimple ()
 Destructor. More...
 
const std::string & getName ()
 Name of this search engine. More...
 
QueryResult checkValidInternal (const Expr &e)
 Checks the validity of a formula in the current context. More...
 
QueryResult restartInternal (const Expr &e)
 Reruns last check with e as an additional assumption. More...
 
void addLiteralFact (const Theorem &thm)
 Notify the search engine about a new literal fact. More...
 
void addNonLiteralFact (const Theorem &thm)
 Notify the search engine about a new non-literal fact. More...
 
- Public Member Functions inherited from CVC3::SearchImplBase
int getBottomScope ()
 
bool isClause (const Expr &e)
 Check if e is a clause (a literal, or a disjunction of literals) More...
 
bool isPropClause (const Expr &e)
 Check if e is a propositional clause. More...
 
bool isCNFVar (const Expr &e)
 Check whether e is a fresh variable introduced by the CNF converter. More...
 
bool isGoodSplitter (const Expr &e)
 Check if a splitter is required for completeness. More...
 
 SearchImplBase (TheoryCore *core)
 Constructor. More...
 
virtual ~SearchImplBase ()
 Destructor. More...
 
virtual void registerAtom (const Expr &e)
 Register an atomic formula of interest. More...
 
virtual Theorem getImpliedLiteral ()
 Return next literal implied by last assertion. Null Expr if none. More...
 
virtual void push ()
 Push a checkpoint. More...
 
virtual void pop ()
 Restore last checkpoint. More...
 
virtual QueryResult checkValid (const Expr &e, Theorem &result)
 Similar to checkValidInternal(), only returns Theorem(e) or Null. More...
 
virtual QueryResult restart (const Expr &e, Theorem &result)
 Reruns last check with e as an additional assumption. More...
 
void returnFromCheck ()
 Returns to context immediately before last call to checkValid. More...
 
virtual Theorem lastThm ()
 Returns the result of the most recent valid theorem. More...
 
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(). More...
 
virtual Theorem newIntAssumption (const Expr &e)
 Add a new internal asserion. More...
 
void newIntAssumption (const Theorem &thm)
 Helper for above function. More...
 
void getUserAssumptions (std::vector< Expr > &assumptions)
 Get all assumptions made in this and all previous contexts. More...
 
void getInternalAssumptions (std::vector< Expr > &assumptions)
 Get assumptions made internally in this and all previous contexts. More...
 
virtual void getAssumptions (std::vector< Expr > &assumptions)
 Get all assumptions made in this and all previous contexts. More...
 
virtual bool isAssumption (const Expr &e)
 Check if the formula has been assumed. More...
 
void addFact (const Theorem &thm)
 Add a new fact to the search engine from the core. More...
 
virtual void addSplitter (const Expr &e, int priority)
 Suggest a splitter to the SearchEngine. More...
 
virtual void getCounterExample (std::vector< Expr > &assertions, bool inOrder=true)
 Will return the set of assertions which make the queried formula false. More...
 
virtual Proof getProof ()
 Returns the proof term for the last proven query. More...
 
virtual const AssumptionsgetAssumptionsUsed ()
 Returns the set of assumptions used in the proof. It should be a subset of getAssumptions(). More...
 
void processResult (const Theorem &res, const Expr &e)
 Process result of checkValid. More...
 
virtual FormulaValue getValue (const CVC3::Expr &e)
 
- Public Member Functions inherited from CVC3::SearchEngine
 SearchEngine (TheoryCore *core)
 Constructor. More...
 
virtual ~SearchEngine ()
 Destructor. More...
 
CommonProofRulesgetCommonRules ()
 Accessor for common rules. More...
 
TheoryCoretheoryCore ()
 Accessor for TheoryCore. More...
 
void getConcreteModel (ExprMap< Expr > &m)
 Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. More...
 
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. More...
 

Private Member Functions

QueryResult checkValidRec (Theorem &thm)
 Recursive DPLL algorithm used by checkValid. More...
 
QueryResult checkValidMain (const Expr &e2)
 Private helper function for checkValid and restart. More...
 

Private Attributes

std::string d_name
 Name. More...
 
DecisionEngined_decisionEngine
 Decision Engine. More...
 
CDO< Theoremd_goal
 Formula being checked. More...
 
CDO< Theoremd_nonLiterals
 Non-literals generated by DP's. More...
 
CDO< Theoremd_simplifiedThm
 Theorem which records simplification of the last query. More...
 

Additional Inherited Members

- Protected Member Functions inherited from CVC3::SearchImplBase
Literal newLiteral (const Expr &e)
 Construct a Literal out of an Expr or return an existing one. More...
 
Theorem simplify (const Theorem &e)
 Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e') More...
 
void addCNFFact (const Theorem &thm, bool fromCore=false)
 Add a new fact to the search engine bypassing CNF converter. More...
 
int scopeLevel ()
 Return the current scope level (for convenience) More...
 
- Protected Member Functions inherited from CVC3::SearchEngine
SearchEngineRulescreateRules ()
 Create the trusted component. More...
 
SearchEngineRulescreateRules (SearchEngine *s_eng)
 
- Protected Attributes inherited from CVC3::SearchImplBase
VariableManagerd_vm
 Variable manager for classes Variable and Literal. More...
 
CDO< int > d_bottomScope
 The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid). More...
 
TheoryCore::CoreSatAPId_coreSatAPI_implBase
 
CDList< Splitterd_dpSplitters
 Backtracking ordered set of DP-suggested splitters. More...
 
Theorem d_lastValid
 Theorem from the last successful checkValid call. It is used by getProof and getAssumptions. More...
 
ExprHashMap< bool > d_lastCounterExample
 Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample. More...
 
CDMap< Expr, Theoremd_assumptions
 Maintain the list of current assumptions (user asserts and splitters) for getAssumptions(). More...
 
CDMap< Expr, Theoremd_cnfCache
 Backtracking cache for the CNF generator. More...
 
CDMap< Expr, bool > d_cnfVars
 Backtracking set of new variables generated by CNF translator. More...
 
const bool * d_cnfOption
 Command line flag whether to convert to CNF. More...
 
const bool * d_ifLiftOption
 Flag: whether to convert term ITEs into CNF. More...
 
const bool * d_ignoreCnfVarsOption
 Flag: ignore auxiliary CNF variables when searching for a splitter. More...
 
const bool * d_origFormulaOption
 Flag: Preserve the original formula with +cnf (for splitter heuristics) More...
 
CDMap< Expr, bool > d_enqueueCNFCache
 Cache for enqueueCNF() More...
 
CDMap< Expr, bool > d_applyCNFRulesCache
 Cache for applyCNFRules() More...
 
CDMap< Expr, Theoremd_replaceITECache
 Cache for replaceITE() More...
 
- Protected Attributes inherited from CVC3::SearchEngine
TheoryCored_core
 Access to theory reasoning. More...
 
CommonProofRulesd_commonRules
 Common proof rules. More...
 
SearchEngineRulesd_rules
 Proof rules for the search engine. More...
 

Detailed Description

Implementation of the simple search engine.

Definition at line 41 of file search_simple.h.


The documentation for this class was generated from the following files: