fix fp issue (#2940)

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index ee35f9e2a5d2f6703550862370d07aab75b0a565..2c93553fe6c5e8c1daa52c11e09fe5a0059f89b7 100644 (file)
--- 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 cca2487d4ea2e9eaed82570cd7fff5126b854a9d..e8b97d610cbe85d29dd9ce20716a356f5be38b6a 100644 (file)
--- 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 8792a594c10b22044b11d8b7474b371d1692dfa9..bf0692f7dde0243019bd7ba9c902c26ed538fd61 100644 (file)
--- 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 92e171312303682cfabf1d931b4f47137693fe5c..a36a000191976761c51dc26975a3d3f2d010f098 100644 (file)
--- 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 (