1id     = "QUANTIFIERS"
2name   = "Quantifiers"
3header = "options/quantifiers_options.h"
4
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 ) )
8[[option]]
9  name       = "miniscopeQuant"
10  category   = "regular"
11  long       = "miniscope-quant"
12  type       = "bool"
13  default    = "true"
14  help       = "miniscope quantifiers"
15
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
19[[option]]
20  name       = "miniscopeQuantFreeVar"
21  category   = "regular"
22  long       = "miniscope-quant-fv"
23  type       = "bool"
24  default    = "true"
25  help       = "miniscope quantifiers for ground subformulas"
26
27[[option]]
28  name       = "quantSplit"
29  category   = "regular"
30  long       = "quant-split"
31  type       = "bool"
32  default    = "true"
33  help       = "apply splitting to quantified formulas based on variable disjoint disjuncts"
34
35[[option]]
36  name       = "prenexQuant"
37  category   = "regular"
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"
44
45[[option]]
46  name       = "prenexQuantUser"
47  category   = "regular"
48  long       = "prenex-quant-user"
49  type       = "bool"
50  default    = "false"
51  help       = "prenex quantified formulas with user patterns"
52
53# Whether to variable-eliminate quantifiers.
54# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
55#   forall y. P( c, y )
56[[option]]
57  name       = "varElimQuant"
58  category   = "regular"
59  long       = "var-elim-quant"
60  type       = "bool"
61  default    = "true"
62  read_only  = true
63  help       = "enable simple variable elimination for quantified formulas"
64
65[[option]]
66  name       = "varIneqElimQuant"
67  category   = "regular"
68  long       = "var-ineq-elim-quant"
69  type       = "bool"
70  default    = "true"
71  read_only  = true
72  help       = "enable variable elimination based on infinite projection of unbound arithmetic variables"
73
74[[option]]
75  name       = "dtVarExpandQuant"
76  category   = "regular"
77  long       = "dt-var-exp-quant"
78  type       = "bool"
79  default    = "true"
80  read_only  = true
81  help       = "expand datatype variables bound to one constructor in quantifiers"
82
83[[option]]
84  name       = "iteLiftQuant"
85  category   = "regular"
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"
92
93[[option]]
94  name       = "condVarSplitQuant"
95  category   = "regular"
96  long       = "cond-var-split-quant"
97  type       = "bool"
98  default    = "true"
99  read_only  = true
100  help       = "split quantified formulas that lead to variable eliminations"
101
102[[option]]
103  name       = "condVarSplitQuantAgg"
104  category   = "regular"
105  long       = "cond-var-split-agg-quant"
106  type       = "bool"
107  default    = "false"
108  read_only  = true
109  help       = "aggressive split quantified formulas that lead to variable eliminations"
110
111[[option]]
112  name       = "iteDtTesterSplitQuant"
113  category   = "regular"
114  long       = "ite-dtt-split-quant"
115  type       = "bool"
116  default    = "false"
117  help       = "split ites with dt testers as conditions"
118
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
122[[option]]
123  name       = "preSkolemQuant"
124  category   = "regular"
125  long       = "pre-skolem-quant"
126  type       = "bool"
127  default    = "false"
128  help       = "apply skolemization eagerly to bodies of quantified formulas"
129
130[[option]]
131  name       = "preSkolemQuantNested"
132  category   = "regular"
133  long       = "pre-skolem-quant-nested"
134  type       = "bool"
135  default    = "true"
136  help       = "apply skolemization to nested quantified formulas"
137
138[[option]]
139  name       = "preSkolemQuantAgg"
140  category   = "regular"
141  long       = "pre-skolem-quant-agg"
142  type       = "bool"
143  default    = "true"
144  help       = "apply skolemization to quantified formulas aggressively"
145
146[[option]]
147  name       = "aggressiveMiniscopeQuant"
148  category   = "regular"
149  long       = "ag-miniscope-quant"
150  type       = "bool"
151  default    = "false"
152  read_only  = true
153  help       = "perform aggressive miniscoping for quantifiers"
154
155[[option]]
156  name       = "elimTautQuant"
157  category   = "regular"
158  long       = "elim-taut-quant"
159  type       = "bool"
160  default    = "true"
161  read_only  = true
162  help       = "eliminate tautological disjuncts of quantified formulas"
163
164[[option]]
165  name       = "elimExtArithQuant"
166  category   = "regular"
167  long       = "elim-ext-arith-quant"
168  type       = "bool"
169  default    = "true"
170  help       = "eliminate extended arithmetic symbols in quantified formulas"
171
172[[option]]
173  name       = "condRewriteQuant"
174  category   = "regular"
175  long       = "cond-rewrite-quant"
176  type       = "bool"
177  default    = "true"
178  read_only  = true
179  help       = "conditional rewriting of quantified formulas"
180
181[[option]]
182  name       = "globalNegate"
183  category   = "regular"
184  long       = "global-negate"
185  type       = "bool"
186  default    = "false"
187  help       = "do global negation of input formula"
188
189#### E-matching options
190
191[[option]]
192  name       = "eMatching"
193  category   = "regular"
194  long       = "e-matching"
195  type       = "bool"
196  default    = "true"
197  help       = "whether to do heuristic E-matching"
198
199[[option]]
200  name       = "termDbMode"
201  category   = "regular"
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"
208
209[[option]]
210  name       = "registerQuantBodyTerms"
211  category   = "regular"
212  long       = "register-quant-body-terms"
213  type       = "bool"
214  default    = "false"
215  read_only  = true
216  help       = "consider ground terms within bodies of quantified formulas for matching"
217
218[[option]]
219  name       = "inferArithTriggerEq"
220  category   = "regular"
221  long       = "infer-arith-trigger-eq"
222  type       = "bool"
223  default    = "false"
224  read_only  = true
225  help       = "infer equalities for trigger terms based on solving arithmetic equalities"
226
227[[option]]
228  name       = "strictTriggers"
229  category   = "regular"
230  long       = "strict-triggers"
231  type       = "bool"
232  default    = "false"
233  read_only  = true
234  help       = "only instantiate quantifiers with user patterns based on triggers"
235
236[[option]]
237  name       = "relevantTriggers"
238  category   = "regular"
239  long       = "relevant-triggers"
240  type       = "bool"
241  default    = "false"
242  read_only  = true
243  help       = "prefer triggers that are more relevant based on SInE style analysis"
244
245[[option]]
246  name       = "relationalTriggers"
247  category   = "regular"
248  long       = "relational-triggers"
249  type       = "bool"
250  default    = "false"
251  read_only  = true
252  help       = "choose relational triggers such as x = f(y), x >= f(y)"
253
254[[option]]
255  name       = "purifyTriggers"
256  category   = "regular"
257  long       = "purify-triggers"
258  type       = "bool"
259  default    = "false"
260  help       = "purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1"
261
262[[option]]
263  name       = "purifyDtTriggers"
264  category   = "regular"
265  long       = "purify-dt-triggers"
266  type       = "bool"
267  default    = "false"
268  help       = "purify dt triggers, match all constructors of correct form instead of selectors"
269
270[[option]]
271  name       = "pureThTriggers"
272  category   = "regular"
273  long       = "pure-th-triggers"
274  type       = "bool"
275  default    = "false"
276  help       = "use pure theory terms as single triggers"
277
278[[option]]
279  name       = "partialTriggers"
280  category   = "regular"
281  long       = "partial-triggers"
282  type       = "bool"
283  default    = "false"
284  help       = "use triggers that do not contain all free variables"
285
286[[option]]
287  name       = "multiTriggerWhenSingle"
288  category   = "regular"
289  long       = "multi-trigger-when-single"
290  type       = "bool"
291  default    = "false"
292  read_only  = true
293  help       = "select multi triggers when single triggers exist"
294
295[[option]]
296  name       = "multiTriggerPriority"
297  category   = "regular"
298  long       = "multi-trigger-priority"
299  type       = "bool"
300  default    = "false"
301  read_only  = true
302  help       = "only try multi triggers if single triggers give no instantiations"
303
304[[option]]
305  name       = "multiTriggerCache"
306  category   = "regular"
307  long       = "multi-trigger-cache"
308  type       = "bool"
309  default    = "false"
310  read_only  = true
311  help       = "caching version of multi triggers"
312
313[[option]]
314  name       = "multiTriggerLinear"
315  category   = "regular"
316  long       = "multi-trigger-linear"
317  type       = "bool"
318  default    = "true"
319  read_only  = true
320  help       = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms"
321
322[[option]]
323  name       = "triggerSelMode"
324  category   = "regular"
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"
331
332[[option]]
333  name       = "triggerActiveSelMode"
334  category   = "regular"
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"
341
342[[option]]
343  name       = "userPatternsQuant"
344  category   = "regular"
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"
351
352[[option]]
353  name       = "incrementTriggers"
354  category   = "regular"
355  long       = "increment-triggers"
356  type       = "bool"
357  default    = "true"
358  read_only  = true
359  help       = "generate additional triggers as needed during search"
360
361[[option]]
362  name       = "instWhenMode"
363  category   = "regular"
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"
371
372[[option]]
373  name       = "instWhenStrictInterleave"
374  category   = "regular"
375  long       = "inst-when-strict-interleave"
376  type       = "bool"
377  default    = "true"
378  help       = "ensure theory combination and standard quantifier effort strategies take turns"
379
380[[option]]
381  name       = "instWhenPhase"
382  category   = "regular"
383  long       = "inst-when-phase=N"
384  type       = "int"
385  default    = "2"
386  help       = "instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen"
387
388[[option]]
389  name       = "instWhenTcFirst"
390  category   = "regular"
391  long       = "inst-when-tc-first"
392  type       = "bool"
393  default    = "true"
394  help       = "allow theory combination to happen once initially, before quantifier strategies are run"
395
396[[option]]
397  name       = "quantModelEe"
398  category   = "regular"
399  long       = "quant-model-ee"
400  type       = "bool"
401  default    = "false"
402  read_only  = true
403  help       = "use equality engine of model for last call effort"
404
405[[option]]
406  name       = "instMaxLevel"
407  category   = "regular"
408  long       = "inst-max-level=N"
409  type       = "int"
410  default    = "-1"
411  help       = "maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)"
412
413[[option]]
414  name       = "instLevelInputOnly"
415  category   = "regular"
416  long       = "inst-level-input-only"
417  type       = "bool"
418  default    = "true"
419  read_only  = true
420  help       = "only input terms are assigned instantiation level zero"
421
422[[option]]
423  name       = "quantRepMode"
424  category   = "regular"
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"
431
432[[option]]
433  name       = "fullSaturateQuant"
434  category   = "regular"
435  long       = "full-saturate-quant"
436  type       = "bool"
437  default    = "false"
438  help       = "when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown"
439
440[[option]]
441  name       = "fullSaturateQuantRd"
442  category   = "regular"
443  long       = "full-saturate-quant-rd"
444  type       = "bool"
445  default    = "true"
446  read_only  = true
447  help       = "whether to use relevant domain first for full saturation instantiation strategy"
448
449[[option]]
450  name       = "fullSaturateInterleave"
451  category   = "regular"
452  long       = "fs-interleave"
453  type       = "bool"
454  default    = "false"
455  read_only  = true
456  help       = "interleave full saturate instantiation with other techniques"
457
458[[option]]
459  name       = "literalMatchMode"
460  category   = "regular"
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"]
467  read_only  = true
468  help       = "choose literal matching mode"
469
470### Finite model finding options
471
472[[option]]
473  name       = "finiteModelFind"
474  category   = "regular"
475  long       = "finite-model-find"
476  type       = "bool"
477  default    = "false"
478  help       = "use finite model finding heuristic for quantifier instantiation"
479
480[[option]]
481  name       = "quantFunWellDefined"
482  category   = "regular"
483  long       = "quant-fun-wd"
484  type       = "bool"
485  default    = "false"
486  read_only  = true
487  help       = "assume that function defined by quantifiers are well defined"
488
489[[option]]
490  name       = "fmfFunWellDefined"
491  category   = "regular"
492  long       = "fmf-fun"
493  type       = "bool"
494  default    = "false"
495  help       = "find models for recursively defined functions, assumes functions are admissible"
496
497[[option]]
498  name       = "fmfFunWellDefinedRelevant"
499  category   = "regular"
500  long       = "fmf-fun-rlv"
501  type       = "bool"
502  default    = "false"
503  read_only  = true
504  help       = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant"
505
506[[option]]
507  name       = "fmfEmptySorts"
508  category   = "regular"
509  long       = "fmf-empty-sorts"
510  type       = "bool"
511  default    = "false"
512  read_only  = true
513  help       = "allow finite model finding to assume sorts that do not occur in ground assertions are empty"
514
515[[option]]
516  name       = "mbqiMode"
517  category   = "regular"
518  long       = "mbqi=MODE"
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"
525
526[[option]]
527  name       = "fmfOneInstPerRound"
528  category   = "regular"
529  long       = "mbqi-one-inst-per-round"
530  type       = "bool"
531  default    = "false"
532  help       = "only add one instantiation per quantifier per round for mbqi"
533
534[[option]]
535  name       = "fmfOneQuantPerRound"
536  category   = "regular"
537  long       = "mbqi-one-quant-per-round"
538  type       = "bool"
539  default    = "false"
540  read_only  = true
541  help       = "only add instantiations for one quantifier per round for mbqi"
542
543[[option]]
544  name       = "mbqiInterleave"
545  category   = "regular"
546  long       = "mbqi-interleave"
547  type       = "bool"
548  default    = "false"
549  read_only  = true
550  help       = "interleave model-based quantifier instantiation with other techniques"
551
552[[option]]
553  name       = "fmfInstEngine"
554  category   = "regular"
555  long       = "fmf-inst-engine"
556  type       = "bool"
557  default    = "false"
558  help       = "use instantiation engine in conjunction with finite model finding"
559
560[[option]]
561  name       = "fmfInstGen"
562  category   = "regular"
563  long       = "fmf-inst-gen"
564  type       = "bool"
565  default    = "true"
566  read_only  = true
567  help       = "enable Inst-Gen instantiation techniques for finite model finding"
568
569[[option]]
570  name       = "fmfInstGenOneQuantPerRound"
571  category   = "regular"
572  long       = "fmf-inst-gen-one-quant-per-round"
573  type       = "bool"
574  default    = "false"
575  read_only  = true
576  help       = "only perform Inst-Gen instantiation techniques on one quantifier per round"
577
578[[option]]
579  name       = "fmfFreshDistConst"
580  category   = "regular"
581  long       = "fmf-fresh-dc"
582  type       = "bool"
583  default    = "false"
584  read_only  = true
585  help       = "use fresh distinguished representative when applying Inst-Gen techniques"
586
587[[option]]
588  name       = "fmfFmcSimple"
589  category   = "regular"
590  long       = "fmf-fmc-simple"
591  type       = "bool"
592  default    = "true"
593  read_only  = true
594  help       = "simple models in full model check for finite model finding"
595
596[[option]]
597  name       = "fmfBoundInt"
598  category   = "regular"
599  long       = "fmf-bound-int"
600  type       = "bool"
601  default    = "false"
602  help       = "finite model finding on bounded integer quantification"
603
604[[option]]
605  name       = "fmfBound"
606  category   = "regular"
607  long       = "fmf-bound"
608  type       = "bool"
609  default    = "false"
610  help       = "finite model finding on bounded quantification"
611
612[[option]]
613  name       = "fmfBoundLazy"
614  category   = "regular"
615  long       = "fmf-bound-lazy"
616  type       = "bool"
617  default    = "false"
618  help       = "enforce bounds for bounded quantification lazily via use of proxy variables"
619
620[[option]]
621  name       = "fmfTypeCompletionThresh"
622  category   = "regular"
623  long       = "fmf-type-completion-thresh=N"
624  type       = "int"
625  default    = "1000"
626  read_only  = true
627  help       = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
628
629[[option]]
630  name       = "quantConflictFind"
631  category   = "regular"
632  long       = "quant-cf"
633  type       = "bool"
634  default    = "true"
635  help       = "enable conflict find mechanism for quantifiers"
636
637[[option]]
638  name       = "qcfMode"
639  category   = "regular"
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"]
645  read_only  = true
646  help       = "what effort to apply conflict find mechanism"
647
648[[option]]
649  name       = "qcfWhenMode"
650  category   = "regular"
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"]
656  read_only  = true
657  help       = "when to invoke conflict find mechanism for quantifiers"
658
659[[option]]
660  name       = "qcfTConstraint"
661  category   = "regular"
662  long       = "qcf-tconstraint"
663  type       = "bool"
664  default    = "false"
665  help       = "enable entailment checks for t-constraints in qcf algorithm"
666
667[[option]]
668  name       = "qcfAllConflict"
669  category   = "regular"
670  long       = "qcf-all-conflict"
671  type       = "bool"
672  default    = "false"
673  help       = "add all available conflicting instances during conflict-based instantiation"
674
675[[option]]
676  name       = "qcfNestedConflict"
677  category   = "regular"
678  long       = "qcf-nested-conflict"
679  type       = "bool"
680  default    = "false"
681  read_only  = true
682  help       = "consider conflicts for nested quantifiers"
683
684[[option]]
685  name       = "qcfVoExp"
686  category   = "regular"
687  long       = "qcf-vo-exp"
688  type       = "bool"
689  default    = "false"
690  read_only  = true
691  help       = "qcf experimental variable ordering"
692
693[[option]]
694  name       = "instNoEntail"
695  category   = "regular"
696  long       = "inst-no-entail"
697  type       = "bool"
698  default    = "true"
699  help       = "do not consider instances of quantified formulas that are currently entailed"
700
701[[option]]
702  name       = "instNoModelTrue"
703  category   = "regular"
704  long       = "inst-no-model-true"
705  type       = "bool"
706  default    = "false"
707  help       = "do not consider instances of quantified formulas that are currently true in model, if it is available"
708
709[[option]]
710  name       = "instPropagate"
711  category   = "regular"
712  long       = "inst-prop"
713  type       = "bool"
714  default    = "false"
715  help       = "internal propagation for instantiations for selecting relevant instances"
716
717[[option]]
718  name       = "qcfEagerTest"
719  category   = "regular"
720  long       = "qcf-eager-test"
721  type       = "bool"
722  default    = "true"
723  read_only  = true
724  help       = "optimization, test qcf instances eagerly"
725
726[[option]]
727  name       = "qcfEagerCheckRd"
728  category   = "regular"
729  long       = "qcf-eager-check-rd"
730  type       = "bool"
731  default    = "true"
732  read_only  = true
733  help       = "optimization, eagerly check relevant domain of matched position"
734
735[[option]]
736  name       = "qcfSkipRd"
737  category   = "regular"
738  long       = "qcf-skip-rd"
739  type       = "bool"
740  default    = "false"
741  read_only  = true
742  help       = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
743
744### Rewrite rules options
745
746[[option]]
747  name       = "quantRewriteRules"
748  category   = "regular"
749  long       = "rewrite-rules"
750  type       = "bool"
751  default    = "false"
752  read_only  = true
753  help       = "use rewrite rules module"
754
755[[option]]
756  name       = "rrOneInstPerRound"
757  category   = "regular"
758  long       = "rr-one-inst-per-round"
759  type       = "bool"
760  default    = "false"
761  read_only  = true
762  help       = "add one instance of rewrite rule per round"
763
764### Induction options
765
766[[option]]
767  name       = "quantInduction"
768  category   = "regular"
769  long       = "quant-ind"
770  type       = "bool"
771  default    = "false"
772  read_only  = true
773  help       = "use all available techniques for inductive reasoning"
774
775[[option]]
776  name       = "dtStcInduction"
777  category   = "regular"
778  long       = "dt-stc-ind"
779  type       = "bool"
780  default    = "false"
781  help       = "apply strengthening for existential quantification over datatypes based on structural induction"
782
783[[option]]
784  name       = "intWfInduction"
785  category   = "regular"
786  long       = "int-wf-ind"
787  type       = "bool"
788  default    = "false"
789  help       = "apply strengthening for integers based on well-founded induction"
790
791[[option]]
792  name       = "conjectureGen"
793  category   = "regular"
794  long       = "conjecture-gen"
795  type       = "bool"
796  default    = "false"
797  help       = "generate candidate conjectures for inductive proofs"
798
799[[option]]
800  name       = "conjectureGenPerRound"
801  category   = "regular"
802  long       = "conjecture-gen-per-round=N"
803  type       = "int"
804  default    = "1"
805  read_only  = true
806  help       = "number of conjectures to generate per instantiation round"
807
808[[option]]
809  name       = "conjectureNoFilter"
810  category   = "regular"
811  long       = "conjecture-no-filter"
812  type       = "bool"
813  default    = "false"
814  read_only  = true
815  help       = "do not filter conjectures"
816
817[[option]]
818  name       = "conjectureFilterActiveTerms"
819  category   = "regular"
820  long       = "conjecture-filter-active-terms"
821  type       = "bool"
822  default    = "true"
823  help       = "filter based on active terms"
824
825[[option]]
826  name       = "conjectureFilterCanonical"
827  category   = "regular"
828  long       = "conjecture-filter-canonical"
829  type       = "bool"
830  default    = "true"
831  help       = "filter based on canonicity"
832
833[[option]]
834  name       = "conjectureFilterModel"
835  category   = "regular"
836  long       = "conjecture-filter-model"
837  type       = "bool"
838  default    = "true"
839  help       = "filter based on model"
840
841[[option]]
842  name       = "conjectureGenGtEnum"
843  category   = "regular"
844  long       = "conjecture-gen-gt-enum=N"
845  type       = "int"
846  default    = "50"
847  read_only  = true
848  help       = "number of ground terms to generate for model filtering"
849
850[[option]]
851  name       = "conjectureUeeIntro"
852  category   = "regular"
853  long       = "conjecture-gen-uee-intro"
854  type       = "bool"
855  default    = "false"
856  read_only  = true
857  help       = "more aggressive merging for universal equality engine, introduces terms"
858
859[[option]]
860  name       = "conjectureGenMaxDepth"
861  category   = "regular"
862  long       = "conjecture-gen-max-depth=N"
863  type       = "int"
864  default    = "3"
865  read_only  = true
866  help       = "maximum depth of terms to consider for conjectures"
867
868### Synthesis options
869
870[[option]]
871  name       = "sygusInference"
872  category   = "regular"
873  long       = "sygus-inference"
874  type       = "bool"
875  default    = "false"
876  read_only  = false
877  help       = "attempt to preprocess arbitrary inputs to sygus conjectures"
878
879[[option]]
880  name       = "sygusAbduct"
881  category   = "regular"
882  long       = "sygus-abduct"
883  type       = "bool"
884  default    = "false"
885  read_only  = false
886  help       = "compute abductions using sygus"
887
888[[option]]
889  name       = "ceGuidedInst"
890  category   = "regular"
891  long       = "cegqi"
892  type       = "bool"
893  default    = "false"
894  help       = "counterexample-guided quantifier instantiation for sygus"
895
896[[option]]
897  name       = "cegqiSingleInvMode"
898  category   = "regular"
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"
905
906[[option]]
907  name       = "cegqiSingleInvPartial"
908  category   = "regular"
909  long       = "cegqi-si-partial"
910  type       = "bool"
911  default    = "false"
912  read_only  = true
913  help       = "combined techniques for synthesis conjectures that are partially single invocation"
914
915[[option]]
916  name       = "cegqiSingleInvReconstruct"
917  category   = "regular"
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"
924
925[[option]]
926  name       = "cegqiSingleInvReconstructLimit"
927  category   = "regular"
928  long       = "cegqi-si-rcons-limit=N"
929  type       = "int"
930  default    = "10000"
931  read_only  = true
932  help       = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)"
933
934[[option]]
935  name       = "cegqiSingleInvReconstructConst"
936  category   = "regular"
937  long       = "cegqi-si-reconstruct-const"
938  type       = "bool"
939  default    = "true"
940  read_only  = true
941  help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
942
943[[option]]
944  name       = "cegqiSolMinCore"
945  category   = "regular"
946  long       = "cegqi-si-sol-min-core"
947  type       = "bool"
948  default    = "false"
949  read_only  = true
950  help       = "minimize solutions for single invocation conjectures based on unsat core"
951
952[[option]]
953  name       = "cegqiSolMinInst"
954  category   = "regular"
955  long       = "cegqi-si-sol-min-inst"
956  type       = "bool"
957  default    = "true"
958  read_only  = true
959  help       = "minimize individual instantiations for single invocation conjectures based on unsat core"
960
961[[option]]
962  name       = "cegqiSingleInvAbort"
963  category   = "regular"
964  long       = "cegqi-si-abort"
965  type       = "bool"
966  default    = "false"
967  read_only  = true
968  help       = "abort if synthesis conjecture is not single invocation"
969
970[[option]]
971  name       = "sygusConstRepairAbort"
972  category   = "regular"
973  long       = "sygus-crepair-abort"
974  type       = "bool"
975  default    = "false"
976  read_only  = true
977  help       = "abort if constant repair techniques are not applicable"
978
979[[option]]
980  name       = "sygusUnif"
981  category   = "regular"
982  long       = "sygus-unif"
983  type       = "bool"
984  default    = "false"
985  help       = "Unification-based function synthesis"
986
987[[option]]
988  name       = "sygusUnifCondIndependent"
989  category   = "regular"
990  long       = "sygus-unif-cond-independent"
991  type       = "bool"
992  default    = "false"
993  help       = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
994
995[[option]]
996  name       = "sygusUnifShuffleCond"
997  category   = "regular"
998  long       = "sygus-unif-shuffle-cond"
999  type       = "bool"
1000  default    = "false"
1001  help       = "Shuffle condition pool when building solutions (may change solutions sizes)"
1002
1003[[option]]
1004  name       = "sygusUnifBooleanHeuristicDt"
1005  category   = "regular"
1006  long       = "sygus-unif-boolean-heuristic-dt"
1007  type       = "bool"
1008  default    = "false"
1009  help       = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
1010
1011[[option]]
1012  name       = "sygusUnifCondIndNoRepeatSol"
1013  category   = "regular"
1014  long       = "sygus-unif-cond-independent-no-repeat-sol"
1015  type       = "bool"
1016  default    = "true"
1017  help       = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis"
1018
1019[[option]]
1020  name       = "sygusBoolIteReturnConst"
1021  category   = "regular"
1022  long       = "sygus-bool-ite-return-const"
1023  type       = "bool"
1024  default    = "true"
1025  help       = "Only use Boolean constants for return values in unification-based function synthesis"
1026
1027[[option]]
1028  name       = "sygusQePreproc"
1029  category   = "regular"
1030  long       = "sygus-qe-preproc"
1031  type       = "bool"
1032  default    = "false"
1033  read_only  = true
1034  help       = "use quantifier elimination as a preprocessing step for sygus"
1035
1036[[option]]
1037  name       = "sygusRepairConst"
1038  category   = "regular"
1039  long       = "sygus-repair-const"
1040  type       = "bool"
1041  default    = "false"
1042  help       = "use approach to repair constants in sygus candidate solutions"
1043
1044[[option]]
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"
1050
1051[[option]]
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"]
1059  read_only  = true
1060  help       = "mode for actively-generated sygus enumerators"
1061
1062[[option]]
1063  name       = "sygusActiveGenEnumConsts"
1064  category   = "regular"
1065  long       = "sygus-active-gen-cfactor=N"
1066  type       = "unsigned long"
1067  default    = "5"
1068  help       = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum"
1069
1070[[option]]
1071  name       = "sygusMinGrammar"
1072  category   = "regular"
1073  long       = "sygus-min-grammar"
1074  type       = "bool"
1075  default    = "true"
1076  read_only  = true
1077  help       = "statically minimize sygus grammars"
1078
1079[[option]]
1080  name       = "sygusAddConstGrammar"
1081  category   = "regular"
1082  long       = "sygus-add-const-grammar"
1083  type       = "bool"
1084  default    = "false"
1085  read_only  = true
1086  help       = "statically add constants appearing in conjecture to grammars"
1087
1088[[option]]
1089  name       = "sygusGrammarNorm"
1090  category   = "regular"
1091  long       = "sygus-grammar-norm"
1092  type       = "bool"
1093  default    = "false"
1094  read_only  = true
1095  help       = "statically normalize sygus grammars based on flattening (linearization)"
1096
1097[[option]]
1098  name       = "sygusTemplEmbedGrammar"
1099  category   = "regular"
1100  long       = "sygus-templ-embed-grammar"
1101  type       = "bool"
1102  default    = "false"
1103  read_only  = true
1104  help       = "embed sygus templates into grammars"
1105
1106[[option]]
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)"
1115
1116[[option]]
1117  name       = "sygusInvTemplWhenSyntax"
1118  category   = "regular"
1119  long       = "sygus-inv-templ-when-sg"
1120  type       = "bool"
1121  default    = "false"
1122  read_only  = false
1123  help       = "use invariant templates (with solution reconstruction) for syntax guided problems"
1124
1125[[option]]
1126  name       = "sygusInvAutoUnfold"
1127  category   = "regular"
1128  long       = "sygus-auto-unfold"
1129  type       = "bool"
1130  default    = "true"
1131  read_only  = true
1132  help       = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
1133
1134[[option]]
1135  name       = "sygusUnifPbe"
1136  category   = "regular"
1137  long       = "sygus-pbe"
1138  type       = "bool"
1139  default    = "true"
1140  help       = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
1141
1142[[option]]
1143  name       = "sygusPbeMultiFair"
1144  category   = "regular"
1145  long       = "sygus-pbe-multi-fair"
1146  type       = "bool"
1147  default    = "false"
1148  help       = "when using multiple enumerators, ensure that we only register value of minimial term size"
1149
1150[[option]]
1151  name       = "sygusPbeMultiFairDiff"
1152  category   = "regular"
1153  long       = "sygus-pbe-multi-fair-diff=N"
1154  type       = "int"
1155  default    = "0"
1156  help       = "when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)"
1157
1158[[option]]
1159  name       = "sygusEvalUnfold"
1160  category   = "regular"
1161  long       = "sygus-eval-unfold"
1162  type       = "bool"
1163  default    = "true"
1164  read_only  = true
1165  help       = "do unfolding of sygus evaluation functions"
1166
1167[[option]]
1168  name       = "sygusEvalUnfoldBool"
1169  category   = "regular"
1170  long       = "sygus-eval-unfold-bool"
1171  type       = "bool"
1172  default    = "true"
1173  read_only  = true
1174  help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
1175
1176[[option]]
1177  name       = "sygusRefEval"
1178  category   = "regular"
1179  long       = "sygus-ref-eval"
1180  type       = "bool"
1181  default    = "true"
1182  read_only  = true
1183  help       = "direct evaluation of refinement lemmas for conflict analysis"
1184
1185[[option]]
1186  name       = "sygusStream"
1187  category   = "regular"
1188  long       = "sygus-stream"
1189  type       = "bool"
1190  default    = "false"
1191  help       = "enumerate a stream of solutions instead of terminating after the first one"
1192
1193[[option]]
1194  name       = "sygusVerifySubcall"
1195  category   = "regular"
1196  long       = "sygus-verify-subcall"
1197  type       = "bool"
1198  default    = "true"
1199  help       = "use separate copy of the SMT solver for verification lemmas in sygus"
1200
1201[[option]]
1202  name       = "sygusExtRew"
1203  category   = "regular"
1204  long       = "sygus-ext-rew"
1205  type       = "bool"
1206  default    = "true"
1207  help       = "use extended rewriter for sygus"
1208
1209[[option]]
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"
1218
1219[[option]]
1220  name       = "minSynthSol"
1221  category   = "regular"
1222  long       = "min-synth-sol"
1223  type       = "bool"
1224  default    = "true"
1225  help       = "Minimize synthesis solutions"
1226
1227[[option]]
1228  name       = "sygusEvalOpt"
1229  category   = "regular"
1230  long       = "sygus-eval-opt"
1231  type       = "bool"
1232  default    = "true"
1233  help       = "use optimized approach for evaluation in sygus"
1234
1235[[option]]
1236  name       = "sygusArgRelevant"
1237  category   = "regular"
1238  long       = "sygus-arg-relevant"
1239  type       = "bool"
1240  default    = "false"
1241  help       = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
1242
1243# Internal uses of sygus
1244
1245[[option]]
1246  name       = "sygusRew"
1247  category   = "regular"
1248  long       = "sygus-rr"
1249  type       = "bool"
1250  default    = "false"
1251  read_only  = true
1252  help       = "use sygus to enumerate and verify correctness of rewrite rules"
1253
1254[[option]]
1255  name       = "sygusRewSynth"
1256  category   = "regular"
1257  long       = "sygus-rr-synth"
1258  type       = "bool"
1259  default    = "false"
1260  help       = "use sygus to enumerate candidate rewrite rules"
1261
1262[[option]]
1263  name       = "sygusRewSynthFilterOrder"
1264  category   = "regular"
1265  long       = "sygus-rr-synth-filter-order"
1266  type       = "bool"
1267  default    = "true"
1268  help       = "filter candidate rewrites based on variable ordering"
1269
1270[[option]]
1271  name       = "sygusRewSynthFilterMatch"
1272  category   = "regular"
1273  long       = "sygus-rr-synth-filter-match"
1274  type       = "bool"
1275  default    = "true"
1276  help       = "filter candidate rewrites based on matching"
1277
1278[[option]]
1279  name       = "sygusRewSynthFilterCong"
1280  category   = "regular"
1281  long       = "sygus-rr-synth-filter-cong"
1282  type       = "bool"
1283  default    = "true"
1284  help       = "filter candidate rewrites based on congruence"
1285
1286[[option]]
1287  name       = "sygusRewSynthFilterNonLinear"
1288  category   = "regular"
1289  long       = "sygus-rr-synth-filter-nl"
1290  type       = "bool"
1291  default    = "false"
1292  help       = "filter non-linear candidate rewrites"
1293
1294[[option]]
1295  name       = "sygusRewVerify"
1296  category   = "regular"
1297  long       = "sygus-rr-verify"
1298  type       = "bool"
1299  default    = "false"
1300  help       = "use sygus to verify the correctness of rewrite rules via sampling"
1301
1302[[option]]
1303  name       = "sygusRewVerifyAbort"
1304  category   = "regular"
1305  long       = "sygus-rr-verify-abort"
1306  type       = "bool"
1307  default    = "true"
1308  help       = "abort when sygus-rr-verify finds an instance of unsoundness"
1309
1310[[option]]
1311  name       = "sygusSamples"
1312  category   = "regular"
1313  long       = "sygus-samples=N"
1314  type       = "int"
1315  default    = "1000"
1316  help       = "number of points to consider when doing sygus rewriter sample testing"
1317
1318[[option]]
1319  name       = "sygusSampleGrammar"
1320  category   = "regular"
1321  long       = "sygus-sample-grammar"
1322  type       = "bool"
1323  default    = "true"
1324  read_only  = true
1325  help       = "when applicable, use grammar for choosing sample points"
1326
1327[[option]]
1328  name       = "sygusSampleFpUniform"
1329  category   = "regular"
1330  long       = "sygus-sample-fp-uniform"
1331  type       = "bool"
1332  default    = "false"
1333  help       = "sample floating-point values uniformly instead of in a biased fashion"
1334
1335[[option]]
1336  name       = "sygusRewSynthAccel"
1337  category   = "regular"
1338  long       = "sygus-rr-synth-accel"
1339  type       = "bool"
1340  default    = "false"
1341  help       = "add dynamic symmetry breaking clauses based on candidate rewrites"
1342
1343[[option]]
1344  name       = "sygusRewSynthCheck"
1345  category   = "regular"
1346  long       = "sygus-rr-synth-check"
1347  type       = "bool"
1348  default    = "false"
1349  help       = "use satisfiability check to verify correctness of candidate rewrites"
1350
1351[[option]]
1352  name       = "sygusRewSynthInput"
1353  category   = "regular"
1354  long       = "sygus-rr-synth-input"
1355  type       = "bool"
1356  default    = "false"
1357  help       = "synthesize rewrite rules based on the input formula"
1358
1359[[option]]
1360  name       = "sygusRewSynthInputNVars"
1361  category   = "regular"
1362  long       = "sygus-rr-synth-input-nvars=N"
1363  type       = "int"
1364  default    = "3"
1365  help       = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input"
1366
1367[[option]]
1368  name       = "sygusRewSynthInputUseBool"
1369  category   = "regular"
1370  long       = "sygus-rr-synth-input-use-bool"
1371  type       = "bool"
1372  default    = "false"
1373  help       = "synthesize Boolean rewrite rules based on the input formula"
1374
1375[[option]]
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"
1381
1382[[option]]
1383  name       = "sygusRewSynthRec"
1384  category   = "regular"
1385  long       = "sygus-rr-synth-rec"
1386  type       = "bool"
1387  default    = "false"
1388  help       = "synthesize rewrite rules over all sygus grammar types recursively"
1389
1390[[option]]
1391  name       = "sygusQueryGen"
1392  category   = "regular"
1393  long       = "sygus-query-gen"
1394  type       = "bool"
1395  default    = "false"
1396  help       = "use sygus to enumerate interesting satisfiability queries"
1397
1398[[option]]
1399  name       = "sygusQueryGenThresh"
1400  category   = "regular"
1401  long       = "sygus-query-gen-thresh=N"
1402  type       = "unsigned"
1403  default    = "5"
1404  help       = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen"
1405
1406[[option]]
1407  name       = "sygusQueryGenCheck"
1408  category   = "regular"
1409  long       = "sygus-query-gen-check"
1410  type       = "bool"
1411  default    = "true"
1412  help       = "use interesting satisfiability queries to check soundness of CVC4"
1413
1414[[option]]
1415  name       = "sygusQueryGenDumpFiles"
1416  category   = "regular"
1417  long       = "sygus-query-gen-dump-files"
1418  type       = "bool"
1419  default    = "false"
1420  help       = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen"
1421
1422[[option]]
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"
1431
1432[[option]]
1433  name       = "sygusFilterSolRevSubsume"
1434  category   = "expert"
1435  long       = "sygus-filter-sol-rev"
1436  type       = "bool"
1437  default    = "false"
1438  help       = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
1439
1440
1441[[option]]
1442  name       = "sygusExprMinerCheckUseExport"
1443  category   = "expert"
1444  long       = "sygus-expr-miner-check-use-export"
1445  type       = "bool"
1446  default    = "true"
1447  help       = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners"
1448
1449# CEGQI applied to general quantified formulas
1450
1451[[option]]
1452  name       = "cbqi"
1453  category   = "regular"
1454  long       = "cbqi"
1455  type       = "bool"
1456  default    = "false"
1457  help       = "turns on counterexample-based quantifier instantiation"
1458
1459[[option]]
1460  name       = "cbqiFullEffort"
1461  category   = "regular"
1462  long       = "cbqi-full"
1463  type       = "bool"
1464  default    = "false"
1465  help       = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
1466
1467[[option]]
1468  name       = "recurseCbqi"
1469  category   = "regular"
1470  long       = "cbqi-recurse"
1471  type       = "bool"
1472  default    = "true"
1473  read_only  = true
1474  help       = "turns on recursive counterexample-based quantifier instantiation"
1475
1476[[option]]
1477  name       = "cbqiSat"
1478  category   = "regular"
1479  long       = "cbqi-sat"
1480  type       = "bool"
1481  default    = "true"
1482  help       = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
1483
1484[[option]]
1485  name       = "cbqiModel"
1486  category   = "regular"
1487  long       = "cbqi-model"
1488  type       = "bool"
1489  default    = "true"
1490  help       = "guide instantiations by model values for counterexample-based quantifier instantiation"
1491
1492[[option]]
1493  name       = "cbqiAll"
1494  category   = "regular"
1495  long       = "cbqi-all"
1496  type       = "bool"
1497  default    = "false"
1498  help       = "apply counterexample-based instantiation to all quantified formulas"
1499
1500[[option]]
1501  name       = "cbqiMultiInst"
1502  category   = "regular"
1503  long       = "cbqi-multi-inst"
1504  type       = "bool"
1505  default    = "false"
1506  help       = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
1507
1508[[option]]
1509  name       = "cbqiRepeatLit"
1510  category   = "regular"
1511  long       = "cbqi-repeat-lit"
1512  type       = "bool"
1513  default    = "false"
1514  help       = "solve literals more than once in counterexample-based quantifier instantiation"
1515
1516[[option]]
1517  name       = "cbqiInnermost"
1518  category   = "regular"
1519  long       = "cbqi-innermost"
1520  type       = "bool"
1521  default    = "true"
1522  help       = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
1523
1524[[option]]
1525  name       = "cbqiNestedQE"
1526  category   = "regular"
1527  long       = "cbqi-nested-qe"
1528  type       = "bool"
1529  default    = "false"
1530  help       = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
1531
1532# CEGQI for arithmetic
1533
1534[[option]]
1535  name       = "cbqiUseInfInt"
1536  category   = "regular"
1537  long       = "cbqi-use-inf-int"
1538  type       = "bool"
1539  default    = "false"
1540  help       = "use integer infinity for vts in counterexample-based quantifier instantiation"
1541
1542[[option]]
1543  name       = "cbqiUseInfReal"
1544  category   = "regular"
1545  long       = "cbqi-use-inf-real"
1546  type       = "bool"
1547  default    = "false"
1548  help       = "use real infinity for vts in counterexample-based quantifier instantiation"
1549
1550[[option]]
1551  name       = "cbqiPreRegInst"
1552  category   = "regular"
1553  long       = "cbqi-prereg-inst"
1554  type       = "bool"
1555  default    = "false"
1556  help       = "preregister ground instantiations in counterexample-based quantifier instantiation"
1557
1558[[option]]
1559  name       = "cbqiMinBounds"
1560  category   = "regular"
1561  long       = "cbqi-min-bounds"
1562  type       = "bool"
1563  default    = "false"
1564  read_only  = true
1565  help       = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
1566
1567[[option]]
1568  name       = "cbqiRoundUpLowerLia"
1569  category   = "regular"
1570  long       = "cbqi-round-up-lia"
1571  type       = "bool"
1572  default    = "false"
1573  read_only  = true
1574  help       = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
1575
1576[[option]]
1577  name       = "cbqiMidpoint"
1578  category   = "regular"
1579  long       = "cbqi-midpoint"
1580  type       = "bool"
1581  default    = "false"
1582  help       = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
1583
1584[[option]]
1585  name       = "cbqiNopt"
1586  category   = "regular"
1587  long       = "cbqi-nopt"
1588  type       = "bool"
1589  default    = "true"
1590  read_only  = true
1591  help       = "non-optimal bounds for counterexample-based quantifier instantiation"
1592
1593[[option]]
1594  name       = "cbqiLitDepend"
1595  category   = "regular"
1596  long       = "cbqi-lit-dep"
1597  type       = "bool"
1598  default    = "true"
1599  read_only  = true
1600  help       = "dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation"
1601
1602# CEGQI for EPR
1603
1604[[option]]
1605  name       = "quantEpr"
1606  category   = "regular"
1607  long       = "quant-epr"
1608  type       = "bool"
1609  default    = "false"
1610  help       = "infer whether in effectively propositional fragment, use for cbqi"
1611
1612[[option]]
1613  name       = "quantEprMatching"
1614  category   = "regular"
1615  long       = "quant-epr-match"
1616  type       = "bool"
1617  default    = "true"
1618  read_only  = true
1619  help       = "use matching heuristics for EPR instantiation"
1620
1621# CEGQI for BV
1622
1623[[option]]
1624  name       = "cbqiBv"
1625  category   = "regular"
1626  long       = "cbqi-bv"
1627  type       = "bool"
1628  default    = "true"
1629  help       = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
1630
1631[[option]]
1632  name       = "cbqiBvInterleaveValue"
1633  category   = "regular"
1634  long       = "cbqi-bv-interleave-value"
1635  type       = "bool"
1636  default    = "false"
1637  help       = "interleave model value instantiation with word-level inversion approach"
1638
1639[[option]]
1640  name       = "cbqiBvIneqMode"
1641  category   = "regular"
1642  long       = "cbqi-bv-ineq=MODE"
1643  type       = "CVC4::theory::quantifiers::CbqiBvIneqMode"
1644  default    = "CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY"
1645  handler    = "stringToCbqiBvIneqMode"
1646  includes   = ["options/quantifiers_modes.h"]
1647  help       = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
1648
1649[[option]]
1650  name       = "cbqiBvRmExtract"
1651  category   = "regular"
1652  long       = "cbqi-bv-rm-extract"
1653  type       = "bool"
1654  default    = "true"
1655  help       = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
1656
1657[[option]]
1658  name       = "cbqiBvLinearize"
1659  category   = "regular"
1660  long       = "cbqi-bv-linear"
1661  type       = "bool"
1662  default    = "true"
1663  help       = "linearize adder chains for variables"
1664
1665[[option]]
1666  name       = "cbqiBvSolveNl"
1667  category   = "regular"
1668  long       = "cbqi-bv-solve-nl"
1669  type       = "bool"
1670  default    = "false"
1671  help       = "try to solve non-linear bv literals using model value projections"
1672
1673[[option]]
1674  name       = "cbqiBvConcInv"
1675  category   = "regular"
1676  long       = "cbqi-bv-concat-inv"
1677  type       = "bool"
1678  default    = "true"
1679  help       = "compute inverse for concat over equalities rather than producing an invertibility condition"
1680
1681### Local theory extensions options
1682
1683[[option]]
1684  name       = "localTheoryExt"
1685  category   = "regular"
1686  long       = "local-t-ext"
1687  type       = "bool"
1688  default    = "false"
1689  read_only  = true
1690  help       = "do instantiation based on local theory extensions"
1691
1692[[option]]
1693  name       = "ltePartialInst"
1694  category   = "regular"
1695  long       = "lte-partial-inst"
1696  type       = "bool"
1697  default    = "false"
1698  read_only  = true
1699  help       = "partially instantiate local theory quantifiers"
1700
1701[[option]]
1702  name       = "lteRestrictInstClosure"
1703  category   = "regular"
1704  long       = "lte-restrict-inst-closure"
1705  type       = "bool"
1706  default    = "false"
1707  read_only  = true
1708  help       = "treat arguments of inst closure as restricted terms for instantiation"
1709
1710### Reduction options
1711
1712[[option]]
1713  name       = "quantAlphaEquiv"
1714  category   = "regular"
1715  long       = "quant-alpha-equiv"
1716  type       = "bool"
1717  default    = "true"
1718  read_only  = true
1719  help       = "infer alpha equivalence between quantified formulas"
1720
1721[[option]]
1722  name       = "macrosQuant"
1723  category   = "regular"
1724  long       = "macros-quant"
1725  type       = "bool"
1726  default    = "false"
1727  help       = "perform quantifiers macro expansion"
1728
1729[[option]]
1730  name       = "macrosQuantMode"
1731  category   = "regular"
1732  long       = "macros-quant-mode=MODE"
1733  type       = "CVC4::theory::quantifiers::MacrosQuantMode"
1734  default    = "CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF"
1735  handler    = "stringToMacrosQuantMode"
1736  includes   = ["options/quantifiers_modes.h"]
1737  read_only  = true
1738  help       = "mode for quantifiers macro expansion"
1739
1740[[option]]
1741  name       = "quantDynamicSplit"
1742  category   = "regular"
1743  long       = "quant-dsplit-mode=MODE"
1744  type       = "CVC4::theory::quantifiers::QuantDSplitMode"
1745  default    = "CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE"
1746  handler    = "stringToQuantDSplitMode"
1747  includes   = ["options/quantifiers_modes.h"]
1748  help       = "mode for dynamic quantifiers splitting"
1749
1750[[option]]
1751  name       = "quantAntiSkolem"
1752  category   = "regular"
1753  long       = "quant-anti-skolem"
1754  type       = "bool"
1755  default    = "false"
1756  help       = "perform anti-skolemization for quantified formulas"
1757
1758### Higher-order options
1759
1760[[option]]
1761  name       = "hoMatching"
1762  category   = "regular"
1763  long       = "ho-matching"
1764  type       = "bool"
1765  default    = "true"
1766  read_only  = true
1767  help       = "do higher-order matching algorithm for triggers with variable operators"
1768
1769[[option]]
1770  name       = "hoMatchingVarArgPriority"
1771  category   = "regular"
1772  long       = "ho-matching-var-priority"
1773  type       = "bool"
1774  default    = "true"
1775  read_only  = true
1776  help       = "give priority to variable arguments over constant arguments"
1777
1778[[option]]
1779  name       = "hoMergeTermDb"
1780  category   = "regular"
1781  long       = "ho-merge-term-db"
1782  type       = "bool"
1783  default    = "true"
1784  read_only  = true
1785  help       = "merge term indices modulo equality"
1786
1787### Proof options
1788
1789[[option]]
1790  name       = "trackInstLemmas"
1791  category   = "regular"
1792  long       = "track-inst-lemmas"
1793  type       = "bool"
1794  default    = "false"
1795  help       = "track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)"
1796