From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 1 Jul 2020 04:48:08 +0000 (-0500)
Subject: (proof-new) Improve rewriter for WITNESS (#4661)
X-Git-Tag: cvc5-1.0.0~3158
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b58e0b24b1f5e319ceb468e9009b727df481af7c;p=cvc5.git

(proof-new) Improve rewriter for WITNESS (#4661)

Proof checking failures revealed that we are not rewriting witness for Boolean variables (witness ((x Bool)) x) ---> true and (witness ((x Bool)) (not x)) ---> false.

Also adds 2 assertions that are required for elimination (witness ((x T)) (= x t)) ---> t. These assertions should always hold due to the witness terms we construct.
---

diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 7a4b2db6f..47986c966 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -98,12 +98,31 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
     {
       for (unsigned i = 0; i < 2; i++)
       {
+        // (witness ((x T)) (= x t)) ---> t
         if (node[1][i] == node[0][0])
         {
+          Trace("builtin-rewrite") << "Witness rewrite: " << node << " --> "
+                                   << node[1][1 - i] << std::endl;
+          // based on the witness terms we construct, this should be a legal
+          // elimination, since t should not contain x and be a subtype of x.
+          Assert(!expr::hasSubterm(node[1][1 - i], node[0][0]));
+          Assert(node[1][i].getType().isSubtypeOf(node[0][0].getType()));
           return RewriteResponse(REWRITE_DONE, node[1][1 - i]);
         }
       }
     }
+    else if (node[1] == node[0][0])
+    {
+      // (witness ((x Bool)) x) ---> true
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(true));
+    }
+    else if (node[1].getKind() == kind::NOT && node[1][0] == node[0][0])
+    {
+      // (witness ((x Bool)) (not x)) ---> false
+      return RewriteResponse(REWRITE_DONE,
+                             NodeManager::currentNM()->mkConst(false));
+    }
     return RewriteResponse(REWRITE_DONE, node);
   }else{ 
     return doRewrite(node);