1SMTENGINE(3cvc)             CVC4 Library Interfaces            SMTENGINE(3cvc)
2
3
4

NAME

6       SmtEngine  -  the primary interface to CVC4's theorem-proving capabili‐
7       ties
8

DESCRIPTION

10       SmtEngine is the main entry point into the CVC4 theorem prover API.
11
12

SMTENGINE OPTIONS

14       The SmtEngine is in charge  of  setting  and  getting  information  and
15       options.  Numerous options are available via the SmtEngine::setOption()
16       call.  SmtEngine::setOption() and SmtEngine::getOption() use  the  fol‐
17       lowing option keys.
18
19
20
21              COMMON OPTIONS
22
23              input-language
24                        (InputLanguage) force input language (default is
25                        "auto"; see --lang help)
26
27              output-language
28                        (OutputLanguage) force output language (default is
29                        "auto"; see --output-lang help)
30
31              quiet     (void) decrease verbosity (may be repeated)
32
33              statistics
34                        (bool) give statistics on exit
35
36              verbose   (void) increase verbosity (may be repeated)
37
38              copyright (void) show CVC4 copyright information
39
40              help      (bool) full command line reference
41
42              seed      (uint64_t) seed for random number generator
43
44              show-config
45                        (void) show CVC4 static configuration
46
47              version   (bool) identify this CVC4 binary
48
49              strict-parsing
50                        (bool) be less tolerant of non-conforming inputs
51
52              cpu-time  (bool) measures CPU time if set to true and wall time
53                        if false (default false)
54
55              dump-to   (std::string) all dumping goes to FILE (instead of
56                        stdout)
57
58              dump      (std::string) dump preprocessed assertions, etc., see
59                        --dump=help
60
61              hard-limit
62                        (bool) the resource limit is hard potentially leaving
63                        the smtEngine in an unsafe state (should be destroyed
64                        and rebuild after resourcing out)
65
66              incremental
67                        (bool) enable incremental solving
68
69              produce-assertions
70                        (bool) keep an assertions list (enables get-assertions
71                        command)
72
73              produce-models
74                        (bool) support the get-value and get-model commands
75
76              reproducible-resource-limit
77                        (unsigned long) enable resource limiting per query
78
79              rlimit    (unsigned long) enable resource limiting (currently,
80                        roughly the number of SAT conflicts)
81
82              tlimit-per
83                        (unsigned long) enable time limiting per query (give
84                        milliseconds)
85
86              tlimit    (unsigned long) enable time limiting (give millisec‐
87                        onds)
88
89
90              ARITHMETIC THEORY OPTIONS
91
92              approx-branch-depth
93                        (int16_t) maximum branch depth the approximate solver
94                        is allowed to take
95
96              arith-no-partial-fun
97                        (bool) do not use partial function semantics for
98                        arithmetic (not SMT LIB compliant)
99
100              arith-prop-clauses
101                        (uint16_t) rows shorter than this are propagated as
102                        clauses
103
104              arith-prop
105                        (ArithPropagationMode) turns on arithmetic propagation
106                        (default is 'old', see --arith-prop=help)
107
108              arith-rewrite-equalities
109                        (bool) turns on the preprocessing rewrite turning
110                        equalities into a conjunction of inequalities
111
112              collect-pivot-stats
113                        (bool) collect the pivot history
114
115              cut-all-bounded
116                        (bool) turns on the integer solving step of periodi‐
117                        cally cutting all integer variables that have both
118                        upper and lower bounds
119
120              dio-decomps
121                        (bool) let skolem variables for integer divisibility
122                        constraints leak from the dio solver
123
124              dio-repeat
125                        (bool) handle dio solver constraints in mass or one at
126                        a time
127
128              dio-solver
129                        (bool) turns on Linear Diophantine Equation solver
130                        (Griggio, JSAT 2012)
131
132              dio-turns (int) turns in a row dio solver cutting gets
133
134              error-selection-rule
135                        (ErrorSelectionRule) change the pivot rule for the
136                        basic variable (default is 'min', see --pivot-rule
137                        help)
138
139              fc-penalties
140                        (bool) turns on degenerate pivot penalties
141
142              heuristic-pivots
143                        (int16_t) the number of times to apply the heuristic
144                        pivot rule; if N < 0, this defaults to the number of
145                        variables; if this is unset, this is tuned by the
146                        logic selection
147
148              lemmas-on-replay-failure
149                        (bool) attempt to use external lemmas if approximate
150                        solve integer failed
151
152              maxCutsInContext
153                        (unsigned) maximum cuts in a given context before sig‐
154                        nalling a restart
155
156              miplib-trick
157                        (bool) turns on the preprocessing step of attempting
158                        to infer bounds on miplib problems
159
160              miplib-trick-subs
161                        (unsigned) do substitution for miplib 'tmp' vars if
162                        defined in <= N eliminated vars
163
164              new-prop  (bool) use the new row propagation system
165
166              nl-ext    (bool) extended approach to non-linear
167
168              nl-ext-ent-conf
169                        (bool) check for entailed conflicts in non-linear
170                        solver
171
172              nl-ext-factor
173                        (bool) use factoring inference in non-linear solver
174
175              nl-ext-inc-prec
176                        (bool) whether to increment the precision for irra‐
177                        tional function constraints
178
179              nl-ext-purify
180                        (bool) purify non-linear terms at preprocess
181
182              nl-ext-rbound
183                        (bool) use resolution-style inference for inferring
184                        new bounds
185
186              nl-ext-rewrite
187                        (bool) do rewrites in non-linear solver
188
189              nl-ext-split-zero
190                        (bool) intial splits on zero for all variables
191
192              nl-ext-tf-taylor-deg
193                        (int16_t) initial degree of polynomials for Taylor
194                        approximation
195
196              nl-ext-tf-tplanes
197                        (bool) use non-terminating tangent plane strategy for
198                        transcendental functions for non-linear
199
200              nl-ext-tplanes
201                        (bool) use non-terminating tangent plane strategy for
202                        non-linear
203
204              nl-ext-tplanes-interleave
205                        (bool) interleave tangent plane strategy for non-lin‐
206                        ear
207
208              pb-rewrites
209                        (bool) apply pseudo boolean rewrites
210
211              pivot-threshold
212                        (uint16_t) sets the number of pivots using
213                        --pivot-rule per basic variable per simplex instance
214                        before using variable order
215
216              pp-assert-max-sub-size
217                        (unsigned) threshold for substituting an equality in
218                        ppAssert
219
220              prop-row-length
221                        (uint16_t) sets the maximum row length to be used in
222                        propagation
223
224              replay-early-close-depth
225                        (int) multiples of the depths to try to close the
226                        approx log eagerly
227
228              replay-failure-penalty
229                        (int) number of solve integer attempts to skips after
230                        a numeric failure
231
232              replay-lemma-reject-cut
233                        (unsigned) maximum complexity of any coefficient while
234                        outputting replaying cut lemmas
235
236              replay-num-err-penalty
237                        (int) number of solve integer attempts to skips after
238                        a numeric failure
239
240              replay-reject-cut
241                        (unsigned) maximum complexity of any coefficient while
242                        replaying cuts
243
244              replay-soi-major-threshold
245                        (double) threshold for a major tolerance failure by
246                        the approximate solver
247
248              replay-soi-major-threshold-pen
249                        (int) threshold for a major tolerance failure by the
250                        approximate solver
251
252              replay-soi-minor-threshold
253                        (double) threshold for a minor tolerance failure by
254                        the approximate solver
255
256              replay-soi-minor-threshold-pen
257                        (int) threshold for a minor tolerance failure by the
258                        approximate solver
259
260              restrict-pivots
261                        (bool) have a pivot cap for simplex at effort levels
262                        below fullEffort
263
264              revert-arith-models-on-unsat
265                        (bool) revert the arithmetic model to a known safe
266                        model on unsat if one is cached
267
268              rewrite-divk
269                        (bool) rewrite division and mod when by a constant
270                        into linear terms
271
272              rr-turns  (int) round robin turn
273
274              se-solve-int
275                        (bool) attempt to use the approximate solve integer
276                        method on standard effort
277
278              simplex-check-period
279                        (uint16_t) the number of pivots to do in simplex
280                        before rechecking for a conflict on all variables
281
282              snorm-infer-eq
283                        (bool) infer equalities based on Shostak normalization
284
285              soi-qe    (bool) use quick explain to minimize the sum of infea‐
286                        sibility conflicts
287
288              standard-effort-variable-order-pivots
289                        (int16_t) limits the number of pivots in a single
290                        invocation of check() at a non-full effort level using
291                        Bland's pivot rule (EXPERTS only)
292
293              unate-lemmas
294                        (ArithUnateLemmaMode) determines which lemmas to add
295                        before solving (default is 'all', see --unate-lem‐
296                        mas=help)
297
298              use-approx
299                        (bool) attempt to use an approximate solver
300
301              use-fcsimplex
302                        (bool) use focusing and converging simplex (FMCAD 2013
303                        submission)
304
305              use-soi   (bool) use sum of infeasibility simplex (FMCAD 2013
306                        submission)
307
308              ARRAYS THEORY OPTIONS
309
310              arrays-config
311                        (int) set different array option configurations - for
312                        developers only
313
314              arrays-eager-index
315                        (bool) turn on eager index splitting for generated
316                        array lemmas
317
318              arrays-eager-lemmas
319                        (bool) turn on eager lemma generation for arrays
320
321              arrays-lazy-rintro1
322                        (bool) turn on optimization to only perform RIntro1
323                        rule lazily (see Jovanovic/Barrett 2012: Being Careful
324                        with Theory Combination)
325
326              arrays-model-based
327                        (bool) turn on model-based array solver
328
329              arrays-optimize-linear
330                        (bool) turn on optimization for linear array terms
331                        (see de Moura FMCAD 09 arrays paper)
332
333              arrays-prop
334                        (int) propagation effort for arrays: 0 is none, 1 is
335                        some, 2 is full
336
337              arrays-reduce-sharing
338                        (bool) use model information to reduce size of care
339                        graph for arrays
340
341              arrays-weak-equiv
342                        (bool) use algorithm from Christ/Hoenicke (SMT 2014)
343
344              BASE OPTIONS
345
346              debug     (std::string) debug something (e.g. -d arith), can
347                        repeat
348
349              parse-only
350                        (bool) exit after parsing input
351
352              preprocess-only
353                        (bool) exit after preprocessing input
354
355              print-success
356                        (bool) print the "success" output required of
357                        SMT-LIBv2
358
359              stats-every-query
360                        (bool) in incremental mode, print stats after every
361                        satisfiability or validity query
362
363              stats-hide-zeros
364                        (bool) hide statistics which are zero
365
366              trace     (std::string) trace something (e.g. -t pushpop), can
367                        repeat
368
369              verbosity (int) the verbosity level of CVC4
370
371              hide-zero-stats
372                        [undocumented]
373
374              language  [undocumented]
375
376              no-statistics
377                        [undocumented]
378
379              no-statistics-every-query
380                        [undocumented]
381
382              output-language
383                        [undocumented]
384
385              show-zero-stats
386                        [undocumented]
387
388              smtlib-strict
389                        SMT-LIBv2 compliance mode (implies other options)
390
391              statistics
392                        [undocumented]
393
394              statistics-every-query
395                        [undocumented]
396
397              stats-show-zeros
398                        [undocumented]
399
400              BITVECTOR THEORY OPTIONS
401
402              bitblast-aig
403                        (bool) bitblast by first converting to AIG (implies
404                        --bitblast=eager)
405
406              bitblast  (CVC4::theory::bv::BitblastMode) choose bitblasting
407                        mode, see --bitblast=help
408
409              bool-to-bv
410                        (bool) convert booleans to bit-vectors of size 1 when
411                        possible
412
413              bv-abstraction
414                        (bool) mcm benchmark abstraction (EXPERTS only)
415
416              bv-aig-simp
417                        (std::string) abc command to run AIG simplifications
418                        (implies --bitblast-aig, default is "balance;drw")
419                        (EXPERTS only)
420
421              bv-alg-extf
422                        (bool) algebraic inferences for extended functions
423
424              bv-algebraic-budget
425                        (unsigned) the budget allowed for the algebraic solver
426                        in number of SAT conflicts (EXPERTS only)
427
428              bv-algebraic-solver
429                        (bool) turn on the algebraic solver for the bit-vector
430                        theory (only if --bitblast=lazy)
431
432              bv-div-zero-const
433                        (bool) always return -1 on division by zero
434
435              bv-eager-explanations
436                        (bool) compute bit-blasting propagation explanations
437                        eagerly (EXPERTS only)
438
439              bv-eq-slicer
440                        (CVC4::theory::bv::BvSlicerMode) turn on the slicing
441                        equality solver for the bit-vector theory (only if
442                        --bitblast=lazy)
443
444              bv-eq-solver
445                        (bool) use the equality engine for the bit-vector the‐
446                        ory (only if --bitblast=lazy)
447
448              bv-extract-arith
449                        (bool) enable rewrite pushing extract [i:0] over
450                        arithmetic operations (can blow up) (EXPERTS only)
451
452              bv-gauss-elim
453                        (bool) simplify formula via Gaussian Elimination if
454                        applicable (EXPERTS only)
455
456              bv-inequality-solver
457                        (bool) turn on the inequality solver for the bit-vec‐
458                        tor theory (only if --bitblast=lazy)
459
460              bv-intro-pow2
461                        (bool) introduce bitvector powers of two as a prepro‐
462                        cessing pass (EXPERTS only)
463
464              bv-lazy-reduce-extf
465                        (bool) reduce extended functions like bv2nat and
466                        int2bv at last call instead of full effort
467
468              bv-lazy-rewrite-extf
469                        (bool) lazily rewrite extended functions like bv2nat
470                        and int2bv
471
472              bv-num-func
473                        (unsigned) number of function symbols in conflicts
474                        that are generalized (EXPERTS only)
475
476              bv-propagate
477                        (bool) use bit-vector propagation in the bit-blaster
478
479              bv-quick-xplain
480                        (bool) minimize bv conflicts using the QuickXplain
481                        algorithm (EXPERTS only)
482
483              bv-sat-solver
484                        (CVC4::theory::bv::SatSolverMode) choose which sat
485                        solver to use, see --bv-sat-solver=help (EXPERTS only)
486
487              bv-skolemize
488                        (bool) skolemize arguments for bv abstraction (only
489                        does something if --bv-abstraction is on) (EXPERTS
490                        only)
491
492              bv-to-bool
493                        (bool) lift bit-vectors of size 1 to booleans when
494                        possible
495
496              DATATYPES THEORY OPTIONS
497
498              cdt-bisimilar
499                        (bool) do bisimilarity check for co-datatypes
500
501              dt-binary-split
502                        (bool) do binary splits for datatype constructor types
503
504              dt-blast-splits
505                        (bool) when applicable, blast splitting lemmas for all
506                        variables at once
507
508              dt-cyclic (bool) do cyclicity check for datatypes
509
510              dt-force-assignment
511                        (bool) force the datatypes solver to give specific
512                        values to all datatypes terms before answering sat
513
514              dt-infer-as-lemmas
515                        (bool) always send lemmas out instead of making inter‐
516                        nal inferences
517
518              dt-ref-sk-intro
519                        (bool) introduce reference skolems for shorter expla‐
520                        nations
521
522              dt-rewrite-error-sel
523                        (bool) rewrite incorrectly applied selectors to arbi‐
524                        trary ground term (EXPERTS only)
525
526              dt-share-sel
527                        (bool) internally use shared selectors across multiple
528                        constructors
529
530              dt-use-testers
531                        (bool) do not preprocess away tester predicates
532
533              sygus-abort-size
534                        (int) tells enumerative sygus to only consider solu‐
535                        tions up to term size N (-1 == no limit, default)
536
537              sygus-eval-builtin
538                        (bool) use builtin kind for evaluation functions in
539                        sygus
540
541              sygus-fair-max
542                        (bool) use max instead of sum for multi-function sygus
543                        conjectures
544
545              sygus-fair
546                        (CVC4::theory::SygusFairMode) if and how to apply
547                        fairness for sygus
548
549              sygus-opt1
550                        (bool) sygus experimental option
551
552              sygus-sym-break
553                        (bool) simple sygus sym break lemmas
554
555              sygus-sym-break-dynamic
556                        (bool) dynamic sygus sym break lemmas
557
558              sygus-sym-break-lazy
559                        (bool) lazily add symmetry breaking lemmas for terms
560
561              sygus-sym-break-pbe
562                        (bool) sygus sym break lemmas based on pbe conjectures
563
564              sygus-sym-break-rlv
565                        (bool) add relevancy conditions to symmetry breaking
566                        lemmas
567
568              DECISION HEURISTICS OPTIONS
569
570              decision-random-weight
571                        (int) assign random weights to nodes between 0 and N-1
572                        (0: disable) (EXPERTS only)
573
574              decision-threshold
575                        (decision::DecisionWeight) ignore all nodes greater
576                        than threshold in first attempt to pick decision
577                        (EXPERTS only)
578
579              decision-use-weight
580                        (bool) use the weight nodes (locally, by looking at
581                        children) to direct recursive search (EXPERTS only)
582
583              decision-weight-internal
584                        (decision::DecisionWeightInternal) computer weights of
585                        internal nodes using children: off, max, sum, usr1
586                        (meaning evolving) (EXPERTS only)
587
588              decision-mode
589                        (decision::DecisionMode) choose decision mode, see
590                        --decision=help
591
592              EXPRESSION PACKAGE OPTIONS
593
594              default-dag-thresh
595                        (int) dagify common subexprs appearing > N times (1 ==
596                        default, 0 == don't dagify)
597
598              default-expr-depth
599                        (int) print exprs to depth N (0 == default, -1 == no
600                        limit)
601
602              eager-type-checking
603                        (bool) type check expressions immediately on creation
604                        (debug builds only)
605
606              print-expr-types
607                        (bool) print types with variables when printing exprs
608
609              type-checking
610                        (bool) never type check expressions
611
612              dag-thresh
613                        [undocumented]
614
615              dag-threshold
616                        [undocumented]
617
618              expr-depth
619                        [undocumented]
620
621              no-type-checking
622                        [undocumented]
623
624              IDL OPTIONS
625
626              idl-rewrite-equalities
627                        (bool) enable rewriting equalities into two inequali‐
628                        ties in IDL solver (default is disabled)
629
630              DRIVER OPTIONS
631
632              continued-execution
633                        (bool) continue executing commands, even on error
634
635              early-exit
636                        (bool) do not run destructors at exit; default on
637                        except in debug builds (EXPERTS only)
638
639              fallback-sequential
640                        (bool) Switch to sequential mode (instead of printing
641                        an error) if it can't be solved in portfolio mode
642
643              filter-lemma-length
644                        (int) don't share (among portfolio threads) lemmas
645                        strictly longer than N
646
647              incremental-parallel
648                        (bool) Use parallel solver even in incremental mode
649                        (may print 'unknown's at times)
650
651              interactive
652                        (bool) force interactive/non-interactive mode
653
654              interactive-prompt
655                        (bool) interactive prompting while in interactive mode
656
657              segv-spin (bool) spin on segfault/other crash waiting for gdb
658
659              show-debug-tags
660                        (void) show all available tags for debugging
661
662              show-trace-tags
663                        (void) show all available tags for tracing
664
665              tear-down-incremental
666                        (int) implement PUSH/POP/multi-query by destroying and
667                        recreating SmtEngine every N queries (EXPERTS only)
668
669              thread-stack
670                        (unsigned) stack size for worker threads in MB (0
671                        means use Boost/thread lib default)
672
673              threadN   (void) configures portfolio thread N (0..#threads-1)
674
675              threads   (unsigned) Total number of threads for portfolio
676
677              wait-to-join
678                        (bool) wait for other threads to join before quitting
679                        (EXPERTS only)
680
681              license   [undocumented]
682
683              segv-nospin
684                        [undocumented]
685
686              PARSER OPTIONS
687
688              filesystem-access
689                        (bool) [undocumented]
690
691              global-declarations
692                        (bool) force all declarations and definitions to be
693                        global
694
695              mmap      (bool) memory map file input
696
697              semantic-checks
698                        (bool) disable ALL semantic checks, including type
699                        checks
700
701              no-checking
702                        [undocumented]
703
704              no-include-file
705                        [undocumented]
706
707              PRINTING OPTIONS
708
709              inst-format
710                        (InstFormatMode) print format mode for instantiations,
711                        see --inst-format=help
712
713              model-format
714                        (ModelFormatMode) print format mode for models, see
715                        --model-format=help
716
717              PROOF OPTIONS
718
719              aggressive-core-min
720                        (bool) turns on aggressive unsat core minimization
721                        (experimental)
722
723              allow-empty-dependencies
724                        (bool) if unable to track the dependencies of a
725                        rewritten/preprocessed assertion, fail silently
726
727              fewer-preprocessing-holes
728                        (bool) try to eliminate preprocessing holes in proofs
729
730              lfsc-letification
731                        (bool) turns on global letification in LFSC proofs
732
733              SAT LAYER OPTIONS
734
735              minisat-dump-dimacs
736                        (bool) instead of solving minisat dumps the asserted
737                        clauses in Dimacs format
738
739              minisat-elimination
740                        (bool) use Minisat elimination
741
742              random-frequency
743                        (double) sets the frequency of random decisions in the
744                        sat solver (P=0.0 by default)
745
746              random-seed
747                        (uint32_t) sets the random seed for the sat solver
748
749              refine-conflicts
750                        (bool) refine theory conflict clauses (default false)
751
752              restart-int-base
753                        (unsigned) sets the base restart interval for the sat
754                        solver (N=25 by default)
755
756              restart-int-inc
757                        (double) sets the restart interval increase factor for
758                        the sat solver (F=3.0 by default)
759
760              QUANTIFIERS OPTIONS
761
762              ag-miniscope-quant
763                        (bool) perform aggressive miniscoping for quantifiers
764
765              cbqi      (bool) turns on counterexample-based quantifier
766                        instantiation
767
768              cbqi-all  (bool) apply counterexample-based instantiation to all
769                        quantified formulas
770
771              cbqi-bv   (bool) use word-level inversion approach for coun‐
772                        terexample-guided quantifier instantiation for
773                        bit-vectors
774
775              cbqi-bv-concat-inv
776                        (bool) compute inverse for concat over equalities
777                        rather than producing an invertibility condition
778
779              cbqi-bv-ineq
780                        (CVC4::theory::quantifiers::CbqiBvIneqMode) choose
781                        mode for handling bit-vector inequalities with coun‐
782                        terexample-guided instantiation
783
784              cbqi-bv-interleave-value
785                        (bool) interleave model value instantiation with
786                        word-level inversion approach
787
788              cbqi-bv-linear
789                        (bool) linearize adder chains for variables
790
791              cbqi-bv-rm-extract
792                        (bool) replaces extract terms with variables for coun‐
793                        terexample-guided instantiation for bit-vectors
794
795              cbqi-bv-solve-nl
796                        (bool) try to solve non-linear bv literals using model
797                        value projections
798
799              cbqi-full (bool) turns on full effort counterexample-based quan‐
800                        tifier instantiation, which may resort to model-value
801                        instantiation
802
803              cbqi-innermost
804                        (bool) only process innermost quantified formulas in
805                        counterexample-based quantifier instantiation
806
807              cbqi-lit-dep
808                        (bool) dependency lemmas for quantifier alternation in
809                        counterexample-based quantifier instantiation
810
811              cbqi-midpoint
812                        (bool) choose substitutions based on midpoints of
813                        lower and upper bounds for counterexample-based quan‐
814                        tifier instantiation
815
816              cbqi-min-bounds
817                        (bool) use minimally constrained lower/upper bound for
818                        counterexample-based quantifier instantiation
819
820              cbqi-model
821                        (bool) guide instantiations by model values for coun‐
822                        terexample-based quantifier instantiation
823
824              cbqi-multi-inst
825                        (bool) when applicable, do multi instantiations per
826                        quantifier per round in counterexample-based quanti‐
827                        fier instantiation
828
829              cbqi-nested-qe
830                        (bool) process nested quantified formulas with quanti‐
831                        fier elimination in counterexample-based quantifier
832                        instantiation
833
834              cbqi-nopt (bool) non-optimal bounds for counterexample-based
835                        quantifier instantiation
836
837              cbqi-prereg-inst
838                        (bool) preregister ground instantiations in counterex‐
839                        ample-based quantifier instantiation
840
841              cbqi-recurse
842                        (bool) turns on recursive counterexample-based quanti‐
843                        fier instantiation
844
845              cbqi-repeat-lit
846                        (bool) solve literals more than once in counterexam‐
847                        ple-based quantifier instantiation
848
849              cbqi-round-up-lia
850                        (bool) round up integer lower bounds in substitutions
851                        for counterexample-based quantifier instantiation
852
853              cbqi-sat  (bool) answer sat when quantifiers are asserted with
854                        counterexample-based quantifier instantiation
855
856              cbqi-use-inf-int
857                        (bool) use integer infinity for vts in counterexam‐
858                        ple-based quantifier instantiation
859
860              cbqi-use-inf-real
861                        (bool) use real infinity for vts in counterexam‐
862                        ple-based quantifier instantiation
863
864              cegis-sample
865                        (CVC4::theory::quantifiers::CegisSampleMode) mode for
866                        using samples in the counterexample-guided inductive
867                        synthesis loop
868
869              cegqi     (bool) counterexample-guided quantifier instantiation
870                        for sygus
871
872              cegqi-si-abort
873                        (bool) abort if synthesis conjecture is not single
874                        invocation
875
876              cegqi-si-partial
877                        (bool) combined techniques for synthesis conjectures
878                        that are partially single invocation
879
880              cegqi-si-reconstruct
881                        (bool) reconstruct solutions for single invocation
882                        conjectures in original grammar
883
884              cegqi-si-reconstruct-const
885                        (bool) include constants when reconstruct solutions
886                        for single invocation conjectures in original grammar
887
888              cegqi-si-sol-min-core
889                        (bool) minimize solutions for single invocation con‐
890                        jectures based on unsat core
891
892              cegqi-si-sol-min-inst
893                        (bool) minimize individual instantiations for single
894                        invocation conjectures based on unsat core
895
896              cegqi-si  (CVC4::theory::quantifiers::CegqiSingleInvMode) mode
897                        for processing single invocation synthesis conjectures
898
899              cond-rewrite-quant
900                        (bool) conditional rewriting of quantified formulas
901
902              cond-var-split-agg-quant
903                        (bool) aggressive split quantified formulas that lead
904                        to variable eliminations
905
906              cond-var-split-quant
907                        (bool) split quantified formulas that lead to variable
908                        eliminations
909
910              conjecture-filter-active-terms
911                        (bool) filter based on active terms
912
913              conjecture-filter-canonical
914                        (bool) filter based on canonicity
915
916              conjecture-filter-model
917                        (bool) filter based on model
918
919              conjecture-gen
920                        (bool) generate candidate conjectures for inductive
921                        proofs
922
923              conjecture-gen-gt-enum
924                        (int) number of ground terms to generate for model
925                        filtering
926
927              conjecture-gen-max-depth
928                        (int) maximum depth of terms to consider for conjec‐
929                        tures
930
931              conjecture-gen-per-round
932                        (int) number of conjectures to generate per instantia‐
933                        tion round
934
935              conjecture-gen-uee-intro
936                        (bool) more aggressive merging for universal equality
937                        engine, introduces terms
938
939              conjecture-no-filter
940                        (bool) do not filter conjectures
941
942              dt-stc-ind
943                        (bool) apply strengthening for existential quantifica‐
944                        tion over datatypes based on structural induction
945
946              dt-var-exp-quant
947                        (bool) expand datatype variables bound to one con‐
948                        structor in quantifiers
949
950              e-matching
951                        (bool) whether to do heuristic E-matching
952
953              elim-ext-arith-quant
954                        (bool) eliminate extended arithmetic symbols in quan‐
955                        tified formulas
956
957              elim-taut-quant
958                        (bool) eliminate tautological disjuncts of quantified
959                        formulas
960
961              finite-model-find
962                        (bool) use finite model finding heuristic for quanti‐
963                        fier instantiation
964
965              fmf-bound (bool) finite model finding on bounded quantification
966
967              fmf-bound-int
968                        (bool) finite model finding on bounded integer quan‐
969                        tification
970
971              fmf-bound-lazy
972                        (bool) enforce bounds for bounded quantification
973                        lazily via use of proxy variables
974
975              fmf-bound-min-mode
976                        (CVC4::theory::quantifiers::FmfBoundMinMode) mode for
977                        which types of bounds to minimize via first decision
978                        heuristics
979
980              fmf-empty-sorts
981                        (bool) allow finite model finding to assume sorts that
982                        do not occur in ground assertions are empty
983
984              fmf-fmc-simple
985                        (bool) simple models in full model check for finite
986                        model finding
987
988              fmf-fresh-dc
989                        (bool) use fresh distinguished representative when
990                        applying Inst-Gen techniques
991
992              fmf-fun   (bool) find models for recursively defined functions,
993                        assumes functions are admissible
994
995              fmf-fun-rlv
996                        (bool) find models for recursively defined functions,
997                        assumes functions are admissible, allows empty type
998                        when function is irrelevant
999
1000              fmf-inst-engine
1001                        (bool) use instantiation engine in conjunction with
1002                        finite model finding
1003
1004              fmf-inst-gen
1005                        (bool) enable Inst-Gen instantiation techniques for
1006                        finite model finding
1007
1008              fmf-inst-gen-one-quant-per-round
1009                        (bool) only perform Inst-Gen instantiation techniques
1010                        on one quantifier per round
1011
1012              fs-interleave
1013                        (bool) interleave full saturate instantiation with
1014                        other techniques
1015
1016              full-saturate-quant
1017                        (bool) when all other quantifier instantiation strate‐
1018                        gies fail, instantiate with ground terms from relevant
1019                        domain, then arbitrary ground terms before answering
1020                        unknown
1021
1022              full-saturate-quant-rd
1023                        (bool) whether to use relevant domain first for full
1024                        saturation instantiation strategy
1025
1026              global-negate
1027                        (bool) do global negation of input formula
1028
1029              ho-matching
1030                        (bool) do higher-order matching algorithm for triggers
1031                        with variable operators
1032
1033              ho-matching-var-priority
1034                        (bool) give priority to variable arguments over con‐
1035                        stant arguments
1036
1037              ho-merge-term-db
1038                        (bool) merge term indices modulo equality
1039
1040              increment-triggers
1041                        (bool) generate additional triggers as needed during
1042                        search
1043
1044              infer-arith-trigger-eq
1045                        (bool) infer equalities for trigger terms based on
1046                        solving arithmetic equalities
1047
1048              infer-arith-trigger-eq-exp
1049                        (bool) record explanations for inferArithTriggerEq
1050
1051              inst-level-input-only
1052                        (bool) only input terms are assigned instantiation
1053                        level zero
1054
1055              inst-max-level
1056                        (int) maximum inst level of terms used to instantiate
1057                        quantified formulas with (-1 == no limit, default)
1058
1059              inst-no-entail
1060                        (bool) do not consider instances of quantified formu‐
1061                        las that are currently entailed
1062
1063              inst-no-model-true
1064                        (bool) do not consider instances of quantified formu‐
1065                        las that are currently true in model, if it is avail‐
1066                        able
1067
1068              inst-prop (bool) internal propagation for instantiations for
1069                        selecting relevant instances
1070
1071              inst-when-phase
1072                        (int) instantiation rounds quantifiers takes (>=1)
1073                        before allowing theory combination to happen
1074
1075              inst-when-strict-interleave
1076                        (bool) ensure theory combination and standard quanti‐
1077                        fier effort strategies take turns
1078
1079              inst-when-tc-first
1080                        (bool) allow theory combination to happen once ini‐
1081                        tially, before quantifier strategies are run
1082
1083              inst-when (CVC4::theory::quantifiers::InstWhenMode) when to
1084                        apply instantiation
1085
1086              int-wf-ind
1087                        (bool) apply strengthening for integers based on
1088                        well-founded induction
1089
1090              ite-dtt-split-quant
1091                        (bool) split ites with dt testers as conditions
1092
1093              ite-lift-quant
1094                        (CVC4::theory::quantifiers::IteLiftQuantMode) ite
1095                        lifting mode for quantified formulas
1096
1097              literal-matching
1098                        (CVC4::theory::quantifiers::LiteralMatchMode) choose
1099                        literal matching mode
1100
1101              local-t-ext
1102                        (bool) do instantiation based on local theory exten‐
1103                        sions
1104
1105              lte-partial-inst
1106                        (bool) partially instantiate local theory quantifiers
1107
1108              lte-restrict-inst-closure
1109                        (bool) treat arguments of inst closure as restricted
1110                        terms for instantiation
1111
1112              macros-quant
1113                        (bool) perform quantifiers macro expansion
1114
1115              macros-quant-mode
1116                        (CVC4::theory::quantifiers::MacrosQuantMode) mode for
1117                        quantifiers macro expansion
1118
1119              mbqi-interleave
1120                        (bool) interleave model-based quantifier instantiation
1121                        with other techniques
1122
1123              mbqi-one-inst-per-round
1124                        (bool) only add one instantiation per quantifier per
1125                        round for mbqi
1126
1127              mbqi-one-quant-per-round
1128                        (bool) only add instantiations for one quantifier per
1129                        round for mbqi
1130
1131              mbqi      (CVC4::theory::quantifiers::MbqiMode) choose mode for
1132                        model-based quantifier instantiation
1133
1134              miniscope-quant
1135                        (bool) miniscope quantifiers
1136
1137              miniscope-quant-fv
1138                        (bool) miniscope quantifiers for ground subformulas
1139
1140              multi-trigger-cache
1141                        (bool) caching version of multi triggers
1142
1143              multi-trigger-linear
1144                        (bool) implementation of multi triggers where maximum
1145                        number of instantiations is linear wrt number of
1146                        ground terms
1147
1148              multi-trigger-priority
1149                        (bool) only try multi triggers if single triggers give
1150                        no instantiations
1151
1152              multi-trigger-when-single
1153                        (bool) select multi triggers when single triggers
1154                        exist
1155
1156              partial-triggers
1157                        (bool) use triggers that do not contain all free vari‐
1158                        ables
1159
1160              pre-skolem-quant
1161                        (bool) apply skolemization eagerly to bodies of quan‐
1162                        tified formulas
1163
1164              pre-skolem-quant-agg
1165                        (bool) apply skolemization to quantified formulas
1166                        aggressively
1167
1168              pre-skolem-quant-nested
1169                        (bool) apply skolemization to nested quantified formu‐
1170                        las
1171
1172              prenex-quant-user
1173                        (bool) prenex quantified formulas with user patterns
1174
1175              prenex-quant
1176                        (CVC4::theory::quantifiers::PrenexQuantMode) prenex
1177                        mode for quantified formulas
1178
1179              pure-th-triggers
1180                        (bool) use pure theory terms as single triggers
1181
1182              purify-dt-triggers
1183                        (bool) purify dt triggers, match all constructors of
1184                        correct form instead of selectors
1185
1186              purify-triggers
1187                        (bool) purify triggers, e.g. f( x+1 ) becomes f( y ),
1188                        x mapsto y-1
1189
1190              qcf-all-conflict
1191                        (bool) add all available conflicting instances during
1192                        conflict-based instantiation
1193
1194              qcf-eager-check-rd
1195                        (bool) optimization, eagerly check relevant domain of
1196                        matched position
1197
1198              qcf-eager-test
1199                        (bool) optimization, test qcf instances eagerly
1200
1201              qcf-nested-conflict
1202                        (bool) consider conflicts for nested quantifiers
1203
1204              qcf-skip-rd
1205                        (bool) optimization, skip instances based on possibly
1206                        irrelevant portions of quantified formulas
1207
1208              qcf-tconstraint
1209                        (bool) enable entailment checks for t-constraints in
1210                        qcf algorithm
1211
1212              qcf-vo-exp
1213                        (bool) qcf experimental variable ordering
1214
1215              quant-alpha-equiv
1216                        (bool) infer alpha equivalence between quantified for‐
1217                        mulas
1218
1219              quant-anti-skolem
1220                        (bool) perform anti-skolemization for quantified for‐
1221                        mulas
1222
1223              quant-cf  (bool) enable conflict find mechanism for quantifiers
1224
1225              quant-cf-mode
1226                        (CVC4::theory::quantifiers::QcfMode) what effort to
1227                        apply conflict find mechanism
1228
1229              quant-cf-when
1230                        (CVC4::theory::quantifiers::QcfWhenMode) when to
1231                        invoke conflict find mechanism for quantifiers
1232
1233              quant-dsplit-mode
1234                        (CVC4::theory::quantifiers::QuantDSplitMode) mode for
1235                        dynamic quantifiers splitting
1236
1237              quant-epr (bool) infer whether in effectively propositional
1238                        fragment, use for cbqi
1239
1240              quant-epr-match
1241                        (bool) use matching heuristics for EPR instantiation
1242
1243              quant-fun-wd
1244                        (bool) assume that function defined by quantifiers are
1245                        well defined
1246
1247              quant-ind (bool) use all available techniques for inductive rea‐
1248                        soning
1249
1250              quant-model-ee
1251                        (bool) use equality engine of model for last call
1252                        effort
1253
1254              quant-rep-mode
1255                        (CVC4::theory::quantifiers::QuantRepMode) selection
1256                        mode for representatives in quantifiers engine
1257
1258              quant-split
1259                        (bool) apply splitting to quantified formulas based on
1260                        variable disjoint disjuncts
1261
1262              register-quant-body-terms
1263                        (bool) consider ground terms within bodies of quanti‐
1264                        fied formulas for matching
1265
1266              relational-triggers
1267                        (bool) choose relational triggers such as x = f(y), x
1268                        >= f(y)
1269
1270              relevant-triggers
1271                        (bool) prefer triggers that are more relevant based on
1272                        SInE style analysis
1273
1274              rewrite-rules
1275                        (bool) use rewrite rules module
1276
1277              rr-one-inst-per-round
1278                        (bool) add one instance of rewrite rule per round
1279
1280              strict-triggers
1281                        (bool) only instantiate quantifiers with user patterns
1282                        based on triggers
1283
1284              sygus-add-const-grammar
1285                        (bool) statically add constants appearing in conjec‐
1286                        ture to grammars
1287
1288              sygus-auto-unfold
1289                        (bool) enable approach which automatically unfolds
1290                        transition systems for directly solving invariant syn‐
1291                        thesis problems
1292
1293              sygus-bool-ite-return-const
1294                        (bool) Only use Boolean constants for return values in
1295                        unification-based function synthesis
1296
1297              sygus-eval-unfold
1298                        (bool) do unfolding of sygus evaluation functions
1299
1300              sygus-eval-unfold-bool
1301                        (bool) do unfolding of Boolean evaluation functions
1302                        that appear in refinement lemmas
1303
1304              sygus-ext-rew
1305                        (bool) use extended rewriter for sygus
1306
1307              sygus-grammar-norm
1308                        (bool) statically normalize sygus grammars based on
1309                        flattening (linearization)
1310
1311              sygus-inference
1312                        (bool) attempt to preprocess arbitrary inputs to sygus
1313                        conjectures
1314
1315              sygus-inv-templ-when-sg
1316                        (bool) use invariant templates (with solution recon‐
1317                        struction) for syntax guided problems
1318
1319              sygus-inv-templ
1320                        (CVC4::theory::quantifiers::SygusInvTemplMode) tem‐
1321                        plate mode for sygus invariant synthesis (weaken
1322                        pre-condition, strengthen post-condition, or none)
1323
1324              sygus-min-grammar
1325                        (bool) statically minimize sygus grammars
1326
1327              sygus-pbe (bool) enable approach which unifies conditional solu‐
1328                        tions, specialized for programming-by-examples (pbe)
1329                        conjectures
1330
1331              sygus-qe-preproc
1332                        (bool) use quantifier elimination as a preprocessing
1333                        step for sygus
1334
1335              sygus-ref-eval
1336                        (bool) direct evaluation of refinement lemmas for con‐
1337                        flict analysis
1338
1339              sygus-repair-const
1340                        (bool) use approach to repair constants in sygus can‐
1341                        didate solutions
1342
1343              sygus-rr  (bool) use sygus to enumerate and verify correctness
1344                        of rewrite rules via sampling
1345
1346              sygus-rr-synth
1347                        (bool) use sygus to enumerate candidate rewrite rules
1348                        via sampling
1349
1350              sygus-rr-synth-accel
1351                        (bool) add dynamic symmetry breaking clauses based on
1352                        candidate rewrites
1353
1354              sygus-rr-synth-check
1355                        (bool) use satisfiability check to verify correctness
1356                        of candidate rewrites
1357
1358              sygus-rr-synth-filter-cong
1359                        (bool) filter candidate rewrites based on congruence
1360
1361              sygus-rr-synth-filter-match
1362                        (bool) filter candidate rewrites based on matching
1363
1364              sygus-rr-synth-filter-order
1365                        (bool) filter candidate rewrites based on variable
1366                        ordering
1367
1368              sygus-rr-verify
1369                        (bool) use sygus to verify the correctness of rewrite
1370                        rules via sampling
1371
1372              sygus-rr-verify-abort
1373                        (bool) abort when sygus-rr-verify finds an instance of
1374                        unsoundness
1375
1376              sygus-sample-grammar
1377                        (bool) when applicable, use grammar for choosing sam‐
1378                        ple points
1379
1380              sygus-samples
1381                        (int) number of points to consider when doing sygus
1382                        rewriter sample testing
1383
1384              sygus-stream
1385                        (bool) enumerate a stream of solutions instead of ter‐
1386                        minating after the first one
1387
1388              sygus-templ-embed-grammar
1389                        (bool) embed sygus templates into grammars
1390
1391              sygus-unif
1392                        (bool) Unification-based function synthesis
1393
1394              term-db-mode
1395                        (CVC4::theory::quantifiers::TermDbMode) which ground
1396                        terms to consider for instantiation
1397
1398              track-inst-lemmas
1399                        (bool) track instantiation lemmas (for proofs, unsat
1400                        cores, qe and synthesis minimization)
1401
1402              trigger-active-sel
1403                        (CVC4::theory::quantifiers::TriggerActiveSelMode)
1404                        selection mode to activate triggers
1405
1406              trigger-sel
1407                        (CVC4::theory::quantifiers::TriggerSelMode) selection
1408                        mode for triggers
1409
1410              user-pat  (CVC4::theory::quantifiers::UserPatMode) policy for
1411                        handling user-provided patterns for quantifier instan‐
1412                        tiation
1413
1414              var-elim-quant
1415                        (bool) enable simple variable elimination for quanti‐
1416                        fied formulas
1417
1418              var-ineq-elim-quant
1419                        (bool) enable variable elimination based on infinite
1420                        projection of unbound arithmetic variables
1421
1422              SEP OPTIONS
1423
1424              sep-check-neg
1425                        (bool) check negated spatial assertions
1426
1427              sep-child-refine
1428                        (bool) child-specific refinements of negated star,
1429                        positive wand
1430
1431              sep-deq-c (bool) assume cardinality elements are distinct
1432
1433              sep-exp   (bool) experimental flag for sep
1434
1435              sep-min-refine
1436                        (bool) only add refinement lemmas for minimal (inner‐
1437                        most) assertions
1438
1439              sep-pre-skolem-emp
1440                        (bool) eliminate emp constraint at preprocess time
1441
1442              SETS OPTIONS
1443
1444              sets-ext  (bool) enable extended symbols such as complement and
1445                        universe in theory of sets
1446
1447              sets-infer-as-lemmas
1448                        (bool) send inferences as lemmas
1449
1450              sets-proxy-lemmas
1451                        (bool) introduce proxy variables eagerly to shorten
1452                        lemmas
1453
1454              sets-rel-eager
1455                        (bool) standard effort checks for relations
1456
1457              SMT LAYER OPTIONS
1458
1459              abstract-values
1460                        (bool) in models, output arrays (and in future, maybe
1461                        others) using abstract values, as required by the
1462                        SMT-LIB standard
1463
1464              bitblast-step
1465                        (unsigned) amount of resources spent for each bitblast
1466                        step (EXPERTS only)
1467
1468              bv-sat-conflict-step
1469                        (unsigned) amount of resources spent for each sat con‐
1470                        flict (bitvectors) (EXPERTS only)
1471
1472              check-models
1473                        (bool) after SAT/INVALID/UNKNOWN, check that the gen‐
1474                        erated model satisfies user assertions
1475
1476              check-proofs
1477                        (bool) after UNSAT/VALID, machine-check the generated
1478                        proof
1479
1480              check-synth-sol
1481                        (bool) checks whether produced solutions to func‐
1482                        tions-to-synthesize satisfy the conjecture
1483
1484              check-unsat-cores
1485                        (bool) after UNSAT/VALID, produce and check an unsat
1486                        core (expensive)
1487
1488              cnf-step  (unsigned) amount of resources spent for each call to
1489                        cnf conversion (EXPERTS only)
1490
1491              decision-step
1492                        (unsigned) amount of getNext decision calls in the
1493                        decision engine (EXPERTS only)
1494
1495              diagnostic-output-channel
1496                        (std::string) set the diagnostic output channel of the
1497                        solver
1498
1499              dump-instantiations
1500                        (bool) output instantiations of quantified formulas
1501                        after every UNSAT/VALID response
1502
1503              dump-models
1504                        (bool) output models after every SAT/INVALID/UNKNOWN
1505                        response
1506
1507              dump-proofs
1508                        (bool) output proofs after every UNSAT/VALID response
1509
1510              dump-synth
1511                        (bool) output solution for synthesis conjectures after
1512                        every UNSAT/VALID response
1513
1514              dump-unsat-cores
1515                        (bool) output unsat cores after every UNSAT/VALID
1516                        response
1517
1518              dump-unsat-cores-full
1519                        (bool) dump the full unsat core, including unlabeled
1520                        assertions
1521
1522              expand-definitions
1523                        (bool) always expand symbol definitions in output
1524
1525              ext-rew-prep
1526                        (bool) use extended rewriter as a preprocessing pass
1527
1528              ext-rew-prep-agg
1529                        (bool) use aggressive extended rewriter as a prepro‐
1530                        cessing pass
1531
1532              force-logic
1533                        (std::string) set the logic, and override all further
1534                        user attempts to change it (EXPERTS only)
1535
1536              force-no-limit-cpu-while-dump
1537                        (bool) Force no CPU limit when dumping models and
1538                        proofs
1539
1540              interactive-mode
1541                        (bool) deprecated name for produce-assertions
1542
1543              ite-simp  (bool) turn on ite simplification (Kim (and Somenzi)
1544                        et al., SAT 2009)
1545
1546              lemma-step
1547                        (unsigned) amount of resources spent when adding lem‐
1548                        mas (EXPERTS only)
1549
1550              model-u-dt-enum
1551                        (bool) in models, output uninterpreted sorts as
1552                        datatype enumerations
1553
1554              omit-dont-cares
1555                        (bool) When producing a model, omit variables whose
1556                        value does not matter
1557
1558              on-repeat-ite-simp
1559                        (bool) do the ite simplification pass again if repeat‐
1560                        ing simplification
1561
1562              parse-step
1563                        (unsigned) amount of resources spent for each com‐
1564                        mand/expression parsing (EXPERTS only)
1565
1566              preprocess-step
1567                        (unsigned) amount of resources spent for each prepro‐
1568                        cessing step in SmtEngine (EXPERTS only)
1569
1570              produce-assignments
1571                        (bool) support the get-assignment command
1572
1573              produce-unsat-assumptions
1574                        (bool) turn on unsat assumptions generation
1575
1576              produce-unsat-cores
1577                        (bool) turn on unsat core generation
1578
1579              produce-proofs
1580                        (bool) turn on proof generation
1581
1582              quantifier-step
1583                        (unsigned) amount of resources spent for quantifier
1584                        instantiations (EXPERTS only)
1585
1586              regular-output-channel
1587                        (std::string) set the regular output channel of the
1588                        solver
1589
1590              repeat-simp
1591                        (bool) make multiple passes with nonclausal simplifier
1592
1593              replay-log
1594                        (std::string) replay decisions from file
1595
1596              replay    (std::string) replay decisions from file
1597
1598              restart-step
1599                        (unsigned) amount of resources spent for each theory
1600                        restart (EXPERTS only)
1601
1602              rewrite-apply-to-const
1603                        (bool) eliminate function applications, rewriting e.g.
1604                        f(5) to a new symbol f_5 (EXPERTS only)
1605
1606              rewrite-step
1607                        (unsigned) amount of resources spent for each rewrite
1608                        step (EXPERTS only)
1609
1610              sat-conflict-step
1611                        (unsigned) amount of resources spent for each sat con‐
1612                        flict (main sat solver) (EXPERTS only)
1613
1614              simp-ite-compress
1615                        (bool) enables compressing ites after ite simplifica‐
1616                        tion
1617
1618              simp-ite-hunt-zombies
1619                        (uint32_t) post ite compression enables zombie removal
1620                        while the number of nodes is above this threshold
1621
1622              simp-with-care
1623                        (bool) enables simplifyWithCare in ite simplificiation
1624
1625              simplification-mode
1626                        (SimplificationMode) choose simplification mode, see
1627                        --simplification=help
1628
1629              solve-int-as-bv
1630                        (uint32_t) attempt to solve a pure integer satisfiable
1631                        problem by bitblasting in sufficient bitwidth (experi‐
1632                        mental)
1633
1634              solve-real-as-int
1635                        (bool) attempt to solve a pure real satisfiable prob‐
1636                        lem as an integer problem (for non-linear)
1637
1638              sort-inference
1639                        (bool) calculate sort inference of input problem, con‐
1640                        vert the input based on monotonic sorts
1641
1642              static-learning
1643                        (bool) use static learning (on by default)
1644
1645              sygus-out (SygusSolutionOutMode) output mode for sygus
1646
1647              sygus-print-callbacks
1648                        (bool) use sygus print callbacks to print sygus terms
1649                        in the user-provided form (disable for debugging)
1650
1651              symmetry-breaker-exp
1652                        (bool) generate symmetry breaking constraints after
1653                        symmetry detection
1654
1655              theory-check-step
1656                        (unsigned) amount of resources spent for each theory
1657                        check call (EXPERTS only)
1658
1659              unconstrained-simp
1660                        (bool) turn on unconstrained simplification (see Brut‐
1661                        tomesso/Brummayer PhD thesis)
1662
1663              no-simplification
1664                        turn off all simplification (same as --simplifica‐
1665                        tion=none)
1666
1667              STRINGS THEORY OPTIONS
1668
1669              strings-abort-loop
1670                        (bool) abort when a looping word equation is encoun‐
1671                        tered
1672
1673              strings-binary-csp
1674                        (bool) use binary search when splitting strings
1675
1676              strings-check-entail-len
1677                        (bool) check entailment between length terms to reduce
1678                        splitting
1679
1680              strings-eager
1681                        (bool) strings eager check
1682
1683              strings-eager-len
1684                        (bool) strings eager length lemmas
1685
1686              strings-eit
1687                        (bool) the eager intersection used by the theory of
1688                        strings
1689
1690              strings-exp
1691                        (bool) experimental features in the theory of strings
1692
1693              strings-fmf
1694                        (bool) the finite model finding used by the theory of
1695                        strings
1696
1697              strings-guess-model
1698                        (bool) use model guessing to avoid string extended
1699                        function reductions
1700
1701              strings-infer-as-lemmas
1702                        (bool) always send lemmas out instead of making inter‐
1703                        nal inferences
1704
1705              strings-infer-sym
1706                        (bool) strings split on empty string
1707
1708              strings-inm
1709                        (bool) internal for strings: ignore negative member‐
1710                        ship constraints (fragment checking is needed, left to
1711                        users for now)
1712
1713              strings-lazy-pp
1714                        (bool) perform string preprocessing lazily
1715
1716              strings-lb
1717                        (unsigned) the strategy of LB rule application:
1718                        0-lazy, 1-eager, 2-no
1719
1720              strings-len-geqz
1721                        (bool) strings length greater than zero lemmas
1722
1723              strings-len-norm
1724                        (bool) strings length normalization lemma
1725
1726              strings-lprop-csp
1727                        (bool) do length propagation based on constant splits
1728
1729              strings-min-prefix-explain
1730                        (bool) minimize explanations for prefix of normal
1731                        forms in strings
1732
1733              strings-opt1
1734                        (bool) internal option1 for strings: normal form
1735
1736              strings-opt2
1737                        (bool) internal option2 for strings: constant regexp
1738                        splitting
1739
1740              strings-print-ascii
1741                        (bool) the alphabet contains only printable characters
1742                        from the standard extended ASCII
1743
1744              strings-process-loop
1745                        (bool) reduce looping word equations to regular
1746                        expressions
1747
1748              strings-rexplain-lemmas
1749                        (bool) regression explanations for string lemmas
1750
1751              strings-sp-emp
1752                        (bool) strings split on empty string
1753
1754              strings-uf-reduct
1755                        (bool) use uninterpreted functions when applying
1756                        extended function reductions
1757
1758              THEORY LAYER OPTIONS
1759
1760              assign-function-values
1761                        (bool) assign values for uninterpreted functions in
1762                        models
1763
1764              condense-function-values
1765                        (bool) condense values for functions in models rather
1766                        than explicitly representing them
1767
1768              theoryof-mode
1769                        (CVC4::theory::TheoryOfMode) mode for Theory::theo‐
1770                        ryof() (EXPERTS only)
1771
1772              use-theory
1773                        (std::string) use alternate theory implementation NAME
1774                        (--use-theory=help for a list). This option may be
1775                        repeated or a comma separated list.
1776
1777              UNINTERPRETED FUNCTIONS THEORY OPTIONS
1778
1779              uf-symmetry-breaker
1780                        (bool) use UF symmetry breaker (Deharbe et al., CADE
1781                        2011)
1782
1783              uf-ho     (bool) enable support for higher-order reasoning
1784
1785              uf-ho-ext (bool) apply extensionality on function symbols
1786
1787              uf-ss-abort-card
1788                        (int) tells the uf strong solver to only consider mod‐
1789                        els that interpret uninterpreted sorts of cardinality
1790                        at most N (-1 == no limit, default)
1791
1792              uf-ss-clique-splits
1793                        (bool) use cliques instead of splitting on demand to
1794                        shrink model
1795
1796              uf-ss-eager-split
1797                        (bool) add splits eagerly for uf strong solver
1798
1799              uf-ss-fair
1800                        (bool) use fair strategy for finite model finding mul‐
1801                        tiple sorts
1802
1803              uf-ss-fair-monotone
1804                        (bool) group monotone sorts when enforcing fairness
1805                        for finite model finding
1806
1807              uf-ss-regions
1808                        (bool) disable region-based method for discovering
1809                        cliques and splits in uf strong solver
1810
1811              uf-ss-totality
1812                        (bool) always use totality axioms for enforcing cardi‐
1813                        nality constraints
1814
1815              uf-ss-totality-limited
1816                        (int) apply totality axioms, but only up to cardinal‐
1817                        ity N (-1 == do not apply totality axioms, default)
1818
1819              uf-ss-totality-sym-break
1820                        (bool) apply symmetry breaking for totality axioms
1821
1822              uf-ss     (CVC4::theory::uf::UfssMode) mode of operation for uf
1823                        strong solver.
1824
1825
1826

VERSION

1828       This manual page refers to CVC4 version 1.6.
1829

BUGS

1831       An  issue   tracker   for   the   CVC4   project   is   maintained   at
1832       https://github.com/CVC4/CVC4/issues.
1833

AUTHORS

1835       CVC4  is  developed by a team of researchers at Stanford University and
1836       the University of Iowa.  See the AUTHORS file in the distribution for a
1837       full list of contributors.
1838

SEE ALSO

1840       libcvc4(3), libcvc4parser(3), libcvc4compat(3)
1841
1842       Additionally,  the  CVC4  wiki  contains  useful  information about the
1843       design and internals of CVC4.  It is maintained at http://cvc4.cs.stan
1844       ford.edu/wiki/.
1845
1846
1847
1848CVC4 release 1.6                 February 2019                 SMTENGINE(3cvc)
Impressum