(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 7a4b2db6fa3cff6d08f1aec18a8899afc9c3ea36..47986c9663d18dffafe901396b162e31ec17ae1e 100644 (file)
--- 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);