Non-implied mode for model cores (#2653)

3 files changed, 40 insertions, 16 deletions

diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index 1cbc18c1a..a077bb2fa 100644
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -21,7 +21,8 @@ using namespace CVC4::kind;
 namespace CVC4 {
 
 bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions,
-                                    Model* m)
+                                    Model* m,
+                                    ModelCoresMode mode)
 {
   if (Trace.isOn("model-core"))
   {
@@ -74,8 +75,22 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions,
 
   Trace("model-core") << "Minimizing substitution..." << std::endl;
   std::vector<Node> coreVars;
-  bool minimized =
-      theory::SubstitutionMinimize::find(formula, truen, vars, subs, coreVars);
+  std::vector<Node> impliedVars;
+  bool minimized = false;
+  if (mode == MODEL_CORES_NON_IMPLIED)
+  {
+    minimized = theory::SubstitutionMinimize::findWithImplied(
+        formula, vars, subs, coreVars, impliedVars);
+  }
+  else if (mode == MODEL_CORES_SIMPLE)
+  {
+    minimized = theory::SubstitutionMinimize::find(
+        formula, truen, vars, subs, coreVars);
+  }
+  else
+  {
+    Unreachable("Unknown model cores mode");
+  }
   Assert(minimized,
          "cannot compute model core, since model does not satisfy input!");
   if (minimized)
diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h
index 29348a4f4..a60a3767c 100644
--- a/src/smt/model_core_builder.h
+++ b/src/smt/model_core_builder.h
@@ -20,6 +20,7 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "options/smt_options.h"
 #include "smt/model.h"
 
 namespace CVC4 {
@@ -32,22 +33,30 @@ 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.
+   * This function updates model m so that it has information regarding its
+   * "model core". A model core for m is a substitution of the form
+   *    { s1 -> m(s1), ..., sn -> m(sn) }
    *
-   * It returns true if m is a model for assertions. In this case, we set:
+   * The criteria for what consistutes a model core given by mode. For
+   * example, if mode is MODEL_CORES_SIMPLE, then a model core corresponds to a
+   * subset of assignments from the model that suffice to show that the set of
+   * assertions, interpreted conjunctively, evaluates to true under the
+   * substitution corresponding to the model core.
+   *
+   * The model core is recorded on the model object m via calls to
+   * m->setUsingModelCore, m->recordModelCoreSymbol, for details see
+   * smt/model.h. In particular, we call:
    *   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.
+   * such that { s1 -> m(s1), ..., sn -> m(sn) } is the model core computed
+   * by this class.
    *
    * 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);
+  static bool setModelCore(const std::vector<Expr>& assertions,
+                           Model* m,
+                           ModelCoresMode mode);
 }; /* class TheoryModelCoreBuilder */
 
 }  // namespace CVC4
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a2dd8276b..63c970920 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1235,7 +1235,7 @@ void SmtEngine::setDefaults() {
   }
 
   if ((options::checkModels() || options::checkSynthSol()
-       || options::produceModelCores())
+       || options::modelCoresMode() != MODEL_CORES_NONE)
       && !options::produceAssertions())
   {
     Notice() << "SmtEngine: turning on produce-assertions to support "
@@ -1432,7 +1432,7 @@ void SmtEngine::setDefaults() {
   // cases where we need produce models
   if (!options::produceModels()
       && (options::produceAssignments() || options::sygusRewSynthCheck()
-          || options::produceModelCores() || is_sygus))
+          || is_sygus))
   {
     Notice() << "SmtEngine: turning on produce-models" << endl;
     setOption("produce-models", SExpr("true"));
@@ -4263,12 +4263,12 @@ Model* SmtEngine::getModel() {
   }
   TheoryModel* m = d_theoryEngine->getModel();
 
-  if (options::produceModelCores())
+  if (options::modelCoresMode() != MODEL_CORES_NONE)
   {
     // 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);
+    ModelCoreBuilder::setModelCore(easserts, m, options::modelCoresMode());
   }
   m->d_inputName = d_filename;
   return m;