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

Implementation of a faster search engine, using newer techniques. More...

#include <search_fast.h>

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

Classes

class  ConflictClauseManager

Public Member Functions

 SearchEngineFast (TheoryCore *core)
 The main Constructor.
virtual ~SearchEngineFast ()
 Destructor.
const std::string & getName ()
 Name of this search engine.
virtual QueryResult checkValidInternal (const Expr &e)
 Implementation of the API call.
virtual QueryResult restartInternal (const Expr &e)
 Reruns last check with e as an additional assumption.
virtual void getCounterExample (std::vector< Expr > &assertions)
 Redefine the counterexample generation.
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.
virtual Theorem newIntAssumption (const Expr &e)
 Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal.
virtual bool isAssumption (const Expr &e)
 Check if the formula has been assumed.
void addSplitter (const Expr &e, int priority)
 Suggest a splitter to the SearchEngine.
- 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)
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().
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.
void addFact (const Theorem &thm)
 Add a new fact to the search engine from the core.
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.
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.

Private Member Functions

std::vector< std::pair< Clause,
int > > & 
wp (const Literal &literal)
 Return a ref to the vector of watched literals. If no such vector exists, create it.
QueryResult checkSAT ()
bool split ()
 Choose a splitter.
Expr findSplitter ()
 Returns a splitter.
void clearLiterals ()
 Clear the list of asserted literals (d_literals)
void updateLitScores (bool firstTime)
void updateLitCounts (const Clause &c)
 Add the literals of a new clause to d_litsByScores.
bool bcp ()
 Boolean constraint propagation.
bool fixConflict ()
 Determines backtracking level and adds conflict clauses.
void assertAssumptions ()
 FIXME: document this.
void enqueueFact (const Theorem &thm)
 Queue up a fact to assert to the DPs later.
void setInconsistent (const Theorem &thm)
 Set the context inconsistent. Takes Theorem(FALSE).
void commitFacts ()
 Commit all the enqueued facts to the DPs.
void clearFacts ()
 Clear the local fact queue.
bool propagate (const Clause &c, int idx, bool &wpUpdated)
 Auxiliary function for unit propagation.
void unitPropagation (const Clause &c, unsigned idx)
 Do the unit propagation for the clause.
void analyzeUIPs (const Theorem &falseThm, int conflictScope)
 Analyse the conflict, find the UIPs, etc.
void addNewClause (Clause &c)
 Go through all the clauses and check the watch pointers (for debugging)
void recordFact (const Theorem &thm)
 Process a new derived fact (auxiliary function)
void traceConflict (const Theorem &conflictThm)
 First pass in conflict analysis; takes a theorem of FALSE.
QueryResult checkValidMain (const Expr &e2)
 Private helper function for checkValid and restart.
Processing a Conflict
Theorem processConflict (const Literal &l)
 Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses.
Theorem processConflict (const Theorem &thm)
 Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses.

Private Attributes

std::string d_name
 Name.
DecisionEngined_decisionEngine
 Decision Engine.
StatCounter d_unitPropCount
 Total number of unit propagations.
StatCounter d_circuitPropCount
 Total number of circuit propagations.
StatCounter d_conflictCount
 Total number of conflicts.
StatCounter d_conflictClauseCount
 Total number of conflict clauses generated (not all may be active)
CDList< ClauseOwnerd_clauses
 Backtrackable list of clauses.
CDMap< Expr, Theoremd_unreportedLits
 Backtrackable set of pending unprocessed literals.
CDMap< Expr, bool > d_unreportedLitsHandled
CDList< SmartCDO< Theorem > > d_nonLiterals
 Backtrackable list of non-literals (non-CNF formulas).
CDMap< Expr, Theoremd_nonLiteralsSaved
 prevent reprocessing
CDO< Theoremd_simplifiedThm
 Theorem which records simplification of the last query.
CDO< unsigned > d_nonlitQueryStart
 Size of d_nonLiterals before most recent query.
