one bug fixed

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3f842bc738f7cdd69cf4e26f45f45eb2db8f5c46..bfff22863ac1bad10c7d19e1f6efbe16cb4466f2 100644 (file)
--- 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 31f54fdfc16219b875eb6bddb247077df1aff214..f40a65161f3acbb46d46b370872955e9c2acd7ee 100644 (file)
--- 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 59568bad6f8d5774b06e77ddfd3a25ee5a6918d7..de4bccd77860876219c3932dbed6b5730ee9e278 100644 (file)
--- 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 57a982d08ebe479646bc3d07a97e404a1cc6fa7d..36c409f3f29b5a0dc807643fc135f57a21f6d368 100644 (file)
--- 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]))