Clean options (#8309)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 23 Mar 2022 23:53:14 +0000 (18:53 -0500)
committerGitHub <noreply@github.com>
Wed, 23 Mar 2022 23:53:14 +0000 (23:53 +0000)
Deletes many unnecessary options, cleans some documentation, consolidates several options.

79 files changed:
contrib/competitions/smt-comp/run-script-smtcomp-current
src/options/arith_options.toml
src/options/main_options.toml
src/options/printer_options.toml
src/options/quantifiers_options.toml
src/options/sets_options.toml
src/options/smt_options.toml
src/options/strings_options.toml
src/preprocessing/passes/ite_simp.cpp
src/preprocessing/passes/ite_simp.h
src/smt/set_defaults.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/ematching/ho_trigger.cpp
src/theory/quantifiers/equality_query.cpp
src/theory/quantifiers/first_order_model.cpp
src/theory/quantifiers/fmf/full_model_check.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quantifiers_modules.cpp
src/theory/quantifiers/quantifiers_preprocess.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/quantifiers_state.cpp
src/theory/quantifiers/quantifiers_statistics.cpp
src/theory/quantifiers/quantifiers_statistics.h
src/theory/quantifiers/sygus/sygus_repair_const.cpp
src/theory/quantifiers/sygus/term_database_sygus.cpp
src/theory/quantifiers/sygus_sampler.cpp
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers_engine.cpp
src/theory/strings/theory_strings.cpp
test/regress/cli/regress0/arith/issue7984-quant-trans.smt2
test/regress/cli/regress0/decision/issue8296-sk-def-before-assert.smt2
test/regress/cli/regress0/nl/nta/issue8294-2-double-solve.smt2
test/regress/cli/regress0/quantifiers/issue5693-prenex.smt2
test/regress/cli/regress0/strings/issue6604-re-elim.smt2
test/regress/cli/regress0/strings/issue8295-star-union-char.smt2
test/regress/cli/regress0/strings/regexp_inclusion.smt2
test/regress/cli/regress0/strings/regexp_inclusion_reduction.smt2
test/regress/cli/regress1/fmf/fib-core.smt2
test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2
test/regress/cli/regress1/fmf/loopy_coda.smt2
test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2
test/regress/cli/regress1/quantifiers/proj-issue155.smt2
test/regress/cli/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2
test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2
test/regress/cli/regress1/rr-verify/bool-crci.sy
test/regress/cli/regress1/rr-verify/bv-term-32.sy
test/regress/cli/regress1/rr-verify/bv-term.sy
test/regress/cli/regress1/rr-verify/fp-arith.sy
test/regress/cli/regress1/rr-verify/fp-bool.sy
test/regress/cli/regress1/rr-verify/string-term.sy
test/regress/cli/regress1/seq/issue8148-const-mv.smt2
test/regress/cli/regress1/strings/issue2982.smt2
test/regress/cli/regress1/strings/issue6604-2.smt2
test/regress/cli/regress1/strings/issue6635-rre.smt2
test/regress/cli/regress1/strings/issue6653-4-rre.smt2
test/regress/cli/regress1/strings/issue6653-rre-small.smt2
test/regress/cli/regress1/strings/issue6653-rre.smt2
test/regress/cli/regress1/strings/issue6766-re-elim-bv.smt2
test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2
test/regress/cli/regress1/strings/non_termination_regular_expression4.smt2
test/regress/cli/regress1/strings/nt6-dd.smt2
test/regress/cli/regress1/strings/policy_variable.smt2
test/regress/cli/regress1/strings/proj254-re-elim-agg.smt2
test/regress/cli/regress1/strings/query4674.smt2
test/regress/cli/regress1/strings/query8485.smt2
test/regress/cli/regress1/strings/re-agg-total1.smt2
test/regress/cli/regress1/strings/re-agg-total2.smt2
test/regress/cli/regress1/strings/re-all-char-hard.smt2
test/regress/cli/regress1/strings/re-elim-exact.smt2
test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2
test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2
test/regress/cli/regress1/sygus/proj-issue165.smt2
test/regress/cli/regress2/strings/issue918.smt2
test/regress/cli/regress2/strings/non_termination_regular_expression6.smt2
test/regress/cli/regress2/strings/small-1.smt2
test/regress/cli/regress3/regex-rrv.sy
test/regress/cli/regress4/unsat-circ-reduce.smt2
test/regress/cli/run_regression.py

index 3fe7bbd11fce9d10f53a2ef3e7fc595933973bd7..01aa78ba4a5b69397a34b149d2562c72d06d5657 100755 (executable)
@@ -90,9 +90,9 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFD
   # other 4 min
   trywith 30 --pre-skolem-quant --enum-inst
   trywith 30 --inst-when=full --enum-inst
-  trywith 30 --no-e-matching --no-quant-cf --enum-inst
+  trywith 30 --no-e-matching --no-cbqi --enum-inst
   trywith 30 --enum-inst --quant-ind
-  trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --enum-inst
+  trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --enum-inst
   trywith 30 --decision=internal --enum-inst --enum-inst-sum
   trywith 30 --term-db-mode=relevant --enum-inst
   trywith 30 --enum-inst-interleave --enum-inst
@@ -100,7 +100,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFD
   trywith 30 --finite-model-find --mbqi=none
   trywith 30 --finite-model-find --decision=internal
   trywith 30 --finite-model-find --macros-quant --macros-quant-mode=all
-  trywith 60 --finite-model-find --fmf-inst-engine
+  trywith 60 --finite-model-find --e-matching
   # long runs 4 min
   trywith 240 --finite-model-find --decision=internal
   finishwith --enum-inst
index a5e8a8a98dffcd95da2d3b636148e3a1ee37925f..63b0658807e2724a665f0a25da0390e5ab1a48bf 100644 (file)
@@ -20,6 +20,7 @@ name   = "Arithmetic Theory"
   help  = "Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d."
 [[option.mode.NO]]
   name = "none"
+  help  = "Do not add unate lemmas."
 
 [[option]]
   name       = "arithPropagationMode"
index ac63b1fb121d2277ea1779177268c754f75fd539..0dbe2899f9566398207cac0b7de766f7eb06eb75 100644 (file)
@@ -143,14 +143,6 @@ name   = "Driver"
   default    = "false"
   help       = "output unsat cores after every UNSAT/VALID response"
 
-[[option]]
-  name       = "printUnsatCoresFull"
-  category   = "regular"
-  long       = "print-unsat-cores-full"
-  type       = "bool"
-  default    = "false"
-  help       = "dump the full unsat core, including unlabeled assertions"
-
 [[option]]
   name       = "dumpDifficulty"
   category   = "regular"
index cc9847469661d755eb590f6737e35e9a594049b5..e6806823de5a47ce992e6ba9b1c9d94661aad597 100644 (file)
@@ -31,3 +31,11 @@ name   = "Printing"
   type       = "bool"
   default    = "true"
   help       = "print instantiations for formulas that do not have given identifiers"
+
+[[option]]
+  name       = "printUnsatCoresFull"
+  category   = "regular"
+  long       = "print-unsat-cores-full"
+  type       = "bool"
+  default    = "false"
+  help       = "when printing unsat cores, include unlabeled assertions"
index 878ee0ac1420d114aec4db1cb9b0604f228c18f6..8e29db08e2be8062e3cc592293de831fabcbbe1c 100644 (file)
@@ -2,34 +2,37 @@ id     = "QUANTIFIERS"
 name   = "Quantifiers"
 
 # Whether to mini-scope quantifiers.
-# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
-# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
+# Miniscoping is done based on two techniques.
+# First, miniscoping can be done based on conjunctions within quantified
+# formulas. For example, forall x. (P(x) ^ Q(x)) can be rewritten to
+# (forall x. P(x)) ^ (forall x. Q(x))
+# Second, miniscoping can be done based which free variables occur in
+# subformulas of quantified formulas. For example, forall xy. (P(x) V Q(y))
+# can be rewritten to:
+# (forall x. P(x)) V (forall y. Q(y)).
 [[option]]
   name       = "miniscopeQuant"
   category   = "regular"
-  long       = "miniscope-quant"
-  type       = "bool"
-  default    = "true"
-  help       = "miniscope quantifiers"
-
-# Whether to mini-scope quantifiers based on formulas with no free variables.
-# For example, forall x. ( P( x ) V Q ) will be rewritten to
-# ( forall x. P( x ) ) V Q
-[[option]]
-  name       = "miniscopeQuantFreeVar"
-  category   = "regular"
-  long       = "miniscope-quant-fv"
-  type       = "bool"
-  default    = "true"
-  help       = "miniscope quantifiers for ground subformulas"
-
-[[option]]
-  name       = "quantSplit"
-  category   = "regular"
-  long       = "quant-split"
-  type       = "bool"
-  default    = "true"
-  help       = "apply splitting to quantified formulas based on variable disjoint disjuncts"
+  long       = "miniscope-quant=MODE"
+  type       = "MiniscopeQuantMode"
+  default    = "CONJ_AND_FV"
+  help       = "miniscope mode for quantified formulas"
+  help_mode  = "Miniscope quantifiers modes."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not miniscope quantifiers."
+[[option.mode.CONJ]]
+  name = "conj"
+  help = "Use miniscoping of conjunctions only."
+[[option.mode.FV]]
+  name = "fv"
+  help = "Use free variable miniscoping only."
+[[option.mode.CONJ_AND_FV]]
+  name = "conj-and-fv"
+  help = "Enable both conjunction and free variable miniscoping."
+[[option.mode.AGG]]
+  name = "agg"
+  help = "Enable aggressive miniscope, which further may rewrite quantified formulas into a form where miniscoping is possible."
 
 [[option]]
   name       = "prenexQuant"
@@ -41,7 +44,7 @@ name   = "Quantifiers"
   help_mode  = "Prenex quantifiers modes."
 [[option.mode.NONE]]
   name = "none"
-  help = "Do no prenex nested quantifiers."
+  help = "Do not prenex nested quantifiers."
 [[option.mode.SIMPLE]]
   name = "simple"
   help = "Do simple prenexing of same sign quantifiers."
@@ -105,38 +108,50 @@ name   = "Quantifiers"
 [[option]]
   name       = "condVarSplitQuant"
   category   = "regular"
-  long       = "cond-var-split-quant"
-  type       = "bool"
-  default    = "true"
+  long       = "cond-var-split-quant=MODE"
+  type       = "CondVarSplitQuantMode"
+  default    = "ON"
   help       = "split quantified formulas that lead to variable eliminations"
-
-[[option]]
-  name       = "condVarSplitQuantAgg"
-  category   = "regular"
-  long       = "cond-var-split-agg-quant"
-  type       = "bool"
-  default    = "false"
-  help       = "aggressive split quantified formulas that lead to variable eliminations"
-
+  help_mode  = "Modes for splitting quantified formulas that lead to variable eliminations."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not split quantified formulas."
+[[option.mode.ON]]
+  name = "on"
+  help = "Split quantified formulas that lead to variable eliminations."
+[[option.mode.AGG]]
+  name = "agg"
+  help = "Aggressively split quantified formulas that lead to variable eliminations."
+  
 [[option]]
   name       = "iteDtTesterSplitQuant"
-  category   = "regular"
+  category   = "expert"
   long       = "ite-dtt-split-quant"
   type       = "bool"
   default    = "false"
   help       = "split ites with dt testers as conditions"
 
-# Whether to pre-skolemize quantifier bodies.
-# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
-#   forall x. P( x ) => f( S( x ) ) = x
 [[option]]
   name       = "preSkolemQuant"
   category   = "regular"
-  long       = "pre-skolem-quant"
-  type       = "bool"
-  default    = "false"
-  help       = "apply skolemization eagerly to bodies of quantified formulas"
+  long       = "pre-skolem-quant=MODE"
+  type       = "PreSkolemQuantMode"
+  default    = "OFF"
+  help       = "modes to apply skolemization eagerly to bodies of quantified formulas"
+  help_mode  = "Modes to apply skolemization eagerly to bodies of quantified formulas."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not apply Skolemization eagerly."
+[[option.mode.ON]]
+  name = "on"
+  help = "Apply Skolemization eagerly to top-level (negatively asserted) quantified formulas."
+[[option.mode.AGG]]
+  name = "agg"
+  help = "Apply Skolemization eagerly and aggressively during preprocessing."
 
+# Whether to pre-skolemize quantifier bodies.
+# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
+#   forall x. P( x ) => f( S( x ) ) = x
 [[option]]
   name       = "preSkolemQuantNested"
   category   = "regular"
@@ -145,22 +160,6 @@ name   = "Quantifiers"
   default    = "true"
   help       = "apply skolemization to nested quantified formulas"
 
-[[option]]
-  name       = "preSkolemQuantAgg"
-  category   = "regular"
-  long       = "pre-skolem-quant-agg"
-  type       = "bool"
-  default    = "true"
-  help       = "apply skolemization to quantified formulas aggressively"
-
-[[option]]
-  name       = "aggressiveMiniscopeQuant"
-  category   = "regular"
-  long       = "ag-miniscope-quant"
-  type       = "bool"
-  default    = "false"
-  help       = "perform aggressive miniscoping for quantifiers"
-
 [[option]]
   name       = "elimTautQuant"
   category   = "regular"
@@ -212,7 +211,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "termDbCd"
-  category   = "regular"
+  category   = "expert"
   long       = "term-db-cd"
   type       = "bool"
   default    = "true"
@@ -220,7 +219,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "registerQuantBodyTerms"
-  category   = "regular"
+  category   = "expert"
   long       = "register-quant-body-terms"
   type       = "bool"
   default    = "false"
@@ -228,7 +227,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "relevantTriggers"
-  category   = "regular"
+  category   = "expert"
   long       = "relevant-triggers"
   type       = "bool"
   default    = "false"
@@ -236,7 +235,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "relationalTriggers"
-  category   = "regular"
+  category   = "expert"
   long       = "relational-triggers"
   type       = "bool"
   default    = "false"
@@ -244,7 +243,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "purifyTriggers"
-  category   = "regular"
+  category   = "expert"
   long       = "purify-triggers"
   type       = "bool"
   default    = "false"
@@ -252,7 +251,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "partialTriggers"
-  category   = "regular"
+  category   = "expert"
   long       = "partial-triggers"
   type       = "bool"
   default    = "false"
@@ -260,7 +259,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "consExpandTriggers"
-  category   = "regular"
+  category   = "expert"
   long       = "cons-exp-triggers"
   type       = "bool"
   default    = "false"
@@ -268,7 +267,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "multiTriggerWhenSingle"
-  category   = "regular"
+  category   = "expert"
   long       = "multi-trigger-when-single"
   type       = "bool"
   default    = "false"
@@ -276,7 +275,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "multiTriggerPriority"
-  category   = "regular"
+  category   = "expert"
   long       = "multi-trigger-priority"
   type       = "bool"
   default    = "false"
@@ -284,7 +283,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "multiTriggerCache"
-  category   = "regular"
+  category   = "expert"
   long       = "multi-trigger-cache"
   type       = "bool"
   default    = "false"
@@ -292,7 +291,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "multiTriggerLinear"
-  category   = "regular"
+  category   = "expert"
   long       = "multi-trigger-linear"
   type       = "bool"
   default    = "true"
@@ -403,7 +402,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "incrementTriggers"
-  category   = "regular"
+  category   = "expert"
   long       = "increment-triggers"
   type       = "bool"
   default    = "true"
@@ -443,36 +442,20 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "instWhenPhase"
-  category   = "regular"
+  category   = "expert"
   long       = "inst-when-phase=N"
   type       = "int64_t"
   default    = "2"
   help       = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen"
 
-[[option]]
-  name       = "instWhenTcFirst"
-  category   = "regular"
-  long       = "inst-when-tc-first"
-  type       = "bool"
-  default    = "true"
-  help       = "allow theory combination to happen once initially, before quantifier strategies are run"
-
 [[option]]
   name       = "instMaxLevel"
-  category   = "regular"
+  category   = "expert"
   long       = "inst-max-level=N"
   type       = "int64_t"
   default    = "-1"
   help       = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)"
 
