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/smt | |
| parent | 2cf12a56cb9c5eb539d50a39b2764a292d6fd13f (diff) | |
fixed failed bv regressions by refactoring out some rewrite rules from smt_engine.cpp
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 3 insertions, 7 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; } |