From: Andrew Reynolds Date: Mon, 11 Jul 2022 20:02:59 +0000 (-0500) Subject: Move bv arith conversions to arith (#8945) X-Git-Tag: cvc5-1.0.1~6 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c3a730c70623001c93751759aee3ab2b3d6fb07;p=cvc5.git Move bv arith conversions to arith (#8945) This is in preparation for lazier handling of bv2nat and int2bv. Our infrastructure in arithmetic is better equipped for doing this. There are no behavior changes in this PR. --- diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index c6ac28950..a5bec7d9e 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -247,6 +247,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::INTS_DIVISION_TOTAL: case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, true); case kind::ABS: return rewriteAbs(t); + case kind::BITVECTOR_TO_NAT: + case kind::INT_TO_BITVECTOR: case kind::IS_INTEGER: case kind::TO_INTEGER: case kind::TO_REAL: @@ -344,10 +346,10 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ ss << " " << t; throw LogicException(ss.str()); } - case kind::PI: - return RewriteResponse(REWRITE_DONE, t); - default: - Unreachable(); + case kind::BITVECTOR_TO_NAT: return rewriteBVToNat(t); + case kind::INT_TO_BITVECTOR: return rewriteIntToBV(t); + case kind::PI: return RewriteResponse(REWRITE_DONE, t); + default: Unreachable(); } } } @@ -1109,6 +1111,26 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) return RewriteResponse(REWRITE_DONE, t); } +RewriteResponse ArithRewriter::rewriteBVToNat(TNode node) +{ + if (node[0].isConst()) + { + Node resultNode = eliminateBv2Nat(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, node); +} + +RewriteResponse ArithRewriter::rewriteIntToBV(TNode node) +{ + if (node[0].isConst()) + { + Node resultNode = eliminateInt2Bv(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, node); +} + TrustNode ArithRewriter::expandDefinition(Node node) { // call eliminate operators, to eliminate partial operators only diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 12f288d74..01b1fa95a 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -92,6 +92,11 @@ class ArithRewriter : public TheoryRewriter /** postRewrite transcendental functions */ static RewriteResponse postRewriteTranscendental(TNode t); + /** rewrite bv2nat */ + static RewriteResponse rewriteBVToNat(TNode node); + /** rewrite int2bv */ + static RewriteResponse rewriteIntToBV(TNode node); + /** return rewrite */ static RewriteResponse returnRewrite(TNode t, Node ret, Rewrite r); /** The operator elimination utility */ diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 02fda5156..dfdd5b754 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -17,6 +17,9 @@ #include +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" + using namespace cvc5::internal::kind; namespace cvc5::internal { @@ -307,6 +310,58 @@ std::pair mkSameType(const Node& a, const Node& b) return {a, nm->mkNode(kind::TO_REAL, b)}; } +/* ------------------------------------------------------------------------- */ + +Node eliminateBv2Nat(TNode node) +{ + const unsigned size = bv::utils::getSize(node[0]); + NodeManager* const nm = NodeManager::currentNM(); + const Node z = nm->mkConstInt(Rational(0)); + const Node bvone = bv::utils::mkOne(1); + + Integer i = 1; + std::vector children; + 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); + children.push_back( + nm->mkNode(kind::ITE, cond, nm->mkConstInt(Rational(i)), z)); + } + // avoid plus with one child + return children.size() == 1 ? children[0] : nm->mkNode(kind::ADD, children); +} + +Node eliminateInt2Bv(TNode node) +{ + const uint32_t size = node.getOperator().getConst().d_size; + NodeManager* const nm = NodeManager::currentNM(); + const Node bvzero = bv::utils::mkZero(1); + const Node bvone = bv::utils::mkOne(1); + + std::vector v; + Integer i = 2; + while (v.size() < size) + { + Node cond = nm->mkNode( + kind::GEQ, + nm->mkNode( + kind::INTS_MODULUS_TOTAL, node[0], nm->mkConstInt(Rational(i))), + nm->mkConstInt(Rational(i, 2))); + v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero)); + i *= 2; + } + if (v.size() == 1) + { + return v[0]; + } + NodeBuilder result(kind::BITVECTOR_CONCAT); + result.append(v.rbegin(), v.rend()); + return Node(result); +} + } // namespace arith } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index c08dbff0b..6628c2621 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -341,6 +341,24 @@ Node mkEquality(const Node& a, const Node& b); */ std::pair mkSameType(const Node& a, const Node& b); +/** + * Returns the rewritten form of node, which is a term of the form bv2nat(x). + * The return value of this method is the integer sum: + * (+ ite( (= ((_ extract (n-1) (n-1)) x) 1) (^ 2 (n-1)) 0) + * ... + * ite( (= ((_ extract 0 0) x) 1) (^ 2 0) 0)) + * where n is the bitwidth of x. + */ +Node eliminateBv2Nat(TNode node); +/** + * Returns the rewritten form of node, which is a term of the form int2bv(x). + * The return value of this method is the concatenation term: + * (bvconcat ite( (>= (mod x (^ 2 n)) (^ 2 (n-1))) (_ bv1 1) (_ bv1 0)) + * ... + * ite( (>= (mod x (^ 2 1)) (^ 2 0)) (_ bv1 1) (_ bv1 0))) + * where n is the bit-width of x. + */ +Node eliminateInt2Bv(TNode node); } // namespace arith } // namespace theory diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 5b302369a..e10d5fd14 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -183,4 +183,20 @@ parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter i typerule IAND_OP ::cvc5::internal::theory::arith::IAndOpTypeRule typerule IAND ::cvc5::internal::theory::arith::IAndTypeRule +## conversion kinds +operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector" + +constant INT_TO_BITVECTOR_OP \ + struct \ + IntToBitVector \ + "::cvc5::internal::UnsignedHashFunction< ::cvc5::internal::IntToBitVector >" \ + "util/bitvector.h" \ + "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::internal::IntToBitVector class" +parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term" + +## conversion kinds +typerule BITVECTOR_TO_NAT ::cvc5::internal::theory::arith::BitVectorConversionTypeRule +typerule INT_TO_BITVECTOR_OP ::cvc5::internal::theory::arith::IntToBitVectorOpTypeRule +typerule INT_TO_BITVECTOR ::cvc5::internal::theory::arith::BitVectorConversionTypeRule + endtheory diff --git a/src/theory/arith/linear/normal_form.cpp b/src/theory/arith/linear/normal_form.cpp index 90a96a874..956a64bf6 100644 --- a/src/theory/arith/linear/normal_form.cpp +++ b/src/theory/arith/linear/normal_form.cpp @@ -42,17 +42,6 @@ bool Variable::isLeafMember(Node n){ VarList::VarList(Node n) : NodeWrapper(n) { Assert(isSorted(begin(), end())); } -bool Variable::isIAndMember(Node n) -{ - return n.getKind() == kind::IAND && Polynomial::isMember(n[0]) - && Polynomial::isMember(n[1]); -} - -bool Variable::isPow2Member(Node n) -{ - return n.getKind() == kind::POW2 && Polynomial::isMember(n[0]); -} - bool Variable::isDivMember(Node n){ switch(n.getKind()){ case kind::DIVISION: @@ -67,30 +56,18 @@ bool Variable::isDivMember(Node n){ } } -bool Variable::isTranscendentalMember(Node n) { - switch(n.getKind()){ - case kind::EXPONENTIAL: - case kind::SINE: - case kind::COSINE: - case kind::TANGENT: - case kind::COSECANT: - case kind::SECANT: - case kind::COTANGENT: - case kind::ARCSINE: - case kind::ARCCOSINE: - case kind::ARCTANGENT: - case kind::ARCCOSECANT: - case kind::ARCSECANT: - case kind::ARCCOTANGENT: - case kind::SQRT: return Polynomial::isMember(n[0]); - case kind::PI: - return true; - default: - return false; +bool Variable::areChildrenPolynomialMembers(Node n) +{ + for (const Node& nc : n) + { + if (!Polynomial::isMember(nc)) + { + return false; + } } + return true; } - bool VarList::isSorted(iterator start, iterator end) { return std::is_sorted(start, end); } diff --git a/src/theory/arith/linear/normal_form.h b/src/theory/arith/linear/normal_form.h index 1829a20f6..6a2cc1471 100644 --- a/src/theory/arith/linear/normal_form.h +++ b/src/theory/arith/linear/normal_form.h @@ -239,8 +239,8 @@ public: case kind::INTS_DIVISION_TOTAL: case kind::INTS_MODULUS_TOTAL: case kind::DIVISION_TOTAL: return isDivMember(n); - case kind::IAND: return isIAndMember(n); - case kind::POW2: return isPow2Member(n); + case kind::IAND: + case kind::POW2: case kind::EXPONENTIAL: case kind::SINE: case kind::COSINE: @@ -255,7 +255,9 @@ public: case kind::ARCSECANT: case kind::ARCCOTANGENT: case kind::SQRT: - case kind::PI: return isTranscendentalMember(n); + case kind::PI: + case kind::INT_TO_BITVECTOR: + case kind::BITVECTOR_TO_NAT: return areChildrenPolynomialMembers(n); case kind::ABS: case kind::TO_INTEGER: // Treat to_int as a variable; it is replaced in early preprocessing @@ -266,13 +268,15 @@ public: } static bool isLeafMember(Node n); - static bool isIAndMember(Node n); - static bool isPow2Member(Node n); static bool isDivMember(Node n); bool isDivLike() const{ return isDivMember(getNode()); } - static bool isTranscendentalMember(Node n); + /** + * Return true if all direct children of n are polynomial members (returns + * true for Polynomial::isMember). + */ + static bool areChildrenPolynomialMembers(Node n); bool isNormalForm() { return isMember(getNode()); } diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 65caeb3d3..ffa19e6d5 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -390,6 +390,8 @@ Node OperatorElim::eliminateOperators(Node node, return var; } + case BITVECTOR_TO_NAT: return eliminateBv2Nat(node); break; + case INT_TO_BITVECTOR: return eliminateInt2Bv(node); break; default: break; } return node; diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp index 8b66d092f..883c3fa78 100644 --- a/src/theory/arith/theory_arith_type_rules.cpp +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -15,6 +15,7 @@ #include "theory/arith/theory_arith_type_rules.h" +#include "util/bitvector.h" #include "util/rational.h" namespace cvc5::internal { @@ -210,6 +211,42 @@ TypeNode IndexedRootPredicateTypeRule::computeType(NodeManager* nodeManager, return nodeManager->booleanType(); } +TypeNode IntToBitVectorOpTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::INT_TO_BITVECTOR_OP); + size_t bvSize = n.getConst(); + if (bvSize == 0) + { + throw TypeCheckingExceptionPrivate(n, "expecting bit-width > 0"); + } + return nodeManager->mkFunctionType(nodeManager->integerType(), + nodeManager->mkBitVectorType(bvSize)); +} + +TypeNode BitVectorConversionTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (n.getKind() == kind::BITVECTOR_TO_NAT) + { + if (check && !n[0].getType(check).isBitVector()) + { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + return nodeManager->integerType(); + } + + Assert(n.getKind() == kind::INT_TO_BITVECTOR); + size_t bvSize = n.getOperator().getConst(); + if (check && !n[0].getType(check).isInteger()) + { + throw TypeCheckingExceptionPrivate(n, "expecting integer term"); + } + return nodeManager->mkBitVectorType(bvSize); +} + } // namespace arith } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 90834a776..9fc9e1145 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -123,6 +123,18 @@ class IndexedRootPredicateTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +class IntToBitVectorOpTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; + +class BitVectorConversionTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; + } // namespace arith } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 90eeeefc9..d665175bb 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -92,9 +92,6 @@ operator BITVECTOR_REDOR 1 "bit-vector redor" ## if-then-else kind operator BITVECTOR_ITE 3 "same semantics as regular ITE, but condition is bv of size 1 instead of Boolean" -## conversion kinds -operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector" - ## internal kinds operator BITVECTOR_ACKERMANNIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" operator BITVECTOR_ACKERMANNIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" @@ -158,14 +155,6 @@ constant BITVECTOR_ZERO_EXTEND_OP \ "operator for the bit-vector zero-extend; payload is an instance of the cvc5::internal::BitVectorZeroExtend class" parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term" -constant INT_TO_BITVECTOR_OP \ - struct \ - IntToBitVector \ - "::cvc5::internal::UnsignedHashFunction< ::cvc5::internal::IntToBitVector >" \ - "util/bitvector.h" \ - "operator for the integer conversion to bit-vector; payload is an instance of the cvc5::internal::IntToBitVector class" -parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term" - ### type rules for non-parameterized operator kinds --------------------------- typerule CONST_BITVECTOR ::cvc5::internal::theory::bv::BitVectorConstantTypeRule @@ -222,9 +211,6 @@ typerule BITVECTOR_ITE ::cvc5::internal::theory::bv::BitVectorITETypeRule typerule BITVECTOR_REDAND ::cvc5::internal::theory::bv::BitVectorUnaryPredicateTypeRule typerule BITVECTOR_REDOR ::cvc5::internal::theory::bv::BitVectorUnaryPredicateTypeRule -## conversion kinds -typerule BITVECTOR_TO_NAT ::cvc5::internal::theory::bv::BitVectorConversionTypeRule - ## internal kinds typerule BITVECTOR_ACKERMANNIZE_UDIV ::cvc5::internal::theory::bv::BitVectorAckermanizationUdivTypeRule typerule BITVECTOR_ACKERMANNIZE_UREM ::cvc5::internal::theory::bv::BitVectorAckermanizationUremTypeRule @@ -246,7 +232,5 @@ typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule" typerule BITVECTOR_SIGN_EXTEND ::cvc5::internal::theory::bv::BitVectorExtendTypeRule typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule" typerule BITVECTOR_ZERO_EXTEND ::cvc5::internal::theory::bv::BitVectorExtendTypeRule -typerule INT_TO_BITVECTOR_OP ::cvc5::internal::theory::bv::IntToBitVectorOpTypeRule -typerule INT_TO_BITVECTOR ::cvc5::internal::theory::bv::BitVectorConversionTypeRule endtheory 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 f9b0bcdfe..1eac7581d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -264,40 +264,6 @@ inline Node RewriteRule::apply(TNode node) return result; } -template <> -inline bool RewriteRule::applies(TNode node) -{ - return (node.getKind() == kind::BITVECTOR_TO_NAT); -} - -template <> -inline Node RewriteRule::apply(TNode node) -{ - Trace("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - - //if( node[0].isConst() ){ - //TODO? direct computation instead of term construction+rewriting - //} - return utils::eliminateBv2Nat(node); -} - -template <> -inline bool RewriteRule::applies(TNode node) -{ - return (node.getKind() == kind::INT_TO_BITVECTOR); -} - -template <> -inline Node RewriteRule::apply(TNode node) -{ - Trace("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - - //if( node[0].isConst() ){ - //TODO? direct computation instead of term construction+rewriting - //} - return utils::eliminateInt2Bv(node); -} - template <> inline bool RewriteRule::applies(TNode node) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 3069b12c0..37450768d 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -61,16 +61,6 @@ TrustNode TheoryBVRewriter::expandDefinition(Node node) case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: case kind::BITVECTOR_SMOD: ret = eliminateBVSDiv(node); break; - case kind::BITVECTOR_TO_NAT: - - ret = utils::eliminateBv2Nat(node); - - break; - case kind::INT_TO_BITVECTOR: - - ret = utils::eliminateInt2Bv(node); - - break; default: break; } if (!ret.isNull() && node != ret) @@ -644,31 +634,6 @@ RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } -RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { - if (node[0].isConst()) - { - Node resultNode = LinearRewriteStrategy - < RewriteRule - >::apply(node); - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - }else{ - return RewriteResponse(REWRITE_DONE, node); - } -} - -RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) { - if (node[0].isConst()) - { - Node resultNode = LinearRewriteStrategy - < RewriteRule - >::apply(node); - - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - }else{ - return RewriteResponse(REWRITE_DONE, node); - } -} - RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) { if (prerewrite) { Node resultNode = LinearRewriteStrategy @@ -756,9 +721,6 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_SLTBV ] = RewriteSltBv; d_rewriteTable [ kind::BITVECTOR_ITE ] = RewriteITEBv; d_rewriteTable[kind::BITVECTOR_EAGER_ATOM] = RewriteEagerAtom; - - 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_type_rules.cpp b/src/theory/bv/theory_bv_type_rules.cpp index 7e8b8b0d3..a1ee0eeff 100644 --- a/src/theory/bv/theory_bv_type_rules.cpp +++ b/src/theory/bv/theory_bv_type_rules.cpp @@ -266,42 +266,6 @@ TypeNode BitVectorExtendTypeRule::computeType(NodeManager* nodeManager, return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize()); } -TypeNode IntToBitVectorOpTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - Assert(n.getKind() == kind::INT_TO_BITVECTOR_OP); - size_t bvSize = n.getConst(); - if (bvSize == 0) - { - throw TypeCheckingExceptionPrivate(n, "expecting bit-width > 0"); - } - return nodeManager->mkFunctionType(nodeManager->integerType(), - nodeManager->mkBitVectorType(bvSize)); -} - -TypeNode BitVectorConversionTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - if (n.getKind() == kind::BITVECTOR_TO_NAT) - { - if (check && !n[0].getType(check).isBitVector()) - { - throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); - } - return nodeManager->integerType(); - } - - Assert(n.getKind() == kind::INT_TO_BITVECTOR); - size_t bvSize = n.getOperator().getConst(); - if (check && !n[0].getType(check).isInteger()) - { - throw TypeCheckingExceptionPrivate(n, "expecting integer term"); - } - return nodeManager->mkBitVectorType(bvSize); -} - TypeNode BitVectorEagerAtomTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 9c31c6590..d96287551 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -134,18 +134,6 @@ class BitVectorExtendTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -class IntToBitVectorOpTypeRule -{ - public: - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; - -class BitVectorConversionTypeRule -{ - public: - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; - /* -------------------------------------------------------------------------- */ /* internal */ /* -------------------------------------------------------------------------- */ diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 768233516..d3d76d208 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -461,58 +461,6 @@ Node flattenAnd(std::vector& queue) return mkAnd(children); } -/* ------------------------------------------------------------------------- */ - -Node eliminateBv2Nat(TNode node) -{ - const unsigned size = utils::getSize(node[0]); - NodeManager* const nm = NodeManager::currentNM(); - const Node z = nm->mkConstInt(Rational(0)); - const Node bvone = utils::mkOne(1); - - Integer i = 1; - std::vector children; - 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); - children.push_back( - nm->mkNode(kind::ITE, cond, nm->mkConstInt(Rational(i)), z)); - } - // avoid plus with one child - return children.size() == 1 ? children[0] : nm->mkNode(kind::ADD, children); -} - -Node eliminateInt2Bv(TNode node) -{ - const uint32_t size = node.getOperator().getConst().d_size; - NodeManager* const nm = NodeManager::currentNM(); - const Node bvzero = utils::mkZero(1); - const Node bvone = utils::mkOne(1); - - std::vector v; - Integer i = 2; - while (v.size() < size) - { - Node cond = nm->mkNode( - kind::GEQ, - nm->mkNode( - kind::INTS_MODULUS_TOTAL, node[0], nm->mkConstInt(Rational(i))), - nm->mkConstInt(Rational(i, 2))); - v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero)); - i *= 2; - } - if (v.size() == 1) - { - return v[0]; - } - NodeBuilder result(kind::BITVECTOR_CONCAT); - result.append(v.rbegin(), v.rend()); - return Node(result); -} - } // namespace utils } // namespace bv } // namespace theory diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 110493517..39bb61b40 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -204,25 +204,6 @@ Node flattenAnd(std::vector& queue); void intersect(const std::vector& v1, const std::vector& v2, std::vector& intersection); - -/** - * Returns the rewritten form of node, which is a term of the form bv2nat(x). - * The return value of this method is the integer sum: - * (+ ite( (= ((_ extract (n-1) (n-1)) x) 1) (^ 2 (n-1)) 0) - * ... - * ite( (= ((_ extract 0 0) x) 1) (^ 2 0) 0)) - * where n is the bitwidth of x. - */ -Node eliminateBv2Nat(TNode node); -/** - * Returns the rewritten form of node, which is a term of the form int2bv(x). - * The return value of this method is the concatenation term: - * (bvconcat ite( (>= (mod x (^ 2 n)) (^ 2 (n-1))) (_ bv1 1) (_ bv1 0)) - * ... - * ite( (>= (mod x (^ 2 1)) (^ 2 0)) (_ bv1 1) (_ bv1 0))) - * where n is the bit-width of x. - */ -Node eliminateInt2Bv(TNode node); } } }