-[[option]]
-  name       = "instLevelInputOnly"
-  category   = "regular"
-  long       = "inst-level-input-only"
-  type       = "bool"
-  default    = "true"
-  help       = "only input terms are assigned instantiation level zero"
-
 [[option]]
   name       = "instMaxRounds"
   category   = "regular"
@@ -483,7 +466,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "quantRepMode"
-  category   = "regular"
+  category   = "expert"
   long       = "quant-rep-mode=MODE"
   type       = "QuantRepMode"
   default    = "FIRST"
@@ -517,7 +500,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "enumInstRd"
-  category   = "regular"
+  category   = "expert"
   long       = "enum-inst-rd"
   type       = "bool"
   default    = "true"
@@ -525,7 +508,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "enumInstLimit"
-  category   = "regular"
+  category   = "expert"
   long       = "enum-inst-limit=N"
   type       = "int64_t"
   default    = "-1"
@@ -541,7 +524,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "enumInstStratify"
-  category   = "regular"
+  category   = "expert"
   long       = "enum-inst-stratify"
   type       = "bool"
   default    = "false"
@@ -549,7 +532,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "enumInstSum"
-  category   = "regular"
+  category   = "expert"
   long       = "enum-inst-sum"
   type       = "bool"
   default    = "false"
@@ -557,7 +540,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "literalMatchMode"
-  category   = "regular"
+  category   = "expert"
   long       = "literal-matching=MODE"
   type       = "LiteralMatchMode"
   default    = "USE"
@@ -578,7 +561,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "poolInst"
-  category   = "regular"
+  category   = "expert"
   long       = "pool-inst"
   type       = "bool"
   default    = "true"
@@ -596,7 +579,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "quantFunWellDefined"
-  category   = "regular"
+  category   = "expert"
   long       = "quant-fun-wd"
   type       = "bool"
   default    = "false"
@@ -620,7 +603,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "mbqiMode"
-  category   = "regular"
+  category   = "expert"
   long       = "mbqi=MODE"
   type       = "MbqiMode"
   default    = "FMC"
@@ -638,7 +621,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "fmfOneInstPerRound"
-  category   = "regular"
+  category   = "expert"
   long       = "mbqi-one-inst-per-round"
   type       = "bool"
   default    = "false"
@@ -646,36 +629,12 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "mbqiInterleave"
-  category   = "regular"
+  category   = "expert"
   long       = "mbqi-interleave"
   type       = "bool"
   default    = "false"
   help       = "interleave model-based quantifier instantiation with other techniques"
 
-[[option]]
-  name       = "fmfInstEngine"
-  category   = "regular"
-  long       = "fmf-inst-engine"
-  type       = "bool"
-  default    = "false"
-  help       = "use instantiation engine in conjunction with finite model finding"
-
-[[option]]
-  name       = "fmfFreshDistConst"
-  category   = "regular"
-  long       = "fmf-fresh-dc"
-  type       = "bool"
-  default    = "false"
-  help       = "use fresh distinguished representative when applying Inst-Gen techniques"
-
-[[option]]
-  name       = "fmfFmcSimple"
-  category   = "regular"
-  long       = "fmf-fmc-simple"
-  type       = "bool"
-  default    = "true"
-  help       = "simple models in full model check for finite model finding"
-
 [[option]]
   name       = "fmfBoundInt"
   category   = "regular"
@@ -694,7 +653,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "fmfBoundLazy"
-  category   = "regular"
+  category   = "expert"
   long       = "fmf-bound-lazy"
   type       = "bool"
   default    = "false"
@@ -702,24 +661,26 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "fmfTypeCompletionThresh"
-  category   = "regular"
+  category   = "expert"
   long       = "fmf-type-completion-thresh=N"
   type       = "int64_t"
   default    = "1000"
   help       = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
 
+### Conflict-based instantiation options
+
 [[option]]
-  name       = "quantConflictFind"
+  name       = "conflictBasedInst"
   category   = "regular"
-  long       = "quant-cf"
+  long       = "cbqi"
   type       = "bool"
   default    = "true"
-  help       = "enable conflict find mechanism for quantifiers"
+  help       = "enable conflict-based quantifier instantiation"
 
 [[option]]
-  name       = "qcfMode"
+  name       = "cbqiMode"
   category   = "regular"
-  long       = "quant-cf-mode=MODE"
+  long       = "cbqi-mode=MODE"
   type       = "QcfMode"
   default    = "PROP_EQ"
   help       = "what effort to apply conflict find mechanism"
@@ -730,100 +691,68 @@ name   = "Quantifiers"
 [[option.mode.PROP_EQ]]
   name = "prop-eq"
   help = "Apply QCF algorithm to propagate equalities as well as conflicts."
-[[option.mode.PARTIAL]]
-  name = "partial"
-  help = "Use QCF for conflicts, propagations and heuristic instantiations."
 
 [[option]]
-  name       = "qcfWhenMode"
-  category   = "regular"
-  long       = "quant-cf-when=MODE"
-  type       = "QcfWhenMode"
-  default    = "DEFAULT"
-  help       = "when to invoke conflict find mechanism for quantifiers"
-  help_mode  = "Quantifier conflict find modes."
-[[option.mode.DEFAULT]]
-  name = "default"
-  help = "Default, apply conflict finding at full effort."
-[[option.mode.LAST_CALL]]
-  name = "last-call"
-  help = "Apply conflict finding at last call, after theory combination and and all theories report sat."
-[[option.mode.STD]]
-  name = "std"
-  help = "Apply conflict finding at standard effort."
-[[option.mode.STD_H]]
-  name = "std-h"
-  help = "Apply conflict finding at standard effort when heuristic says to."
-
-[[option]]
-  name       = "qcfTConstraint"
-  category   = "regular"
-  long       = "qcf-tconstraint"
+  name       = "cbqiTConstraint"
+  category   = "expert"
+  long       = "cbqi-tconstraint"
   type       = "bool"
   default    = "false"
-  help       = "enable entailment checks for t-constraints in qcf algorithm"
+  help       = "enable entailment checks for t-constraints in cbqi algorithm"
 
 [[option]]
-  name       = "qcfAllConflict"
-  category   = "regular"
-  long       = "qcf-all-conflict"
+  name       = "cbqiAllConflict"
+  category   = "expert"
+  long       = "cbqi-all-conflict"
   type       = "bool"
   default    = "false"
   help       = "add all available conflicting instances during conflict-based instantiation"
 
 [[option]]
-  name       = "qcfNestedConflict"
-  category   = "regular"
-  long       = "qcf-nested-conflict"
-  type       = "bool"
-  default    = "false"
-  help       = "consider conflicts for nested quantifiers"
-
-[[option]]
-  name       = "qcfVoExp"
-  category   = "regular"
-  long       = "qcf-vo-exp"
+  name       = "cbqiVoExp"
+  category   = "expert"
+  long       = "cbqi-vo-exp"
   type       = "bool"
   default    = "false"
-  help       = "qcf experimental variable ordering"
+  help       = "cbqi experimental variable ordering"
 
 [[option]]
-  name       = "instNoEntail"
-  category   = "regular"
-  long       = "inst-no-entail"
+  name       = "cbqiEagerTest"
+  category   = "expert"
+  long       = "cbqi-eager-test"
   type       = "bool"
   default    = "true"
-  help       = "do not consider instances of quantified formulas that are currently entailed"
+  help       = "optimization, test cbqi instances eagerly"
 
 [[option]]
-  name       = "qcfEagerTest"
-  category   = "regular"
-  long       = "qcf-eager-test"
+  name       = "cbqiEagerCheckRd"
+  category   = "expert"
+  long       = "cbqi-eager-check-rd"
   type       = "bool"
   default    = "true"
-  help       = "optimization, test qcf instances eagerly"
+  help       = "optimization, eagerly check relevant domain of matched position"
 
 [[option]]
-  name       = "qcfEagerCheckRd"
-  category   = "regular"
-  long       = "qcf-eager-check-rd"
+  name       = "cbqiSkipRd"
+  category   = "expert"
+  long       = "cbqi-skip-rd"
   type       = "bool"
-  default    = "true"
-  help       = "optimization, eagerly check relevant domain of matched position"
+  default    = "false"
+  help       = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
 
 [[option]]
-  name       = "qcfSkipRd"
+  name       = "instNoEntail"
   category   = "regular"
-  long       = "qcf-skip-rd"
+  long       = "inst-no-entail"
   type       = "bool"
-  default    = "false"
-  help       = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
+  default    = "true"
+  help       = "do not consider instances of quantified formulas that are currently entailed"
 
 ### Induction options
 
 [[option]]
   name       = "quantInduction"
-  category   = "regular"
+  category   = "expert"
   long       = "quant-ind"
   type       = "bool"
   default    = "false"
@@ -831,7 +760,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "dtStcInduction"
-  category   = "regular"
+  category   = "expert"
   long       = "dt-stc-ind"
   type       = "bool"
   default    = "false"
@@ -839,7 +768,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "intWfInduction"
-  category   = "regular"
+  category   = "expert"
   long       = "int-wf-ind"
   type       = "bool"
   default    = "false"
@@ -847,7 +776,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "conjectureGen"
-  category   = "regular"
+  category   = "expert"
   long       = "conjecture-gen"
   type       = "bool"
   default    = "false"
@@ -855,7 +784,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "conjectureGenPerRound"
-  category   = "regular"
+  category   = "expert"
   long       = "conjecture-gen-per-round=N"
   type       = "int64_t"
   default    = "1"
@@ -863,7 +792,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "conjectureNoFilter"
-  category   = "regular"
+  category   = "expert"
   long       = "conjecture-no-filter"
   type       = "bool"
   default    = "false"
@@ -871,7 +800,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "conjectureFilterActiveTerms"
-  category   = "regular"
+  category   = "expert"
   long       = "conjecture-filter-active-terms"
   type       = "bool"
   default    = "true"
