summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/fp/fp_converter.cpp4
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp73
-rw-r--r--src/theory/fp/theory_fp_type_rules.h49
3 files changed, 70 insertions, 56 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 47a4af43e..0d088fe41 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -1578,7 +1578,7 @@ Node FpConverter::convert(TNode node)
symfpu::convertFloatToUBV<traits>(fpt(childType),
(*mode).second,
(*arg1).second,
- info.bvs,
+ info.d_bv_size,
ubv(current[2])));
i = d_ubvMap.find(current);
}
@@ -1620,7 +1620,7 @@ Node FpConverter::convert(TNode node)
symfpu::convertFloatToSBV<traits>(fpt(childType),
(*mode).second,
(*arg1).second,
- info.bvs,
+ info.d_bv_size,
sbv(current[2])));
i = d_sbvMap.find(current);
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 120f71b6d..49b4e85c5 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -369,7 +369,7 @@ namespace constantFold {
FloatingPoint arg1(node[1].getConst<FloatingPoint>());
FloatingPoint arg2(node[2].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2)));
}
@@ -382,7 +382,7 @@ namespace constantFold {
FloatingPoint arg1(node[1].getConst<FloatingPoint>());
FloatingPoint arg2(node[2].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.mult(rm, arg2)));
}
@@ -396,8 +396,8 @@ namespace constantFold {
FloatingPoint arg2(node[2].getConst<FloatingPoint>());
FloatingPoint arg3(node[3].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
- Assert(arg1.t == arg3.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
+ Assert(arg1.d_fp_size == arg3.d_fp_size);
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.fma(rm, arg2, arg3)));
}
@@ -410,7 +410,7 @@ namespace constantFold {
FloatingPoint arg1(node[1].getConst<FloatingPoint>());
FloatingPoint arg2(node[2].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.div(rm, arg2)));
}
@@ -442,7 +442,7 @@ namespace constantFold {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.rem(arg2)));
}
@@ -454,7 +454,7 @@ namespace constantFold {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
FloatingPoint::PartialFloatingPoint res(arg1.min(arg2));
@@ -474,7 +474,7 @@ namespace constantFold {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
FloatingPoint::PartialFloatingPoint res(arg1.max(arg2));
@@ -494,7 +494,7 @@ namespace constantFold {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
// Can be called with the third argument non-constant
if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
@@ -524,7 +524,7 @@ namespace constantFold {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
// Can be called with the third argument non-constant
if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
@@ -558,7 +558,7 @@ namespace constantFold {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2));
@@ -580,7 +580,7 @@ namespace constantFold {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 <= arg2));
}
@@ -593,7 +593,7 @@ namespace constantFold {
FloatingPoint arg1(node[0].getConst<FloatingPoint>());
FloatingPoint arg2(node[1].getConst<FloatingPoint>());
- Assert(arg1.t == arg2.t);
+ Assert(arg1.d_fp_size == arg2.d_fp_size);
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 < arg2));
}
@@ -654,12 +654,12 @@ namespace constantFold {
TNode op = node.getOperator();
const FloatingPointToFPIEEEBitVector &param = op.getConst<FloatingPointToFPIEEEBitVector>();
const BitVector &bv = node[0].getConst<BitVector>();
-
- Node lit =
- NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(),
- param.t.significand(),
- bv));
-
+
+ Node lit = NodeManager::currentNM()->mkConst(
+ FloatingPoint(param.d_fp_size.exponentWidth(),
+ param.d_fp_size.significandWidth(),
+ bv));
+
return RewriteResponse(REWRITE_DONE, lit);
}
@@ -671,7 +671,9 @@ namespace constantFold {
FloatingPoint arg1(node[1].getConst<FloatingPoint>());
FloatingPointToFPFloatingPoint info = node.getOperator().getConst<FloatingPointToFPFloatingPoint>();
- return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.convert(info.t,rm)));
+ return RewriteResponse(
+ REWRITE_DONE,
+ NodeManager::currentNM()->mkConst(arg1.convert(info.d_fp_size, rm)));
}
RewriteResponse convertFromRealLiteral (TNode node, bool) {
@@ -683,8 +685,8 @@ namespace constantFold {
RoundingMode rm(node[0].getConst<RoundingMode>());
Rational arg(node[1].getConst<Rational>());
- FloatingPoint res(param.t, rm, arg);
-
+ FloatingPoint res(param.d_fp_size, rm, arg);
+
Node lit = NodeManager::currentNM()->mkConst(res);
return RewriteResponse(REWRITE_DONE, lit);
@@ -699,8 +701,8 @@ namespace constantFold {
RoundingMode rm(node[0].getConst<RoundingMode>());
BitVector arg(node[1].getConst<BitVector>());
- FloatingPoint res(param.t, rm, arg, true);
-
+ FloatingPoint res(param.d_fp_size, rm, arg, true);
+
Node lit = NodeManager::currentNM()->mkConst(res);
return RewriteResponse(REWRITE_DONE, lit);
@@ -715,8 +717,8 @@ namespace constantFold {
RoundingMode rm(node[0].getConst<RoundingMode>());
BitVector arg(node[1].getConst<BitVector>());
- FloatingPoint res(param.t, rm, arg, false);
-
+ FloatingPoint res(param.d_fp_size, rm, arg, false);
+
Node lit = NodeManager::currentNM()->mkConst(res);
return RewriteResponse(REWRITE_DONE, lit);
@@ -731,7 +733,8 @@ namespace constantFold {
RoundingMode rm(node[0].getConst<RoundingMode>());
FloatingPoint arg(node[1].getConst<FloatingPoint>());
- FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, false));
+ FloatingPoint::PartialBitVector res(
+ arg.convertToBV(param.d_bv_size, rm, false));
if (res.second) {
Node lit = NodeManager::currentNM()->mkConst(res.first);
@@ -751,7 +754,8 @@ namespace constantFold {
RoundingMode rm(node[0].getConst<RoundingMode>());
FloatingPoint arg(node[1].getConst<FloatingPoint>());
- FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, true));
+ FloatingPoint::PartialBitVector res(
+ arg.convertToBV(param.d_bv_size, rm, true));
if (res.second) {
Node lit = NodeManager::currentNM()->mkConst(res.first);
@@ -791,12 +795,14 @@ namespace constantFold {
if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
BitVector partialValue(node[2].getConst<BitVector>());
- BitVector folded(arg.convertToBVTotal(param.bvs, rm, false, partialValue));
+ BitVector folded(
+ arg.convertToBVTotal(param.d_bv_size, rm, false, partialValue));
Node lit = NodeManager::currentNM()->mkConst(folded);
return RewriteResponse(REWRITE_DONE, lit);
} else {
- FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, false));
+ FloatingPoint::PartialBitVector res(
+ arg.convertToBV(param.d_bv_size, rm, false));
if (res.second) {
Node lit = NodeManager::currentNM()->mkConst(res.first);
@@ -821,13 +827,14 @@ namespace constantFold {
if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
BitVector partialValue(node[2].getConst<BitVector>());
- BitVector folded(arg.convertToBVTotal(param.bvs, rm, true, partialValue));
+ BitVector folded(
+ arg.convertToBVTotal(param.d_bv_size, rm, true, partialValue));
Node lit = NodeManager::currentNM()->mkConst(folded);
return RewriteResponse(REWRITE_DONE, lit);
} else {
-
- FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, true));
+ FloatingPoint::PartialBitVector res(
+ arg.convertToBV(param.d_bv_size, rm, true));
if (res.second) {
Node lit = NodeManager::currentNM()->mkConst(res.first);
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index bff909a39..4d4f3c660 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -39,17 +39,20 @@ class FloatingPointConstantTypeRule {
const FloatingPoint& f = n.getConst<FloatingPoint>();
- if (check) {
- if (!(validExponentSize(f.t.exponent()))) {
+ if (check)
+ {
+ if (!(validExponentSize(f.d_fp_size.exponentWidth())))
+ {
throw TypeCheckingExceptionPrivate(
n, "constant with invalid exponent size");
}
- if (!(validSignificandSize(f.t.significand()))) {
+ if (!(validSignificandSize(f.d_fp_size.significandWidth())))
+ {
throw TypeCheckingExceptionPrivate(
n, "constant with invalid significand size");
}
}
- return nodeManager->mkFloatingPointType(f.t);
+ return nodeManager->mkFloatingPointType(f.d_fp_size);
}
};
@@ -252,13 +255,17 @@ class FloatingPointToFPIEEEBitVectorTypeRule {
if (check) {
TypeNode operandType = n[0].getType(check);
- if (!(operandType.isBitVector())) {
+ if (!(operandType.isBitVector()))
+ {
throw TypeCheckingExceptionPrivate(n,
"conversion to floating-point from "
"bit vector used with sort other "
"than bit vector");
- } else if (!(operandType.getBitVectorSize() ==
- info.t.exponent() + info.t.significand())) {
+ }
+ else if (!(operandType.getBitVectorSize()
+ == info.d_fp_size.exponentWidth()
+ + info.d_fp_size.significandWidth()))
+ {
throw TypeCheckingExceptionPrivate(
n,
"conversion to floating-point from bit vector used with bit vector "
@@ -266,7 +273,7 @@ class FloatingPointToFPIEEEBitVectorTypeRule {
}
}
- return nodeManager->mkFloatingPointType(info.t);
+ return nodeManager->mkFloatingPointType(info.d_fp_size);
}
};
@@ -298,7 +305,7 @@ class FloatingPointToFPFloatingPointTypeRule {
}
}
- return nodeManager->mkFloatingPointType(info.t);
+ return nodeManager->mkFloatingPointType(info.d_fp_size);
}
};
@@ -330,7 +337,7 @@ class FloatingPointToFPRealTypeRule {
}
}
- return nodeManager->mkFloatingPointType(info.t);
+ return nodeManager->mkFloatingPointType(info.d_fp_size);
}
};
@@ -362,7 +369,7 @@ class FloatingPointToFPSignedBitVectorTypeRule {
}
}
- return nodeManager->mkFloatingPointType(info.t);
+ return nodeManager->mkFloatingPointType(info.d_fp_size);
}
};
@@ -394,7 +401,7 @@ class FloatingPointToFPUnsignedBitVectorTypeRule {
}
}
- return nodeManager->mkFloatingPointType(info.t);
+ return nodeManager->mkFloatingPointType(info.d_fp_size);
}
};
@@ -419,7 +426,7 @@ class FloatingPointToFPGenericTypeRule {
}
}
- return nodeManager->mkFloatingPointType(info.t);
+ return nodeManager->mkFloatingPointType(info.d_fp_size);
}
};
@@ -450,7 +457,7 @@ class FloatingPointToUBVTypeRule {
}
}
- return nodeManager->mkBitVectorType(info.bvs);
+ return nodeManager->mkBitVectorType(info.d_bv_size);
}
};
@@ -481,7 +488,7 @@ class FloatingPointToSBVTypeRule {
}
}
- return nodeManager->mkBitVectorType(info.bvs);
+ return nodeManager->mkBitVectorType(info.d_bv_size);
}
};
@@ -522,7 +529,7 @@ class FloatingPointToUBVTotalTypeRule {
}
}
- return nodeManager->mkBitVectorType(info.bvs);
+ return nodeManager->mkBitVectorType(info.d_bv_size);
}
};
@@ -563,7 +570,7 @@ class FloatingPointToSBVTotalTypeRule {
}
}
- return nodeManager->mkBitVectorType(info.bvs);
+ return nodeManager->mkBitVectorType(info.d_bv_size);
}
};
@@ -686,7 +693,7 @@ class FloatingPointComponentExponent
* Here we use types from floatingpoint.h which are the literal
* back-end but it should't make a difference. */
FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
- symfpuLiteral::fpt format(fps); // The symfpu interface to type info
+ symfpuLiteral::CVC4FPSize format(fps); // The symfpu interface to type info
unsigned bw = FloatingPointLiteral::exponentWidth(format);
#else
unsigned bw = 2;
@@ -729,7 +736,7 @@ class FloatingPointComponentSignificand
#ifdef CVC4_USE_SYMFPU
/* As before we need to use some of sympfu. */
FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
- symfpuLiteral::fpt format(fps);
+ symfpuLiteral::CVC4FPSize format(fps);
unsigned bw = FloatingPointLiteral::significandWidth(format);
#else
unsigned bw = 1;
@@ -791,8 +798,8 @@ public:
* = 5 + ((2^e)-1)*2^s
*/
- Integer significandValues = Integer(2).pow(fps.significand());
- Integer exponentValues = Integer(2).pow(fps.exponent());
+ Integer significandValues = Integer(2).pow(fps.significandWidth());
+ Integer exponentValues = Integer(2).pow(fps.exponentWidth());
exponentValues -= Integer(1);
return Integer(5) + exponentValues * significandValues;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback