Fast Search Engine
[Search Engine]

Collaboration diagram for Fast Search Engine:

Classes

• class CVCL::SearchEngineFast

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

• class CVCL::SearchEngineFast::ConflictClauseManager

Functions

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

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

• bool CVCL::SearchEngineFast::checkSAT ()
• bool CVCL::SearchEngineFast::split ()

  Choose a splitter.
  

• Expr CVCL::SearchEngineFast::findSplitter ()

  Returns a splitter.
  

• void CVCL::SearchEngineFast::clearLiterals ()

  Clear the list of asserted literals (d_literals).
  

• void CVCL::SearchEngineFast::updateLitScores (bool firstTime)
• void CVCL::SearchEngineFast::updateLitCounts (const Clause &c)

  Add the literals of a new clause to d_litsByScores.
  

• bool CVCL::SearchEngineFast::bcp ()

  Boolean constraint propagation.
  

• bool CVCL::SearchEngineFast::fixConflict ()

  Determines backtracking level and adds conflict clauses.
  

• void CVCL::SearchEngineFast::assertAssumptions ()

  FIXME: document this.
  

• void CVCL::SearchEngineFast::enqueueFact (const Theorem &thm)

  Queue up a fact to assert to the DPs later.
  

• void CVCL::SearchEngineFast::setInconsistent (const Theorem &thm)

  Set the context inconsistent. Takes Theorem(FALSE).
  

• void CVCL::SearchEngineFast::commitFacts ()

  Commit all the enqueued facts to the DPs.
  

• void CVCL::SearchEngineFast::clearFacts ()

  Clear the local fact queue.
  

Variables

• std::string CVCL::SearchEngineFast::d_name

  Name.
  

• DecisionEngine * CVCL::SearchEngineFast::d_decisionEngine

  Decision Engine.
  

• StatCounter CVCL::SearchEngineFast::d_unitPropCount

  Total number of unit propagations.
  

• StatCounter CVCL::SearchEngineFast::d_circuitPropCount

  Total number of circuit propagations.
  

• StatCounter CVCL::SearchEngineFast::d_conflictCount

  Total number of conflicts.
  

• StatCounter CVCL::SearchEngineFast::d_conflictClauseCount

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

• CDList< ClauseOwner > CVCL::SearchEngineFast::d_clauses

  Backtrackable list of clauses.
  

• CDMap< Expr, Theorem > CVCL::SearchEngineFast::d_unreportedLits

  Backtrackable set of pending unprocessed literals.
  

• CDMap< Expr, bool > CVCL::SearchEngineFast::d_unreportedLitsHandled
• CDList< SmartCDO< Theorem > > CVCL::SearchEngineFast::d_nonLiterals

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

• CDMap< Expr, Theorem > CVCL::SearchEngineFast::d_nonLiteralsSaved

  prevent reprocessing
  

• CDO< Theorem > CVCL::SearchEngineFast::d_simplifiedThm

  Theorem which records simplification of the last query.
  

• CDO< unsigned > CVCL::SearchEngineFast::d_nonlitQueryStart

  Size of d_nonLiterals before most recent query.
  

• CDO< unsigned > CVCL::SearchEngineFast::d_nonlitQueryEnd

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

• CDO< unsigned > CVCL::SearchEngineFast::d_clausesQueryStart

  Size of d_clauses before most recent query.
  

• CDO< unsigned > CVCL::SearchEngineFast::d_clausesQueryEnd

  Size of d_clauses after query.
  

• std::vector< std::deque< ClauseOwner > * > CVCL::SearchEngineFast::d_conflictClauseStack

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

• std::deque< ClauseOwner > * CVCL::SearchEngineFast::d_conflictClauses

  Reference to top deque of conflict clauses.
  

• ConflictClauseManager CVCL::SearchEngineFast::d_conflictClauseManager
• std::vector< Clause > CVCL::SearchEngineFast::d_unitConflictClauses

  Unprocessed unit conflict clauses.
  

• std::vector< Literal > CVCL::SearchEngineFast::d_literals

  Set of literals to be processed by bcp.
  

• CDMap< Expr, Literal > CVCL::SearchEngineFast::d_literalSet

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

• std::vector< Theorem > CVCL::SearchEngineFast::d_factQueue

  Queue of derived facts to be sent to DPs.
  

• bool CVCL::SearchEngineFast::d_useEnqueueFact

  When true, use TheoryCore::enqueueFact() instead of addFact() in commitFacts().
  

