diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-15 20:51:05 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-15 20:51:05 +0000 |
| commit | b286d6463eb671d35b81958b18309b8f096c2586 (patch) | |
| tree | c690e7448a05d241ad2387edc9d14430d3f98dd7 /src/theory/bv | |
| parent | c8f7cff1911b1fb3136f41e67d92a3d66280add7 (diff) | |
Reverting rewrite rule to working version
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 13c049c85..896133e46 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -615,7 +615,8 @@ Node RewriteRule<SolveEq>::apply(TNode node) { template<> inline bool RewriteRule<BitwiseEq>::applies(TNode node) { - if (node.getKind() != kind::EQUAL) { + if (node.getKind() != kind::EQUAL || + utils::getSize(node[0]) != 1) { return false; } TNode term; @@ -635,15 +636,11 @@ 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; @@ -681,7 +678,7 @@ Node RewriteRule<BitwiseEq>::apply(TNode node) { term = node[0]; } - bool eqOne = (c == BitVector(utils::getSize(node[0]),(unsigned)1)); + bool eqOne = (c == BitVector(1,(unsigned)1)); switch (term.getKind()) { case kind::BITVECTOR_AND: @@ -727,7 +724,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; } |