From 7fcf0cb48a02115ff93395b89db722d10abf5f41 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Thu, 28 Jun 2012 11:26:07 +0000 Subject: Fixed bug in bv rewriter that caused wrong answer in SMT-COMP --- .../theory_bv_rewrite_rules_constant_evaluation.h | 11 +++++- .../theory_bv_rewrite_rules_operator_elimination.h | 9 +++-- .../bv/theory_bv_rewrite_rules_simplification.h | 42 ++++++++++++++++++---- test/regress/regress0/aufbv/Makefile.am | 9 +++-- test/regress/regress0/aufbv/rewrite_bug.smt | 28 +++++++++++++++ test/regress/regress0/bv/Makefile.am | 3 +- test/regress/regress0/bv/smtcompbug.smt | 13 +++++++ 7 files changed, 99 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress0/aufbv/rewrite_bug.smt create mode 100644 test/regress/regress0/bv/smtcompbug.smt diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index 82f4779c6..8cbf99ae9 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -30,12 +30,15 @@ namespace bv { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_AND && + node.getNumChildren() == 2 && utils::isBVGroundTerm(node)); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; BitVector a = node[0].getConst(); BitVector b = node[1].getConst(); @@ -46,12 +49,15 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_OR && + node.getNumChildren() == 2 && utils::isBVGroundTerm(node)); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; BitVector a = node[0].getConst(); BitVector b = node[1].getConst(); @@ -62,12 +68,15 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_XOR && + node.getNumChildren() == 2 && utils::isBVGroundTerm(node)); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; BitVector a = node[0].getConst(); BitVector b = node[1].getConst(); @@ -101,7 +110,7 @@ template<> inline Node RewriteRule::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; BitVector a = node[0].getConst(); - BitVector res = ~ a; + BitVector res = ~ a; return utils::mkConst(res); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index d2cc7e05f..506570ed2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -221,7 +221,8 @@ Node RewriteRule::apply(TNode node) { template<> bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_NAND); + return (node.getKind() == kind::BITVECTOR_NAND && + node.getNumChildren() == 2); } template<> @@ -236,7 +237,8 @@ Node RewriteRule::apply(TNode node) { template<> bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_NOR); + return (node.getKind() == kind::BITVECTOR_NOR && + node.getNumChildren() == 2); } template<> @@ -251,7 +253,8 @@ Node RewriteRule::apply(TNode node) { template<> bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_XNOR); + return (node.getKind() == kind::BITVECTOR_XNOR && + node.getNumChildren() == 2); } template<> diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 8e14980a7..272b56ae9 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -152,13 +152,16 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); return ((node.getKind() == kind::BITVECTOR_AND || node.getKind() == kind::BITVECTOR_OR) && + node.getNumChildren() == 2 && node[0] == node[1]); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; return node[0]; } @@ -171,14 +174,17 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); unsigned size = utils::getSize(node); return (node.getKind() == kind::BITVECTOR_AND && + node.getNumChildren() == 2 && (node[0] == utils::mkConst(size, 0) || node[1] == utils::mkConst(size, 0))); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; return utils::mkConst(utils::getSize(node), 0); } @@ -191,15 +197,18 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); unsigned size = utils::getSize(node); Node ones = utils::mkOnes(size); return (node.getKind() == kind::BITVECTOR_AND && + node.getNumChildren() == 2 && (node[0] == ones || node[1] == ones)); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; unsigned size = utils::getSize(node); @@ -219,14 +228,17 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); unsigned size = utils::getSize(node); return (node.getKind() == kind::BITVECTOR_OR && + node.getNumChildren() == 2 && (node[0] == utils::mkConst(size, 0) || node[1] == utils::mkConst(size, 0))); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; unsigned size = utils::getSize(node); @@ -246,15 +258,18 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); unsigned size = utils::getSize(node); Node ones = utils::mkOnes(size); return (node.getKind() == kind::BITVECTOR_OR && + node.getNumChildren() == 2 && (node[0] == ones || node[1] == ones)); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; return utils::mkOnes(utils::getSize(node)); } @@ -268,12 +283,15 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_XOR && + node.getNumChildren() == 2 && node[0] == node[1]); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); } @@ -367,13 +385,16 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_AND && + node.getNumChildren() == 2 && ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) || (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); } @@ -386,13 +407,16 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_OR && + node.getNumChildren() == 2 && ((node[0].getKind() == kind::BITVECTOR_NOT && node[0][0] == node[1]) || (node[1].getKind() == kind::BITVECTOR_NOT && node[1][0] == node[0]))); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; uint32_t size = utils::getSize(node); Integer ones = Integer(1).multiplyByPow2(size) - 1; @@ -407,13 +431,16 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_XOR && + Unreachable(); + if (node.getKind() == kind::BITVECTOR_XOR && + node.getNumChildren() == 2 && node[0].getKind() == kind::BITVECTOR_NOT && node[1].getKind() == kind::BITVECTOR_NOT); } template<> inline Node RewriteRule::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; Node a = node[0][0]; Node b = node[1][0]; @@ -434,11 +461,14 @@ bool RewriteRule::applies(TNode node) { template<> inline Node RewriteRule::apply(TNode node) { - BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - Node a = node[0][0]; - Node b = node[0][1]; - Node nota = utils::mkNode(kind::BITVECTOR_NOT, a); - return utils::mkSortedNode(kind::BITVECTOR_XOR, nota, b); + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + std::vector children; + TNode::iterator child_it = node[0].begin(); + children.push_back(utils::mkNode(kind::BITVECTOR_NOT, *child_it)); + for(++child_it; child_it != node[0].end(); ++child_it) { + children.push_back(*child_it); + } + return utils::mkSortedNode(kind::BITVECTOR_XOR, children); } /** diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 41bb5db5b..482c06ac7 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -22,9 +22,10 @@ TESTS = \ wchains010ue.delta02.smt \ dubreva005ue.delta01.smt \ fuzz00.smt \ + fuzz01.smt \ fuzz01.delta01.smt \ fuzz02.delta01.smt \ - fuzz02.smt \ + fuzz02.smt \ fuzz03.delta01.smt \ fuzz03.smt \ fuzz04.delta01.smt \ @@ -37,11 +38,9 @@ TESTS = \ fuzz08.smt \ fuzz09.smt \ fuzz10.smt \ - fifo32bc06k08.delta01.smt + fifo32bc06k08.delta01.smt \ + rewrite_bug.smt -# failing -# fuzz01.smt \ -# EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/aufbv/rewrite_bug.smt b/test/regress/regress0/aufbv/rewrite_bug.smt new file mode 100644 index 000000000..c0906ba0d --- /dev/null +++ b/test/regress/regress0/aufbv/rewrite_bug.smt @@ -0,0 +1,28 @@ +(benchmark B_ +:logic QF_AUFBV +:extrafuns ((a Array[32:8])) +:status sat +:formula +(flet ($n1 true) +(let (?n2 bv0[8]) +(let (?n3 (sign_extend[24] ?n2)) +(let (?n4 bv1[32]) +(let (?n5 bv1[8]) +(let (?n6 (store a ?n4 ?n5)) +(let (?n7 bv0[32]) +(let (?n8 (select a ?n4)) +(let (?n9 (sign_extend[24] ?n8)) +(let (?n10 (extract[7:0] ?n9)) +(let (?n11 (store ?n6 ?n7 ?n10)) +(let (?n12 (select ?n11 ?n4)) +(let (?n13 (store ?n11 ?n4 ?n12)) +(let (?n14 (select ?n13 ?n7)) +(let (?n15 (sign_extend[24] ?n14)) +(flet ($n16 (bvslt ?n3 ?n15)) +(flet ($n17 (not $n16)) +(let (?n18 (select ?n13 ?n4)) +(let (?n19 (sign_extend[24] ?n18)) +(flet ($n20 (bvslt ?n7 ?n19)) +(flet ($n21 (and $n1 $n1 $n1 $n1 $n17 $n20)) +$n21 +)))))))))))))))))))))) diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index a21c772b1..937a886f6 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -81,7 +81,8 @@ SMT_TESTS = \ fuzz40.delta01.smt \ fuzz40.smt \ fuzz41.smt \ - calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt + calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \ + smtcompbug.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/bv/smtcompbug.smt b/test/regress/regress0/bv/smtcompbug.smt new file mode 100644 index 000000000..7efe3015c --- /dev/null +++ b/test/regress/regress0/bv/smtcompbug.smt @@ -0,0 +1,13 @@ +(benchmark B_ + :status sat + :category { unknown } + :logic QF_BV + :extrafuns ((x781 BitVec[32])) + :extrafuns ((x803 BitVec[8])) + :extrafuns ((x804 BitVec[8])) + :extrafuns ((x791 BitVec[8])) + :formula (and +(= x804 (bvxor (bvxor (extract[7:0] (bvadd bv1[32] x781)) x791) x803)) +(= (bvnot (extract[0:0] x804)) bv0[1]) +(= x781 bv0[32])) +) -- cgit v1.2.3