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.
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:
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();
}
}
}
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
/** 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 */
#include <cmath>
+#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+
using namespace cvc5::internal::kind;
namespace cvc5::internal {
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<Node> 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<IntToBitVector>().d_size;
+ NodeManager* const nm = NodeManager::currentNM();
+ const Node bvzero = bv::utils::mkZero(1);
+ const Node bvone = bv::utils::mkOne(1);
+
+ 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->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
*/
std::pair<Node,Node> 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
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
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:
}
}
-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);
}
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:
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
}
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()); }
return var;
}
+ case BITVECTOR_TO_NAT: return eliminateBv2Nat(node); break;
+ case INT_TO_BITVECTOR: return eliminateInt2Bv(node); break;
default: break;
}
return node;
#include "theory/arith/theory_arith_type_rules.h"
+#include "util/bitvector.h"
#include "util/rational.h"
namespace cvc5::internal {
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<IntToBitVector>();
+ 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<IntToBitVector>();
+ if (check && !n[0].getType(check).isInteger())
+ {
+ throw TypeCheckingExceptionPrivate(n, "expecting integer term");
+ }
+ return nodeManager->mkBitVectorType(bvSize);
+}
+
} // namespace arith
} // namespace theory
} // namespace cvc5::internal
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
## 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)"
"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
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
typerule BITVECTOR_SIGN_EXTEND ::cvc5::internal::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
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
return result;
}
-template <>
-inline bool RewriteRule<BVToNatEliminate>::applies(TNode node)
-{
- return (node.getKind() == kind::BITVECTOR_TO_NAT);
-}
-
-template <>
-inline Node RewriteRule<BVToNatEliminate>::apply(TNode node)
-{
- Trace("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl;
-
- //if( node[0].isConst() ){
- //TODO? direct computation instead of term construction+rewriting
- //}
- return utils::eliminateBv2Nat(node);
-}
-
-template <>
-inline bool RewriteRule<IntToBVEliminate>::applies(TNode node)
-{
- return (node.getKind() == kind::INT_TO_BITVECTOR);
-}
-
-template <>
-inline Node RewriteRule<IntToBVEliminate>::apply(TNode node)
-{
- Trace("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl;
-
- //if( node[0].isConst() ){
- //TODO? direct computation instead of term construction+rewriting
- //}
- return utils::eliminateInt2Bv(node);
-}
-
template <>
inline bool RewriteRule<NandEliminate>::applies(TNode 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)
return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
}
-RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
- if (node[0].isConst())
- {
- Node resultNode = LinearRewriteStrategy
- < RewriteRule<BVToNatEliminate>
- >::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<IntToBVEliminate>
- >::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
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) {
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<IntToBitVector>();
- 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<IntToBitVector>();
- 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)
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 */
/* -------------------------------------------------------------------------- */
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<Node> 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<IntToBitVector>().d_size;
- NodeManager* const nm = NodeManager::currentNM();
- const Node bvzero = utils::mkZero(1);
- const Node bvone = utils::mkOne(1);
-
- 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->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
void intersect(const std::vector<uint32_t>& v1,
const std::vector<uint32_t>& v2,
std::vector<uint32_t>& 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);
}
}
}
projects / cvc5.git / commitdiff