CVC3::SearchEngineFast Class Reference
[Fast Search Engine]

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

#include <search_fast.h>

Inheritance diagram for CVC3::SearchEngineFast:

[legend]

Collaboration diagram for CVC3::SearchEngineFast:

[legend]

List of all members.

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.
  

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.
  

• DecisionEngine * d_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< ClauseOwner > d_clauses

  Backtrackable list of clauses.
  

• CDMap< Expr, Theorem > d_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, Theorem > d_nonLiteralsSaved

  prevent reprocessing
  

• CDO< Theorem > d_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< Clause > d_unitConflictClauses

  Unprocessed unit conflict clauses.
  

• std::vector< Literal > d_literals

  Set of literals to be processed by bcp.
  

• CDMap< Expr, Literal > d_literalSet

  Set of asserted literals which may survive accross checkValid() calls.
  

• std::vector< Theorem > d_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< Literal > d_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< Literal > d_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.
  

---

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:

• search_fast.h
• search_fast.cpp