From: Andrew Reynolds Date: Wed, 23 Mar 2022 23:53:14 +0000 (-0500) Subject: Clean options (#8309) X-Git-Tag: cvc5-1.0.0~190 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a84ee32687d84ff18835c23196086f1ef1ba3aa;p=cvc5.git Clean options (#8309) Deletes many unnecessary options, cleans some documentation, consolidates several options. --- diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 3fe7bbd11..01aa78ba4 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -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 diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index a5e8a8a98..63b065880 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -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" diff --git a/src/options/main_options.toml b/src/options/main_options.toml index ac63b1fb1..0dbe2899f 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -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" diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index cc9847469..e6806823d 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -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" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 878ee0ac1..8e29db08e 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -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" diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml index dee134ae4..ba0a9ad1d 100644 --- a/src/options/sets_options.toml +++ b/src/options/sets_options.toml @@ -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" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index fdf65f5ec..8dee79cd3 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -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" diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 66753fc0b..52fec34af 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -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" diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 65ea84125..97de3c206 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -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; } diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index 183cec946..65a483e74 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -49,6 +49,8 @@ class ITESimp : public PreprocessingPass util::ITEUtilities d_iteUtilities; Statistics d_statistics; + + static const uint32_t zombieHuntThreshold = 524288; }; } // namespace passes diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index d5fc48f2a..f47d768c0 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -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) diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 9e38ed3ec..1e5555e9b 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -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; diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 9e845827f..96944fde1 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -339,14 +339,10 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& 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; } diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index d09b90b6b..e1e41c997 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -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) { diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 1ccdd52e7..07241e150 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -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); diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 8931ee14d..351a5e43e 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -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()) diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index dc5c89791..604d8e4eb 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -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(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(); jgetTermDatabase()->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::iterator itv = d_var_num.find(n); if( itv!=d_var_num.end() ){ std::vector& 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& 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& 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& 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& 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& 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& 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& 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& assigned, bool doContinue) Node z = d_parent->getZero(d_vars[index].getType(), k); if( !z.isNull() ){ size_t vni = static_cast(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& 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& 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& 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& assigned, bool doContinue) if( !doFail ){ if( d_una_indexgetNextMatch()) { - 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& 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& 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& 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& 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& 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& 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& 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; } diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index a81abc3a0..f971e4311 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -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()); diff --git a/src/theory/quantifiers/quantifiers_preprocess.cpp b/src/theory/quantifiers/quantifiers_preprocess.cpp index 321ad1717..d9d01c297 100644 --- a/src/theory/quantifiers/quantifiers_preprocess.cpp +++ b/src/theory/quantifiers/quantifiers_preprocess.cpp @@ -127,6 +127,8 @@ Node QuantifiersPreprocess::preSkolemizeQuantifiers( std::unordered_map, Node, NodePolPairHashFunction>& visited) const { + Assert(options().quantifiers.preSkolemQuant + != options::PreSkolemQuantMode::OFF); std::pair key(n, polarity); std::unordered_map, 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 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) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 255cd77a2..03caa0187 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -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& 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 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 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 ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 1aabfe3c3..7e7dda4b7 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -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& 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. */ diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 8492fd621..62fe96439 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -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; diff --git a/src/theory/quantifiers/quantifiers_statistics.cpp b/src/theory/quantifiers/quantifiers_statistics.cpp index 59fdb1808..6437683f7 100644 --- a/src/theory/quantifiers/quantifiers_statistics.cpp +++ b/src/theory/quantifiers/quantifiers_statistics.cpp @@ -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( diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h index 438efd30f..0ece9aedf 100644 --- a/src/theory/quantifiers/quantifiers_statistics.h +++ b/src/theory/quantifiers/quantifiers_statistics.h @@ -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; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index a7df0bb51..284d3aaf8 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -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(); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 8ecfc4e50..712cf6bc0 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -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 diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index ae74b94a1..208e750f1 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -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!"; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 767c74c92..39729bc15 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -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 diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e5d019a76..33935511c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -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) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 273b3364c..7b1facde1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -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& 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); diff --git a/test/regress/cli/regress0/arith/issue7984-quant-trans.smt2 b/test/regress/cli/regress0/arith/issue7984-quant-trans.smt2 index 9a36d87a6..b0de9c7a5 100644 --- a/test/regress/cli/regress0/arith/issue7984-quant-trans.smt2 +++ b/test/regress/cli/regress0/arith/issue7984-quant-trans.smt2 @@ -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) diff --git a/test/regress/cli/regress0/decision/issue8296-sk-def-before-assert.smt2 b/test/regress/cli/regress0/decision/issue8296-sk-def-before-assert.smt2 index 3665d6a55..60269f472 100644 --- a/test/regress/cli/regress0/decision/issue8296-sk-def-before-assert.smt2 +++ b/test/regress/cli/regress0/decision/issue8296-sk-def-before-assert.smt2 @@ -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) diff --git a/test/regress/cli/regress0/nl/nta/issue8294-2-double-solve.smt2 b/test/regress/cli/regress0/nl/nta/issue8294-2-double-solve.smt2 index fb903fb9f..42ca73d3a 100644 --- a/test/regress/cli/regress0/nl/nta/issue8294-2-double-solve.smt2 +++ b/test/regress/cli/regress0/nl/nta/issue8294-2-double-solve.smt2 @@ -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) diff --git a/test/regress/cli/regress0/quantifiers/issue5693-prenex.smt2 b/test/regress/cli/regress0/quantifiers/issue5693-prenex.smt2 index cc89b7829..7424bf960 100644 --- a/test/regress/cli/regress0/quantifiers/issue5693-prenex.smt2 +++ b/test/regress/cli/regress0/quantifiers/issue5693-prenex.smt2 @@ -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) diff --git a/test/regress/cli/regress0/strings/issue6604-re-elim.smt2 b/test/regress/cli/regress0/strings/issue6604-re-elim.smt2 index f75b1b642..f3ba20457 100644 --- a/test/regress/cli/regress0/strings/issue6604-re-elim.smt2 +++ b/test/regress/cli/regress0/strings/issue6604-re-elim.smt2 @@ -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) diff --git a/test/regress/cli/regress0/strings/issue8295-star-union-char.smt2 b/test/regress/cli/regress0/strings/issue8295-star-union-char.smt2 index a11e5ae64..f2dafa46d 100644 --- a/test/regress/cli/regress0/strings/issue8295-star-union-char.smt2 +++ b/test/regress/cli/regress0/strings/issue8295-star-union-char.smt2 @@ -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) diff --git a/test/regress/cli/regress0/strings/regexp_inclusion.smt2 b/test/regress/cli/regress0/strings/regexp_inclusion.smt2 index 648a1b111..b1a07413b 100644 --- a/test/regress/cli/regress0/strings/regexp_inclusion.smt2 +++ b/test/regress/cli/regress0/strings/regexp_inclusion.smt2 @@ -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) diff --git a/test/regress/cli/regress0/strings/regexp_inclusion_reduction.smt2 b/test/regress/cli/regress0/strings/regexp_inclusion_reduction.smt2 index 20ac8f4e4..70bb1c68a 100644 --- a/test/regress/cli/regress0/strings/regexp_inclusion_reduction.smt2 +++ b/test/regress/cli/regress0/strings/regexp_inclusion_reduction.smt2 @@ -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) diff --git a/test/regress/cli/regress1/fmf/fib-core.smt2 b/test/regress/cli/regress1/fmf/fib-core.smt2 index 1a7950a6d..3b9e821f0 100644 --- a/test/regress/cli/regress1/fmf/fib-core.smt2 +++ b/test/regress/cli/regress1/fmf/fib-core.smt2 @@ -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) diff --git a/test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 index 9cafbfc6b..2b9f93d60 100644 --- a/test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 +++ b/test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2 @@ -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) diff --git a/test/regress/cli/regress1/fmf/loopy_coda.smt2 b/test/regress/cli/regress1/fmf/loopy_coda.smt2 index 273235261..6b7b95230 100644 --- a/test/regress/cli/regress1/fmf/loopy_coda.smt2 +++ b/test/regress/cli/regress1/fmf/loopy_coda.smt2 @@ -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) diff --git a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 index beafff29b..18671b4d0 100644 --- a/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2 @@ -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) diff --git a/test/regress/cli/regress1/quantifiers/proj-issue155.smt2 b/test/regress/cli/regress1/quantifiers/proj-issue155.smt2 index 775ed2e5d..559899ff1 100644 --- a/test/regress/cli/regress1/quantifiers/proj-issue155.smt2 +++ b/test/regress/cli/regress1/quantifiers/proj-issue155.smt2 @@ -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) diff --git a/test/regress/cli/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 b/test/regress/cli/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 index 20ab505d4..b123f5573 100644 --- a/test/regress/cli/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 +++ b/test/regress/cli/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --qcf-tconstraint +; COMMAND-LINE: --cbqi-tconstraint ; EXPECT: unsat (set-logic AUFLIA) (set-info :source | diff --git a/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 b/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 index a5e893d9b..d489b0c89 100644 --- a/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 +++ b/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 @@ -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 |) diff --git a/test/regress/cli/regress1/rr-verify/bool-crci.sy b/test/regress/cli/regress1/rr-verify/bool-crci.sy index 614a83f2b..f723e2d00 100644 --- a/test/regress/cli/regress1/rr-verify/bool-crci.sy +++ b/test/regress/cli/regress1/rr-verify/bool-crci.sy @@ -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 diff --git a/test/regress/cli/regress1/rr-verify/bv-term-32.sy b/test/regress/cli/regress1/rr-verify/bv-term-32.sy index 4cf4e3488..f2b1fabf2 100644 --- a/test/regress/cli/regress1/rr-verify/bv-term-32.sy +++ b/test/regress/cli/regress1/rr-verify/bv-term-32.sy @@ -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 diff --git a/test/regress/cli/regress1/rr-verify/bv-term.sy b/test/regress/cli/regress1/rr-verify/bv-term.sy index af954cbb1..9064d0064 100644 --- a/test/regress/cli/regress1/rr-verify/bv-term.sy +++ b/test/regress/cli/regress1/rr-verify/bv-term.sy @@ -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 diff --git a/test/regress/cli/regress1/rr-verify/fp-arith.sy b/test/regress/cli/regress1/rr-verify/fp-arith.sy index ad8635ca8..4407043f2 100644 --- a/test/regress/cli/regress1/rr-verify/fp-arith.sy +++ b/test/regress/cli/regress1/rr-verify/fp-arith.sy @@ -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 diff --git a/test/regress/cli/regress1/rr-verify/fp-bool.sy b/test/regress/cli/regress1/rr-verify/fp-bool.sy index 33caed2e9..78e8b4fb9 100644 --- a/test/regress/cli/regress1/rr-verify/fp-bool.sy +++ b/test/regress/cli/regress1/rr-verify/fp-bool.sy @@ -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 diff --git a/test/regress/cli/regress1/rr-verify/string-term.sy b/test/regress/cli/regress1/rr-verify/string-term.sy index 815cb70a5..9040ab252 100644 --- a/test/regress/cli/regress1/rr-verify/string-term.sy +++ b/test/regress/cli/regress1/rr-verify/string-term.sy @@ -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 diff --git a/test/regress/cli/regress1/seq/issue8148-const-mv.smt2 b/test/regress/cli/regress1/seq/issue8148-const-mv.smt2 index 01f7aefe0..f7bbb1169 100644 --- a/test/regress/cli/regress1/seq/issue8148-const-mv.smt2 +++ b/test/regress/cli/regress1/seq/issue8148-const-mv.smt2 @@ -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)) diff --git a/test/regress/cli/regress1/strings/issue2982.smt2 b/test/regress/cli/regress1/strings/issue2982.smt2 index a57915b44..289ea0931 100644 --- a/test/regress/cli/regress1/strings/issue2982.smt2 +++ b/test/regress/cli/regress1/strings/issue2982.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/issue6604-2.smt2 b/test/regress/cli/regress1/strings/issue6604-2.smt2 index e28f5dcb5..91da234ab 100644 --- a/test/regress/cli/regress1/strings/issue6604-2.smt2 +++ b/test/regress/cli/regress1/strings/issue6604-2.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/issue6635-rre.smt2 b/test/regress/cli/regress1/strings/issue6635-rre.smt2 index cbca77783..368b4fc87 100644 --- a/test/regress/cli/regress1/strings/issue6635-rre.smt2 +++ b/test/regress/cli/regress1/strings/issue6635-rre.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/issue6653-4-rre.smt2 b/test/regress/cli/regress1/strings/issue6653-4-rre.smt2 index 8de99a334..f9f7dea22 100644 --- a/test/regress/cli/regress1/strings/issue6653-4-rre.smt2 +++ b/test/regress/cli/regress1/strings/issue6653-4-rre.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/issue6653-rre-small.smt2 b/test/regress/cli/regress1/strings/issue6653-rre-small.smt2 index c4b6a497b..bc1d4bbd9 100644 --- a/test/regress/cli/regress1/strings/issue6653-rre-small.smt2 +++ b/test/regress/cli/regress1/strings/issue6653-rre-small.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/issue6653-rre.smt2 b/test/regress/cli/regress1/strings/issue6653-rre.smt2 index 66b7dd64e..22513c99b 100644 --- a/test/regress/cli/regress1/strings/issue6653-rre.smt2 +++ b/test/regress/cli/regress1/strings/issue6653-rre.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/issue6766-re-elim-bv.smt2 b/test/regress/cli/regress1/strings/issue6766-re-elim-bv.smt2 index 13677838b..72cb45af4 100644 --- a/test/regress/cli/regress1/strings/issue6766-re-elim-bv.smt2 +++ b/test/regress/cli/regress1/strings/issue6766-re-elim-bv.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2 index 36162852f..c6fa580f0 100644 --- a/test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2 +++ b/test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/non_termination_regular_expression4.smt2 b/test/regress/cli/regress1/strings/non_termination_regular_expression4.smt2 index 1e3f3cb96..356ce9ba7 100644 --- a/test/regress/cli/regress1/strings/non_termination_regular_expression4.smt2 +++ b/test/regress/cli/regress1/strings/non_termination_regular_expression4.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/nt6-dd.smt2 b/test/regress/cli/regress1/strings/nt6-dd.smt2 index ad1e4edf5..4b74bfe20 100644 --- a/test/regress/cli/regress1/strings/nt6-dd.smt2 +++ b/test/regress/cli/regress1/strings/nt6-dd.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/policy_variable.smt2 b/test/regress/cli/regress1/strings/policy_variable.smt2 index c74765108..2ffe62aad 100644 --- a/test/regress/cli/regress1/strings/policy_variable.smt2 +++ b/test/regress/cli/regress1/strings/policy_variable.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/proj254-re-elim-agg.smt2 b/test/regress/cli/regress1/strings/proj254-re-elim-agg.smt2 index cd19dc114..1894e6987 100644 --- a/test/regress/cli/regress1/strings/proj254-re-elim-agg.smt2 +++ b/test/regress/cli/regress1/strings/proj254-re-elim-agg.smt2 @@ -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)) diff --git a/test/regress/cli/regress1/strings/query4674.smt2 b/test/regress/cli/regress1/strings/query4674.smt2 index 86a08162a..2f3ccc6e9 100644 --- a/test/regress/cli/regress1/strings/query4674.smt2 +++ b/test/regress/cli/regress1/strings/query4674.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/query8485.smt2 b/test/regress/cli/regress1/strings/query8485.smt2 index ca222119f..e9bf2c7c7 100644 --- a/test/regress/cli/regress1/strings/query8485.smt2 +++ b/test/regress/cli/regress1/strings/query8485.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/re-agg-total1.smt2 b/test/regress/cli/regress1/strings/re-agg-total1.smt2 index fba863a6c..8090d6508 100644 --- a/test/regress/cli/regress1/strings/re-agg-total1.smt2 +++ b/test/regress/cli/regress1/strings/re-agg-total1.smt2 @@ -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) diff --git a/test/regress/cli/regress1/strings/re-agg-total2.smt2 b/test/regress/cli/regress1/strings/re-agg-total2.smt2 index 80e422224..f1bad3def 100644 --- a/test/regress/cli/regress1/strings/re-agg-total2.smt2 +++ b/test/regress/cli/regress1/strings/re-agg-total2.smt2 @@ -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'")))) diff --git a/test/regress/cli/regress1/strings/re-all-char-hard.smt2 b/test/regress/cli/regress1/strings/re-all-char-hard.smt2 index fc156c116..9fcecd81c 100644 --- a/test/regress/cli/regress1/strings/re-all-char-hard.smt2 +++ b/test/regress/cli/regress1/strings/re-all-char-hard.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-re-elim ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic ALL) diff --git a/test/regress/cli/regress1/strings/re-elim-exact.smt2 b/test/regress/cli/regress1/strings/re-elim-exact.smt2 index 9504aad93..003ee08a4 100644 --- a/test/regress/cli/regress1/strings/re-elim-exact.smt2 +++ b/test/regress/cli/regress1/strings/re-elim-exact.smt2 @@ -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))) diff --git a/test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2 b/test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2 index c8e2db922..3d4951f35 100644 --- a/test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2 +++ b/test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2 @@ -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) diff --git a/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 b/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 index 0afc35e00..4e867e8aa 100644 --- a/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 +++ b/test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2 @@ -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) diff --git a/test/regress/cli/regress1/sygus/proj-issue165.smt2 b/test/regress/cli/regress1/sygus/proj-issue165.smt2 index 37e746c3b..81e463da0 100644 --- a/test/regress/cli/regress1/sygus/proj-issue165.smt2 +++ b/test/regress/cli/regress1/sygus/proj-issue165.smt2 @@ -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) diff --git a/test/regress/cli/regress2/strings/issue918.smt2 b/test/regress/cli/regress2/strings/issue918.smt2 index c335ca642..2aad9b2f4 100644 --- a/test/regress/cli/regress2/strings/issue918.smt2 +++ b/test/regress/cli/regress2/strings/issue918.smt2 @@ -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) diff --git a/test/regress/cli/regress2/strings/non_termination_regular_expression6.smt2 b/test/regress/cli/regress2/strings/non_termination_regular_expression6.smt2 index 175ee5cc0..e3b260d7c 100644 --- a/test/regress/cli/regress2/strings/non_termination_regular_expression6.smt2 +++ b/test/regress/cli/regress2/strings/non_termination_regular_expression6.smt2 @@ -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) diff --git a/test/regress/cli/regress2/strings/small-1.smt2 b/test/regress/cli/regress2/strings/small-1.smt2 index e0dea5d89..82748c169 100644 --- a/test/regress/cli/regress2/strings/small-1.smt2 +++ b/test/regress/cli/regress2/strings/small-1.smt2 @@ -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) diff --git a/test/regress/cli/regress3/regex-rrv.sy b/test/regress/cli/regress3/regex-rrv.sy index 2d911e56a..4410ec807 100644 --- a/test/regress/cli/regress3/regex-rrv.sy +++ b/test/regress/cli/regress3/regex-rrv.sy @@ -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 diff --git a/test/regress/cli/regress4/unsat-circ-reduce.smt2 b/test/regress/cli/regress4/unsat-circ-reduce.smt2 index b584c0fb1..2db29693d 100644 --- a/test/regress/cli/regress4/unsat-circ-reduce.smt2 +++ b/test/regress/cli/regress4/unsat-circ-reduce.smt2 @@ -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) diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py index 227ff2ef1..8ef0da532 100755 --- a/test/regress/cli/run_regression.py +++ b/test/regress/cli/run_regression.py @@ -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 )