CVCL::SearchEngineFast Class Reference
[Fast Search Engine]

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

#include <search_fast.h>

Inheritance diagram for CVCL::SearchEngineFast:

[legend]Collaboration diagram for CVCL::SearchEngineFast:

[legend]List of all members.

Public Member Functions

SearchEngineFast (TheoryCore *core)
The main Constructor.
virtual ~SearchEngineFast ()
Destructor.
const std::string & getName ()
Name of this search engine.
virtual bool checkValidInternal (const Expr &e)
Implementation of the API call.
virtual bool 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.
bool 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.
IF_DEBUG (void fullCheck())
Go through all the clauses and check the watch pointers (for debugging).
void addNewClause (Clause &c)
Set up the watch pointers for the new clause.
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.
bool 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.

Classes

class ConflictClauseManager

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, CVCL 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 77 of file search_fast.h.

Constructor & Destructor Documentation

SearchEngineFast::SearchEngineFast ( TheoryCore * core )

The main Constructor.

Definition at line 79 of file search_fast.cpp.
References d_clauses, d_conflictClauses, d_conflictClauseStack, d_decisionEngine, d_nonLiterals, CVCL::TheoryCore::getFlags(), and IF_DEBUG().

SearchEngineFast::~SearchEngineFast ( ) [virtual]

Destructor.
We own the proof rules (d_rules) and the variable manager (d_vm); delete them.
Definition at line 125 of file search_fast.cpp.
References d_circuits, d_conflictClauseStack, and d_decisionEngine.

Member Function Documentation

Theorem CVCL::SearchEngineFast::processConflict ( const Literal & l ) [private]

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

Theorem CVCL::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]

Auxiliary function for unit propagation.

Definition at line 824 of file search_fast.cpp.
References CVCL::SearchEngineRules::conflictRule(), d_conflictTheorem, CVCL::SearchEngine::d_rules, d_unitPropCount, CVCL::Clause::dir(), CVCL::Literal::getExpr(), CVCL::Clause::getTheorem(), CVCL::Literal::getValue(), CVCL::int2string(), CVCL::Expr::isAbsLiteral(), CVCL::Clause::markSat(), CVCL::Clause::size(), CVCL::Expr::toString(), CVCL::Clause::toString(), CVCL::TRACE, unitPropagation(), CVCL::Clause::watched(), wp(), and CVCL::Clause::wp().
Referenced by bcp().

void SearchEngineFast::unitPropagation ( const Clause & c,

unsigned idx

) [private]

Do the unit propagation for the clause.

Definition at line 923 of file search_fast.cpp.
References d_literals, CVCL::SearchEngine::d_rules, enqueueFact(), CVCL::Theorem::getExpr(), CVCL::Clause::getTheorem(), CVCL::Literal::getValue(), CVCL::int2string(), CVCL::Theorem::isAbsLiteral(), CVCL::SearchImplBase::newLiteral(), CVCL::Clause::size(), CVCL::Literal::toString(), CVCL::Expr::toString(), CVCL::Clause::toString(), and CVCL::SearchEngineRules::unitProp().
Referenced by fixConflict(), and propagate().

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

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.

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.

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 1274 of file search_fast.cpp.
References CVCL::Assumptions::begin(), CVCL::Theorem::clearAllFlags(), CVCL::SearchEngineRules::conflictClause(), CVCL::Debug::counter(), CVCL::SearchImplBase::d_bottomScope, d_conflictClauseCount, d_conflictClauses, CVCL::SearchEngine::d_core, d_lastConflictClause, d_lastConflictScope, CVCL::SearchEngine::d_rules, d_unitConflictClauses, CVCL::SearchImplBase::d_vm, CVCL::debugger, CVCL::Assumptions::end(), std::endl(), CVCL::Theorem::getAssumptionsRef(), CVCL::Theorem::getExpr(), CVCL::Debug::getOS(), CVCL::Clause::getScope(), IF_DEBUG(), CVCL::int2string(), CVCL::Clause::isNull(), CVCL::Theorem::printDebug(), processNode(), CVCL::Clause::size(), CVCL::Debug::trace(), CVCL::TRACE, updateLitCounts(), CVCL::Clause::watched(), wp(), and CVCL::Clause::wp().

