diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-15 19:05:56 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-15 19:05:56 +0000 |
commit | c8f7cff1911b1fb3136f41e67d92a3d66280add7 (patch) | |
tree | 8ee9f3ab7853e265b3c6dada03984a02555770c5 /src/theory/bv | |
parent | 43839eed3814cb4175869cd1fbbb4e9a5ece59dc (diff) |
Fixes some assertion failures
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 896133e46..13c049c85 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -615,8 +615,7 @@ Node RewriteRule<SolveEq>::apply(TNode node) { template<> inline bool RewriteRule<BitwiseEq>::applies(TNode node) { - if (node.getKind() != kind::EQUAL || - utils::getSize(node[0]) != 1) { + if (node.getKind() != kind::EQUAL) { return false; } TNode term; @@ -636,11 +635,15 @@ bool RewriteRule<BitwiseEq>::applies(TNode node) { case kind::BITVECTOR_AND: case kind::BITVECTOR_OR: //operator BITVECTOR_XOR 2: "bitwise xor" - case kind::BITVECTOR_NOT: case kind::BITVECTOR_NAND: case kind::BITVECTOR_NOR: //operator BITVECTOR_XNOR 2 "bitwise xnor" case kind::BITVECTOR_COMP: + if (utils::getSize(node[0]) != 1) { + return false; + } + break; + case kind::BITVECTOR_NOT: case kind::BITVECTOR_NEG: return true; break; @@ -678,7 +681,7 @@ Node RewriteRule<BitwiseEq>::apply(TNode node) { term = node[0]; } - bool eqOne = (c == BitVector(1,(unsigned)1)); + bool eqOne = (c == BitVector(utils::getSize(node[0]),(unsigned)1)); switch (term.getKind()) { case kind::BITVECTOR_AND: @@ -724,7 +727,7 @@ Node RewriteRule<BitwiseEq>::apply(TNode node) { return term[0].eqNode(term[1]).notNode(); } case kind::BITVECTOR_NEG: - return term[0].eqNode(utils::mkConst(c)); + return term[0].eqNode(utils::mkConst(-c)); default: break; } |