From 43cec89207dd1043608273769a20309167ad3c90 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 12 Oct 2018 19:35:01 -0700 Subject: [PATCH] Reset input language for ExprMiner subsolver (#2624) --- src/options/quantifiers_options.toml | 8 ++++ src/smt/smt_engine.cpp | 16 +++++++ src/theory/quantifiers/expr_miner.cpp | 4 +- test/regress/CMakeLists.txt | 4 +- test/regress/Makefile.tests | 2 + test/regress/regress1/rr-verify/fp-arith.sy | 34 ++++++++++++++ test/regress/regress1/rr-verify/fp-bool.sy | 50 +++++++++++++++++++++ 7 files changed, 115 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress1/rr-verify/fp-arith.sy create mode 100644 test/regress/regress1/rr-verify/fp-bool.sy diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index e65d57770..f3baa8214 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1355,6 +1355,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 67aa8688c..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& 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 @@ -91,6 +90,7 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); checker->setOption("sygus-rr-synth-input", false); + checker->setOption("input-language", "smt2"); Expr equery = squery.toExpr().exportTo(&em, varMap); checker->assertFormula(equery); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 902ddf0f9..aef40d373 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1168,8 +1168,8 @@ set(regress_1_tests regress1/nl/dist-big.smt2 regress1/nl/div-mod-partial.smt2 regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 - regress1/nl/exp-approx.smt2 regress1/nl/exp-4.5-lt.smt2 + regress1/nl/exp-approx.smt2 regress1/nl/exp1-lb.smt2 regress1/nl/exp_monotone.smt2 regress1/nl/factor_agg_s.smt2 @@ -1412,6 +1412,8 @@ set(regress_1_tests regress1/rr-verify/bool-crci.sy regress1/rr-verify/bv-term-32.sy regress1/rr-verify/bv-term.sy + regress1/rr-verify/fp-arith.sy + regress1/rr-verify/fp-bool.sy regress1/rr-verify/regex.sy regress1/rr-verify/string-term.sy regress1/sep/chain-int.smt2 diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 91f33721a..b4e151a17 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1409,6 +1409,8 @@ 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-arith.sy \ + regress1/rr-verify/fp-bool.sy \ regress1/rr-verify/regex.sy \ regress1/rr-verify/string-term.sy \ regress1/sep/chain-int.smt2 \ diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy new file mode 100644 index 000000000..1b056271c --- /dev/null +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -0,0 +1,34 @@ +; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --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|\(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) 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..e94319401 --- /dev/null +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -0,0 +1,50 @@ +; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --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|\(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) -- 2.30.2