summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp94
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/nl/issue3718.smt26
-rw-r--r--test/regress/regress1/rewriterules/datatypes_sat.smt22
-rw-r--r--test/regress/regress1/rewriterules/length_gen_020_sat.smt22
5 files changed, 61 insertions, 44 deletions
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<bool>())
+ {
+ // 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback