Fix handling of `LogicException` during solving (#8000)

Fixes #7974. This commit fixes our handling of LogicExceptions during solving. Instead of leaving MiniSat in a bad state, it catches the exception, resets the decision trail, prints the error message, and then returns unknown.

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 07d260c7ee34f2234a8e0ff830d66873e7ff8232..2151dc03e6d5c8dde162136ef6456e03afe3ea98 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -20,6 +20,7 @@
 #include "prop/prop_engine.h"
 #include "smt/assertions.h"
 #include "smt/env.h"
+#include "smt/logic_exception.h"
 #include "smt/preprocessor.h"
 #include "smt/solver_engine.h"
 #include "smt/solver_engine_state.h"
@@ -115,85 +116,103 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
                                       const std::vector<Node>& assumptions,
                                       bool isEntailmentCheck)
 {
-  // update the state to indicate we are about to run a check-sat
-  bool hasAssumptions = !assumptions.empty();
-  d_state.notifyCheckSat(hasAssumptions);
-
-  // then, initialize the assertions
-  as.initializeCheckSat(assumptions, isEntailmentCheck);
-
-  // make the check, where notice smt engine should be fully inited by now
+  Result result;
 
-  Trace("smt") << "SmtSolver::check()" << endl;
+  bool hasAssumptions = !assumptions.empty();
 
-  const std::string& filename = d_env.getOptions().driver.filename;
-  ResourceManager* rm = d_env.getResourceManager();
-  if (rm->out())
+  try
   {
-    Result::UnknownExplanation why =
-        rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
-    return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
-  }
-  rm->beginCall();
-
-  // Make sure the prop layer has all of the assertions
-  Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
-  processAssertions(as);
-  Trace("smt") << "SmtSolver::check(): done processing assertions" << endl;
+    // update the state to indicate we are about to run a check-sat
+    d_state.notifyCheckSat(hasAssumptions);
 
-  TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);
+    // then, initialize the assertions
+    as.initializeCheckSat(assumptions, isEntailmentCheck);
 
-  d_env.verbose(2) << "solving..." << std::endl;
-  Trace("smt") << "SmtSolver::check(): running check" << endl;
-  Result result = d_propEngine->checkSat();
-  Trace("smt") << "SmtSolver::check(): result " << result << std::endl;
+    // make the check, where notice smt engine should be fully inited by now
 
-  rm->endCall();
-  Trace("limit") << "SmtSolver::check(): cumulative millis "
-                 << rm->getTimeUsage() << ", resources "
-                 << rm->getResourceUsage() << endl;
+    Trace("smt") << "SmtSolver::check()" << endl;
 
-  if ((d_env.getOptions().smt.solveRealAsInt
-       || d_env.getOptions().smt.solveIntAsBV > 0)
-      && result.asSatisfiabilityResult().isSat() == Result::UNSAT)
-  {
-    result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-  }
-  // flipped if we did a global negation
-  if (as.isGlobalNegated())
-  {
-    Trace("smt") << "SmtSolver::process global negate " << result << std::endl;
-    if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    ResourceManager* rm = d_env.getResourceManager();
+    if (rm->out())
     {
-      result = Result(Result::SAT);
+      Result::UnknownExplanation why =
+          rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
+      result = Result(Result::ENTAILMENT_UNKNOWN, why);
     }
-    else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
+    else
     {
-      // Only can answer unsat if the theory is satisfaction complete. This
-      // includes linear arithmetic and bitvectors, which are the primary
-      // targets for the global negate option. Other logics are possible here
-      // but not considered.
-      LogicInfo logic = d_env.getLogicInfo();
-      if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) ||
-          logic.isPure(theory::THEORY_BV))
+      rm->beginCall();
+
+      // Make sure the prop layer has all of the assertions
+      Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
+      processAssertions(as);
+      Trace("smt") << "SmtSolver::check(): done processing assertions" << endl;
+
+      TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);
+
+      d_env.verbose(2) << "solving..." << std::endl;
+      Trace("smt") << "SmtSolver::check(): running check" << endl;
+      result = d_propEngine->checkSat();
+      Trace("smt") << "SmtSolver::check(): result " << result << std::endl;
+
+      rm->endCall();
+      Trace("limit") << "SmtSolver::check(): cumulative millis "
+                     << rm->getTimeUsage() << ", resources "
+                     << rm->getResourceUsage() << endl;
+
+      if ((d_env.getOptions().smt.solveRealAsInt
+           || d_env.getOptions().smt.solveIntAsBV > 0)
+          && result.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
-        result = Result(Result::UNSAT);
+        result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
       }