@@ -879,7 +808,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "conjectureFilterCanonical"
-  category   = "regular"
+  category   = "expert"
   long       = "conjecture-filter-canonical"
   type       = "bool"
   default    = "true"
@@ -887,7 +816,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "conjectureFilterModel"
-  category   = "regular"
+  category   = "expert"
   long       = "conjecture-filter-model"
   type       = "bool"
   default    = "true"
@@ -895,23 +824,15 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "conjectureGenGtEnum"
-  category   = "regular"
+  category   = "expert"
   long       = "conjecture-gen-gt-enum=N"
   type       = "int64_t"
   default    = "50"
   help       = "number of ground terms to generate for model filtering"
 
-[[option]]
-  name       = "conjectureUeeIntro"
-  category   = "regular"
-  long       = "conjecture-gen-uee-intro"
-  type       = "bool"
-  default    = "false"
-  help       = "more aggressive merging for universal equality engine, introduces terms"
-
 [[option]]
   name       = "conjectureGenMaxDepth"
-  category   = "regular"
+  category   = "expert"
   long       = "conjecture-gen-max-depth=N"
   type       = "int64_t"
   default    = "3"
@@ -1030,7 +951,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusUnifShuffleCond"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-unif-shuffle-cond"
   type       = "bool"
   default    = "false"
@@ -1038,7 +959,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusUnifCondIndNoRepeatSol"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-unif-cond-independent-no-repeat-sol"
   type       = "bool"
   default    = "true"
@@ -1046,7 +967,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusBoolIteReturnConst"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-bool-ite-return-const"
   type       = "bool"
   default    = "true"
@@ -1054,7 +975,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusQePreproc"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-qe-preproc"
   type       = "bool"
   default    = "false"
@@ -1110,7 +1031,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusEnumRandomP"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-enum-random-p=P"
   type       = "double"
   default    = "0.5"
@@ -1120,7 +1041,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusEnumFastNumConsts"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-enum-fast-num-consts=N"
   type       = "uint64_t"
   default    = "5"
@@ -1144,7 +1065,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusGrammarNorm"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-grammar-norm"
   type       = "bool"
   default    = "false"
@@ -1207,7 +1128,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusInvAutoUnfold"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-auto-unfold"
   type       = "bool"
   default    = "true"
@@ -1223,7 +1144,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusPbeMultiFair"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-pbe-multi-fair"
   type       = "bool"
   default    = "false"
@@ -1231,7 +1152,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusPbeMultiFairDiff"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-pbe-multi-fair-diff=N"
   type       = "int64_t"
   default    = "0"
@@ -1247,7 +1168,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusEvalUnfoldBool"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-eval-unfold-bool"
   type       = "bool"
   default    = "true"
@@ -1263,7 +1184,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegisSample"
-  category   = "regular"
+  category   = "expert"
   long       = "cegis-sample=MODE"
   type       = "CegisSampleMode"
   default    = "NONE"
@@ -1279,17 +1200,9 @@ name   = "Quantifiers"
   name = "trust"
   help = "Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures."
 
-[[option]]
-  name       = "sygusEvalOpt"
-  category   = "regular"
-  long       = "sygus-eval-opt"
-  type       = "bool"
-  default    = "true"
-  help       = "use optimized approach for evaluation in sygus"
-
 [[option]]
   name       = "sygusArgRelevant"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-arg-relevant"
   type       = "bool"
   default    = "false"
@@ -1297,7 +1210,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRecFun"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rec-fun"
   type       = "bool"
   default    = "true"
@@ -1305,7 +1218,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRecFunEvalLimit"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rec-fun-eval-limit=N"
   type       = "uint64_t"
   default    = "1000"
@@ -1313,7 +1226,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusVerifyInstMaxRounds"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-verify-inst-max-rounds=N"
   type       = "int64_t"
   default    = "3"
@@ -1329,17 +1242,9 @@ name   = "Quantifiers"
 
 # Internal uses of sygus
 
-[[option]]
-  name       = "sygusRew"
-  category   = "regular"
-  long       = "sygus-rr"
-  type       = "bool"
-  default    = "false"
-  help       = "use sygus to enumerate and verify correctness of rewrite rules"
-
 [[option]]
   name       = "sygusRewSynth"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth"
   type       = "bool"
   default    = "false"
@@ -1347,7 +1252,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthFilterOrder"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-filter-order"
   type       = "bool"
   default    = "true"
@@ -1355,7 +1260,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthFilterMatch"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-filter-match"
   type       = "bool"
   default    = "true"
@@ -1363,7 +1268,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthFilterCong"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-filter-cong"
   type       = "bool"
   default    = "true"
@@ -1371,7 +1276,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthFilterNonLinear"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-filter-nl"
   type       = "bool"
   default    = "false"
@@ -1385,17 +1290,9 @@ name   = "Quantifiers"
   default    = "false"
   help       = "use sygus to verify the correctness of rewrite rules via sampling"
 
-[[option]]
-  name       = "sygusRewVerifyAbort"
-  category   = "regular"
-  long       = "sygus-rr-verify-abort"
-  type       = "bool"
-  default    = "true"
-  help       = "abort when sygus-rr-verify finds an instance of unsoundness"
-
 [[option]]
   name       = "sygusSamples"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-samples=N"
   type       = "int64_t"
   default    = "1000"
@@ -1403,7 +1300,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusSampleGrammar"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-sample-grammar"
   type       = "bool"
   default    = "true"
@@ -1411,7 +1308,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusSampleFpUniform"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-sample-fp-uniform"
   type       = "bool"
   default    = "false"
@@ -1419,7 +1316,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthAccel"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-accel"
   type       = "bool"
   default    = "false"
@@ -1427,7 +1324,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthCheck"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-check"
   type       = "bool"
   default    = "true"
@@ -1435,7 +1332,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthInput"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-input"
   type       = "bool"
   default    = "false"
@@ -1443,7 +1340,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthInputNVars"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-input-nvars=N"
   type       = "int64_t"
   default    = "3"
@@ -1451,7 +1348,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthInputUseBool"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-input-use-bool"
   type       = "bool"
   default    = "false"
@@ -1467,7 +1364,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusRewSynthRec"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-rr-synth-rec"
   type       = "bool"
   default    = "false"
@@ -1496,7 +1393,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusQueryGenThresh"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-query-gen-thresh=N"
   type       = "uint64_t"
   default    = "5"
@@ -1522,7 +1419,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusFilterSolMode"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-filter-sol=MODE"
   type       = "SygusFilterSolMode"
   default    = "NONE"
@@ -1558,7 +1455,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiFullEffort"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-full"
   type       = "bool"
   default    = "false"
@@ -1566,7 +1463,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiAll"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-all"
   type       = "bool"
   default    = "false"
@@ -1574,23 +1471,15 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiMultiInst"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-multi-inst"
   type       = "bool"
   default    = "false"
   help       = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
 
-[[option]]
-  name       = "cegqiRepeatLit"
-  category   = "regular"
-  long       = "cegqi-repeat-lit"
-  type       = "bool"
-  default    = "false"
-  help       = "solve literals more than once in counterexample-based quantifier instantiation"
-
 [[option]]
   name       = "cegqiInnermost"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-innermost"
   type       = "bool"
   default    = "true"
@@ -1598,7 +1487,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiNestedQE"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-nested-qe"
   type       = "bool"
   default    = "false"
@@ -1608,7 +1497,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiUseInfInt"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-use-inf-int"
   type       = "bool"
   default    = "false"
@@ -1616,7 +1505,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiUseInfReal"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-use-inf-real"
   type       = "bool"
   default    = "false"
@@ -1624,7 +1513,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiMinBounds"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-min-bounds"
   type       = "bool"
   default    = "false"
@@ -1632,7 +1521,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiRoundUpLowerLia"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-round-up-lia"
   type       = "bool"
   default    = "false"
@@ -1640,7 +1529,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiMidpoint"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-midpoint"
   type       = "bool"
   default    = "false"
@@ -1648,7 +1537,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiNopt"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-nopt"
   type       = "bool"
   default    = "true"
@@ -1666,7 +1555,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiBvInterleaveValue"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-bv-interleave-value"
   type       = "bool"
   default    = "false"
@@ -1692,7 +1581,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiBvRmExtract"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-bv-rm-extract"
   type       = "bool"
   default    = "true"
@@ -1700,7 +1589,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiBvLinearize"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-bv-linear"
   type       = "bool"
   default    = "true"
@@ -1708,7 +1597,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiBvSolveNl"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-bv-solve-nl"
   type       = "bool"
   default    = "false"
@@ -1716,7 +1605,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "cegqiBvConcInv"
-  category   = "regular"
+  category   = "expert"
   long       = "cegqi-bv-concat-inv"
   type       = "bool"
   default    = "true"
@@ -1780,23 +1669,15 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "hoMatching"
-  category   = "regular"
+  category   = "expert"
   long       = "ho-matching"
   type       = "bool"
   default    = "true"
   help       = "do higher-order matching algorithm for triggers with variable operators"
 
-[[option]]
-  name       = "hoMatchingVarArgPriority"
-  category   = "regular"
-  long       = "ho-matching-var-priority"
-  type       = "bool"
-  default    = "true"
-  help       = "give priority to variable arguments over constant arguments"
-
 [[option]]
   name       = "hoMergeTermDb"
-  category   = "regular"
+  category   = "expert"
   long       = "ho-merge-term-db"
   type       = "bool"
   default    = "true"
@@ -1804,7 +1685,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "hoElim"
-  category   = "regular"
+  category   = "expert"
   long       = "ho-elim"
   type       = "bool"
   default    = "false"
@@ -1812,7 +1693,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "hoElimStoreAx"
-  category   = "regular"
+  category   = "expert"
   long       = "ho-elim-store-ax"
   type       = "bool"
   default    = "true"
@@ -1830,7 +1711,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusInstScope"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-inst-scope=MODE"
   type       = "SygusInstScope"
   default    = "IN"
@@ -1848,7 +1729,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusInstTermSel"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-inst-term-sel=MODE"
   type       = "SygusInstTermSelMode"
   default    = "MIN"
@@ -1866,7 +1747,7 @@ name   = "Quantifiers"
 
 [[option]]
   name       = "sygusInstMode"
-  category   = "regular"
+  category   = "expert"
   long       = "sygus-inst-mode=MODE"
   type       = "SygusInstMode"
   default    = "PRIORITY_INST"
index dee134ae4d4f86f3a88c544656f26aee0b5ba39e..ba0a9ad1df6090a149326a2b56c194af65d95bb3 100644 (file)
@@ -3,7 +3,7 @@ name   = "Sets Theory"
 
 [[option]]
   name       = "setsProxyLemmas"
-  category   = "regular"
+  category   = "expert"
   long       = "sets-proxy-lemmas"
   type       = "bool"
   default    = "false"
@@ -11,7 +11,7 @@ name   = "Sets Theory"
 
 [[option]]
   name       = "setsInferAsLemmas"
-  category   = "regular"
+  category   = "expert"
   long       = "sets-infer-as-lemmas"
   type       = "bool"
   default    = "true"
@@ -19,7 +19,7 @@ name   = "Sets Theory"
 
 [[option]]
   name       = "setsExt"
-  category   = "regular"
+  category   = "expert"
   long       = "sets-ext"
   type       = "bool"
   default    = "false"
index fdf65f5eca0863fd4d9e1ebb839cbee7cd4ea9db..8dee79cd35f88ba988ab355f3e2b86eb10a9a76f 100644 (file)
@@ -134,6 +134,23 @@ name   = "SMT Layer"
   default    = "false"
   help       = "produce proofs, support check-proofs and get-proof"
 
+[[option]]
+  name       = "proofMode"
+  category   = "expert"
+  long       = "proof-mode=MODE"
+  type       = "ProofMode"
+  default    = "OFF"
+  help       = "choose proof mode, see --proof-mode=help"
+  help_mode  = "proof modes."
+[[option.mode.OFF]]
+  name = "off"
+[[option.mode.PP_ONLY]]
+  name = "pp-only"
+[[option.mode.SAT]]
+  name = "sat-proof"
+[[option.mode.FULL]]
+  name = "full-proof"
+
 [[option]]
   name       = "checkProofs"
   category   = "regular"
@@ -189,23 +206,6 @@ name   = "SMT Layer"
   name = "assumptions"
   help = "Produce unsat cores using solving under assumptions and preprocessing proofs."
 
-[[option]]
-  name       = "proofMode"
-  category   = "expert"
-  long       = "proof-mode=MODE"
-  type       = "ProofMode"
-  default    = "OFF"
-  help       = "choose proof mode, see --proof-mode=help"
-  help_mode  = "proof modes."
-[[option.mode.OFF]]
-  name = "off"
-[[option.mode.PP_ONLY]]
-  name = "pp-only"
-[[option.mode.SAT]]
-  name = "sat-proof"
-[[option.mode.FULL]]
-  name = "full-proof"
-
 [[option]]
   name       = "minimalUnsatCores"
   category   = "regular"
