operator FLOATINGPOINT_MAX 2 "floating-point maximum"
typerule FLOATINGPOINT_MAX ::CVC4::theory::fp::FloatingPointOperationTypeRule
+operator FLOATINGPOINT_MIN_TOTAL 3 "floating-point minimum (defined for all inputs)"
+typerule FLOATINGPOINT_MIN_TOTAL ::CVC4::theory::fp::FloatingPointPartialOperationTypeRule
+
+operator FLOATINGPOINT_MAX_TOTAL 3 "floating-point maximum (defined for all inputs)"
+typerule FLOATINGPOINT_MAX_TOTAL ::CVC4::theory::fp::FloatingPointPartialOperationTypeRule
+
operator FLOATINGPOINT_LEQ 2: "floating-point less than or equal"
typerule FLOATINGPOINT_LEQ ::CVC4::theory::fp::FloatingPointTestTypeRule
typerule FLOATINGPOINT_TO_UBV ::CVC4::theory::fp::FloatingPointToUBVTypeRule
+constant FLOATINGPOINT_TO_UBV_TOTAL_OP \
+ ::CVC4::FloatingPointToUBVTotal \
+ "::CVC4::FloatingPointToBVHashFunction<0x4>" \
+ "util/floatingpoint.h" \
+ "operator for to_ubv_total"
+typerule FLOATINGPOINT_TO_UBV_TOTAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_UBV_TOTAL FLOATINGPOINT_TO_UBV_TOTAL_OP 3 "convert a floating-point value to an unsigned bit vector (defined for all inputs)"
+typerule FLOATINGPOINT_TO_UBV_TOTAL ::CVC4::theory::fp::FloatingPointToUBVTotalTypeRule
+
+
constant FLOATINGPOINT_TO_SBV_OP \
::CVC4::FloatingPointToSBV \
typerule FLOATINGPOINT_TO_SBV ::CVC4::theory::fp::FloatingPointToSBVTypeRule
+constant FLOATINGPOINT_TO_SBV_TOTAL_OP \
+ ::CVC4::FloatingPointToSBVTotal \
+ "::CVC4::FloatingPointToBVHashFunction<0x8>" \
+ "util/floatingpoint.h" \
+ "operator for to_sbv_total"
+typerule FLOATINGPOINT_TO_SBV_TOTAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_SBV_TOTAL FLOATINGPOINT_TO_SBV_TOTAL_OP 3 "convert a floating-point value to a signed bit vector (defined for all inputs)"
+typerule FLOATINGPOINT_TO_SBV_TOTAL ::CVC4::theory::fp::FloatingPointToSBVTotalTypeRule
+
+
operator FLOATINGPOINT_TO_REAL 1 "floating-point to real"
typerule FLOATINGPOINT_TO_REAL ::CVC4::theory::fp::FloatingPointToRealTypeRule
+operator FLOATINGPOINT_TO_REAL_TOTAL 2 "floating-point to real (defined for all inputs)"
+typerule FLOATINGPOINT_TO_REAL_TOTAL ::CVC4::theory::fp::FloatingPointToRealTotalTypeRule
+
endtheory
RewriteResponse compactMinMax (TNode node, bool isPreRewrite) {
#ifdef CVC4_ASSERTIONS
Kind k = node.getKind();
- Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX));
+ Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX) ||
+ (k == kind::FLOATINGPOINT_MIN_TOTAL) || (k == kind::FLOATINGPOINT_MAX_TOTAL));
#endif
if (node[0] == node[1]) {
return RewriteResponse(REWRITE_DONE, node[0]);
}
}
+ RewriteResponse minTotal (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL);
+ Assert(node.getNumChildren() == 3);
+
+ FloatingPoint arg1(node[0].getConst<FloatingPoint>());
+ FloatingPoint arg2(node[1].getConst<FloatingPoint>());
+
+ Assert(arg1.t == arg2.t);
+
+ // Can be called with the third argument non-constant
+ if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
+ BitVector arg3(node[2].getConst<BitVector>());
+
+ FloatingPoint folded(arg1.minTotal(arg2, arg3.isBitSet(0)));
+ Node lit = NodeManager::currentNM()->mkConst(folded);
+ return RewriteResponse(REWRITE_DONE, lit);
+
+ } else {
+ FloatingPoint::PartialFloatingPoint res(arg1.min(arg2));
+
+ if (res.second) {
+ Node lit = NodeManager::currentNM()->mkConst(res.first);
+ return RewriteResponse(REWRITE_DONE, lit);
+ } else {
+ // Can't constant fold the underspecified case
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+ }
+
+ RewriteResponse maxTotal (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL);
+ Assert(node.getNumChildren() == 3);
+
+ FloatingPoint arg1(node[0].getConst<FloatingPoint>());
+ FloatingPoint arg2(node[1].getConst<FloatingPoint>());
+
+ Assert(arg1.t == arg2.t);
+
+ // Can be called with the third argument non-constant
+ if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
+ BitVector arg3(node[2].getConst<BitVector>());
+
+ FloatingPoint folded(arg1.maxTotal(arg2, arg3.isBitSet(0)));
+ Node lit = NodeManager::currentNM()->mkConst(folded);
+ return RewriteResponse(REWRITE_DONE, lit);
+
+ } else {
+ FloatingPoint::PartialFloatingPoint res(arg1.max(arg2));
+
+ if (res.second) {
+ Node lit = NodeManager::currentNM()->mkConst(res.first);
+ return RewriteResponse(REWRITE_DONE, lit);
+ } else {
+ // Can't constant fold the underspecified case
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+ }
+
RewriteResponse equal (TNode node, bool isPreRewrite) {
Assert(node.getKind() == kind::EQUAL);
}
}
+ RewriteResponse convertToUBVTotal (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL);
+
+ TNode op = node.getOperator();
+ const FloatingPointToUBVTotal ¶m = op.getConst<FloatingPointToUBVTotal>();
+
+ RoundingMode rm(node[0].getConst<RoundingMode>());
+ FloatingPoint arg(node[1].getConst<FloatingPoint>());
+
+ // Can be called with the third argument non-constant
+ if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
+ BitVector partialValue(node[2].getConst<BitVector>());
+
+ BitVector folded(arg.convertToBVTotal(param.bvs, rm, false, partialValue));
+ Node lit = NodeManager::currentNM()->mkConst(folded);
+ return RewriteResponse(REWRITE_DONE, lit);
+
+ } else {
+ FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, false));
+
+ if (res.second) {
+ Node lit = NodeManager::currentNM()->mkConst(res.first);
+ return RewriteResponse(REWRITE_DONE, lit);
+ } else {
+ // Can't constant fold the underspecified case
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+ }
+
+ RewriteResponse convertToSBVTotal (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL);
+
+ TNode op = node.getOperator();
+ const FloatingPointToSBVTotal ¶m = op.getConst<FloatingPointToSBVTotal>();
+
+ RoundingMode rm(node[0].getConst<RoundingMode>());
+ FloatingPoint arg(node[1].getConst<FloatingPoint>());
+
+ // Can be called with the third argument non-constant
+ if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
+ BitVector partialValue(node[2].getConst<BitVector>());
+
+ BitVector folded(arg.convertToBVTotal(param.bvs, rm, true, partialValue));
+ Node lit = NodeManager::currentNM()->mkConst(folded);
+ return RewriteResponse(REWRITE_DONE, lit);
+
+ } else {
+
+ FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, true));
+
+ if (res.second) {
+ Node lit = NodeManager::currentNM()->mkConst(res.first);
+ return RewriteResponse(REWRITE_DONE, lit);
+ } else {
+ // Can't constant fold the underspecified case
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+ }
+
+ RewriteResponse convertToRealTotal (TNode node, bool) {
+ Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL);
+
+ FloatingPoint arg(node[0].getConst<FloatingPoint>());
+
+ // Can be called with the third argument non-constant
+ if (node[1].getMetaKind() == kind::metakind::CONSTANT) {
+ Rational partialValue(node[1].getConst<Rational>());
+
+ Rational folded(arg.convertToRationalTotal(partialValue));
+ Node lit = NodeManager::currentNM()->mkConst(folded);
+ return RewriteResponse(REWRITE_DONE, lit);
+
+ } else {
+ FloatingPoint::PartialRational res(arg.convertToRational());
+
+ if (res.second) {
+ Node lit = NodeManager::currentNM()->mkConst(res.first);
+ return RewriteResponse(REWRITE_DONE, lit);
+ } else {
+ // Can't constant fold the underspecified case
+ return RewriteResponse(REWRITE_DONE, node);
+ }
+ }
+ }
+
+
}; /* CVC4::theory::fp::constantFold */
preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+ preRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
+ preRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
/******** Comparisons ********/
preRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::then<rewrite::breakChain,rewrite::ieeeEqToEq>;
preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
+ preRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
/******** Variables ********/
preRewriteTable[kind::VARIABLE] = rewrite::variable;
postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+ postRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax;
+ postRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax;
/******** Comparisons ********/
postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::removed;
postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity;
+ postRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity;
/******** Variables ********/
postRewriteTable[kind::VARIABLE] = rewrite::variable;
constantFoldTable[kind::FLOATINGPOINT_RTI] = constantFold::rti;
constantFoldTable[kind::FLOATINGPOINT_MIN] = constantFold::min;
constantFoldTable[kind::FLOATINGPOINT_MAX] = constantFold::max;
+ constantFoldTable[kind::FLOATINGPOINT_MIN_TOTAL] = constantFold::minTotal;
+ constantFoldTable[kind::FLOATINGPOINT_MAX_TOTAL] = constantFold::maxTotal;
/******** Comparisons ********/
constantFoldTable[kind::FLOATINGPOINT_EQ] = rewrite::removed;
constantFoldTable[kind::FLOATINGPOINT_TO_UBV] = constantFold::convertToUBV;
constantFoldTable[kind::FLOATINGPOINT_TO_SBV] = constantFold::convertToSBV;
constantFoldTable[kind::FLOATINGPOINT_TO_REAL] = constantFold::convertToReal;
+ constantFoldTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = constantFold::convertToUBVTotal;
+ constantFoldTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = constantFold::convertToSBVTotal;
+ constantFoldTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = constantFold::convertToRealTotal;
/******** Variables ********/
constantFoldTable[kind::VARIABLE] = rewrite::variable;
if (res.status == REWRITE_DONE) {
bool allChildrenConst = true;
bool apartFromRoundingMode = false;
+ bool apartFromPartiallyDefinedArgument = false;
for (Node::const_iterator i = res.node.begin();
i != res.node.end();
++i) {
if ((*i).getMetaKind() != kind::metakind::CONSTANT) {
if ((*i).getType().isRoundingMode() && !apartFromRoundingMode) {
apartFromRoundingMode = true;
+ } else if ((res.node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL ||
+ res.node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL ||
+ res.node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL ||
+ res.node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL ||
+ res.node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL) &&
+ ((*i).getType().isBitVector() ||
+ (*i).getType().isReal()) &&
+ !apartFromPartiallyDefinedArgument) {
+ apartFromPartiallyDefinedArgument = true;
} else {
allChildrenConst = false;
break;
}
};
+class FloatingPointPartialOperationTypeRule {
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+ bool check) {
+ TRACE("FloatingPointOperationTypeRule");
+
+ TypeNode firstOperand = n[0].getType(check);
+
+ if (check) {
+ if (!firstOperand.isFloatingPoint()) {
+ throw TypeCheckingExceptionPrivate(
+ n, "floating-point operation applied to a non floating-point sort");
+ }
+
+ size_t children = n.getNumChildren();
+ for (size_t i = 1; i < children - 1; ++i) {
+ if (!(n[i].getType(check) == firstOperand)) {
+ throw TypeCheckingExceptionPrivate(
+ n, "floating-point partial operation applied to mixed sorts");
+ }
+ }
+
+ TypeNode UFValueType = n[children - 1].getType(check);
+
+ if (!(UFValueType.isBitVector()) ||
+ !(UFValueType.getBitVectorSize() == 1)) {
+ throw TypeCheckingExceptionPrivate(
+ n, "floating-point partial operation final argument must be a bit-vector of length 1");
+ }
+ }
+
+ return firstOperand;
+ }
+};
+
+
class FloatingPointParametricOpTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
}
};
+class FloatingPointToUBVTotalTypeRule {
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+ bool check) {
+ TRACE("FloatingPointToUBVTotalTypeRule");
+
+ FloatingPointToUBVTotal info = n.getOperator().getConst<FloatingPointToUBVTotal>();
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(
+ n, "first argument must be a rounding mode");
+ }
+
+ TypeNode operandType = n[1].getType(check);
+
+ if (!(operandType.isFloatingPoint())) {
+ throw TypeCheckingExceptionPrivate(n,
+ "conversion to unsigned bit vector total"
+ "used with a sort other than "
+ "floating-point");
+ }
+
+ TypeNode defaultValueType = n[2].getType(check);
+
+ if (!(defaultValueType.isBitVector()) ||
+ !(defaultValueType.getBitVectorSize() == info)) {
+ throw TypeCheckingExceptionPrivate(n,
+ "conversion to unsigned bit vector total"
+ "needs a bit vector of the same length"
+ "as last argument");
+ }
+ }
+
+ return nodeManager->mkBitVectorType(info.bvs);
+ }
+};
+
+class FloatingPointToSBVTotalTypeRule {
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+ bool check) {
+ TRACE("FloatingPointToSBVTotalTypeRule");
+
+ FloatingPointToSBVTotal info = n.getOperator().getConst<FloatingPointToSBVTotal>();
+
+ if (check) {
+ TypeNode roundingModeType = n[0].getType(check);
+
+ if (!roundingModeType.isRoundingMode()) {
+ throw TypeCheckingExceptionPrivate(
+ n, "first argument must be a rounding mode");
+ }
+
+ TypeNode operandType = n[1].getType(check);
+
+ if (!(operandType.isFloatingPoint())) {
+ throw TypeCheckingExceptionPrivate(n,
+ "conversion to signed bit vector "
+ "used with a sort other than "
+ "floating-point");
+ }
+
+ TypeNode defaultValueType = n[2].getType(check);
+
+ if (!(defaultValueType.isBitVector()) ||
+ !(defaultValueType.getBitVectorSize() == info)) {
+ throw TypeCheckingExceptionPrivate(n,
+ "conversion to signed bit vector total"
+ "needs a bit vector of the same length"
+ "as last argument");
+ }
+ }
+
+ return nodeManager->mkBitVectorType(info.bvs);
+ }
+};
+
class FloatingPointToRealTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
}
};
+class FloatingPointToRealTotalTypeRule {
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+ bool check) {
+ TRACE("FloatingPointToRealTotalTypeRule");
+
+ if (check) {
+ TypeNode operandType = n[0].getType(check);
+
+ if (!operandType.isFloatingPoint()) {
+ throw TypeCheckingExceptionPrivate(
+ n, "floating-point to real total applied to a non floating-point sort");
+ }
+
+ TypeNode defaultValueType = n[1].getType(check);
+
+ if (!defaultValueType.isReal()) {
+ throw TypeCheckingExceptionPrivate(
+ n, "floating-point to real total needs a real second argument");
+ }
+
+ }
+
+ return nodeManager->realType();
+ }
+};
+
class CardinalityComputer {
public:
projects / cvc5.git / commitdiff