CVCL::SearchEngineFast::IF_DEBUG ( void fullCheck() ) [private]

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

Referenced by addNonLiteralFact(), analyzeUIPs(), bcp(), checkValidMain(), findSplitter(), fixConflict(), recordFact(), SearchEngineFast(), setInconsistent(), split(), and traceConflict().

void SearchEngineFast::addNewClause ( Clause & c ) [private]

Set up the watch pointers for the new clause.

Definition at line 1077 of file search_fast.cpp.
References d_clauses, CVCL::CDList< T >::push_back(), CVCL::Clause::size(), updateLitCounts(), CVCL::Clause::watched(), wp(), and CVCL::Clause::wp().
Referenced by addNonLiteralFact().

void SearchEngineFast::recordFact ( const Theorem & thm ) [private]

Process a new derived fact (auxiliary function).

Definition at line 557 of file search_fast.cpp.
References CVCL::CommonProofRules::contradictionRule(), CVCL::Debug::counter(), CVCL::SearchEngine::d_commonRules, d_unreportedLits, CVCL::debugger, CVCL::Literal::deriveTheorem(), CVCL::Literal::getExpr(), CVCL::Theorem::getExpr(), CVCL::Literal::getScope(), CVCL::Theorem::getScope(), CVCL::Literal::getValue(), IF_DEBUG(), CVCL::CDMap< Key, Data, HashFcn >::insert(), CVCL::Literal::isNegative(), CVCL::SearchImplBase::newLiteral(), setInconsistent(), and CVCL::Literal::setValue().
Referenced by CVCL::Circuit::propagate().

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):

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

ASSUMPTIONS:

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 1845 of file search_fast.cpp.
References CVCL::Assumptions::begin(), CVCL::Theorem::clearAllFlags(), CVCL::SearchImplBase::d_bottomScope, d_decisionEngine, CVCL::Assumptions::end(), CVCL::Theorem::getAssumptionsRef(), CVCL::Theorem::getCachedValue(), CVCL::Theorem::getExpr(), CVCL::Literal::getScope(), CVCL::Theorem::getScope(), CVCL::Literal::getValue(), IF_DEBUG(), CVCL::int2string(), CVCL::Theorem::isAbsLiteral(), CVCL::Theorem::isAssump(), CVCL::Theorem::isFlagged(), CVCL::SearchImplBase::newLiteral(), CVCL::DecisionEngine::popTo(), CVCL::SearchImplBase::scopeLevel(), CVCL::Theorem::setCachedValue(), CVCL::Theorem::setExpandFlag(), CVCL::Theorem::setFlag(), CVCL::Theorem::setLitFlag(), CVCL::Theorem::toString(), CVCL::Expr::toString(), and CVCL::TRACE.
Referenced by fixConflict().

bool SearchEngineFast::checkValidMain ( const Expr & e2 ) [private]

Private helper function for checkValid and restart.

