From 4956453dda9d055a3fc4d65ffc964c7cf22d825b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Mar 2022 20:53:51 -0500 Subject: [PATCH] More minor cleaning of options (#8401) Removes a few more unnecessary options and moves the location of one. --- src/options/printer_options.toml | 18 ++++++++++++++++++ src/options/quantifiers_options.toml | 16 ---------------- src/options/smt_options.toml | 18 ------------------ src/options/uf_options.toml | 2 +- src/smt/set_defaults.cpp | 19 +------------------ test/regress/cli/regress1/bug516.smt2 | 2 +- .../cli/regress1/fmf/bound-int-alt.smt2 | 2 +- .../cli/regress1/fmf/fmf-bound-int.smt2 | 2 +- .../cli/regress1/fmf/ko-bound-set.cvc.smt2 | 2 +- .../cli/regress1/ho/issue4065-no-rep.smt2 | 2 +- .../set-choice-koikonomou.cvc.smt2 | 2 +- .../sygus/issue4022-conjecture-gen.smt2 | 3 ++- 12 files changed, 28 insertions(+), 60 deletions(-) diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index 210803dbb..9ac284ddd 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -57,3 +57,21 @@ name = "Printing" [[option.mode.None]] name = "none" help = "(default) do not print declarations of uninterpreted elements in models." + +[[option]] + name = "sygusOut" + category = "regular" + long = "sygus-out=MODE" + type = "SygusSolutionOutMode" + default = "STANDARD" + help = "output mode for sygus" + help_mode = "Modes for sygus solution output." +[[option.mode.STATUS]] + name = "status" + help = "Print only status for check-synth calls." +[[option.mode.STATUS_AND_DEF]] + name = "status-and-def" + help = "Print status followed by definition corresponding to solution." +[[option.mode.STANDARD]] + name = "sygus-standard" + help = "Print based on SyGuS standard." diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 36f49836e..199445117 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -627,14 +627,6 @@ name = "Quantifiers" default = "false" help = "interleave model-based quantifier instantiation with other techniques" -[[option]] - name = "fmfBoundInt" - category = "regular" - long = "fmf-bound-int" - type = "bool" - default = "false" - help = "finite model finding on bounded integer quantification" - [[option]] name = "fmfBound" category = "regular" @@ -782,14 +774,6 @@ name = "Quantifiers" default = "1" help = "number of conjectures to generate per instantiation round" -[[option]] - name = "conjectureNoFilter" - category = "expert" - long = "conjecture-no-filter" - type = "bool" - default = "false" - help = "do not filter conjectures" - [[option]] name = "conjectureFilterActiveTerms" category = "expert" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 30da2e1de..97f4b408d 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -151,24 +151,6 @@ name = "SMT Layer" default = "false" help = "after UNSAT/VALID, check the generated proof (with proof)" -[[option]] - name = "sygusOut" - category = "regular" - long = "sygus-out=MODE" - type = "SygusSolutionOutMode" - default = "STANDARD" - help = "output mode for sygus" - help_mode = "Modes for sygus solution output." -[[option.mode.STATUS]] - name = "status" - help = "Print only status for check-synth calls." -[[option.mode.STATUS_AND_DEF]] - name = "status-and-def" - help = "Print status followed by definition corresponding to solution." -[[option.mode.STANDARD]] - name = "sygus-standard" - help = "Print based on SyGuS standard." - [[option]] name = "unsatCores" category = "regular" diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index c6907a83d..1c81dcf3d 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -53,7 +53,7 @@ name = "Uninterpreted Functions Theory" [[option]] name = "ufHoExt" - category = "regular" + category = "expert" long = "uf-ho-ext" type = "bool" default = "true" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 9f322f487..888800e4f 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1328,10 +1328,8 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, opts.quantifiers.cegqi = false; } - if ((opts.quantifiers.fmfBoundLazyWasSetByUser + if (opts.quantifiers.fmfBoundLazyWasSetByUser && opts.quantifiers.fmfBoundLazy) - || (opts.quantifiers.fmfBoundIntWasSetByUser - && opts.quantifiers.fmfBoundInt)) { opts.quantifiers.fmfBound = true; Trace("smt") @@ -1524,21 +1522,6 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, opts.quantifiers.purifyTriggers = true; } } - if (opts.quantifiers.conjectureNoFilter) - { - if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser) - { - opts.quantifiers.conjectureFilterActiveTerms = false; - } - if (!opts.quantifiers.conjectureFilterCanonicalWasSetByUser) - { - opts.quantifiers.conjectureFilterCanonical = false; - } - if (!opts.quantifiers.conjectureFilterModelWasSetByUser) - { - opts.quantifiers.conjectureFilterModel = false; - } - } if (opts.quantifiers.conjectureGenPerRoundWasSetByUser) { if (opts.quantifiers.conjectureGenPerRound > 0) diff --git a/test/regress/cli/regress1/bug516.smt2 b/test/regress/cli/regress1/bug516.smt2 index f9d478b07..19a500bed 100644 --- a/test/regress/cli/regress1/bug516.smt2 +++ b/test/regress/cli/regress1/bug516.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-bound-int -q +; COMMAND-LINE: --finite-model-find --fmf-bound -q ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/cli/regress1/fmf/bound-int-alt.smt2 b/test/regress/cli/regress1/fmf/bound-int-alt.smt2 index 57fbe66bb..1768f9fd3 100644 --- a/test/regress/cli/regress1/fmf/bound-int-alt.smt2 +++ b/test/regress/cli/regress1/fmf/bound-int-alt.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-bound-int +; COMMAND-LINE: --finite-model-find --fmf-bound ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/cli/regress1/fmf/fmf-bound-int.smt2 b/test/regress/cli/regress1/fmf/fmf-bound-int.smt2 index fb3106bdf..3e17e5de5 100644 --- a/test/regress/cli/regress1/fmf/fmf-bound-int.smt2 +++ b/test/regress/cli/regress1/fmf/fmf-bound-int.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-bound-int +; COMMAND-LINE: --finite-model-find --fmf-bound ; EXPECT: sat (set-logic UFLIA) (declare-fun P (Int Int) Bool) diff --git a/test/regress/cli/regress1/fmf/ko-bound-set.cvc.smt2 b/test/regress/cli/regress1/fmf/ko-bound-set.cvc.smt2 index 80bc294e6..47bf74a2e 100644 --- a/test/regress/cli/regress1/fmf/ko-bound-set.cvc.smt2 +++ b/test/regress/cli/regress1/fmf/ko-bound-set.cvc.smt2 @@ -2,7 +2,7 @@ (set-logic ALL) (set-option :incremental false) (set-option :finite-model-find true) -(set-option :fmf-bound-int true) +(set-option :fmf-bound true) (set-option :produce-models true) (declare-fun X () (Set Int)) (declare-fun Y () (Set Int)) diff --git a/test/regress/cli/regress1/ho/issue4065-no-rep.smt2 b/test/regress/cli/regress1/ho/issue4065-no-rep.smt2 index a13aa2bae..f6d11bb3d 100644 --- a/test/regress/cli/regress1/ho/issue4065-no-rep.smt2 +++ b/test/regress/cli/regress1/ho/issue4065-no-rep.smt2 @@ -1,6 +1,6 @@ (set-logic HO_AUFBV) (set-info :status unsat) -(set-option :fmf-bound-int true) +(set-option :fmf-bound true) (declare-fun _substvar_20_ () Bool) (declare-sort S4 0) (assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true))) diff --git a/test/regress/cli/regress1/quantifiers/set-choice-koikonomou.cvc.smt2 b/test/regress/cli/regress1/quantifiers/set-choice-koikonomou.cvc.smt2 index 61088eeeb..8e5598b6c 100644 --- a/test/regress/cli/regress1/quantifiers/set-choice-koikonomou.cvc.smt2 +++ b/test/regress/cli/regress1/quantifiers/set-choice-koikonomou.cvc.smt2 @@ -2,7 +2,7 @@ (set-logic ALL) (set-option :incremental false) (set-option :finite-model-find true) -(set-option :fmf-bound-int true) +(set-option :fmf-bound true) (declare-fun X () (Set Int)) (assert (= (set.card X) 3)) (assert (forall ((z Int)) (=> (set.member z X) (and (> z 0) (< z 2))))) diff --git a/test/regress/cli/regress2/sygus/issue4022-conjecture-gen.smt2 b/test/regress/cli/regress2/sygus/issue4022-conjecture-gen.smt2 index 1e77e88f3..37eccc67f 100644 --- a/test/regress/cli/regress2/sygus/issue4022-conjecture-gen.smt2 +++ b/test/regress/cli/regress2/sygus/issue4022-conjecture-gen.smt2 @@ -3,7 +3,8 @@ (set-logic ALL) (set-option :conjecture-filter-model true) (set-option :conjecture-gen true) -(set-option :conjecture-no-filter true) +(set-option :conjecture-filter-canonical false) +(set-option :conjecture-filter-active-terms false) (set-option :quant-ind true) (set-option :sygus-inference true) (set-info :status sat) -- 2.30.2