@@ -283,7 +283,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "doITESimp"
-  category   = "regular"
+  category   = "expert"
   long       = "ite-simp"
   type       = "bool"
   default    = "false"
@@ -291,7 +291,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "doITESimpOnRepeat"
-  category   = "regular"
+  category   = "expert"
   long       = "on-repeat-ite-simp"
   type       = "bool"
   default    = "false"
@@ -299,7 +299,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "extRewPrep"
-  category   = "regular"
+  category   = "expert"
   long       = "ext-rew-prep=MODE"
   type       = "ExtRewPrepMode"
   default    = "OFF"
@@ -317,7 +317,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "simplifyWithCareEnabled"
-  category   = "regular"
+  category   = "expert"
   long       = "simp-with-care"
   type       = "bool"
   default    = "false"
@@ -325,7 +325,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "compressItes"
-  category   = "regular"
+  category   = "expert"
   long       = "simp-ite-compress"
   type       = "bool"
   default    = "false"
@@ -349,20 +349,12 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "repeatSimp"
-  category   = "regular"
+  category   = "expert"
   long       = "repeat-simp"
   type       = "bool"
   default    = "false"
   help       = "make multiple passes with nonclausal simplifier"
 
-[[option]]
-  name       = "zombieHuntThreshold"
-  category   = "regular"
-  long       = "simp-ite-hunt-zombies=N"
-  type       = "uint64_t"
-  default    = "524288"
-  help       = "post ite compression enables zombie removal while the number of nodes is above this threshold"
-
 [[option]]
   name       = "sortInference"
   category   = "regular"
@@ -373,7 +365,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "abstractValues"
-  category   = "regular"
+  category   = "expert"
   long       = "abstract-values"
   type       = "bool"
   default    = "false"
@@ -400,7 +392,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "foreignTheoryRewrite"
-  category   = "regular"
+  category   = "expert"
   long       = "foreign-theory-rewrite"
   type       = "bool"
   default    = "false"
index 66753fc0bacb479e6191a29af803b34026d69781..52fec34af5da96cc34c9fc187f9931c9e3303faf 100644 (file)
@@ -47,7 +47,7 @@ name   = "Strings Theory"
   long       = "strings-infer-sym"
   type       = "bool"
   default    = "true"
-  help       = "strings split on empty string"
+  help       = "generalized inferences in strings based on proxy symbols"
 
 [[option]]
   name       = "stringEagerLen"
@@ -89,7 +89,6 @@ name   = "Strings Theory"
   name = "abort"
   help = "Abort if looping word equations are encountered."
 
-
 [[option]]
   name       = "stringInferAsLemmas"
   category   = "regular"
@@ -125,18 +124,20 @@ name   = "Strings Theory"
 [[option]]
   name       = "regExpElim"
   category   = "regular"
-  long       = "re-elim"
-  type       = "bool"
-  default    = "false"
-  help       = "elimination techniques for regular expressions"
-
-[[option]]
-  name       = "regExpElimAgg"
-  category   = "regular"
-  long       = "re-elim-agg"
-  type       = "bool"
-  default    = "false"
-  help       = "aggressive elimination techniques for regular expressions"
+  long       = "re-elim=MODE"
+  type       = "RegExpElimMode"
+  default    = "OFF"
+  help       = "regular expression elimination mode"
+  help_mode  = "Regular expression elimination modes."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not use regular expression elimination."
+[[option.mode.ON]]
+  name = "on"
+  help = "Use regular expression elimination."
+[[option.mode.AGG]]
+  name = "agg"
+  help = "Use aggressive regular expression elimination."
 
 [[option]]
   name       = "stringFlatForms"
@@ -222,7 +223,7 @@ name   = "Strings Theory"
   long       = "strings-regexp-inclusion"
   type       = "bool"
   default    = "true"
-  help       = "use regular expression inclusion"
+  help       = "use regular expression inclusion for finding conflicts and avoiding regular expression unfolding"
 
 [[option]]
   name       = "seqArray"
index 65ea84125ae840301470aed942dce96d76b4b20d..97de3c20623d0ebca0bb6f5662dd564cb4812d8a 100644 (file)
@@ -208,7 +208,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
     {
       // if false, don't bother to reclaim memory here.
       NodeManager* nm = NodeManager::currentNM();
-      if (nm->poolSize() >= options().smt.zombieHuntThreshold)
+      if (nm->poolSize() >= zombieHuntThreshold)
       {
         verbose(2) << "..ite simplifier did quite a bit of work.. "
                << nm->poolSize() << endl;
@@ -216,7 +216,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
                << " nodes before cleanup" << endl;
         d_iteUtilities.clear();
         d_env.getRewriter()->clearCaches();
-        nm->reclaimZombiesUntil(options().smt.zombieHuntThreshold);
+        nm->reclaimZombiesUntil(zombieHuntThreshold);
         verbose(2) << "....node manager contains " << nm->poolSize()
                << " nodes after cleanup" << endl;
       }
index 183cec946af276c4fae8f00b171c3dd7ebb5261d..65a483e74a22f038a1b6d58f20ddc2fa76f2017b 100644 (file)
@@ -49,6 +49,8 @@ class ITESimp : public PreprocessingPass
   util::ITEUtilities d_iteUtilities;
 
   Statistics d_statistics;
+
+  static const uint32_t zombieHuntThreshold = 524288;
 };
 
 }  // namespace passes
index d5fc48f2a13177d0f673fc545b6f702c999d96be..f47d768c06e704e2e3860c249205ee2665d1bc04 100644 (file)
@@ -300,10 +300,10 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
   //
   // We don't want to set this option when we are in logics that contain ALL.
   //
-  // We also must enable stringExp if reElimAgg is true, since this introduces
-  // bounded quantifiers during preprocessing.
+  // We also must enable stringExp if reElim is aggressive, since this
+  // introduces bounded quantifiers during preprocessing.
   if ((!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS))
-      || opts.strings.regExpElimAgg)
+      || opts.strings.regExpElim == options::RegExpElimMode::AGG)
   {
     // If the user explicitly set a logic that includes strings, but is not
     // the generic "ALL" logic, then enable stringsExp.
@@ -1091,15 +1091,15 @@ bool SetDefaults::incompatibleWithUnsatCores(Options& opts,
     opts.smt.sortInference = false;
   }
 
-  if (opts.quantifiers.preSkolemQuant)
+  if (opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
   {
     if (opts.quantifiers.preSkolemQuantWasSetByUser)
     {
       reason << "pre-skolemization";
       return true;
     }
-    notifyModifyOption("preSkolemQuant", "false", "unsat cores");
-    opts.quantifiers.preSkolemQuant = false;
+    notifyModifyOption("preSkolemQuant", "off", "unsat cores");
+    opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::OFF;
   }
 
   if (opts.bv.bitvectorToBool)
@@ -1397,7 +1397,9 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     }
     if (!opts.quantifiers.eMatchingWasSetByUser)
     {
-      opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine;
+      // do not use E-matching by default. For E-matching + FMF, the user should
+      // specify --finite-model-find --e-matching.
+      opts.quantifiers.eMatching = false;
     }
     if (!opts.quantifiers.instWhenModeWasSetByUser)
     {
@@ -1449,9 +1451,9 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   {
     if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
     {
-      if (!opts.quantifiers.quantConflictFindWasSetByUser)
+      if (!opts.quantifiers.conflictBasedInstWasSetByUser)
       {
-        opts.quantifiers.quantConflictFind = false;
+        opts.quantifiers.conflictBasedInst = false;
       }
       if (!opts.quantifiers.instNoEntailWasSetByUser)
       {
@@ -1477,16 +1479,16 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     }
   }
   // implied options...
-  if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint)
+  if (opts.quantifiers.cbqiModeWasSetByUser || opts.quantifiers.cbqiTConstraint)
   {
-    opts.quantifiers.quantConflictFind = true;
+    opts.quantifiers.conflictBasedInst = true;
   }
   if (opts.quantifiers.cegqiNestedQE)
   {
     opts.quantifiers.prenexQuantUser = true;
     if (!opts.quantifiers.preSkolemQuantWasSetByUser)
     {
-      opts.quantifiers.preSkolemQuant = true;
+      opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::ON;
     }
   }
   // for induction techniques
@@ -1547,7 +1549,8 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
     }
   }
   // can't pre-skolemize nested quantifiers without UF theory
-  if (!logic.isTheoryEnabled(THEORY_UF) && opts.quantifiers.preSkolemQuant)
+  if (!logic.isTheoryEnabled(THEORY_UF)
+      && opts.quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
   {
     if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
     {
@@ -1590,7 +1593,7 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
     // optimization: apply preskolemization, makes it succeed more often
     if (!opts.quantifiers.preSkolemQuantWasSetByUser)
     {
-      opts.quantifiers.preSkolemQuant = true;
+      opts.quantifiers.preSkolemQuant = options::PreSkolemQuantMode::ON;
     }
     if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
     {
@@ -1602,9 +1605,9 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
   {
     opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE;
   }
-  if (!opts.quantifiers.quantConflictFindWasSetByUser)
+  if (!opts.quantifiers.conflictBasedInstWasSetByUser)
   {
-    opts.quantifiers.quantConflictFind = false;
+    opts.quantifiers.conflictBasedInst = false;
   }
   if (!opts.quantifiers.instNoEntailWasSetByUser)
   {
@@ -1615,11 +1618,6 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
     // should use full effort cbqi for single invocation and repair const
     opts.quantifiers.cegqiFullEffort = true;
   }
-  if (opts.quantifiers.sygusRew)
-  {
-    opts.quantifiers.sygusRewSynth = true;
-    opts.quantifiers.sygusRewVerify = true;
-  }
   if (opts.quantifiers.sygusRewSynthInput)
   {
     // If we are using synthesis rewrite rules from input, we use
@@ -1685,15 +1683,7 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
   // do not miniscope
   if (!opts.quantifiers.miniscopeQuantWasSetByUser)
   {
-    opts.quantifiers.miniscopeQuant = false;
-  }
-  if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser)
-  {
-    opts.quantifiers.miniscopeQuantFreeVar = false;
-  }
-  if (!opts.quantifiers.quantSplitWasSetByUser)
-  {
-    opts.quantifiers.quantSplit = false;
+    opts.quantifiers.miniscopeQuant = options::MiniscopeQuantMode::OFF;
   }
   // do not do macros
   if (!opts.quantifiers.macrosQuantWasSetByUser)
index 9e38ed3ece5cba7cd7ec7bf3d6d2e899974e3408..1e5555e9bc6552ec250b55d704126251e846797f 100644 (file)
@@ -278,9 +278,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
               {
                 Assert(eqt.getType() == tn);
                 registerPattern(eqt, tn);
-                if (isUniversalLessThan(eqt, t)
-                    || (options().quantifiers.conjectureUeeIntro
-                        && d_pattern_fun_sum[t] >= d_pattern_fun_sum[eqt]))
+                if (isUniversalLessThan(eqt, t))
                 {
                   setUniversalRelevant(eqt);
                   assertEq = true;
index 9e845827fadf2b38dacfac39b7d76f07daf091a1..96944fde12c020d4839bdd0945c33330555b033f 100644 (file)
@@ -339,14 +339,10 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
             {
               arg_to_rep[r] = index;
               // function applied to single value, can either use variable or
-              // value at this argument position
+              // value at this argument position. We give priority to variables,
+              // although this order could be changed.
               d_arg_vector[vnum][index].push_back(bv_at_index);
               d_arg_vector[vnum][index].push_back(itf->second);
-              if (!options().quantifiers.hoMatchingVarArgPriority)
-              {
-                std::reverse(d_arg_vector[vnum][index].begin(),
-                             d_arg_vector[vnum][index].end());
-              }
               Trace("ho-unif-debug") << " = { self, " << itf->second << " } "
                                      << std::endl;
             }
index d09b90b6b57401fab617959c2ecbb2221882c1e8..e1e41c99702a4dc2bc3d0c5ed3a17130cb448c9a 100644 (file)
@@ -181,7 +181,7 @@ int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn)
     if( n.hasAttribute(InstLevelAttribute()) ){
       return n.getAttribute(InstLevelAttribute());
     }
-    return options().quantifiers.instLevelInputOnly ? -1 : 0;
+    return -1;
   }
   else if (options().quantifiers.quantRepMode == options::QuantRepMode::FIRST)
   {
index 1ccdd52e7951a867838bc169a37c7cca064b5542..07241e150bad143e93544198524372738f8510ec 100644 (file)
@@ -294,18 +294,11 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
     }
     else
     {
-      if (options().quantifiers.fmfFreshDistConst)
-      {
-        mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn);
-      }
-      else
-      {
-        // The model basis term cannot be an interpreted function, or else we
-        // may produce an inconsistent model by choosing an arbitrary
-        // equivalence class for it. Hence, we require that it be an existing or
-        // fresh variable.
-        mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
-      }
+      // The model basis term cannot be an interpreted function, or else we
+      // may produce an inconsistent model by choosing an arbitrary
+      // equivalence class for it. Hence, we require that it be an existing or
+      // fresh variable.
+      mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
     }
     ModelBasisAttribute mba;
     mbt.setAttribute(mba, true);
index 8931ee14dd023b5997f907e05121f56be4f6f064..351a5e43e00fd31e745b9ed068d42eb867c5f73d 100644 (file)
@@ -488,7 +488,9 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
       if( !nv.isConst() ){
         Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
       }
-      Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
+      Node en = hasNonStar ? n
+                           : NodeManager::currentNM()->mkNode(APPLY_UF,
+                                                              entry_children);
       if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
         Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
         conds.push_back(n);
@@ -1378,10 +1380,6 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const
   return fm->getFunctionValue(op, argPrefix);
 }
 
-
-bool FullModelChecker::useSimpleModels() {
-  return options().quantifiers.fmfFmcSimple;
-}
 void FullModelChecker::registerQuantifiedFormula(Node q)
 {
   if (d_quant_cond.find(q) != d_quant_cond.end())
index dc5c8979176d74e1979640540fdca1239b8784bb..604d8e4eb56a045bdfcfca0c21c85de0a32f4dc6 100644 (file)
@@ -61,7 +61,6 @@ QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q)
 
   registerNode( qn, true, true );
 
-
   Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
   d_mg.reset(new MatchGen(p, this, qn));
 
@@ -76,12 +75,13 @@ QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q)
           is_tsym = true;
           d_tsym_vars.push_back( j );
         }