CDO< unsigned > d_nonlitQueryEnd
 Size of d_nonLiterals after query (not including DP-generated non-literals)
CDO< unsigned > d_clausesQueryStart
 Size of d_clauses before most recent query.
CDO< unsigned > d_clausesQueryEnd
 Size of d_clauses after query.
std::vector< std::deque
< ClauseOwner > * > 
d_conflictClauseStack
 Array of conflict clauses: one deque for each outstanding query.
std::deque< ClauseOwner > * d_conflictClauses
 Reference to top deque of conflict clauses.
ConflictClauseManager d_conflictClauseManager
std::vector< Claused_unitConflictClauses
 Unprocessed unit conflict clauses.
std::vector< Literald_literals
 Set of literals to be processed by bcp.
CDMap< Expr, Literald_literalSet
 Set of asserted literals which may survive accross checkValid() calls.
std::vector< Theoremd_factQueue
 Queue of derived facts to be sent to DPs.
bool d_useEnqueueFact
 When true, use TheoryCore::enqueueFact() instead of addFact() in commitFacts()
bool d_inCheckSAT
 True when checkSAT() is running.
CDList< Literald_litsAlive
 Set of alive literals that shouldn't be garbage-collected.
std::vector< Circuit * > d_circuits
 Mappings of literals to vectors of pointers to the corresponding watched literals.
ExprHashMap< std::vector
< Circuit * > > 
d_circuitsByExpr
int d_lastConflictScope
 The scope of the last conflict.
Clause d_lastConflictClause
 The last conflict clause (for checkSAT()). May be Null.
Theorem d_conflictTheorem
 Theorem(FALSE) which generated a conflict.
unsigned d_litsMaxScorePos
 Position of a literal with max score in d_litsByScores.
std::vector< Literald_litsByScores
 Vector of literals sorted by score.
int d_splitterCount
 Internal splitter counter for delaying updateLitScores()
int d_litSortCount
 Internal (decrementing) count of added splitters, to sort d_litByScores.
const bool d_berkminFlag
 Flag to switch on/off the berkmin heuristic.

Friends

class Circuit
class ConflictClauseManager
 Helper class for managing conflict clauses.

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.
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)
- Protected Attributes inherited from CVC3::SearchImplBase
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)
CDMap< Expr, bool > d_enqueueCNFCache
 Cache for enqueueCNF()
CDMap< Expr, bool > d_applyCNFRulesCache
 Cache for applyCNFRules()
CDMap< Expr, Theoremd_replaceITECache
 Cache for replaceITE()

Detailed Description

Implementation of a faster search engine, using newer techniques.

This search engine is engineered for greater speed. It seeks to eliminate the use of recursion, and instead replace it with iterative procedures that have cleanly defined invariants. This will hopefully not only eliminate bugs or inefficiencies that have been difficult to track down in the default version, but it should also make it easier to trace, read, and understand. It strives to be in line with the most modern SAT techniques.

There are three other significant changes.

One, we want to improve the performance on heavily non-CNF problems. Unlike the older CVC, CVC3 does not expand problems into CNF and solve, but rather uses decision procedures to effect the same thing, but often much more slowly. This search engine will leverage off knowledge gained from the DPs in the form of conflict clauses as much as possible.

Two, the solver has traditionally had a difficult time getting started on non-CNF problems. Modern satsolvers also have this problem, and so they employ "restarts" to try solving the problem again after gaining more knowledge about the problem at hand. This allows a more accurate choice of splitters, and in the case of non-CNF problems, the solver can immediately leverage off CNF conflict clauses that were not initially available.

Third, this code is specifically designed to deal with the new dependency tracking. Lazy maps will be eliminated in favor implicit conflict graphs, reducing computation time in two different ways.

Definition at line 86 of file search_fast.h.

Friends And Related Function Documentation

friend class Circuit
friend

Definition at line 88 of file search_fast.h.

Referenced by addNonLiteralFact().


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