From 4303c4ee5a9234ee03904b16c519a0ce6fcd80d1 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 9 Feb 2022 10:42:37 -0800 Subject: [PATCH] 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. --- src/smt/smt_solver.cpp | 135 ++++++++++-------- src/smt/solver_engine.cpp | 24 ++-- test/regress/CMakeLists.txt | 1 + .../issue7974-incomplete-neg-member.smt2 | 10 ++ 4 files changed, 99 insertions(+), 71 deletions(-) create mode 100644 test/regress/regress0/strings/issue7974-incomplete-neg-member.smt2 diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 07d260c7e..2151dc03e 100644 --- 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& 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 68cdf2780..4fb7dbc26 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -768,6 +768,8 @@ Result SolverEngine::checkEntailed(const std::vector& nodes) Result SolverEngine::checkSatInternal(const std::vector& assumptions, bool isEntailmentCheck) { + Result r; + try { SolverEngineScope smts(this); @@ -777,7 +779,7 @@ Result SolverEngine::checkSatInternal(const std::vector& 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& 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& 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 SolverEngine::getUnsatAssumptions(void) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3e98a01ad..bc3880b18 100644 --- 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 index 000000000..6173c4087 --- /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) -- 2.30.2