diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-21 17:43:22 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-21 17:43:22 +0000 |
commit | 7f49a7aedc16cb46216f92d00881cd3485acc206 (patch) | |
tree | 7e04162a06a37d17df29b88dcddf7934473f9376 | |
parent | 195fee60c540eec5aa880606c4962e6c25384635 (diff) |
fixing a bug in the BV rewrite, off by one error when merging constants
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_core.h | 20 | ||||
-rw-r--r-- | test/regress/regress0/bv/core/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/bv/core/a78test0002.smt | 19 |
3 files changed, 41 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 7cfb46835..dfc401616 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -33,6 +33,7 @@ bool RewriteRule<ConcatFlatten>::applies(Node node) { template<> Node RewriteRule<ConcatFlatten>::apply(Node node) { + Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl; NodeBuilder<> result(kind::BITVECTOR_CONCAT); std::vector<Node> processing_stack; processing_stack.push_back(node); @@ -57,6 +58,9 @@ bool RewriteRule<ConcatExtractMerge>::applies(Node node) { template<> Node RewriteRule<ConcatExtractMerge>::apply(Node node) { + + Debug("bv-rewrite") << "RewriteRule<ConcatExtractMerge>(" << node << ")" << std::endl; + std::vector<Node> mergedExtracts; Node current = node[0]; @@ -115,6 +119,9 @@ bool RewriteRule<ConcatConstantMerge>::applies(Node node) { template<> Node RewriteRule<ConcatConstantMerge>::apply(Node node) { + + Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ")" << std::endl; + std::vector<Node> mergedConstants; for (unsigned i = 0, end = node.getNumChildren(); i < end;) { if (node[i].getKind() != kind::CONST_BITVECTOR) { @@ -138,10 +145,12 @@ Node RewriteRule<ConcatConstantMerge>::apply(Node node) { } // Add the new merged constant mergedConstants.push_back(utils::mkConst(current)); - i = j + 1; + i = j; } } + Debug("bv-rewrite") << "RewriteRule<ConcatConstantMerge>(" << node << ") => " << utils::mkConcat(mergedConstants) << std::endl; + return utils::mkConcat(mergedConstants); } @@ -158,6 +167,7 @@ bool RewriteRule<ExtractWhole>::applies(Node node) { template<> Node RewriteRule<ExtractWhole>::apply(Node node) { + Debug("bv-rewrite") << "RewriteRule<ExtractWhole>(" << node << ")" << std::endl; return node[0]; } @@ -170,6 +180,7 @@ bool RewriteRule<ExtractConstant>::applies(Node node) { template<> Node RewriteRule<ExtractConstant>::apply(Node node) { + Debug("bv-rewrite") << "RewriteRule<ExtractConstant>(" << node << ")" << std::endl; Node child = node[0]; BitVector childValue = child.getConst<BitVector>(); return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node))); @@ -177,6 +188,7 @@ Node RewriteRule<ExtractConstant>::apply(Node node) { template<> bool RewriteRule<ExtractConcat>::applies(Node node) { + Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl; if (node.getKind() != kind::BITVECTOR_EXTRACT) return false; if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false; return true; @@ -184,6 +196,7 @@ bool RewriteRule<ExtractConcat>::applies(Node node) { template<> Node RewriteRule<ExtractConcat>::apply(Node node) { + Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl; int extract_high = utils::getExtractHigh(node); int extract_low = utils::getExtractLow(node); @@ -216,6 +229,8 @@ bool RewriteRule<ExtractExtract>::applies(Node node) { template<> Node RewriteRule<ExtractExtract>::apply(Node node) { + Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl; + // x[i:j][k:l] ~> x[k+j:l+j] Node child = node[0]; unsigned k = utils::getExtractHigh(node); @@ -228,6 +243,7 @@ Node RewriteRule<ExtractExtract>::apply(Node node) { template<> bool RewriteRule<FailEq>::applies(Node node) { + Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl; if (node.getKind() != kind::EQUAL) return false; if (node[0].getKind() != kind::CONST_BITVECTOR) return false; if (node[1].getKind() != kind::CONST_BITVECTOR) return false; @@ -247,6 +263,7 @@ bool RewriteRule<SimplifyEq>::applies(Node node) { template<> Node RewriteRule<SimplifyEq>::apply(Node node) { + Debug("bv-rewrite") << "RewriteRule<SimplifyEq>(" << node << ")" << std::endl; return utils::mkTrue(); } @@ -257,6 +274,7 @@ bool RewriteRule<ReflexivityEq>::applies(Node node) { template<> Node RewriteRule<ReflexivityEq>::apply(Node node) { + Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl; return node[1].eqNode(node[0]);; } diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 25f977f3b..9182bfbc6 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -63,8 +63,9 @@ TESTS = \ slice-18.smt \ slice-19.smt \ slice-20.smt \ - ext_con_004_001_1024.smt - + ext_con_004_001_1024.smt \ + a78test0002.smt + EXTRA_DIST = $(TESTS) # synonyms for "check" diff --git a/test/regress/regress0/bv/core/a78test0002.smt b/test/regress/regress0/bv/core/a78test0002.smt new file mode 100644 index 000000000..28f6aea09 --- /dev/null +++ b/test/regress/regress0/bv/core/a78test0002.smt @@ -0,0 +1,19 @@ +(benchmark a78test0002.smt + :source { +Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh +(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using +CVC3. + +} + :status sat + :difficulty { 0 } + :category { industrial } + :logic QF_BV + :extrafuns ((r1 BitVec[16])) + :assumption +(not (= r1 bv0[16])) + :assumption +(not (not (= (concat bv0[16] r1) bv65535[32]))) + :formula +(not false) +) |