-      else
+      // flipped if we did a global negation
+      if (as.isGlobalNegated())
       {
-        result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+        Trace("smt") << "SmtSolver::process global negate " << result
+                     << std::endl;
+        if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
+        {
+          result = Result(Result::SAT);
+        }
+        else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
+        {
+          // Only can answer unsat if the theory is satisfaction complete. This
+          // includes linear arithmetic and bitvectors, which are the primary
+          // targets for the global negate option. Other logics are possible
+          // here but not considered.
+          LogicInfo logic = d_env.getLogicInfo();
+          if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear())
+              || logic.isPure(theory::THEORY_BV))
+          {
+            result = Result(Result::UNSAT);
+          }
+          else
+          {
+            result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+          }
+        }
+        Trace("smt") << "SmtSolver::global negate returned " << result
+                     << std::endl;
       }
     }
-    Trace("smt") << "SmtSolver::global negate returned " << result << std::endl;
+  }
+  catch (const LogicException& e)
+  {
+    // The exception may have been throw during solving, backtrack to reset the
+    // decision level to the level expected after this method finishes
+    getPropEngine()->resetTrail();
+    throw;
   }
 
   // set the filename on the result
-  Result r = Result(result, filename);
+  const std::string& filename = d_env.getOptions().driver.filename;
+  result = Result(result, filename);
 
   // notify our state of the check-sat result
-  d_state.notifyCheckSatResult(hasAssumptions, r);
+  d_state.notifyCheckSatResult(hasAssumptions, result);
 
-  return r;
+  return result;
 }
 
 void SmtSolver::processAssertions(Assertions& as)

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 68cdf27806f993ac9a6f6ad0cc66ab16fb4fbded..4fb7dbc26efcd85972778f28c44dd45b2b247878 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -768,6 +768,8 @@ Result SolverEngine::checkEntailed(const std::vector<Node>& nodes)
 Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
                                       bool isEntailmentCheck)
 {
+  Result r;
+
   try
   {
     SolverEngineScope smts(this);
@@ -777,7 +779,7 @@ Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
                  << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
                  << assumptions << ")" << endl;
     // check the satisfiability with the solver object
-    Result r = d_smtSolver->checkSatisfiability(
+    r = d_smtSolver->checkSatisfiability(
         *d_asserts.get(), assumptions, isEntailmentCheck);
 
     Trace("smt") << "SolverEngine::"
@@ -809,13 +811,8 @@ Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
         checkUnsatCore();
       }
     }
-    if (d_env->getOptions().base.statisticsEveryQuery)
-    {
-      printStatisticsDiff();
-    }
-    return r;
   }
-  catch (UnsafeInterruptException& e)
+  catch (const UnsafeInterruptException& e)
   {
     AlwaysAssert(getResourceManager()->out());
     // Notice that we do not notify the state of this result. If we wanted to
@@ -826,13 +823,14 @@ Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
                                          ? Result::RESOURCEOUT
                                          : Result::TIMEOUT;
 
-    if (d_env->getOptions().base.statisticsEveryQuery)
-    {
-      printStatisticsDiff();
-    }
-    return Result(
-        Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename);
+    r = Result(Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename);
   }
+
+  if (d_env->getOptions().base.statisticsEveryQuery)
+  {
+    printStatisticsDiff();
+  }
+  return r;
 }
 
 std::vector<Node> SolverEngine::getUnsatAssumptions(void)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3e98a01adc15ba4c23d6ba67c934c07b137bb649..bc3880b189060a1430bd1f64db3bcf2404166aff 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1296,6 +1296,7 @@ set(regress_0_tests
   regress0/strings/issue6643-ctn-decompose-conflict.smt2
   regress0/strings/issue6681-split-eq-strip-l.smt2
   regress0/strings/issue6834-str-eq-const-nhomog.smt2
+  regress0/strings/issue7974-incomplete-neg-member.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/regress0/strings/issue7974-incomplete-neg-member.smt2 b/test/regress/regress0/strings/issue7974-incomplete-neg-member.smt2
new file mode 100644 (file)
index 0000000..6173c40
--- /dev/null
+++ b/test/regress/regress0/strings/issue7974-incomplete-neg-member.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --incremental
+; EXPECT: (error "Strings Incomplete (due to Negative Membership) by default, try --strings-exp option.")
+; EXIT: 1
+(set-logic ALL)
+(declare-fun v () String)
+(declare-fun a () Int)
+(push)
+(assert (and (= 0 (mod 0 a)) (not (str.in_re v (re.* (re.comp (str.to_re "")))))))
+(check-sat)
+(get-info :reason-unknown)