-        if (!is_tsym || options().quantifiers.qcfTConstraint)
+        if (!is_tsym || options().quantifiers.cbqiTConstraint)
         {
           d_var_mg[j] = std::make_unique<MatchGen>(p, this, d_vars[j], true);
         }
         if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
-          Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
+          Trace("qcf-invalid")
+              << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
           d_mg->setInvalid();
           break;
         }else{
@@ -95,16 +95,19 @@ QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q)
       d_mg->determineVariableOrder(bvars);
     }
   }else{
-    Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
+    Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed."
+                         << std::endl;
   }
-  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
+  Trace("qcf-qregister-summary")
+      << "QCF register : " << (d_mg->isValid() ? "VALID " : "INVALID") << " : "
+      << q << std::endl;
 
-  if (d_mg->isValid() && options().quantifiers.qcfEagerCheckRd)
+  if (d_mg->isValid() && options().quantifiers.cbqiEagerCheckRd)
   {
     //optimization : record variable argument positions for terms that must be matched
     std::vector< TNode > vars;
     //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
-    if (options().quantifiers.qcfSkipRd)
+    if (options().quantifiers.cbqiSkipRd)
     {
       for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
         vars.push_back( d_vars[j] );
@@ -120,14 +123,16 @@ QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q)
     {
       TNode f = p->getTermDatabase()->getMatchOperator( v );
       if( !f.isNull() ){
-        Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
+        Trace("qcf-opt") << "Record variable argument positions in " << v
+                         << ", op=" << f << "..." << std::endl;
         for (size_t k = 0, vnchild = v.getNumChildren(); k < vnchild; k++)
         {
           Node n = v[k];
           std::map<TNode, size_t>::iterator itv = d_var_num.find(n);
           if( itv!=d_var_num.end() ){
             std::vector<size_t>& vrd = d_var_rel_dom[itv->second][f];
-            Trace("qcf-opt") << "  arg " << k << " is var #" << itv->second << std::endl;
+            Trace("qcf-opt")
+                << "  arg " << k << " is var #" << itv->second << std::endl;
             if (std::find(vrd.begin(), vrd.end(), k) == vrd.end())
             {
               vrd.push_back(k);
@@ -174,7 +179,8 @@ void QuantInfo::getPropagateVars(std::vector<TNode>& vars,
       Assert(n.getKind() != IMPLIES);
       QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
     }
-    Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
+    Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol
+                           << ", rec = " << rec << std::endl;
     if( rec ){
       for (const Node& nc : n)
       {
@@ -216,7 +222,7 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
           }
           registerNode(n[0], false, pol, beneathQuant);
         }
-        else if (options().quantifiers.qcfTConstraint)
+        else if (options().quantifiers.cbqiTConstraint)
         {
           // a theory-specific predicate
           for (unsigned i = 0; i < n.getNumChildren(); i++)
@@ -230,9 +236,6 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant )
         bool newHasPol;
         bool newPol;
         QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
-        //QcfNode * qcfc = new QcfNode( d_c );
-        //qcfc->d_parent = qcf;
-        //qcf->d_child[i] = qcfc;
         registerNode( n[i], newHasPol, newPol, beneathQuant );
       }
     }
@@ -647,7 +650,7 @@ bool QuantInfo::isMatchSpurious()
 
 bool QuantInfo::isTConstraintSpurious(const std::vector<Node>& terms)
 {
-  if (options().quantifiers.qcfEagerTest)
+  if (options().quantifiers.cbqiEagerTest)
   {
     EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
     //check whether the instantiation evaluates as expected
@@ -665,10 +668,12 @@ bool QuantInfo::isTConstraintSpurious(const std::vector<Node>& terms)
       subs[d_extra_var[i]] = n;
     }
     if (d_parent->atConflictEffort()) {
-      Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
+      Trace("qcf-instance-check")
+          << "Possible conflict instance for " << d_q << " : " << std::endl;
       if (!echeck->isEntailed(d_q[1], subs, false, false))
       {
-        Trace("qcf-instance-check") << "...not entailed to be false." << std::endl;
+        Trace("qcf-instance-check")
+            << "...not entailed to be false." << std::endl;
         return true;
       }
     }else{
@@ -676,11 +681,12 @@ bool QuantInfo::isTConstraintSpurious(const std::vector<Node>& terms)
       // combination of known terms under the current substitution. We use
       // the helper method evaluateTerm from the entailment check utility.
       Node inst_eval = echeck->evaluateTerm(
-          d_q[1], subs, false, options().quantifiers.qcfTConstraint, true);
+          d_q[1], subs, false, options().quantifiers.cbqiTConstraint, true);
       if( TraceIsOn("qcf-instance-check") ){
         Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
         Trace("qcf-instance-check") << "  " << terms << std::endl;
-        Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
+        Trace("qcf-instance-check")
+            << "...evaluates to " << inst_eval << std::endl;
       }
       // If it is the case that instantiation can be rewritten to a Boolean
       // combination of terms that exist in the current context, then inst_eval
@@ -773,7 +779,7 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
     doFail = true;
     success = false;
   }else{
-    if (isBaseMatchComplete() && options().quantifiers.qcfEagerTest)
+    if (isBaseMatchComplete() && options().quantifiers.cbqiEagerTest)
     {
       return true;
     }
@@ -786,7 +792,9 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
       if( v==d_vars[index] ){
         slv_v = index;
       }
-      Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
+      Trace("qcf-tconstraint-debug")
+          << "Solve " << d_vars[index] << " = " << v << " "
+          << d_vars[index].getKind() << std::endl;
       if (d_vars[index].getKind() == ADD || d_vars[index].getKind() == MULT)
       {
         Kind k = d_vars[index].getKind();
@@ -798,7 +806,8 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
             if( vv==vi ){
               //we will assign this
               if( slv_v==-1 ){
-                Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
+                Trace("qcf-tconstraint-debug")
+                    << "...will solve for var #" << vn << std::endl;
                 slv_v = vn;
                 if (!d_parent->atConflictEffort())
                 {
@@ -808,7 +817,8 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
                 Node z = d_parent->getZero(d_vars[index].getType(), k);
                 if( !z.isNull() ){
                   size_t vni = static_cast<size_t>(vn);
-                  Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
+                  Trace("qcf-tconstraint-debug")
+                      << "...set " << d_vars[vn] << " = " << z << std::endl;
                   assigned.push_back(vni);
                   if (!setMatch(vni, z, false, true))
                   {
@@ -818,7 +828,8 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
                 }
               }
             }else{
-              Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;
+              Trace("qcf-tconstraint-debug")
+                  << "...sum value " << vv << std::endl;
               children.push_back( vv );
             }
           }else{
@@ -854,7 +865,8 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
             }
             if( !sum.isNull() ){
               assigned.push_back( slv_v );
-              Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
+              Trace("qcf-tconstraint-debug")
+                  << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
               if (!setMatch(slv_v, sum, false, true))
               {
                 success = false;
@@ -904,7 +916,8 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
   }
 
   if( !d_unassigned.empty() && ( success || doContinue ) ){
-    Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size() << ")..." << std::endl;
+    Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size()
+                       << ")..." << std::endl;
     do {
       if( doFail ){
         Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
@@ -934,18 +947,22 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
           if( !doFail ){
             if( d_una_index<d_unassigned_nvar ){
               if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
-                Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
+                Trace("qcf-check-unassign")
+                    << "Succeeded, variable unconstrained at " << d_una_index
+                    << std::endl;
                 d_una_index++;
               }
               else if (d_var_mg[d_unassigned[d_una_index]]->getNextMatch())
               {
-                Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;
+                Trace("qcf-check-unassign") << "Succeeded match with mg at "
+                                            << d_una_index << std::endl;
                 d_una_index++;
               }
               else
               {
                 failed = true;
-                Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;
+                Trace("qcf-check-unassign")
+                    << "Failed match with mg at " << d_una_index << std::endl;
               }
             }else{
               Assert(doFail || d_una_index + 1 == d_una_eqc_count.size());
@@ -961,19 +978,22 @@ bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
                         d_unassigned[d_una_index], eqcs[currIndex], true, true))
                 {
                   d_match_term[d_unassigned[d_una_index]] = TNode::null();
-                  Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
+                  Trace("qcf-check-unassign")
+                      << "Succeeded match " << d_una_index << std::endl;
                   d_una_index++;
                 }
                 else
                 {
-                  Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;
+                  Trace("qcf-check-unassign")
+                      << "Failed match " << d_una_index << std::endl;
                   invalidMatch = true;
                 }
               }
               else
               {
                 failed = true;
-                Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;
+                Trace("qcf-check-unassign")
+                    << "No more matches " << d_una_index << std::endl;
               }
             }
           }
@@ -1105,8 +1125,9 @@ MatchGen::MatchGen(QuantConflictFind* p, QuantInfo* qi, Node n, bool isVar)
   //initialize temporary
   d_child_counter = -1;
   d_use_children = true;
-  
-  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
+
+  Trace("qcf-qregister-debug")
+      << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
   std::vector< Node > qni_apps;
   d_qni_size = 0;
   if( isVar ){
@@ -1174,7 +1195,9 @@ MatchGen::MatchGen(QuantConflictFind* p, QuantInfo* qi, Node n, bool isVar)
         }else if( d_n.getKind()==BOUND_VARIABLE ){
           Assert(d_n.getType().isBoolean());
           d_type = typ_bool_var;
-        }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
+        }
+        else if (d_n.getKind() == EQUAL || options::cbqiTConstraint())
+        {
           for (unsigned i = 0; i < d_n.getNumChildren(); i++)
           {
             if (expr::hasBoundVar(d_n[i]))
@@ -1208,7 +1231,6 @@ MatchGen::MatchGen(QuantConflictFind* p, QuantInfo* qi, Node n, bool isVar)
   Trace("qcf-qregister-debug")  << "Done make match gen " << n << ", type = ";
   debugPrintType( "qcf-qregister-debug", d_type );
   Trace("qcf-qregister-debug") << std::endl;
-
 }
 
 void MatchGen::collectBoundVar(Node n,
@@ -1234,7 +1256,8 @@ void MatchGen::collectBoundVar(Node n,
 
 void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
 {
-  Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl;
+  Trace("qcf-qregister-debug") << "Determine variable order " << d_n
+                               << ", #bvars = " << bvars.size() << std::endl;
   bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL );
   if( isComm ){
     std::map< int, std::vector< int > > c_to_vars;
@@ -1264,7 +1287,8 @@ void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
       }
     }
     //children that bind no unbound variable, then the most number of bound, unbound variables go first
-    Trace("qcf-qregister-vo") << "Variable order for " << d_n << " : " << std::endl;
+    Trace("qcf-qregister-vo")
+        << "Variable order for " << d_n << " : " << std::endl;
     size_t nqvars = d_qi->d_vars.size();
     do {
       int min_score0 = -1;
@@ -1273,12 +1297,17 @@ void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
       for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
       {
         if( !assigned[i] ){
-          Trace("qcf-qregister-debug2") << "Child " << i << " has b/ub : " << vb_count[i] << "/" << vu_count[i] << std::endl;
+          Trace("qcf-qregister-debug2")
+              << "Child " << i << " has b/ub : " << vb_count[i] << "/"
+              << vu_count[i] << std::endl;
           int score0 = 0;//has_nested[i] ? 0 : 1;
           int score;
-          if( !options::qcfVoExp() ){
+          if (!options::cbqiVoExp())
+          {
             score = vu_count[i];
-          }else{
+          }
+          else
+          {
             score = vu_count[i] == 0 ? 0
                                      : (1 + nqvars * (nqvars - vb_count[i])
                                         + (nqvars - vu_count[i]));
@@ -1293,8 +1322,11 @@ void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
       Trace("qcf-qregister-vo")
           << "  " << d_children_order.size() + 1 << ": "
           << d_children[min_score_index]->getNode() << " : ";
-      Trace("qcf-qregister-vo") << vu_count[min_score_index] << " " << vb_count[min_score_index] << " " << has_nested[min_score_index] << std::endl;
-      Trace("qcf-qregister-debug") << "...assign child " << min_score_index << std::endl;
+      Trace("qcf-qregister-vo")
+          << vu_count[min_score_index] << " " << vb_count[min_score_index]
+          << " " << has_nested[min_score_index] << std::endl;
+      Trace("qcf-qregister-debug")
+          << "...assign child " << min_score_index << std::endl;
       Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl;
       Assert(min_score_index != -1);
       //add to children order
@@ -1302,7 +1334,7 @@ void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
       assigned[min_score_index] = true;
       //determine order internal to children
       d_children[min_score_index]->determineVariableOrder(bvars);
-      Trace("qcf-qregister-debug")  << "...bind variables" << std::endl;
+      Trace("qcf-qregister-debug") << "...bind variables" << std::endl;
       //now, make it a bound variable
       if( vu_count[min_score_index]>0 ){
         for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
@@ -1317,9 +1349,11 @@ void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
           }
         }
       }
-      Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
+      Trace("qcf-qregister-debug")
+          << "...done assign child " << min_score_index << std::endl;
     }while( d_children_order.size()!=d_children.size() );
-    Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;
+    Trace("qcf-qregister-debug")
+        << "Done assign variable ordering for " << d_n << std::endl;
   }else{
     for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
     {
@@ -1416,7 +1450,7 @@ void MatchGen::reset(bool tgt)
       d_child_counter = 0;
     }
   }
-  else if (d_qi->isBaseMatchComplete() && options::qcfEagerTest())
+  else if (d_qi->isBaseMatchComplete() && options::cbqiEagerTest())
   {
     d_use_children = false;
     d_child_counter = 0;
@@ -1542,7 +1576,6 @@ void MatchGen::reset(bool tgt)
       success = addc!=-1;
       //if successful and non-redundant, store that we need to cleanup this
       if( addc==1 ){
-        //Trace("qcf-explain") << "       reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;
         for (size_t i = 0; i < 2; i++)
         {
           if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
@@ -1567,8 +1600,7 @@ void MatchGen::reset(bool tgt)
       if( d_tgt && d_n.getKind()==FORALL ){
         //fail
       }
-      else if (d_n.getKind() == FORALL && d_parent->atConflictEffort()
-               && !options::qcfNestedConflict())
+      else if (d_n.getKind() == FORALL && d_parent->atConflictEffort())
       {
         //fail
       }
@@ -2044,16 +2076,18 @@ bool MatchGen::doMatching()
   return !d_qn.empty();
 }
 
-void MatchGen::debugPrintType( const char * c, short typ) {
-    switch( typ ){
-    case typ_invalid: Trace(c) << "invalid";break;
-    case typ_ground: Trace(c) << "ground";break;
-    case typ_eq: Trace(c) << "eq";break;
-    case typ_pred: Trace(c) << "pred";break;
-    case typ_formula: Trace(c) << "formula";break;
-    case typ_var: Trace(c) << "var";break;
-    case typ_bool_var: Trace(c) << "bool_var";break;
-    }
+void MatchGen::debugPrintType(const char* c, short typ)
+{
+  switch (typ)
+  {
+    case typ_invalid: Trace(c) << "invalid"; break;
+    case typ_ground: Trace(c) << "ground"; break;
+    case typ_eq: Trace(c) << "eq"; break;
+    case typ_pred: Trace(c) << "pred"; break;
+    case typ_formula: Trace(c) << "formula"; break;
+    case typ_var: Trace(c) << "var"; break;
+    case typ_bool_var: Trace(c) << "bool_var"; break;
+  }
 }
 
 void MatchGen::setInvalid() {
@@ -2143,21 +2177,7 @@ void QuantConflictFind::registerQuantifier( Node q ) {
 //-------------------------------------------------- check function
 
 bool QuantConflictFind::needsCheck( Theory::Effort level ) {
-  bool performCheck = false;
-  if (options().quantifiers.quantConflictFind && !d_conflict)
-  {
-    if( level==Theory::EFFORT_LAST_CALL ){
-      performCheck =
-          options().quantifiers.qcfWhenMode == options::QcfWhenMode::LAST_CALL;
-    }else if( level==Theory::EFFORT_FULL ){
-      performCheck =
-          options().quantifiers.qcfWhenMode == options::QcfWhenMode::DEFAULT;
-    }else if( level==Theory::EFFORT_STANDARD ){
-      performCheck =
-          options().quantifiers.qcfWhenMode == options::QcfWhenMode::STD;
-    }
-  }
-  return performCheck;
+  return !d_conflict && (level == Theory::EFFORT_FULL);
 }
 
 void QuantConflictFind::reset_round( Theory::Effort level ) {
@@ -2205,7 +2225,7 @@ inline QuantConflictFind::Effort QcfEffortStart() {
 // Returns the beginning of a range of efforts. The value returned is included
 // in the range.
 inline QuantConflictFind::Effort QcfEffortEnd() {
-  return options::qcfMode() == options::QcfMode::PROP_EQ
+  return options::cbqiMode() == options::QcfMode::PROP_EQ
              ? QuantConflictFind::EFFORT_PROP_EQ
              : QuantConflictFind::EFFORT_CONFLICT;
 }
@@ -2215,7 +2235,7 @@ inline QuantConflictFind::Effort QcfEffortEnd() {
 /** check */
 void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
 {
-  CodeTimer codeTimer(d_qstate.getStats().d_qcf_time);
+  CodeTimer codeTimer(d_qstate.getStats().d_cbqi_time);
   if (quant_e != QEFFORT_CONFLICT)
   {
     return;
@@ -2427,7 +2447,7 @@ void QuantConflictFind::checkQuantifiedFormula(Node q,
         // ensure that quantified formulas that are more likely to have
         // conflicting instances are checked earlier.
         d_treg.getModel()->markRelevant(q);
-        if (options().quantifiers.qcfAllConflict)
+        if (options().quantifiers.cbqiAllConflict)
         {
           isConflict = true;
         }
index a81abc3a0347a797f3adfef6c0ec78bc66cc70e5..f971e431104efdb77b5a77cdf356251273c5a482 100644 (file)
@@ -51,7 +51,7 @@ void QuantifiersModules::initialize(Env& env,
 {
   // add quantifiers modules
   const Options& options = env.getOptions();
-  if (options.quantifiers.quantConflictFind)
+  if (options.quantifiers.conflictBasedInst)
   {
     d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr));
     modules.push_back(d_qcf.get());
@@ -61,7 +61,7 @@ void QuantifiersModules::initialize(Env& env,
     d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr));
     modules.push_back(d_sg_gen.get());
   }
-  if (!options.quantifiers.finiteModelFind || options.quantifiers.fmfInstEngine)
+  if (options.quantifiers.eMatching)
   {
     d_inst_engine.reset(new InstantiationEngine(env, qs, qim, qr, tr));
     modules.push_back(d_inst_engine.get());
index 321ad1717e0e8ed18f0763fb08b3b7f61b926a7c..d9d01c297ba33f70c2e7ebd57ca30d8ee7535a89 100644 (file)
@@ -127,6 +127,8 @@ Node QuantifiersPreprocess::preSkolemizeQuantifiers(
     std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>&
         visited) const
 {
+  Assert(options().quantifiers.preSkolemQuant
+         != options::PreSkolemQuantMode::OFF);
   std::pair<Node, bool> key(n, polarity);
   std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>::
       iterator it = visited.find(key);
@@ -149,8 +151,7 @@ Node QuantifiersPreprocess::preSkolemizeQuantifiers(
     }
     else if (polarity)
     {
-      if (options().quantifiers.preSkolemQuant
-          && options().quantifiers.preSkolemQuantNested)
+      if (options().quantifiers.preSkolemQuantNested)
       {
         std::vector<Node> children;
         children.push_back(n[0]);
@@ -192,7 +193,8 @@ Node QuantifiersPreprocess::preSkolemizeQuantifiers(
   Assert(n.getType().isBoolean());
   if (k == ITE || (k == EQUAL && n[0].getType().isBoolean()))
   {
-    if (options().quantifiers.preSkolemQuantAgg)
+    if (options().quantifiers.preSkolemQuant
+        == options::PreSkolemQuantMode::AGG)
     {
       Node nn;
       // must remove structure
@@ -231,7 +233,7 @@ Node QuantifiersPreprocess::preSkolemizeQuantifiers(
 TrustNode QuantifiersPreprocess::preprocess(Node n, bool isInst) const
 {
   Node prev = n;
-  if (options().quantifiers.preSkolemQuant)
+  if (options().quantifiers.preSkolemQuant != options::PreSkolemQuantMode::OFF)
   {
     if (!isInst || !options().quantifiers.preSkolemQuantNested)
     {
index 255cd77a2b2a3381c3e2e0c5e138f02385f55816..03caa0187ae81cad015d79ae8621358b228a9b6c 100644 (file)
@@ -710,7 +710,8 @@ Node QuantifiersRewriter::computeCondSplit(Node body,
       return nm->mkNode(AND, conj);
     }
   }
-  if (!d_opts.quantifiers.condVarSplitQuant)
+  if (d_opts.quantifiers.condVarSplitQuant
+      == options::CondVarSplitQuantMode::OFF)
   {
     return body;
   }
@@ -719,14 +720,15 @@ Node QuantifiersRewriter::computeCondSplit(Node body,
   // we only do this splitting if miniscoping is enabled, as this is
   // required to eliminate variables in conjuncts below. We also never
   // miniscope non-standard quantifiers, so this is also guarded here.
-  if (!d_opts.quantifiers.miniscopeQuant || !qa.isStandard())
+  if (!doMiniscopeConj(d_opts) || !qa.isStandard())
   {
     return body;
   }
 
+  bool aggCondSplit = (d_opts.quantifiers.condVarSplitQuant
+                       == options::CondVarSplitQuantMode::AGG);
   if (bk == ITE
-      || (bk == EQUAL && body[0].getType().isBoolean()
-          && d_opts.quantifiers.condVarSplitQuantAgg))
+      || (bk == EQUAL && body[0].getType().isBoolean() && aggCondSplit))
   {
     Assert(!qa.isFunDef());
     bool do_split = false;
@@ -786,7 +788,7 @@ Node QuantifiersRewriter::computeCondSplit(Node body,
             // Figure out if we should split
             // Currently we split if the aggressive option is set, or
             // if the top-level OR is binary.
-            if (d_opts.quantifiers.condVarSplitQuantAgg || size == 2)
+            if (aggCondSplit || size == 2)
             {
               do_split = true;
             }
@@ -1717,7 +1719,10 @@ Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
 }
 
 //computes miniscoping, also eliminates variables that do not occur free in body
-Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa) const
+Node QuantifiersRewriter::computeMiniscoping(Node q,
+                                             QAttributes& qa,
+                                             bool miniscopeConj,
+                                             bool miniscopeFv) const
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> args(q[0].begin(), q[0].end());
@@ -1733,8 +1738,7 @@ Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa) const
   }else if( body.getKind()==AND ){
     // aggressive miniscoping implies that structural miniscoping should
     // be applied first
-    if (d_opts.quantifiers.miniscopeQuant
-        || d_opts.quantifiers.aggressiveMiniscopeQuant)
+    if (miniscopeConj)
     {
       BoundVarManager* bvm = nm->getBoundVarManager();
       // Break apart the quantifed formula
@@ -1778,38 +1782,11 @@ Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa) const
       return retVal;
     }
   }else if( body.getKind()==OR ){
-    if (d_opts.quantifiers.quantSplit)
+    if (miniscopeFv)
     {
       //splitting subsumes free variable miniscoping, apply it with higher priority
       return computeSplit( args, body, qa );
     }
-    else if (d_opts.quantifiers.miniscopeQuantFreeVar
-             || d_opts.quantifiers.aggressiveMiniscopeQuant)
-    {
-      // aggressive miniscoping implies that free variable miniscoping should
-      // be applied first
-      Node newBody = body;
-      NodeBuilder body_split(kind::OR);
-      NodeBuilder tb(kind::OR);
-      for (const Node& trm : body)
-      {
-        if (expr::hasSubterm(trm, args))
-        {
-          tb << trm;
-        }else{
-          body_split << trm;
-        }
-      }
-      if( tb.getNumChildren()==0 ){
-        return body_split;
-      }else if( body_split.getNumChildren()>0 ){
-        newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
-        std::vector< Node > activeArgs;
-        computeArgVec2( args, activeArgs, newBody, qa.d_ipl );
-        body_split << mkForAll( activeArgs, newBody, qa );
-        return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
-      }
-    }
   }else if( body.getKind()==NOT ){
     Assert(isLiteral(body[0]));
   }
@@ -1948,7 +1925,8 @@ bool QuantifiersRewriter::doOperation(Node q,
   }
   else if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
   {
-    return d_opts.quantifiers.aggressiveMiniscopeQuant && is_std;
+    return d_opts.quantifiers.miniscopeQuant == options::MiniscopeQuantMode::AGG
+           && is_std;
   }
   else if (computeOption == COMPUTE_EXT_REWRITE)
   {
@@ -1961,13 +1939,16 @@ bool QuantifiersRewriter::doOperation(Node q,
   else if (computeOption == COMPUTE_COND_SPLIT)
   {
     return (d_opts.quantifiers.iteDtTesterSplitQuant
-            || d_opts.quantifiers.condVarSplitQuant)
+            || d_opts.quantifiers.condVarSplitQuant
+                   != options::CondVarSplitQuantMode::OFF)
            && !is_strict_trigger;
   }
   else if (computeOption == COMPUTE_PRENEX)
   {
     return d_opts.quantifiers.prenexQuant != options::PrenexQuantMode::NONE
-           && !d_opts.quantifiers.aggressiveMiniscopeQuant && is_std;
+           && d_opts.quantifiers.miniscopeQuant
+                  != options::MiniscopeQuantMode::AGG
+           && is_std;
   }
   else if (computeOption == COMPUTE_VAR_ELIMINATION)
   {
@@ -1996,8 +1977,10 @@ Node QuantifiersRewriter::computeOperation(Node f,
         return f;
       }
     }
+    bool miniscopeConj = doMiniscopeConj(d_opts);
+    bool miniscopeFv = doMiniscopeFv(d_opts);
     //return directly
-    return computeMiniscoping(f, qa);
+    return computeMiniscoping(f, qa, miniscopeConj, miniscopeFv);
   }
   std::vector<Node> args(f[0].begin(), f[0].end());
   Node n = f[1];
@@ -2055,6 +2038,21 @@ Node QuantifiersRewriter::computeOperation(Node f,
     }
   }
 }
+bool QuantifiersRewriter::doMiniscopeConj(const Options& opts)
+{
+  options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
+  return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
+         || mqm == options::MiniscopeQuantMode::CONJ
+         || mqm == options::MiniscopeQuantMode::AGG;
+}
+
+bool QuantifiersRewriter::doMiniscopeFv(const Options& opts)
+{
+  options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
+  return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
+         || mqm == options::MiniscopeQuantMode::FV
+         || mqm == options::MiniscopeQuantMode::AGG;
+}
 
 bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
   if( n.getKind()==FORALL ){
index 1aabfe3c3f1b6f0dda25d5025874878d8d9a8744..7e7dda4b71ec5fcfce9965fe578613d271576a52 100644 (file)
@@ -170,7 +170,10 @@ class QuantifiersRewriter : public TheoryRewriter
   /**
    * Compute miniscoping in quantified formula q with attributes in qa.
    */
-  Node computeMiniscoping(Node q, QAttributes& qa) const;
+  Node computeMiniscoping(Node q,
+                          QAttributes& qa,
+                          bool miniscopeConj,
+                          bool miniscopeFv) const;
   Node computeAggressiveMiniscoping(std::vector<Node>& args, Node body) const;
   /**
    * This function removes top-level quantifiers from subformulas of body
@@ -319,6 +322,10 @@ class QuantifiersRewriter : public TheoryRewriter
    * q with attributes qa.
    */
   bool doOperation(Node q, RewriteStep computeOption, QAttributes& qa) const;
+  /** Whether we should miniscope based on conjunctions based on option */
+  static bool doMiniscopeConj(const Options& opts);
+  /** Whether we should miniscope based on free variables based on option */
+  static bool doMiniscopeFv(const Options& opts);
   /**
    * Return the rewritten form of q after applying operator computeOption to it.
    */
index 8492fd62160d82ae0168a84cfda0347123a4784a..62fe96439eb309c846492c72fbc4bd5fd9eaa93f 100644 (file)
@@ -30,7 +30,7 @@ QuantifiersState::QuantifiersState(Env& env,
       d_logicInfo(logicInfo)
 {
   // allow theory combination to go first, once initially
-  d_ierCounter = options().quantifiers.instWhenTcFirst ? 0 : 1;
+  d_ierCounter = 0;
   d_ierCounterc = d_ierCounter;
   d_ierCounterLc = 0;
   d_ierCounterLastLc = 0;
index 59fdb18085cf4b96815649147732aeb71f2cabd6..6437683f73d46f4a20b6a61416d57a80283154da 100644 (file)
@@ -24,8 +24,8 @@ namespace quantifiers {
 QuantifiersStatistics::QuantifiersStatistics()
     : d_time(smtStatisticsRegistry().registerTimer(
         "theory::QuantifiersEngine::time")),
-      d_qcf_time(smtStatisticsRegistry().registerTimer(
-          "theory::QuantifiersEngine::time_qcf")),
+      d_cbqi_time(smtStatisticsRegistry().registerTimer(
+          "theory::QuantifiersEngine::time_conflict_based_inst")),
       d_ematching_time(smtStatisticsRegistry().registerTimer(
           "theory::QuantifiersEngine::time_ematching")),
       d_num_quant(smtStatisticsRegistry().registerInt(
index 438efd30f28d71253d696de4a4e5f453f634c728..0ece9aedf93a86b02f8a8af9f2f3d043d7e912c5 100644 (file)
@@ -33,7 +33,7 @@ class QuantifiersStatistics
  public:
   QuantifiersStatistics();
   TimerStat d_time;
-  TimerStat d_qcf_time;
+  TimerStat d_cbqi_time;
   TimerStat d_ematching_time;
   IntStat d_num_quant;
   IntStat d_instantiation_rounds;
index a7df0bb51b4369c61c45f7554aa77c19b9d413ac..284d3aaf84cbb4c314fd0262ccf07474f2d4b4b4 100644 (file)
@@ -236,9 +236,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
                       options().quantifiers.sygusRepairConstTimeoutWasSetByUser,
                       options().quantifiers.sygusRepairConstTimeout);
   // renable options disabled by sygus
-  repcChecker->setOption("miniscope-quant", "true");
-  repcChecker->setOption("miniscope-quant-fv", "true");
-  repcChecker->setOption("quant-split", "true");
+  repcChecker->setOption("miniscope-quant", "conj-and-fv");
   repcChecker->assertFormula(fo_body);
   // check satisfiability
   Result r = repcChecker->checkSat();
index 8ecfc4e50ddd4259ea696b3afdfc93931b3cefd6..712cf6bc0930ffe8ef4110260ebd5ee3cf44afdc 100644 (file)
@@ -996,7 +996,7 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
   Assert(varlist.size() == args.size());
 
   Node res;
-  if (tryEval && options().quantifiers.sygusEvalOpt)
+  if (tryEval)
   {
     // Try evaluating, which is much faster than substitution+rewriting.
     // This may fail if there is a subterm of bn under the
index ae74b94a17723ad43beb1173c40aeec2a6a1bc49..208e750f1aa8f76b93b9fe5523a77f8592e180ac 100644 (file)
@@ -831,12 +831,8 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr, std::ostream& out)
     out << ptOut.str();
     Assert(bve != bvre);
     out << "where they evaluate to " << bve << " and " << bvre << std::endl;
-
-    if (options().quantifiers.sygusRewVerifyAbort)
-    {
-      AlwaysAssert(false)
-          << "--sygus-rr-verify detected unsoundness in the rewriter!";
-    }
+    AlwaysAssert(false)
+        << "--sygus-rr-verify detected unsoundness in the rewriter!";
   }
 }
 
index 767c74c924740a587f3b4c0a7ec96a91ac54f54b..39729bc1518d7672a6bba4c503d62408960198dd 100644 (file)
@@ -508,11 +508,10 @@ bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
         return false;
       }
     }else{
-      if (options().quantifiers.instLevelInputOnly)
-      {
-        Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
-        return false;
-      }
+      Trace("inst-add-debug")
+          << "Term " << n << " does not have an instantiation level."
+          << std::endl;
+      return false;
     }
   }
   // it cannot have instantiation constants, which originate from
index e5d019a76045c79f8c275c058f91185f13a32ded..33935511cdf21533abe8e9adabde2c41e2753393 100644 (file)
@@ -168,8 +168,7 @@ void QuantifiersEngine::ppNotifyAssertions(
   Trace("quant-engine-proc")
       << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
       << std::endl;
-  if (options().quantifiers.instLevelInputOnly
-      && options().quantifiers.instMaxLevel != -1)
+  if (options().quantifiers.instMaxLevel != -1)
   {
     for (const Node& a : assertions)
     {
index 273b3364c259906aee726a1207727244d9dde4b0..7b1facde1646776e8c409cb1dfdc61c271ccfc8a 100644 (file)
@@ -82,7 +82,10 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
           env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_extTheory),
       d_rsolver(
           env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
-      d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()),
+      d_regexp_elim(
+          options().strings.regExpElim == options::RegExpElimMode::AGG,
+          d_pnm,
+          userContext()),
       d_stringsFmf(env, valuation, d_termReg),
       d_strat(d_env),
       d_absModelCounter(0),
@@ -1174,7 +1177,8 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
   }
   TrustNode ret;
   Node atomRet = atom;
-  if (options().strings.regExpElim && atom.getKind() == STRING_IN_REGEXP)
+  if (options().strings.regExpElim != options::RegExpElimMode::OFF
+      && atom.getKind() == STRING_IN_REGEXP)
   {
     // aggressive elimination of regular expression membership
     ret = d_regexp_elim.eliminateTrusted(atomRet);
index 9a36d87a6818e08c45c183e5cbf3fee5cc611f34..b0de9c7a5eed28d01429ed7cbb099fc8bb9cf4ad 100644 (file)
@@ -2,7 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
 (declare-fun r6 () Real)
 (assert (= 0.0 (cos r6)))
 (check-sat)
index 3665d6a554d1140c39d88d89df5995752b9ebc88..60269f4728872aa842f8913aee4413efc7424f70 100644 (file)
@@ -2,7 +2,7 @@
 ; EXPECT: sat
 ; EXPECT: sat
 (set-logic ALL)
-(set-option :miniscope-quant false)
+(set-option :miniscope-quant off)
 (declare-fun i2 () Int)
 (declare-fun v6 () Bool)
 (declare-sort S2 0)
index fb903fb9f5ebbb78046646e9e40345cfdc3a52c4..42ca73d3ae330789481295450f1e4550b00fe1fe 100644 (file)
@@ -2,7 +2,7 @@
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
 (declare-fun r3 () Real)
 (assert (= 0.0 (+ (- r3) (cos r3) (- 1.0))))
 (check-sat)
index cc89b78293416a1a7626acb87bc90a40082ab5bd..7424bf960aabbf7c83ac783b36de33e00a4d876b 100644 (file)
@@ -2,7 +2,7 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: unsat-core
 (set-logic ALL)
-(set-option :pre-skolem-quant true)
+(set-option :pre-skolem-quant on)
 (declare-fun v7 () Bool)
 (assert (forall ((q49 Bool) (q55 Bool)) (xor v7 (exists ((q49 Bool)) (xor v7 q49 q49)) v7 (= q55 q49))))
 (check-sat)
index f75b1b6428fa9bee41ed660550fd2ab7c3d9c329..f3ba204570b61e95584c3c3c932eb6cf909d88dc 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --re-elim --strings-exp
+; COMMAND-LINE: --re-elim=on --strings-exp
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-fun a () String)
index a11e5ae6472d3e82d86926187004c6a1b33c94fb..f2dafa46da4244dc65c76ea8c55094ce14ce0d6f 100644 (file)
@@ -1,7 +1,6 @@
 (set-logic ALL)
 (set-info :status sat)
-(set-option :re-elim-agg true)
-(set-option :re-elim true)
+(set-option :re-elim agg)
 (declare-fun str9 () String)
 (assert (str.in_re str9 (re.* (re.union re.allchar (str.to_re "lE")))))
 (check-sat)
index 648a1b11103f374b48e14c757c7b218acc0b4b5c..b1a07413b9b883c4159e9b7f8429116686c391a6 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-re-elim
+; COMMAND-LINE: --strings-exp
 (set-info :status unsat)
 (set-logic ALL)
 (declare-const actionName String)
index 20ac8f4e497db1683407db3bc53ea6a32b3cec0b..70bb1c68ac1160b2fbbf7dd8d5bad4520358f225 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-re-elim
+; COMMAND-LINE: --strings-exp
 (set-info :status sat)
 (set-logic QF_SLIA)
 (declare-const x String)
index 1a7950a6d1395b6f2b7774438b071737e34f7b98..3b9e821f0f2b21ebd6bd0982eae19e989ee504a9 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine
+; COMMAND-LINE: --finite-model-find --e-matching
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
index 9cafbfc6b646af2040806f8e9725c14b83aa8a2e..2b9f93d60ce426a6cac3603dfe054659155417c1 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
+; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
index 27323526114a8a54f2a38c90b01cb05202603fcc..6b7b95230ff73dc848e1237db6685ed14632afe1 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
+; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
index beafff29ba16fab89eba9e1601a75a1423f143f3..18671b4d03470d81c312087fb74a253ffe51119a 100644 (file)
@@ -1,7 +1,7 @@
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
 (set-logic HO_ALL)
-(set-option :ag-miniscope-quant true)
+(set-option :miniscope-quant agg)
 (set-option :conjecture-gen true)
 (set-option :int-wf-ind true)
 (set-option :sygus-inference true)
index 775ed2e5de9bc2da0662da9c23430226be037501..559899ff149d2d46f44816eadfe9fe2ddffeb515 100644 (file)
@@ -1,7 +1,6 @@
 (set-logic ALL)
 (set-info :status unsat)
-(set-option :ag-miniscope-quant true)
-(set-option :qcf-nested-conflict true)
+(set-option :miniscope-quant agg)
 (set-option :macros-quant true)
 (set-option :cegqi false)
 (set-option :fmf-fun-rlv true)
index 20ab505d4494d381e462ee2edb085b631b1580ea..b123f55734e63d7c27afd0c5227670002e5f170c 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --qcf-tconstraint
+; COMMAND-LINE: --cbqi-tconstraint
 ; EXPECT: unsat
 (set-logic AUFLIA)
 (set-info :source | 
index a5e893d9b9ebfb2c2386b025bd6aa93e8aca5619..d489b0c89f0d3da049fb9ec594956a9358c47c92 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --qcf-tconstraint
+; COMMAND-LINE: --cbqi-tconstraint
 ; EXPECT: unsat
 (set-logic AUFLIRA)
 (set-info :source |http://proval.lri.fr/why-benchmarks |)
index 614a83f2b2d52479866ccf530b486ebc0c580e92..f723e2d00e5e5ca7579abec16de20e8a975d6d17 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --sygus-simple-sym-break=none
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=3 --sygus-simple-sym-break=none
 ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
index 4cf4e3488b11ea092ee16b3d2d829735be42b707..f2b1fabf2372fb7aa1ce2628dcf8b5c28d990bbf 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --no-sygus-rr-synth-check
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=1 --sygus-simple-sym-break=none --no-sygus-rr-synth-check
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
index af954cbb1ade3914f1a2a8d12702866e19b458ab..9064d0064efd327a3a2640373b7a92776584a2e0 100644 (file)
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-simple-sym-break=none
-; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=2 --sygus-simple-sym-break=none
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-synth-check
 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite|\(rewrite)'
 ; EXIT: 1
index ad8635ca8851e6a48d6e8c955f1f4747ab6a53ea..4407043f2287e3d37632715aec4e60b4ce616b72 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-simple-sym-break=none --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1
index 33caed2e919ea9599cce73e988d89833ce2af156..78e8b4fb954ce239b80e5a5740a834b937d48b73 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-simple-sym-break=none --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1
index 815cb70a508430a91384b299f1f30b5201d74b45..9040ab252d77f35df7b593b2cc41c820c330de7b 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=1 --sygus-simple-sym-break=none
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
index 01f7aefe021ae5dcd274c8fc7143599c1641b303..f7bbb1169b846af62a2acfc362af3c17306f451a 100644 (file)
@@ -2,7 +2,7 @@
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
 (declare-fun e!0 () (Seq Bool))
 (assert (= e!0 seq.empty))
 (assert (seq.nth e!0 0))
index a57915b446cc84079c81fbf5d9eef19b311f0a0d..289ea093126d5245ec6544c00a930b0cca15dccd 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
 ; EXPECT: unsat
 (set-logic QF_SLIA)
 
index e28f5dcb51febb5404f3ab21bbe7bb6c4f8cf2ef..91da234abc17c495fddd5ff7adcbf1b3e11b6073 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim
+; COMMAND-LINE: --strings-exp --re-elim=on
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-const a String)
index cbca77783ec7713fe19b3ae7f576bbc2b723f74a..368b4fc87f5c3fb60682048154bb08d459df0ff4 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-fun a () String)
index 8de99a334ad87972269c155e841a90abaa3df22e..f9f7dea2249cfd545789be1e03c19f69fed75c6e 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun x () String)
index c4b6a497bbf2cacead26d1003a5b1513ff665fd8..bc1d4bbd9d8b925af3a20fa283e4ce3d688e8ba5 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --strings-fmf --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --strings-fmf --re-elim=agg
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun a () String)
index 66b7dd64eb56d27333d978149b3777cf6ee2676f..22513c99b24f9e58da9af059ad6a2dccbd7db63e 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun a () String)
index 13677838bf06d19fa7652029db095504abf96bf0..72cb45af4c177f2dd18c71728c75bf1d72a34dbc 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun a () String)
index 36162852fb1631f4b54e564c8a32b425cdb325d0..c6fa580f00ed73960b3fa546d5da84e8f6bd7169 100644 (file)
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --strings-exp
-; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; COMMAND-LINE: --strings-exp --re-elim=agg
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (declare-fun a () String)
index 1e3f3cb96da107323811d2fc2bad40ac5127eca0..356ce9ba7341ce64ddb9785b2b1a41547ed26acf 100644 (file)
@@ -2,7 +2,7 @@
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :strings-exp true)
-(set-option :re-elim true)
+(set-option :re-elim on)
 (declare-const actionName String)
 (declare-const actionNamespace String)
 
index ad1e4edf5b863f8d55c0e0e1056123ae9e87291b..4b74bfe2088e3ace52e643f9ba352f389dbe4692 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim
+; COMMAND-LINE: --strings-exp --re-elim=on
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic ALL)
index c74765108d7e696c140347a4e381916cea8d6291..2ffe62aad984dc7c1f82a5852057da3cf464a6ee 100644 (file)
@@ -2,7 +2,7 @@
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :strings-exp true)
-(set-option :re-elim true)
+(set-option :re-elim on)
 (declare-const actionName String)
 (declare-const actionNamespace String)
 (declare-const example_key String)
index cd19dc114e44b688c9f18278e9895935c25323b9..1894e6987d80162609d9ceae634c50951b07c615 100644 (file)
@@ -2,8 +2,7 @@
 (set-info :status sat)
 (set-option :produce-models true)
 (set-option :strings-exp true)
-(set-option :re-elim true)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
 (declare-fun a () String)
 (assert (str.in_re a (re.++ (re.+ (str.to_re "AB")) (str.to_re "B"))))
 (assert (<= (str.len a) 4))
index 86a08162a9231d920fa6c0c061f51ad2c24e618c..2f3ccc6e9e086d6a30b767bde3acdf5afe09c2e9 100644 (file)
@@ -2,7 +2,7 @@
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
-(set-option :re-elim false)
+(set-option :re-elim off)
 (declare-fun x () String)
 (assert (let ((_let_0 (re.* re.allchar ))) (and (not (= (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "A" (str.++ "B" (str.++ "C" "A")))) _let_0 re.allchar  _let_0)) (str.in_re x (re.++ _let_0 re.allchar  _let_0 re.allchar  _let_0 (str.to_re (str.++ "B" (str.++ "C" (str.++ "B" "B")))) _let_0)))) (not (= (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "C" (str.++ "B" "C"))) _let_0 (str.to_re "B") _let_0)) (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re "C") _let_0 (str.to_re (str.++ "B" (str.++ "C" "B"))) _let_0)))))))
 (check-sat)
index ca222119fb33afe18ea15a5631f129d77468333f..e9bf2c7c7b3860206586b3e51e9038e65eddf162 100644 (file)
@@ -2,7 +2,7 @@
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
-(set-option :re-elim false)
+(set-option :re-elim off)
 (declare-fun x () String)
 (assert (let ((_let_0 (re.* re.allchar ))) (and (not (= (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "B" (str.++ "A" (str.++ "C" "B")))) _let_0 re.allchar  _let_0)) (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "A" (str.++ "B" (str.++ "C" "C")))) _let_0 re.allchar  _let_0)))) (not (= (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "C" (str.++ "B" (str.++ "A" "B")))) _let_0 re.allchar  _let_0)) (str.in_re x (re.++ _let_0 re.allchar  _let_0 (str.to_re (str.++ "C" (str.++ "B" "A"))) _let_0 (str.to_re "B") _let_0)))))))
 (check-sat)
index fba863a6c8069e0f49d229217d4f57dac1c4b32e..8090d65087768dc3b4b766a9ae1a7dcc92da49a9 100644 (file)
@@ -2,7 +2,7 @@
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
 (declare-const x String)
 (declare-const y String)
 
index 80e4222249a7bd49c34e7521d03d7b40b408070e..f1bad3defdb8f0795b6742749e5c9b9d1be00f4b 100644 (file)
@@ -2,7 +2,7 @@
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :strings-exp true)
-(set-option :re-elim-agg true)
+(set-option :re-elim agg)
 (declare-const x String)
 (declare-const y String)
 (assert (str.in_re x (re.* (str.to_re "'\r''k'\n'"))))
