From b58e0b24b1f5e319ceb468e9009b727df481af7c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Jun 2020 23:48:08 -0500 Subject: [PATCH] (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. --- .../builtin/theory_builtin_rewriter.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) 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); -- 2.30.2