Support model cores via option --produce-model-cores. (#2407)

This adds support for model cores, fixes #1233.

It includes some minor cleanup and additions to utility functions.

4 files changed, 191 insertions, 10 deletions

diff --git a/src/smt/model.h b/src/smt/model.h
index 927a055fd..3ad35fa5f 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -38,14 +38,14 @@ class Model {
   /** the input name (file name, etc.) this model is associated to */
   std::string d_inputName;
 
-protected:
+ protected:
   /** The SmtEngine we're associated with */
   SmtEngine& d_smt;
 
   /** construct the base class; users cannot do this, only CVC4 internals */
   Model();
 
-public:
+ public:
   /** virtual destructor */
   virtual ~Model() { }
   /** get number of commands to report */
@@ -58,9 +58,28 @@ public:
   const SmtEngine* getSmtEngine() const { return &d_smt; }
   /** get the input name (file name, etc.) this model is associated to */
   std::string getInputName() const { return d_inputName; }
-public:
-  /** Check whether this expr is a don't-care in the model */
-  virtual bool isDontCare(Expr expr) const { return false; }
+  //--------------------------- model cores
+  /** set using model core
+   *
+   * This sets that this model is minimized to be a "model core" for some
+   * formula (typically the input formula).
+   *
+   * For example, given formula ( a>5 OR b>5 ) AND f( c ) = 0,
+   * a model for this formula is: a -> 6, b -> 0, c -> 0, f -> lambda x. 0.
+   * A "model core" is a subset of this model that suffices to show the
+   * above formula is true, for example { a -> 6, f -> lambda x. 0 } is a
+   * model core for this formula.
+   */
+  virtual void setUsingModelCore() = 0;
+  /** record model core symbol
+   *
+   * This marks that sym is a "model core symbol". In other words, its value is
+   * critical to the satisfiability of the formula this model is for.
+   */
+  virtual void recordModelCoreSymbol(Expr sym) = 0;
+  /** Check whether this expr is in the model core */
+  virtual bool isModelCoreSymbol(Expr expr) const = 0;
+  //--------------------------- end model cores
   /** get value for expression */
   virtual Expr getValue(Expr expr) const = 0;
   /** get cardinality for sort */
diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
new file mode 100644
index 000000000..dbc6c5c9e
--- /dev/null
+++ b/src/smt/model_core_builder.cpp
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file model_core_builder.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 Implementation of utility for building model cores
+ **/
+
+#include "smt/model_core_builder.h"
+
+#include "theory/subs_minimize.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions,
+                                    Model* m)
+{
+  if (Trace.isOn("model-core"))
+  {
+    Trace("model-core") << "Compute model core, assertions:" << std::endl;
+    for (const Node& a : assertions)
+    {
+      Trace("model-core") << "  " << a << std::endl;
+    }
+  }
+
+  // convert to nodes
+  std::vector<Node> asserts;
+  for (unsigned i = 0, size = assertions.size(); i < size; i++)
+  {
+    asserts.push_back(Node::fromExpr(assertions[i]));
+  }
+  NodeManager* nm = NodeManager::currentNM();
+
+  Node formula = nm->mkNode(AND, asserts);
+  std::vector<Node> vars;
+  std::vector<Node> subs;
+  Trace("model-core") << "Assignments: " << std::endl;
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(formula);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isVar())
+      {
+        Node vcur = Node::fromExpr(m->getValue(cur.toExpr()));
+        Trace("model-core") << "  " << cur << " -> " << vcur << std::endl;
+        vars.push_back(cur);
+        subs.push_back(vcur);
+      }
+      if (cur.getMetaKind() == metakind::PARAMETERIZED)
+      {
+        visit.push_back(cur.getOperator());
+      }
+      visit.insert(visit.end(), cur.begin(), cur.end());
+    }
+  } while (!visit.empty());
+
+  Node truen = nm->mkConst(true);
+
+  Trace("model-core") << "Minimizing substitution..." << std::endl;
+  std::vector<Node> coreVars;
+  bool minimized =
+      theory::SubstitutionMinimize::find(formula, truen, vars, subs, coreVars);
+  Assert(minimized,
+         "cannot compute model core, since model does not satisfy input!");
+  if (minimized)
+  {
+    m->setUsingModelCore();
+    Trace("model-core") << "...got core vars : " << coreVars << std::endl;
+
+    for (const Node& cv : coreVars)
+    {
+      m->recordModelCoreSymbol(cv.toExpr());
+    }
+    return true;
+  }
+  Trace("model-core") << "...failed, model does not satisfy input!"
+                      << std::endl;
+  return false;
+}
+
+} /* namespace CVC4 */
diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h
new file mode 100644
index 000000000..29348a4f4
--- /dev/null
+++ b/src/smt/model_core_builder.h
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file model_core_builder.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 building model cores
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__MODEL_CORE_BUILDER_H
+#define __CVC4__THEORY__MODEL_CORE_BUILDER_H
+
+#include <vector>
+
+#include "expr/expr.h"
+#include "smt/model.h"
+
+namespace CVC4 {
+
+/**
+ * A utility for building model cores.
+ */
+class ModelCoreBuilder
+{
+ public:
+  /** set model core
+   *
+   * This function updates the model m so that it is a minimal "core" of
+   * substitutions that satisfy the formulas in assertions, interpreted
+   * conjunctively. This is specified via calls to
+   * Model::setUsingModelCore, Model::recordModelCoreSymbol,
+   * for details see smt/model.h.
+   *
+   * It returns true if m is a model for assertions. In this case, we set:
+   *   m->usingModelCore();
+   *   m->recordModelCoreSymbol(s1); ... m->recordModelCoreSymbol(sn);
+   * such that each formula in assertions under the substitution
+   * { s1 -> m(s1), ..., sn -> m(sn) } rewrites to true.
+   *
+   * If m is not a model for assertions, this method returns false and m is
+   * left unchanged.
+   */
+  static bool setModelCore(const std::vector<Expr>& assertions, Model* m);
+}; /* class TheoryModelCoreBuilder */
+
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__MODEL_CORE_BUILDER_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8cd236a89..73264daa5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -114,6 +114,7 @@
 #include "smt/command_list.h"
 #include "smt/logic_request.h"
 #include "smt/managed_ostreams.h"
+#include "smt/model_core_builder.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/term_formula_removal.h"
 #include "smt/update_ostream.h"
@@ -1255,12 +1256,13 @@ void SmtEngine::setDefaults() {
     is_sygus = true;
   }
 
-  if ((options::checkModels() || options::checkSynthSol())
+  if ((options::checkModels() || options::checkSynthSol()
+       || options::produceModelCores())
       && !options::produceAssertions())
   {
-      Notice() << "SmtEngine: turning on produce-assertions to support "
-               << "check-models or check-synth-sol." << endl;
-      setOption("produce-assertions", SExpr("true"));
+    Notice() << "SmtEngine: turning on produce-assertions to support "
+             << "check-models, check-synth-sol or produce-model-cores." << endl;
+    setOption("produce-assertions", SExpr("true"));
   }
 
   // Disable options incompatible with incremental solving, unsat cores, and
@@ -1452,7 +1454,7 @@ void SmtEngine::setDefaults() {
   // cases where we need produce models
   if (!options::produceModels()
       && (options::produceAssignments() || options::sygusRewSynthCheck()
-          || is_sygus))
+          || options::produceModelCores() || is_sygus))
   {
     Notice() << "SmtEngine: turning on produce-models" << endl;
     setOption("produce-models", SExpr("true"));
@@ -4125,6 +4127,14 @@ Model* SmtEngine::getModel() {
     throw ModalException(msg);
   }
   TheoryModel* m = d_theoryEngine->getModel();
+
+  if (options::produceModelCores())
+  {
+    // If we enabled model cores, we compute a model core for m based on our
+    // assertions using the model core builder utility
+    std::vector<Expr> easserts = getAssertions();
+    ModelCoreBuilder::setModelCore(easserts, m);
+  }
   m->d_inputName = d_filename;
   return m;
 }