Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)

Fixes #4620.

The extended rewrite (and A B) ---> (and A (B * { A -> true } ) triggers an unsoundness when B contains witness terms. More generally, contextual substitution into witness terms is unsound since the skolemization of witness terms is added globally whereas the substitution corresponds to a fact that holds locally. This means that A -> true above may be added as a global constraint indirectly through witness skolemization.

A general example of this unsoundness:

(or (and (>= x 0) (P (witness ((z Int)) (=> (>= x 0) (= (* z z) x))))) F)
rewrites to
(or (and (>= x 0) (P (witness ((z Int)) (= (* z z) x)))) F)
preprocesses to
(and (or (and (>= x 0) (P k)) F) (= (* k k) x))
which now implies that (>= x 0) by the last conjunct, whereas this was not implied in the original formula
This PR limits the kinds that can be traversed when applying substitutions in the extended rewriter, including from the rewrite above. In particular, the fix ensures that the partialSubstitute method is used in the extended rewriter when applicable, which now explicitly disallows recursion on WITNESS.

Notice that this fixes contextual substitutions in the extended rewriter, but does not fix the more general issue. In particular, we still should be careful to check if contextual substitutions are applied by any other preprocessing passes.

5 files changed, 60 insertions, 40 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 125559218..c1a0b8ee9 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -488,6 +488,9 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
     {
       // reverse substitution to opposite child
       // r{ x -> t } = s  implies  ite( x=t ^ C, s, r ) ---> r
+      // We can use ordinary substitute since the result of the substitution
+      // is not being returned. In other words, nn is only being used to query
+      // whether the second branch is a generalization of the first.
       Node nn =
           t2.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
       if (nn != t2)
@@ -501,7 +504,9 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
       }
 
       // ite( x=t ^ C, s, r ) ---> ite( x=t ^ C, s{ x -> t }, r )
-      nn = t1.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+      // must use partial substitute here, to avoid substitution into witness
+      std::map<Kind, bool> rkinds;
+      nn = partialSubstitute(t1, vars, subs, rkinds);
       if (nn != t1)
       {
         // If full=false, then we've duplicated a term u in the children of n.
@@ -524,9 +529,11 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
     if (new_ret.isNull())
     {
       // ite( C, t, s ) ----> ite( C, t, s { C -> false } )
-      TNode tv = n[0];
-      TNode ts = d_false;
-      Node nn = t2.substitute(tv, ts);
+      // use partial substitute to avoid substitution into witness
+      std::map<Node, Node> assign;
+      assign[n[0]] = d_false;
+      std::map<Kind, bool> rkinds;
+      Node nn = partialSubstitute(t2, assign, rkinds);
       if (nn != t2)
       {
         nn = Rewriter::rewrite(nn);
@@ -561,7 +568,8 @@ Node ExtendedRewriter::extendedRewriteAndOr(Node n)
     return Node::null();
   }
   Node new_ret;
-  // all kinds are legal to substitute over : hence we give the empty map
+  // we allow substitutions to recurse over any kind, except WITNESS which is
+  // managed by partialSubstitute.
   std::map<Kind, bool> bcp_kinds;
   new_ret = extendedRewriteBcp(AND, OR, NOT, bcp_kinds, n);
   if (!new_ret.isNull())
@@ -858,20 +866,10 @@ Node ExtendedRewriter::extendedRewriteBcp(
       std::vector<Node> ccs_children;
       for (const Node& cc : ca)
       {
-        Node ccs = cc;
-        if (bcp_kinds.empty())
-        {
-          Trace("ext-rew-bcp-debug") << "...do ordinary substitute"
-                                     << std::endl;
-          ccs = cc.substitute(
-              avars.begin(), avars.end(), asubs.begin(), asubs.end());
-        }
-        else
-        {
-          Trace("ext-rew-bcp-debug") << "...do partial substitute" << std::endl;
-          // substitution is only applicable to compatible kinds
-          ccs = partialSubstitute(ccs, assign, bcp_kinds);
-        }
+        // always use partial substitute, to avoid substitution in witness
+        Trace("ext-rew-bcp-debug") << "...do partial substitute" << std::endl;
+        // substitution is only applicable to compatible kinds in bcp_kinds
+        Node ccs = partialSubstitute(cc, assign, bcp_kinds);
         childChanged = childChanged || ccs != cc;
         ccs_children.push_back(ccs);
       }
@@ -1071,19 +1069,10 @@ Node ExtendedRewriter::extendedRewriteEqRes(Kind andk,
             Node ccs = n[j];
             if (i != j)
             {
-              if (bcp_kinds.empty())
-              {
-                ccs = ccs.substitute(
-                    vars.begin(), vars.end(), subs.begin(), subs.end());
-              }
-              else
-              {
-                std::map<Node, Node> assign;
-                // vars.size()==subs.size()==1
-                assign[vars[0]] = subs[0];
-                // substitution is only applicable to compatible kinds
-                ccs = partialSubstitute(ccs, assign, bcp_kinds);
-              }
+              // Substitution is only applicable to compatible kinds. We always
+              // use the partialSubstitute method to avoid substitution into
+              // witness terms.
+              ccs = partialSubstitute(ccs, vars, subs, bcp_kinds);
               childrenChanged = childrenChanged || n[j] != ccs;
             }
             children.push_back(ccs);
@@ -1538,11 +1527,12 @@ Node ExtendedRewriter::extendedRewriteEqChain(
 }
 
 Node ExtendedRewriter::partialSubstitute(Node n,
-                                         std::map<Node, Node>& assign,
-                                         std::map<Kind, bool>& rkinds)
+                                         const std::map<Node, Node>& assign,
+                                         const std::map<Kind, bool>& rkinds)
 {
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::map<Node, Node>::const_iterator ita;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
@@ -1554,16 +1544,19 @@ Node ExtendedRewriter::partialSubstitute(Node n,
 
     if (it == visited.end())
     {
-      std::map<Node, Node>::iterator ita = assign.find(cur);
+      ita = assign.find(cur);
       if (ita != assign.end())
       {
         visited[cur] = ita->second;
       }
       else
       {
-        // can only recurse on these kinds
+        // If rkinds is non-empty, then can only recurse on its kinds.
+        // We also always disallow substitution into witness. Notice that
+        // we disallow witness here, due to unsoundness when applying contextual
+        // substitutions over witness terms (see #4620).
         Kind k = cur.getKind();
-        if (rkinds.find(k) != rkinds.end())
+        if (k != WITNESS && (rkinds.empty() || rkinds.find(k) != rkinds.end()))
         {
           visited[cur] = Node::null();
           visit.push_back(cur);
@@ -1607,6 +1600,20 @@ Node ExtendedRewriter::partialSubstitute(Node n,
   return visited[n];
 }
 
+Node ExtendedRewriter::partialSubstitute(Node n,
+                                         const std::vector<Node>& vars,
+                                         const std::vector<Node>& subs,
+                                         const std::map<Kind, bool>& rkinds)
+{
+  Assert(vars.size() == subs.size());
+  std::map<Node, Node> assign;
+  for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
+  {
+    assign[vars[i]] = subs[i];
+  }
+  return partialSubstitute(n, assign, rkinds);
+}
+
 Node ExtendedRewriter::solveEquality(Node n)
 {
   // TODO (#1706) : implement
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 63cc017dc..5ed6ee3f3 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -200,11 +200,17 @@ class ExtendedRewriter
   /** Partial substitute
    *
    * Applies the substitution specified by assign to n, recursing only beneath
-   * terms whose Kind appears in rec_kinds.
+   * terms whose Kind appears in rkinds (when rkinds is empty), and additionally
+   * never recursing beneath WITNESS.
    */
   Node partialSubstitute(Node n,
-                         std::map<Node, Node>& assign,
-                         std::map<Kind, bool>& rkinds);
+                         const std::map<Node, Node>& assign,
+                         const std::map<Kind, bool>& rkinds);
+  /** same as above, with vectors */
+  Node partialSubstitute(Node n,
+                         const std::vector<Node>& vars,
+                         const std::vector<Node>& subs,
+                         const std::map<Kind, bool>& rkinds);
   /** solve equality
    *
    * If this function returns a non-null node n', then n' is equivalent to n
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 93d6a3ef8..cdac5fc6c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1549,6 +1549,7 @@ set(regress_1_tests
   regress1/quantifiers/issue4062-cegqi-aux.smt2
   regress1/quantifiers/issue4243-prereg-inc.smt2
   regress1/quantifiers/issue4290-cegqi-r.smt2
+  regress1/quantifiers/issue4620-erq-witness-unsound.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2
diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2
index 3fb3a9e53..726487e18 100644
--- a/test/regress/regress0/fp/ext-rew-test.smt2
+++ b/test/regress/regress0/fp/ext-rew-test.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: symfpu
 ; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
 ; EXPECT: unsat
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2 b/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2
new file mode 100644
index 000000000..ee7cafd63
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --ext-rewrite-quant
+; EXPECT: sat
+(set-logic NIA)
+(assert (exists ((x Int)) (= (div 1 x x) x)))
+(check-sat)