From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 7 Feb 2020 20:47:46 +0000 (-0600)
Subject: Refactor check-model handling in SmtEngine (#3723)
X-Git-Tag: cvc5-1.0.0~3672
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3962050ee990d942dad89fcbf118591995f279cd;p=cvc5.git

Refactor check-model handling in SmtEngine (#3723)
---

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