update

7 files changed, 113 insertions, 2 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2e5252529..6ee7dc7c5 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1347,6 +1347,14 @@ header = "options/quantifiers_options.h"
   type       = "unsigned long"
   help       = "timeout (in milliseconds) for satisfiability checks in expression miners"
 
+[[option]]
+  name       = "sygusExprMinerCheckUseExport"
+  category   = "expert"
+  long       = "sygus-expr-miner-check-use-export"
+  type       = "bool"
+  default    = "true"
+  help       = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners"
+
 # CEGQI applied to general quantified formulas
 
 [[option]]
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0a4859971..b1d6df852 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2182,6 +2182,22 @@ void SmtEngine::setDefaults() {
         << endl;
     options::bvLazyRewriteExtf.set(false);
   }
+
+  if (!options::sygusExprMinerCheckUseExport())
+  {
+    if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+    {
+      throw OptionException(
+          "--sygus-expr-miner-check-timeout=N requires "
+          "--sygus-expr-miner-check-use-export");
+    }
+    if (options::sygusRewSynthInput())
+    {
+      throw OptionException(
+          "--sygus-rr-synth-input requires "
+          "--sygus-expr-miner-check-use-export");
+    }
+  }
 }
 
 void SmtEngine::setProblemExtended(bool value)
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index ddf377508..16e59c119 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -77,8 +77,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   // check is ground.
   Node squery = convertToSkolem(query);
   NodeManager* nm = NodeManager::currentNM();
-  if (options::sygusExprMinerCheckTimeout.wasSetByUser()
-      || options::sygusRewSynthInput())
+  if (options::sygusExprMinerCheckUseExport())
   {
     // To support a separate timeout for the subsolver, we need to create
     // a separate ExprManager with its own options. This requires that
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 902ddf0f9..139613ab6 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1409,6 +1409,7 @@ set(regress_1_tests
   regress1/rewriterules/length_gen_040_lemma_trigger.smt2
   regress1/rewriterules/reachability_back_to_the_future.smt2
   regress1/rewriterules/read5.smt2
+	regress1/rr-verify/fp-bool.sy
   regress1/rr-verify/bool-crci.sy
   regress1/rr-verify/bv-term-32.sy
   regress1/rr-verify/bv-term.sy
@@ -1660,6 +1661,7 @@ set(regress_1_tests
 # Regression level 2 tests
 
 set(regress_2_tests
+	regress2/rr-verify/fp-arith.sy
   regress2/DTP_k2_n35_c175_s15.smt2
   regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2
   regress2/GEO123+1.minimized.smt2
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 91f33721a..ab82042eb 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1409,6 +1409,7 @@ REG1_TESTS = \
 	regress1/rr-verify/bool-crci.sy \
 	regress1/rr-verify/bv-term-32.sy \
 	regress1/rr-verify/bv-term.sy \
+	regress1/rr-verify/fp-bool.sy \
 	regress1/rr-verify/regex.sy \
 	regress1/rr-verify/string-term.sy \
 	regress1/sep/chain-int.smt2 \
@@ -1699,6 +1700,7 @@ REG2_TESTS = \
 	regress2/quantifiers/mutualrec2.cvc \
 	regress2/quantifiers/net-policy-no-time.smt2 \
 	regress2/quantifiers/nunchaku2309663.nun.min.smt2 \
+	regress2/rr-verify/fp-arith.sy \
 	regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \
 	regress2/strings/cmu-dis-0707-3.smt2 \
 	regress2/strings/cmu-disagree-0707-dd.smt2 \
diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
new file mode 100644
index 000000000..9096a57b8
--- /dev/null
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -0,0 +1,50 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic FP)
+
+(define-fun fp_plus_zero () Float16 (_ +zero 5 11))
+(define-fun fp_minus_zero () Float16 (_ -zero 5 11))
+(define-fun fp_plus_inf () Float16 (_ +oo 5 11))
+(define-fun fp_minus_inf () Float16 (_ -oo 5 11))
+(define-fun fp_nan () Float16 (_ NaN 5 11))
+
+(synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Bool
+(
+ (Start Bool (
+  (fp.isNaN FpOp)
+  (fp.isNegative FpOp)
+  (fp.isPositive FpOp)
+  (fp.isZero FpOp)
+  (fp.isSubnormal FpOp)
+  (fp.isNormal FpOp)
+  (and Start Start)
+  (or Start Start)
+  (not Start Start)
+  true
+  false
+ ))
+
+ (FpOp Float16 (
+  (fp.abs FpOp)
+  (fp.neg FpOp)
+  (fp.add r FpOp FpOp)
+  (fp.sub r FpOp FpOp)
+  (fp.mul r FpOp FpOp)
+  (fp.div r FpOp FpOp)
+  (fp.sqrt r FpOp)
+  (fp.rem FpOp FpOp)
+  x
+  y
+  fp_plus_zero
+  fp_minus_zero
+  fp_plus_inf
+  fp_minus_inf
+  fp_nan
+  (ite Start FpOp FpOp)
+ ))
+
+))
+(check-synth)
diff --git a/test/regress/regress2/rr-verify/fp-arith.sy b/test/regress/regress2/rr-verify/fp-arith.sy
new file mode 100644
index 000000000..62f01dbda
--- /dev/null
+++ b/test/regress/regress2/rr-verify/fp-arith.sy
@@ -0,0 +1,34 @@
+; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
+; EXIT: 1
+
+(set-logic FP)
+
+(define-fun fp_plus_zero () Float16 (_ +zero 5 11))
+(define-fun fp_minus_zero () Float16 (_ -zero 5 11))
+(define-fun fp_plus_inf () Float16 (_ +oo 5 11))
+(define-fun fp_minus_inf () Float16 (_ -oo 5 11))
+(define-fun fp_nan () Float16 (_ NaN 5 11))
+
+(synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Float16
+(
+ (Start Float16 (
+  (fp.abs Start)
+  (fp.neg Start)
+  (fp.add r Start Start)
+  (fp.sub r Start Start)
+  (fp.mul r Start Start)
+  (fp.div r Start Start)
+  (fp.sqrt r Start)
+  (fp.rem Start Start)
+  x
+  y
+  fp_plus_zero
+  fp_minus_zero
+  fp_plus_inf
+  fp_minus_inf
+  fp_nan
+ ))
+))
+(check-synth)