CVC3  2.4.1
Classes | Public Member Functions | Protected Member Functions | Protected Attributes | Private Member Functions | Friends | List of all members
CVC3::SearchImplBase Class Reference

API to to a generic proof search engine (a.k.a. SAT solver) More...

#include <search_impl_base.h>

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

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 AssumptionsgetAssumptionsUsed ()
 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.
CommonProofRulesgetCommonRules ()
 Accessor for common rules.
TheoryCoretheoryCore ()
 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
SearchEngineRulescreateRules ()
 Create the trusted component.
SearchEngineRulescreateRules (SearchEngine *s_eng)

Protected Attributes

VariableManagerd_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::CoreSatAPId_coreSatAPI_implBase
CDList< Splitterd_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, Theoremd_assumptions
 Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
CDMap< Expr, Theoremd_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, Theoremd_replaceITECache
 Cache for replaceITE()
- Protected Attributes inherited from CVC3::SearchEngine
TheoryCored_core
 Access to theory reasoning.
CommonProofRulesd_commonRules
 Common proof rules.
SearchEngineRulesd_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 class DecisionEngine
friend

Definition at line 38 of file search_impl_base.h.


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