diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-11-13 20:38:40 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-11-13 20:38:40 +0000 |
commit | 740df5937639738a0238312dfb061643e62ba605 (patch) | |
tree | 5ef76fbe6d2365ed5e67a7d24fd877abce741b85 /src | |
parent | 2cf12a56cb9c5eb539d50a39b2764a292d6fd13f (diff) |
fixed failed bv regressions by refactoring out some rewrite rules from smt_engine.cpp
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 12 |
3 files changed, 21 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1fc32917e..32557e7c8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -41,7 +41,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/theory_engine.h" -#include "theory/bv/theory_bv_rewrite_rules.h" +#include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" #include "util/proof.h" #include "util/boolean_simplification.h" @@ -1195,16 +1195,12 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF Node node = n; NodeManager* nm = d_smt.d_nodeManager; - + // FIXME: this theory specific code should be factored out of the SmtEngine, somehow switch(k) { case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: case kind::BITVECTOR_SMOD: { - node = bv::LinearRewriteStrategy < - bv::RewriteRule<bv::SremEliminate>, - bv::RewriteRule<bv::SdivEliminate>, - bv::RewriteRule<bv::SmodEliminate> - >::apply(node); + node = bv::TheoryBVRewriter::eliminateBVSDiv(node); break; } 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 */ |