FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)

This pushes all symfpu specific parts from FloatingPoint into
FloatingPointLiteral. FloatingPoint is now generic. An additional
FloatingPointLiteral implementation using MPFR will be made configurable
similiarly to how we handle Integers with either GMP or CLN backend.

2 files changed, 42 insertions, 36 deletions

diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index d4d47731d..3e03bbdbe 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -370,7 +370,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2)));
   }
@@ -383,7 +383,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.mult(rm, arg2)));
   }
@@ -397,8 +397,8 @@ namespace constantFold {
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
     FloatingPoint arg3(node[3].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
-    Assert(arg1.d_fp_size == arg3.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
+    Assert(arg1.getSize() == arg3.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.fma(rm, arg2, arg3)));
   }
@@ -411,7 +411,7 @@ namespace constantFold {
     FloatingPoint arg1(node[1].getConst<FloatingPoint>());
     FloatingPoint arg2(node[2].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.div(rm, arg2)));
   }
@@ -443,7 +443,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.rem(arg2)));
   }
@@ -455,7 +455,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     FloatingPoint::PartialFloatingPoint res(arg1.min(arg2));
 
@@ -475,7 +475,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     FloatingPoint::PartialFloatingPoint res(arg1.max(arg2));
 
@@ -495,7 +495,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     // Can be called with the third argument non-constant
     if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
@@ -525,7 +525,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     // Can be called with the third argument non-constant
     if (node[2].getMetaKind() == kind::metakind::CONSTANT) {
@@ -559,7 +559,7 @@ namespace constantFold {
       FloatingPoint arg1(node[0].getConst<FloatingPoint>());
       FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-      Assert(arg1.d_fp_size == arg2.d_fp_size);
+      Assert(arg1.getSize() == arg2.getSize());
 
       return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2));
 
@@ -581,7 +581,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 <= arg2));
   }
@@ -594,7 +594,7 @@ namespace constantFold {
     FloatingPoint arg1(node[0].getConst<FloatingPoint>());
     FloatingPoint arg2(node[1].getConst<FloatingPoint>());
 
-    Assert(arg1.d_fp_size == arg2.d_fp_size);
+    Assert(arg1.getSize() == arg2.getSize());
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 < arg2));
   }
@@ -657,8 +657,8 @@ namespace constantFold {
     const BitVector &bv = node[0].getConst<BitVector>();
 
     Node lit = NodeManager::currentNM()->mkConst(
-        FloatingPoint(param.d_fp_size.exponentWidth(),
-                      param.d_fp_size.significandWidth(),
+        FloatingPoint(param.getSize().exponentWidth(),
+                      param.getSize().significandWidth(),
                       bv));
 
     return RewriteResponse(REWRITE_DONE, lit);
@@ -674,7 +674,7 @@ namespace constantFold {
 
     return RewriteResponse(
         REWRITE_DONE,
-        NodeManager::currentNM()->mkConst(arg1.convert(info.d_fp_size, rm)));
+        NodeManager::currentNM()->mkConst(arg1.convert(info.getSize(), rm)));
   }
 
   RewriteResponse convertFromRealLiteral (TNode node, bool) {
@@ -686,7 +686,7 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     Rational arg(node[1].getConst<Rational>());
 
-    FloatingPoint res(param.d_fp_size, rm, arg);
+    FloatingPoint res(param.getSize(), rm, arg);
 
     Node lit = NodeManager::currentNM()->mkConst(res);
     
@@ -702,7 +702,7 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     BitVector arg(node[1].getConst<BitVector>());
 
-    FloatingPoint res(param.d_fp_size, rm, arg, true);
+    FloatingPoint res(param.getSize(), rm, arg, true);
 
     Node lit = NodeManager::currentNM()->mkConst(res);
     
@@ -718,7 +718,7 @@ namespace constantFold {
     RoundingMode rm(node[0].getConst<RoundingMode>());
     BitVector arg(node[1].getConst<BitVector>());
 
-    FloatingPoint res(param.d_fp_size, rm, arg, false);
+    FloatingPoint res(param.getSize(), rm, arg, false);
 
     Node lit = NodeManager::currentNM()->mkConst(res);
     
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 32c718654..ab193d7ba 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -42,18 +42,18 @@ class FloatingPointConstantTypeRule {
 
     if (check)
     {
-      if (!(validExponentSize(f.d_fp_size.exponentWidth())))
+      if (!(validExponentSize(f.getSize().exponentWidth())))
       {
         throw TypeCheckingExceptionPrivate(
             n, "constant with invalid exponent size");
       }
-      if (!(validSignificandSize(f.d_fp_size.significandWidth())))
+      if (!(validSignificandSize(f.getSize().significandWidth())))
       {
         throw TypeCheckingExceptionPrivate(
             n, "constant with invalid significand size");
       }
     }
-    return nodeManager->mkFloatingPointType(f.d_fp_size);
+    return nodeManager->mkFloatingPointType(f.getSize());
   }
 };
 
@@ -243,7 +243,8 @@ class FloatingPointParametricOpTypeRule {
   }
 };
 
-class FloatingPointToFPIEEEBitVectorTypeRule {
+class FloatingPointToFPIEEEBitVectorTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -264,8 +265,8 @@ class FloatingPointToFPIEEEBitVectorTypeRule {
                                            "than bit vector");
       }
       else if (!(operandType.getBitVectorSize()
-                 == info.d_fp_size.exponentWidth()
-                        + info.d_fp_size.significandWidth()))
+                 == info.getSize().exponentWidth()
+                        + info.getSize().significandWidth()))
       {
         throw TypeCheckingExceptionPrivate(
             n,
@@ -274,11 +275,12 @@ class FloatingPointToFPIEEEBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPFloatingPointTypeRule {
+class FloatingPointToFPFloatingPointTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -306,11 +308,12 @@ class FloatingPointToFPFloatingPointTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPRealTypeRule {
+class FloatingPointToFPRealTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -338,11 +341,12 @@ class FloatingPointToFPRealTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPSignedBitVectorTypeRule {
+class FloatingPointToFPSignedBitVectorTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -370,11 +374,12 @@ class FloatingPointToFPSignedBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPUnsignedBitVectorTypeRule {
+class FloatingPointToFPUnsignedBitVectorTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -402,11 +407,12 @@ class FloatingPointToFPUnsignedBitVectorTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };
 
-class FloatingPointToFPGenericTypeRule {
+class FloatingPointToFPGenericTypeRule
+{
  public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
@@ -427,7 +433,7 @@ class FloatingPointToFPGenericTypeRule {
       }
     }
 
-    return nodeManager->mkFloatingPointType(info.d_fp_size);
+    return nodeManager->mkFloatingPointType(info.getSize());
   }
 };