Split CheckModels utility to its own file (#5303)

This utility will be undergoing major additions to make it more robust. Thus it should be moved to its own file.

There are no major code changes in this PR, a few things were changed to be consistent to the coding standard.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index ec8aaf8dcc0e6056dcf43429d9df11bf8a1fef68..29f5a57d4c8ca97d5379cbfb6f0a216a7d1f95fa 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -208,6 +208,8 @@ libcvc4_add_sources(
   smt/abstract_values.h
   smt/assertions.cpp
   smt/assertions.h
+  smt/check_models.cpp
+  smt/check_models.h
   smt/command.cpp
   smt/command.h
   smt/defined_function.h

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
new file mode 100644 (file)
index 0000000..a55f53f
--- /dev/null
+++ b/src/smt/check_models.cpp
@@ -0,0 +1,271 @@
+/*********************                                                        */
+/*! \file check_models.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utility for constructing and maintaining abstract values.
+ **/
+
+#include "smt/check_models.h"
+
+#include "options/smt_options.h"
+#include "smt/node_command.h"
+#include "smt/preprocessor.h"
+#include "theory/rewriter.h"
+#include "theory/substitutions.h"
+#include "theory/theory_engine.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+CheckModels::CheckModels(SmtSolver& s) : d_smt(s) {}
+CheckModels::~CheckModels() {}
+
+void CheckModels::checkModel(Model* m,
+                             context::CDList<Node>* al,
+                             bool hardFailure)
+{
+  // Throughout, we use Notice() to give diagnostic output.
+  //
+  // If this function is running, the user gave --check-model (or equivalent),
+  // and if Notice() is on, the user gave --verbose (or equivalent).
+
+  // check-model is not guaranteed to succeed if approximate values were used.
+  // Thus, we intentionally abort here.
+  if (m->hasApproximations())
+  {
+    throw RecoverableModalException(
+        "Cannot run check-model on a model with approximate values.");
+  }
+
+  // Check individual theory assertions
+  if (options::debugCheckModels())
+  {
+    TheoryEngine* te = d_smt.getTheoryEngine();
+    Assert(te != nullptr);
+    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;
+  for (size_t k = 0, ncmd = m->getNumCommands(); k < ncmd; ++k)
+  {
+    const DeclareFunctionNodeCommand* c =
+        dynamic_cast<const DeclareFunctionNodeCommand*>(m->getCommand(k));
+    Notice() << "SmtEngine::checkModel(): model command " << k << " : "
+             << m->getCommand(k)->toString() << std::endl;
+    if (c == nullptr)
+    {
+      // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
+      Notice() << "SmtEngine::checkModel(): skipping..." << std::endl;
+      continue;
+    }
+    // We have a DECLARE-FUN:
+    //
+    // We'll first do some checks, then add to our substitution map
+    // the mapping: function symbol |-> value
+
+    Node func = c->getFunction();
+    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;
+  // 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;
+    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);
+    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;
+
+    // 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 and replace the already-known ITEs (this is important
+    // for ground ITEs under quantifiers).
+    n = pp->simplify(n, true);
+    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
+      continue;
+    }
+
+    // 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 << std::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' ***"
+             << std::endl;
+    std::stringstream ss;
+    ss << "SmtEngine::checkModel(): "
+       << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl
+       << "assertion:     " << assertion << std::endl
+       << "simplifies to: " << n << std::endl
+       << "expected `true'." << std::endl
+       << "Run with `--check-models -v' for additional diagnostics.";
+    if (hardFailure)
+    {
+      // internal error if hardFailure is true
+      InternalError() << ss.str();
+    }
+    else
+    {
+      Warning() << ss.str() << std::endl;
+    }
+  }
+  Trace("check-model") << "checkModel: Finish" << std::endl;
+  Notice() << "SmtEngine::checkModel(): all assertions checked out OK !"
+           << std::endl;
+}
+
+}  // namespace smt
+}  // namespace CVC4

