From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 5 Apr 2019 19:01:33 +0000 (-0500)
Subject: fix fp issue (#2940)
X-Git-Tag: cvc5-1.0.0~4190
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=afc70ac962185b97e10f4e796f46c638ed1e18ab;p=cvc5.git

fix fp issue (#2940)
---

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index ee35f9e2a..2c93553fe 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -884,14 +884,20 @@ void TheoryFp::preRegisterTerm(TNode node)
   if (Configuration::isBuiltWithSymFPU() && !options::fpExp())
   {
     TypeNode tn = node.getType();
-    unsigned exp_sz = tn.getFloatingPointExponentSize();
-    unsigned sig_sz = tn.getFloatingPointSignificandSize();
-    if (!((exp_sz == 8 && sig_sz == 24) || (exp_sz == 11 && sig_sz == 53)))
+    if (tn.isFloatingPoint())
     {
-      std::stringstream ss;
-      ss << "FP types with sizes other than 8/24 or 11/53 are not supported in "
-            "default mode, try the experimental solver via --fp-exp";
-      throw LogicException(ss.str());
+      unsigned exp_sz = tn.getFloatingPointExponentSize();
+      unsigned sig_sz = tn.getFloatingPointSignificandSize();
+      if (!((exp_sz == 8 && sig_sz == 24) || (exp_sz == 11 && sig_sz == 53)))
+      {
+        std::stringstream ss;
+        ss << "FP term " << node << " with type whose size is " << exp_sz << "/"
+           << sig_sz
+           << " is not supported, only Float32 (8/24) or Float64 (11/53) types "
+              "are supported in default mode. Try the experimental solver via "
+              "--fp-exp";
+        throw LogicException(ss.str());
+      }
     }
   }
   Trace("fp-preRegisterTerm")
diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy
index cca2487d4..e8b97d610 100644
--- a/test/regress/regress1/rr-verify/fp-arith.sy
+++ b/test/regress/regress1/rr-verify/fp-arith.sy
@@ -1,5 +1,5 @@
 ; REQUIRES: symfpu
-; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1
diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
index 8792a594c..bf0692f7d 100644
--- a/test/regress/regress1/rr-verify/fp-bool.sy
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -1,5 +1,5 @@
 ; REQUIRES: symfpu
-; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1
diff --git a/test/regress/regress2/sygus/min_IC_1.sy b/test/regress/regress2/sygus/min_IC_1.sy
index 92e171312..a36a00019 100644
--- a/test/regress/regress2/sygus/min_IC_1.sy
+++ b/test/regress/regress2/sygus/min_IC_1.sy
@@ -1,6 +1,6 @@
 ; REQUIRES: symfpu
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --fp-exp
 (set-logic ALL)
 (define-sort FP () (_ FloatingPoint 3 5))
 (define-fun IC ((t FP)) Bool (=> (fp.isInfinite t) (fp.isNegative t)))
@@ -12,7 +12,7 @@
 
      (fp.isInfinite StartFP)
      (fp.isNegative StartFP)
-     
+
      (ite Start Start Start)
    ))
    (StartFP FP (