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 89 of file search_fast.h.

Friends And Related Function Documentation

friend class Circuit [friend]

Definition at line 91 of file search_fast.h.

Referenced by addNonLiteralFact().

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

CVC3::SearchEngineFast Class ReferenceFast Search Engine