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.

8 files changed, 453 insertions, 27 deletions

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 470f9ac7f..9ccaa58e9 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -57,6 +57,12 @@ unsigned getSignExtendAmount(TNode node)
 
 /* ------------------------------------------------------------------------- */
 
+bool isOnes(TNode node)
+{
+  if (!node.isConst()) return false;
+  return node == mkOnes(getSize(node));
+}
+
 bool isZero(TNode node)
 {
   if (!node.isConst()) return false;
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 9fccf92a7..2ece472e4 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -52,6 +52,9 @@ unsigned getExtractLow(TNode node);
 /* Get the number of bits by which a given node is extended. */
 unsigned getSignExtendAmount(TNode node);
 
+/* Returns true if given node represents a bit-vector comprised of ones.  */
+bool isOnes(TNode node);
+
 /* Returns true if given node represents a zero bit-vector.  */
 bool isZero(TNode node);
 
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index d0e6b0247..d2b7688ec 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -879,7 +879,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
   return false;
 }
 
-Node TermUtil::isSingularArg(Node n, Kind ik, int arg)
+Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
 {
   TypeNode tn = n.getType();
   if (n == getTypeValue(tn, 0))
@@ -918,10 +918,6 @@ Node TermUtil::isSingularArg(Node n, Kind ik, int arg)
       {
         return n;
       }
-      else
-      {
-        // TODO?
-      }
     }
     else if (ik == STRING_SUBSTR)
     {
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index bc936e4a3..dd3e76ee2 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -313,10 +313,10 @@ public:
 
   /** is singular arg
    * Returns true if
-   *   <k>( ... t_{arg-1}, n, t_{arg+1}...) = n
-   * always holds.
+   *   <k>( ... t_{arg-1}, n, t_{arg+1}...) = ret
+   * always holds for some constant ret, which is returned by this function.
    */
-  Node isSingularArg(Node n, Kind ik, int arg);
+  Node isSingularArg(Node n, Kind ik, unsigned arg);
 
   /** get type value
    * This gets the Node that represents value val for Type tn
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
new file mode 100644
index 000000000..03a55b3a4
--- /dev/null
+++ b/src/theory/subs_minimize.cpp
@@ -0,0 +1,332 @@
+/*********************                                                        */
+/*! \file subs_minimize.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 substitution minimization.
+ **/
+
+#include "theory/subs_minimize.h"
+
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+SubstitutionMinimize::SubstitutionMinimize() {}
+
+bool SubstitutionMinimize::find(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;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = value.find(cur);
+
+    if (it == value.end())
+    {
+      if (cur.isVar())
+      {
+        const std::vector<Node>::const_iterator& it =
+            std::find(vars.begin(), vars.end(), cur);
+        if (it == vars.end())
+        {
+          value[cur] = cur;
+        }
+        else
+        {
+          ptrdiff_t pos = std::distance(vars.begin(), it);
+          value[cur] = subs[pos];
+        }
+      }
+      else
+      {
+        value[cur] = Node::null();
+        visit.push_back(cur);
+        if (cur.getKind() == APPLY_UF)
+        {
+          visit.push_back(cur.getOperator());
+        }
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      if (cur.getNumChildren() > 0)
+      {
+        std::vector<Node> children;
+        NodeBuilder<> nb(cur.getKind());
+        if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+        {
+          if (cur.getKind() == APPLY_UF)
+          {
+            children.push_back(cur.getOperator());
+          }
+          else
+          {
+            nb << cur.getOperator();
+          }
+        }
+        children.insert(children.end(), cur.begin(), cur.end());
+        for (const Node& cn : children)
+        {
+          it = value.find(cn);
+          Assert(it != value.end());
+          Assert(!it->second.isNull());
+          nb << it->second;
+        }
+        ret = nb.constructNode();
+        ret = Rewriter::rewrite(ret);
+      }
+      value[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(value.find(n) != value.end());
+  Assert(!value.find(n)->second.isNull());
+
+  Trace("subs-min") << "... got " << value[n] << std::endl;
+  if (value[n] != target)
+  {
+    Trace("subs-min") << "... not equal to target " << target << std::endl;
+    return false;
+  }
+
+  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;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator itv;
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    itv = visited.find(cur);
+    if (itv == visited.end())
+    {
+      visited.insert(cur);
+      it = value.find(cur);
+      if (it->second == cur)
+      {
+        // if its value is the same as current, there is nothing to do
+      }
+      else if (cur.isVar())
+      {
+        // must include
+        rlvFv.insert(cur);
+      }
+      else if (cur.getKind() == ITE)
+      {
+        // only recurse on relevant branch
+        Node bval = value[cur[0]];
+        Assert(!bval.isNull() && bval.isConst());
+        unsigned cindex = bval.getConst<bool>() ? 1 : 2;
+        visit.push_back(cur[0]);
+        visit.push_back(cur[cindex]);
+      }
+      else if (cur.getNumChildren() > 0)
+      {
+        Kind ck = cur.getKind();
+        bool alreadyJustified = false;
+
+        // if the operator is an apply uf, check its value
+        if (cur.getKind() == APPLY_UF)
+        {
+          Node op = cur.getOperator();
+          it = value.find(op);
+          Assert(it != value.end());
+          TNode vop = it->second;
+          if (vop.getKind() == LAMBDA)
+          {
+            visit.push_back(op);
+            // do iterative partial evaluation on the body of the lambda
+            Node curr = vop[1];
+            for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++)
+            {
+              it = value.find(cur[i]);
+              Assert(it != value.end());
+              Node scurr = curr.substitute(vop[0][i], it->second);
+              // if the valuation of the i^th argument changes the
+              // interpretation of the body of the lambda, then the i^th
+              // argument is relevant to the substitution. Hence, we add
+              // i to visit, and update curr below.
+              if (scurr != curr)
+              {
+                curr = Rewriter::rewrite(scurr);
+                visit.push_back(cur[i]);
+              }
+            }
+            alreadyJustified = true;
+          }
+        }
+        if (!alreadyJustified)
+        {
+          // a subset of the arguments of cur that fully justify the evaluation
+          std::vector<unsigned> justifyArgs;
+          if (cur.getNumChildren() > 1)
+          {
+            for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++)
+            {
+              Node cn = cur[i];
+              it = value.find(cn);
+              Assert(it != value.end());
+              Assert(!it->second.isNull());
+              if (isSingularArg(it->second, ck, i))
+              {
+                // have we seen this argument already? if so, we are done
+                if (visited.find(cn) != visited.end())
+                {
+                  alreadyJustified = true;
+                  break;
+                }
+                justifyArgs.push_back(i);
+              }
+            }
+          }
+          // we need to recurse on at most one child
+          if (!alreadyJustified && !justifyArgs.empty())
+          {
+            unsigned sindex = justifyArgs[0];
+            // could choose a best index, for now, we just take the first
+            visit.push_back(cur[sindex]);
+            alreadyJustified = true;
+          }
+        }
+        if (!alreadyJustified)
+        {
+          // must recurse on all arguments, including operator
+          if (cur.getKind() == APPLY_UF)
+          {
+            visit.push_back(cur.getOperator());
+          }
+          for (const Node& cn : cur)
+          {
+            visit.push_back(cn);
+          }
+        }
+      }
+    }
+  } while (!visit.empty());
+
+  for (const Node& v : rlvFv)
+  {
+    Assert(std::find(vars.begin(), vars.end(), v) != vars.end());
+    reqVars.push_back(v);
+  }
+
+  Trace("subs-min") << "... requires " << reqVars.size() << "/" << vars.size()
+                    << " : " << reqVars << std::endl;
+
+  return true;
+}
+
+bool SubstitutionMinimize::isSingularArg(Node n, Kind k, unsigned arg)
+{
+  // Notice that this function is hardcoded. We could compute this function
+  // in a theory-independent way using partial evaluation. However, we
+  // prefer performance to generality here.
+
+  // TODO: a variant of this code is implemented in quantifiers::TermUtil.
+  // These implementations should be merged (see #1216).
+  if (!n.isConst())
+  {
+    return false;
+  }
+  if (k == AND)
+  {
+    return !n.getConst<bool>();
+  }
+  else if (k == OR)
+  {
+    return n.getConst<bool>();
+  }
+  else if (k == IMPLIES)
+  {
+    return arg == (n.getConst<bool>() ? 1 : 0);
+  }
+  if (k == MULT
+      || (arg == 0
+          && (k == DIVISION_TOTAL || k == INTS_DIVISION_TOTAL
+              || k == INTS_MODULUS_TOTAL))
+      || (arg == 2 && k == STRING_SUBSTR))
+  {
+    // zero
+    if (n.getConst<Rational>().sgn() == 0)
+    {
+      return true;
+    }
+  }
+  if (k == BITVECTOR_AND || k == BITVECTOR_MULT || k == BITVECTOR_UDIV_TOTAL
+      || k == BITVECTOR_UREM_TOTAL
+      || (arg == 0
+          && (k == BITVECTOR_SHL || k == BITVECTOR_LSHR
+              || k == BITVECTOR_ASHR)))
+  {
+    if (bv::utils::isZero(n))
+    {
+      return true;
+    }
+  }
+  if (k == BITVECTOR_OR)
+  {
+    // bit-vector ones
+    if (bv::utils::isOnes(n))
+    {
+      return true;
+    }
+  }
+
+  if ((arg == 1 && k == STRING_STRCTN) || (arg == 0 && k == STRING_SUBSTR))
+  {
+    // empty string
+    if (n.getConst<String>().size() == 0)
+    {
+      return true;
+    }
+  }
+  if ((arg != 0 && k == STRING_SUBSTR) || (arg == 2 && k == STRING_STRIDOF))
+  {
+    // negative integer
+    if (n.getConst<Rational>().sgn() < 0)
+    {
+      return true;
+    }
+  }
+  return false;
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h
new file mode 100644
index 000000000..55e57b921
--- /dev/null
+++ b/src/theory/subs_minimize.h
@@ -0,0 +1,66 @@
+/*********************                                                        */
+/*! \file subs_minimize.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 Substitution minimization.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SUBS_MINIMIZE_H
+#define __CVC4__THEORY__SUBS_MINIMIZE_H
+
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+/** SubstitutionMinimize
+ *
+ * This class is used for finding a minimal substitution under which an
+ * evaluation holds.
+ */
+class SubstitutionMinimize
+{
+ public:
+  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 n { vars -> subs } does not rewrite to target, this method returns
+   * false.
+   */
+  static bool find(Node n,
+                   Node target,
+                   const std::vector<Node>& vars,
+                   const std::vector<Node>& subs,
+                   std::vector<Node>& reqVars);
+
+ private:
+  /** is singular arg
+   *
+   * Returns true if
+   *   <k>( ... t_{arg-1}, n, t_{arg+1}...) = c
+   * always holds for some constant c.
+   */
+  static bool isSingularArg(Node n, Kind k, unsigned arg);
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* __CVC4__THEORY__SUBS_MINIMIZE_H */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 34e1d455b..2ccc48a6a 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -31,6 +31,7 @@ TheoryModel::TheoryModel(context::Context* c,
     : d_substitutions(c, false),
       d_modelBuilt(false),
       d_modelBuiltSuccess(false),
+      d_using_model_core(false),
       d_enableFuncModels(enableFuncModels)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
@@ -79,6 +80,8 @@ void TheoryModel::reset(){
   d_uf_models.clear();
   d_eeContext->pop();
   d_eeContext->push();
+  d_using_model_core = false;
+  d_model_core.clear();
 }
 
 void TheoryModel::getComments(std::ostream& out) const {
@@ -114,12 +117,13 @@ std::vector<std::pair<Expr, Expr> > TheoryModel::getApproximations() const
   return approx;
 }
 
-Node TheoryModel::getValue(TNode n, bool useDontCares) const {
+Node TheoryModel::getValue(TNode n) const
+{
   //apply substitutions
   Node nn = d_substitutions.apply(n);
   Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl;
   //get value in model
-  nn = getModelValue(nn, false, useDontCares);
+  nn = getModelValue(nn, false);
   if (nn.isNull()) return nn;
   if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
     //normalize
@@ -130,8 +134,15 @@ Node TheoryModel::getValue(TNode n, bool useDontCares) const {
   return nn;
 }
 
-bool TheoryModel::isDontCare(Expr expr) const {
-  return getValue(Node::fromExpr(expr), true).isNull();
+bool TheoryModel::isModelCoreSymbol(Expr sym) const
+{
+  if (!d_using_model_core)
+  {
+    return true;
+  }
+  Node s = Node::fromExpr(sym);
+  Assert(s.isVar() && s.getKind() != BOUND_VARIABLE);
+  return d_model_core.find(s) != d_model_core.end();
 }
 
 Expr TheoryModel::getValue( Expr expr ) const{
@@ -158,7 +169,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
   }
 }
 
-Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) const
+Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
 {
   std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
   if (it != d_modelCache.end()) {
@@ -303,10 +314,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c
     }
     else
     {
-      if (options::omitDontCares() && useDontCares)
-      {
-        return Node();
-      }
       // Unknown term - return first enumerated value for this type
       TypeEnumerator te(n.getType());
       ret = *te;
@@ -491,6 +498,16 @@ void TheoryModel::recordApproximation(TNode n, TNode pred)
   d_approximations[n] = pred;
   d_approx_list.push_back(std::pair<Node, Node>(n, pred));
 }
+void TheoryModel::setUsingModelCore()
+{
+  d_using_model_core = true;
+  d_model_core.clear();
+}
+
+void TheoryModel::recordModelCoreSymbol(Expr sym)
+{
+  d_model_core.insert(Node::fromExpr(sym));
+}
 
 void TheoryModel::setUnevaluatedKind(Kind k)
 {
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 47d68a365..3ffd1e8c1 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -223,10 +223,8 @@ public:
   /** Get value function.
    * This should be called only after a ModelBuilder
    * has called buildModel(...) on this model.
-   *   useDontCares is whether to return Node::null() if
-   *     n does not occur in the equality engine.
    */
-  Node getValue(TNode n, bool useDontCares = false) const;
+  Node getValue(TNode n) const;
   /** get comments */
   void getComments(std::ostream& out) const override;
 
@@ -245,8 +243,16 @@ public:
   const RepSet* getRepSet() const { return &d_rep_set; }
   /** get the representative set object (FIXME: remove this, see #1199) */
   RepSet* getRepSetPtr() { return &d_rep_set; }
-  /** return whether this node is a don't-care */
-  bool isDontCare(Expr expr) const override;
+
+  //---------------------------- model cores
+  /** set using model core */
+  void setUsingModelCore() override;
+  /** record model core symbol */
+  void recordModelCoreSymbol(Expr sym) override;
+  /** Return whether symbol expr is in the model core. */
+  bool isModelCoreSymbol(Expr sym) const override;
+  //---------------------------- end model cores
+
   /** get value function for Exprs. */
   Expr getValue(Expr expr) const override;
   /** get cardinality for sort */
@@ -301,16 +307,16 @@ public:
   Node d_false;
   /** comment stream to include in printing */
   std::stringstream d_comment_str;
+  /** are we using model cores? */
+  bool d_using_model_core;
+  /** symbols that are in the model core */
+  std::unordered_set<Node, NodeHashFunction> d_model_core;
   /** Get model value function.
    *
    * This function is a helper function for getValue.
    *   hasBoundVars is whether n may contain bound variables
-   *   useDontCares is whether to return Node::null() if
-   *     n does not occur in the equality engine.
    */
-  Node getModelValue(TNode n,
-                     bool hasBoundVars = false,
-                     bool useDontCares = false) const;
+  Node getModelValue(TNode n, bool hasBoundVars = false) const;
   /** add term internal
    *
    * This will do any model-specific processing necessary for n,