index fc156c11641e55991ac57d8be6c7a6ad64be2cc7..9fcecd81cda735d01fd51464e06e00302238c643 100644 (file)
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-re-elim
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic ALL)
index 9504aad93e2d60962cbf2584c7a61eb09d941040..003ee08a4ab9cbf8902f62fdf0e5de7aa68a21a7 100644 (file)
@@ -2,7 +2,7 @@
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
-(set-option :re-elim true)
+(set-option :re-elim on)
 (declare-fun x () String)
 
 (assert (str.in_re x (re.++ re.allchar (str.to_re "A") re.allchar (str.to_re "B") re.allchar)))
index c8e2db922b1913a67092001eb332c0aef6d8e448..3d4951f35581db69aa31ebf0c1924f1831613201 100644 (file)
@@ -1,7 +1,7 @@
 ; EXPECT: sat
 ; COMMAND-LINE: --sygus-inference
 (set-logic ALL)
-(set-option :ag-miniscope-quant true)
+(set-option :miniscope-quant agg)
 (set-option :sygus-inference true)
 (declare-fun a () Real)
 (declare-fun b () Real)
index 0afc35e00467020cdc4cc5ff4613b9b03740167b..4e867e8aaab58dfdab1e789540a4cf66d50defda 100644 (file)
@@ -3,7 +3,7 @@
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: proof
 (set-logic ALL)
