From 3962050ee990d942dad89fcbf118591995f279cd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 7 Feb 2020 14:47:46 -0600 Subject: [PATCH] Refactor check-model handling in SmtEngine (#3723) --- src/smt/smt_engine.cpp | 94 ++++++++++--------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/nl/issue3718.smt2 | 6 ++ .../regress1/rewriterules/datatypes_sat.smt2 | 2 +- .../rewriterules/length_gen_020_sat.smt2 | 2 +- 5 files changed, 61 insertions(+), 44 deletions(-) create mode 100644 test/regress/regress0/nl/issue3718.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6a63a991f..4cb76eda6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4784,21 +4784,11 @@ void SmtEngine::checkModel(bool hardFailure) { Debug("boolean-terms") << "++ got " << n << endl; Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl; - if( n.getKind() != kind::REWRITE_RULE ){ - // In case it's a quantifier (or contains one), look up its value before - // simplifying, or the quantifier might be irreparably altered. - n = m->getValue(n); - Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl; - } else { - // Note this "skip" is done here, rather than above. This is - // because (1) the quantifier could in principle simplify to false, - // which should be reported, and (2) checking for the quantifier - // above, before simplification, doesn't catch buried quantifiers - // anyway (those not at the top-level). - Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion" - << endl; - continue; - } + // We look up the value before simplifying. If n contains quantifiers, + // this may increases the chance of finding its value before the node is + // altered by simplification below. + n = m->getValue(n); + Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl; // Simplify the result. n = d_private->simplify(n); @@ -4820,36 +4810,56 @@ void SmtEngine::checkModel(bool hardFailure) { n = m->getValue(n); Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl; - if( d_logic.isQuantified() ){ - // AJR: since quantified formulas are not checkable, we assign them to true/false based on the satisfying assignment. - // however, quantified formulas can be modified during preprocess, so they may not correspond to those in the satisfying assignment. - // hence we use a relaxed version of check model here. - // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas - if( hardFailure && !n.isConst() && n.getKind() != kind::LAMBDA ){ - Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl; - AlwaysAssert(expr::hasClosure(n)); - Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n << endl; + if (n.isConst()) + { + if (n.getConst()) + { + // assertion is true, everything is fine continue; } - }else{ - AlwaysAssert(!hardFailure || n.isConst() || n.getKind() == kind::LAMBDA); } - // The result should be == true. - if(n != NodeManager::currentNM()->mkConst(true)) { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" - << endl; - stringstream ss; - ss << "SmtEngine::checkModel(): " - << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl - << "assertion: " << *i << endl - << "simplifies to: " << n << endl - << "expected `true'." << endl - << "Run with `--check-models -v' for additional diagnostics."; - if(hardFailure) { - InternalError() << ss.str(); - } else { - Warning() << ss.str() << endl; - } + + // Otherwise, we did not succeed in showing the current assertion to be + // true. This may either indicate that our model is wrong, or that we cannot + // check it. The latter may be the case for several reasons. + // For example, quantified formulas are not checkable, although we assign + // them to true/false based on the satisfying assignment. However, + // quantified formulas can be modified during preprocess, so they may not + // correspond to those in the satisfying assignment. Hence we throw + // warnings for assertions that do not simplify to either true or false. + // Other theories such as non-linear arithmetic (in particular, + // transcendental functions) also have the property of not being able to + // be checked precisely here. + // Note that warnings like these can be avoided for quantified formulas + // by making preprocessing passes explicitly record how they + // rewrite quantified formulas (see cvc4-wishues#43). + if (!n.isConst()) + { + // Not constant, print a less severe warning message here. + Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified " + "assertion : " + << n << endl; + continue; + } + // Assertions that simplify to false result in an InternalError or + // Warning being thrown below (when hardFailure is false). + Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" + << endl; + stringstream ss; + ss << "SmtEngine::checkModel(): " + << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl + << "assertion: " << *i << endl + << "simplifies to: " << n << endl + << "expected `true'." << endl + << "Run with `--check-models -v' for additional diagnostics."; + if (hardFailure) + { + // internal error if hardFailure is true + InternalError() << ss.str(); + } + else + { + Warning() << ss.str() << endl; } } Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ef33adb59..ada5230d9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -558,6 +558,7 @@ set(regress_0_tests regress0/nl/issue3411.smt2 regress0/nl/issue3475.smt2 regress0/nl/issue3652.smt2 + regress0/nl/issue3718.smt2 regress0/nl/issue3719.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 diff --git a/test/regress/regress0/nl/issue3718.smt2 b/test/regress/regress0/nl/issue3718.smt2 new file mode 100644 index 000000000..363c1cb46 --- /dev/null +++ b/test/regress/regress0/nl/issue3718.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --quiet +; EXPECT: sat +(set-logic QF_NRAT) +(set-info :status sat) +(assert (= (sqrt 0) 0)) +(check-sat) diff --git a/test/regress/regress1/rewriterules/datatypes_sat.smt2 b/test/regress/regress1/rewriterules/datatypes_sat.smt2 index 428598c5b..ab32e4190 100644 --- a/test/regress/regress1/rewriterules/datatypes_sat.smt2 +++ b/test/regress/regress1/rewriterules/datatypes_sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --rewrite-rules +; COMMAND-LINE: --rewrite-rules --quiet ;; try to solve datatypes with rewriterules (set-logic AUFLIA) (set-info :status sat) diff --git a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 index 70511d9b3..d46065c73 100644 --- a/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 +++ b/test/regress/regress1/rewriterules/length_gen_020_sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --rewrite-rules +; COMMAND-LINE: --rewrite-rules --quiet ;; Same than length.smt2 but the nil case is not a rewrite rule ;; So here the rewrite rules have no guards length -- 2.30.2