[[option]]
name = "termDbMode"
category = "regular"
- long = "term-db-mode"
+ long = "term-db-mode=MODE"
type = "CVC4::theory::quantifiers::TermDbMode"
default = "CVC4::theory::quantifiers::TERM_DB_ALL"
handler = "stringToTermDbMode"
read_only = true
help = "infer equalities for trigger terms based on solving arithmetic equalities"
-[[option]]
- name = "inferArithTriggerEqExp"
- category = "regular"
- long = "infer-arith-trigger-eq-exp"
- type = "bool"
- default = "false"
- read_only = true
- help = "record explanations for inferArithTriggerEq"
-
[[option]]
name = "strictTriggers"
category = "regular"
category = "regular"
long = "relational-triggers"
type = "bool"
- default = "false"
+ default = "true"
read_only = true
help = "choose relational triggers such as x = f(y), x >= f(y)"
[[option]]
name = "triggerSelMode"
category = "regular"
- long = "trigger-sel"
+ long = "trigger-sel=MODE"
type = "CVC4::theory::quantifiers::TriggerSelMode"
default = "CVC4::theory::quantifiers::TRIGGER_SEL_MIN"
handler = "stringToTriggerSelMode"
[[option]]
name = "triggerActiveSelMode"
category = "regular"
- long = "trigger-active-sel"
+ long = "trigger-active-sel=MODE"
type = "CVC4::theory::quantifiers::TriggerActiveSelMode"
default = "CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL"
handler = "stringToTriggerActiveSelMode"
read_only = true
help = "interleave full saturate instantiation with other techniques"
+[[option]]
+ name = "fullSaturateStratify"
+ category = "regular"
+ long = "fs-stratify"
+ type = "bool"
+ default = "false"
+ read_only = true
+ help = "stratify effort levels in enumerative instantiation, which favors speed over fairness"
+
[[option]]
name = "literalMatchMode"
category = "regular"
default = "false"
help = "enforce bounds for bounded quantification lazily via use of proxy variables"
-[[option]]
- name = "fmfBoundMinMode"
- category = "regular"
- long = "fmf-bound-min-mode=MODE"
- type = "CVC4::theory::quantifiers::FmfBoundMinMode"
- default = "CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE"
- handler = "stringToFmfBoundMinMode"
- includes = ["options/quantifiers_modes.h"]
- read_only = true
- help = "mode for which types of bounds to minimize via first decision heuristics"
-
[[option]]
name = "fmfTypeCompletionThresh"
category = "regular"
read_only = true
help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
-### Rewrite rules options
+### Rewrite rules options
[[option]]
name = "quantRewriteRules"
read_only = true
help = "add one instance of rewrite rule per round"
-### Induction options
+### Induction options
[[option]]
name = "quantInduction"
read_only = false
help = "attempt to preprocess arbitrary inputs to sygus conjectures"
+[[option]]
+ name = "sygusAbduct"
+ category = "regular"
+ long = "sygus-abduct"
+ type = "bool"
+ default = "false"
+ read_only = false
+ help = "compute abductions using sygus"
+
[[option]]
name = "ceGuidedInst"
category = "regular"
default = "false"
help = "Unification-based function synthesis"
+[[option]]
+ name = "sygusUnifCondIndependent"
+ category = "regular"
+ long = "sygus-unif-cond-independent"
+ type = "bool"
+ default = "false"
+ help = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
+
+[[option]]
+ name = "sygusUnifShuffleCond"
+ category = "regular"
+ long = "sygus-unif-shuffle-cond"
+ type = "bool"
+ default = "false"
+ help = "Shuffle condition pool when building solutions (may change solutions sizes)"
+
+[[option]]
+ name = "sygusUnifBooleanHeuristicDt"
+ category = "regular"
+ long = "sygus-unif-boolean-heuristic-dt"
+ type = "bool"
+ default = "false"
+ help = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
+
+[[option]]
+ name = "sygusUnifCondIndNoRepeatSol"
+ category = "regular"
+ long = "sygus-unif-cond-independent-no-repeat-sol"
+ type = "bool"
+ default = "true"
+ help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis"
+
[[option]]
name = "sygusBoolIteReturnConst"
category = "regular"
category = "regular"
long = "sygus-repair-const"
type = "bool"
- default = "true"
+ default = "false"
help = "use approach to repair constants in sygus candidate solutions"
+[[option]]
+ name = "sygusRepairConstTimeout"
+ category = "regular"
+ long = "sygus-repair-const-timeout=N"
+ type = "unsigned long"
+ help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
+
+[[option]]
+ 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"]
+ read_only = true
+ help = "mode for actively-generated sygus enumerators"
+
+[[option]]
+ name = "sygusActiveGenEnumConsts"
+ category = "regular"
+ long = "sygus-active-gen-cfactor=N"
+ type = "unsigned long"
+ default = "5"
+ help = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum"
+
[[option]]
name = "sygusMinGrammar"
category = "regular"
default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
handler = "stringToSygusInvTemplMode"
includes = ["options/quantifiers_modes.h"]
- read_only = true
help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
[[option]]
category = "regular"
long = "sygus-pbe-multi-fair"
type = "bool"
- default = "true"
+ default = "false"
help = "when using multiple enumerators, ensure that we only register value of minimial term size"
[[option]]
type = "bool"
default = "true"
help = "Minimize synthesis solutions"
-
+
[[option]]
name = "sygusEvalOpt"
category = "regular"
default = "true"
help = "use optimized approach for evaluation in sygus"
+[[option]]
+ name = "sygusArgRelevant"
+ category = "regular"
+ long = "sygus-arg-relevant"
+ type = "bool"
+ default = "false"
+ help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
+
# Internal uses of sygus
[[option]]
type = "bool"
default = "false"
read_only = true
- help = "use sygus to enumerate and verify correctness of rewrite rules via sampling"
+ help = "use sygus to enumerate and verify correctness of rewrite rules"
[[option]]
name = "sygusRewSynth"
long = "sygus-rr-synth"
type = "bool"
default = "false"
- help = "use sygus to enumerate candidate rewrite rules via sampling"
+ help = "use sygus to enumerate candidate rewrite rules"
[[option]]
name = "sygusRewSynthFilterOrder"
default = "true"
help = "filter candidate rewrites based on congruence"
+[[option]]
+ name = "sygusRewSynthFilterNonLinear"
+ category = "regular"
+ long = "sygus-rr-synth-filter-nl"
+ type = "bool"
+ default = "false"
+ help = "filter non-linear candidate rewrites"
+
[[option]]
name = "sygusRewVerify"
category = "regular"
help = "use satisfiability check to verify correctness of candidate rewrites"
[[option]]
- name = "sygusRewSynthCheckTimeout"
+ name = "sygusRewSynthInput"
category = "regular"
- long = "sygus-rr-synth-check-timeout"
+ long = "sygus-rr-synth-input"
+ type = "bool"
+ default = "false"
+ help = "synthesize rewrite rules based on the input formula"
+
+[[option]]
+ name = "sygusRewSynthInputNVars"
+ category = "regular"
+ long = "sygus-rr-synth-input-nvars=N"
+ type = "int"
+ default = "3"
+ help = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input"
+
+[[option]]
+ name = "sygusRewSynthInputUseBool"
+ category = "regular"
+ long = "sygus-rr-synth-input-use-bool"
+ type = "bool"
+ default = "false"
+ help = "synthesize Boolean rewrite rules based on the input formula"
+
+[[option]]
+ name = "sygusExprMinerCheckTimeout"
+ category = "regular"
+ long = "sygus-expr-miner-check-timeout=N"
type = "unsigned long"
- help = "timeout (in milliseconds) for the satisfiability check to verify correctness of candidate rewrites"
+ help = "timeout (in milliseconds) for satisfiability checks in expression miners"
+
+[[option]]
+ name = "sygusRewSynthRec"
+ category = "regular"
+ long = "sygus-rr-synth-rec"
+ type = "bool"
+ default = "false"
+ help = "synthesize rewrite rules over all sygus grammar types recursively"
+
+[[option]]
+ name = "sygusQueryGen"
+ category = "regular"
+ long = "sygus-query-gen"
+ type = "bool"
+ default = "false"
+ help = "use sygus to enumerate interesting satisfiability queries"
+
+[[option]]
+ name = "sygusQueryGenThresh"
+ category = "regular"
+ long = "sygus-query-gen-thresh=N"
+ type = "unsigned"
+ default = "5"
+ help = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen"
+
+[[option]]
+ name = "sygusQueryGenCheck"
+ category = "regular"
+ long = "sygus-query-gen-check"
+ type = "bool"
+ default = "true"
+ help = "use interesting satisfiability queries to check soundness of CVC4"
+
+[[option]]
+ name = "sygusQueryGenDumpFiles"
+ category = "regular"
+ long = "sygus-query-gen-dump-files"
+ type = "bool"
+ default = "false"
+ help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen"
+
+[[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"]
+ help = "mode for filtering sygus solutions"
+
+[[option]]
+ name = "sygusFilterSolRevSubsume"
+ category = "expert"
+ long = "sygus-filter-sol-rev"
+ type = "bool"
+ default = "false"
+ help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
+
+
+[[option]]
+ name = "sygusExprMinerCheckUseExport"
+ category = "expert"
+ long = "sygus-expr-miner-check-use-export"
+ type = "bool"
+ default = "true"
+ help = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners"
# CEGQI applied to general quantified formulas
default = "false"
help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
-[[option]]
- name = "recurseCbqi"
- category = "regular"
- long = "cbqi-recurse"
- type = "bool"
- default = "true"
- read_only = true
- help = "turns on recursive counterexample-based quantifier instantiation"
-
[[option]]
name = "cbqiSat"
category = "regular"
projects / cvc5.git / blobdiff