3 header = "options/quantifiers_options.h"
5 # Whether to mini-scope quantifiers.
6 # For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
7 # ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
9 name = "miniscopeQuant"
11 long = "miniscope-quant"
14 help = "miniscope quantifiers"
16 # Whether to mini-scope quantifiers based on formulas with no free variables.
17 # For example, forall x. ( P( x ) V Q ) will be rewritten to
18 # ( forall x. P( x ) ) V Q
20 name = "miniscopeQuantFreeVar"
22 long = "miniscope-quant-fv"
25 help = "miniscope quantifiers for ground subformulas"
33 help = "apply splitting to quantified formulas based on variable disjoint disjuncts"
38 long = "prenex-quant=MODE"
39 type = "CVC4::theory::quantifiers::PrenexQuantMode"
40 default = "CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE"
41 handler = "stringToPrenexQuantMode"
42 includes = ["options/quantifiers_modes.h"]
43 help = "prenex mode for quantified formulas"
46 name = "prenexQuantUser"
48 long = "prenex-quant-user"
51 help = "prenex quantified formulas with user patterns"
53 # Whether to variable-eliminate quantifiers.
54 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
59 long = "var-elim-quant"
63 help = "enable simple variable elimination for quantified formulas"
66 name = "varIneqElimQuant"
68 long = "var-ineq-elim-quant"
72 help = "enable variable elimination based on infinite projection of unbound arithmetic variables"
75 name = "dtVarExpandQuant"
77 long = "dt-var-exp-quant"
81 help = "expand datatype variables bound to one constructor in quantifiers"
86 long = "ite-lift-quant=MODE"
87 type = "CVC4::theory::quantifiers::IteLiftQuantMode"
88 default = "CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE"
89 handler = "stringToIteLiftQuantMode"
90 includes = ["options/quantifiers_modes.h"]
91 help = "ite lifting mode for quantified formulas"
94 name = "condVarSplitQuant"
96 long = "cond-var-split-quant"
100 help = "split quantified formulas that lead to variable eliminations"
103 name = "condVarSplitQuantAgg"
105 long = "cond-var-split-agg-quant"
109 help = "aggressive split quantified formulas that lead to variable eliminations"
112 name = "iteDtTesterSplitQuant"
114 long = "ite-dtt-split-quant"
117 help = "split ites with dt testers as conditions"
119 # Whether to pre-skolemize quantifier bodies.
120 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
121 # forall x. P( x ) => f( S( x ) ) = x
123 name = "preSkolemQuant"
125 long = "pre-skolem-quant"
128 help = "apply skolemization eagerly to bodies of quantified formulas"
131 name = "preSkolemQuantNested"
133 long = "pre-skolem-quant-nested"
136 help = "apply skolemization to nested quantified formulas"
139 name = "preSkolemQuantAgg"
141 long = "pre-skolem-quant-agg"
144 help = "apply skolemization to quantified formulas aggressively"
147 name = "aggressiveMiniscopeQuant"
149 long = "ag-miniscope-quant"
153 help = "perform aggressive miniscoping for quantifiers"
156 name = "elimTautQuant"
158 long = "elim-taut-quant"
162 help = "eliminate tautological disjuncts of quantified formulas"
165 name = "elimExtArithQuant"
167 long = "elim-ext-arith-quant"
170 help = "eliminate extended arithmetic symbols in quantified formulas"
173 name = "condRewriteQuant"
175 long = "cond-rewrite-quant"
179 help = "conditional rewriting of quantified formulas"
182 name = "globalNegate"
184 long = "global-negate"
187 help = "do global negation of input formula"
189 #### E-matching options
197 help = "whether to do heuristic E-matching"
202 long = "term-db-mode=MODE"
203 type = "CVC4::theory::quantifiers::TermDbMode"
204 default = "CVC4::theory::quantifiers::TERM_DB_ALL"
205 handler = "stringToTermDbMode"
206 includes = ["options/quantifiers_modes.h"]
207 help = "which ground terms to consider for instantiation"
210 name = "registerQuantBodyTerms"
212 long = "register-quant-body-terms"
216 help = "consider ground terms within bodies of quantified formulas for matching"
219 name = "inferArithTriggerEq"
221 long = "infer-arith-trigger-eq"
225 help = "infer equalities for trigger terms based on solving arithmetic equalities"
228 name = "strictTriggers"
230 long = "strict-triggers"
234 help = "only instantiate quantifiers with user patterns based on triggers"
237 name = "relevantTriggers"
239 long = "relevant-triggers"
243 help = "prefer triggers that are more relevant based on SInE style analysis"
246 name = "relationalTriggers"
248 long = "relational-triggers"
252 help = "choose relational triggers such as x = f(y), x >= f(y)"
255 name = "purifyTriggers"
257 long = "purify-triggers"
260 help = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1"
263 name = "purifyDtTriggers"
265 long = "purify-dt-triggers"
268 help = "purify dt triggers, match all constructors of correct form instead of selectors"
271 name = "pureThTriggers"
273 long = "pure-th-triggers"
276 help = "use pure theory terms as single triggers"
279 name = "partialTriggers"
281 long = "partial-triggers"
284 help = "use triggers that do not contain all free variables"
287 name = "multiTriggerWhenSingle"
289 long = "multi-trigger-when-single"
293 help = "select multi triggers when single triggers exist"
296 name = "multiTriggerPriority"
298 long = "multi-trigger-priority"
302 help = "only try multi triggers if single triggers give no instantiations"
305 name = "multiTriggerCache"
307 long = "multi-trigger-cache"
311 help = "caching version of multi triggers"
314 name = "multiTriggerLinear"
316 long = "multi-trigger-linear"
320 help = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms"
323 name = "triggerSelMode"
325 long = "trigger-sel=MODE"
326 type = "CVC4::theory::quantifiers::TriggerSelMode"
327 default = "CVC4::theory::quantifiers::TRIGGER_SEL_MIN"
328 handler = "stringToTriggerSelMode"
329 includes = ["options/quantifiers_modes.h"]
330 help = "selection mode for triggers"
333 name = "triggerActiveSelMode"
335 long = "trigger-active-sel=MODE"
336 type = "CVC4::theory::quantifiers::TriggerActiveSelMode"
337 default = "CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL"
338 handler = "stringToTriggerActiveSelMode"
339 includes = ["options/quantifiers_modes.h"]
340 help = "selection mode to activate triggers"
343 name = "userPatternsQuant"
345 long = "user-pat=MODE"
346 type = "CVC4::theory::quantifiers::UserPatMode"
347 default = "CVC4::theory::quantifiers::USER_PAT_MODE_TRUST"
348 handler = "stringToUserPatMode"
349 includes = ["options/quantifiers_modes.h"]
350 help = "policy for handling user-provided patterns for quantifier instantiation"
353 name = "incrementTriggers"
355 long = "increment-triggers"
359 help = "generate additional triggers as needed during search"
362 name = "instWhenMode"
364 long = "inst-when=MODE"
365 type = "CVC4::theory::quantifiers::InstWhenMode"
366 default = "CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL"
367 handler = "stringToInstWhenMode"
368 predicates = ["checkInstWhenMode"]
369 includes = ["options/quantifiers_modes.h"]
370 help = "when to apply instantiation"
373 name = "instWhenStrictInterleave"
375 long = "inst-when-strict-interleave"
378 help = "ensure theory combination and standard quantifier effort strategies take turns"
381 name = "instWhenPhase"
383 long = "inst-when-phase=N"
386 help = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen"
389 name = "instWhenTcFirst"
391 long = "inst-when-tc-first"
394 help = "allow theory combination to happen once initially, before quantifier strategies are run"
397 name = "quantModelEe"
399 long = "quant-model-ee"
403 help = "use equality engine of model for last call effort"
406 name = "instMaxLevel"
408 long = "inst-max-level=N"
411 help = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)"
414 name = "instLevelInputOnly"
416 long = "inst-level-input-only"
420 help = "only input terms are assigned instantiation level zero"
423 name = "quantRepMode"
425 long = "quant-rep-mode=MODE"
426 type = "CVC4::theory::quantifiers::QuantRepMode"
427 default = "CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST"
428 handler = "stringToQuantRepMode"
429 includes = ["options/quantifiers_modes.h"]
430 help = "selection mode for representatives in quantifiers engine"
433 name = "fullSaturateQuant"
435 long = "full-saturate-quant"
438 help = "when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown"
441 name = "fullSaturateQuantRd"
443 long = "full-saturate-quant-rd"
447 help = "whether to use relevant domain first for full saturation instantiation strategy"
450 name = "fullSaturateInterleave"
452 long = "fs-interleave"
456 help = "interleave full saturate instantiation with other techniques"
459 name = "literalMatchMode"
461 long = "literal-matching=MODE"
462 type = "CVC4::theory::quantifiers::LiteralMatchMode"
463 default = "CVC4::theory::quantifiers::LITERAL_MATCH_USE"
464 handler = "stringToLiteralMatchMode"
465 predicates = ["checkLiteralMatchMode"]
466 includes = ["options/quantifiers_modes.h"]
468 help = "choose literal matching mode"
470 ### Finite model finding options
473 name = "finiteModelFind"
475 long = "finite-model-find"
478 help = "use finite model finding heuristic for quantifier instantiation"
481 name = "quantFunWellDefined"
483 long = "quant-fun-wd"
487 help = "assume that function defined by quantifiers are well defined"
490 name = "fmfFunWellDefined"
495 help = "find models for recursively defined functions, assumes functions are admissible"
498 name = "fmfFunWellDefinedRelevant"
504 help = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant"
507 name = "fmfEmptySorts"
509 long = "fmf-empty-sorts"
513 help = "allow finite model finding to assume sorts that do not occur in ground assertions are empty"
519 type = "CVC4::theory::quantifiers::MbqiMode"
520 default = "CVC4::theory::quantifiers::MBQI_FMC"
521 handler = "stringToMbqiMode"
522 predicates = ["checkMbqiMode"]
523 includes = ["options/quantifiers_modes.h"]
524 help = "choose mode for model-based quantifier instantiation"
527 name = "fmfOneInstPerRound"
529 long = "mbqi-one-inst-per-round"
532 help = "only add one instantiation per quantifier per round for mbqi"
535 name = "fmfOneQuantPerRound"
537 long = "mbqi-one-quant-per-round"
541 help = "only add instantiations for one quantifier per round for mbqi"
544 name = "mbqiInterleave"
546 long = "mbqi-interleave"
550 help = "interleave model-based quantifier instantiation with other techniques"
553 name = "fmfInstEngine"
555 long = "fmf-inst-engine"
558 help = "use instantiation engine in conjunction with finite model finding"
563 long = "fmf-inst-gen"
567 help = "enable Inst-Gen instantiation techniques for finite model finding"
570 name = "fmfInstGenOneQuantPerRound"
572 long = "fmf-inst-gen-one-quant-per-round"
576 help = "only perform Inst-Gen instantiation techniques on one quantifier per round"
579 name = "fmfFreshDistConst"
581 long = "fmf-fresh-dc"
585 help = "use fresh distinguished representative when applying Inst-Gen techniques"
588 name = "fmfFmcSimple"
590 long = "fmf-fmc-simple"
594 help = "simple models in full model check for finite model finding"
599 long = "fmf-bound-int"
602 help = "finite model finding on bounded integer quantification"
610 help = "finite model finding on bounded quantification"
613 name = "fmfBoundLazy"
615 long = "fmf-bound-lazy"
618 help = "enforce bounds for bounded quantification lazily via use of proxy variables"
621 name = "fmfTypeCompletionThresh"
623 long = "fmf-type-completion-thresh=N"
627 help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
630 name = "quantConflictFind"
635 help = "enable conflict find mechanism for quantifiers"
640 long = "quant-cf-mode=MODE"
641 type = "CVC4::theory::quantifiers::QcfMode"
642 default = "CVC4::theory::quantifiers::QCF_PROP_EQ"
643 handler = "stringToQcfMode"
644 includes = ["options/quantifiers_modes.h"]
646 help = "what effort to apply conflict find mechanism"
651 long = "quant-cf-when=MODE"
652 type = "CVC4::theory::quantifiers::QcfWhenMode"
653 default = "CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT"
654 handler = "stringToQcfWhenMode"
655 includes = ["options/quantifiers_modes.h"]
657 help = "when to invoke conflict find mechanism for quantifiers"
660 name = "qcfTConstraint"
662 long = "qcf-tconstraint"
665 help = "enable entailment checks for t-constraints in qcf algorithm"
668 name = "qcfAllConflict"
670 long = "qcf-all-conflict"
673 help = "add all available conflicting instances during conflict-based instantiation"
676 name = "qcfNestedConflict"
678 long = "qcf-nested-conflict"
682 help = "consider conflicts for nested quantifiers"
691 help = "qcf experimental variable ordering"
694 name = "instNoEntail"
696 long = "inst-no-entail"
699 help = "do not consider instances of quantified formulas that are currently entailed"
702 name = "instNoModelTrue"
704 long = "inst-no-model-true"
707 help = "do not consider instances of quantified formulas that are currently true in model, if it is available"
710 name = "instPropagate"
715 help = "internal propagation for instantiations for selecting relevant instances"
718 name = "qcfEagerTest"
720 long = "qcf-eager-test"
724 help = "optimization, test qcf instances eagerly"
727 name = "qcfEagerCheckRd"
729 long = "qcf-eager-check-rd"
733 help = "optimization, eagerly check relevant domain of matched position"
742 help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
744 ### Rewrite rules options
747 name = "quantRewriteRules"
749 long = "rewrite-rules"
753 help = "use rewrite rules module"
756 name = "rrOneInstPerRound"
758 long = "rr-one-inst-per-round"
762 help = "add one instance of rewrite rule per round"
764 ### Induction options
767 name = "quantInduction"
773 help = "use all available techniques for inductive reasoning"
776 name = "dtStcInduction"
781 help = "apply strengthening for existential quantification over datatypes based on structural induction"
784 name = "intWfInduction"
789 help = "apply strengthening for integers based on well-founded induction"
792 name = "conjectureGen"
794 long = "conjecture-gen"
797 help = "generate candidate conjectures for inductive proofs"
800 name = "conjectureGenPerRound"
802 long = "conjecture-gen-per-round=N"
806 help = "number of conjectures to generate per instantiation round"
809 name = "conjectureNoFilter"
811 long = "conjecture-no-filter"
815 help = "do not filter conjectures"
818 name = "conjectureFilterActiveTerms"
820 long = "conjecture-filter-active-terms"
823 help = "filter based on active terms"
826 name = "conjectureFilterCanonical"
828 long = "conjecture-filter-canonical"
831 help = "filter based on canonicity"
834 name = "conjectureFilterModel"
836 long = "conjecture-filter-model"
839 help = "filter based on model"
842 name = "conjectureGenGtEnum"
844 long = "conjecture-gen-gt-enum=N"
848 help = "number of ground terms to generate for model filtering"
851 name = "conjectureUeeIntro"
853 long = "conjecture-gen-uee-intro"
857 help = "more aggressive merging for universal equality engine, introduces terms"
860 name = "conjectureGenMaxDepth"
862 long = "conjecture-gen-max-depth=N"
866 help = "maximum depth of terms to consider for conjectures"
868 ### Synthesis options
871 name = "sygusInference"
873 long = "sygus-inference"
877 help = "attempt to preprocess arbitrary inputs to sygus conjectures"
880 name = "ceGuidedInst"
885 help = "counterexample-guided quantifier instantiation for sygus"
888 name = "cegqiSingleInvMode"
890 long = "cegqi-si=MODE"
891 type = "CVC4::theory::quantifiers::CegqiSingleInvMode"
892 default = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE"
893 handler = "stringToCegqiSingleInvMode"
894 includes = ["options/quantifiers_modes.h"]
895 help = "mode for processing single invocation synthesis conjectures"
898 name = "cegqiSingleInvPartial"
900 long = "cegqi-si-partial"
904 help = "combined techniques for synthesis conjectures that are partially single invocation"
907 name = "cegqiSingleInvReconstruct"
909 long = "cegqi-si-rcons=MODE"
910 type = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode"
911 default = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT"
912 handler = "stringToCegqiSingleInvRconsMode"
913 includes = ["options/quantifiers_modes.h"]
914 help = "policy for reconstructing solutions for single invocation conjectures"
917 name = "cegqiSingleInvReconstructLimit"
919 long = "cegqi-si-rcons-limit=N"
923 help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)"
926 name = "cegqiSingleInvReconstructConst"
928 long = "cegqi-si-reconstruct-const"
932 help = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
935 name = "cegqiSolMinCore"
937 long = "cegqi-si-sol-min-core"
941 help = "minimize solutions for single invocation conjectures based on unsat core"
944 name = "cegqiSolMinInst"
946 long = "cegqi-si-sol-min-inst"
950 help = "minimize individual instantiations for single invocation conjectures based on unsat core"
953 name = "cegqiSingleInvAbort"
955 long = "cegqi-si-abort"
959 help = "abort if synthesis conjecture is not single invocation"
962 name = "sygusConstRepairAbort"
964 long = "sygus-crepair-abort"
968 help = "abort if constant repair techniques are not applicable"
976 help = "Unification-based function synthesis"
979 name = "sygusUnifCondIndependent"
981 long = "sygus-unif-cond-independent"
984 help = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
987 name = "sygusUnifBooleanHeuristicDt"
989 long = "sygus-unif-boolean-heuristic-dt"
992 help = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
995 name = "sygusUnifCondIndNoRepeatSol"
997 long = "sygus-unif-cond-indpendent-no-repeat-sol"
1000 help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis"
1003 name = "sygusBoolIteReturnConst"
1004 category = "regular"
1005 long = "sygus-bool-ite-return-const"
1008 help = "Only use Boolean constants for return values in unification-based function synthesis"
1011 name = "sygusQePreproc"
1012 category = "regular"
1013 long = "sygus-qe-preproc"
1017 help = "use quantifier elimination as a preprocessing step for sygus"
1020 name = "sygusRepairConst"
1021 category = "regular"
1022 long = "sygus-repair-const"
1025 help = "use approach to repair constants in sygus candidate solutions"
1028 name = "sygusRepairConstTimeout"
1029 category = "regular"
1030 long = "sygus-repair-const-timeout=N"
1031 type = "unsigned long"
1032 help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
1035 name = "sygusEnumVarAgnostic"
1036 category = "regular"
1037 long = "sygus-var-agnostic"
1040 help = "when possible, use variable-agnostic enumerators"
1043 name = "sygusMinGrammar"
1044 category = "regular"
1045 long = "sygus-min-grammar"
1049 help = "statically minimize sygus grammars"
1052 name = "sygusAddConstGrammar"
1053 category = "regular"
1054 long = "sygus-add-const-grammar"
1058 help = "statically add constants appearing in conjecture to grammars"
1061 name = "sygusGrammarNorm"
1062 category = "regular"
1063 long = "sygus-grammar-norm"
1067 help = "statically normalize sygus grammars based on flattening (linearization)"
1070 name = "sygusTemplEmbedGrammar"
1071 category = "regular"
1072 long = "sygus-templ-embed-grammar"
1076 help = "embed sygus templates into grammars"
1079 name = "sygusInvTemplMode"
1080 category = "regular"
1081 long = "sygus-inv-templ=MODE"
1082 type = "CVC4::theory::quantifiers::SygusInvTemplMode"
1083 default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
1084 handler = "stringToSygusInvTemplMode"
1085 includes = ["options/quantifiers_modes.h"]
1087 help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
1090 name = "sygusInvTemplWhenSyntax"
1091 category = "regular"
1092 long = "sygus-inv-templ-when-sg"
1096 help = "use invariant templates (with solution reconstruction) for syntax guided problems"
1099 name = "sygusInvAutoUnfold"
1100 category = "regular"
1101 long = "sygus-auto-unfold"
1105 help = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1108 name = "sygusUnifPbe"
1109 category = "regular"
1113 help = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
1116 name = "sygusPbeMultiFair"
1117 category = "regular"
1118 long = "sygus-pbe-multi-fair"
1121 help = "when using multiple enumerators, ensure that we only register value of minimial term size"
1124 name = "sygusPbeMultiFairDiff"
1125 category = "regular"
1126 long = "sygus-pbe-multi-fair-diff=N"
1129 help = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)"
1132 name = "sygusEvalUnfold"
1133 category = "regular"
1134 long = "sygus-eval-unfold"
1138 help = "do unfolding of sygus evaluation functions"
1141 name = "sygusEvalUnfoldBool"
1142 category = "regular"
1143 long = "sygus-eval-unfold-bool"
1147 help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1150 name = "sygusRefEval"
1151 category = "regular"
1152 long = "sygus-ref-eval"
1156 help = "direct evaluation of refinement lemmas for conflict analysis"
1159 name = "sygusStream"
1160 category = "regular"
1161 long = "sygus-stream"
1164 help = "enumerate a stream of solutions instead of terminating after the first one"
1167 name = "sygusVerifySubcall"
1168 category = "regular"
1169 long = "sygus-verify-subcall"
1172 help = "use separate copy of the SMT solver for verification lemmas in sygus"
1175 name = "sygusExtRew"
1176 category = "regular"
1177 long = "sygus-ext-rew"
1180 help = "use extended rewriter for sygus"
1183 name = "cegisSample"
1184 category = "regular"
1185 long = "cegis-sample=MODE"
1186 type = "CVC4::theory::quantifiers::CegisSampleMode"
1187 default = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE"
1188 handler = "stringToCegisSampleMode"
1189 includes = ["options/quantifiers_modes.h"]
1190 help = "mode for using samples in the counterexample-guided inductive synthesis loop"
1193 name = "minSynthSol"
1194 category = "regular"
1195 long = "min-synth-sol"
1198 help = "Minimize synthesis solutions"
1201 name = "sygusEvalOpt"
1202 category = "regular"
1203 long = "sygus-eval-opt"
1206 help = "use optimized approach for evaluation in sygus"
1209 name = "sygusArgRelevant"
1210 category = "regular"
1211 long = "sygus-arg-relevant"
1214 help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
1216 # Internal uses of sygus
1220 category = "regular"
1225 help = "use sygus to enumerate and verify correctness of rewrite rules via sampling"
1228 name = "sygusRewSynth"
1229 category = "regular"
1230 long = "sygus-rr-synth"
1233 help = "use sygus to enumerate candidate rewrite rules via sampling"
1236 name = "sygusRewSynthFilterOrder"
1237 category = "regular"
1238 long = "sygus-rr-synth-filter-order"
1241 help = "filter candidate rewrites based on variable ordering"
1244 name = "sygusRewSynthFilterMatch"
1245 category = "regular"
1246 long = "sygus-rr-synth-filter-match"
1249 help = "filter candidate rewrites based on matching"
1252 name = "sygusRewSynthFilterCong"
1253 category = "regular"
1254 long = "sygus-rr-synth-filter-cong"
1257 help = "filter candidate rewrites based on congruence"
1260 name = "sygusRewVerify"
1261 category = "regular"
1262 long = "sygus-rr-verify"
1265 help = "use sygus to verify the correctness of rewrite rules via sampling"
1268 name = "sygusRewVerifyAbort"
1269 category = "regular"
1270 long = "sygus-rr-verify-abort"
1273 help = "abort when sygus-rr-verify finds an instance of unsoundness"
1276 name = "sygusSamples"
1277 category = "regular"
1278 long = "sygus-samples=N"
1281 help = "number of points to consider when doing sygus rewriter sample testing"
1284 name = "sygusSampleGrammar"
1285 category = "regular"
1286 long = "sygus-sample-grammar"
1290 help = "when applicable, use grammar for choosing sample points"
1293 name = "sygusSampleFpUniform"
1294 category = "regular"
1295 long = "sygus-sample-fp-uniform"
1298 help = "sample floating-point values uniformly instead of in a biased fashion"
1301 name = "sygusRewSynthAccel"
1302 category = "regular"
1303 long = "sygus-rr-synth-accel"
1306 help = "add dynamic symmetry breaking clauses based on candidate rewrites"
1309 name = "sygusRewSynthCheck"
1310 category = "regular"
1311 long = "sygus-rr-synth-check"
1314 help = "use satisfiability check to verify correctness of candidate rewrites"
1317 name = "sygusExprMinerCheckTimeout"
1318 category = "regular"
1319 long = "sygus-expr-miner-check-timeout=N"
1320 type = "unsigned long"
1321 help = "timeout (in milliseconds) for satisfiability checks in expression miners"
1323 # CEGQI applied to general quantified formulas
1327 category = "regular"
1331 help = "turns on counterexample-based quantifier instantiation"
1334 name = "cbqiFullEffort"
1335 category = "regular"
1339 help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1342 name = "recurseCbqi"
1343 category = "regular"
1344 long = "cbqi-recurse"
1348 help = "turns on recursive counterexample-based quantifier instantiation"
1352 category = "regular"
1356 help = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1360 category = "regular"
1364 help = "guide instantiations by model values for counterexample-based quantifier instantiation"
1368 category = "regular"
1372 help = "apply counterexample-based instantiation to all quantified formulas"
1375 name = "cbqiMultiInst"
1376 category = "regular"
1377 long = "cbqi-multi-inst"
1380 help = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1383 name = "cbqiRepeatLit"
1384 category = "regular"
1385 long = "cbqi-repeat-lit"
1388 help = "solve literals more than once in counterexample-based quantifier instantiation"
1391 name = "cbqiInnermost"
1392 category = "regular"
1393 long = "cbqi-innermost"
1396 help = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1399 name = "cbqiNestedQE"
1400 category = "regular"
1401 long = "cbqi-nested-qe"
1404 help = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1406 # CEGQI for arithmetic
1409 name = "cbqiUseInfInt"
1410 category = "regular"
1411 long = "cbqi-use-inf-int"
1414 help = "use integer infinity for vts in counterexample-based quantifier instantiation"
1417 name = "cbqiUseInfReal"
1418 category = "regular"
1419 long = "cbqi-use-inf-real"
1422 help = "use real infinity for vts in counterexample-based quantifier instantiation"
1425 name = "cbqiPreRegInst"
1426 category = "regular"
1427 long = "cbqi-prereg-inst"
1430 help = "preregister ground instantiations in counterexample-based quantifier instantiation"
1433 name = "cbqiMinBounds"
1434 category = "regular"
1435 long = "cbqi-min-bounds"
1439 help = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1442 name = "cbqiRoundUpLowerLia"
1443 category = "regular"
1444 long = "cbqi-round-up-lia"
1448 help = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1451 name = "cbqiMidpoint"
1452 category = "regular"
1453 long = "cbqi-midpoint"
1456 help = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1460 category = "regular"
1465 help = "non-optimal bounds for counterexample-based quantifier instantiation"
1468 name = "cbqiLitDepend"
1469 category = "regular"
1470 long = "cbqi-lit-dep"
1474 help = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
1480 category = "regular"
1484 help = "infer whether in effectively propositional fragment, use for cbqi"
1487 name = "quantEprMatching"
1488 category = "regular"
1489 long = "quant-epr-match"
1493 help = "use matching heuristics for EPR instantiation"
1499 category = "regular"
1503 help = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1506 name = "cbqiBvInterleaveValue"
1507 category = "regular"
1508 long = "cbqi-bv-interleave-value"
1511 help = "interleave model value instantiation with word-level inversion approach"
1514 name = "cbqiBvIneqMode"
1515 category = "regular"
1516 long = "cbqi-bv-ineq=MODE"
1517 type = "CVC4::theory::quantifiers::CbqiBvIneqMode"
1518 default = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY"
1519 handler = "stringToCbqiBvIneqMode"
1520 includes = ["options/quantifiers_modes.h"]
1521 help = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1524 name = "cbqiBvRmExtract"
1525 category = "regular"
1526 long = "cbqi-bv-rm-extract"
1529 help = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1532 name = "cbqiBvLinearize"
1533 category = "regular"
1534 long = "cbqi-bv-linear"
1537 help = "linearize adder chains for variables"
1540 name = "cbqiBvSolveNl"
1541 category = "regular"
1542 long = "cbqi-bv-solve-nl"
1545 help = "try to solve non-linear bv literals using model value projections"
1548 name = "cbqiBvConcInv"
1549 category = "regular"
1550 long = "cbqi-bv-concat-inv"
1553 help = "compute inverse for concat over equalities rather than producing an invertibility condition"
1555 ### Local theory extensions options
1558 name = "localTheoryExt"
1559 category = "regular"
1560 long = "local-t-ext"
1564 help = "do instantiation based on local theory extensions"
1567 name = "ltePartialInst"
1568 category = "regular"
1569 long = "lte-partial-inst"
1573 help = "partially instantiate local theory quantifiers"
1576 name = "lteRestrictInstClosure"
1577 category = "regular"
1578 long = "lte-restrict-inst-closure"
1582 help = "treat arguments of inst closure as restricted terms for instantiation"
1584 ### Reduction options
1587 name = "quantAlphaEquiv"
1588 category = "regular"
1589 long = "quant-alpha-equiv"
1593 help = "infer alpha equivalence between quantified formulas"
1596 name = "macrosQuant"
1597 category = "regular"
1598 long = "macros-quant"
1601 help = "perform quantifiers macro expansion"
1604 name = "macrosQuantMode"
1605 category = "regular"
1606 long = "macros-quant-mode=MODE"
1607 type = "CVC4::theory::quantifiers::MacrosQuantMode"
1608 default = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF"
1609 handler = "stringToMacrosQuantMode"
1610 includes = ["options/quantifiers_modes.h"]
1612 help = "mode for quantifiers macro expansion"
1615 name = "quantDynamicSplit"
1616 category = "regular"
1617 long = "quant-dsplit-mode=MODE"
1618 type = "CVC4::theory::quantifiers::QuantDSplitMode"
1619 default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
1620 handler = "stringToQuantDSplitMode"
1621 includes = ["options/quantifiers_modes.h"]
1622 help = "mode for dynamic quantifiers splitting"
1625 name = "quantAntiSkolem"
1626 category = "regular"
1627 long = "quant-anti-skolem"
1630 help = "perform anti-skolemization for quantified formulas"
1632 ### Higher-order options
1636 category = "regular"
1637 long = "ho-matching"
1641 help = "do higher-order matching algorithm for triggers with variable operators"
1644 name = "hoMatchingVarArgPriority"
1645 category = "regular"
1646 long = "ho-matching-var-priority"
1650 help = "give priority to variable arguments over constant arguments"
1653 name = "hoMergeTermDb"
1654 category = "regular"
1655 long = "ho-merge-term-db"
1659 help = "merge term indices modulo equality"
1664 name = "trackInstLemmas"
1665 category = "regular"
1666 long = "track-inst-lemmas"
1669 help = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"