FP: Move type check from expandDefinitions. (#6479)

diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
index 34cc1ed5d573c4a17f2b0a05b4f989a5245b12f9..1fc893a3064f63ca61d7770fea66e7f1a09b83a1 100644 (file)
--- a/src/theory/fp/fp_expand_defs.cpp
+++ b/src/theory/fp/fp_expand_defs.cpp
@@ -40,37 +40,26 @@ Node removeToFPGeneric(TNode node)
     op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
     return nm->mkNode(op, node[0]);
   }
+  Assert(children == 2);
+  Assert(node[0].getType().isRoundingMode());
+
+  TypeNode t = node[1].getType();
+
+  if (t.isFloatingPoint())
+  {
+    op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
+  }
+  else if (t.isReal())
+  {
+    op = nm->mkConst(FloatingPointToFPReal(info));
+  }
   else
   {
-    Assert(children == 2);
-    Assert(node[0].getType().isRoundingMode());
-
-    TypeNode t = node[1].getType();
-
-    if (t.isFloatingPoint())
-    {
-      op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
-    }
-    else if (t.isReal())
-    {
-      op = nm->mkConst(FloatingPointToFPReal(info));
-    }
-    else if (t.isBitVector())
-    {
-      op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
-    }
-    else
-    {
-      throw TypeCheckingExceptionPrivate(
-          node,
-          "cannot rewrite to_fp generic due to incorrect type of second "
-          "argument");
-    }
-
-    return nm->mkNode(op, node[0], node[1]);
+    Assert(t.isBitVector());
+    op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
   }
 
-  Unreachable() << "to_fp generic not rewritten";
+  return nm->mkNode(op, node[0], node[1]);
 }
 }  // namespace removeToFPGeneric
 

diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp
index 6beba19ad3ba49b4d6bd0b620bd12654f5189b60..5951decd42e69e8176347e0db18bebd28bc7d50c 100644 (file)
--- a/src/theory/fp/theory_fp_type_rules.cpp
+++ b/src/theory/fp/theory_fp_type_rules.cpp
@@ -431,18 +431,31 @@ TypeNode FloatingPointToFPGenericTypeRule::computeType(NodeManager* nodeManager,
 
   if (check)
   {
-    /* As this is a generic kind intended only for parsing,
-     * the checking here is light.  For better checking, use
-     * expandDefinitions first.
-     */
-
-    size_t children = n.getNumChildren();
-    for (size_t i = 0; i < children; ++i)
+    uint32_t nchildren = n.getNumChildren();
+    if (nchildren == 1)
+    {
+      if (!n[0].getType(check).isBitVector())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "first argument must be a bit-vector");
+      }
+    }
+    else
     {
-      n[i].getType(check);
+      Assert(nchildren == 2);
+      if (!n[0].getType(check).isRoundingMode())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "first argument must be a roundingmode");
+      }
+      TypeNode tn = n[1].getType(check);
+      if (!tn.isBitVector() && !tn.isFloatingPoint() && !tn.isReal())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "second argument must be a bit-vector, floating-point or Real");
+      }
     }
   }
-
   return nodeManager->mkFloatingPointType(info.getSize());
 }