Non-implied mode for model cores (#2653)

13 files changed, 322 insertions, 66 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 676943b11..4cf8412f0 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -823,7 +823,7 @@ install(FILES
           options/printer_modes.h
           options/quantifiers_modes.h
           options/set_language.h
-          options/simplification_mode.h
+          options/smt_modes.h
           options/sygus_out_mode.h
           options/theoryof_mode.h
         DESTINATION
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 457fd23cd..dd0e34578 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -32,8 +32,8 @@ libcvc4_add_sources(
   quantifiers_modes.h
   set_language.cpp
   set_language.h
-  simplification_mode.cpp
-  simplification_mode.h
+  smt_modes.cpp
+  smt_modes.h
   sygus_out_mode.h
   theoryof_mode.cpp
   theoryof_mode.h
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index c311e04d8..54047efcc 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -96,8 +96,8 @@ liboptions_la_SOURCES = \
 	quantifiers_modes.h \
 	set_language.cpp \
 	set_language.h \
-	simplification_mode.cpp \
-	simplification_mode.h \
+	smt_modes.cpp \
+	smt_modes.h \
 	sygus_out_mode.h \
 	theoryof_mode.cpp \
 	theoryof_mode.h \
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index be2d7883d..46663ce7c 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -42,8 +42,6 @@
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/printer_modes.h"
-#include "options/quantifiers_modes.h"
-#include "options/simplification_mode.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/theoryof_mode.h"
@@ -1472,6 +1470,51 @@ SimplificationMode OptionsHandler::stringToSimplificationMode(
   }
 }
 
+const std::string OptionsHandler::s_modelCoresHelp =
+    "\
+Model cores modes currently supported by the --simplification option:\n\
+\n\
+none (default) \n\
++ do not compute model cores\n\
+\n\
+simple\n\
++ only include a subset of variables whose values are sufficient to show the\n\
+input formula is satisfied by the given model\n\
+\n\
+non-implied\n\
++ only include a subset of variables whose values, in addition to the values\n\
+of variables whose values are implied, are sufficient to show the input\n\
+formula is satisfied by the given model\n\
+\n\
+";
+
+ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option,
+                                                      std::string optarg)
+{
+  if (optarg == "none")
+  {
+    return MODEL_CORES_NONE;
+  }
+  else if (optarg == "simple")
+  {
+    return MODEL_CORES_SIMPLE;
+  }
+  else if (optarg == "non-implied")
+  {
+    return MODEL_CORES_NON_IMPLIED;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_modelCoresHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --model-cores: `")
+                          + optarg + "'.  Try --model-cores help.");
+  }
+}
+
 const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
     "\
 Modes for finite model finding bound minimization, supported by --sygus-out:\n\
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 0205b0b73..3078db0f8 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -35,7 +35,7 @@
 #include "options/options.h"
 #include "options/printer_modes.h"
 #include "options/quantifiers_modes.h"
-#include "options/simplification_mode.h"
+#include "options/smt_modes.h"
 #include "options/sygus_out_mode.h"
 #include "options/theoryof_mode.h"
 #include "options/ufss_mode.h"
@@ -171,6 +171,7 @@ public:
   void notifyDumpMode(std::string option);
   SimplificationMode stringToSimplificationMode(std::string option,
                                                 std::string optarg);
+  ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg);
   SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option,
                                                     std::string optarg);
   void setProduceAssertions(std::string option, bool value);
@@ -241,6 +242,7 @@ public:
   static const std::string s_qcfModeHelp;
   static const std::string s_qcfWhenModeHelp;
   static const std::string s_simplificationHelp;
+  static const std::string s_modelCoresHelp;
   static const std::string s_sygusSolutionOutModeHelp;
   static const std::string s_cbqiBvIneqModeHelp;
   static const std::string s_cegqiSingleInvHelp;
diff --git a/src/options/simplification_mode.cpp b/src/options/smt_modes.cpp
index 6b6fc842d..4a2fd404c 100644
--- a/src/options/simplification_mode.cpp
+++ b/src/options/smt_modes.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file simplification_mode.cpp
+/*! \file smt_modes.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
@@ -15,25 +15,22 @@
  ** \todo document this file
  **/
 
-#include "options/simplification_mode.h"
+#include "options/smt_modes.h"
 
 #include <iostream>
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, SimplificationMode mode) {
-  switch(mode) {
-  case SIMPLIFICATION_MODE_BATCH:
-    out << "SIMPLIFICATION_MODE_BATCH";
-    break;
-  case SIMPLIFICATION_MODE_NONE:
-    out << "SIMPLIFICATION_MODE_NONE";
-    break;
-  default:
-    out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";
+std::ostream& operator<<(std::ostream& out, SimplificationMode mode)
+{
+  switch (mode)
+  {
+    case SIMPLIFICATION_MODE_BATCH: out << "SIMPLIFICATION_MODE_BATCH"; break;
+    case SIMPLIFICATION_MODE_NONE: out << "SIMPLIFICATION_MODE_NONE"; break;
+    default: out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";
   }
 
   return out;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC4
diff --git a/src/options/simplification_mode.h b/src/options/smt_modes.h
index 52bf25fa1..761f3be01 100644
--- a/src/options/simplification_mode.h
+++ b/src/options/smt_modes.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file simplification_mode.h
+/*! \file smt_modes.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
@@ -17,23 +17,42 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H
-#define __CVC4__SMT__SIMPLIFICATION_MODE_H
+#ifndef __CVC4__SMT__MODES_H
+#define __CVC4__SMT__MODES_H
 
 #include <iosfwd>
 
 namespace CVC4 {
 
 /** Enumeration of simplification modes (when to simplify). */
-typedef enum {
+enum SimplificationMode
+{
   /** Simplify the assertions all together once a check is requested */
   SIMPLIFICATION_MODE_BATCH,
   /** Don't do simplification */
   SIMPLIFICATION_MODE_NONE
-} SimplificationMode;
-
-std::ostream& operator<<(std::ostream& out, SimplificationMode mode) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__SIMPLIFICATION_MODE_H */
+};
+
+std::ostream& operator<<(std::ostream& out,
+                         SimplificationMode mode) CVC4_PUBLIC;
+
+/** Enumeration of model core modes. */
+enum ModelCoresMode
+{
+  /** Do not compute model cores */
+  MODEL_CORES_NONE,
+  /**
+   * Compute "simple" model cores that exclude variables that do not
+   * contribute to satisfying the input.
+   */
+  MODEL_CORES_SIMPLE,
+  /**
+   * Compute model cores that also exclude variables whose variables are implied
+   * by others.
+   */
+  MODEL_CORES_NON_IMPLIED
+};
+
+}  // namespace CVC4
+
+#endif /* __CVC4__SMT__MODES_H */
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 8af1000ba..e0041774a 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -40,7 +40,7 @@ header = "options/smt_options.h"
   type       = "SimplificationMode"
   default    = "SIMPLIFICATION_MODE_BATCH"
   handler    = "stringToSimplificationMode"
-  includes   = ["options/simplification_mode.h"]
+  includes   = ["options/smt_modes.h"]
   help       = "choose simplification mode, see --simplification=help"
 
 [[alias]]
@@ -99,13 +99,14 @@ header = "options/smt_options.h"
   help       = "output models after every SAT/INVALID/UNKNOWN response"
 
 [[option]]
-  name       = "produceModelCores"
+  name       = "modelCoresMode"
   category   = "regular"
-  long       = "produce-model-cores"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "when printing models, compute a minimal core of relevant definitions"
+  long       = "model-cores=MODE"
+  type       = "ModelCoresMode"
+  default    = "MODEL_CORES_NONE"
+  handler    = "stringToModelCoresMode"
+  includes   = ["options/smt_modes.h"]
+  help       = "mode for producing model cores"
 
 [[option]]
   name       = "proof"
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;
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index 03a55b3a4..58daf5c75 100644
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/subs_minimize.h"
 
+#include "expr/node_algorithm.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
@@ -25,20 +26,157 @@ namespace theory {
 
 SubstitutionMinimize::SubstitutionMinimize() {}
 
-bool SubstitutionMinimize::find(Node n,
+bool SubstitutionMinimize::find(Node t,
                                 Node target,
                                 const std::vector<Node>& vars,
                                 const std::vector<Node>& subs,
                                 std::vector<Node>& reqVars)
 {
+  return findInternal(t, target, vars, subs, reqVars);
+}
+
+void getConjuncts(Node n, std::vector<Node>& conj)
+{
+  if (n.getKind() == AND)
+  {
+    for (const Node& nc : n)
+    {
+      conj.push_back(nc);
+    }
+  }
+  else
+  {
+    conj.push_back(n);
+  }
+}
+
+bool SubstitutionMinimize::findWithImplied(Node t,
+                                           const std::vector<Node>& vars,
+                                           const std::vector<Node>& subs,
+                                           std::vector<Node>& reqVars,
+                                           std::vector<Node>& impliedVars)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node truen = nm->mkConst(true);
+  if (!findInternal(t, truen, vars, subs, reqVars))
+  {
+    return false;
+  }
+  if (reqVars.empty())
+  {
+    return true;
+  }
+
+  // map from conjuncts of t to whether they may be used to show an implied var
+  std::vector<Node> tconj;
+  getConjuncts(t, tconj);
+  // map from conjuncts to their free symbols
+  std::map<Node, std::unordered_set<Node, NodeHashFunction> > tcFv;
+
+  std::unordered_set<Node, NodeHashFunction> reqSet;
+  std::vector<Node> reqSubs;
+  std::map<Node, unsigned> reqVarToIndex;
+  for (const Node& v : reqVars)
+  {
+    reqVarToIndex[v] = reqSubs.size();
+    const std::vector<Node>::const_iterator& it =
+        std::find(vars.begin(), vars.end(), v);
+    Assert(it != vars.end());
+    ptrdiff_t pos = std::distance(vars.begin(), it);
+    reqSubs.push_back(subs[pos]);
+  }
+  std::vector<Node> finalReqVars;
+  for (const Node& v : vars)
+  {
+    if (reqVarToIndex.find(v) == reqVarToIndex.end())
+    {
+      // not a required variable, nothing to do
+      continue;
+    }
+    unsigned vindex = reqVarToIndex[v];
+    Node prev = reqSubs[vindex];
+    // make identity substitution
+    reqSubs[vindex] = v;
+    bool madeImplied = false;
+    // it is a required variable, can we make an implied variable?
+    for (const Node& tc : tconj)
+    {
+      // ensure we've computed its free symbols
+      std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator
+          itf = tcFv.find(tc);
+      if (itf == tcFv.end())
+      {
+        expr::getSymbols(tc, tcFv[tc]);
+        itf = tcFv.find(tc);
+      }
+      // only have a chance if contains v
+      if (itf->second.find(v) == itf->second.end())
+      {
+        continue;
+      }
+      // try the current substitution
+      Node tcs = tc.substitute(
+          reqVars.begin(), reqVars.end(), reqSubs.begin(), reqSubs.end());
+      Node tcsr = Rewriter::rewrite(tcs);
+      std::vector<Node> tcsrConj;
+      getConjuncts(tcsr, tcsrConj);
+      for (const Node& tcc : tcsrConj)
+      {
+        if (tcc.getKind() == EQUAL)
+        {
+          for (unsigned r = 0; r < 2; r++)
+          {
+            if (tcc[r] == v)
+            {
+              Node res = tcc[1 - r];
+              if (res.isConst())
+              {
+                Assert(res == prev);
+                madeImplied = true;
+                break;
+              }
+            }
+          }
+        }
+        if (madeImplied)
+        {
+          break;
+        }
+      }
+      if (madeImplied)
+      {
+        break;
+      }
+    }
+    if (!madeImplied)
+    {
+      // revert the substitution
+      reqSubs[vindex] = prev;
+      finalReqVars.push_back(v);
+    }
+    else
+    {
+      impliedVars.push_back(v);
+    }
+  }
+  reqVars.clear();
+  reqVars.insert(reqVars.end(), finalReqVars.begin(), finalReqVars.end());
+
+  return true;
+}
+
+bool SubstitutionMinimize::findInternal(Node n,
+                                        Node target,
+                                        const std::vector<Node>& vars,
+                                        const std::vector<Node>& subs,
+                                        std::vector<Node>& reqVars)
+{
   Trace("subs-min") << "Substitution minimize : " << std::endl;
   Trace("subs-min") << "  substitution : " << vars << " -> " << subs
                     << std::endl;
   Trace("subs-min") << "  node : " << n << std::endl;
   Trace("subs-min") << "  target : " << target << std::endl;
 
-  std::map<Node, std::unordered_set<Node, NodeHashFunction> > fvDepend;
-
   Trace("subs-min") << "--- Compute values for subterms..." << std::endl;
   // the value of each subterm in n under the substitution
   std::unordered_map<TNode, Node, TNodeHashFunction> value;
@@ -124,8 +262,6 @@ bool SubstitutionMinimize::find(Node n,
   Trace("subs-min") << "--- Compute relevant variables..." << std::endl;
   std::unordered_set<Node, NodeHashFunction> rlvFv;
   // only variables that occur in assertions are relevant
-  std::map<Node, unsigned> iteBranch;
-  std::map<Node, std::vector<unsigned> > justifyArgs;
 
   visit.push_back(n);
   std::unordered_set<TNode, TNodeHashFunction> visited;
diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h
index 55e57b921..bf6ccffae 100644
--- a/src/theory/subs_minimize.h
+++ b/src/theory/subs_minimize.h
@@ -36,21 +36,55 @@ class SubstitutionMinimize
   ~SubstitutionMinimize() {}
   /** find
    *
-   * If n { vars -> subs } rewrites to target, this method returns true, and
-   * vars[i1], ..., vars[in] are added to rewVars, such that
-   * n { vars[i_1] -> subs[i_1], ..., vars[i_n] -> subs[i_n] } also rewrites to
-   * target.
+   * If t { vars -> subs } rewrites to target, this method returns true, and
+   * vars[i_1], ..., vars[i_n] are added to reqVars, such that i_1, ..., i_n are
+   * distinct, and t { vars[i_1] -> subs[i_1], ..., vars[i_n] -> subs[i_n] }
+   * rewrites to target.
    *
-   * If n { vars -> subs } does not rewrite to target, this method returns
+   * If t { vars -> subs } does not rewrite to target, this method returns
    * false.
    */
-  static bool find(Node n,
+  static bool find(Node t,
                    Node target,
                    const std::vector<Node>& vars,
                    const std::vector<Node>& subs,
                    std::vector<Node>& reqVars);
+  /** find with implied
+   *
+   * This method should be called on a formula t.
+   *
+   * If t { vars -> subs } rewrites to true, this method returns true,
+   * vars[i_1], ..., vars[i_n] are added to reqVars, and
+   * vars[i_{n+1}], ..., vars[i_{n+m}] are added to impliedVars such that
+   * i_1...i_{n+m} are distinct, i_{n+1} < ... < i_{n+m}, and:
+   *
+   * (1) t { vars[i_1]->subs[i_1], ..., vars[i_{n+k}]->subs[i_{n+k}] } implies
+   * vars[i_{n+k+1}] = subs[i_{n+k+1}] for k = 0, ..., m-1.
+   *
+   * (2) t { vars[i_1] -> subs[i_1], ..., vars[i_{n+m}] -> subs[i_{n+m}] }
+   * rewrites to true.
+   *
+   * For example, given (x>0 ^ x = y ^ y = z){ x -> 1, y -> 1, z -> 1, w -> 0 },
+   * this method may add { x } to reqVars, and { y, z } to impliedVars.
+   *
+   * Notice that the order of variables in vars matters. By the semantics above,
+   * variables that appear earlier in the variable list vars are more likely
+   * to appear in reqVars, whereas those later in the vars are more likely to
+   * appear in impliedVars.
+   */
+  static bool findWithImplied(Node t,
+                              const std::vector<Node>& vars,
+                              const std::vector<Node>& subs,
+                              std::vector<Node>& reqVars,
+                              std::vector<Node>& impliedVars);
 
  private:
+  /** Common helper function for the above functions. */
+  static bool findInternal(Node t,
+                           Node target,
+                           const std::vector<Node>& vars,
+                           const std::vector<Node>& subs,
+                           std::vector<Node>& reqVars);
   /** is singular arg
    *
    * Returns true if