diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-30 23:48:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-30 23:48:08 -0500 |
commit | b58e0b24b1f5e319ceb468e9009b727df481af7c (patch) | |
tree | 5b98baebdef6758817c6c8a81a1a2c66e790ee1e /src | |
parent | ffed5a43764641d4808aa77bb0e393623fd4442d (diff) |
(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.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 19 |
1 files changed, 19 insertions, 0 deletions
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); |