Do not traverse WITNESS for partial substitutions in extended rewrite…

…r (#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.

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

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

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

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)

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)