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.

18 files changed, 50 insertions, 146 deletions

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<Node>& 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<Node, Node, NodeHashFunction> cache;
+  // the list of assertions that did not rewrite to true
+  std::vector<Node> 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<bool>())
-    {
-      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<bool>())
     {
       // 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))