diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-28 11:26:07 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-28 11:26:07 +0000 |
commit | 7fcf0cb48a02115ff93395b89db722d10abf5f41 (patch) | |
tree | c087609c08ac23331122470afc037a6da463b7c5 /src/theory | |
parent | 2f282e67ed10bd58c24cdc14ec53857b79e59a35 (diff) |
Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2
Diffstat (limited to 'src/theory')
3 files changed, 52 insertions, 10 deletions
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<EvalAnd>::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_AND && + node.getNumChildren() == 2 && utils::isBVGroundTerm(node)); } template<> inline Node RewriteRule<EvalAnd>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<EvalAnd>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); BitVector b = node[1].getConst<BitVector>(); @@ -46,12 +49,15 @@ Node RewriteRule<EvalAnd>::apply(TNode node) { template<> inline bool RewriteRule<EvalOr>::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_OR && + node.getNumChildren() == 2 && utils::isBVGroundTerm(node)); } template<> inline Node RewriteRule<EvalOr>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<EvalOr>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); BitVector b = node[1].getConst<BitVector>(); @@ -62,12 +68,15 @@ Node RewriteRule<EvalOr>::apply(TNode node) { template<> inline bool RewriteRule<EvalXor>::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_XOR && + node.getNumChildren() == 2 && utils::isBVGroundTerm(node)); } template<> inline Node RewriteRule<EvalXor>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<EvalXor>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); BitVector b = node[1].getConst<BitVector>(); @@ -101,7 +110,7 @@ template<> inline Node RewriteRule<EvalNot>::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule<EvalNot>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); - 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<RotateRightEliminate>::apply(TNode node) { template<> bool RewriteRule<NandEliminate>::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<NandEliminate>::apply(TNode node) { template<> bool RewriteRule<NorEliminate>::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<NorEliminate>::apply(TNode node) { template<> bool RewriteRule<XnorEliminate>::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<AshrByConst>::apply(TNode node) { template<> inline bool RewriteRule<BitwiseIdemp>::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<BitwiseIdemp>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<BitwiseIdemp>(" << node << ")" << std::endl; return node[0]; } @@ -171,14 +174,17 @@ Node RewriteRule<BitwiseIdemp>::apply(TNode node) { template<> inline bool RewriteRule<AndZero>::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<AndZero>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<AndZero>(" << node << ")" << std::endl; return utils::mkConst(utils::getSize(node), 0); } @@ -191,15 +197,18 @@ Node RewriteRule<AndZero>::apply(TNode node) { template<> inline bool RewriteRule<AndOne>::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<AndOne>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<AndOne>(" << node << ")" << std::endl; unsigned size = utils::getSize(node); @@ -219,14 +228,17 @@ Node RewriteRule<AndOne>::apply(TNode node) { template<> inline bool RewriteRule<OrZero>::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<OrZero>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<OrZero>(" << node << ")" << std::endl; unsigned size = utils::getSize(node); @@ -246,15 +258,18 @@ Node RewriteRule<OrZero>::apply(TNode node) { template<> inline bool RewriteRule<OrOne>::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<OrOne>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<OrOne>(" << node << ")" << std::endl; return utils::mkOnes(utils::getSize(node)); } @@ -268,12 +283,15 @@ Node RewriteRule<OrOne>::apply(TNode node) { template<> inline bool RewriteRule<XorDuplicate>::applies(TNode node) { + Unreachable(); return (node.getKind() == kind::BITVECTOR_XOR && + node.getNumChildren() == 2 && node[0] == node[1]); } template<> inline Node RewriteRule<XorDuplicate>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<XorDuplicate>(" << node << ")" << std::endl; return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); } @@ -367,13 +385,16 @@ Node RewriteRule<XorZero>::apply(TNode node) { template<> inline bool RewriteRule<BitwiseNotAnd>::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<BitwiseNotAnd>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<BitwiseNegAnd>(" << node << ")" << std::endl; return utils::mkConst(BitVector(utils::getSize(node), Integer(0))); } @@ -386,13 +407,16 @@ Node RewriteRule<BitwiseNotAnd>::apply(TNode node) { template<> inline bool RewriteRule<BitwiseNotOr>::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<BitwiseNotOr>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<BitwiseNotOr>(" << node << ")" << std::endl; uint32_t size = utils::getSize(node); Integer ones = Integer(1).multiplyByPow2(size) - 1; @@ -407,13 +431,16 @@ Node RewriteRule<BitwiseNotOr>::apply(TNode node) { template<> inline bool RewriteRule<XorNot>::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<XorNot>::apply(TNode node) { + Unreachable(); BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << node << ")" << std::endl; Node a = node[0][0]; Node b = node[1][0]; @@ -434,11 +461,14 @@ bool RewriteRule<NotXor>::applies(TNode node) { template<> inline Node RewriteRule<NotXor>::apply(TNode node) { - BVDebug("bv-rewrite") << "RewriteRule<XorNot>(" << 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<NotXor>(" << node << ")" << std::endl; + std::vector<Node> 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); } /** |