Definition at line 1632 of file search_fast.cpp.
References CVCL::CDMap< Key, Data, HashFcn >::begin(), checkAssumpDebug(), checkSAT(), CVCL::ExprHashMap< Data >::clear(), clearFacts(), clearLiterals(), CVCL::SearchImplBase::d_assumptions, CVCL::SearchImplBase::d_bottomScope, d_clauses, d_clausesQueryEnd, d_clausesQueryStart, CVCL::SearchEngine::d_commonRules, d_conflictTheorem, CVCL::SearchEngine::d_core, d_factQueue, CVCL::SearchImplBase::d_lastCounterExample, CVCL::SearchImplBase::d_lastValid, d_literals, d_literalSet, d_litsMaxScorePos, d_nonLiterals, d_nonlitQueryEnd, d_nonlitQueryStart, d_simplifiedThm, d_unitConflictClauses, CVCL::CDMap< Key, Data, HashFcn >::end(), CVCL::TheoryCore::getCM(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLeafAssumptions(), IF_DEBUG(), CVCL::CommonProofRules::iffContrapositive(), CVCL::CommonProofRules::iffMP(), CVCL::Expr::isTrue(), CVCL::ContextManager::pop(), CVCL::ContextManager::popto(), CVCL::SearchImplBase::processResult(), CVCL::SearchImplBase::simplify(), CVCL::CommonProofRules::symmetryRule(), and CVCL::TRACE.
Referenced by checkValidInternal(), and restartInternal().

const std::string& CVCL::SearchEngineFast::getName ( ) [inline, virtual]

Name of this search engine.

Implements CVCL::SearchEngine.
Definition at line 381 of file search_fast.h.
References d_name.

bool SearchEngineFast::checkValidInternal ( const Expr & e ) [virtual]

Implementation of the API call.

Implements CVCL::SearchImplBase.
Definition at line 1705 of file search_fast.cpp.
References checkValidMain(), CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::SearchImplBase::d_assumptions, CVCL::SearchImplBase::d_bottomScope, d_clauses, d_clausesQueryEnd, d_clausesQueryStart, d_conflictClauseManager, CVCL::SearchEngine::d_core, d_factQueue, d_nonLiterals, d_nonlitQueryEnd, d_nonlitQueryStart, d_simplifiedThm, d_splitterCount, d_unitConflictClauses, CVCL::CDO< T >::get(), CVCL::TheoryCore::getCM(), CVCL::TheoryCore::getExprTrans(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::negate(), CVCL::SearchImplBase::newUserAssumption(), CVCL::ExprTransform::preprocess(), CVCL::ContextManager::push(), CVCL::SearchImplBase::scopeLevel(), CVCL::SearchEngineFast::ConflictClauseManager::setRestorePoint(), CVCL::CDList< T >::size(), CVCL::Type::toString(), CVCL::Expr::toString(), and CVCL::TRACE.

bool SearchEngineFast::restartInternal ( const Expr & e ) [virtual]

Reruns last check with e as an additional assumption.

Implements CVCL::SearchImplBase.
Definition at line 1758 of file search_fast.cpp.
References CVCL::TheoryCore::addFact(), checkValidMain(), CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::SearchImplBase::d_assumptions, CVCL::SearchImplBase::d_bottomScope, CVCL::SearchEngine::d_core, d_factQueue, d_simplifiedThm, d_unitConflictClauses, CVCL::CDO< T >::get(), CVCL::TheoryCore::getCM(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::negate(), CVCL::SearchImplBase::newUserAssumption(), CVCL::ContextManager::popto(), CVCL::Type::toString(), CVCL::Expr::toString(), and CVCL::TRACE.

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 1432 of file search_fast.cpp.
References CVCL::SearchImplBase::getAssumptions(), and CVCL::SearchImplBase::getCounterExample().

void SearchEngineFast::addLiteralFact ( const Theorem & thm ) [virtual]

Notify the search engine about a new literal fact.
It should be called by TheoryCore::assertFactCore()
Implements CVCL::SearchImplBase.
Definition at line 1538 of file search_fast.cpp.
References bcp(), CVCL::CommonProofRules::contradictionRule(), CVCL::SearchEngine::d_commonRules, d_inCheckSAT, d_literals, d_literalSet, d_useEnqueueFact, CVCL::Literal::deriveTheorem(), CVCL::Literal::getExpr(), CVCL::Theorem::getExpr(), CVCL::Literal::getValue(), CVCL::CDMap< Key, Data, HashFcn >::insert(), CVCL::Expr::isAbsLiteral(), CVCL::Theorem::isAbsLiteral(), CVCL::Literal::isNegative(), CVCL::SearchImplBase::newLiteral(), CVCL::SearchImplBase::scopeLevel(), setInconsistent(), CVCL::Literal::setValue(), CVCL::Literal::toString(), CVCL::Expr::toString(), CVCL::Theorem::toString(), and CVCL::TRACE.
Referenced by enqueueFact(), and split().

void SearchEngineFast::addNonLiteralFact ( const Theorem & thm ) [virtual]

Notify the search engine about a new non-literal fact.
It should be called by TheoryCore::assertFactCore().
If the fact is an AND, we split it into individual conjuncts and add them individually.
If the fact is an OR, we check whether it's a CNF clause; that is, whether all disjuncts are literals. If they are, we add it as a CNF clause.
Otherwise add the fact to d_nonLiterals as it is.
Implements CVCL::SearchImplBase.
Definition at line 1453 of file search_fast.cpp.
References addNewClause(), CVCL::AND_R, CVCL::CommonProofRules::andElim(), CVCL::Expr::arity(), Circuit, CVCL::SearchEngineRules::conflictRule(), CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::Debug::counter(), d_circuits, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, d_nonLiterals, d_nonLiteralsSaved, CVCL::SearchEngine::d_rules, CVCL::SearchImplBase::d_vm, CVCL::debugger, CVCL::Literal::deriveTheorem(), CVCL::TheoryCore::enqueueFact(), CVCL::TheoryCore::getCM(), CVCL::ContextManager::getCurrentContext(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Literal::getValue(), IF_DEBUG(), CVCL::IFF_R, CVCL::int2string(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isAnd(), CVCL::Expr::isOr(), CVCL::ITE_R, CVCL::SearchImplBase::newLiteral(), CVCL::CDList< T >::push_back(), CVCL::SearchImplBase::scopeLevel(), setInconsistent(), CVCL::CDMap< Key, Data, HashFcn >::size(), CVCL::TRACE, and CVCL::SearchEngineRules::unitProp().

Theorem SearchEngineFast::newIntAssumption ( const Expr & e ) [virtual]

Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal.

Reimplemented from CVCL::SearchImplBase.
Definition at line 1581 of file search_fast.cpp.
References d_literals, d_litsAlive, CVCL::Literal::getExpr(), CVCL::Theorem::getExpr(), CVCL::Literal::getValue(), CVCL::Expr::isAbsLiteral(), CVCL::Theorem::isAssump(), CVCL::SearchImplBase::newIntAssumption(), CVCL::SearchImplBase::newLiteral(), CVCL::CDList< T >::push_back(), CVCL::SearchImplBase::scopeLevel(), CVCL::Literal::setValue(), CVCL::Literal::toString(), CVCL::Theorem::toString(), and CVCL::TRACE.

bool SearchEngineFast::isAssumption ( const Expr & e ) [virtual]

Check if the formula has been assumed.

Reimplemented from CVCL::SearchImplBase.
Definition at line 1602 of file search_fast.cpp.
References CVCL::CDMap< Key, Data, HashFcn >::count(), d_nonLiteralsSaved, and CVCL::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 CVCL::SearchImplBase.
Definition at line 1609 of file search_fast.cpp.
References CVCL::Literal::added(), compareLits(), CVCL::SearchImplBase::d_dpSplitters, d_litsByScores, d_litSortCount, CVCL::Expr::isAbsLiteral(), CVCL::SearchImplBase::newLiteral(), CVCL::CDList< T >::push_back(), CVCL::Literal::score(), CVCL::Expr::toString(), and CVCL::TRACE.

Friends And Related Function Documentation

friend class Circuit [friend]

Definition at line 79 of file search_fast.h.
Referenced by addNonLiteralFact().

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

Generated on Thu Apr 13 16:57:43 2006 for CVC Lite by

1.4.4

CVCL::SearchEngineFast Class Reference [Fast Search Engine]