22 #ifndef _cvc3__include__search_sat_h_
23 #define _cvc3__include__search_sat_h_
182 void addLemma(
const Theorem& thm,
int priority = 0,
bool atBotomScope =
false);
217 "Lit out of bounds in getValue");
274 {
return check(e, result); }
276 {
return check(e, result,
true); }
285 bool inOrder =
true);
CDO< bool > d_dplltReady
Whether it's OK to call DPLLT solver from the current scope.
void setJustified(SAT::Var v)
Mark this variable as justified.
void addSplitter(const Expr &e, int priority)
Core theory callback which suggests a splitter.
CDO< int > d_bottomScope
Bottom scope for current query.
API to to a generic proof search engine.
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
std::vector< unsigned > d_prioritySetBottomEntriesSizeStack
Backtracking size of priority set entries at bottom scope.
virtual QueryResult checkValid(const Expr &e, Theorem &result)
Checks the validity of a formula in the current context.
CDO< unsigned > d_idxUserAssump
Index to where unprocessed assumptions start.
CDMap< Expr, Theorem > d_theorems
Store of theorems for expressions sent to DPLLT.
std::vector< bool > d_pendingScopes
Scope parameter for lemmas waiting to be translated since last call to getNewClauses() ...
Abstract API to the proof search engine.
CDO< unsigned > d_prioritySetEntriesSize
Backtracking size of priority set entries.
std::string d_name
Name of search engine.
SAT::DPLLT * d_dpllt
Pointer to DPLLT implementation.
CDList< Theorem > d_intAssumptions
List of all internal assumptions.
virtual void pop()
Restore last checkpoint.
SAT::Var::Val getValue(SAT::Lit c)
Get the value of a CNF Literal.
bool d_inCheckSat
Whether we are currently in a call to dpllt->checkSat.
CDO< unsigned > d_nextImpliedLiteral
std::set< LitPriorityPair > d_prioritySet
Used to determine order to find splitters.
SAT::Var::Val getValue(SAT::Var v)
virtual QueryResult restart(const Expr &e, Theorem &result)
Reruns last check with e as an additional assumption.
void assertLit(SAT::Lit l)
DPLLT callback to inform theory that a literal has been assigned.
SAT::CNF_Manager::CNFCallback * d_cnfCallback
Callback for CNF_Manager.
#define DebugAssert(cond, str)
CDO< unsigned > d_lastRegisteredVar
Last Var registered with core theory.
Lit getCNFLit(const CVC3::Expr &e)
Look up the CNF literal for an Expr.
Search engine that connects to a generic SAT reasoning module.
virtual Theorem lastThm()
Returns the result of the most recent valid theorem.
SAT::Lit getImplication()
DPLLT callback to get theory propagations.
std::vector< std::pair< Theorem, int > > d_pendingLemmas
Lemmas waiting to be translated since last call to getNewClauses()
Pair of Lit and priority of this Lit.
void restore()
Get rid of entries in prioritySet and pendingLemmas added since last push.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void restorePre()
Get rid of bottom scope entries in prioritySet.
LitPriorityPair(SAT::Lit lit, int priority)
CDO< unsigned > d_pendingLemmasNext
Backtracking next item in d_pendingLemmas.
virtual void push()
Push a checkpoint.
virtual FormulaValue getValue(const CVC3::Expr &e)
virtual void getInternalAssumptions(std::vector< Expr > &assumptions)
Get assumptions made internally in this and all previous contexts.
virtual Theorem newUserAssumption(const Expr &e)
Generate and add an assumption to the set of assumptions in the current context.
virtual void getAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
SAT::Lit makeDecision()
DPLLT callback to decide which literal to split on next.
virtual Proof getProof()
Returns the proof term for the last proven query.
virtual void getCounterExample(std::vector< Expr > &assertions, bool inOrder=true)
Will return the set of assertions which make the queried formula false.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
friend bool operator<(const LitPriorityPair &p1, const LitPriorityPair &p2)
std::string toString() const
Print the expression to a string.
void newUserAssumptionIntHelper(const Theorem &thm, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)
Helper for newUserAssumptionInt.
bool checkJustified(SAT::Var v)
Check whether this variable's value is justified.
std::vector< SAT::Var::Val > d_vars
Cached values of variables.
virtual bool isAssumption(const Expr &e)
Check if the formula has already been assumed previously.
SAT::CD_CNF_Formula d_lemmas
CNF Formula used for theory lemmas.
Interface class for callbacks to SAT from Core.
virtual void getUserAssumptions(std::vector< Expr > &assumptions)
Get all user assumptions made in this and all previous contexts.
virtual Theorem getImpliedLiteral()
Return next literal implied by last assertion. Null Expr if none.
CDO< Expr > d_lastCheck
Last expr checked for validity.
virtual void push()=0
Set a checkpoint for backtracking.
bool operator<(const Expr &e1, const Expr &e2)
Manager for conversion to and traversal of CNF formulas.
Abstract class for callbacks.
virtual void returnFromCheck()
Returns to context immediately before last call to checkValid.
void addLemma(const Theorem &thm, int priority=0, bool atBotomScope=false)
Core theory callback which adds a new lemma from the core theory.
virtual const std::string & getName()
Name of this search engine.
TheoryCore::CoreSatAPI * d_coreSatAPI
std::vector< std::set< LitPriorityPair >::iterator > d_prioritySetEntries
Entries in priority set in insertion order (so set can be backtracked)
CVC3::Expr concreteLit(Lit l, bool checkTranslated=true)
Convert a CNF literal to an Expr literal.
CDO< unsigned > d_lemmasNext
Current position in d_lemmas.
SearchSat(TheoryCore *core, const std::string &name)
int getBottomScope()
Core theory callback which asks for the bottom scope for current query.
CDO< unsigned > d_pendingLemmasSize
Backtracking size of d_pendingLemmas.
CDList< Theorem > d_userAssumptions
List of all user assumptions.
QueryResult check(const Expr &e, Theorem &result, bool isRestart=false)
Main checking procedure shared by checkValid and restart.
virtual void pop()=0
Restore checkpoint.
std::vector< std::set< LitPriorityPair >::iterator > d_prioritySetBottomEntries
Entries in priority set in insertion order (so set can be backtracked)
bool recordNewRootLit(SAT::Lit lit, int priority=0, bool atBottomScope=false)
Helper for addLemma and check.
Definition of the API to expression package. See class Expr for details.
CDO< unsigned > d_varsUndoListSize
Backtracking size of d_varsUndoList.
std::vector< unsigned > d_varsUndoList
List for backtracking var values.
void getExplanation(SAT::Lit l, SAT::CNF_Formula &cnf)
DPLLT callback to explain a theory propagation.
bool findSplitterRec(SAT::Lit lit, SAT::Var::Val value, SAT::Lit *litDecision)
Recursively traverse DAG looking for a splitter.
Restorer d_restorer
Instance of Restorer class.
CDO< std::set< LitPriorityPair >::const_iterator > d_prioritySetStart
Current position in prioritySet.
Theorem newUserAssumptionInt(const Expr &e, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)
Helper for newUserAssumption.
virtual ~SearchSat()
Destructor.
SAT::DPLLT::ConsistentResult checkConsistent(SAT::CNF_Formula &cnf, bool fullEffort)
DPLLT callback to ask if theory has detected inconsistency.
Restorer(Context *context, SearchSat *ss)
static Val invertValue(Val)
void setJustified() const
SAT::CNF_Manager * d_cnfManager
Manages CNF formula and its relationship to original Exprs and Theorems.
bool getNewClauses(SAT::CNF_Formula &cnf)
DPLLT callback to get more general theory clauses.
unsigned d_prioritySetBottomEntriesSize
Current size of bottom entries.
SAT::DPLLT::TheoryAPI * d_theoryAPI
Implementation of TheoryAPI for DPLLT.
Smart context-dependent object wrapper.
CDO< Theorem > d_lastValid
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
virtual void registerAtom(const Expr &e)
Register an atomic formula of interest.
void setValue(SAT::Var v, SAT::Var::Val val)
Set the value of a variable.
SAT::DPLLT::Decider * d_decider
Implementation of Decider for DPLLT.