diff options
author | lianah <lianahady@gmail.com> | 2013-05-07 17:21:58 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-05-07 17:21:58 -0400 |
commit | b702a70790f37e239c6f8c91bbc0ac107f1a4618 (patch) | |
tree | 2e9cd845556faa0e9a16561435b7c1a7da8ebb0a /src/theory/bv | |
parent | 778004b0fe366f6ecfb53a594bd5be335a2dc4b7 (diff) |
added type checking rule to check for bit-vector constants of size 0
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 17 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 5 |
2 files changed, 19 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index d660dde29..ff7d67cb0 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -45,7 +45,9 @@ template<> inline Node RewriteRule<ShlByConst>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<ShlByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); - + if (amount == 0) { + return node[0]; + } Node a = node[0]; uint32_t size = utils::getSize(a); @@ -59,6 +61,7 @@ Node RewriteRule<ShlByConst>::apply(TNode node) { Assert(amount < Integer(1).multiplyByPow2(32)); uint32_t uint32_amount = amount.toUnsignedInt(); + Node left = utils::mkExtract(a, size - 1 - uint32_amount, 0); Node right = utils::mkConst(BitVector(uint32_amount, Integer(0))); return utils::mkConcat(left, right); @@ -81,6 +84,9 @@ template<> inline Node RewriteRule<LshrByConst>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<LshrByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); + if (amount == 0) { + return node[0]; + } Node a = node[0]; uint32_t size = utils::getSize(a); @@ -117,7 +123,10 @@ template<> inline Node RewriteRule<AshrByConst>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<AshrByConst>(" << node << ")" << std::endl; Integer amount = node[1].getConst<BitVector>().toInteger(); - + if (amount == 0) { + return node[0]; + } + Node a = node[0]; uint32_t size = utils::getSize(a); Node sign_bit = utils::mkExtract(a, size-1, size-1); @@ -812,7 +821,9 @@ Node RewriteRule<UdivPow2>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<UdivPow2>(" << node << ")" << std::endl; Node a = node[0]; unsigned power = utils::isPow2Const(node[1]) -1; - + if (power == 0) { + return a; + } Node extract = utils::mkExtract(a, utils::getSize(node) - 1, power); Node zeros = utils::mkConst(power, 0); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 00284e7ae..effef49e8 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -29,6 +29,11 @@ class BitVectorConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { + if (check) { + if (n.getConst<BitVector>().getSize() == 0) { + throw TypeCheckingExceptionPrivate(n, "constant of size 0"); + } + } return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize()); } }; |