-(set-option :miniscope-quant true)
+(set-option :miniscope-quant conj-and-fv)
 (set-option :sygus-inference true)
 (set-option :var-ineq-elim-quant false)
 (set-info :status unsat)
index 37e746c3bad2fde768a99164322c60f9b7261acf..81e463da04c0bfb43f891beea7b3910974e164d0 100644 (file)
@@ -3,7 +3,7 @@
 (set-logic QF_UFNIA)
 (set-info :status sat)
 (set-option :cegqi-all true)
-(set-option :quant-split true)
+(set-option :miniscope-quant fv)
 (set-option :partial-triggers true)
 (set-option :full-saturate-quant true)
 (set-option :sygus-inference true)
index c335ca642534c6320258be96c8884c356e96968e..2aad9b2f4d50593fbefebb0fd93e671ef194a708 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim
+; COMMAND-LINE: --strings-exp --re-elim=on
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-option :produce-models true)
index 175ee5cc0dc63f6c8f1df8848e58b82fa571782f..e3b260d7c5b0c0f079450099442bea2f48170331 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --re-elim
+; COMMAND-LINE: --strings-exp --re-elim=on
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
index e0dea5d8913ec2236a7f66046f7e839897e20128..82748c169efff1ef6b5d0a3886fb00ecc61f8362 100644 (file)
@@ -2,7 +2,7 @@
 (set-logic ALL)
 (set-info :status sat)
 (set-option :strings-exp true)