• bool CVCL::SearchEngineFast::d_inCheckSAT

  True when checkSAT() is running.
  

• CDList< Literal > CVCL::SearchEngineFast::d_litsAlive

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

• std::vector< Circuit * > CVCL::SearchEngineFast::d_circuits

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

• ExprHashMap< std::vector<
  Circuit * > > CVCL::SearchEngineFast::d_circuitsByExpr
• int CVCL::SearchEngineFast::d_lastConflictScope

  The scope of the last conflict.
  

• Clause CVCL::SearchEngineFast::d_lastConflictClause

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

• Theorem CVCL::SearchEngineFast::d_conflictTheorem

  Theorem(FALSE) which generated a conflict.
  

• unsigned CVCL::SearchEngineFast::d_litsMaxScorePos

  Position of a literal with max score in d_litsByScores.
  

• std::vector< Literal > CVCL::SearchEngineFast::d_litsByScores

  Vector of literals sorted by score.
  

• int CVCL::SearchEngineFast::d_splitterCount

  Internal splitter counter for delaying updateLitScores().
  

• int CVCL::SearchEngineFast::d_litSortCount

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

• const bool & CVCL::SearchEngineFast::d_berkminFlag

  Flag to switch on/off the berkmin heuristic.
  

---

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, inherited]

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 143 of file search_fast.cpp. References CVCL::Literal::wp(). Referenced by CVCL::SearchEngineFast::addNewClause(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchEngineFast::bcp(), and CVCL::SearchEngineFast::propagate().

bool SearchEngineFast::checkSAT (   )  [private, inherited]

Returns: true if SAT, false otherwise. When false is returned, proof is saved in d_lastConflictTheorem Definition at line 194 of file search_fast.cpp. References CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::d_decisionEngine, CVCL::SearchEngineFast::d_factQueue, CVCL::SearchEngineFast::d_inCheckSAT, CVCL::SearchEngineFast::fixConflict(), CVCL::DecisionEngine::goalSatisfied(), and CVCL::SearchEngineFast::split(). Referenced by CVCL::SearchEngineFast::checkValidMain().

bool SearchEngineFast::split (   )  [private, inherited]

Choose a splitter. Preconditions: The current context is consistent. Returns: true if splitter available, and it asserts it through newIntAssumption() after first pushing a new context. false if no splitters are available, which means the context is SAT. Postconditions: A literal has been asserted through newIntAssumption(). Definition at line 262 of file search_fast.cpp. References CVCL::TheoryCore::addFact(), CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::bcp(), CVCL::TheoryCore::checkSATCore(), CVCL::Statistics::counter(), CVCL::Debug::counter(), CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, CVCL::SearchEngineFast::d_decisionEngine, CVCL::SearchEngineFast::d_literals, CVCL::SearchEngineFast::d_splitterCount, CVCL::debugger, CVCL::Literal::deriveTheorem(), CVCL::SearchEngineFast::findSplitter(), CVCL::Theorem::getExpr(), CVCL::Theorem::getRHS(), CVCL::TheoryCore::getStatistics(), CVCL::Literal::getValue(), CVCL::SearchEngineFast::IF_DEBUG(), CVCL::CommonProofRules::iffFalseElim(), CVCL::CommonProofRules::iffTrueElim(), CVCL::TheoryCore::inconsistent(), CVCL::int2string(), CVCL::Expr::isBoolConst(), CVCL::Expr::isNot(), CVCL::Expr::isNull(), CVCL::Expr::isTrue(), CVCL::SearchImplBase::newLiteral(), CVCL::CommonProofRules::notNotElim(), CVCL::DecisionEngine::pushDecision(), CVCL::TheoryCore::simplify(), CVCL::Literal::toString(), CVCL::Expr::toString(), and CVCL::TRACE. Referenced by CVCL::SearchEngineFast::checkSAT().

Expr SearchEngineFast::findSplitter (   )  [private, inherited]

Returns a splitter. Definition at line 446 of file search_fast.cpp. References CVCL::Debug::counter(), CVCL::SearchEngineFast::d_berkminFlag, CVCL::SearchEngineFast::d_conflictClauses, CVCL::SearchEngine::d_core, CVCL::SearchEngineFast::d_decisionEngine, CVCL::SearchEngineFast::d_litsByScores, CVCL::SearchEngineFast::d_litsMaxScorePos, CVCL::SearchEngineFast::d_nonLiterals, CVCL::SearchEngineFast::d_splitterCount, CVCL::debugger, CVCL::DecisionEngine::findSplitter(), CVCL::Literal::getExpr(), CVCL::Literal::getValue(), CVCL::SearchEngineFast::IF_DEBUG(), CVCL::int2string(), CVCL::Expr::isBoolConst(), CVCL::SearchImplBase::isGoodSplitter(), CVCL::Expr::isNull(), CVCL::Expr::isTrue(), CVCL::Literal::score(), CVCL::Theory::simplifyExpr(), CVCL::CDList< T >::size(), CVCL::Clause::size(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::SearchEngineFast::updateLitScores(). Referenced by CVCL::SearchEngineFast::split().

void SearchEngineFast::clearLiterals (   )  [private, inherited]

Clear the list of asserted literals (d_literals). Definition at line 639 of file search_fast.cpp. References CVCL::SearchEngineFast::d_literals. Referenced by CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::checkValidMain(), and CVCL::SearchEngineFast::fixConflict().

void SearchEngineFast::updateLitScores (  bool  firstTime  )  [private, inherited]

Recompute the scores for all known literals. This is a relatively expensive procedure, so it should not be called too often. Currently, it is called once per 100 splitters. Definition at line 353 of file search_fast.cpp. References CVCL::Literal::added(), compareLits(), CVCL::Literal::count(), CVCL::Literal::countPrev(), CVCL::SearchEngineFast::d_litsByScores, CVCL::SearchEngineFast::d_litsMaxScorePos, CVCL::SearchEngineFast::d_litSortCount, CVCL::int2string(), CVCL::Literal::score(), CVCL::Literal::toString(), and CVCL::TRACE. Referenced by CVCL::SearchEngineFast::findSplitter().

void SearchEngineFast::updateLitCounts (  const Clause &  c  )  [private, inherited]

Add the literals of a new clause to d_litsByScores. Definition at line 420 of file search_fast.cpp. References CVCL::Literal::added(), compareLits(), CVCL::SearchEngineFast::d_litsByScores, CVCL::SearchEngineFast::d_litSortCount, CVCL::Literal::getExpr(), CVCL::Expr::isAbsLiteral(), CVCL::Clause::size(), and CVCL::TRACE. Referenced by CVCL::SearchEngineFast::addNewClause(), and CVCL::SearchEngineFast::analyzeUIPs().

bool SearchEngineFast::bcp (   )  [private, inherited]

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 645 of file search_fast.cpp. References CVCL::SearchEngineFast::clearFacts(), CVCL::SearchEngineFast::clearLiterals(), CVCL::SearchEngineFast::commitFacts(), CVCL::Debug::counter(), CVCL::SearchEngineFast::d_circuitsByExpr, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngineFast::d_conflictTheorem, CVCL::SearchEngine::d_core, CVCL::SearchEngineFast::d_factQueue, CVCL::SearchEngineFast::d_literals, CVCL::SearchEngineFast::d_litsAlive, CVCL::SearchEngineFast::d_nonLiterals, CVCL::debugger, CVCL::Clause::deleted(), CVCL::SearchEngineFast::enqueueFact(), CVCL::Theorem::getExpr(), CVCL::Literal::getExpr(), CVCL::TheoryCore::getFlags(), CVCL::Literal::getValue(), CVCL::SearchEngineFast::IF_DEBUG(), CVCL::TheoryCore::inconsistent(), CVCL::TheoryCore::inconsistentThm(), CVCL::int2string(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isExists(), CVCL::Expr::isFalse(), CVCL::Expr::isTrue(), CVCL::SearchEngineFast::propagate(), CVCL::CDList< T >::push_back(), CVCL::Clause::sat(), CVCL::SearchImplBase::scopeLevel(), CVCL::SearchEngineFast::setInconsistent(), CVCL::SearchImplBase::simplify(), CVCL::CDList< T >::size(), CVCL::CommonProofRules::skolemize(), CVCL::Literal::toString(), CVCL::TRACE, CVCL::Clause::watched(), and CVCL::SearchEngineFast::wp(). Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::checkSAT(), and CVCL::SearchEngineFast::split().

bool SearchEngineFast::fixConflict (   )  [private, inherited]

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 947 of file search_fast.cpp. References CVCL::SearchEngineFast::clearLiterals(), CVCL::SearchEngineFast::commitFacts(), CVCL::SearchImplBase::d_bottomScope, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngineFast::d_conflictCount, CVCL::SearchEngineFast::d_conflictTheorem, CVCL::SearchEngineFast::d_decisionEngine, CVCL::SearchEngineFast::d_lastConflictClause, CVCL::SearchEngineFast::d_lastConflictScope, CVCL::SearchEngineFast::d_litsMaxScorePos, CVCL::SearchEngineFast::d_unitConflictClauses, CVCL::debugger, CVCL::SearchEngineFast::enqueueFact(), CVCL::Literal::getExpr(), CVCL::Theorem::getExpr(), CVCL::Clause::getScope(), CVCL::Theorem::getScope(), CVCL::Clause::getTheorem(), CVCL::SearchEngineFast::IF_DEBUG(), CVCL::CommonProofRules::iffMP(), CVCL::int2string(), CVCL::Expr::isNull(), CVCL::Clause::isNull(), CVCL::Expr::isOr(), CVCL::DecisionEngine::popTo(), CVCL::Theorem::printDebug(), CVCL::CommonProofRules::rewriteOr(), CVCL::SearchImplBase::scopeLevel(), CVCL::Clause::size(), CVCL::Clause::toString(), CVCL::Literal::toString(), CVCL::Debug::trace(), CVCL::TRACE, CVCL::SearchEngineFast::traceConflict(), and CVCL::SearchEngineFast::unitPropagation(). Referenced by CVCL::SearchEngineFast::checkSAT().

void CVCL::SearchEngineFast::assertAssumptions (   )  [private, inherited]

FIXME: document this.

void SearchEngineFast::enqueueFact (  const Theorem &  thm  )  [private, inherited]

Queue up a fact to assert to the DPs later. Definition at line 1039 of file search_fast.cpp. References CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::d_factQueue, CVCL::Theorem::getExpr(), CVCL::Theorem::isAbsLiteral(), and CVCL::TRACE. Referenced by CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::fixConflict(), and CVCL::SearchEngineFast::unitPropagation().

void SearchEngineFast::setInconsistent (  const Theorem &  thm  )  [private, inherited]

Set the context inconsistent. Takes Theorem(FALSE). Definition at line 1051 of file search_fast.cpp. References CVCL::Debug::counter(), CVCL::SearchEngine::d_core, CVCL::SearchEngineFast::d_factQueue, CVCL::debugger, CVCL::SearchEngineFast::IF_DEBUG(), and CVCL::TheoryCore::setInconsistent(). Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchEngineFast::bcp(), and CVCL::SearchEngineFast::recordFact().

void SearchEngineFast::commitFacts (   )  [private, inherited]

Commit all the enqueued facts to the DPs. Definition at line 1058 of file search_fast.cpp. References CVCL::TheoryCore::addFact(), CVCL::SearchEngine::d_core, CVCL::SearchEngineFast::d_factQueue, CVCL::SearchEngineFast::d_useEnqueueFact, CVCL::TheoryCore::enqueueFact(), and CVCL::TRACE. Referenced by CVCL::SearchEngineFast::bcp(), and CVCL::SearchEngineFast::fixConflict().

void SearchEngineFast::clearFacts (   )  [private, inherited]

Clear the local fact queue. Definition at line 1071 of file search_fast.cpp. References CVCL::SearchEngineFast::d_factQueue. Referenced by CVCL::SearchEngineFast::bcp(), and CVCL::SearchEngineFast::checkValidMain().

---

Variable Documentation

std::string CVCL::SearchEngineFast::d_name [private, inherited]

Name. Definition at line 86 of file search_fast.h. Referenced by CVCL::SearchEngineFast::getName().

DecisionEngine* CVCL::SearchEngineFast::d_decisionEngine [private, inherited]

Decision Engine. Definition at line 88 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkSAT(), CVCL::SearchEngineFast::findSplitter(), CVCL::SearchEngineFast::fixConflict(), CVCL::SearchEngineFast::SearchEngineFast(), CVCL::SearchEngineFast::split(), CVCL::SearchEngineFast::traceConflict(), and CVCL::SearchEngineFast::~SearchEngineFast().

StatCounter CVCL::SearchEngineFast::d_unitPropCount [private, inherited]

Total number of unit propagations. Definition at line 90 of file search_fast.h. Referenced by CVCL::SearchEngineFast::propagate().

StatCounter CVCL::SearchEngineFast::d_circuitPropCount [private, inherited]

Total number of circuit propagations. Definition at line 92 of file search_fast.h. Referenced by CVCL::Circuit::propagate().

StatCounter CVCL::SearchEngineFast::d_conflictCount [private, inherited]

Total number of conflicts. Definition at line 94 of file search_fast.h. Referenced by CVCL::SearchEngineFast::fixConflict().

StatCounter CVCL::SearchEngineFast::d_conflictClauseCount [private, inherited]

Total number of conflict clauses generated (not all may be active). Definition at line 96 of file search_fast.h. Referenced by CVCL::SearchEngineFast::analyzeUIPs().

CDList<ClauseOwner> CVCL::SearchEngineFast::d_clauses [private, inherited]

Backtrackable list of clauses. New clauses may come into play from the decision procedures that are context dependent. Definition at line 101 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addNewClause(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngineFast::checkValidMain(), and CVCL::SearchEngineFast::SearchEngineFast().

CDMap<Expr,Theorem> CVCL::SearchEngineFast::d_unreportedLits [private, inherited]

Backtrackable set of pending unprocessed literals. These can be discovered at any scope level during conflict analysis. Definition at line 106 of file search_fast.h. Referenced by CVCL::SearchEngineFast::recordFact().

CDMap<Expr,bool> CVCL::SearchEngineFast::d_unreportedLitsHandled [private, inherited]

Definition at line 107 of file search_fast.h.

CDList<SmartCDO<Theorem> > CVCL::SearchEngineFast::d_nonLiterals [private, inherited]

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 113 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngineFast::findSplitter(), and CVCL::SearchEngineFast::SearchEngineFast().

CDMap<Expr,Theorem> CVCL::SearchEngineFast::d_nonLiteralsSaved [private, inherited]

prevent reprocessing Definition at line 114 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), and CVCL::SearchEngineFast::isAssumption().

CDO<Theorem> CVCL::SearchEngineFast::d_simplifiedThm [private, inherited]

Theorem which records simplification of the last query. Definition at line 118 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngineFast::checkValidMain(), and CVCL::SearchEngineFast::restartInternal().

CDO<unsigned> CVCL::SearchEngineFast::d_nonlitQueryStart [private, inherited]

Size of d_nonLiterals before most recent query. Definition at line 121 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkValidInternal(), and CVCL::SearchEngineFast::checkValidMain().

CDO<unsigned> CVCL::SearchEngineFast::d_nonlitQueryEnd [private, inherited]

Size of d_nonLiterals after query (not including DP-generated non-literals). Definition at line 123 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkValidInternal(), and CVCL::SearchEngineFast::checkValidMain().

CDO<unsigned> CVCL::SearchEngineFast::d_clausesQueryStart [private, inherited]

Size of d_clauses before most recent query. Definition at line 125 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkValidInternal(), and CVCL::SearchEngineFast::checkValidMain().

CDO<unsigned> CVCL::SearchEngineFast::d_clausesQueryEnd [private, inherited]

Size of d_clauses after query. Definition at line 127 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkValidInternal(), and CVCL::SearchEngineFast::checkValidMain().

std::vector<std::deque<ClauseOwner>* > CVCL::SearchEngineFast::d_conflictClauseStack [private, inherited]

Array of conflict clauses: one deque for each outstanding query. Definition at line 130 of file search_fast.h. Referenced by CVCL::SearchEngineFast::ConflictClauseManager::notify(), CVCL::SearchEngineFast::SearchEngineFast(), CVCL::SearchEngineFast::ConflictClauseManager::setRestorePoint(), and CVCL::SearchEngineFast::~SearchEngineFast().

std::deque<ClauseOwner>* CVCL::SearchEngineFast::d_conflictClauses [private, inherited]

Reference to top deque of conflict clauses. Definition at line 132 of file search_fast.h. Referenced by CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchEngineFast::findSplitter(), CVCL::SearchEngineFast::ConflictClauseManager::notify(), CVCL::SearchEngineFast::SearchEngineFast(), and CVCL::SearchEngineFast::ConflictClauseManager::setRestorePoint().

ConflictClauseManager CVCL::SearchEngineFast::d_conflictClauseManager [private, inherited]

Definition at line 150 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkValidInternal().

std::vector<Clause> CVCL::SearchEngineFast::d_unitConflictClauses [private, inherited]

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 160 of file search_fast.h. Referenced by CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngineFast::fixConflict(), and CVCL::SearchEngineFast::restartInternal().

std::vector<Literal> CVCL::SearchEngineFast::d_literals [private, inherited]

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 167 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngineFast::clearLiterals(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::Circuit::propagate(), CVCL::SearchEngineFast::split(), and CVCL::SearchEngineFast::unitPropagation().

CDMap<Expr,Literal> CVCL::SearchEngineFast::d_literalSet [private, inherited]

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 176 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addLiteralFact(), and CVCL::SearchEngineFast::checkValidMain().

std::vector<Theorem> CVCL::SearchEngineFast::d_factQueue [private, inherited]

Queue of derived facts to be sent to DPs. See also: addFact() and commitFacts() Definition at line 180 of file search_fast.h. Referenced by CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::checkSAT(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngineFast::clearFacts(), CVCL::SearchEngineFast::commitFacts(), CVCL::SearchEngineFast::enqueueFact(), CVCL::SearchEngineFast::restartInternal(), and CVCL::SearchEngineFast::setInconsistent().

bool CVCL::SearchEngineFast::d_useEnqueueFact [private, inherited]

When true, use TheoryCore::enqueueFact() instead of addFact() in commitFacts(). Definition at line 184 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addLiteralFact(), and CVCL::SearchEngineFast::commitFacts().

bool CVCL::SearchEngineFast::d_inCheckSAT [private, inherited]

True when checkSAT() is running. Used by addLiteralFact() to determine whether to BCP the literals immediately (outside of checkSAT()) or not. Definition at line 189 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addLiteralFact(), and CVCL::SearchEngineFast::checkSAT().

CDList<Literal> CVCL::SearchEngineFast::d_litsAlive [private, inherited]

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 196 of file search_fast.h. Referenced by CVCL::SearchEngineFast::bcp(), and CVCL::SearchEngineFast::newIntAssumption().

std::vector<Circuit*> CVCL::SearchEngineFast::d_circuits [private, inherited]

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 205 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), and CVCL::SearchEngineFast::~SearchEngineFast().

ExprHashMap<std::vector<Circuit*> > CVCL::SearchEngineFast::d_circuitsByExpr [private, inherited]

Definition at line 206 of file search_fast.h. Referenced by CVCL::SearchEngineFast::bcp(), and CVCL::Circuit::Circuit().

int CVCL::SearchEngineFast::d_lastConflictScope [private, inherited]

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 211 of file search_fast.h. Referenced by CVCL::SearchEngineFast::analyzeUIPs(), and CVCL::SearchEngineFast::fixConflict().

Clause CVCL::SearchEngineFast::d_lastConflictClause [private, inherited]

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 218 of file search_fast.h. Referenced by CVCL::SearchEngineFast::analyzeUIPs(), and CVCL::SearchEngineFast::fixConflict().

Theorem CVCL::SearchEngineFast::d_conflictTheorem [private, inherited]

Theorem(FALSE) which generated a conflict. Definition at line 220 of file search_fast.h. Referenced by CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngineFast::fixConflict(), CVCL::SearchEngineFast::propagate(), and CVCL::Circuit::propagate().

unsigned CVCL::SearchEngineFast::d_litsMaxScorePos [private, inherited]

Position of a literal with max score in d_litsByScores. Definition at line 249 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngineFast::findSplitter(), CVCL::SearchEngineFast::fixConflict(), and CVCL::SearchEngineFast::updateLitScores().

std::vector<Literal> CVCL::SearchEngineFast::d_litsByScores [private, inherited]

Vector of literals sorted by score. Definition at line 251 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addSplitter(), CVCL::SearchEngineFast::findSplitter(), CVCL::SearchEngineFast::updateLitCounts(), and CVCL::SearchEngineFast::updateLitScores().

int CVCL::SearchEngineFast::d_splitterCount [private, inherited]

Internal splitter counter for delaying updateLitScores(). Definition at line 261 of file search_fast.h. Referenced by CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngineFast::findSplitter(), and CVCL::SearchEngineFast::split().

int CVCL::SearchEngineFast::d_litSortCount [private, inherited]

Internal (decrementing) count of added splitters, to sort d_litByScores. Definition at line 263 of file search_fast.h. Referenced by CVCL::SearchEngineFast::addSplitter(), CVCL::SearchEngineFast::updateLitCounts(), and CVCL::SearchEngineFast::updateLitScores().

const bool& CVCL::SearchEngineFast::d_berkminFlag [private, inherited]

Flag to switch on/off the berkmin heuristic. Definition at line 266 of file search_fast.h. Referenced by CVCL::SearchEngineFast::findSplitter().

---