From 9b4696559cd2c74afb825d793614eb4cd6ee817e Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 13 Jun 2012 02:49:35 +0000 Subject: Fixes lots of problems in bv rewrite rules and adds lots of assertions to catch any that I may have missed --- src/theory/bv/theory_bv.h | 2 +- src/theory/bv/theory_bv_rewrite_rules.h | 15 -- .../theory_bv_rewrite_rules_constant_evaluation.h | 18 +- .../bv/theory_bv_rewrite_rules_normalization.h | 271 ++++++++++++--------- .../bv/theory_bv_rewrite_rules_simplification.h | 74 +----- src/theory/bv/theory_bv_rewriter.h | 2 +- src/theory/bv/theory_bv_utils.h | 10 +- 7 files changed, 170 insertions(+), 222 deletions(-) (limited to 'src/theory/bv') diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 247d66d89..761c11e3d 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -65,7 +65,7 @@ public: std::string identify() const { return std::string("TheoryBV"); } PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - Node ppRewrite(TNode atom); + Node ppRewrite(TNode t); private: diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 620d33aea..2fd409313 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -118,12 +118,7 @@ enum RewriteRuleId { UleMax, NotUlt, NotUle, - MultOne, - MultZero, MultPow2, - PlusZero, - PlusSelf, - PlusNegSelf, NegIdemp, UdivPow2, UdivOne, @@ -242,12 +237,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case OrOne : out << "OrOne"; return out; case XorOne : out << "XorOne"; return out; case XorZero : out << "XorZero"; return out; - case MultOne : out << "MultOne"; return out; - case MultZero : out << "MultZero"; return out; case MultPow2 : out << "MultPow2"; return out; - case PlusZero : out << "PlusZero"; return out; - case PlusSelf : out << "PlusSelf"; return out; - case PlusNegSelf : out << "PlusNegSelf"; return out; case NegIdemp : out << "NegIdemp"; return out; case UdivPow2 : out << "UdivPow2"; return out; case UdivOne : out << "UdivOne"; return out; @@ -465,12 +455,7 @@ struct AllRewriteRules { RewriteRule rule82; RewriteRule rule83; RewriteRule rule84; - RewriteRule rule85; - RewriteRule rule86; RewriteRule rule87; - RewriteRule rule88; - RewriteRule rule89; - RewriteRule rule90; RewriteRule rule91; RewriteRule rule92; RewriteRule rule93; 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 c695d20ab..82f4779c6 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -135,10 +135,11 @@ bool RewriteRule::applies(TNode node) { template<> inline Node RewriteRule::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - BitVector a = node[0].getConst(); - BitVector b = node[1].getConst(); - BitVector res = a * b; - + TNode::iterator child_it = node.begin(); + BitVector res = (*child_it).getConst(); + for(++child_it; child_it != node.end(); ++child_it) { + res = res * (*child_it).getConst(); + } return utils::mkConst(res); } @@ -151,10 +152,11 @@ bool RewriteRule::applies(TNode node) { template<> inline Node RewriteRule::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - BitVector a = node[0].getConst(); - BitVector b = node[1].getConst(); - BitVector res = a + b; - + TNode::iterator child_it = node.begin(); + BitVector res = (*child_it).getConst(); + for(++child_it; child_it != node.end(); ++child_it) { + res = res + (*child_it).getConst(); + } return utils::mkConst(res); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 6ac9da7cb..f8399041d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -127,7 +127,7 @@ Node RewriteRule::apply(TNode node) { children.push_back(utils::mkExtract(node[0][i], high, 0)); } Kind kind = node[0].getKind(); - Node op_children = utils::mkSortedNode(kind, children); + Node op_children = utils::mkNode(kind, children); return utils::mkExtract(op_children, high, low); } @@ -163,7 +163,13 @@ Node RewriteRule::apply(TNode node) { children.push_back(current); } } - return utils::mkSortedNode(kind, children); + if (node.getKind() == kind::BITVECTOR_PLUS || + node.getKind() == kind::BITVECTOR_MULT) { + return utils::mkNode(kind, children); + } + else { + return utils::mkSortedNode(kind, children); + } } static inline void addToCoefMap(std::map& map, @@ -179,49 +185,65 @@ static inline void addToCoefMap(std::map& map, static inline void updateCoefMap(TNode current, unsigned size, std::map& factorToCoefficient, BitVector& constSum) { - // look for c * x, where c is a constant - if (current.getKind() == kind::BITVECTOR_MULT && - (current[0].getKind() == kind::CONST_BITVECTOR || - current[1].getKind() == kind::CONST_BITVECTOR)) { - // if we are multiplying by a constant - BitVector coeff; - TNode term; - // figure out which part is the constant - if (current[0].getKind() == kind::CONST_BITVECTOR) { - coeff = current[0].getConst(); - term = current[1]; - } else { - coeff = current[1].getConst(); - term = current[0]; - } - if(term.getKind() == kind::BITVECTOR_SUB) { - TNode a = term[0]; - TNode b = term[1]; - addToCoefMap(factorToCoefficient, a, coeff); - addToCoefMap(factorToCoefficient, b, -coeff); - } - else if(term.getKind() == kind::BITVECTOR_NEG) { - addToCoefMap(factorToCoefficient, term[0], -BitVector(size, coeff)); + switch (current.getKind()) { + case kind::BITVECTOR_MULT: { + // look for c * term, where c is a constant + BitVector coeff; + Node term; + if (current.getNumChildren() == 2) { + // Mult should be normalized with only one constant at end + Assert(!current[0].isConst()); + if (current[1].isConst()) { + coeff = current[1].getConst(); + term = current[0]; + } + } + else if (current[current.getNumChildren()-1].isConst()) { + NodeBuilder<> nb(kind::BITVECTOR_MULT); + TNode::iterator child_it = current.begin(); + for(; (child_it+1) != current.end(); ++child_it) { + Assert(!(*child_it).isConst()); + nb << (*child_it); + } + term = nb; + coeff = (*child_it).getConst(); + } + if (term.isNull()) { + coeff = BitVector(size, (unsigned)1); + term = current; + } + if(term.getKind() == kind::BITVECTOR_SUB) { + TNode a = term[0]; + TNode b = term[1]; + addToCoefMap(factorToCoefficient, a, coeff); + addToCoefMap(factorToCoefficient, b, -coeff); + } + else if(term.getKind() == kind::BITVECTOR_NEG) { + addToCoefMap(factorToCoefficient, term[0], -BitVector(size, coeff)); + } + else { + addToCoefMap(factorToCoefficient, term, coeff); + } + break; } - else { - addToCoefMap(factorToCoefficient, term, coeff); + case kind::BITVECTOR_SUB: + // turn into a + (-1)*b + Assert(current.getNumChildren() == 2); + addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1)); + addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1)); + break; + case kind::BITVECTOR_NEG: + addToCoefMap(factorToCoefficient, current[0], -BitVector(size, (unsigned)1)); + break; + case kind::CONST_BITVECTOR: { + BitVector constValue = current.getConst(); + constSum = constSum + constValue; + break; } - } - else if (current.getKind() == kind::BITVECTOR_SUB) { - // turn into a + (-1)*b - addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1)); - addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1)); - } - else if (current.getKind() == kind::BITVECTOR_NEG) { - addToCoefMap(factorToCoefficient, current[0], -BitVector(size, (unsigned)1)); - } - else if (current.getKind() == kind::CONST_BITVECTOR) { - BitVector constValue = current.getConst(); - constSum = constSum + constValue; - } - else { - // store as 1 * current - addToCoefMap(factorToCoefficient, current, BitVector(size, (unsigned)1)); + default: + // store as 1 * current + addToCoefMap(factorToCoefficient, current, BitVector(size, (unsigned)1)); + break; } } @@ -237,9 +259,18 @@ static inline void addToChildren(TNode term, unsigned size, BitVector coeff, std // avoid introducing an extra multiplication children.push_back(utils::mkNode(kind::BITVECTOR_NEG, term)); } + else if (term.getKind() == kind::BITVECTOR_MULT) { + NodeBuilder<> nb(kind::BITVECTOR_MULT); + TNode::iterator child_it = term.begin(); + for(; child_it != term.end(); ++child_it) { + nb << *child_it; + } + nb << utils::mkConst(coeff); + children.push_back(Node(nb)); + } else { Node coeffNode = utils::mkConst(coeff); - Node product = utils::mkSortedNode(kind::BITVECTOR_MULT, coeffNode, term); + Node product = utils::mkNode(kind::BITVECTOR_MULT, term, coeffNode); children.push_back(product); } } @@ -265,9 +296,6 @@ Node RewriteRule::apply(TNode node) { } std::vector children; - if ( constSum!= BitVector(size, (unsigned)0)) { - children.push_back(utils::mkConst(constSum)); - } // construct result std::map::const_iterator it = factorToCoefficient.begin(); @@ -276,17 +304,36 @@ Node RewriteRule::apply(TNode node) { addToChildren(it->first, size, it->second, children); } + if (constSum != BitVector(size, (unsigned)0)) { + children.push_back(utils::mkConst(constSum)); + } + if(children.size() == 0) { return utils::mkConst(size, (unsigned)0); } - - return utils::mkSortedNode(kind::BITVECTOR_PLUS, children); + + return utils::mkNode(kind::BITVECTOR_PLUS, children); } template<> inline bool RewriteRule::applies(TNode node) { - return (node.getKind() == kind::BITVECTOR_MULT); + if (node.getKind() != kind::BITVECTOR_MULT) { + return false; + } + TNode::iterator child_it = node.begin(); + TNode::iterator child_next = child_it + 1; + for(; child_next != node.end(); ++child_it, ++child_next) { + if ((*child_it).isConst() || + !((*child_it) < (*child_next))) { + return true; + } + } + if ((*child_it).isConst() && + (*child_it).getConst() == BitVector(utils::getSize(node), (unsigned) 0)) { + return true; + } + return false; } template<> inline @@ -309,33 +356,30 @@ Node RewriteRule::apply(TNode node) { } } + std::sort(children.begin(), children.end()); if(constant != BitVector(size, (unsigned)1)) { children.push_back(utils::mkConst(constant)); } - if(children.size() == 0) { return utils::mkConst(size, (unsigned)1); } - return utils::mkSortedNode(kind::BITVECTOR_MULT, children); + return utils::mkNode(kind::BITVECTOR_MULT, children); } template<> inline bool RewriteRule::applies(TNode node) { - if (node.getKind() != kind::BITVECTOR_MULT) + if (node.getKind() != kind::BITVECTOR_MULT || + node.getNumChildren() != 2) { return false; - - TNode factor; - if (node[0].getKind() == kind::CONST_BITVECTOR) { - factor = node[1]; - } else if (node[1].getKind() == kind::CONST_BITVECTOR) { - factor = node[0]; - } else { - return false; } - + Assert(!node[0].isConst()); + if (!node[1].isConst()) { + return false; + } + TNode factor = node[0]; return (factor.getKind() == kind::BITVECTOR_PLUS || factor.getKind() == kind::BITVECTOR_SUB || factor.getKind() == kind::BITVECTOR_NEG); @@ -345,32 +389,24 @@ template<> inline Node RewriteRule::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - TNode constant; - TNode factor; - if (node[0].getKind() == kind::CONST_BITVECTOR) { - constant = node[0]; - factor = node[1]; - } else { - Assert(node[1].getKind() == kind::CONST_BITVECTOR); - constant = node[1]; - factor = node[0]; - } + TNode constant = node[1]; + TNode factor = node[0]; + Assert(constant.getKind() == kind::CONST_BITVECTOR); if (factor.getKind() == kind::BITVECTOR_NEG) { // push negation on the constant part BitVector const_bv = constant.getConst(); - return utils::mkSortedNode(kind::BITVECTOR_MULT, - utils::mkConst(-const_bv), - factor[0]); + return utils::mkNode(kind::BITVECTOR_MULT, + factor[0], + utils::mkConst(-const_bv)); } std::vector children; for(unsigned i = 0; i < factor.getNumChildren(); ++i) { - children.push_back(utils::mkSortedNode(kind::BITVECTOR_MULT, constant, factor[i])); + children.push_back(utils::mkNode(kind::BITVECTOR_MULT, factor[i], constant)); } - return utils::mkSortedNode(factor.getKind(), children); - + return utils::mkNode(factor.getKind(), children); } @@ -427,18 +463,6 @@ Node RewriteRule::apply(TNode node) { std::vector childrenLeft, childrenRight; - // If both constants are nonzero, combine on right, otherwise leave them where they are - if (rightConst != zero) { - rightConst = rightConst - leftConst; - leftConst = zero; - if (rightConst != zero) { - childrenRight.push_back(utils::mkConst(rightConst)); - } - } - else if (leftConst != zero) { - childrenLeft.push_back(utils::mkConst(leftConst)); - } - std::map::const_iterator iLeft = leftMap.begin(), iLeftEnd = leftMap.end(); std::map::const_iterator iRight = rightMap.begin(), iRightEnd = rightMap.end(); @@ -481,6 +505,7 @@ Node RewriteRule::apply(TNode node) { if (incLeft) { ++iLeft; if (iLeft != iLeftEnd) { + Assert(termLeft < iLeft->first); coeffLeft = iLeft->second; termLeft = iLeft->first; } @@ -488,6 +513,7 @@ Node RewriteRule::apply(TNode node) { if (incRight) { ++iRight; if (iRight != iRightEnd) { + Assert(termRight < iRight->first); coeffRight = iRight->second; termRight = iRight->first; } @@ -496,31 +522,41 @@ Node RewriteRule::apply(TNode node) { // construct result + // If both constants are nonzero, combine on right, otherwise leave them where they are + if (rightConst != zero) { + rightConst = rightConst - leftConst; + leftConst = zero; + if (rightConst != zero) { + childrenRight.push_back(utils::mkConst(rightConst)); + } + } + else if (leftConst != zero) { + childrenLeft.push_back(utils::mkConst(leftConst)); + } + Node newLeft, newRight; if(childrenRight.size() == 0 && leftConst != zero) { - Assert(childrenLeft[0].isConst() && childrenLeft[0].getConst() == leftConst); + Assert(childrenLeft.back().isConst() && childrenLeft.back().getConst() == leftConst); if (childrenLeft.size() == 1) { // c = 0 ==> false return utils::mkFalse(); } // special case - if right is empty and left has a constant, move the constant - // TODO: this is inefficient - would be better if constant were at the end in the normal form childrenRight.push_back(utils::mkConst(-leftConst)); - childrenLeft.erase(childrenLeft.begin()); + childrenLeft.pop_back(); } if(childrenLeft.size() == 0) { if (rightConst != zero) { - Assert(childrenRight[0].isConst() && childrenRight[0].getConst() == rightConst); + Assert(childrenRight.back().isConst() && childrenRight.back().getConst() == rightConst); if (childrenRight.size() == 1) { // 0 = c ==> false return utils::mkFalse(); } // special case - if left is empty and right has a constant, move the constant - // TODO: this is inefficient - would be better if constant were at the end in the normal form newLeft = utils::mkConst(-rightConst); - childrenRight.erase(childrenRight.begin()); + childrenRight.pop_back(); } else { newLeft = utils::mkConst(size, (unsigned)0); @@ -530,7 +566,7 @@ Node RewriteRule::apply(TNode node) { newLeft = childrenLeft[0]; } else { - newLeft = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenLeft); + newLeft = utils::mkNode(kind::BITVECTOR_PLUS, childrenLeft); } if (childrenRight.size() == 0) { @@ -540,7 +576,7 @@ Node RewriteRule::apply(TNode node) { newRight = childrenRight[0]; } else { - newRight = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenRight); + newRight = utils::mkNode(kind::BITVECTOR_PLUS, childrenRight); } // Assert(newLeft == Rewriter::rewrite(newLeft)); @@ -552,9 +588,15 @@ Node RewriteRule::apply(TNode node) { } if (newLeft < newRight) { + Assert((newRight == left && newLeft == right) || + Rewriter::rewrite(newRight) != left || + Rewriter::rewrite(newLeft) != right); return newRight.eqNode(newLeft); } + Assert((newLeft == left && newRight == right) || + Rewriter::rewrite(newLeft) != left || + Rewriter::rewrite(newRight) != right); return newLeft.eqNode(newRight); } @@ -685,33 +727,26 @@ Node RewriteRule::apply(TNode node) { template<> inline bool RewriteRule::applies(TNode node) { if(node.getKind()!= kind::BITVECTOR_NEG || - node[0].getKind() != kind::BITVECTOR_MULT) { - return false; + node[0].getKind() != kind::BITVECTOR_MULT) { + return false; } - TNode mult = node[0]; - for (unsigned i = 0; i < mult.getNumChildren(); ++i) { - if (mult[i].getKind() == kind::CONST_BITVECTOR) { - return true; - } - } - return false; + return node[node.getNumChildren()-1].isConst(); } template<> inline Node RewriteRule::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; TNode mult = node[0]; - std::vector children; + NodeBuilder<> nb(kind::BITVECTOR_MULT); BitVector bv(utils::getSize(node), (unsigned)1); - for(unsigned i = 0; i < mult.getNumChildren(); ++i) { - if(mult[i].getKind() == kind::CONST_BITVECTOR) { - bv = bv * mult[i].getConst(); - } else { - children.push_back(mult[i]); - } - } - children.push_back(utils::mkConst(-bv)); - return utils::mkSortedNode(kind::BITVECTOR_MULT, children); + TNode::iterator child_it = mult.begin(); + for(; (child_it+1) != mult.end(); ++child_it) { + nb << (*child_it); + } + Assert((*child_it).isConst()); + bv = (*child_it).getConst(); + nb << utils::mkConst(-bv); + return Node(nb); } template<> inline @@ -739,7 +774,7 @@ Node RewriteRule::apply(TNode node) { for (unsigned i = 0; i < node[0].getNumChildren(); ++i) { children.push_back(utils::mkNode(kind::BITVECTOR_NEG, node[0][i])); } - return utils::mkSortedNode(kind::BITVECTOR_PLUS, children); + return utils::mkNode(kind::BITVECTOR_PLUS, children); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index ee0e0fc43..8e14980a7 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -656,51 +656,6 @@ Node RewriteRule::apply(TNode node) { return utils::mkNode(kind::BITVECTOR_ULT, b, a); } -/** - * MultOne - * - * (a * 1) ==> a - */ - -template<> inline -bool RewriteRule::applies(TNode node) { - unsigned size = utils::getSize(node); - return (node.getKind() == kind::BITVECTOR_MULT && - (node[0] == utils::mkConst(size, 1) || - node[1] == utils::mkConst(size, 1))); -} - -template<> inline -Node RewriteRule::apply(TNode node) { - BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - unsigned size = utils::getSize(node); - if (node[0] == utils::mkConst(size, 1)) { - return node[1]; - } - Assert(node[1] == utils::mkConst(size, 1)); - return node[0]; -} - -/** - * MultZero - * - * (a * 0) ==> 0 - */ - -template<> inline -bool RewriteRule::applies(TNode node) { - unsigned size = utils::getSize(node); - return (node.getKind() == kind::BITVECTOR_MULT && - (node[0] == utils::mkConst(size, 0) || - node[1] == utils::mkConst(size, 0))); -} - -template<> inline -Node RewriteRule::apply(TNode node) { - BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - return utils::mkConst(utils::getSize(node), 0); -} - /** * MultPow2 * @@ -736,38 +691,13 @@ Node RewriteRule::apply(TNode node) { } } - Node a = utils::mkSortedNode(kind::BITVECTOR_MULT, children); + Node a = utils::mkNode(kind::BITVECTOR_MULT, children); Node extract = utils::mkExtract(a, utils::getSize(node) - exponent - 1, 0); Node zeros = utils::mkConst(exponent, 0); return utils::mkConcat(extract, zeros); } -/** - * PlusZero - * - * (a + 0) ==> a - */ - -template<> inline -bool RewriteRule::applies(TNode node) { - Node zero = utils::mkConst(utils::getSize(node), 0); - return (node.getKind() == kind::BITVECTOR_PLUS && - (node[0] == zero || - node[1] == zero)); -} - -template<> inline -Node RewriteRule::apply(TNode node) { - BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - Node zero = utils::mkConst(utils::getSize(node), 0); - if (node[0] == zero) { - return node[1]; - } - - return node[0]; -} - /** * NegIdemp * @@ -966,7 +896,7 @@ Node RewriteRule::apply(TNode node) { Assert(neg_count!= 0); children.push_back(utils::mkConst(utils::getSize(node), neg_count)); - return utils::mkSortedNode(kind::BITVECTOR_PLUS, children); + return utils::mkNode(kind::BITVECTOR_PLUS, children); } // /** diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 60715ee60..bfd8a2897 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -84,7 +84,7 @@ public: static RewriteResponse preRewrite(TNode node); - static inline Node rewriteEquality(TNode node) { + static Node rewriteEquality(TNode node) { Debug("bitvector") << "TheoryBV::rewriteEquality(" << node << ")" << std::endl; return postRewrite(node).node; } diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index c456ef73f..a0d418c4b 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -95,12 +95,10 @@ inline Node mkAnd(std::vector& children) { } inline Node mkSortedNode(Kind kind, std::vector& children) { - Assert (kind == kind::BITVECTOR_PLUS || - kind == kind::BITVECTOR_MULT || - kind == kind::BITVECTOR_AND || + Assert (kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_XOR); - + Assert(children.size() > 0); if (children.size() == 1) { return children[0]; } @@ -126,9 +124,7 @@ inline Node mkNode(Kind kind, TNode child1, TNode child2) { inline Node mkSortedNode(Kind kind, TNode child1, TNode child2) { - Assert (kind == kind::BITVECTOR_PLUS || - kind == kind::BITVECTOR_MULT || - kind == kind::BITVECTOR_AND || + Assert (kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_XOR); -- cgit v1.2.3