CVC3  2.4.1
Classes | Functions | Variables | Friends
Fast Search Engine

Classes

class  CVC3::SearchEngineFast::ConflictClauseManager
 
class  CVC3::SearchEngineFast
 Implementation of a faster search engine, using newer techniques. More...
 

Functions

std::vector< std::pair< Clause, int > > & CVC3::SearchEngineFast::wp (const Literal &literal)
 Return a ref to the vector of watched literals. If no such vector exists, create it. More...
 
QueryResult CVC3::SearchEngineFast::checkSAT ()
 
bool CVC3::SearchEngineFast::split ()
 Choose a splitter. More...
 
Expr CVC3::SearchEngineFast::findSplitter ()
 Returns a splitter. More...
 
void CVC3::SearchEngineFast::clearLiterals ()
 Clear the list of asserted literals (d_literals) More...
 
void CVC3::SearchEngineFast::updateLitScores (bool firstTime)
 
void CVC3::SearchEngineFast::updateLitCounts (const Clause &c)
 Add the literals of a new clause to d_litsByScores. More...
 
bool CVC3::SearchEngineFast::bcp ()
 Boolean constraint propagation. More...
 
bool CVC3::SearchEngineFast::fixConflict ()
 Determines backtracking level and adds conflict clauses. More...
 
void CVC3::SearchEngineFast::assertAssumptions ()
 FIXME: document this. More...
 
void CVC3::SearchEngineFast::enqueueFact (const Theorem &thm)
 Queue up a fact to assert to the DPs later. More...
 
void CVC3::SearchEngineFast::setInconsistent (const Theorem &thm)
 Set the context inconsistent. Takes Theorem(FALSE). More...
 
void CVC3::SearchEngineFast::commitFacts ()
 Commit all the enqueued facts to the DPs. More...
 
void CVC3::SearchEngineFast::clearFacts ()
 Clear the local fact queue. More...
 
bool CVC3::SearchEngineFast::propagate (const Clause &c, int idx, bool &wpUpdated)
 Auxiliary function for unit propagation. More...
 
void CVC3::SearchEngineFast::unitPropagation (const Clause &c, unsigned idx)
 Do the unit propagation for the clause. More...
 
void CVC3::SearchEngineFast::analyzeUIPs (const Theorem &falseThm, int conflictScope)
 Analyse the conflict, find the UIPs, etc. More...
 
void CVC3::SearchEngineFast::addNewClause (Clause &c)
 Go through all the clauses and check the watch pointers (for debugging) More...
 
void CVC3::SearchEngineFast::recordFact (const Theorem &thm)
 Process a new derived fact (auxiliary function) More...
 
void CVC3::SearchEngineFast::traceConflict (const Theorem &conflictThm)
 First pass in conflict analysis; takes a theorem of FALSE. More...
 
QueryResult CVC3::SearchEngineFast::checkValidMain (const Expr &e2)
 Private helper function for checkValid and restart. More...
 
 CVC3::SearchEngineFast::SearchEngineFast (TheoryCore *core)
 The main Constructor. More...
 
virtual CVC3::SearchEngineFast::~SearchEngineFast ()
 Destructor. More...
 
const std::string & CVC3::SearchEngineFast::getName ()
 Name of this search engine. More...
 
virtual QueryResult CVC3::SearchEngineFast::checkValidInternal (const Expr &e)
 Implementation of the API call. More...
 
virtual QueryResult CVC3::SearchEngineFast::restartInternal (const Expr &e)
 Reruns last check with e as an additional assumption. More...
 
virtual void CVC3::SearchEngineFast::getCounterExample (std::vector< Expr > &assertions)
 Redefine the counterexample generation. More...
 
void CVC3::SearchEngineFast::addLiteralFact (const Theorem &thm)
 Notify the search engine about a new literal fact. More...
 
void CVC3::SearchEngineFast::addNonLiteralFact (const Theorem &thm)
 Notify the search engine about a new non-literal fact. More...
 
virtual Theorem CVC3::SearchEngineFast::newIntAssumption (const Expr &e)
 Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal. More...
 
virtual bool CVC3::SearchEngineFast::isAssumption (const Expr &e)
 Check if the formula has been assumed. More...
 
