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"
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 = "inferArithTriggerEqExp"
230 long = "infer-arith-trigger-eq-exp"
234 help = "record explanations for inferArithTriggerEq"
237 name = "strictTriggers"
239 long = "strict-triggers"
243 help = "only instantiate quantifiers with user patterns based on triggers"
246 name = "relevantTriggers"
248 long = "relevant-triggers"
252 help = "prefer triggers that are more relevant based on SInE style analysis"
255 name = "relationalTriggers"
257 long = "relational-triggers"
261 help = "choose relational triggers such as x = f(y), x >= f(y)"
264 name = "purifyTriggers"
266 long = "purify-triggers"
269 help = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1"
272 name = "purifyDtTriggers"
274 long = "purify-dt-triggers"
277 help = "purify dt triggers, match all constructors of correct form instead of selectors"
280 name = "pureThTriggers"
282 long = "pure-th-triggers"
285 help = "use pure theory terms as single triggers"
288 name = "partialTriggers"
290 long = "partial-triggers"
293 help = "use triggers that do not contain all free variables"
296 name = "multiTriggerWhenSingle"
298 long = "multi-trigger-when-single"
302 help = "select multi triggers when single triggers exist"
305 name = "multiTriggerPriority"
307 long = "multi-trigger-priority"
311 help = "only try multi triggers if single triggers give no instantiations"
314 name = "multiTriggerCache"
316 long = "multi-trigger-cache"
320 help = "caching version of multi triggers"
323 name = "multiTriggerLinear"
325 long = "multi-trigger-linear"
329 help = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms"
332 name = "triggerSelMode"
335 type = "CVC4::theory::quantifiers::TriggerSelMode"
336 default = "CVC4::theory::quantifiers::TRIGGER_SEL_MIN"
337 handler = "stringToTriggerSelMode"
338 includes = ["options/quantifiers_modes.h"]
339 help = "selection mode for triggers"
342 name = "triggerActiveSelMode"
344 long = "trigger-active-sel"
345 type = "CVC4::theory::quantifiers::TriggerActiveSelMode"
346 default = "CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL"
347 handler = "stringToTriggerActiveSelMode"
348 includes = ["options/quantifiers_modes.h"]
349 help = "selection mode to activate triggers"
352 name = "userPatternsQuant"
354 long = "user-pat=MODE"
355 type = "CVC4::theory::quantifiers::UserPatMode"
356 default = "CVC4::theory::quantifiers::USER_PAT_MODE_TRUST"
357 handler = "stringToUserPatMode"
358 includes = ["options/quantifiers_modes.h"]
359 help = "policy for handling user-provided patterns for quantifier instantiation"
362 name = "incrementTriggers"
364 long = "increment-triggers"
368 help = "generate additional triggers as needed during search"
371 name = "instWhenMode"
373 long = "inst-when=MODE"
374 type = "CVC4::theory::quantifiers::InstWhenMode"
375 default = "CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL"
376 handler = "stringToInstWhenMode"
377 predicates = ["checkInstWhenMode"]
378 includes = ["options/quantifiers_modes.h"]
379 help = "when to apply instantiation"
382 name = "instWhenStrictInterleave"
384 long = "inst-when-strict-interleave"
387 help = "ensure theory combination and standard quantifier effort strategies take turns"
390 name = "instWhenPhase"
392 long = "inst-when-phase=N"
395 help = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen"
398 name = "instWhenTcFirst"
400 long = "inst-when-tc-first"
403 help = "allow theory combination to happen once initially, before quantifier strategies are run"
406 name = "quantModelEe"
408 long = "quant-model-ee"
412 help = "use equality engine of model for last call effort"
415 name = "instMaxLevel"
417 long = "inst-max-level=N"
420 help = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)"
423 name = "instLevelInputOnly"
425 long = "inst-level-input-only"
429 help = "only input terms are assigned instantiation level zero"
432 name = "quantRepMode"
434 long = "quant-rep-mode=MODE"
435 type = "CVC4::theory::quantifiers::QuantRepMode"
436 default = "CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST"
437 handler = "stringToQuantRepMode"
438 includes = ["options/quantifiers_modes.h"]
439 help = "selection mode for representatives in quantifiers engine"
442 name = "fullSaturateQuant"
444 long = "full-saturate-quant"
447 help = "when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown"
450 name = "fullSaturateQuantRd"
452 long = "full-saturate-quant-rd"
456 help = "whether to use relevant domain first for full saturation instantiation strategy"
459 name = "fullSaturateInterleave"
461 long = "fs-interleave"
465 help = "interleave full saturate instantiation with other techniques"
468 name = "literalMatchMode"
470 long = "literal-matching=MODE"
471 type = "CVC4::theory::quantifiers::LiteralMatchMode"
472 default = "CVC4::theory::quantifiers::LITERAL_MATCH_USE"
473 handler = "stringToLiteralMatchMode"
474 predicates = ["checkLiteralMatchMode"]
475 includes = ["options/quantifiers_modes.h"]
477 help = "choose literal matching mode"
479 ### Finite model finding options
482 name = "finiteModelFind"
484 long = "finite-model-find"
487 help = "use finite model finding heuristic for quantifier instantiation"
490 name = "quantFunWellDefined"
492 long = "quant-fun-wd"
496 help = "assume that function defined by quantifiers are well defined"
499 name = "fmfFunWellDefined"
504 help = "find models for recursively defined functions, assumes functions are admissible"
507 name = "fmfFunWellDefinedRelevant"
513 help = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant"
516 name = "fmfEmptySorts"
518 long = "fmf-empty-sorts"
522 help = "allow finite model finding to assume sorts that do not occur in ground assertions are empty"
528 type = "CVC4::theory::quantifiers::MbqiMode"
529 default = "CVC4::theory::quantifiers::MBQI_FMC"
530 handler = "stringToMbqiMode"
531 predicates = ["checkMbqiMode"]
532 includes = ["options/quantifiers_modes.h"]
533 help = "choose mode for model-based quantifier instantiation"
536 name = "fmfOneInstPerRound"
538 long = "mbqi-one-inst-per-round"
541 help = "only add one instantiation per quantifier per round for mbqi"
544 name = "fmfOneQuantPerRound"
546 long = "mbqi-one-quant-per-round"
550 help = "only add instantiations for one quantifier per round for mbqi"
553 name = "mbqiInterleave"
555 long = "mbqi-interleave"
559 help = "interleave model-based quantifier instantiation with other techniques"
562 name = "fmfInstEngine"
564 long = "fmf-inst-engine"
567 help = "use instantiation engine in conjunction with finite model finding"
572 long = "fmf-inst-gen"
576 help = "enable Inst-Gen instantiation techniques for finite model finding"
579 name = "fmfInstGenOneQuantPerRound"
581 long = "fmf-inst-gen-one-quant-per-round"
585 help = "only perform Inst-Gen instantiation techniques on one quantifier per round"
588 name = "fmfFreshDistConst"
590 long = "fmf-fresh-dc"
594 help = "use fresh distinguished representative when applying Inst-Gen techniques"
597 name = "fmfFmcSimple"
599 long = "fmf-fmc-simple"
603 help = "simple models in full model check for finite model finding"
608 long = "fmf-bound-int"
611 help = "finite model finding on bounded integer quantification"
619 help = "finite model finding on bounded quantification"
622 name = "fmfBoundLazy"
624 long = "fmf-bound-lazy"
627 help = "enforce bounds for bounded quantification lazily via use of proxy variables"
630 name = "fmfBoundMinMode"
632 long = "fmf-bound-min-mode=MODE"
633 type = "CVC4::theory::quantifiers::FmfBoundMinMode"
634 default = "CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE"
635 handler = "stringToFmfBoundMinMode"
636 includes = ["options/quantifiers_modes.h"]
638 help = "mode for which types of bounds to minimize via first decision heuristics"
641 name = "quantConflictFind"
646 help = "enable conflict find mechanism for quantifiers"
651 long = "quant-cf-mode=MODE"
652 type = "CVC4::theory::quantifiers::QcfMode"
653 default = "CVC4::theory::quantifiers::QCF_PROP_EQ"
654 handler = "stringToQcfMode"
655 includes = ["options/quantifiers_modes.h"]
657 help = "what effort to apply conflict find mechanism"
662 long = "quant-cf-when=MODE"
663 type = "CVC4::theory::quantifiers::QcfWhenMode"
664 default = "CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT"
665 handler = "stringToQcfWhenMode"
666 includes = ["options/quantifiers_modes.h"]
668 help = "when to invoke conflict find mechanism for quantifiers"
671 name = "qcfTConstraint"
673 long = "qcf-tconstraint"
676 help = "enable entailment checks for t-constraints in qcf algorithm"
679 name = "qcfAllConflict"
681 long = "qcf-all-conflict"
684 help = "add all available conflicting instances during conflict-based instantiation"
687 name = "qcfNestedConflict"
689 long = "qcf-nested-conflict"
693 help = "consider conflicts for nested quantifiers"
702 help = "qcf experimental variable ordering"
705 name = "instNoEntail"
707 long = "inst-no-entail"
710 help = "do not consider instances of quantified formulas that are currently entailed"
713 name = "instNoModelTrue"
715 long = "inst-no-model-true"
718 help = "do not consider instances of quantified formulas that are currently true in model, if it is available"
721 name = "instPropagate"
726 help = "internal propagation for instantiations for selecting relevant instances"
729 name = "qcfEagerTest"
731 long = "qcf-eager-test"
735 help = "optimization, test qcf instances eagerly"
738 name = "qcfEagerCheckRd"
740 long = "qcf-eager-check-rd"
744 help = "optimization, eagerly check relevant domain of matched position"
753 help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
755 ### Rewrite rules options
758 name = "quantRewriteRules"
760 long = "rewrite-rules"
764 help = "use rewrite rules module"
767 name = "rrOneInstPerRound"
769 long = "rr-one-inst-per-round"
773 help = "add one instance of rewrite rule per round"
775 ### Induction options
778 name = "quantInduction"
784 help = "use all available techniques for inductive reasoning"
787 name = "dtStcInduction"
792 help = "apply strengthening for existential quantification over datatypes based on structural induction"
795 name = "intWfInduction"
800 help = "apply strengthening for integers based on well-founded induction"
803 name = "conjectureGen"
805 long = "conjecture-gen"
808 help = "generate candidate conjectures for inductive proofs"
811 name = "conjectureGenPerRound"
813 long = "conjecture-gen-per-round=N"
817 help = "number of conjectures to generate per instantiation round"
820 name = "conjectureNoFilter"
822 long = "conjecture-no-filter"
826 help = "do not filter conjectures"
829 name = "conjectureFilterActiveTerms"
831 long = "conjecture-filter-active-terms"
834 help = "filter based on active terms"
837 name = "conjectureFilterCanonical"
839 long = "conjecture-filter-canonical"
842 help = "filter based on canonicity"
845 name = "conjectureFilterModel"
847 long = "conjecture-filter-model"
850 help = "filter based on model"
853 name = "conjectureGenGtEnum"
855 long = "conjecture-gen-gt-enum=N"
859 help = "number of ground terms to generate for model filtering"
862 name = "conjectureUeeIntro"
864 long = "conjecture-gen-uee-intro"
868 help = "more aggressive merging for universal equality engine, introduces terms"
871 name = "conjectureGenMaxDepth"
873 long = "conjecture-gen-max-depth=N"
877 help = "maximum depth of terms to consider for conjectures"
879 ### Synthesis options
882 name = "sygusInference"
884 long = "sygus-inference"
888 help = "attempt to preprocess arbitrary inputs to sygus conjectures"
891 name = "ceGuidedInst"
896 help = "counterexample-guided quantifier instantiation for sygus"
899 name = "cegqiSingleInvMode"
901 long = "cegqi-si=MODE"
902 type = "CVC4::theory::quantifiers::CegqiSingleInvMode"
903 default = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE"
904 handler = "stringToCegqiSingleInvMode"
905 includes = ["options/quantifiers_modes.h"]
906 help = "mode for processing single invocation synthesis conjectures"
909 name = "cegqiSingleInvPartial"
911 long = "cegqi-si-partial"
915 help = "combined techniques for synthesis conjectures that are partially single invocation"
918 name = "cegqiSingleInvReconstruct"
920 long = "cegqi-si-reconstruct"
924 help = "reconstruct solutions for single invocation conjectures in original grammar"
927 name = "cegqiSolMinCore"
929 long = "cegqi-si-sol-min-core"
933 help = "minimize solutions for single invocation conjectures based on unsat core"
936 name = "cegqiSolMinInst"
938 long = "cegqi-si-sol-min-inst"
942 help = "minimize individual instantiations for single invocation conjectures based on unsat core"
945 name = "cegqiSingleInvReconstructConst"
947 long = "cegqi-si-reconstruct-const"
951 help = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
954 name = "cegqiSingleInvAbort"
956 long = "cegqi-si-abort"
960 help = "abort if synthesis conjecture is not single invocation"
968 help = "Unification-based function synthesis"
971 name = "sygusQePreproc"
973 long = "sygus-qe-preproc"
977 help = "use quantifier elimination as a preprocessing step for sygus"
980 name = "sygusMinGrammar"
982 long = "sygus-min-grammar"
986 help = "statically minimize sygus grammars"
989 name = "sygusAddConstGrammar"
991 long = "sygus-add-const-grammar"
995 help = "statically add constants appearing in conjecture to grammars"
998 name = "sygusGrammarNorm"
1000 long = "sygus-grammar-norm"
1004 help = "statically normalize sygus grammars based on flattening (linearization)"
1007 name = "sygusTemplEmbedGrammar"
1008 category = "regular"
1009 long = "sygus-templ-embed-grammar"
1013 help = "embed sygus templates into grammars"
1016 name = "sygusInvTemplMode"
1017 category = "regular"
1018 long = "sygus-inv-templ=MODE"
1019 type = "CVC4::theory::quantifiers::SygusInvTemplMode"
1020 default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
1021 handler = "stringToSygusInvTemplMode"
1022 includes = ["options/quantifiers_modes.h"]
1024 help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
1027 name = "sygusInvTemplWhenSyntax"
1028 category = "regular"
1029 long = "sygus-inv-templ-when-sg"
1033 help = "use invariant templates (with solution reconstruction) for syntax guided problems"
1036 name = "sygusInvAutoUnfold"
1037 category = "regular"
1038 long = "sygus-auto-unfold"
1042 help = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1045 name = "sygusUnifPbe"
1046 category = "regular"
1050 help = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
1053 name = "sygusDirectEval"
1054 category = "regular"
1055 long = "sygus-direct-eval"
1059 help = "direct unfolding of evaluation functions"
1062 name = "sygusUnfoldBool"
1063 category = "regular"
1064 long = "sygus-unfold-bool"
1068 help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1071 name = "sygusCRefEval"
1072 category = "regular"
1073 long = "sygus-cref-eval"
1077 help = "direct evaluation of refinement lemmas for conflict analysis"
1080 name = "sygusCRefEvalMinExp"
1081 category = "regular"
1082 long = "sygus-cref-eval-min-exp"
1086 help = "use min explain for direct evaluation of refinement lemmas for conflict analysis"
1089 name = "sygusStream"
1090 category = "regular"
1091 long = "sygus-stream"
1094 help = "enumerate a stream of solutions instead of terminating after the first one"
1097 name = "sygusExtRew"
1098 category = "regular"
1099 long = "sygus-ext-rew"
1102 help = "use extended rewriter for sygus"
1105 name = "cegisSample"
1106 category = "regular"
1107 long = "cegis-sample=MODE"
1108 type = "CVC4::theory::quantifiers::CegisSampleMode"
1109 default = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE"
1110 handler = "stringToCegisSampleMode"
1111 includes = ["options/quantifiers_modes.h"]
1112 help = "mode for using samples in the counterexample-guided inductive synthesis loop"
1114 # Internal uses of sygus
1118 category = "regular"
1123 help = "use sygus to enumerate and verify correctness of rewrite rules via sampling"
1126 name = "sygusRewSynth"
1127 category = "regular"
1128 long = "sygus-rr-synth"
1131 help = "use sygus to enumerate candidate rewrite rules via sampling"
1134 name = "sygusRewSynthFilterOrder"
1135 category = "regular"
1136 long = "sygus-rr-synth-filter-order"
1139 help = "filter candidate rewrites based on variable ordering"
1142 name = "sygusRewSynthFilterMatch"
1143 category = "regular"
1144 long = "sygus-rr-synth-filter-match"
1147 help = "filter candidate rewrites based on matching"
1150 name = "sygusRewSynthFilterCong"
1151 category = "regular"
1152 long = "sygus-rr-synth-filter-cong"
1155 help = "filter candidate rewrites based on congruence"
1158 name = "sygusRewVerify"
1159 category = "regular"
1160 long = "sygus-rr-verify"
1163 help = "use sygus to verify the correctness of rewrite rules via sampling"
1166 name = "sygusRewVerifyAbort"
1167 category = "regular"
1168 long = "sygus-rr-verify-abort"
1171 help = "abort when sygus-rr-verify finds an instance of unsoundness"
1174 name = "sygusSamples"
1175 category = "regular"
1176 long = "sygus-samples=N"
1179 help = "number of points to consider when doing sygus rewriter sample testing"
1182 name = "sygusSampleGrammar"
1183 category = "regular"
1184 long = "sygus-sample-grammar"
1188 help = "when applicable, use grammar for choosing sample points"
1191 name = "sygusRewSynthAccel"
1192 category = "regular"
1193 long = "sygus-rr-synth-accel"
1196 help = "add dynamic symmetry breaking clauses based on candidate rewrites"
1199 name = "sygusRewSynthCheck"
1200 category = "regular"
1201 long = "sygus-rr-synth-check"
1204 help = "use satisfiability check to verify correctness of candidate rewrites"
1206 # CEGQI applied to general quantified formulas
1210 category = "regular"
1214 help = "turns on counterexample-based quantifier instantiation"
1217 name = "cbqiFullEffort"
1218 category = "regular"
1222 help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1225 name = "recurseCbqi"
1226 category = "regular"
1227 long = "cbqi-recurse"
1231 help = "turns on recursive counterexample-based quantifier instantiation"
1235 category = "regular"
1239 help = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1243 category = "regular"
1247 help = "guide instantiations by model values for counterexample-based quantifier instantiation"
1251 category = "regular"
1255 help = "apply counterexample-based instantiation to all quantified formulas"
1258 name = "cbqiMultiInst"
1259 category = "regular"
1260 long = "cbqi-multi-inst"
1263 help = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1266 name = "cbqiRepeatLit"
1267 category = "regular"
1268 long = "cbqi-repeat-lit"
1271 help = "solve literals more than once in counterexample-based quantifier instantiation"
1274 name = "cbqiInnermost"
1275 category = "regular"
1276 long = "cbqi-innermost"
1279 help = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1282 name = "cbqiNestedQE"
1283 category = "regular"
1284 long = "cbqi-nested-qe"
1287 help = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1289 # CEGQI for arithmetic
1292 name = "cbqiUseInfInt"
1293 category = "regular"
1294 long = "cbqi-use-inf-int"
1297 help = "use integer infinity for vts in counterexample-based quantifier instantiation"
1300 name = "cbqiUseInfReal"
1301 category = "regular"
1302 long = "cbqi-use-inf-real"
1305 help = "use real infinity for vts in counterexample-based quantifier instantiation"
1308 name = "cbqiPreRegInst"
1309 category = "regular"
1310 long = "cbqi-prereg-inst"
1313 help = "preregister ground instantiations in counterexample-based quantifier instantiation"
1316 name = "cbqiMinBounds"
1317 category = "regular"
1318 long = "cbqi-min-bounds"
1322 help = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1325 name = "cbqiRoundUpLowerLia"
1326 category = "regular"
1327 long = "cbqi-round-up-lia"
1331 help = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1334 name = "cbqiMidpoint"
1335 category = "regular"
1336 long = "cbqi-midpoint"
1339 help = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1343 category = "regular"
1348 help = "non-optimal bounds for counterexample-based quantifier instantiation"
1351 name = "cbqiLitDepend"
1352 category = "regular"
1353 long = "cbqi-lit-dep"
1357 help = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
1363 category = "regular"
1367 help = "infer whether in effectively propositional fragment, use for cbqi"
1370 name = "quantEprMatching"
1371 category = "regular"
1372 long = "quant-epr-match"
1376 help = "use matching heuristics for EPR instantiation"
1382 category = "regular"
1386 help = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1389 name = "cbqiBvInterleaveValue"
1390 category = "regular"
1391 long = "cbqi-bv-interleave-value"
1394 help = "interleave model value instantiation with word-level inversion approach"
1397 name = "cbqiBvIneqMode"
1398 category = "regular"
1399 long = "cbqi-bv-ineq=MODE"
1400 type = "CVC4::theory::quantifiers::CbqiBvIneqMode"
1401 default = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY"
1402 handler = "stringToCbqiBvIneqMode"
1403 includes = ["options/quantifiers_modes.h"]
1404 help = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1407 name = "cbqiBvRmExtract"
1408 category = "regular"
1409 long = "cbqi-bv-rm-extract"
1412 help = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1415 name = "cbqiBvLinearize"
1416 category = "regular"
1417 long = "cbqi-bv-linear"
1420 help = "linearize adder chains for variables"
1423 name = "cbqiBvConcInv"
1424 category = "regular"
1425 long = "cbqi-bv-concat-inv"
1428 help = "compute inverse for concat over equalities rather than producing an invertibility condition"
1430 ### Local theory extensions options
1433 name = "localTheoryExt"
1434 category = "regular"
1435 long = "local-t-ext"
1439 help = "do instantiation based on local theory extensions"
1442 name = "ltePartialInst"
1443 category = "regular"
1444 long = "lte-partial-inst"
1448 help = "partially instantiate local theory quantifiers"
1451 name = "lteRestrictInstClosure"
1452 category = "regular"
1453 long = "lte-restrict-inst-closure"
1457 help = "treat arguments of inst closure as restricted terms for instantiation"
1459 ### Reduction options
1462 name = "quantAlphaEquiv"
1463 category = "regular"
1464 long = "quant-alpha-equiv"
1468 help = "infer alpha equivalence between quantified formulas"
1471 name = "macrosQuant"
1472 category = "regular"
1473 long = "macros-quant"
1476 help = "perform quantifiers macro expansion"
1479 name = "macrosQuantMode"
1480 category = "regular"
1481 long = "macros-quant-mode=MODE"
1482 type = "CVC4::theory::quantifiers::MacrosQuantMode"
1483 default = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF"
1484 handler = "stringToMacrosQuantMode"
1485 includes = ["options/quantifiers_modes.h"]
1487 help = "mode for quantifiers macro expansion"
1490 name = "quantDynamicSplit"
1491 category = "regular"
1492 long = "quant-dsplit-mode=MODE"
1493 type = "CVC4::theory::quantifiers::QuantDSplitMode"
1494 default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
1495 handler = "stringToQuantDSplitMode"
1496 includes = ["options/quantifiers_modes.h"]
1497 help = "mode for dynamic quantifiers splitting"
1500 name = "quantAntiSkolem"
1501 category = "regular"
1502 long = "quant-anti-skolem"
1505 help = "perform anti-skolemization for quantified formulas"
1507 ### Higher-order options
1511 category = "regular"
1512 long = "ho-matching"
1516 help = "do higher-order matching algorithm for triggers with variable operators"
1519 name = "hoMatchingVarArgPriority"
1520 category = "regular"
1521 long = "ho-matching-var-priority"
1525 help = "give priority to variable arguments over constant arguments"
1528 name = "hoMergeTermDb"
1529 category = "regular"
1530 long = "ho-merge-term-db"
1534 help = "merge term indices modulo equality"
1539 name = "trackInstLemmas"
1540 category = "regular"
1541 long = "track-inst-lemmas"
1544 help = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"