diff --git a/src/smt/check_models.h b/src/smt/check_models.h
new file mode 100644 (file)
index 0000000..14af41b
--- /dev/null
+++ b/src/smt/check_models.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file check_models.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Utility for checking models
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__CHECK_MODELS_H
+#define CVC4__SMT__CHECK_MODELS_H
+
+#include "context/cdlist.h"
+#include "expr/node.h"
+#include "smt/model.h"
+#include "smt/smt_solver.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * This utility is responsible for checking the current model.
+ */
+class CheckModels
+{
+ public:
+  CheckModels(SmtSolver& s);
+  ~CheckModels();
+  /**
+   * Check model m against the current set of input assertions al.
+   *
+   * This throws an exception if we fail to verify that m is a proper model
+   * given assertion list al based on the model checking policy.
+   */
+  void checkModel(Model* m, context::CDList<Node>* al, bool hardFailure);
+
+ private:
+  /** Reference to the SMT solver */
+  SmtSolver& d_smt;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2f9918486b7d2c2020a2b5f42beb7a5d3139940d..343b79966bc6813bf591e7b8348aa702e32da68c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -16,19 +16,6 @@
 
 #include "smt/smt_engine.h"
 
-#include <algorithm>
-#include <cctype>
-#include <iterator>
-#include <memory>
-#include <sstream>
-#include <stack>
-#include <string>
-#include <tuple>
-#include <unordered_map>
-#include <unordered_set>
-#include <utility>
-#include <vector>
-
 #include "api/cvc4cpp.h"
 #include "base/check.h"
 #include "base/configuration.h"
@@ -36,41 +23,25 @@
 #include "base/exception.h"
 #include "base/modal_exception.h"
 #include "base/output.h"
-#include "context/cdhashmap.h"
-#include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "context/context.h"
 #include "decision/decision_engine.h"
-#include "expr/attribute.h"
-#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
 #include "expr/node.h"
-#include "expr/node_algorithm.h"
-#include "expr/node_builder.h"
 #include "expr/node_self_iterator.h"
 #include "expr/node_visitor.h"
 #include "options/base_options.h"
-#include "options/decision_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
-#include "options/open_ostream.h"
 #include "options/option_exception.h"
 #include "options/printer_options.h"
-#include "options/prop_options.h"
-#include "options/quantifiers_options.h"
 #include "options/set_language.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
-#include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "printer/printer.h"
 #include "proof/proof_manager.h"
 #include "proof/unsat_core.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
+#include "smt/check_models.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
 #include "smt/expr_names.h"
@@ -91,16 +62,10 @@
 #include "smt/sygus_solver.h"
 #include "smt/term_formula_removal.h"
 #include "smt/update_ostream.h"
-#include "smt_util/boolean_simplification.h"
-#include "smt_util/nary_builder.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
-#include "theory/sort_inference.h"
-#include "theory/substitutions.h"
 #include "theory/theory_engine.h"
-#include "theory/theory_model.h"
-#include "theory/theory_traits.h"
 #include "util/hash.h"
 #include "util/random.h"
 #include "util/resource_manager.h"
@@ -128,6 +93,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_smtSolver(nullptr),
       d_proofManager(nullptr),
       d_model(nullptr),
+      d_checkModels(nullptr),
       d_pfManager(nullptr),
       d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
@@ -282,6 +248,8 @@ void SmtEngine::finishInit()
   if (tm != nullptr)
   {
     d_model.reset(new Model(*this, tm));
+    // make the check models utility
+    d_checkModels.reset(new CheckModels(*d_smtSolver.get()));
   }
 
   // global push/pop around everything, to ensure proper destruction
@@ -1557,229 +1525,13 @@ void SmtEngine::checkModel(bool hardFailure) {
 
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
 
-  // Throughout, we use Notice() to give diagnostic output.
-  //
-  // If this function is running, the user gave --check-model (or equivalent),
-  // and if Notice() is on, the user gave --verbose (or equivalent).
-
   Notice() << "SmtEngine::checkModel(): generating model" << endl;
   Model* m = getAvailableModel("check model");
   Assert(m != nullptr);
 
-  // check-model is not guaranteed to succeed if approximate values were used.
-  // Thus, we intentionally abort here.
-  if (m->hasApproximations())
-  {
-    throw RecoverableModalException(
-        "Cannot run check-model on a model with approximate values.");
-  }
-
-  // Check individual theory assertions
-  if (options::debugCheckModels())
-  {
-    TheoryEngine* te = getTheoryEngine();
-    Assert(te != nullptr);
-    te->checkTheoryAssertionsWithModel(hardFailure);
-  }
-
-  // Output the model
-  Notice() << *m;
-
-  // 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);
-
-  for(size_t k = 0; k < m->getNumCommands(); ++k) {
-    const DeclareFunctionNodeCommand* c =
-        dynamic_cast<const DeclareFunctionNodeCommand*>(m->getCommand(k));
-    Notice() << "SmtEngine::checkModel(): model command " << k << " : "
-             << m->getCommand(k)->toString() << endl;
-    if(c == NULL) {
-      // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ...
-      Notice() << "SmtEngine::checkModel(): skipping..." << endl;
-    } else {
-      // We have a DECLARE-FUN:
-      //
-      // We'll first do some checks, then add to our substitution map
-      // the mapping: function symbol |-> value
-
-      Node func = c->getFunction();
-      Node val = m->getValue(func);
-
-      Notice() << "SmtEngine::checkModel(): adding substitution: " << func << " |-> " << val << 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
-        Debug("boolean-terms") << "applying subses to " << val[1] << endl;
-        Node n = substitutions.apply(val[1]);
-        Debug("boolean-terms") << "++ got " << n << endl;
-        // 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 = NodeManager::currentNM()->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 ***" << endl;
-          stringstream ss;
-          ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
-             << "considering model value for " << func << endl
-             << "body of lambda is:   " << val << endl;
-          if(n != val[1]) {
-            ss << "body substitutes to: " << n << endl;
-          }
-          ss << "so " << func << " is defined in terms of itself." << 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 << 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
-      // 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 ***" << endl;
-        InternalError()
-            << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
-               "MODEL:"
-            << endl
-            << "model value for " << func << endl
-            << "             is " << val << endl
-            << "value type is     " << val.getType() << endl
-            << "should be of type " << func.getType() << endl
-            << "Run with `--check-models -v' for additional diagnostics.";
-      }
-
-      // (4) checks complete, add the substitution
-      Debug("boolean-terms") << "cm: adding subs " << func << " :=> " << val << endl;
-      substitutions.addSubstitution(func, val);
-    }
-  }
-
-  // Now go through all our user assertions checking if they're satisfied.
-  for (const Node& assertion : *al)
-  {
-    Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
-             << endl;
-    Node n = assertion;
-    Node nr = Rewriter::rewrite(substitutions.apply(n));
-    Trace("boolean-terms") << "n: " << n << endl;
-    Trace("boolean-terms") << "nr: " << nr << endl;
-    if (nr.isConst() && nr.getConst<bool>())
-    {
-      continue;
-    }
-    // Apply any define-funs from the problem.
-    {
-      unordered_map<Node, Node, NodeHashFunction> cache;
-      n = d_pp->expandDefinitions(n, cache);
-    }
-    Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
-
-    // Apply our model value substitutions.
-    Debug("boolean-terms") << "applying subses to " << n << endl;
-    n = substitutions.apply(n);
-    Debug("boolean-terms") << "++ got " << n << endl;
-    Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << 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
-    // altered by simplification below.
-    n = m->getValue(n);
-    Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
-
-    // Simplify the result and replace the already-known ITEs (this is important
-    // for ground ITEs under quantifiers).
-    n = d_pp->simplify(n, true);
-    Notice()
-        << "SmtEngine::checkModel(): -- simplifies with ite replacement to  "
-        << n << endl;
-
-    // Apply our model value substitutions (again), as things may have been simplified.
-    Debug("boolean-terms") << "applying subses to " << n << endl;
-    n = substitutions.apply(n);
-    Debug("boolean-terms") << "++ got " << n << endl;
-    Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n << 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 << endl;
-
-    if (n.isConst())
-    {
-      if (n.getConst<bool>())
-      {
-        // assertion is true, everything is fine
-        continue;
-      }
-    }
-
-    // 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:     " << assertion << 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;
+  // check the model with the check models utility
+  Assert(d_checkModels != nullptr);
+  d_checkModels->checkModel(m, al, hardFailure);
 }
 
 // TODO(#1108): Simplify the error reporting of this method.
@@ -1892,7 +1644,6 @@ void SmtEngine::getInstantiationTermVectors(
     Node q, std::vector<std::vector<Node>>& tvecs)
 {
   SmtScope smts(this);
-  Assert(options::trackInstLemmas());
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
   te->getInstantiationTermVectors(q, tvecs);

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index da12d336b913ffd20dc24c019e3e91cd29f98bc1..53e982a2d6b90f319bcd6bb273150b3d57e1aacc 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -104,6 +104,7 @@ class ResourceOutListener;
 class SmtNodeManagerListener;
 class OptionsManager;
 class Preprocessor;
+class CheckModels;
 /** Subsolvers */
 class SmtSolver;
 class SygusSolver;
@@ -1096,6 +1097,11 @@ class CVC4_PUBLIC SmtEngine
    */
   std::unique_ptr<smt::Model> d_model;
 
+  /**
+   * The utility used for checking models
+   */
+  std::unique_ptr<smt::CheckModels> d_checkModels;
+
   /**
    * The proof manager, which manages all things related to checking,
    * processing, and printing proofs.

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 8ff022556950cc509051eb523253f0b2d9be6a6a..26a2ff3e1d9384f34714106cddb97a00c9d197f6 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -260,5 +260,7 @@ TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
 
 prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
 
+Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; }
+
 }  // namespace smt
 }  // namespace CVC4

diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 037c9fb9c2c40cd44d75305bbf4ef627749eba6f..e3cbea152bd3af21fbd4fdbbf9d0bf303cbede00 100644 (file)
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -119,6 +119,8 @@ class SmtSolver
   TheoryEngine* getTheoryEngine();
   /** Get a pointer to the PropEngine owned by this solver. */
   prop::PropEngine* getPropEngine();
+  /** Get a pointer to the preprocessor */
+  Preprocessor* getPreprocessor();
   //------------------------------------------ end access methods
  private:
   /** Reference to the parent SMT engine */