Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)

5 files changed, 32 insertions, 4 deletions

diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml
index eb8c933af..af8d044f7 100644
--- a/src/options/fp_options.toml
+++ b/src/options/fp_options.toml
@@ -1,3 +1,11 @@
 id     = "FP"
 name   = "Fp"
 header = "options/fp_options.h"
+
+[[option]]
+  name       = "fpExp"
+  category   = "regular"
+  long       = "fp-exp"
+  type       = "bool"
+  default    = "false"
+  help       = "Allow floating-point sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental)"
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 9dae2a5c3..ee35f9e2a 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -15,9 +15,12 @@
  ** \todo document this file
  **/
 
-#include "theory/fp/theory_fp.h"
+
+#include "options/fp_options.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/fp/theory_fp.h"
+
 
 #include <set>
 #include <stack>
@@ -306,7 +309,7 @@ Node TheoryFp::toRealUF(Node node) {
     std::vector<TypeNode> args(1);
     args[0] = t;
     fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case",
-		       nm->mkFunctionType(args, nm->realType()),
+                       nm->mkFunctionType(args, nm->realType()),
                        "floatingpoint_to_real_infinity_and_NaN_case",
                        NodeManager::SKOLEM_EXACT_NAME);
     d_toRealMap.insert(t, fun);
@@ -876,7 +879,21 @@ bool TheoryFp::isRegistered(TNode node) {
   return !(d_registeredTerms.find(node) == d_registeredTerms.end());
 }
 
-void TheoryFp::preRegisterTerm(TNode node) {
+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)))
+    {
+      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());
+    }
+  }
   Trace("fp-preRegisterTerm")
       << "TheoryFp::preRegisterTerm(): " << node << std::endl;
   registerTerm(node);
diff --git a/test/regress/regress0/fp/abs-unsound.smt2 b/test/regress/regress0/fp/abs-unsound.smt2
index 4ac53b830..b5aa0452e 100644
--- a/test/regress/regress0/fp/abs-unsound.smt2
+++ b/test/regress/regress0/fp/abs-unsound.smt2
@@ -1,4 +1,5 @@
 ; REQUIRES: symfpu
+; COMMAND-LINE: --fp-exp
 ; EXPECT: sat
 (set-logic QF_FP)
 (set-info :status sat)
diff --git a/test/regress/regress0/fp/abs-unsound2.smt2 b/test/regress/regress0/fp/abs-unsound2.smt2
index a6172b157..ad603f8c9 100644
--- a/test/regress/regress0/fp/abs-unsound2.smt2
+++ b/test/regress/regress0/fp/abs-unsound2.smt2
@@ -1,4 +1,5 @@
 ; REQUIRES: symfpu
+; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
 (set-logic QF_FP)
 (set-info :status unsat)
diff --git a/test/regress/regress0/fp/wrong-model.smt2 b/test/regress/regress0/fp/wrong-model.smt2
index 4bb7645d5..7694d8a35 100644
--- a/test/regress/regress0/fp/wrong-model.smt2
+++ b/test/regress/regress0/fp/wrong-model.smt2
@@ -1,10 +1,11 @@
 ; REQUIRES: symfpu
+; COMMAND-LINE: --fp-exp
 ; EXPECT: sat
 
 ; NOTE: the (set-logic ALL) is on purpose because the problem was not triggered
 ; with QF_FP.
 (set-logic ALL)
-(declare-const r RoundingMode) 
+(declare-const r RoundingMode)
 (declare-const x (_ FloatingPoint 5 11))
 (declare-const y (_ FloatingPoint 5 11))
 (assert (not (= (fp.isSubnormal x) false)))