22 #ifndef _cvc3__include__search_fast_h_
23 #define _cvc3__include__search_fast_h_
36 class VariableManager;
233 std::vector<std::pair<Clause, int> >&
wp(
const Literal& literal);
263 ExprHashMap<unsigned> d_litScores;
265 ExprHashMap<unsigned> d_litCounts;
267 ExprHashMap<unsigned> d_litCountPrev;
StatCounter d_conflictCount
Total number of conflicts.
std::vector< Literal > d_litsByScores
Vector of literals sorted by score.
CDO< unsigned > d_clausesQueryEnd
Size of d_clauses after query.
CDO< unsigned > d_nonlitQueryEnd
Size of d_nonLiterals after query (not including DP-generated non-literals)
void addSplitter(const Expr &e, int priority)
Suggest a splitter to the SearchEngine.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
void addLiteralFact(const Theorem &thm)
Notify the search engine about a new literal fact.
bool fixConflict()
Determines backtracking level and adds conflict clauses.
int d_litSortCount
Internal (decrementing) count of added splitters, to sort d_litByScores.
ExprHashMap< std::vector< Circuit * > > d_circuitsByExpr
bool split()
Choose a splitter.
StatCounter d_circuitPropCount
Total number of circuit propagations.
void recordFact(const Theorem &thm)
Process a new derived fact (auxiliary function)
std::vector< int > d_restorePoints
void clearLiterals()
Clear the list of asserted literals (d_literals)
void traceConflict(const Theorem &conflictThm)
First pass in conflict analysis; takes a theorem of FALSE.
CDMap< Expr, Theorem > d_unreportedLits
Backtrackable set of pending unprocessed literals.
void analyzeUIPs(const Theorem &falseThm, int conflictScope)
Analyse the conflict, find the UIPs, etc.
unsigned d_litsMaxScorePos
Position of a literal with max score in d_litsByScores.
int d_lastConflictScope
The scope of the last conflict.
void updateLitCounts(const Clause &c)
Add the literals of a new clause to d_litsByScores.
ConflictClauseManager d_conflictClauseManager
void enqueueFact(const Theorem &thm)
Queue up a fact to assert to the DPs later.
Theorem d_conflictTheorem
Theorem(FALSE) which generated a conflict.
CDMap< Expr, bool > d_unreportedLitsHandled
StatCounter d_conflictClauseCount
Total number of conflict clauses generated (not all may be active)
virtual QueryResult restartInternal(const Expr &e)
Reruns last check with e as an additional assumption.
void unitPropagation(const Clause &c, unsigned idx)
Do the unit propagation for the clause.
CDList< ClauseOwner > d_clauses
Backtrackable list of clauses.
CDMap< Expr, Theorem > d_nonLiteralsSaved
prevent reprocessing
Description: Counters and flags for collecting run-time statistics.
void updateLitScores(bool firstTime)
void commitFacts()
Commit all the enqueued facts to the DPs.
std::vector< Theorem > d_factQueue
Queue of derived facts to be sent to DPs.
virtual Theorem newIntAssumption(const Expr &e)
Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal.
CDO< unsigned > d_nonlitQueryStart
Size of d_nonLiterals before most recent query.
void setInconsistent(const Theorem &thm)
Set the context inconsistent. Takes Theorem(FALSE).
std::vector< std::deque< ClauseOwner > * > d_conflictClauseStack
Array of conflict clauses: one deque for each outstanding query.
CDMap< Expr, Literal > d_literalSet
Set of asserted literals which may survive accross checkValid() calls.
Abstract API to the proof search engine.
std::vector< Literal > d_literals
Set of literals to be processed by bcp.
const std::string & getName()
Name of this search engine.
ConflictClauseManager(Context *context, SearchEngineFast *se)
void addNewClause(Clause &c)
Go through all the clauses and check the watch pointers (for debugging)
std::vector< Circuit * > d_circuits
Mappings of literals to vectors of pointers to the corresponding watched literals.
CDO< Theorem > d_simplifiedThm
Theorem which records simplification of the last query.
void assertAssumptions()
FIXME: document this.
A class representing a CNF clause (a smart pointer)
Implementation of a faster search engine, using newer techniques.
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.
virtual ~SearchEngineFast()
Destructor.
void addNonLiteralFact(const Theorem &thm)
Notify the search engine about a new non-literal fact.
bool d_inCheckSAT
True when checkSAT() is running.
void clearFacts()
Clear the local fact queue.
SearchEngineFast(TheoryCore *core)
The main Constructor.
virtual QueryResult checkValidInternal(const Expr &e)
Implementation of the API call.
bool d_useEnqueueFact
When true, use TheoryCore::enqueueFact() instead of addFact() in commitFacts()
std::vector< Clause > d_unitConflictClauses
Unprocessed unit conflict clauses.
API to to a generic proof search engine (a.k.a. SAT solver)
QueryResult checkValidMain(const Expr &e2)
Private helper function for checkValid and restart.
CDO< unsigned > d_clausesQueryStart
Size of d_clauses before most recent query.
virtual bool isAssumption(const Expr &e)
Check if the formula has been assumed.
Expr findSplitter()
Returns a splitter.
bool bcp()
Boolean constraint propagation.
int d_splitterCount
Internal splitter counter for delaying updateLitScores()
Theorem processConflict(const Literal &l)
Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses...
CDList< SmartCDO< Theorem > > d_nonLiterals
Backtrackable list of non-literals (non-CNF formulas).
bool propagate(const Clause &c, int idx, bool &wpUpdated)
Auxiliary function for unit propagation.
CDList< Literal > d_litsAlive
Set of alive literals that shouldn't be garbage-collected.
Clause d_lastConflictClause
The last conflict clause (for checkSAT()). May be Null.
const bool d_berkminFlag
Flag to switch on/off the berkmin heuristic.
StatCounter d_unitPropCount
Total number of unit propagations.
std::deque< ClauseOwner > * d_conflictClauses
Reference to top deque of conflict clauses.
DecisionEngine * d_decisionEngine
Decision Engine.
Smart context-dependent object wrapper.
virtual void getCounterExample(std::vector< Expr > &assertions)
Redefine the counterexample generation.