Do not invoke rewriter on terms involving abstract sorts in DSL proof…

… reconstruction (cvc5#10517)

This adopts the policy that terms involving abstract sorts should not be passed to the rewriter. We consider terms with any abstract subterms to rewrite to themselves in the DSL proof reconstruction algorithm.

Pros:

This makes it so that we do not need to make the rewriter robust to rewriting with abstract subterms. This is particularly important for BV which assumes that all children of BV operators have concrete bitwidth. This change makes it so that the BV rewriter does not require further changes from proof-new. The same applies to the FP rewriter.
Cons:

The DSL reconstruction algorithm is not able to invoke the rewriter as an oracle in some contexts. This means that certain optimizations are not applicable, especially when doing proof reconstruction for BV.
In my alf development branch, this limitation leads to only a difference of 2 unproven BV rewrites on our regressions (99 -> 101).

This also includes a minor change from proof-new to ensure terms are properly converted upon entry to the DSL rewrite reconstruction algorithm.

This fixes make regress-dsl-proof and should fix the nightly failures.

src/rewriter/rewrite_db_proof_cons.cpp

@@ -340,7 +340,7 @@ bool RewriteDbProofCons::proveWithRule(DslProofRule id,
     {
       return false;
     }
-    Node r = rewrite(target[0]);
+    Node r = rewriteConcrete(target[0]);
     if (r != r2)
     {
       return false;
@@ -351,7 +351,7 @@ bool RewriteDbProofCons::proveWithRule(DslProofRule id,
     std::vector<Node> rchildren;
     for (size_t i = 0; i < nchild; i++)
     {
-      Node rr = rewrite(target[0][i]);
+      Node rr = rewriteConcrete(target[0][i]);
       if (!rr.isConst())
       {
         return false;
@@ -449,7 +449,8 @@ bool RewriteDbProofCons::proveWithRule(DslProofRule id,
       // The conclusion term may actually change type. Note that we must rewrite
       // the terms, since they may involve operators with abstract type that
       // evaluate to terms with concrete types.
-      if (!rewrite(stgt).getType().isComparableTo(rewrite(target[1]).getType()))
+      if (!rewriteConcrete(stgt).getType().isComparableTo(
+              rewriteConcrete(target[1]).getType()))
       {
         Trace("rpc-debug2") << "...fail (types)" << std::endl;
         return false;
@@ -630,7 +631,7 @@ bool RewriteDbProofCons::proveInternalBase(const Node& eqi, DslProofRule& idb)
         Trace("rpc-debug2") << "...fail, ill-typed equality" << std::endl;
         return true;
       }
-      Node eqr = rewrite(eq);
+      Node eqr = rewriteConcrete(eq);
       if (eqr.isConst())
       {
         // definitely not true
@@ -1059,5 +1060,14 @@ void RewriteDbProofCons::cacheProofSubPlaceholder(TNode context,
   }
 }
 
+Node RewriteDbProofCons::rewriteConcrete(const Node& n)
+{
+  if (expr::hasAbstractSubterm(n))
+  {
+    return n;
+  }
+  return rewrite(n);
+}
+
 }  // namespace rewriter
 }  // namespace cvc5::internal

src/rewriter/rewrite_db_proof_cons.h

@@ -218,7 +218,18 @@ class RewriteDbProofCons : protected EnvObj
                                 TNode placeholder,
                                 TNode source,
                                 TNode target);
-
+  /**
+   * Rewrite concrete, which returns the result of rewriting n if it contains
+   * no abstract subterms, or n itself otherwise.
+   *
+   * This method is required since the algorithm in this class often invokes
+   * the rewriter as an oracle. We operate on terms with abstract subterms
+   * in this class, and these terms should not be passed to the rewriter,
+   * since the rewriter does not properly handle abstract subterms (for
+   * instance, the BV theory rewriter assumes that all children of BV operators
+   * have concrete bitwidths).
+   */
+  Node rewriteConcrete(const Node& n);
   /** Notify class for matches */
   RdpcMatchTrieNotify d_notify;
   /**

src/rewriter/rewrite_db_term_process.cpp

@@ -46,9 +46,23 @@ Node RewriteDbNodeConverter::postConvert(Node n)
     }
     return nm->mkNode(Kind::STRING_CONCAT, children);
   }
+  else if (k == Kind::FORALL)
+  {
+    // ignore annotation
+    if (n.getNumChildren() == 3)
+    {
+      NodeManager* nm = NodeManager::currentNM();
+      return nm->mkNode(Kind::FORALL, n[0], n[1]);
+    }
+  }
 
   return n;
 }
 
+bool RewriteDbNodeConverter::shouldTraverse(Node n)
+{
+  return n.getKind() != Kind::INST_PATTERN_LIST;
+}
+
 }  // namespace rewriter
 }  // namespace cvc5::internal

src/rewriter/rewrite_db_term_process.h

@@ -50,6 +50,10 @@ class RewriteDbNodeConverter : public NodeConverter
    * for the DSL proof reconstruction algorithm.
    */
   Node postConvert(Node n) override;
+
+ protected:
+  /** Should we traverse n? */
+  bool shouldTraverse(Node n) override;
 };
 
 }  // namespace rewriter