Merge branch 'master' into fixMacBuildfixMacBuild

4 files changed, 212 insertions, 29 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 7c008dc14..1dc894117 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -507,9 +507,7 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node)
         }
 
         // (= "" (str.replace x "A" "")) ---> (str.prefix x "A")
-        Node one = nm->mkConst(Rational(1));
-        Node ylen = nm->mkNode(STRING_LENGTH, ne[1]);
-        if (checkEntailArithEq(ylen, one) && ne[2] == empty)
+        if (checkEntailLengthOne(ne[1]) && ne[2] == empty)
         {
           Node ret = nm->mkNode(STRING_PREFIX, ne[0], ne[1]);
           return returnRewrite(node, ret, "str-emp-repl-emp");
@@ -1658,11 +1656,8 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
     // if (str.len y) = 1 and (str.len z) = 1
     if (node[1] == zero)
     {
-      Node one = nm->mkConst(Rational(1));
-      Node n1len = nm->mkNode(kind::STRING_LENGTH, node[0][1]);
-      Node n2len = nm->mkNode(kind::STRING_LENGTH, node[0][2]);
-      if (checkEntailArith(one, n1len) && checkEntailArith(one, n2len)
-          && checkEntailNonEmpty(node[0][1]) && checkEntailNonEmpty(node[0][2]))
+      if (checkEntailLengthOne(node[0][1], true)
+          && checkEntailLengthOne(node[0][2], true))
       {
         Node ret = nm->mkNode(
             kind::STRING_STRREPL,
@@ -1739,8 +1734,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
       }
 
       // (str.substr s x x) ---> "" if (str.len s) <= 1
-      Node one = nm->mkConst(CVC4::Rational(1));
-      if (node[1] == node[2] && checkEntailArith(one, tot_len))
+      if (node[1] == node[2] && checkEntailLengthOne(node[0]))
       {
         Node ret = nm->mkConst(::CVC4::String(""));
         return returnRewrite(node, ret, "ss-len-one-z-z");
@@ -2155,8 +2149,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
 
       // (str.contains (str.replace x y x) z) ---> (str.contains x z)
       // if (str.len z) <= 1
-      Node one = nm->mkConst(Rational(1));
-      if (checkEntailArith(one, len_n2))
+      if (checkEntailLengthOne(node[1]))
       {
         Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
         return returnRewrite(node, ret, "ctn-repl-len-one-to-ctn");
@@ -2474,7 +2467,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
 
     // (str.replace x y x) ---> (str.replace x (str.++ y1 ... yn) x)
     // if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "")
-    if (checkEntailArith(nm->mkConst(Rational(1)), l0))
+    if (checkEntailLengthOne(node[0]))
     {
       Node empty = nm->mkConst(String(""));
       Node rn1 = Rewriter::rewrite(
@@ -2850,7 +2843,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
   //   str.replace( x ++ y ++ x ++ y, "A", z ) -->
   //   str.replace( x ++ y, "A", z ) ++ x ++ y
   // since if "A" occurs in x ++ y ++ x ++ y, then it must occur in x ++ y.
-  if (node[1].isConst() && node[1].getConst<String>().size() == 1)
+  if (checkEntailLengthOne(node[1]))
   {
     Node lastLhs;
     unsigned lastCheckIndex = 0;
@@ -3826,6 +3819,15 @@ bool TheoryStringsRewriter::checkEntailNonEmpty(Node a)
   return checkEntailArith(len, true);
 }
 
+bool TheoryStringsRewriter::checkEntailLengthOne(Node s, bool strict)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node one = nm->mkConst(Rational(1));
+  Node len = nm->mkNode(STRING_LENGTH, s);
+  len = Rewriter::rewrite(len);
+  return checkEntailArith(one, len) && (!strict || checkEntailArith(len, true));
+}
+
 bool TheoryStringsRewriter::checkEntailArithEq(Node a, Node b)
 {
   if (a == b)
@@ -4714,8 +4716,7 @@ Node TheoryStringsRewriter::getStringOrEmpty(Node n)
           break;
         }
 
-        Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0]));
-        if (strlen == nm->mkConst(Rational(1)) && n[2] == empty)
+        if (checkEntailLengthOne(n[0]) && n[2] == empty)
         {
           // (str.replace "A" x "") --> "A"
           res = n[0];
@@ -4727,8 +4728,7 @@ Node TheoryStringsRewriter::getStringOrEmpty(Node n)
       }
       case kind::STRING_SUBSTR:
       {
-        Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0]));
-        if (strlen == nm->mkConst(Rational(1)))
+        if (checkEntailLengthOne(n[0]))
         {
           // (str.substr "A" x y) --> "A"
           res = n[0];
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 3d71423ab..2e356f8f7 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -455,6 +455,19 @@ class TheoryStringsRewriter {
    * the call checkArithEntail( len( a ), true ).
    */
   static bool checkEntailNonEmpty(Node a);
+
+  /**
+   * Checks whether string has at most/exactly length one. Length one strings
+   * can be used for more aggressive rewriting because there is guaranteed that
+   * it cannot be overlap multiple components in a string concatenation.
+   *
+   * @param s The string to check
+   * @param strict If true, the string must have exactly length one, otherwise
+   * at most length one
+   * @return True if the string has at most/exactly length one, false otherwise
+   */
+  static bool checkEntailLengthOne(Node s, bool strict = false);
+
   /** check arithmetic entailment equal
    * Returns true if it is always the case that a = b.
    */
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