diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/kinds | 11 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 20 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h | 51 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 21 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 23 |
6 files changed, 121 insertions, 8 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 052e477ea..aeae1073e 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -120,6 +120,14 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign- parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" +constant INT_TO_BITVECTOR_OP \ + ::CVC4::IntToBitVector \ + "::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \ + "util/bitvector.h" \ + "operator for the integer conversion to bit-vector" +parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector" +operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer" + typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule @@ -166,4 +174,7 @@ typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule +typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule +typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule + endtheory diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index baaf7e133..8426afb59 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -66,6 +66,9 @@ enum RewriteRuleId { SremEliminate, ZeroExtendEliminate, SignExtendEliminate, + BVToNatEliminate, + IntToBVEliminate, + /// ground term evaluation EvalEquals, EvalConcat, @@ -173,13 +176,15 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case FailEq: out << "FailEq"; return out; case SimplifyEq: out << "SimplifyEq"; return out; case ReflexivityEq: out << "ReflexivityEq"; return out; - case UgtEliminate: out << "UgtEliminate"; return out; - case SgtEliminate: out << "SgtEliminate"; return out; - case UgeEliminate: out << "UgeEliminate"; return out; - case SgeEliminate: out << "SgeEliminate"; return out; + case UgtEliminate: out << "UgtEliminate"; return out; + case SgtEliminate: out << "SgtEliminate"; return out; + case UgeEliminate: out << "UgeEliminate"; return out; + case SgeEliminate: out << "SgeEliminate"; return out; case RepeatEliminate: out << "RepeatEliminate"; return out; case RotateLeftEliminate: out << "RotateLeftEliminate"; return out; case RotateRightEliminate:out << "RotateRightEliminate";return out; + case BVToNatEliminate: out << "BVToNatEliminate"; return out; + case IntToBVEliminate: out << "IntToBVEliminate"; return out; case NandEliminate: out << "NandEliminate"; return out; case NorEliminate : out << "NorEliminate"; return out; case SdivEliminate : out << "SdivEliminate"; return out; @@ -214,7 +219,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case ExtractBitwise : out << "ExtractBitwise"; return out; case ExtractNot : out << "ExtractNot"; return out; case ExtractArith : out << "ExtractArith"; return out; - case ExtractArith2 : out << "ExtractArith2"; return out; + case ExtractArith2 : out << "ExtractArith2"; return out; case DoubleNeg : out << "DoubleNeg"; return out; case NotConcat : out << "NotConcat"; return out; case NotAnd : out << "NotAnd"; return out; @@ -226,7 +231,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case BitwiseNotOr : out << "BitwiseNotOr"; return out; case XorNot : out << "XorNot"; return out; case LtSelf : out << "LtSelf"; return out; - case LteSelf : out << "LteSelf"; return out; + case LteSelf : out << "LteSelf"; return out; case UltZero : out << "UltZero"; return out; case UleZero : out << "UleZero"; return out; case ZeroUle : out << "ZeroUle"; return out; @@ -491,7 +496,8 @@ struct AllRewriteRules { RewriteRule<BitwiseEq> rule113; RewriteRule<UltOne> rule114; RewriteRule<SltZero> rule115; - + RewriteRule<BVToNatEliminate> rule116; + RewriteRule<IntToBVEliminate> rule117; }; template<> inline 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 cf36633fa..b513dbf90 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -231,6 +231,57 @@ Node RewriteRule<RotateRightEliminate>::apply(TNode node) { } template<> +bool RewriteRule<BVToNatEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_TO_NAT); +} + +template<> +Node RewriteRule<BVToNatEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl; + + const unsigned size = utils::getSize(node[0]); + NodeManager* const nm = NodeManager::currentNM(); + const Node z = nm->mkConst(Rational(0)); + const Node bvone = nm->mkConst(BitVector(1u, 1u)); + + NodeBuilder<> result(kind::PLUS); + Integer i = 1; + for(unsigned bit = 0; bit < size; ++bit, i *= 2) { + Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]), bvone); + result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z); + } + + return Node(result); +} + +template<> +bool RewriteRule<IntToBVEliminate>::applies(TNode node) { + return (node.getKind() == kind::INT_TO_BITVECTOR); +} + +template<> +Node RewriteRule<IntToBVEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl; + + const unsigned size = node.getOperator().getConst<IntToBitVector>().size; + NodeManager* const nm = NodeManager::currentNM(); + const Node bvzero = nm->mkConst(BitVector(1u, 0u)); + const Node bvone = nm->mkConst(BitVector(1u, 1u)); + + std::vector<Node> v; + Integer i = 2; + while(v.size() < size) { + Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2))); + v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero)); + i *= 2; + } + + NodeBuilder<> result(kind::BITVECTOR_CONCAT); + result.append(v.rbegin(), v.rend()); + return Node(result); +} + +template<> bool RewriteRule<NandEliminate>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_NAND && node.getNumChildren() == 2); diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index f698ec83d..2467ae3f1 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -553,11 +553,27 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool prerewrite RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite){ Node resultNode = LinearRewriteStrategy < RewriteRule<RotateLeftEliminate > - >::apply(node); + >::apply(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { + Node resultNode = LinearRewriteStrategy + < RewriteRule<BVToNatEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) { + Node resultNode = LinearRewriteStrategy + < RewriteRule<IntToBVEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) { if (prerewrite) { Node resultNode = LinearRewriteStrategy @@ -640,6 +656,9 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend; d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight; d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft; + + d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat; + d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV; } Node TheoryBVRewriter::eliminateBVSDiv(TNode node) { diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 183b5e8d5..def8e24fe 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -78,6 +78,9 @@ class TheoryBVRewriter { static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false); + static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false); + static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false); + public: static RewriteResponse postRewrite(TNode node); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index effef49e8..67dae0cfa 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -195,6 +195,29 @@ public: } }; +class BitVectorConversionTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if(n.getKind() == kind::BITVECTOR_TO_NAT) { + if(check && !n[0].getType(check).isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + return nodeManager->integerType(); + } + + if(n.getKind() == kind::INT_TO_BITVECTOR) { + size_t bvSize = n.getOperator().getConst<IntToBitVector>(); + if(check && !n[0].getType(check).isInteger()) { + throw TypeCheckingExceptionPrivate(n, "expecting integer term"); + } + return nodeManager->mkBitVectorType(bvSize); + } + + InternalError("bv-conversion typerule invoked for non-bv-conversion kind"); + } +}; + class CardinalityComputer { public: inline static Cardinality computeCardinality(TypeNode type) { |