52 { d_ss->addLemma(thm, priority, atBottomScope); }
54 {
return d_ss->newUserAssumption(assump); }
56 { d_ss->addSplitter(e, priority); }
57 bool check(
const Expr& e);
62 bool SearchSatCoreSatAPI::check(
const Expr& e)
77 : d_cm(ss->theoryCore()->getCM()), d_ss(ss) {}
79 void push() {
return d_cm->push(); }
80 void pop() {
return d_cm->pop(); }
83 {
return d_ss->checkConsistent(cnf, fullEffort); }
108 { d_ss->theoryCore()->theoryOf(e)->registerAtom(e, thm); }
115 void SearchSat::restorePre()
117 if (d_core->getCM()->scopeLevel() == d_bottomScope) {
118 DebugAssert(d_prioritySetBottomEntriesSizeStack.size() > 0,
"Expected non-empty stack");
119 d_prioritySetBottomEntriesSize = d_prioritySetBottomEntriesSizeStack.back();
120 d_prioritySetBottomEntriesSizeStack.pop_back();
121 while (d_prioritySetBottomEntriesSize < d_prioritySetBottomEntries.size()) {
122 d_prioritySet.erase(d_prioritySetBottomEntries.back());
123 d_prioritySetBottomEntries.pop_back();
129 void SearchSat::restore()
131 while (d_prioritySetEntriesSize < d_prioritySetEntries.size()) {
132 d_prioritySet.erase(d_prioritySetEntries.back());
133 d_prioritySetEntries.pop_back();
135 while (d_pendingLemmasSize < d_pendingLemmas.size()) {
136 d_pendingLemmas.pop_back();
137 d_pendingScopes.pop_back();
139 while (d_varsUndoListSize < d_varsUndoList.size()) {
141 d_varsUndoList.pop_back();
146 bool SearchSat::recordNewRootLit(
Lit lit,
int priority,
bool atBottomScope)
148 DebugAssert(d_prioritySetEntriesSize == d_prioritySetEntries.size() &&
149 d_prioritySetBottomEntriesSize == d_prioritySetBottomEntries.size(),
151 pair<set<LitPriorityPair>::iterator,
bool> status =
153 if (!status.second)
return false;
154 if (!atBottomScope || d_bottomScope == d_core->getCM()->scopeLevel()) {
155 d_prioritySetEntries.push_back(status.first);
156 d_prioritySetEntriesSize = d_prioritySetEntriesSize + 1;
159 d_prioritySetBottomEntries.push_back(status.first);
160 ++d_prioritySetBottomEntriesSize;
163 if (d_prioritySetStart.get() == d_prioritySet.end() ||
164 ((*status.first) < (*(d_prioritySetStart.get()))))
165 d_prioritySetStart = status.first;
170 void SearchSat::addLemma(
const Theorem& thm,
int priority,
bool atBottomScope)
173 string indentStr(theoryCore()->getCM()->scopeLevel(),
' ');
177 DebugAssert(d_pendingLemmasSize == d_pendingLemmas.size(),
"Size mismatch");
178 DebugAssert(d_pendingLemmasSize == d_pendingScopes.size(),
"Size mismatch");
179 DebugAssert(d_pendingLemmasNext <= d_pendingLemmas.size(),
"Size mismatch");
180 d_pendingLemmas.push_back(pair<Theorem,int>(thm, priority));
181 d_pendingScopes.push_back(atBottomScope);
182 d_pendingLemmasSize = d_pendingLemmasSize + 1;
186 void SearchSat::addSplitter(
const Expr& e,
int priority)
188 DebugAssert(!e.
isEq() || e[0] != e[1],
"Expected non-trivial splitter");
189 addLemma(d_commonRules->excludedMiddle(e), priority);
193 void SearchSat::assertLit(
Lit l)
196 Expr e = d_cnfManager->concreteLit(l);
199 string indentStr(theoryCore()->getCM()->scopeLevel(),
' ');
202 std::stringstream ss;
203 ss<<theoryCore()->getCM()->scopeLevel();
207 if (l.
isPositive()) val +=
"1";
else val +=
"0";
208 TRACE(
"assertLit",
"",
"",
"");
209 TRACE(
"assertLitScope", indentStr,
"Scope level = ", temp);
222 bool isSATLemma =
false;
224 e = d_cnfManager->concreteLit(l,
false);
227 TRACE(
"quant-level",
"found null expr ",e,
"");
232 "internal assumptions should be true");
246 Theorem thm = d_commonRules->assumpRule(e);
249 d_cnfManager->addAssumption(thm, cnf);
253 d_intAssumptions.push_back(thm);
254 d_core->addFact(thm);
260 DebugAssert(d_inCheckSat,
"Should only be used as a call-back");
261 if (d_core->inconsistent()) {
262 d_cnfManager->convertLemma(d_core->inconsistentThm(), cnf);
263 if (d_cnfManager->numVars() > d_vars.size()) {
266 return DPLLT::INCONSISTENT;
269 if (d_core->checkSATCore() && d_pendingLemmasNext == d_pendingLemmas.size() && d_lemmasNext == d_lemmas.numClauses()) {
270 if (d_core->inconsistent()) {
271 d_cnfManager->convertLemma(d_core->inconsistentThm(), cnf);
272 if (d_cnfManager->numVars() > d_vars.size()) {
275 return DPLLT::INCONSISTENT;
277 else return DPLLT::CONSISTENT;
280 return DPLLT::MAYBE_CONSISTENT;
284 Lit SearchSat::getImplication()
288 Theorem imp = d_core->getImpliedLiteral();
290 l = d_cnfManager->getCNFLit(imp.
getExpr());
292 "implied literals should be registered by cnf or by user");
294 d_theorems.insert(imp.
getExpr(), imp);
298 imp = d_core->getImpliedLiteral();
308 Expr e = d_cnfManager->concreteLit(l);
310 DebugAssert(i != d_theorems.end(),
"getExplanation: no explanation found");
311 d_cnfManager->convertLemma((*i).second, cnf);
312 if (d_cnfManager->numVars() > d_vars.size()) {
323 for (i = d_pendingLemmasNext; i < d_pendingLemmas.size(); ++i) {
324 l = d_cnfManager->addLemma(d_pendingLemmas[i].first, d_lemmas);
325 if (!recordNewRootLit(l, d_pendingLemmas[i].second, d_pendingScopes[i])) {
327 d_lemmas.deleteLast();
330 d_pendingLemmasNext = d_pendingLemmas.size();
332 if (d_cnfManager->numVars() > d_vars.size()) {
336 DebugAssert(d_lemmasNext <= d_lemmas.numClauses(),
"");
337 if (d_lemmasNext == d_lemmas.numClauses())
return false;
339 cnf += d_lemmas[d_lemmasNext];
340 d_lemmasNext = d_lemmasNext + 1;
341 }
while (d_lemmasNext < d_lemmas.numClauses());
346 Lit SearchSat::makeDecision()
348 DebugAssert(d_inCheckSat,
"Should only be used as a call-back");
351 set<LitPriorityPair>::const_iterator i, iend;
353 for (i = d_prioritySetStart, iend = d_prioritySet.end(); i != iend; ++i) {
355 if (findSplitterRec(lit, getValue(lit), &litDecision)) {
359 d_prioritySetStart = i;
376 "invariant violated");
378 if (checkJustified(v))
return false;
381 value = Var::invertValue(value);
384 if (d_cnfManager->numFanins(v) == 0) {
394 else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) {
398 n = d_cnfManager->numFanins(v);
399 for (i=0; i < n; ++i) {
400 litTmp = d_cnfManager->getFanin(v, i);
403 if (checkJustified(varTmp))
continue;
407 Lit cIf = d_cnfManager->getFanin(varTmp,0);
408 Lit cThen = d_cnfManager->getFanin(varTmp,1);
409 Lit cElse = d_cnfManager->getFanin(varTmp,2);
419 cout << d_cnfManager->concreteVar(cIf.
getVar()) <<
endl;
420 DebugAssert(
false,
"No controlling input found (1)");
428 if (cThen.
getVar() != v &&
439 if (cElse.
getVar() != v &&
446 setJustified(varTmp);
458 int kind = d_cnfManager->concreteVar(v).getKind();
464 if (value == valHard) {
465 n = d_cnfManager->numFanins(v);
466 for (i=0; i < n; ++i) {
467 litTmp = d_cnfManager->getFanin(v, i);
468 if (findSplitterRec(litTmp, valHard, litDecision)) {
472 DebugAssert(getValue(v) == valHard,
"Output should be justified");
477 Var::Val valEasy = Var::invertValue(valHard);
478 n = d_cnfManager->numFanins(v);
479 for (i=0; i < n; ++i) {
480 litTmp = d_cnfManager->getFanin(v, i);
481 if (getValue(litTmp) != valHard) {
482 if (findSplitterRec(litTmp, valEasy, litDecision)) {
485 DebugAssert(getValue(v) == valEasy,
"Output should be justified");
490 DebugAssert(
false,
"No controlling input found (2)");
494 DebugAssert(d_cnfManager->numFanins(v) == 2,
"Expected 2 fanins");
496 litTmp = d_cnfManager->getFanin(v, 0);
500 litTmp = d_cnfManager->getFanin(v, 1);
509 litTmp = d_cnfManager->getFanin(v, 0);
518 litTmp = d_cnfManager->getFanin(v, 1);
527 DebugAssert(
false,
"No controlling input found (3)");
531 litTmp = d_cnfManager->getFanin(v, 0);
534 if (findSplitterRec(litTmp, val, litDecision)) {
538 litTmp = d_cnfManager->getFanin(v, 1);
540 if (findSplitterRec(litTmp, val, litDecision)) {
543 DebugAssert(getValue(v) == value,
"Output should be justified");
548 val = getValue(d_cnfManager->getFanin(v, 1));
551 if (findSplitterRec(litTmp, val, litDecision)) {
554 DebugAssert(
false,
"Unable to find controlling input (4)");
559 litTmp = d_cnfManager->getFanin(v, 0);
562 if (findSplitterRec(litTmp, val, litDecision)) {
566 litTmp = d_cnfManager->getFanin(v, 1);
567 if (findSplitterRec(litTmp, val, litDecision)) {
570 DebugAssert(getValue(v) == value,
"Output should be justified");
575 val = getValue(d_cnfManager->getFanin(v, 1));
578 if (findSplitterRec(litTmp, val, litDecision)) {
581 DebugAssert(
false,
"Unable to find controlling input (5)");
586 Lit cIf = d_cnfManager->getFanin(v, 0);
587 Lit cThen = d_cnfManager->getFanin(v, 1);
588 Lit cElse = d_cnfManager->getFanin(v, 2);
590 if (getValue(cElse) == value ||
591 getValue(cThen) == Var::invertValue(value)) {
598 cout << d_cnfManager->concreteVar(cIf.
getVar()) <<
endl;
599 DebugAssert(
false,
"No controlling input found (6)");
609 getValue(cThen) == value) &&
610 findSplitterRec(cThen, value, litDecision)) {
620 getValue(cElse) == value) &&
621 findSplitterRec(cElse, value, litDecision)) {
625 DebugAssert(getValue(v) == value,
"Output should be justified");
640 DebugAssert(d_dplltReady,
"SAT solver is not ready");
641 if (isRestart && d_lastCheck.get().isNull()) {
643 (
"restart called without former call to checkValid");
646 DebugAssert(!d_inCheckSat,
"checkValid should not be called recursively");
647 TRACE(
"searchsat",
"checkValid: ", e,
"");
651 (
"checking validity of a non-Boolean expression:\n\n "
653 +
"\n\nwhich has the following type:\n\n "
660 while (e2.
isNot() && e2[0].
isNot()) e2 = e2[0][0];
662 result = d_lastValid;
668 d_lastValid = d_commonRules->assumpRule(d_lastCheck);
669 result = d_lastValid;
675 d_lastValid = d_commonRules->trueTheorem();
676 result = d_lastValid;
680 d_bottomScope = d_core->getCM()->scopeLevel();
681 d_prioritySetBottomEntriesSizeStack.push_back(d_prioritySetBottomEntriesSize);
689 d_cnfManager->setBottomScope(d_bottomScope);
690 d_dplltReady =
false;
692 newUserAssumptionInt(e2, cnf,
true);
698 if (!isRestart && d_core->inconsistent()) {
700 thm = d_rules->proofByContradiction(e, d_core->inconsistentThm());
703 d_cnfManager->setBottomScope(-1);
704 d_inCheckSat =
false;
705 result = d_lastValid;
710 qres = isRestart ? d_dpllt->continueCheck(cnf) : d_dpllt->checkSat(cnf);
714 DebugAssert(d_core->getCM()->scopeLevel() == d_bottomScope,
715 "Expected unchanged context after unsat");
718 if (d_core->getTM()->withProof()) {
719 Proof pf = d_dpllt->getSatProof(d_cnfManager, d_core);
721 d_lastValid = d_rules->satProof(e2, pf);
724 d_lastValid = d_commonRules->assumpRule(d_lastCheck);
729 "Expected no lemmas after satisfiable check");
734 #ifdef _CVC3_DEBUG_MODE
736 if( CVC3::debugger.trace(
"quant debug") ){
737 d_core->theoryOf(
FORALL)->debug(1);
741 if( CVC3::debugger.trace(
"sat model unknown") ){
742 std::vector<SAT::Lit> cur_assigns = d_dpllt->getCurAssignments();
743 cout<<
"Current assignments"<<
endl;
745 for(
size_t i = 0 ; i < cur_assigns.size(); i++){
746 Lit l = cur_assigns[i];
747 Expr e = d_cnfManager->concreteLit(l);
751 if (l.
isPositive()) val +=
"1";
else val +=
"0";
759 std::vector< std::vector<SAT::Lit> > cur_clauses = d_dpllt->getCurClauses();
760 cout<<
"Current Clauses"<<
endl;
762 for(
size_t i = 0 ; i < cur_clauses.size(); i++){
764 for(
size_t j = 0; j < cur_clauses[i].size(); j++){
766 Lit l = cur_clauses[i][j];
768 if (l.
isPositive()) val +=
"+";
else val +=
"-";
769 cout<<val<<l.
getVar()<<
" ";
776 if( CVC3::debugger.trace(
"model unknown") ){
778 cout<<
"===========terms begin=========="<<
endl;
780 for (
size_t i=0; i<allterms.
size(); i++){
782 cout<<
"i="<<i<<
" :"<<allterms[i].getFindLevel()<<
":"<<d_core->simplifyExpr(allterms[i])<<
"|"<<allterms[i]<<
endl;
787 cout<<
"-----------term end ---------"<<
endl;
789 cout<<
"===========pred begin=========="<<
endl;
791 for (
size_t i=0; i<allpreds.
size(); i++){
792 if(allpreds[i].hasFind()){
793 if( (d_core->findExpr(allpreds[i])).isTrue()){
794 cout<<
"ASSERT "<< allpreds[i] <<
";" <<
endl;
797 cout<<
"ASSERT NOT("<< allpreds[i] <<
");" <<
endl;
809 cout<<
"-----------end----------pred"<<
endl;
812 if( CVC3::debugger.trace(
"model unknown quant") ){
813 cout<<
"=========== quant pred begin=========="<<
endl;
815 for (
size_t i=0; i<allpreds.
size(); i++){
817 Expr cur = allpreds[i];
819 if(allpreds[i].hasFind()) {
821 cout<<allpreds[i].getFindLevel();
822 cout<<
":"<<d_core->findExpr(allpreds[i])<<
"|"<<allpreds[i]<<
endl;
826 cout<<
"-----------end----------pred"<<
endl;
829 if( CVC3::debugger.trace(
"model unknown nonquant") ){
830 cout<<
"=========== quant pred begin=========="<<
endl;
832 for (
size_t i=0; i<allpreds.
size(); i++){
834 Expr cur = allpreds[i];
841 if(allpreds[i].hasFind()) {
843 cout<<allpreds[i].getFindLevel();
844 cout<<
":"<<d_core->findExpr(allpreds[i])<<
"|"<<allpreds[i]<<
endl;
848 cout<<
"-----------end----------pred"<<
endl;
851 if( CVC3::debugger.trace(
"unknown state") ){
853 cout<<
"===========pred begin=========="<<
endl;
855 for (
size_t i=0; i<allpreds.
size(); i++){
856 if(allpreds[i].hasFind()){
864 if( (d_core->findExpr(allpreds[i])).isTrue()){
865 cout<<
":assumption "<< allpreds[i] <<
"" <<
endl;
868 cout<<
":assumption(not "<< allpreds[i] <<
")" <<
endl;
880 cout<<
"-----------end----------pred"<<
endl;
883 if( CVC3::debugger.trace(
"unknown state noforall") ){
885 cout<<
"===========pred begin=========="<<
endl;
887 for (
size_t i=0; i<allpreds.
size(); i++){
888 if(allpreds[i].hasFind()){
889 Expr cur(allpreds[i]);
896 if( (d_core->findExpr(allpreds[i])).isTrue()){
900 cout<<
"ASSERT "<< allpreds[i] <<
";" <<
endl;
903 else if ( (d_core->findExpr(allpreds[i])).isFalse()){
907 cout<<
"ASSERT (NOT "<< allpreds[i] <<
");" <<
endl;
911 cout<<
"--ERROR"<<
endl;
923 cout<<
"-----------end----------pred"<<
endl;
929 d_cnfManager->setBottomScope(-1);
930 d_inCheckSat =
false;
931 result = d_lastValid;
939 d_bottomScope(core->getCM()->getCurrentContext(), -1),
940 d_lastCheck(core->getCM()->getCurrentContext()),
941 d_lastValid(core->getCM()->getCurrentContext(),
942 d_commonRules->trueTheorem()),
943 d_userAssumptions(core->getCM()->getCurrentContext()),
944 d_intAssumptions(core->getCM()->getCurrentContext()),
945 d_idxUserAssump(core->getCM()->getCurrentContext(), 0),
947 d_theorems(core->getCM()->getCurrentContext()),
949 d_lemmas(core->getCM()->getCurrentContext()),
950 d_pendingLemmasSize(core->getCM()->getCurrentContext(), 0),
951 d_pendingLemmasNext(core->getCM()->getCurrentContext(), 0),
952 d_lemmasNext(core->getCM()->getCurrentContext(), 0),
953 d_varsUndoListSize(core->getCM()->getCurrentContext(), 0),
954 d_prioritySetStart(core->getCM()->getCurrentContext()),
955 d_prioritySetEntriesSize(core->getCM()->getCurrentContext(), 0),
956 d_prioritySetBottomEntriesSize(0),
957 d_lastRegisteredVar(core->getCM()->getCurrentContext(), 0),
958 d_dplltReady(core->getCM()->getCurrentContext(), true),
959 d_nextImpliedLiteral(core->getCM()->getCurrentContext(), 0),
960 d_restorer(core->getCM()->getCurrentContext(), this)
972 if (core->
getFlags()[
"sat"].getString() ==
"sat") {
975 core->
getFlags()[
"stats"].getBool());
977 throw CLException(
"SAT solver 'sat' not supported in this build");
979 }
else if (core->
getFlags()[
"sat"].getString() ==
"minisat") {
981 core->
getFlags()[
"stats"].getBool(),
984 throw CLException(
"Unrecognized SAT solver name: " + (core->
getFlags()[
"sat"].getString()));
1013 while (d_nextImpliedLiteral < d_core->numImpliedLiterals()) {
1026 (
"returnFromCheck called with no previous invalid call to checkValid");
1035 for (
int i = 0; i < e.
arity(); ++i) {
1046 for (
int i = 0; i < e.
arity(); ++i) {
1067 "User assumptions should be added before calling checkSat");
1115 assumptions.push_back((*i).getExpr());
1123 assumptions.push_back((*i).getExpr());
1135 if (iU == iUend)
break;
1136 assumptions.push_back((*iU).getExpr());
1139 else if (iU == iUend) {
1140 Expr intAssump = (*iI).getExpr();
1142 assumptions.push_back(intAssump);
1147 if ((*iI).getScope() <= (*iU).getScope()) {
1148 Expr intAssump = (*iI).getExpr();
1150 assumptions.push_back(intAssump);
1155 assumptions.push_back((*iU).getExpr());
1172 throw Exception(
"Expected last query to be invalid");
1182 (
"getProof cannot be called without proofs activated");
1185 (
"getProof must be called only after a successful check");
void addLemma(const Theorem &thm, int priority, bool atBottomScope)
Add a new lemma derived by theory core.
ExprStream & pop(ExprStream &os)
Restore the indentation.
friend class SearchSatCoreSatAPI
void registerCNFCallback(CNFCallback *cnfCallback)
Register CNF callback.
CDO< int > d_bottomScope
Bottom scope for current query.
API to to a generic proof search engine.
virtual void addAssertion(const CNF_Formula &cnf)=0
Add new clauses to the SAT solver.
Data structure of expressions in CVC3.
TheoremManager * getTM() const
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
const CLFlags & getFlags() const
Description: Collection of debugging macros and functions.
unsigned numVars()
Return the number of variables being managed.
void push()
Set a checkpoint for backtracking.
void getExplanation(Lit l, CNF_Formula &cnf)
Get an explanation for a literal that was implied.
SAT::DPLLT * d_dpllt
Pointer to DPLLT implementation.
CDList< Theorem > d_intAssumptions
List of all internal assumptions.
An exception to be thrown at typecheck error.
SearchSatTheoryAPI(SearchSat *ss)
void registerCoreSatAPI(CoreSatAPI *coreSatAPI)
Register a SatAPI for TheoryCore.
virtual void pop()
Restore last checkpoint.
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.
virtual Theorem assumpRule(const Expr &a, int scope=-1)=0
SAT::DPLLT::ConsistentResult checkConsistent(CNF_Formula &cnf, bool fullEffort)
Check consistency of the current assignment.
Implementation of dpllt module based on minisat.
Lit getImplication()
Get a literal that is implied by the current assignment.
static void setRecursiveInUserAssumption(const Expr &e, int scope)
void setUserAssumption(int scope=-1) const
SAT::CNF_Manager::CNFCallback * d_cnfCallback
Callback for CNF_Manager.
#define DebugAssert(cond, str)
bool inUserAssumption() const
Search engine that connects to a generic SAT reasoning module.
Theorem addAssumption(const Expr &assump)
Add an assumption to the set of assumptions in the current context.
CommonProofRules * d_commonRules
Common proof rules.
Pair of Lit and priority of this Lit.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool getNewClauses(CNF_Formula &cnf)
Get new clauses from the theory.
Abstract proof rules interface to the simple search engine.
void registerAtom(const Expr &e, const Theorem &thm)
Register an atom.
void pop()
Restore most recent checkpoint.
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.
Theorem getImpliedLiteralByIndex(unsigned index)
Return an implied literal by index.
friend class SearchSatCNFCallback
Search engine that uses an external SAT engine.
virtual void getAssumptions(std::vector< Expr > &assumptions)
Get all assumptions made in this and all previous contexts.
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).
ExprTransform * getExprTrans() const
void setQuantLevel(unsigned level)
Set the quantification level for this theorem.
bool outOfResources()
Check if the work budget has been exceeded.
std::string toString() const
Print the expression to a string.
SearchSatDecider(SearchSat *ss)
void newUserAssumptionIntHelper(const Theorem &thm, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)
Helper for newUserAssumptionInt.
std::vector< SAT::Var::Val > d_vars
Cached values of variables.
const Expr & unnegate() const
Remove leading NOT if any.
Basic implementation of dpllt module.
virtual bool isAssumption(const Expr &e)
Check if the formula has already been assumed previously.
std::string toString() const
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.
friend class SearchSatTheoryAPI
Abstract class for callbacks.
virtual void returnFromCheck()
Returns to context immediately before last call to checkValid.
void setInUserAssumption(int scope=-1) const
void setUserRegisteredAtom() const
Set the UserRegisteredAtom flag for this Expr.
bool isUserRegisteredAtom() const
void registerAtom(const Expr &e, const Theorem &thm)
Register an atomic formula of interest.
TheoryCore::CoreSatAPI * d_coreSatAPI
ContextManager * getCM() const
SearchSatCoreSatAPI(SearchSat *ss)
friend class SearchSatDecider
bool isRegisteredAtom() const
Generic API for Theories plus methods commonly used by theories.
bool isUserAssumption() const
void addSplitter(const Expr &e, int priority)
Suggest a splitter to the Sat engine.
bool isAbsLiteral() const
Test if e is an abstract literal.
CDList< Theorem > d_userAssumptions
List of all user assumptions.
bool isIntAssumption() const
SearchSatCNFCallback(SearchSat *ss)
bool recordNewRootLit(SAT::Lit lit, int priority=0, bool atBottomScope=false)
Helper for addLemma and check.
void setIntAssumption() const
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.
Lit makeDecision()
Make a decision.
Manager for multiple contexts. Also holds current context.
Type getType() const
Get the type. Recursively compute if necessary.
std::deque< T >::const_iterator const_iterator
SAT::CNF_Manager * d_cnfManager
Manages CNF formula and its relationship to original Exprs and Theorems.
void addFact(const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure;...
virtual Theorem andElim(const Theorem &e, int i)=0
TheoryCore * d_core
Access to theory reasoning.
Lit addAssumption(const CVC3::Theorem &thm, CNF_Formula &cnf)
Given thm of form A |- B, convert B to CNF and add it to cnf.
void assertLit(Lit l)
Notify theory when a literal is set to true.
Statistics & getStatistics() const
SAT::DPLLT::TheoryAPI * d_theoryAPI
Implementation of TheoryAPI for DPLLT.
Nice SAL-like language for manually written specs.
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
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.
SAT::DPLLT::Decider * d_decider
Implementation of Decider for DPLLT.