diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-30 20:33:40 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-05-30 20:33:40 +0000 |
commit | 03305bfae27642ed714eab144cf977d1943bb88d (patch) | |
tree | 42e24296848e69a7c6d2f5dd3eed53b518dc1954 /src/theory | |
parent | 81b78827f65b42f22f16874bbf0c8269ed0734fc (diff) |
Added BitwiseEq bitvector rewrite
Added option "--repeat-simp" which repeats nonclausal simplification: 4 times,
twice before ite removal and twice after
Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant
speedup on dwp examples
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 567f9dc46..d6de6edbd 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -516,17 +516,20 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule<FailEq>, RewriteRule<SimplifyEq>, - RewriteRule<ReflexivityEq> + RewriteRule<ReflexivityEq>, + RewriteRule<BitwiseEq> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); } - + else if(RewriteRule<BitwiseEq>::applies(node)) { + Node resultNode = RewriteRule<BitwiseEq>::run<false>(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } else { Node resultNode = LinearRewriteStrategy < RewriteRule<FailEq>, RewriteRule<SimplifyEq>, RewriteRule<ReflexivityEq>, - // ,RewriteRule<BitwiseEq>, RewriteRule<SolveEq> >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); |