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.

1 files changed, 332 insertions, 0 deletions

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