CVC3::SearchImplBase Class Reference

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:

List of all members.

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)

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 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()
  

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:

• search_impl_base.h
• search_impl_base.cpp