-(set-option :re-elim true)
+(set-option :re-elim on)
 (declare-const x String)
 (assert (str.in_re x (re.++ (str.to_re "example-bucket/") (re.* re.allchar) (str.to_re "/") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar (str.to_re "-") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to_re "/foo"))))
 (check-sat)
index 2d911e56a4886bc4d04deea162846c3567930945..4410ec8078f5b0f72b71a4129a18565341e56657 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-rr-verify --sygus-samples=1000 --sygus-abort-size=3 --no-sygus-sym-break
 ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
index b584c0fb1abfbd0fb1d59cbc65f4cbc5d2fd2c28..2db29693d14bbe60769976d7710e1af2f318dc79 100644 (file)
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --strings-exp --no-re-elim
+; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
 (set-logic QF_SLIA)
 (set-info :status unsat)
index 227ff2ef1e9242380a682ea9db8ac1a58e772369..8ef0da5324bc84f3fe4b464acc9212e362a47aac 100755 (executable)
@@ -210,7 +210,8 @@ class SynthTester(Tester):
         return (
             benchmark_info.benchmark_ext == ".sy"
             and "--no-check-synth-sol" not in benchmark_info.command_line_args
-            and "--sygus-rr" not in benchmark_info.command_line_args
+            and "--sygus-rr-synth" not in benchmark_info.command_line_args
+            and "--sygus-rr-verify" not in benchmark_info.command_line_args
             and "--check-synth-sol" not in benchmark_info.command_line_args
         )