From 94334c412be47c1555e52d9e20a6ff5e18817249 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 Dec 2020 03:10:39 -0600 Subject: Simplify and fix check models (#5685) Currently --check-models is implemented by replaying several preprocessing steps, including theory-specific expand definitions, and then checking whether the result evaluates to true. However, by having --check-models rely on complex preprocessing machinery defeats its purpose, as these steps are part of its trusted base. Moreover, issue #5645 demonstrates that this may lead to spurious errors where we incorrectly conclude that an input assertion is false, when it is not. This PR significantly simplifies --check-models so that it only relies on define-fun expansion + rewriting + evaluation. This ensures that --check-models is "sound" i.e. it does not falsely report a formula as evaluating to false. As a consequence, this makes check-models give warnings more often, i.e. when partial operators are involved, thus -q is added to silence warnings on some regressions. A followup PR will use a satisfiability check on the input formula post-expand-definitions to properly implement a trustworthy version of check-models that is robust for partial operators. Fixes #5645. --- src/smt/check_models.cpp | 154 +++------------------ test/regress/CMakeLists.txt | 1 + test/regress/regress0/datatypes/issue1433.smt2 | 2 + test/regress/regress0/decision/quant-ex1.smt2 | 2 +- .../regress0/fmf/QEpres-uf.855035.smtv1.smt2 | 2 +- test/regress/regress0/fp/issue3536.smt2 | 2 + test/regress/regress0/fp/issue3619.smt2 | 2 + test/regress/regress0/parser/to_fp.smt2 | 2 +- .../quantifiers/issue5645-dt-cm-spurious.smt2 | 5 + test/regress/regress1/arith/arith-brab-test.smt2 | 4 +- test/regress/regress1/bug507.smt2 | 1 + .../regress1/fmf/Hoare-z3.931718.smtv1.smt2 | 2 +- test/regress/regress1/fmf/am-bad-model.cvc | 1 + test/regress/regress1/fmf/refcount24.cvc.smt2 | 2 +- ...tersection-example-onelane.proof-node22337.smt2 | 2 +- test/regress/regress1/sets/choose3.smt2 | 4 +- .../regress1/wrong-qfabvfp-smtcomp2018.smt2 | 6 +- test/regress/regress2/issue3687-check-models.smt2 | 2 +- 18 files changed, 50 insertions(+), 146 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 2338ebd61..310201f47 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -54,129 +54,28 @@ void CheckModels::checkModel(Model* m, te->checkTheoryAssertionsWithModel(hardFailure); } - // Output the model - Notice() << *m; - - NodeManager* nm = NodeManager::currentNM(); Preprocessor* pp = d_smt.getPreprocessor(); - // We have a "fake context" for the substitution map (we don't need it - // to be context-dependent) - context::Context fakeContext; - SubstitutionMap substitutions(&fakeContext, - /* substituteUnderQuantifiers = */ false); - - Trace("check-model") << "checkModel: Collect substitution..." << std::endl; - const std::vector& decTerms = m->getDeclaredTerms(); - for (const Node& func : decTerms) - { - // We have a DECLARE-FUN: - // - // We'll first do some checks, then add to our substitution map - // the mapping: function symbol |-> value - - Node val = m->getValue(func); - - Notice() << "SmtEngine::checkModel(): adding substitution: " << func - << " |-> " << val << std::endl; - - // (1) if the value is a lambda, ensure the lambda doesn't contain the - // function symbol (since then the definition is recursive) - if (val.getKind() == kind::LAMBDA) - { - // first apply the model substitutions we have so far - Node n = substitutions.apply(val[1]); - // now check if n contains func by doing a substitution - // [func->func2] and checking equality of the Nodes. - // (this just a way to check if func is in n.) - SubstitutionMap subs(&fakeContext); - Node func2 = - nm->mkSkolem("", func.getType(), "", NodeManager::SKOLEM_NO_NOTIFY); - subs.addSubstitution(func, func2); - if (subs.apply(n) != n) - { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE DEFINED " - "IN TERMS OF ITSELF ***" - << std::endl; - std::stringstream ss; - ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH " - "MODEL:" - << std::endl - << "considering model value for " << func << std::endl - << "body of lambda is: " << val << std::endl; - if (n != val[1]) - { - ss << "body substitutes to: " << n << std::endl; - } - ss << "so " << func << " is defined in terms of itself." << std::endl - << "Run with `--check-models -v' for additional diagnostics."; - InternalError() << ss.str(); - } - } - - // (2) check that the value is actually a value - else if (!val.isConst()) - { - // This is only a warning since it could have been assigned an - // unevaluable term (e.g. an application of a transcendental function). - // This parallels the behavior (warnings for non-constant expressions) - // when checking whether assertions are satisfied below. - Warning() << "Warning : SmtEngine::checkModel(): " - << "model value for " << func << std::endl - << " is " << val << std::endl - << "and that is not a constant (.isConst() == false)." - << std::endl - << "Run with `--check-models -v' for additional diagnostics." - << std::endl; - } - - // (3) check that it's the correct (sub)type - // This was intended to be a more general check, but for now we can't do - // that because e.g. "1" is an INT, which isn't a subrange type [1..10] - // (etc.). - else if (func.getType().isInteger() && !val.getType().isInteger()) - { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT " - "CORRECT TYPE ***" - << std::endl; - InternalError() - << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH " - "MODEL:" - << std::endl - << "model value for " << func << std::endl - << " is " << val << std::endl - << "value type is " << val.getType() << std::endl - << "should be of type " << func.getType() << std::endl - << "Run with `--check-models -v' for additional diagnostics."; - } - - // (4) checks complete, add the substitution - Trace("check-model") << "Substitution: " << func << " :=> " << val - << std::endl; - substitutions.addSubstitution(func, val); - } - Trace("check-model") << "checkModel: Check assertions..." << std::endl; std::unordered_map cache; + // the list of assertions that did not rewrite to true + std::vector noCheckList; // Now go through all our user assertions checking if they're satisfied. for (const Node& assertion : *al) { Notice() << "SmtEngine::checkModel(): checking assertion " << assertion << std::endl; - Node n = assertion; - Notice() << "SmtEngine::checkModel(): -- rewritten form is " << Rewriter::rewrite(n) << std::endl; - Node nr = Rewriter::rewrite(substitutions.apply(n)); - if (nr.isConst() && nr.getConst()) - { - continue; - } - // Apply any define-funs from the problem. - n = pp->expandDefinitions(n, cache); + + // Apply any define-funs from the problem. We do not expand theory symbols + // like integer division here. Hence, the code below is not able to properly + // evaluate e.g. divide-by-zero. This is intentional since the evaluation + // is not trustworthy, since the UF introduced by expanding definitions may + // not be properly constrained. + Node n = pp->expandDefinitions(assertion, cache, true); Notice() << "SmtEngine::checkModel(): -- expands to " << n << std::endl; - // Apply our model value substitutions. - n = substitutions.apply(n); - Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << std::endl; + n = Rewriter::rewrite(n); + Notice() << "SmtEngine::checkModel(): -- rewrites to " << n << std::endl; // We look up the value before simplifying. If n contains quantifiers, // this may increases the chance of finding its value before the node is @@ -184,25 +83,6 @@ void CheckModels::checkModel(Model* m, n = m->getValue(n); Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl; - // Simplify the result - n = pp->simplify(n); - Notice() - << "SmtEngine::checkModel(): -- simplifies with ite replacement to " - << n << std::endl; - - // Apply our model value substitutions (again), as things may have been - // simplified. - n = substitutions.apply(n); - Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n - << std::endl; - - // As a last-ditch effort, ask model to simplify it. - // Presently, this is only an issue for quantifiers, which can have a value - // but don't show up in our substitution map above. - n = m->getValue(n); - Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n - << std::endl; - if (n.isConst() && n.getConst()) { // assertion is true, everything is fine @@ -229,6 +109,7 @@ void CheckModels::checkModel(Model* m, Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified " "assertion : " << n << std::endl; + noCheckList.push_back(n); continue; } // Assertions that simplify to false result in an InternalError or @@ -252,9 +133,16 @@ void CheckModels::checkModel(Model* m, Warning() << ss.str() << std::endl; } } + if (noCheckList.empty()) + { + Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" + << std::endl; + return; + } + // if the noCheckList is non-empty, we could expand definitions on this list + // and check satisfiability + Trace("check-model") << "checkModel: Finish" << std::endl; - Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" - << std::endl; } } // namespace smt diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 01903202c..d185049e0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -833,6 +833,7 @@ set(regress_0_tests regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 regress0/quantifiers/issue4437-unc-quant.smt2 regress0/quantifiers/issue4576.smt2 + regress0/quantifiers/issue5645-dt-cm-spurious.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macros-int-real.smt2 regress0/quantifiers/macros-real-arg.smt2 diff --git a/test/regress/regress0/datatypes/issue1433.smt2 b/test/regress/regress0/datatypes/issue1433.smt2 index bac9b8af1..edbd6da69 100644 --- a/test/regress/regress0/datatypes/issue1433.smt2 +++ b/test/regress/regress0/datatypes/issue1433.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_UFDTLIA) (set-info :status sat) (declare-datatype MyList (par (T) ((nelem) (cons (hd T) (tl (MyList T)))))) diff --git a/test/regress/regress0/decision/quant-ex1.smt2 b/test/regress/regress0/decision/quant-ex1.smt2 index 21fa06270..749b0e218 100644 --- a/test/regress/regress0/decision/quant-ex1.smt2 +++ b/test/regress/regress0/decision/quant-ex1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --decision=justification +; COMMAND-LINE: --decision=justification -q ; EXPECT: sat (set-logic AUFLIRA) diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 index 619779c78..32a75e846 100644 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find -q ; EXPECT: sat (set-option :incremental false) (set-info :status sat) diff --git a/test/regress/regress0/fp/issue3536.smt2 b/test/regress/regress0/fp/issue3536.smt2 index 4293cbdee..68a17347e 100644 --- a/test/regress/regress0/fp/issue3536.smt2 +++ b/test/regress/regress0/fp/issue3536.smt2 @@ -1,4 +1,6 @@ ; REQUIRES: symfpu +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_FP) (declare-const x (_ FloatingPoint 11 53)) (assert (= true (fp.eq x ((_ to_fp 11 53) (_ bv13831004815617530266 64))) true)) diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2 index 9d6e0a36d..3e0858035 100644 --- a/test/regress/regress0/fp/issue3619.smt2 +++ b/test/regress/regress0/fp/issue3619.smt2 @@ -1,4 +1,6 @@ ; REQUIRES: symfpu +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_FPLRA) (set-info :status sat) (declare-fun a () (_ FloatingPoint 11 53)) diff --git a/test/regress/regress0/parser/to_fp.smt2 b/test/regress/regress0/parser/to_fp.smt2 index 8652a5c33..277209ff8 100644 --- a/test/regress/regress0/parser/to_fp.smt2 +++ b/test/regress/regress0/parser/to_fp.smt2 @@ -1,5 +1,5 @@ ; REQUIRES: symfpu -; COMMAND-LINE: --strict-parsing +; COMMAND-LINE: --strict-parsing -q ; EXPECT: sat (set-logic QF_FP) (declare-fun |c::main::main::3::div@1!0&0#1| () (_ FloatingPoint 8 24)) diff --git a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 new file mode 100644 index 000000000..0d3f711bf --- /dev/null +++ b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((Enum1 0)) (((None) (cons (data Bool))))) +(assert (forall ((var_1 Enum1)) (data var_1))) +(check-sat) diff --git a/test/regress/regress1/arith/arith-brab-test.smt2 b/test/regress/regress1/arith/arith-brab-test.smt2 index 7856ae0e6..4d87fdbae 100644 --- a/test/regress/regress1/arith/arith-brab-test.smt2 +++ b/test/regress/regress1/arith/arith-brab-test.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --arith-brab -; COMMAND-LINE: --no-arith-brab +; COMMAND-LINE: --arith-brab -q +; COMMAND-LINE: --no-arith-brab -q ; EXPECT: sat (set-logic ALL) diff --git a/test/regress/regress1/bug507.smt2 b/test/regress/regress1/bug507.smt2 index b93229dfe..0176d1043 100644 --- a/test/regress/regress1/bug507.smt2 +++ b/test/regress/regress1/bug507.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: -q ; EXPECT: sat (set-logic QF_ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 b/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 index 8ee89145b..0bc9fe2bb 100644 --- a/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 +++ b/test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find -q ; EXPECT: sat (set-option :incremental false) (set-info :status sat) diff --git a/test/regress/regress1/fmf/am-bad-model.cvc b/test/regress/regress1/fmf/am-bad-model.cvc index e30b5e04a..75d4e9f3d 100644 --- a/test/regress/regress1/fmf/am-bad-model.cvc +++ b/test/regress/regress1/fmf/am-bad-model.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: -q % EXPECT: sat OPTION "produce-models"; OPTION "finite-model-find"; diff --git a/test/regress/regress1/fmf/refcount24.cvc.smt2 b/test/regress/regress1/fmf/refcount24.cvc.smt2 index e3b6957d0..2aaa28a3a 100644 --- a/test/regress/regress1/fmf/refcount24.cvc.smt2 +++ b/test/regress/regress1/fmf/refcount24.cvc.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 index fdbac9996..585ea0602 100644 --- a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 +++ b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv +; COMMAND-LINE: --cegqi-bv -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/sets/choose3.smt2 b/test/regress/regress1/sets/choose3.smt2 index 744192496..2a844efeb 100644 --- a/test/regress/regress1/sets/choose3.smt2 +++ b/test/regress/regress1/sets/choose3.smt2 @@ -1,7 +1,9 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic ALL) (set-info :status sat) (set-option :produce-models true) (declare-fun A () (Set Int)) (assert (= (choose A) 10)) (assert (= A (as emptyset (Set Int)))) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 index 3636b5795..c674c4039 100644 --- a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 +++ b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 @@ -1,6 +1,6 @@ ; REQUIRES: symfpu -; COMMAND-LINE: --decision=internal -; COMMAND-LINE: --decision=justification +; COMMAND-LINE: --decision=internal -q +; COMMAND-LINE: --decision=justification -q ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic QF_BVFP) @@ -12,4 +12,4 @@ (assert (or (= k2 b) (= k2 a))) (assert (or (fp.isNaN ((_ to_fp 11 53) k2)) (fp.gt ((_ to_fp 11 53) k2) ((_ to_fp 11 53) (_ bv4626322717216342016 64))) )) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2 index 02f7754cf..5c4155b83 100644 --- a/test/regress/regress2/issue3687-check-models.smt2 +++ b/test/regress/regress2/issue3687-check-models.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --check-models +; COMMAND-LINE: --check-models -q ; EXPECT: sat (set-logic QF_ABV) (declare-fun c () (_ BitVec 32)) -- cgit v1.2.3