diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-01-04 17:30:25 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-04 15:30:25 -0800 |
commit | e1df8f68a90c7ba548b2746704b978555ec4283f (patch) | |
tree | b3bcea5160fdb6fa38252e20eea7f759a9bfae85 /src/theory/builtin | |
parent | 256d4093ab6ac3b792c6f1f11131124d1ae6b069 (diff) |
Improvements for CBQI (#1478)
Includes:
- Basic rewriting for choice functions in the builtin rewriter,
- Do not consider more than one equal term in ceg instantiator (helps cases where we have a
repeated pattern of duplicate instantiations),
- Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat
equalities suffice).
- Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index edc934d0d..b0e3aeb6f 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -94,6 +94,20 @@ RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) { Trace("builtin-rewrite-debug") << "...failed to get array representation." << std::endl; } return RewriteResponse(REWRITE_DONE, node); + } + else if (node.getKind() == kind::CHOICE) + { + if (node[1].getKind() == kind::EQUAL) + { + for (unsigned i = 0; i < 2; i++) + { + if (node[1][i] == node[0][0]) + { + return RewriteResponse(REWRITE_DONE, node[1][1 - i]); + } + } + } + return RewriteResponse(REWRITE_DONE, node); }else{ return doRewrite(node); } |