diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 40 | ||||
| -rw-r--r-- | test/regress/regress0/decision/Makefile.am | 7 | ||||
| -rw-r--r-- | test/regress/regress0/decision/error3.delta01.smt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/decision/error3.smt | 2 |
4 files changed, 33 insertions, 18 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3f842bc73..bfff22863 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -145,8 +145,10 @@ class SmtEnginePrivate { /** * Runs the nonclausal solver and tries to solve all the assigned * theory literals. + * + * Returns false if the formula simplifies to "false" */ - void nonClausalSimplify(); + bool nonClausalSimplify(); /** * Performs static learning on the assertions. @@ -176,8 +178,10 @@ class SmtEnginePrivate { * Perform non-clausal simplification of a Node. This involves * Theory implementations, but does NOT involve the SAT solver in * any way. + * + * Returns false if the formula simplifies to "false" */ - void simplifyAssertions() throw(NoSuchFunctionException, AssertionException); + bool simplifyAssertions() throw(NoSuchFunctionException, AssertionException); public: @@ -890,7 +894,9 @@ void SmtEnginePrivate::staticLearning() { } } -void SmtEnginePrivate::nonClausalSimplify() { + +// returns false if it learns a conflict +bool SmtEnginePrivate::nonClausalSimplify() { d_smt.finalOptionsAreSet(); TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime); @@ -923,7 +929,7 @@ void SmtEnginePrivate::nonClausalSimplify() { << "conflict in non-clausal propagation" << endl; d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); - return; + return false; } // No, conflict, go through the literals and solve them @@ -956,7 +962,7 @@ void SmtEnginePrivate::nonClausalSimplify() { << d_nonClausalLearnedLiterals[i] << endl; d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); - return; + return false; } } // Solve it with the corresponding theory @@ -987,7 +993,7 @@ void SmtEnginePrivate::nonClausalSimplify() { << learnedLiteral << endl; d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); - return; + return false; default: if (d_doConstantProp && learnedLiteral.getKind() == kind::EQUAL && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) { // constant propagation @@ -1136,6 +1142,8 @@ void SmtEnginePrivate::nonClausalSimplify() { << "non-clausal constant propagation : " << d_assertionsToCheck.back() << endl; } + + return true; } @@ -1218,7 +1226,8 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion } while(! worklist.empty()); } -void SmtEnginePrivate::simplifyAssertions() +// returns false if simpflication led to "false" +bool SmtEnginePrivate::simplifyAssertions() throw(NoSuchFunctionException, AssertionException) { try { @@ -1230,8 +1239,9 @@ void SmtEnginePrivate::simplifyAssertions() << "performing non-clausal simplification" << endl; // Abuse the user context to make sure circuit propagator gets backtracked d_smt.d_userContext->push(); - nonClausalSimplify(); + bool noConflict = nonClausalSimplify(); d_smt.d_userContext->pop(); + if(!noConflict) return false; } else { Assert(d_assertionsToCheck.empty()); d_assertionsToCheck.swap(d_assertionsToPreprocess); @@ -1279,8 +1289,9 @@ void SmtEnginePrivate::simplifyAssertions() d_assertionsToCheck.swap(d_assertionsToPreprocess); // Abuse the user context to make sure circuit propagator gets backtracked d_smt.d_userContext->push(); - nonClausalSimplify(); + bool noConflict = nonClausalSimplify(); d_smt.d_userContext->pop(); + if(!noConflict) return false; } Debug("smt") << "POST repeatSimp" << std::endl; @@ -1299,6 +1310,7 @@ void SmtEnginePrivate::simplifyAssertions() << tcep; InternalError(ss.str().c_str()); } + return true; } Result SmtEngine::check() { @@ -1385,7 +1397,7 @@ void SmtEnginePrivate::processAssertions() { } } - simplifyAssertions(); + bool noConflict = simplifyAssertions(); if(Options::current()->doStaticLearning) { // Perform static learning @@ -1404,7 +1416,7 @@ void SmtEnginePrivate::processAssertions() { if(Options::current()->repeatSimp) { d_assertionsToCheck.swap(d_assertionsToPreprocess); - simplifyAssertions(); + noConflict &= simplifyAssertions(); removeITEs(); } @@ -1440,8 +1452,10 @@ void SmtEnginePrivate::processAssertions() { // Push the formula to decision engine Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); - d_smt.d_decisionEngine->addAssertions - (d_assertionsToCheck, realAssertionsEnd, d_iteSkolemMap); + if(noConflict) { + d_smt.d_decisionEngine->addAssertions + (d_assertionsToCheck, realAssertionsEnd, d_iteSkolemMap); + } // end: INVARIANT to maintain: no reordering of assertions or // introducing new ones diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 31f54fdfc..f40a65161 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -27,10 +27,11 @@ TESTS = \ error20.smt \ error20.delta01.smt \ error122.smt \ - error122.delta01.smt + error122.delta01.smt \ + error3.smt \ + error3.delta01.smt + # Incorrect answers: -# error3.smt \ -# error3.delta01.smt # EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/decision/error3.delta01.smt b/test/regress/regress0/decision/error3.delta01.smt index 59568bad6..de4bccd77 100644 --- a/test/regress/regress0/decision/error3.delta01.smt +++ b/test/regress/regress0/decision/error3.delta01.smt @@ -2,7 +2,7 @@ :logic QF_AUFBV :extrafuns ((v1 BitVec[3])) :extrafuns ((a2 Array[13:3])) -:status unknown +:status unsat :formula (let (?n1 bv0[3]) (flet ($n2 (bvsgt v1 v1)) diff --git a/test/regress/regress0/decision/error3.smt b/test/regress/regress0/decision/error3.smt index 57a982d08..36c409f3f 100644 --- a/test/regress/regress0/decision/error3.smt +++ b/test/regress/regress0/decision/error3.smt @@ -1,6 +1,6 @@ (benchmark fuzzsmt :logic QF_AUFBV -:status unknown +:status unsat :extrafuns ((v0 BitVec[15])) :extrafuns ((v1 BitVec[3])) :extrafuns ((a2 Array[13:3])) |