CVC3
2.4.1
|
Implementation of a faster search engine, using newer techniques. More...
#include <search_fast.h>
Classes | |
class | ConflictClauseManager |
Public Member Functions | |
SearchEngineFast (TheoryCore *core) | |
The main Constructor. More... | |
virtual | ~SearchEngineFast () |
Destructor. More... | |
const std::string & | getName () |
Name of this search engine. More... | |
virtual QueryResult | checkValidInternal (const Expr &e) |
Implementation of the API call. More... | |
virtual QueryResult | restartInternal (const Expr &e) |
Reruns last check with e as an additional assumption. More... | |
virtual void | getCounterExample (std::vector< Expr > &assertions) |
Redefine the counterexample generation. More... | |
void | addLiteralFact (const Theorem &thm) |
Notify the search engine about a new literal fact. More... | |
void | addNonLiteralFact (const Theorem &thm) |
Notify the search engine about a new non-literal fact. More... | |
virtual Theorem | newIntAssumption (const Expr &e) |
Redefine newIntAssumption(): we need to add the new theorem to the appropriate Literal. More... | |
virtual bool | isAssumption (const Expr &e) |
Check if the formula has been assumed. More... | |
void | addSplitter (const Expr &e, int priority) |
Suggest a splitter to the SearchEngine. More... | |
![]() | |
int | getBottomScope () |
bool | isClause (const Expr &e) |
Check if e is a clause (a literal, or a disjunction of literals) More... | |
bool | isPropClause (const Expr &e) |
Check if e is a propositional clause. More... | |
bool | isCNFVar (const Expr &e) |
Check whether e is a fresh variable introduced by the CNF converter. More... | |
bool | isGoodSplitter (const Expr &e) |
Check if a splitter is required for completeness. More... | |
SearchImplBase (TheoryCore *core) | |
Constructor. More... | |
virtual | ~SearchImplBase () |
Destructor. More... | |
virtual void | registerAtom (const Expr &e) |
Register an atomic formula of interest. More... | |
virtual Theorem | getImpliedLiteral () |
Return next literal implied by last assertion. Null Expr if none. More... | |
virtual void | push () |
Push a checkpoint. More... | |
virtual void | pop () |
Restore last checkpoint. More... | |
virtual QueryResult | checkValid (const Expr &e, Theorem &result) |
Similar to checkValidInternal(), only returns Theorem(e) or Null. More... | |
virtual QueryResult | restart (const Expr &e, Theorem &result) |
Reruns last check with e as an additional assumption. More... | |
void | returnFromCheck () |
Returns to context immediately before last call to checkValid. More... | |
virtual Theorem | lastThm () |
Returns the result of the most recent valid theorem. More... | |
Theorem | newUserAssumption (const Expr &e) |
Generate and add a new assertion to the set of assertions in the current context. This should only be used by class VCL in assertFormula(). More... | |
void | newIntAssumption (const Theorem &thm) |
Helper for above function. More... | |
void | getUserAssumptions (std::vector< Expr > &assumptions) |
Get all assumptions made in this and all previous contexts. More... | |
void | getInternalAssumptions (std::vector< Expr > &assumptions) |
Get assumptions made internally in this and all previous contexts. More... | |
virtual void | getAssumptions (std::vector< Expr > &assumptions) |
Get all assumptions made in this and all previous contexts. More... | |
void | addFact (const Theorem &thm) |
Add a new fact to the search engine from the core. More... | |
virtual void | getCounterExample (std::vector< Expr > &assertions, bool inOrder=true) |
Will return the set of assertions which make the queried formula false. More... | |
virtual Proof | getProof () |
Returns the proof term for the last proven query. More... | |
virtual const Assumptions & | getAssumptionsUsed () |
Returns the set of assumptions used in the proof. It should be a subset of getAssumptions(). More... | |
void | processResult (const Theorem &res, const Expr &e) |
Process result of checkValid. More... | |
virtual FormulaValue | getValue (const CVC3::Expr &e) |
![]() | |
SearchEngine (TheoryCore *core) | |
Constructor. More... | |
virtual | ~SearchEngine () |
Destructor. More... | |
CommonProofRules * | getCommonRules () |
Accessor for common rules. More... | |
TheoryCore * | theoryCore () |
Accessor for TheoryCore. More... | |
void | getConcreteModel (ExprMap< Expr > &m) |
Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. More... | |
bool | tryModelGeneration (Theorem &thm) |
Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent. More... | |
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. More... | |
QueryResult | checkSAT () |
bool | split () |
Choose a splitter. More... | |
Expr | findSplitter () |
Returns a splitter. More... | |
void | clearLiterals () |
Clear the list of asserted literals (d_literals) More... | |
void | updateLitScores (bool firstTime) |
void | updateLitCounts (const Clause &c) |
Add the literals of a new clause to d_litsByScores. More... | |
bool | bcp () |
Boolean constraint propagation. More... | |
bool | fixConflict () |
Determines backtracking level and adds conflict clauses. More... | |
void | assertAssumptions () |
FIXME: document this. More... | |
void | enqueueFact (const Theorem &thm) |
Queue up a fact to assert to the DPs later. More... | |
void | setInconsistent (const Theorem &thm) |
Set the context inconsistent. Takes Theorem(FALSE). More... | |
void | commitFacts () |
Commit all the enqueued facts to the DPs. More... | |
void | clearFacts () |
Clear the local fact queue. More... | |
bool | propagate (const Clause &c, int idx, bool &wpUpdated) |
Auxiliary function for unit propagation. More... | |
void | unitPropagation (const Clause &c, unsigned idx) |
Do the unit propagation for the clause. More... | |
void | analyzeUIPs (const Theorem &falseThm, int conflictScope) |
Analyse the conflict, find the UIPs, etc. More... | |
void | addNewClause (Clause &c) |
Go through all the clauses and check the watch pointers (for debugging) More... | |
void | recordFact (const Theorem &thm) |
Process a new derived fact (auxiliary function) More... | |
void | traceConflict (const Theorem &conflictThm) |
First pass in conflict analysis; takes a theorem of FALSE. More... | |
QueryResult | checkValidMain (const Expr &e2) |
Private helper function for checkValid and restart. More... | |
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. More... | |
Theorem | processConflict (const Theorem &thm) |
Take a conflict in the form of Literal, or Theorem, and generate all the necessary conflict clauses. More... | |
Private Attributes | |
std::string | d_name |
Name. More... | |
DecisionEngine * | d_decisionEngine |
Decision Engine. More... | |
StatCounter | d_unitPropCount |
Total number of unit propagations. More... | |
StatCounter | d_circuitPropCount |
Total number of circuit propagations. More... | |
StatCounter | d_conflictCount |
Total number of conflicts. More... | |
StatCounter | d_conflictClauseCount |
Total number of conflict clauses generated (not all may be active) More... | |
CDList< ClauseOwner > | d_clauses |
Backtrackable list of clauses. More... | |
CDMap< Expr, Theorem > | d_unreportedLits |
Backtrackable set of pending unprocessed literals. More... | |
CDMap< Expr, bool > | d_unreportedLitsHandled |
CDList< SmartCDO< Theorem > > | d_nonLiterals |
Backtrackable list of non-literals (non-CNF formulas). More... | |
CDMap< Expr, Theorem > | d_nonLiteralsSaved |
prevent reprocessing More... | |
CDO< Theorem > | d_simplifiedThm |
Theorem which records simplification of the last query. More... | |
CDO< unsigned > | d_nonlitQueryStart |
Size of d_nonLiterals before most recent query. More... | |
CDO< unsigned > | d_nonlitQueryEnd |
Size of d_nonLiterals after query (not including DP-generated non-literals) More... | |
CDO< unsigned > | d_clausesQueryStart |
Size of d_clauses before most recent query. More... | |
CDO< unsigned > | d_clausesQueryEnd |
Size of d_clauses after query. More... | |
std::vector< std::deque < ClauseOwner > * > | d_conflictClauseStack |
Array of conflict clauses: one deque for each outstanding query. More... | |
std::deque< ClauseOwner > * | d_conflictClauses |
Reference to top deque of conflict clauses. More... | |
ConflictClauseManager | d_conflictClauseManager |
std::vector< Clause > | d_unitConflictClauses |
Unprocessed unit conflict clauses. More... | |
std::vector< Literal > | d_literals |
Set of literals to be processed by bcp. More... | |
CDMap< Expr, Literal > | d_literalSet |
Set of asserted literals which may survive accross checkValid() calls. More... | |
std::vector< Theorem > | d_factQueue |
Queue of derived facts to be sent to DPs. More... | |
bool | d_useEnqueueFact |
When true, use TheoryCore::enqueueFact() instead of addFact() in commitFacts() More... | |
bool | d_inCheckSAT |
True when checkSAT() is running. More... | |
CDList< Literal > | d_litsAlive |
Set of alive literals that shouldn't be garbage-collected. More... | |
std::vector< Circuit * > | d_circuits |
Mappings of literals to vectors of pointers to the corresponding watched literals. More... | |
ExprHashMap< std::vector < Circuit * > > | d_circuitsByExpr |
int | d_lastConflictScope |
The scope of the last conflict. More... | |
Clause | d_lastConflictClause |
The last conflict clause (for checkSAT()). May be Null. More... | |
Theorem | d_conflictTheorem |
Theorem(FALSE) which generated a conflict. More... | |
unsigned | d_litsMaxScorePos |
Position of a literal with max score in d_litsByScores. More... | |
std::vector< Literal > | d_litsByScores |
Vector of literals sorted by score. More... | |
int | d_splitterCount |
Internal splitter counter for delaying updateLitScores() More... | |
int | d_litSortCount |
Internal (decrementing) count of added splitters, to sort d_litByScores. More... | |
const bool | d_berkminFlag |
Flag to switch on/off the berkmin heuristic. More... | |
Friends | |
class | Circuit |
class | ConflictClauseManager |
Helper class for managing conflict clauses. More... | |
Additional Inherited Members | |
![]() | |
Literal | newLiteral (const Expr &e) |
Construct a Literal out of an Expr or return an existing one. More... | |
Theorem | simplify (const Theorem &e) |
Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e') More... | |
void | addCNFFact (const Theorem &thm, bool fromCore=false) |
Add a new fact to the search engine bypassing CNF converter. More... | |
int | scopeLevel () |
Return the current scope level (for convenience) More... | |
![]() | |
SearchEngineRules * | createRules () |
Create the trusted component. More... | |
SearchEngineRules * | createRules (SearchEngine *s_eng) |
![]() | |
VariableManager * | d_vm |
Variable manager for classes Variable and Literal. More... | |
CDO< int > | d_bottomScope |
The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid). More... | |
TheoryCore::CoreSatAPI * | d_coreSatAPI_implBase |
CDList< Splitter > | d_dpSplitters |
Backtracking ordered set of DP-suggested splitters. More... | |
Theorem | d_lastValid |
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions. More... | |
ExprHashMap< bool > | d_lastCounterExample |
Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample. More... | |
CDMap< Expr, Theorem > | d_assumptions |
Maintain the list of current assumptions (user asserts and splitters) for getAssumptions(). More... | |
CDMap< Expr, Theorem > | d_cnfCache |
Backtracking cache for the CNF generator. More... | |
CDMap< Expr, bool > | d_cnfVars |
Backtracking set of new variables generated by CNF translator. More... | |
const bool * | d_cnfOption |
Command line flag whether to convert to CNF. More... | |
const bool * | d_ifLiftOption |
Flag: whether to convert term ITEs into CNF. More... | |
const bool * | d_ignoreCnfVarsOption |
Flag: ignore auxiliary CNF variables when searching for a splitter. More... | |
const bool * | d_origFormulaOption |
Flag: Preserve the original formula with +cnf (for splitter heuristics) More... | |
CDMap< Expr, bool > | d_enqueueCNFCache |
Cache for enqueueCNF() More... | |
CDMap< Expr, bool > | d_applyCNFRulesCache |
Cache for applyCNFRules() More... | |
CDMap< Expr, Theorem > | d_replaceITECache |
Cache for replaceITE() More... | |
![]() | |
TheoryCore * | d_core |
Access to theory reasoning. More... | |
CommonProofRules * | d_commonRules |
Common proof rules. More... | |
SearchEngineRules * | d_rules |
Proof rules for the search engine. More... | |
Implementation of a faster search engine, using newer techniques.
This search engine is engineered for greater speed. It seeks to eliminate the use of recursion, and instead replace it with iterative procedures that have cleanly defined invariants. This will hopefully not only eliminate bugs or inefficiencies that have been difficult to track down in the default version, but it should also make it easier to trace, read, and understand. It strives to be in line with the most modern SAT techniques.
There are three other significant changes.
One, we want to improve the performance on heavily non-CNF problems. Unlike the older CVC, CVC3 does not expand problems into CNF and solve, but rather uses decision procedures to effect the same thing, but often much more slowly. This search engine will leverage off knowledge gained from the DPs in the form of conflict clauses as much as possible.
Two, the solver has traditionally had a difficult time getting started on non-CNF problems. Modern satsolvers also have this problem, and so they employ "restarts" to try solving the problem again after gaining more knowledge about the problem at hand. This allows a more accurate choice of splitters, and in the case of non-CNF problems, the solver can immediately leverage off CNF conflict clauses that were not initially available.
Third, this code is specifically designed to deal with the new dependency tracking. Lazy maps will be eliminated in favor implicit conflict graphs, reducing computation time in two different ways.
Definition at line 86 of file search_fast.h.
|
friend |
Definition at line 88 of file search_fast.h.
Referenced by addNonLiteralFact().