From ee75ebf00e1aa463656cd192e52d3aec224345c0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 29 Feb 2020 10:28:27 -0600 Subject: [PATCH] Throw warning instead of error for non-constant values in check-model stages (#3844) Fixes #3729 and fixes #3720. This updates two more stages of check-model (checking whether values assigned to terms are constants and internally checking whether assertions belonging to theories) to only throw warnings when a term/assertion has a non-constant value in the model. This is to accommodate cases where check-model is infeasible. --- src/smt/smt_engine.cpp | 23 ++++++++++-------- src/theory/theory_engine.cpp | 24 ++++++++++++++----- test/regress/CMakeLists.txt | 2 ++ .../regress0/nl/issue3729-cm-solved-tf.smt2 | 7 ++++++ .../regress0/sep/issue3720-check-model.smt2 | 5 ++++ 5 files changed, 45 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 create mode 100644 test/regress/regress0/sep/issue3720-check-model.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 915dc603e..cde85a186 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4785,16 +4785,19 @@ void SmtEngine::checkModel(bool hardFailure) { } // (2) check that the value is actually a value - else if (!val.isConst()) { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl; - InternalError() - << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH " - "MODEL:" - << endl - << "model value for " << func << endl - << " is " << val << endl - << "and that is not a constant (.isConst() == false)." << endl - << "Run with `--check-models -v' for additional diagnostics."; + 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 << endl + << " is " << val << 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 diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d176b015d..e15641bb4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2268,14 +2268,26 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { Node val = getModel()->getValue(assertion); if (val != d_true) { + std::stringstream ss; + ss << theoryId + << " has an asserted fact that the model doesn't satisfy." << endl + << "The fact: " << assertion << endl + << "Model value: " << val << endl; if (hardFailure) { - InternalError() - << theoryId - << " has an asserted fact that the model doesn't satisfy." - << endl - << "The fact: " << assertion << endl - << "Model value: " << val << endl; + if (val == d_false) + { + // Always an error if it is false + InternalError() << ss.str(); + } + else + { + // Otherwise just a warning. Notice this case may happen for + // assertions with unevaluable operators, e.g. transcendental + // functions. It also may happen for separation logic, where + // check-model support is limited. + Warning() << ss.str(); + } } } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3cbc2953f..34f7a8713 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -573,6 +573,7 @@ set(regress_0_tests regress0/nl/issue3652.smt2 regress0/nl/issue3718.smt2 regress0/nl/issue3719.smt2 + regress0/nl/issue3729-cm-solved-tf.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 regress0/nl/nia-wrong-tl.smt2 @@ -811,6 +812,7 @@ set(regress_0_tests regress0/reset-assertions.smt2 regress0/sep/dispose-1.smt2 regress0/sep/dup-nemp.smt2 + regress0/sep/issue3720-check-model.smt2 regress0/sep/nemp.smt2 regress0/sep/nil-no-elim.smt2 regress0/sep/nspatial-simp.smt2 diff --git a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 new file mode 100644 index 000000000..69bb74e84 --- /dev/null +++ b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --quiet +; EXPECT: sat +(set-logic QF_NRAT) +(set-info :status sat) +(declare-fun a () Real) +(assert (= a (sin 1.0))) +(check-sat) diff --git a/test/regress/regress0/sep/issue3720-check-model.smt2 b/test/regress/regress0/sep/issue3720-check-model.smt2 new file mode 100644 index 000000000..6130c0ca8 --- /dev/null +++ b/test/regress/regress0/sep/issue3720-check-model.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --quiet +; EXPECT: sat +(set-logic ALL) +(assert (_ emp Int Int)) +(check-sat) -- 2.30.2