51 void addLemma(
const Theorem& thm,
int priority,
bool atBottomScope)
52 { d_ss->addLemma(thm, priority, atBottomScope); }
54 {
return d_ss->newUserAssumption(assump); }
55 void addSplitter(
const Expr& e,
int priority)
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");