diff options
Diffstat (limited to 'src/theory/bv/theory_bv.cpp')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 58 |
1 files changed, 0 insertions, 58 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 69ff48721..c9e7c397e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -19,7 +19,6 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/theory_engine.h" @@ -41,63 +40,6 @@ void TheoryBV::preRegisterTerm(TNode node) { } } -RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) { - - Debug("bitvector") << "TheoryBV::postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ")" << std::endl; - - Node result; - - if (node.getKind() == kind::CONST_BITVECTOR /* || isLeaf(n)) */) - result = node; - else { - switch (node.getKind()) { - case kind::BITVECTOR_CONCAT: - result = LinearRewriteStrategy< - // Flatten the top level concatenations - CoreRewriteRules::ConcatFlatten, - // Merge the adjacent extracts on non-constants - CoreRewriteRules::ConcatExtractMerge, - // Merge the adjacent extracts on constants - CoreRewriteRules::ConcatConstantMerge, - // At this point only Extract-Whole could apply, if the result is only one extract - // or at some sub-expression if the result is a concatenation. - ApplyRuleToChildren<kind::BITVECTOR_CONCAT, CoreRewriteRules::ExtractWhole> - >::apply(node); - break; - case kind::BITVECTOR_EXTRACT: - result = LinearRewriteStrategy< - // Extract over a constant gives a constant - CoreRewriteRules::ExtractConstant, - // Extract over an extract is simplified to one extract - CoreRewriteRules::ExtractExtract, - // Extract over a concatenation is distributed to the appropriate concatenations - CoreRewriteRules::ExtractConcat, - // At this point only Extract-Whole could apply - CoreRewriteRules::ExtractWhole - >::apply(node); - break; - case kind::EQUAL: - result = LinearRewriteStrategy< - // Two distinct values rewrite to false - CoreRewriteRules::FailEq, - // If both sides are equal equality is true - CoreRewriteRules::SimplifyEq - >::apply(node); - break; - default: - // TODO: figure out when this is an operator - result = node; - break; - // Unhandled(); - } - } - - Debug("bitvector") << "TheoryBV::postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ") => " << result << std::endl; - - return RewriteComplete(result); -} - - void TheoryBV::check(Effort e) { Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; |