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"
882 long = "sygus-abduct"
886 help = "compute abductions using sygus"
889 name = "ceGuidedInst"
894 help = "counterexample-guided quantifier instantiation for sygus"
897 name = "cegqiSingleInvMode"
899 long = "cegqi-si=MODE"
900 type = "CVC4::theory::quantifiers::CegqiSingleInvMode"
901 default = "CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE"
902 handler = "stringToCegqiSingleInvMode"
903 includes = ["options/quantifiers_modes.h"]
904 help = "mode for processing single invocation synthesis conjectures"
907 name = "cegqiSingleInvPartial"
909 long = "cegqi-si-partial"
913 help = "combined techniques for synthesis conjectures that are partially single invocation"
916 name = "cegqiSingleInvReconstruct"
918 long = "cegqi-si-rcons=MODE"
919 type = "CVC4::theory::quantifiers::CegqiSingleInvRconsMode"
920 default = "CVC4::theory::quantifiers::CEGQI_SI_RCONS_MODE_ALL_LIMIT"
921 handler = "stringToCegqiSingleInvRconsMode"
922 includes = ["options/quantifiers_modes.h"]
923 help = "policy for reconstructing solutions for single invocation conjectures"
926 name = "cegqiSingleInvReconstructLimit"
928 long = "cegqi-si-rcons-limit=N"
932 help = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)"
935 name = "cegqiSingleInvReconstructConst"
937 long = "cegqi-si-reconstruct-const"
941 help = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
944 name = "cegqiSolMinCore"
946 long = "cegqi-si-sol-min-core"
950 help = "minimize solutions for single invocation conjectures based on unsat core"
953 name = "cegqiSolMinInst"
955 long = "cegqi-si-sol-min-inst"
959 help = "minimize individual instantiations for single invocation conjectures based on unsat core"
962 name = "cegqiSingleInvAbort"
964 long = "cegqi-si-abort"
968 help = "abort if synthesis conjecture is not single invocation"
971 name = "sygusConstRepairAbort"
973 long = "sygus-crepair-abort"
977 help = "abort if constant repair techniques are not applicable"
985 help = "Unification-based function synthesis"
988 name = "sygusUnifCondIndependent"
990 long = "sygus-unif-cond-independent"
993 help = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
996 name = "sygusUnifShuffleCond"
998 long = "sygus-unif-shuffle-cond"
1001 help = "Shuffle condition pool when building solutions (may change solutions sizes)"
1004 name = "sygusUnifBooleanHeuristicDt"
1005 category = "regular"
1006 long = "sygus-unif-boolean-heuristic-dt"
1009 help = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
1012 name = "sygusUnifCondIndNoRepeatSol"
1013 category = "regular"
1014 long = "sygus-unif-cond-independent-no-repeat-sol"
1017 help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis"
1020 name = "sygusBoolIteReturnConst"
1021 category = "regular"
1022 long = "sygus-bool-ite-return-const"
1025 help = "Only use Boolean constants for return values in unification-based function synthesis"
1028 name = "sygusQePreproc"
1029 category = "regular"
1030 long = "sygus-qe-preproc"
1034 help = "use quantifier elimination as a preprocessing step for sygus"
1037 name = "sygusRepairConst"
1038 category = "regular"
1039 long = "sygus-repair-const"
1042 help = "use approach to repair constants in sygus candidate solutions"
1045 name = "sygusRepairConstTimeout"
1046 category = "regular"
1047 long = "sygus-repair-const-timeout=N"
1048 type = "unsigned long"
1049 help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
1052 name = "sygusActiveGenMode"
1053 category = "regular"
1054 long = "sygus-active-gen=MODE"
1055 type = "CVC4::theory::quantifiers::SygusActiveGenMode"
1056 default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO"
1057 handler = "stringToSygusActiveGenMode"
1058 includes = ["options/quantifiers_modes.h"]
1060 help = "mode for actively-generated sygus enumerators"
1063 name = "sygusActiveGenEnumConsts"
1064 category = "regular"
1065 long = "sygus-active-gen-cfactor=N"
1066 type = "unsigned long"
1068 help = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum"
1071 name = "sygusMinGrammar"
1072 category = "regular"
1073 long = "sygus-min-grammar"
1077 help = "statically minimize sygus grammars"
1080 name = "sygusAddConstGrammar"
1081 category = "regular"
1082 long = "sygus-add-const-grammar"
1086 help = "statically add constants appearing in conjecture to grammars"
1089 name = "sygusGrammarNorm"
1090 category = "regular"
1091 long = "sygus-grammar-norm"
1095 help = "statically normalize sygus grammars based on flattening (linearization)"
1098 name = "sygusTemplEmbedGrammar"
1099 category = "regular"
1100 long = "sygus-templ-embed-grammar"
1104 help = "embed sygus templates into grammars"
1107 name = "sygusInvTemplMode"
1108 category = "regular"
1109 long = "sygus-inv-templ=MODE"
1110 type = "CVC4::theory::quantifiers::SygusInvTemplMode"
1111 default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST"
1112 handler = "stringToSygusInvTemplMode"
1113 includes = ["options/quantifiers_modes.h"]
1114 help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)"
1117 name = "sygusInvTemplWhenSyntax"
1118 category = "regular"
1119 long = "sygus-inv-templ-when-sg"
1123 help = "use invariant templates (with solution reconstruction) for syntax guided problems"
1126 name = "sygusInvAutoUnfold"
1127 category = "regular"
1128 long = "sygus-auto-unfold"
1132 help = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1135 name = "sygusUnifPbe"
1136 category = "regular"
1140 help = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
1143 name = "sygusPbeMultiFair"
1144 category = "regular"
1145 long = "sygus-pbe-multi-fair"
1148 help = "when using multiple enumerators, ensure that we only register value of minimial term size"
1151 name = "sygusPbeMultiFairDiff"
1152 category = "regular"
1153 long = "sygus-pbe-multi-fair-diff=N"
1156 help = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)"
1159 name = "sygusEvalUnfold"
1160 category = "regular"
1161 long = "sygus-eval-unfold"
1165 help = "do unfolding of sygus evaluation functions"
1168 name = "sygusEvalUnfoldBool"
1169 category = "regular"
1170 long = "sygus-eval-unfold-bool"
1174 help = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1177 name = "sygusRefEval"
1178 category = "regular"
1179 long = "sygus-ref-eval"
1183 help = "direct evaluation of refinement lemmas for conflict analysis"
1186 name = "sygusStream"
1187 category = "regular"
1188 long = "sygus-stream"
1191 help = "enumerate a stream of solutions instead of terminating after the first one"
1194 name = "sygusVerifySubcall"
1195 category = "regular"
1196 long = "sygus-verify-subcall"
1199 help = "use separate copy of the SMT solver for verification lemmas in sygus"
1202 name = "sygusExtRew"
1203 category = "regular"
1204 long = "sygus-ext-rew"
1207 help = "use extended rewriter for sygus"
1210 name = "cegisSample"
1211 category = "regular"
1212 long = "cegis-sample=MODE"
1213 type = "CVC4::theory::quantifiers::CegisSampleMode"
1214 default = "CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE"
1215 handler = "stringToCegisSampleMode"
1216 includes = ["options/quantifiers_modes.h"]
1217 help = "mode for using samples in the counterexample-guided inductive synthesis loop"
1220 name = "minSynthSol"
1221 category = "regular"
1222 long = "min-synth-sol"
1225 help = "Minimize synthesis solutions"
1228 name = "sygusEvalOpt"
1229 category = "regular"
1230 long = "sygus-eval-opt"
1233 help = "use optimized approach for evaluation in sygus"
1236 name = "sygusArgRelevant"
1237 category = "regular"
1238 long = "sygus-arg-relevant"
1241 help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
1243 # Internal uses of sygus
1247 category = "regular"
1252 help = "use sygus to enumerate and verify correctness of rewrite rules"
1255 name = "sygusRewSynth"
1256 category = "regular"
1257 long = "sygus-rr-synth"
1260 help = "use sygus to enumerate candidate rewrite rules"
1263 name = "sygusRewSynthFilterOrder"
1264 category = "regular"
1265 long = "sygus-rr-synth-filter-order"
1268 help = "filter candidate rewrites based on variable ordering"
1271 name = "sygusRewSynthFilterMatch"
1272 category = "regular"
1273 long = "sygus-rr-synth-filter-match"
1276 help = "filter candidate rewrites based on matching"
1279 name = "sygusRewSynthFilterCong"
1280 category = "regular"
1281 long = "sygus-rr-synth-filter-cong"
1284 help = "filter candidate rewrites based on congruence"
1287 name = "sygusRewSynthFilterNonLinear"
1288 category = "regular"
1289 long = "sygus-rr-synth-filter-nl"
1292 help = "filter non-linear candidate rewrites"
1295 name = "sygusRewVerify"
1296 category = "regular"
1297 long = "sygus-rr-verify"
1300 help = "use sygus to verify the correctness of rewrite rules via sampling"
1303 name = "sygusRewVerifyAbort"
1304 category = "regular"
1305 long = "sygus-rr-verify-abort"
1308 help = "abort when sygus-rr-verify finds an instance of unsoundness"
1311 name = "sygusSamples"
1312 category = "regular"
1313 long = "sygus-samples=N"
1316 help = "number of points to consider when doing sygus rewriter sample testing"
1319 name = "sygusSampleGrammar"
1320 category = "regular"
1321 long = "sygus-sample-grammar"
1325 help = "when applicable, use grammar for choosing sample points"
1328 name = "sygusSampleFpUniform"
1329 category = "regular"
1330 long = "sygus-sample-fp-uniform"
1333 help = "sample floating-point values uniformly instead of in a biased fashion"
1336 name = "sygusRewSynthAccel"
1337 category = "regular"
1338 long = "sygus-rr-synth-accel"
1341 help = "add dynamic symmetry breaking clauses based on candidate rewrites"
1344 name = "sygusRewSynthCheck"
1345 category = "regular"
1346 long = "sygus-rr-synth-check"
1349 help = "use satisfiability check to verify correctness of candidate rewrites"
1352 name = "sygusRewSynthInput"
1353 category = "regular"
1354 long = "sygus-rr-synth-input"
1357 help = "synthesize rewrite rules based on the input formula"
1360 name = "sygusRewSynthInputNVars"
1361 category = "regular"
1362 long = "sygus-rr-synth-input-nvars=N"
1365 help = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input"
1368 name = "sygusRewSynthInputUseBool"
1369 category = "regular"
1370 long = "sygus-rr-synth-input-use-bool"
1373 help = "synthesize Boolean rewrite rules based on the input formula"
1376 name = "sygusExprMinerCheckTimeout"
1377 category = "regular"
1378 long = "sygus-expr-miner-check-timeout=N"
1379 type = "unsigned long"
1380 help = "timeout (in milliseconds) for satisfiability checks in expression miners"
1383 name = "sygusRewSynthRec"
1384 category = "regular"
1385 long = "sygus-rr-synth-rec"
1388 help = "synthesize rewrite rules over all sygus grammar types recursively"
1391 name = "sygusQueryGen"
1392 category = "regular"
1393 long = "sygus-query-gen"
1396 help = "use sygus to enumerate interesting satisfiability queries"
1399 name = "sygusQueryGenThresh"
1400 category = "regular"
1401 long = "sygus-query-gen-thresh=N"
1404 help = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen"
1407 name = "sygusQueryGenCheck"
1408 category = "regular"
1409 long = "sygus-query-gen-check"
1412 help = "use interesting satisfiability queries to check soundness of CVC4"
1415 name = "sygusQueryGenDumpFiles"
1416 category = "regular"
1417 long = "sygus-query-gen-dump-files"
1420 help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen"
1423 name = "sygusFilterSolMode"
1424 category = "regular"
1425 long = "sygus-filter-sol=MODE"
1426 type = "CVC4::theory::quantifiers::SygusFilterSolMode"
1427 default = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE"
1428 handler = "stringToSygusFilterSolMode"
1429 includes = ["options/quantifiers_modes.h"]
1430 help = "mode for filtering sygus solutions"
1433 name = "sygusFilterSolRevSubsume"
1435 long = "sygus-filter-sol-rev"
1438 help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
1442 name = "sygusExprMinerCheckUseExport"
1444 long = "sygus-expr-miner-check-use-export"
1447 help = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners"
1449 # CEGQI applied to general quantified formulas
1453 category = "regular"
1457 help = "turns on counterexample-based quantifier instantiation"
1460 name = "cbqiFullEffort"
1461 category = "regular"
1465 help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1469 category = "regular"
1473 help = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1477 category = "regular"
1481 help = "guide instantiations by model values for counterexample-based quantifier instantiation"
1485 category = "regular"
1489 help = "apply counterexample-based instantiation to all quantified formulas"
1492 name = "cbqiMultiInst"
1493 category = "regular"
1494 long = "cbqi-multi-inst"
1497 help = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1500 name = "cbqiRepeatLit"
1501 category = "regular"
1502 long = "cbqi-repeat-lit"
1505 help = "solve literals more than once in counterexample-based quantifier instantiation"
1508 name = "cbqiInnermost"
1509 category = "regular"
1510 long = "cbqi-innermost"
1513 help = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1516 name = "cbqiNestedQE"
1517 category = "regular"
1518 long = "cbqi-nested-qe"
1521 help = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1523 # CEGQI for arithmetic
1526 name = "cbqiUseInfInt"
1527 category = "regular"
1528 long = "cbqi-use-inf-int"
1531 help = "use integer infinity for vts in counterexample-based quantifier instantiation"
1534 name = "cbqiUseInfReal"
1535 category = "regular"
1536 long = "cbqi-use-inf-real"
1539 help = "use real infinity for vts in counterexample-based quantifier instantiation"
1542 name = "cbqiPreRegInst"
1543 category = "regular"
1544 long = "cbqi-prereg-inst"
1547 help = "preregister ground instantiations in counterexample-based quantifier instantiation"
1550 name = "cbqiMinBounds"
1551 category = "regular"
1552 long = "cbqi-min-bounds"
1556 help = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1559 name = "cbqiRoundUpLowerLia"
1560 category = "regular"
1561 long = "cbqi-round-up-lia"
1565 help = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1568 name = "cbqiMidpoint"
1569 category = "regular"
1570 long = "cbqi-midpoint"
1573 help = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1577 category = "regular"
1582 help = "non-optimal bounds for counterexample-based quantifier instantiation"
1585 name = "cbqiLitDepend"
1586 category = "regular"
1587 long = "cbqi-lit-dep"
1591 help = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
1597 category = "regular"
1601 help = "infer whether in effectively propositional fragment, use for cbqi"
1604 name = "quantEprMatching"
1605 category = "regular"
1606 long = "quant-epr-match"
1610 help = "use matching heuristics for EPR instantiation"
1616 category = "regular"
1620 help = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1623 name = "cbqiBvInterleaveValue"
1624 category = "regular"
1625 long = "cbqi-bv-interleave-value"
1628 help = "interleave model value instantiation with word-level inversion approach"
1631 name = "cbqiBvIneqMode"
1632 category = "regular"
1633 long = "cbqi-bv-ineq=MODE"
1634 type = "CVC4::theory::quantifiers::CbqiBvIneqMode"
1635 default = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY"
1636 handler = "stringToCbqiBvIneqMode"
1637 includes = ["options/quantifiers_modes.h"]
1638 help = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1641 name = "cbqiBvRmExtract"
1642 category = "regular"
1643 long = "cbqi-bv-rm-extract"
1646 help = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1649 name = "cbqiBvLinearize"
1650 category = "regular"
1651 long = "cbqi-bv-linear"
1654 help = "linearize adder chains for variables"
1657 name = "cbqiBvSolveNl"
1658 category = "regular"
1659 long = "cbqi-bv-solve-nl"
1662 help = "try to solve non-linear bv literals using model value projections"
1665 name = "cbqiBvConcInv"
1666 category = "regular"
1667 long = "cbqi-bv-concat-inv"
1670 help = "compute inverse for concat over equalities rather than producing an invertibility condition"
1672 ### Local theory extensions options
1675 name = "localTheoryExt"
1676 category = "regular"
1677 long = "local-t-ext"
1681 help = "do instantiation based on local theory extensions"
1684 name = "ltePartialInst"
1685 category = "regular"
1686 long = "lte-partial-inst"
1690 help = "partially instantiate local theory quantifiers"
1693 name = "lteRestrictInstClosure"
1694 category = "regular"
1695 long = "lte-restrict-inst-closure"
1699 help = "treat arguments of inst closure as restricted terms for instantiation"
1701 ### Reduction options
1704 name = "quantAlphaEquiv"
1705 category = "regular"
1706 long = "quant-alpha-equiv"
1710 help = "infer alpha equivalence between quantified formulas"
1713 name = "macrosQuant"
1714 category = "regular"
1715 long = "macros-quant"
1718 help = "perform quantifiers macro expansion"
1721 name = "macrosQuantMode"
1722 category = "regular"
1723 long = "macros-quant-mode=MODE"
1724 type = "CVC4::theory::quantifiers::MacrosQuantMode"
1725 default = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF"
1726 handler = "stringToMacrosQuantMode"
1727 includes = ["options/quantifiers_modes.h"]
1729 help = "mode for quantifiers macro expansion"
1732 name = "quantDynamicSplit"
1733 category = "regular"
1734 long = "quant-dsplit-mode=MODE"
1735 type = "CVC4::theory::quantifiers::QuantDSplitMode"
1736 default = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
1737 handler = "stringToQuantDSplitMode"
1738 includes = ["options/quantifiers_modes.h"]
1739 help = "mode for dynamic quantifiers splitting"
1742 name = "quantAntiSkolem"
1743 category = "regular"
1744 long = "quant-anti-skolem"
1747 help = "perform anti-skolemization for quantified formulas"
1749 ### Higher-order options
1753 category = "regular"
1754 long = "ho-matching"
1758 help = "do higher-order matching algorithm for triggers with variable operators"
1761 name = "hoMatchingVarArgPriority"
1762 category = "regular"
1763 long = "ho-matching-var-priority"
1767 help = "give priority to variable arguments over constant arguments"
1770 name = "hoMergeTermDb"
1771 category = "regular"
1772 long = "ho-merge-term-db"
1776 help = "merge term indices modulo equality"
1781 name = "trackInstLemmas"
1782 category = "regular"
1783 long = "track-inst-lemmas"
1786 help = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"