More minor cleaning of options (#8401)

Removes a few more unnecessary options and moves the location of one.

diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index 210803dbba6b4bb64a410db67b0bb1d0caf61014..9ac284ddd6ab2364563d0936d0f0784457bd19e8 100644 (file)
--- 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 36f49836ed131d4a03b057893b13ea12733cee4a..199445117342bff401211e651640b17e6b1c5cda 100644 (file)
--- 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 30da2e1defe7899e9a393bea5c53664b44aaef2f..97f4b408d3d982b2f357c5ebdcba267d4dfa3095 100644 (file)
--- 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 c6907a83d7e109a7b13f1706d6238eded0a0fbe2..1c81dcf3dafe639a6fc0ac5f6f248aa9f1d78fba 100644 (file)
--- 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 9f322f4877bf30961306bf55b7f8c37fcfe19f4d..888800e4f4cc03f4e31b34ec8eee9ebeab9aed47 100644 (file)
--- 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 f9d478b0749c7937198f30bfc81fc15786a2275d..19a500bed2a6495269f49091c41610e2183efd1e 100644 (file)
--- 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 57fbe66bb9fa39fae92dead6f587b2271d0f3d1c..1768f9fd36dd19f32a7372bd92f55038b56b2382 100644 (file)
--- 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 fb3106bdf4fb8478cdf5778c296631986faed061..3e17e5de54a0cd7287cda74dfe444bfb2f6943f9 100644 (file)
--- 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 80bc294e6ca914cff93eb3feda21001e8bbef0c0..47bf74a2e30cddfaebc6f4afc5ba7ae1f11dcfd6 100644 (file)
--- 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 a13aa2bae4cbf860f8f31464f293830b3bcdf4a2..f6d11bb3d6b8c1c84c4c2ecdcdb9eb623b9889fa 100644 (file)
--- 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 61088eeeb646244674b69fb2db421bf3998196b1..8e5598b6c1be9d22b8f77960fe701505c05bb895 100644 (file)
--- 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 1e77e88f3498d93df409b68d63aa8f1cd86c6339..37eccc67f3f03ec62b8e13d931ac729f919e20f6 100644 (file)
--- 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)