diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 12 |
2 files changed, 18 insertions, 2 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 1335f8f4a..23018605f 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -594,6 +594,14 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft; } +Node TheoryBVRewriter::eliminateBVSDiv(TNode node) { + Node result = bv::LinearRewriteStrategy < + bv::RewriteRule<bv::SremEliminate>, + bv::RewriteRule<bv::SdivEliminate>, + bv::RewriteRule<bv::SmodEliminate> + >::apply(node); + return result; +} diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 59a2f90f6..3e7fc272b 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -83,10 +83,18 @@ public: static RewriteResponse postRewrite(TNode node); static RewriteResponse preRewrite(TNode node); - + static void init(); static void shutdown(); - + /** + * Temporary hack for devision-by-zero until we refactor theory code from + * smt engine. + * + * @param node + * + * @return + */ + static Node eliminateBVSDiv(TNode node); };/* class TheoryBVRewriter */ }/* CVC4::theory::bv namespace */ |