diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-12-17 13:43:44 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-17 13:43:44 -0800 |
commit | e9499c41f405df8b42fd9ae10004b1b91a869106 (patch) | |
tree | fa1475f43a3e61b8f6ffdcb903b65919eba28661 /src/options/quantifiers_options.toml | |
parent | 9b2914ed9f7b14ecf535ffe9e1328d0fa042e072 (diff) |
Generate code for options with modes. (#3561)
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
Diffstat (limited to 'src/options/quantifiers_options.toml')
-rw-r--r-- | src/options/quantifiers_options.toml | 471 |
1 files changed, 373 insertions, 98 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index d37c9db83..95ec636ca 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -36,11 +36,22 @@ header = "options/quantifiers_options.h" name = "prenexQuant" category = "regular" long = "prenex-quant=MODE" - type = "CVC4::theory::quantifiers::PrenexQuantMode" - default = "CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE" - handler = "stringToPrenexQuantMode" - includes = ["options/quantifiers_modes.h"] + type = "PrenexQuantMode" + default = "SIMPLE" help = "prenex mode for quantified formulas" + help_mode = "Prenex quantifiers modes." +[[option.mode.NONE]] + name = "none" + help = "Do no prenex nested quantifiers." +[[option.mode.SIMPLE]] + name = "simple" + help = "Do simple prenexing of same sign quantifiers." +[[option.mode.DISJ_NORMAL]] + name = "dnorm" + help = "Prenex to disjunctive prenex normal form." +[[option.mode.NORMAL]] + name = "norm" + help = "Prenex to prenex normal form." [[option]] name = "prenexQuantUser" @@ -84,11 +95,19 @@ header = "options/quantifiers_options.h" name = "iteLiftQuant" category = "regular" long = "ite-lift-quant=MODE" - type = "CVC4::theory::quantifiers::IteLiftQuantMode" - default = "CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE" - handler = "stringToIteLiftQuantMode" - includes = ["options/quantifiers_modes.h"] + type = "IteLiftQuantMode" + default = "SIMPLE" help = "ite lifting mode for quantified formulas" + help_mode = "ITE lifting modes for quantified formulas." +[[option.mode.NONE]] + name = "none" + help = "Do not lift if-then-else in quantified formulas." +[[option.mode.SIMPLE]] + name = "simple" + help = "Lift if-then-else in quantified formulas if results in smaller term size." +[[option.mode.ALL]] + name = "all" + help = "Lift if-then-else in quantified formulas." [[option]] name = "condVarSplitQuant" @@ -200,11 +219,16 @@ header = "options/quantifiers_options.h" name = "termDbMode" category = "regular" long = "term-db-mode=MODE" - type = "CVC4::theory::quantifiers::TermDbMode" - default = "CVC4::theory::quantifiers::TERM_DB_ALL" - handler = "stringToTermDbMode" - includes = ["options/quantifiers_modes.h"] + type = "TermDbMode" + default = "ALL" help = "which ground terms to consider for instantiation" + help_mode = "Modes for terms included in the quantifiers term database." +[[option.mode.ALL]] + name = "all" + help = "Quantifiers module considers all ground terms." +[[option.mode.RELEVANT]] + name = "relevant" + help = "Quantifiers module considers only ground terms connected to current assertions." [[option]] name = "registerQuantBodyTerms" @@ -310,35 +334,105 @@ header = "options/quantifiers_options.h" read_only = true help = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms" +# Trigger selection mode. +# +# These modes are used for determining which terms to select +# as triggers for quantified formulas, when necessary, during E-matching. +# In the following, note the following terminology. A trigger is a set of terms, +# where a single trigger is a singleton set and a multi-trigger is a set of more +# than one term. +# +# MIN selects single triggers of minimal term size. +# MAX selects single triggers of maximal term size. +# +# For example, consider the quantified formula : +# forall xy. P( f( g( x, y ) ) ) V Q( f( x ), y ) +# +# MIN will select g( x, y ) and Q( f( x ), y ). +# MAX will select P( f( g( x ) ) ) and Q( f( x ), y ). +# +# The remaining three trigger selections make a difference for multi-triggers +# only. For quantified formulas that require multi-triggers, we build a set of +# partial triggers that don't contain all variables, call this set S. Then, +# multi-triggers are built by taking a random subset of S that collectively +# contains all variables. +# +# Consider the quantified formula : +# forall xyz. P( h( x ), y ) V Q( y, z ) +# +# For ALL and MIN_SINGLE_ALL, +# S = { h( x ), P( h( x ), y ), Q( y, z ) }. +# For MIN_SINGLE_MAX, +# S = { P( h( x ), y ), Q( y, z ) }. +# +# Furthermore, MIN_SINGLE_ALL and MIN_SINGLE_MAX, when +# selecting single triggers, only select terms of minimal size. +# [[option]] name = "triggerSelMode" category = "regular" long = "trigger-sel=MODE" - type = "CVC4::theory::quantifiers::TriggerSelMode" - default = "CVC4::theory::quantifiers::TRIGGER_SEL_MIN" - handler = "stringToTriggerSelMode" - includes = ["options/quantifiers_modes.h"] + type = "TriggerSelMode" + default = "MIN" help = "selection mode for triggers" + help_mode = "Trigger selection modes." +[[option.mode.MIN]] + name = "min" + help = "Consider only minimal subterms that meet criteria for triggers." +[[option.mode.MAX]] + name = "max" + help = "Consider only maximal subterms that meet criteria for triggers." +[[option.mode.MIN_SINGLE_MAX]] + name = "min-s-max" + help = "Consider only minimal subterms that meet criteria for single triggers, maximal otherwise." +[[option.mode.MIN_SINGLE_ALL]] + name = "min-s-all" + help = "Consider only minimal subterms that meet criteria for single triggers, all otherwise." +[[option.mode.ALL]] + name = "all" + help = "Consider all subterms that meet criteria for triggers." [[option]] name = "triggerActiveSelMode" category = "regular" long = "trigger-active-sel=MODE" - type = "CVC4::theory::quantifiers::TriggerActiveSelMode" - default = "CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL" - handler = "stringToTriggerActiveSelMode" - includes = ["options/quantifiers_modes.h"] + type = "TriggerActiveSelMode" + default = "ALL" help = "selection mode to activate triggers" + help_mode = "Trigger active selection modes." +[[option.mode.ALL]] + name = "all" + help = "Make all triggers active." +[[option.mode.MIN]] + name = "min" + help = "Activate triggers with minimal ground terms." +[[option.mode.MAX]] + name = "max" + help = "Activate triggers with maximal ground terms." [[option]] name = "userPatternsQuant" category = "regular" long = "user-pat=MODE" - type = "CVC4::theory::quantifiers::UserPatMode" - default = "CVC4::theory::quantifiers::USER_PAT_MODE_TRUST" - handler = "stringToUserPatMode" - includes = ["options/quantifiers_modes.h"] + type = "UserPatMode" + default = "TRUST" help = "policy for handling user-provided patterns for quantifier instantiation" + help_mode = "These modes determine how user provided patterns (triggers) are used during E-matching. The modes vary on when instantiation based on user-provided triggers is combined with instantiation based on automatically selected triggers." +[[option.mode.USE]] + name = "use" + help = "Use both user-provided and auto-generated patterns when patterns are provided for a quantified formula." +[[option.mode.TRUST]] + name = "trust" + help = "When provided, use only user-provided patterns for a quantified formula." +[[option.mode.RESORT]] + name = "resort" + help = "Use user-provided patterns only after auto-generated patterns saturate." +[[option.mode.IGNORE]] + name = "ignore" + help = "Ignore user-provided patterns." +[[option.mode.INTERLEAVE]] + name = "interleave" + help = "Alternate between use/resort." [[option]] name = "incrementTriggers" @@ -353,12 +447,29 @@ header = "options/quantifiers_options.h" name = "instWhenMode" category = "regular" long = "inst-when=MODE" - type = "CVC4::theory::quantifiers::InstWhenMode" - default = "CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL" - handler = "stringToInstWhenMode" + type = "InstWhenMode" + default = "FULL_LAST_CALL" predicates = ["checkInstWhenMode"] - includes = ["options/quantifiers_modes.h"] help = "when to apply instantiation" + help_mode = "Instantiation modes." +[[option.mode.PRE_FULL]] + name = "pre-full" + help = "Run instantiation round before full effort (possibly at standard effort)." +[[option.mode.FULL]] + name = "full" + help = "Run instantiation round at full effort, before theory combination." +[[option.mode.FULL_DELAY]] + name = "full-delay" + help = "Run instantiation round at full effort, before theory combination, after all other theories have finished." +[[option.mode.FULL_LAST_CALL]] + name = "full-last-call" + help = "Alternate running instantiation rounds at full effort and last call. In other words, interleave instantiation and theory combination." +[[option.mode.FULL_DELAY_LAST_CALL]] + name = "full-delay-last-call" + help = "Alternate running instantiation rounds at full effort after all other theories have finished, and last call." +[[option.mode.LAST_CALL]] + name = "last-call" + help = "Run instantiation at last call effort, after theory combination and and theories report sat." [[option]] name = "instWhenStrictInterleave" @@ -414,11 +525,19 @@ header = "options/quantifiers_options.h" name = "quantRepMode" category = "regular" long = "quant-rep-mode=MODE" - type = "CVC4::theory::quantifiers::QuantRepMode" - default = "CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST" - handler = "stringToQuantRepMode" - includes = ["options/quantifiers_modes.h"] + type = "QuantRepMode" + default = "FIRST" help = "selection mode for representatives in quantifiers engine" + help_mode = "Modes for quantifiers representative selection." +[[option.mode.EE]] + name = "ee" + help = "Let equality engine choose representatives." +[[option.mode.FIRST]] + name = "first" + help = "Choose terms that appear first." +[[option.mode.DEPTH]] + name = "depth" + help = "Choose terms that are of minimal depth." [[option]] name = "fullSaturateQuant" @@ -459,13 +578,23 @@ header = "options/quantifiers_options.h" name = "literalMatchMode" category = "regular" long = "literal-matching=MODE" - type = "CVC4::theory::quantifiers::LiteralMatchMode" - default = "CVC4::theory::quantifiers::LITERAL_MATCH_USE" - handler = "stringToLiteralMatchMode" - predicates = ["checkLiteralMatchMode"] - includes = ["options/quantifiers_modes.h"] + type = "LiteralMatchMode" + default = "USE" read_only = true help = "choose literal matching mode" + help_mode = "Literal match modes." +[[option.mode.NONE]] + name = "none" + help = "Do not use literal matching." +[[option.mode.USE]] + name = "use" + help = "Consider phase requirements of triggers conservatively. For example, the trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with terms in the equivalence class of true, and likewise Q( x ) will not be matched terms in the equivalence class of false. Extends to equality." +[[option.mode.AGG_PREDICATE]] + name = "agg-predicate" + help = "Consider phase requirements aggressively for predicates. In the above example, only match P( x ) with terms that are in the equivalence class of false." +[[option.mode.AGG]] + name = "agg" + help = "Consider the phase requirements aggressively for all triggers." ### Finite model finding options @@ -516,12 +645,19 @@ header = "options/quantifiers_options.h" name = "mbqiMode" category = "regular" long = "mbqi=MODE" - type = "CVC4::theory::quantifiers::MbqiMode" - default = "CVC4::theory::quantifiers::MBQI_FMC" - handler = "stringToMbqiMode" - predicates = ["checkMbqiMode"] - includes = ["options/quantifiers_modes.h"] + type = "MbqiMode" + default = "FMC" help = "choose mode for model-based quantifier instantiation" + help_mode = "Model-based quantifier instantiation modes." +[[option.mode.NONE]] + name = "none" + help = "Disable model-based quantifier instantiation." +[[option.mode.FMC]] + name = "fmc" + help = "Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability Modulo Theories." +[[option.mode.TRUST]] + name = "trust" + help = "Do not instantiate quantified formulas (incomplete technique)." [[option]] name = "fmfOneInstPerRound" @@ -638,23 +774,42 @@ header = "options/quantifiers_options.h" name = "qcfMode" category = "regular" long = "quant-cf-mode=MODE" - type = "CVC4::theory::quantifiers::QcfMode" - default = "CVC4::theory::quantifiers::QCF_PROP_EQ" - handler = "stringToQcfMode" - includes = ["options/quantifiers_modes.h"] + type = "QcfMode" + default = "PROP_EQ" read_only = true help = "what effort to apply conflict find mechanism" + help_mode = "Quantifier conflict find modes." +[[option.mode.CONFLICT_ONLY]] + name = "conflict" + help = "Apply QCF algorithm to find conflicts only." +[[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 = "CVC4::theory::quantifiers::QcfWhenMode" - default = "CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT" - handler = "stringToQcfWhenMode" - includes = ["options/quantifiers_modes.h"] + type = "QcfWhenMode" + default = "DEFAULT" read_only = true 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" @@ -888,11 +1043,19 @@ header = "options/quantifiers_options.h" name = "cegqiSingleInvMode" category = "regular" long = "cegqi-si=MODE" - type = "CVC4::theory::quantifiers::CegqiSingleInvMode" - default = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE" - handler = "stringToCegqiSingleInvMode" - includes = ["options/quantifiers_modes.h"] + type = "CegqiSingleInvMode" + default = "NONE" help = "mode for processing single invocation synthesis conjectures" + help_mode = "Modes for single invocation techniques." +[[option.mode.NONE]] + name = "none" + help = "Do not use single invocation techniques." +[[option.mode.USE]] + name = "use" + help = "Use single invocation techniques only if grammar is not restrictive." +[[option.mode.ALL]] + name = "all" + help = "Always use single invocation techniques." [[option]] name = "cegqiSingleInvPartial" @@ -903,15 +1066,32 @@ header = "options/quantifiers_options.h" read_only = true help = "combined techniques for synthesis conjectures that are partially single invocation" +# Solution reconstruction modes for single invocation conjectures +# +# These modes indicate the policy when CVC4 solves a synthesis conjecture using +# single invocation techniques for a sygus problem with a user-specified +# grammar. +# [[option]] name = "cegqiSingleInvReconstruct" category = "regular" long = "cegqi-si-rcons=MODE" - type = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode" - default = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT" - handler = "stringToCegqiSingleInvRconsMode" - includes = ["options/quantifiers_modes.h"] + type = "CegqiSingleInvRconsMode" + default = "ALL_LIMIT" help = "policy for reconstructing solutions for single invocation conjectures" + help_mode = "Modes for reconstruction solutions while using single invocation techniques." +[[option.mode.NONE]] + name = "none" + help = "Do not try to reconstruct solutions in the original (user-provided) grammar when using single invocation techniques. In this mode, solutions produced by CVC4 may violate grammar restrictions." +[[option.mode.TRY]] + name = "try" + help = "Try to reconstruct solutions in the original grammar when using single invocation techniques in an incomplete (fail-fast) manner." +[[option.mode.ALL_LIMIT]] + name = "all-limit" + help = "Try to reconstruct solutions in the original grammar, but termintate if a maximum number of rounds for reconstruction is exceeded." +[[option.mode.ALL]] + name = "all" + help = "Try to reconstruct solutions in the original grammar. In this mode, we do not terminate until a solution is successfully reconstructed." [[option]] name = "cegqiSingleInvReconstructLimit" @@ -949,16 +1129,30 @@ header = "options/quantifiers_options.h" read_only = true help = "abort if constant repair techniques are not applicable" +# Modes for piecewise-independent unification for synthesis (see Barbosa et al +# FMCAD 2019). +# [[option]] name = "sygusUnifPi" category = "regular" long = "sygus-unif-pi=MODE" - type = "CVC4::theory::quantifiers::SygusUnifPiMode" - default = "CVC4::theory::quantifiers::SYGUS_UNIF_PI_NONE" - handler = "stringToSygusUnifPiMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusUnifPiMode" + default = "NONE" read_only = true help = "mode for synthesis via piecewise-indepedent unification" + help_mode = "Modes for piecewise-independent unification." +[[option.mode.NONE]] + name = "none" + help = "Do not use piecewise-independent unification." +[[option.mode.COMPLETE]] + name = "complete" + help = "Use complete approach for piecewise-independent unification (see Section 3 of Barbosa et al FMCAD 2019)" +[[option.mode.CENUM]] + name = "cond-enum" + help = "Use unconstrained condition enumeration for piecewise-independent unification (see Section 4 of Barbosa et al FMCAD 2019)." +[[option.mode.CENUM_IGAIN]] + name = "cond-enum-igain" + help = "Same as cond-enum, but additionally uses an information gain heuristic when doing decision tree learning." [[option]] name = "sygusUnifShuffleCond" @@ -1020,12 +1214,26 @@ header = "options/quantifiers_options.h" name = "sygusActiveGenMode" category = "regular" long = "sygus-active-gen=MODE" - type = "CVC4::theory::quantifiers::SygusActiveGenMode" - default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO" - handler = "stringToSygusActiveGenMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusActiveGenMode" + default = "AUTO" read_only = true help = "mode for actively-generated sygus enumerators" + help_mode = "Modes for actively-generated sygus enumerators." +[[option.mode.NONE]] + name = "none" + help = "Do not use actively-generated sygus enumerators." +[[option.mode.ENUM_BASIC]] + name = "basic" + help = "Use basic type enumerator for actively-generated sygus enumerators." +[[option.mode.ENUM]] + name = "enum" + help = "Use optimized enumerator for actively-generated sygus enumerators." +[[option.mode.VAR_AGNOSTIC]] + name = "var-agnostic" + help = "Use sygus solver to enumerate terms that are agnostic to variables." +[[option.mode.AUTO]] + name = "auto" + help = "Internally decide the best policy for each enumerator." [[option]] name = "sygusActiveGenEnumConsts" @@ -1075,21 +1283,40 @@ header = "options/quantifiers_options.h" name = "sygusGrammarConsMode" category = "regular" long = "sygus-grammar-cons=MODE" - type = "CVC4::theory::quantifiers::SygusGrammarConsMode" - default = "CVC4::theory::quantifiers::SYGUS_GCONS_SIMPLE" - handler = "stringToSygusGrammarConsMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusGrammarConsMode" + default = "SIMPLE" help = "mode for SyGuS grammar construction" + help_mode = "Modes for default SyGuS grammars." +[[option.mode.SIMPLE]] + name = "simple" + help = "Use simple grammar construction (no symbolic terms or constants)." +[[option.mode.ANY_CONST]] + name = "any-const" + help = "Use symoblic constant constructors." +[[option.mode.ANY_TERM]] + name = "any-term" + help = "When applicable, use constructors corresponding to any symbolic term. This option enables a sum-of-monomials grammar for arithmetic. For all other types, it enables symbolic constant constructors." +[[option.mode.ANY_TERM_CONCISE]] + name = "any-term-concise" + help = "When applicable, use constructors corresponding to any symbolic term, favoring conciseness over generality. This option is equivalent to any-term but enables a polynomial grammar for arithmetic when not in a combined theory." [[option]] name = "sygusInvTemplMode" category = "regular" long = "sygus-inv-templ=MODE" - type = "CVC4::theory::quantifiers::SygusInvTemplMode" - default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST" - handler = "stringToSygusInvTemplMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusInvTemplMode" + default = "POST" help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)" + help_mode = "Template modes for sygus invariant synthesis." +[[option.mode.NONE]] + name = "none" + help = "Synthesize invariant directly." +[[option.mode.PRE]] + name = "pre" + help = "Synthesize invariant based on weakening of precondition." +[[option.mode.POST]] + name = "post" + help = "Synthesize invariant based on strengthening of postcondition." [[option]] name = "sygusInvTemplWhenSyntax" @@ -1188,11 +1415,19 @@ header = "options/quantifiers_options.h" name = "cegisSample" category = "regular" long = "cegis-sample=MODE" - type = "CVC4::theory::quantifiers::CegisSampleMode" - default = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE" - handler = "stringToCegisSampleMode" - includes = ["options/quantifiers_modes.h"] + type = "CegisSampleMode" + default = "NONE" help = "mode for using samples in the counterexample-guided inductive synthesis loop" + help_mode = "Modes for sampling with counterexample-guided inductive synthesis (CEGIS)." +[[option.mode.NONE]] + name = "none" + help = "Do not use sampling with CEGIS." +[[option.mode.USE]] + name = "use" + help = "Use sampling to accelerate CEGIS. This will rule out solutions for a conjecture when they are not satisfied by a sample point." +[[option.mode.TRUST]] + 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 = "minSynthSol" @@ -1409,21 +1644,37 @@ header = "options/quantifiers_options.h" name = "sygusQueryGenDumpFiles" category = "regular" long = "sygus-query-gen-dump-files=MODE" - type = "CVC4::theory::quantifiers::SygusQueryDumpFilesMode" - default = "CVC4::theory::quantifiers::SYGUS_QUERY_DUMP_NONE" - handler = "stringToSygusQueryDumpFilesMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusQueryDumpFilesMode" + default = "NONE" help = "mode for dumping external files corresponding to interesting satisfiability queries with sygus-query-gen" + help_mode = "Query file options." +[[option.mode.NONE]] + name = "none" + help = "Do not dump query files when using --sygus-query-gen." +[[option.mode.ALL]] + name = "all" + help = "Dump all query files." +[[option.mode.UNSOLVED]] + name = "unsolved" + help = "Dump query files that the subsolver did not solve." [[option]] name = "sygusFilterSolMode" category = "regular" long = "sygus-filter-sol=MODE" - type = "CVC4::theory::quantifiers::SygusFilterSolMode" - default = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE" - handler = "stringToSygusFilterSolMode" - includes = ["options/quantifiers_modes.h"] + type = "SygusFilterSolMode" + default = "NONE" help = "mode for filtering sygus solutions" + help_mode = "Modes for filtering sygus solutions." +[[option.mode.NONE]] + name = "none" + help = "Do not filter sygus solutions." +[[option.mode.STRONG]] + name = "strong" + help = "Filter solutions that are logically stronger than others." +[[option.mode.WEAK]] + name = "weak" + help = "Filter solutions that are logically weaker than others." [[option]] name = "sygusFilterSolRevSubsume" @@ -1627,11 +1878,19 @@ header = "options/quantifiers_options.h" name = "cbqiBvIneqMode" category = "regular" long = "cbqi-bv-ineq=MODE" - type = "CVC4::theory::quantifiers::CbqiBvIneqMode" - default = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY" - handler = "stringToCbqiBvIneqMode" - includes = ["options/quantifiers_modes.h"] + type = "CbqiBvIneqMode" + default = "EQ_BOUNDARY" help = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation" + help_mode = "Modes for handling bit-vector inequalities in counterexample-guided instantiation." +[[option.mode.EQ_SLACK]] + name = "eq-slack" + help = "Solve for the inequality using the slack value in the model, e.g., t > s becomes t = s + ( t-s )^M." +[[option.mode.EQ_BOUNDARY]] + name = "eq-boundary" + help = "Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1." +[[option.mode.KEEP]] + name = "keep" + help = "Solve for the inequality directly using side conditions for invertibility." [[option]] name = "cbqiBvRmExtract" @@ -1717,22 +1976,38 @@ header = "options/quantifiers_options.h" name = "macrosQuantMode" category = "regular" long = "macros-quant-mode=MODE" - type = "CVC4::theory::quantifiers::MacrosQuantMode" - default = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF" - handler = "stringToMacrosQuantMode" - includes = ["options/quantifiers_modes.h"] + type = "MacrosQuantMode" + default = "GROUND_UF" read_only = true help = "mode for quantifiers macro expansion" + help_mode = "Modes for quantifiers macro expansion." +[[option.mode.ALL]] + name = "all" + help = "Infer definitions for functions, including those containing quantified formulas." +[[option.mode.GROUND]] + name = "ground" + help = "Only infer ground definitions for functions." +[[option.mode.GROUND_UF]] + name = "ground-uf" + help = "Only infer ground definitions for functions that result in triggers for all free variables." [[option]] name = "quantDynamicSplit" category = "regular" long = "quant-dsplit-mode=MODE" - type = "CVC4::theory::quantifiers::QuantDSplitMode" - default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_DEFAULT" - handler = "stringToQuantDSplitMode" - includes = ["options/quantifiers_modes.h"] + type = "QuantDSplitMode" + default = "DEFAULT" help = "mode for dynamic quantifiers splitting" + help_mode = "Modes for quantifiers splitting." +[[option.mode.NONE]] + name = "none" + help = "Never split quantified formulas." +[[option.mode.DEFAULT]] + name = "default" + help = "Split quantified formulas over some finite datatypes when finite model finding is enabled." +[[option.mode.AGG]] + name = "agg" + help = "Aggressively split quantified formulas." [[option]] name = "quantAntiSkolem" |