void CVC3::SearchEngineFast::addSplitter (const Expr &e, int priority)
 Suggest a splitter to the SearchEngine. More...
 

Variables

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

Friends

class CVC3::SearchEngineFast::ConflictClauseManager
 Helper class for managing conflict clauses. More...
 

Processing a Conflict

Theorem CVC3::SearchEngineFast::processConflict (const Literal &l)
 Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses. More...
 
Theorem CVC3::SearchEngineFast::processConflict (const Theorem &thm)
 Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses. More...
 

Detailed Description

This module includes all the components of the fast search engine.

Function Documentation

vector< std::pair< Clause, int > > & SearchEngineFast::wp ( const Literal literal)
private

Return a ref to the vector of watched literals. If no such vector exists, create it.

This function is normally used when the value of 'literal' becomes false. The vector contains pointers to all clauses where this literal occurs, and therefore, these clauses may cause unit propagation. In any case, the watch pointers in these clauses need to be updated.

Definition at line 136 of file search_fast.cpp.

References CVC3::Literal::wp().

Referenced by CVC3::SearchEngineFast::addNewClause(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::bcp(), and CVC3::SearchEngineFast::propagate().

QueryResult SearchEngineFast::checkSAT ( )
private
bool SearchEngineFast::split ( )
private
Expr SearchEngineFast::findSplitter ( )
private
void SearchEngineFast::clearLiterals ( )
private

Clear the list of asserted literals (d_literals)

Definition at line 631 of file search_fast.cpp.

References CVC3::SearchEngineFast::d_literals, and TRACE_MSG.

Referenced by CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::checkValidMain(), and CVC3::SearchEngineFast::fixConflict().

void CVC3::SearchEngineFast::updateLitScores ( bool  firstTime)
private
void SearchEngineFast::updateLitCounts ( const Clause c)
private
bool SearchEngineFast::bcp ( )
private

Boolean constraint propagation.

Preconditions: On every run besides the first, the CNF clause database must not have any unit or unsat clauses, and there must be a literal queued up for processing. The current context must be consistent. Any and all assertions and assignments must actually be made within the bcp loop. Other parts of the solver may queue new facts with addLiteralFact() and addNonLiteralFact(). bcp() will either process them, or it will find a conflict, in which case they will no longer be valid and will be dumped. Any nonLiterals must already be simplified.

Description: BCP will systematically work through all the literals and nonliterals, using boolean constraint propagation by detecting unit clauses and using addLiteralFact() on the unit literal while also marking the clause as SAT. Any clauses marked SAT are guaranteed to be SAT, but clauses not marked SAT are not guaranteed to be unsat.

Returns
false if a conflict is found, true otherwise.

Postconditions: False indicates conflict. If the conflict was discovered in CNF, we call the proof rule, then store that clause pointer so fixConflict() can skip over it during the search (when we finally change dependency tracking).

True indicates success. All literals and nonLiterals have been processed without causing a conflict. Processing nonliterals implies running simplify on them, immediately asserting any simplifications back to the core, and marking the original nonLiteral as simplified, to be ignored by all future (this context or deeper) splitters and bcp runs. Therefore, there will be no unsimplified nonliterals remaining.

Definition at line 637 of file search_fast.cpp.

References CVC3::SearchEngineFast::clearFacts(), CVC3::SearchEngineFast::clearLiterals(), CVC3::SearchEngineFast::commitFacts(), CVC3::SearchEngineFast::d_circuitsByExpr, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngineFast::d_conflictTheorem, CVC3::SearchEngine::d_core, CVC3::SearchEngineFast::d_factQueue, CVC3::SearchEngineFast::d_literals, CVC3::SearchEngineFast::d_litsAlive, CVC3::SearchEngineFast::d_nonLiterals, DebugAssert, CVC3::Clause::deleted(), CVC3::SearchEngineFast::enqueueFact(), CVC3::Literal::getExpr(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getFlags(), CVC3::Literal::getValue(), IF_DEBUG(), CVC3::TheoryCore::inconsistent(), CVC3::TheoryCore::inconsistentThm(), CVC3::int2string(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isExists(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), CVC3::SearchEngineFast::propagate(), CVC3::Clause::sat(), CVC3::SearchImplBase::scopeLevel(), CVC3::SearchEngineFast::setInconsistent(), CVC3::SearchImplBase::simplify(), CVC3::CommonProofRules::skolemize(), CVC3::Literal::toString(), TRACE, TRACE_MSG, CVC3::Clause::watched(), and CVC3::SearchEngineFast::wp().

Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::checkSAT(), and CVC3::SearchEngineFast::split().

bool SearchEngineFast::fixConflict ( )
private

Determines backtracking level and adds conflict clauses.

Preconditions: The current context is inconsistent. If it resulted from a conflictRule() application, then the theorem is stored inside d_lastConflictTheorem.

If this was caused from bcp, we obtain the conflictRule() theorem from the d_lastConflictTheorem instance variable. From here we build conflict clauses and determine the correct backtracking level, at which point we actually backtrack there. Finally, we also call addLiteralFact() on the "failure driven assertion" literal so that bcp has some place to begin (and it satisfies the bcp preconditions)

Postconditions: If True is returned: The current context is consistent, and a literal is queued up for bcp to process. If False is returned: The context cannot be made consistent without backtracking past the original one, so the formula is unsat.

Definition at line 939 of file search_fast.cpp.

References CVC3::SearchEngineFast::clearLiterals(), CVC3::SearchEngineFast::commitFacts(), CVC3::SearchImplBase::d_bottomScope, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngineFast::d_conflictCount, CVC3::SearchEngineFast::d_conflictTheorem, CVC3::SearchEngineFast::d_decisionEngine, CVC3::SearchEngineFast::d_lastConflictClause, CVC3::SearchEngineFast::d_lastConflictScope, CVC3::SearchEngineFast::d_unitConflictClauses, DebugAssert, CVC3::SearchEngineFast::enqueueFact(), CVC3::Literal::getExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getScope(), CVC3::Clause::getTheorem(), IF_DEBUG(), CVC3::CommonProofRules::iffMP(), CVC3::int2string(), CVC3::Clause::isNull(), CVC3::Expr::isNull(), CVC3::Expr::isOr(), CVC3::DecisionEngine::popTo(), CVC3::Theorem::printDebug(), CVC3::CommonProofRules::rewriteOr(), CVC3::SearchImplBase::scopeLevel(), CVC3::Clause::size(), CVC3::Literal::toString(), TRACE, TRACE_MSG, CVC3::SearchEngineFast::traceConflict(), and CVC3::SearchEngineFast::unitPropagation().

Referenced by CVC3::SearchEngineFast::checkSAT().

void CVC3::SearchEngineFast::assertAssumptions ( )
private

FIXME: document this.

void SearchEngineFast::enqueueFact ( const Theorem thm)
private
void SearchEngineFast::setInconsistent ( const Theorem thm)
private
void SearchEngineFast::commitFacts ( )
private
void SearchEngineFast::clearFacts ( )
private

Clear the local fact queue.

Definition at line 1063 of file search_fast.cpp.

References CVC3::SearchEngineFast::d_factQueue, and TRACE_MSG.

Referenced by CVC3::SearchEngineFast::bcp(), and CVC3::SearchEngineFast::checkValidMain().

Theorem CVC3::SearchEngineFast::processConflict ( const Literal l)
private

Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses.

Theorem CVC3::SearchEngineFast::processConflict ( const Theorem thm)
private

Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses.

bool SearchEngineFast::propagate ( const Clause c,
int  idx,
bool &  wpUpdated 
)
private
void SearchEngineFast::unitPropagation ( const Clause c,
unsigned  idx 
)
private
void SearchEngineFast::analyzeUIPs ( const Theorem falseThm,
int  conflictScope 
)
private

Analyse the conflict, find the UIPs, etc.

Finding UIPs (Unique Implication Pointers)

This is basically the same as finding hammocks of the subset of the implication graph composed of only the nodes from the current scope. A hammock is a portion of the graph which has a single source and/or sink such that removing that single node makes the graph disconnected.

Conceptually, the algorithm maintains four sets of nodes: literals (named lits), gamma, fringe, and pending. Literals are nodes whose expressions will become literals in the conflict clause of the current hammock, and the nodes in gamma are assumptions from which such conflict clause theorem is derived. Nodes in fringe are intermediate nodes which are ready to be "expanded" (see the algorithm description below). The pending nodes are those which are not yet ready to be processed (they later become literal or fringe nodes).

These sets are maintained as vectors, and are updated in such a way that the nodes in the vectors never repeat. The exception is the pending set, for which only a size counter is maintained. A node belongs to the pending set if it has been visited (isFlagged() method), and its fan-out count is non-zero (stored in the cache, getCachedValue()). In other words, pending nodes are those that have been visited, but not sufficient number of times.

Also, fringe is maintained as a pair of vectors. One vector is always the current fringe, and the other one is built when the current is processed. When processing of the current fringe is finished, it is cleared, and the other vector becomes the current fringe (that is, they swap roles).

A node is expanded if it is marked for expansion (getExpandFlag()). If its fan-out count is not yet zero, it is added to the set of pending nodes.

If a node has a literal flag (getLitFlag()), it goes into literals when its fan-out count reaches zero. Since this will be the last time the node is visited, it is added to the vector only once.

A node neither marked for expansion nor with the literal flag goes into the gamma set. It is added the first time the node is visited (isFlagged() returns false), and therefore, is added to the vector only once. This is an important distinction from the other sets, since a gamma-node may be used by several conflict clauses.

Clearing the gamma set after each UIP requires both clearing the vector and resetting all flags (clearAllFlags()).

The algorithm

  1. Initially, the fringe contains exactly the predecessors of falseThm from the current scope which are ready to be expanded (fan-out count is zero). All the other predecessors of falseThm go to the appropriate sets of literals, gamma, and pending.

  2. If fringe.size() <= 1 and the set of pending nodes is empty, then the element in the fringe (if it's non-empty) is a UIP. Generate a conflict clause from the UIP and the literals (using gamma as the set of assumptions), empty the sets, and continue with the next step. Note, that the UIP remains in the fringe, and will be expanded in the next step.

    The important exception: if the only element in the fringe is marked for expansion, then this is a false UIP (the SAT solver doesn't know about this node), and it should not appear in the conflict clause. In this case, simply proceed to step 3 as if nothing happened.

  3. If fringe.size()==0, stop (the set of pending nodes must also be empty at this point). Otherwise, for every node in the fringe, decrement the fan-out for each of its predecessors, and empty the fringe. Take the predecessors from the current scope, and add those to the fringe for which fan-out count is zero, and remove them from the set of pending nodes. Add the other predecessors from the current scope to the set of pending nodes. Add the remaining predecessors (not from the current scope) to the literals or gamma, as appropriate. Continue with step 2.

Definition at line 1266 of file search_fast.cpp.

References CVC3::Assumptions::begin(), CVC3::Theorem::clearAllFlags(), CVC3::SearchEngineRules::conflictClause(), CVC3::SearchImplBase::d_bottomScope, CVC3::SearchEngineFast::d_conflictClauseCount, CVC3::SearchEngineFast::d_conflictClauses, CVC3::SearchEngine::d_core, CVC3::SearchEngineFast::d_lastConflictClause, CVC3::SearchEngineFast::d_lastConflictScope, CVC3::SearchEngine::d_rules, CVC3::SearchEngineFast::d_unitConflictClauses, CVC3::SearchImplBase::d_vm, DebugAssert, CVC3::Assumptions::end(), std::endl(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Clause::getScope(), IF_DEBUG(), CVC3::int2string(), CVC3::Clause::isNull(), CVC3::Theorem::printDebug(), processNode(), CVC3::Clause::size(), TRACE, TRACE_MSG, CVC3::SearchEngineFast::updateLitCounts(), CVC3::Clause::watched(), CVC3::Clause::wp(), and CVC3::SearchEngineFast::wp().

Referenced by CVC3::SearchEngineFast::traceConflict().

void SearchEngineFast::addNewClause ( Clause c)
private

Go through all the clauses and check the watch pointers (for debugging)

Set up the watch pointers for the new clause

Definition at line 1069 of file search_fast.cpp.

References CVC3::SearchEngineFast::d_clauses, DebugAssert, CVC3::Clause::size(), CVC3::SearchEngineFast::updateLitCounts(), CVC3::Clause::watched(), CVC3::Clause::wp(), and CVC3::SearchEngineFast::wp().

Referenced by CVC3::SearchEngineFast::addNonLiteralFact().

void SearchEngineFast::recordFact ( const Theorem thm)
private
void SearchEngineFast::traceConflict ( const Theorem conflictThm)
private

First pass in conflict analysis; takes a theorem of FALSE.

The purpose of this method is to mark up the assumption graph of the FALSE Theorem (conflictThm) for the later UIP analysis. The required flags for each assumption in the graph are:

ExpandFlag: whether to "expand" the node or not; that is, whether to consider the current node as a final assumption (either as a conflict clause literal, or a context assumption from $\Gamma$)

LitFlag: the node (actually, its inverse) is a literal of the conflict clause

CachedValue: the "fanout" count, how many nodes in the assumption graph are derived from the current node.

INVARIANTS (after the method returns):

  1. The currect scope is the "true" conflict scope, i.e. scopeLevel() == conflictThm.getScope()
  2. The literals marked with LitFlag (CC literals) are known to the SAT solver, i.e. their Literal class has a value == 1
  3. The only CC literal from the current scope is the latest splitter

ASSUMPTIONS:

  1. The Theorem scope of an assumption is the same as its Literal scope; i.e. if thm is a splitter, then thm.getScope() == newLiteral(thm.getExpr()).getScope()

Algorithm:

First, backtrack to the scope level of the conflict. Then, traverse the implication graph until we either hit a literal known to the SAT solver at a lower scope: newLiteral(e).getScope()<scopeLevel(), or a splitter (assumption), or a fact from the bottom scope. The literals from the first two categories are marked with LitFlag (they'll comprise the conflict clause), and the bottom scope facts will be the assumptions in the conflict clause's theorem.

The traversed nodes are cached by the .isFlagged() flag, and subsequent hits only increase the fanout count of the node.

Notice, that there can only be one literal in the conflict clause from the current scope. Also, even if some intermediate literals were delayed by the DPs and reported to the SAT solver at or below the conflict scope (which may be below their "true" Theorem scope), they will be skipped, and their assumptions will be used.

In other words, it is safe to backtrack to the "true" conflict level, since, in the worst case, we traverse the graph all the way to the splitters, and make a conflict clause out of those. The hope is, however, that this wouldn't happen too often.

Definition at line 1837 of file search_fast.cpp.

References CVC3::SearchEngineFast::analyzeUIPs(), CVC3::Assumptions::begin(), CVC3::Theorem::clearAllFlags(), CVC3::SearchImplBase::d_bottomScope, CVC3::SearchEngineFast::d_decisionEngine, CVC3::SearchEngineFast::d_lastConflictScope, DebugAssert, CVC3::Assumptions::end(), std::endl(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Literal::getScope(), CVC3::Theorem::getScope(), CVC3::Literal::getValue(), IF_DEBUG(), CVC3::int2string(), CVC3::SearchImplBase::newLiteral(), CVC3::DecisionEngine::popTo(), CVC3::Theorem::printDebug(), CVC3::SearchImplBase::scopeLevel(), CVC3::Theorem::setCachedValue(), CVC3::Theorem::setExpandFlag(), CVC3::Clause::size(), TRACE, and TRACE_MSG.

Referenced by CVC3::SearchEngineFast::fixConflict().

QueryResult SearchEngineFast::checkValidMain ( const Expr e2)
private

Private helper function for checkValid and restart.

Definition at line 1624 of file search_fast.cpp.

References CVC3::SearchEngineFast::checkSAT(), CVC3::ExprHashMap< Data >::clear(), CVC3::SearchEngineFast::clearFacts(), CVC3::SearchEngineFast::clearLiterals(), CVC3::SearchImplBase::d_assumptions, CVC3::SearchImplBase::d_bottomScope, CVC3::SearchEngineFast::d_clauses, CVC3::SearchEngineFast::d_clausesQueryEnd, CVC3::SearchEngineFast::d_clausesQueryStart, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngineFast::d_conflictTheorem, CVC3::SearchEngine::d_core, CVC3::SearchEngineFast::d_factQueue, CVC3::SearchImplBase::d_lastCounterExample, CVC3::SearchImplBase::d_lastValid, CVC3::SearchEngineFast::d_literals, CVC3::SearchEngineFast::d_literalSet, CVC3::SearchEngineFast::d_nonLiterals, CVC3::SearchEngineFast::d_nonlitQueryEnd, CVC3::SearchEngineFast::d_nonlitQueryStart, CVC3::SearchEngineFast::d_simplifiedThm, CVC3::SearchEngineFast::d_unitConflictClauses, DebugAssert, CVC3::TheoryCore::getCM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLeafAssumptions(), IF_DEBUG(), CVC3::CommonProofRules::iffContrapositive(), CVC3::CommonProofRules::iffMP(), CVC3::Expr::isTrue(), CVC3::ContextManager::pop(), CVC3::ContextManager::popto(), CVC3::SearchImplBase::processResult(), CVC3::SATISFIABLE, CVC3::SearchImplBase::simplify(), CVC3::CommonProofRules::symmetryRule(), TRACE, TRACE_MSG, and CVC3::UNSATISFIABLE.

Referenced by CVC3::SearchEngineFast::checkValidInternal(), and CVC3::SearchEngineFast::restartInternal().

SearchEngineFast::SearchEngineFast ( TheoryCore core)
SearchEngineFast::~SearchEngineFast ( )
virtual

Destructor.

We own the proof rules (d_rules) and the variable manager (d_vm); delete them.

Definition at line 118 of file search_fast.cpp.

References CVC3::SearchEngineFast::d_circuits, CVC3::SearchEngineFast::d_conflictClauseStack, and CVC3::SearchEngineFast::d_decisionEngine.

const std::string& CVC3::SearchEngineFast::getName ( )
inlinevirtual

Name of this search engine.

Implements CVC3::SearchEngine.

Definition at line 390 of file search_fast.h.

References CVC3::SearchEngineFast::d_name.

QueryResult SearchEngineFast::checkValidInternal ( const Expr e)
virtual
QueryResult SearchEngineFast::restartInternal ( const Expr e)
virtual
void SearchEngineFast::getCounterExample ( std::vector< Expr > &  assertions)
virtual

Redefine the counterexample generation.

FIXME: for now, it just dumps all the assumptions (same as getAssumptions()). Eventually, it will simplify the related formulas to TRUE, merge all the generated assumptions into d_lastCounterExample, and call the parent's method.

Definition at line 1424 of file search_fast.cpp.

References CVC3::SearchImplBase::getAssumptions(), and CVC3::SearchImplBase::getCounterExample().

void SearchEngineFast::addLiteralFact ( const Theorem thm)
virtual
void SearchEngineFast::addNonLiteralFact ( const Theorem thm)
virtual
Theorem SearchEngineFast::newIntAssumption ( const Expr e)
virtual
bool SearchEngineFast::isAssumption ( const Expr e)
virtual

Check if the formula has been assumed.

Reimplemented from CVC3::SearchImplBase.

Definition at line 1594 of file search_fast.cpp.

References CVC3::SearchEngineFast::d_nonLiteralsSaved, and CVC3::SearchImplBase::isAssumption().

void SearchEngineFast::addSplitter ( const Expr e,
int  priority 
)
virtual

Suggest a splitter to the SearchEngine.

The higher is the priority, the sooner the SAT solver will split on it. It can be positive or negative (default is 0).

The set of suggested splitters is backtracking; that is, a splitter is "forgotten" once the scope is backtracked.

This method can be used either to change the priority of existing splitters, or to introduce new splitters that DPs consider relevant, even though they do not appear in existing formulas.

Reimplemented from CVC3::SearchImplBase.

Definition at line 1601 of file search_fast.cpp.

References compareLits(), CVC3::SearchImplBase::d_dpSplitters, CVC3::SearchEngineFast::d_litsByScores, CVC3::SearchEngineFast::d_litSortCount, DebugAssert, CVC3::Expr::isAbsLiteral(), CVC3::SearchImplBase::newLiteral(), CVC3::Expr::toString(), and TRACE.

Variable Documentation

std::string CVC3::SearchEngineFast::d_name
private

Name.

Definition at line 95 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::getName().

DecisionEngine* CVC3::SearchEngineFast::d_decisionEngine
private
StatCounter CVC3::SearchEngineFast::d_unitPropCount
private

Total number of unit propagations.

Definition at line 99 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::propagate().

StatCounter CVC3::SearchEngineFast::d_circuitPropCount
private

Total number of circuit propagations.

Definition at line 101 of file search_fast.h.

Referenced by CVC3::Circuit::propagate().

StatCounter CVC3::SearchEngineFast::d_conflictCount
private

Total number of conflicts.

Definition at line 103 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::fixConflict().

StatCounter CVC3::SearchEngineFast::d_conflictClauseCount
private

Total number of conflict clauses generated (not all may be active)

Definition at line 105 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::analyzeUIPs().

CDList<ClauseOwner> CVC3::SearchEngineFast::d_clauses
private

Backtrackable list of clauses.

New clauses may come into play from the decision procedures that are context dependent.

Definition at line 110 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addNewClause(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchEngineFast::checkValidMain(), and CVC3::SearchEngineFast::SearchEngineFast().

CDMap<Expr,Theorem> CVC3::SearchEngineFast::d_unreportedLits
private

Backtrackable set of pending unprocessed literals.

These can be discovered at any scope level during conflict analysis.

Definition at line 115 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::recordFact().

CDMap<Expr,bool> CVC3::SearchEngineFast::d_unreportedLitsHandled
private

Definition at line 116 of file search_fast.h.

CDList<SmartCDO<Theorem> > CVC3::SearchEngineFast::d_nonLiterals
private

Backtrackable list of non-literals (non-CNF formulas).

We treat nonliterals like clauses, because they are a superset of clauses. We stick the real clauses into d_clauses, but all the rest have to be stored elsewhere.

Definition at line 122 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchEngineFast::findSplitter(), and CVC3::SearchEngineFast::SearchEngineFast().

CDMap<Expr,Theorem> CVC3::SearchEngineFast::d_nonLiteralsSaved
private

prevent reprocessing

Definition at line 123 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), and CVC3::SearchEngineFast::isAssumption().

CDO<Theorem> CVC3::SearchEngineFast::d_simplifiedThm
private

Theorem which records simplification of the last query.

Definition at line 127 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchEngineFast::checkValidMain(), and CVC3::SearchEngineFast::restartInternal().

CDO<unsigned> CVC3::SearchEngineFast::d_nonlitQueryStart
private

Size of d_nonLiterals before most recent query.

Definition at line 130 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::checkValidInternal(), and CVC3::SearchEngineFast::checkValidMain().

CDO<unsigned> CVC3::SearchEngineFast::d_nonlitQueryEnd
private

Size of d_nonLiterals after query (not including DP-generated non-literals)

Definition at line 132 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::checkValidInternal(), and CVC3::SearchEngineFast::checkValidMain().

CDO<unsigned> CVC3::SearchEngineFast::d_clausesQueryStart
private

Size of d_clauses before most recent query.

Definition at line 134 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::checkValidInternal(), and CVC3::SearchEngineFast::checkValidMain().

CDO<unsigned> CVC3::SearchEngineFast::d_clausesQueryEnd
private

Size of d_clauses after query.

Definition at line 136 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::checkValidInternal(), and CVC3::SearchEngineFast::checkValidMain().

std::vector<std::deque<ClauseOwner>* > CVC3::SearchEngineFast::d_conflictClauseStack
private

Array of conflict clauses: one deque for each outstanding query.

Definition at line 139 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::SearchEngineFast(), and CVC3::SearchEngineFast::~SearchEngineFast().

std::deque<ClauseOwner>* CVC3::SearchEngineFast::d_conflictClauses
private

Reference to top deque of conflict clauses.

Definition at line 141 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::findSplitter(), and CVC3::SearchEngineFast::SearchEngineFast().

ConflictClauseManager CVC3::SearchEngineFast::d_conflictClauseManager
private

Definition at line 159 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::checkValidInternal().

std::vector<Clause> CVC3::SearchEngineFast::d_unitConflictClauses
private

Unprocessed unit conflict clauses.

When we find unit conflict clauses, we are automatically going to jump back to the original scope. Hopefully we won't find multiple ones, but you never know with those wacky decision procedures just spitting new information out. These are then directly asserted then promptly forgotten about. Chaff keeps them around (for correctness maybe), but we already have the proofs stored in the literals themselves.

Definition at line 169 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchEngineFast::fixConflict(), and CVC3::SearchEngineFast::restartInternal().

std::vector<Literal> CVC3::SearchEngineFast::d_literals
private

Set of literals to be processed by bcp.

These are emptied out upon backtracking, because they can only be valid if they were already all processed without conflicts. Therefore, they don't need to be context dependent.

Definition at line 176 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchEngineFast::clearLiterals(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::Circuit::propagate(), CVC3::SearchEngineFast::split(), and CVC3::SearchEngineFast::unitPropagation().

CDMap<Expr,Literal> CVC3::SearchEngineFast::d_literalSet
private

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

When a literal is asserted outside of checkValid() call, its value is remembered in a Literal database, but the literal queue for BCP is cleared. We add literals to this set at the proper scope levels, and propagate them at the beginning of a checkValid() call.

Definition at line 185 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addLiteralFact(), and CVC3::SearchEngineFast::checkValidMain().

std::vector<Theorem> CVC3::SearchEngineFast::d_factQueue
private
bool CVC3::SearchEngineFast::d_useEnqueueFact
private
bool CVC3::SearchEngineFast::d_inCheckSAT
private

True when checkSAT() is running.

Used by addLiteralFact() to determine whether to BCP the literals immediately (outside of checkSAT()) or not.

Definition at line 198 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addLiteralFact(), and CVC3::SearchEngineFast::checkSAT().

CDList<Literal> CVC3::SearchEngineFast::d_litsAlive
private

Set of alive literals that shouldn't be garbage-collected.

Unfortunately, I have a keep-alive issue. I think literals actually have to hang around, so I assert them to a separate d_litsAlive CDList.

Definition at line 205 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::bcp(), and CVC3::SearchEngineFast::newIntAssumption().

std::vector<Circuit*> CVC3::SearchEngineFast::d_circuits
private

Mappings of literals to vectors of pointers to the corresponding watched literals.

A pointer is a pair (clause,i), where 'i' in {0,1} is the index of the watch pointer in the clause.

Definition at line 214 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), and CVC3::SearchEngineFast::~SearchEngineFast().

ExprHashMap<std::vector<Circuit*> > CVC3::SearchEngineFast::d_circuitsByExpr
private

Definition at line 215 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::bcp(), and CVC3::Circuit::Circuit().

int CVC3::SearchEngineFast::d_lastConflictScope
private

The scope of the last conflict.

This is the true scope of the conflict, not necessarily the scope where the conflict was detected.

Definition at line 220 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::fixConflict(), and CVC3::SearchEngineFast::traceConflict().

Clause CVC3::SearchEngineFast::d_lastConflictClause
private

The last conflict clause (for checkSAT()). May be Null.

It records which conflict clause must be processed by BCP after backtracking from a conflict. A conflict may generate several conflict clauses, but only one of them will cause a unit propagation.

Definition at line 227 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), and CVC3::SearchEngineFast::fixConflict().

Theorem CVC3::SearchEngineFast::d_conflictTheorem
private
unsigned CVC3::SearchEngineFast::d_litsMaxScorePos
private

Position of a literal with max score in d_litsByScores.

Definition at line 258 of file search_fast.h.

std::vector<Literal> CVC3::SearchEngineFast::d_litsByScores
private

Vector of literals sorted by score.

Definition at line 260 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addSplitter(), CVC3::SearchEngineFast::findSplitter(), and CVC3::SearchEngineFast::updateLitCounts().

int CVC3::SearchEngineFast::d_splitterCount
private
int CVC3::SearchEngineFast::d_litSortCount
private

Internal (decrementing) count of added splitters, to sort d_litByScores.

Definition at line 272 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::addSplitter(), and CVC3::SearchEngineFast::updateLitCounts().

const bool CVC3::SearchEngineFast::d_berkminFlag
private

Flag to switch on/off the berkmin heuristic.

Definition at line 275 of file search_fast.h.

Referenced by CVC3::SearchEngineFast::findSplitter().

Friends

friend class ConflictClauseManager
friend

Helper class for managing conflict clauses.

Conflict clauses should only get popped when the context in which a call to checkValid originates is popped. This helper class checks every time there's a pop to see if the conflict clauses need to be restored.

Definition at line 149 of file search_fast.h.