1CVC4(1)                          User Manuals                          CVC4(1)
2
3
4

NAME

6       cvc4, pcvc4 - an automated theorem prover
7

SYNOPSIS

9       cvc4 [ options ] [ file ]
10
11       pcvc4 [ options ] [ file ]
12

DESCRIPTION

14       cvc4  is  an  automated  theorem  prover  for first-order formulas with
15       respect to background theories of interest.  pcvc4 is  CVC4's  "portfo‐
16       lio"  variant,  which  is capable of running multiple CVC4 instances in
17       parallel, configured differently.
18
19       With file , commands are read from file and  executed.   CVC4  supports
20       the  SMT-LIB  (versions  1.2  and 2.0) input format, as well as its own
21       native “presentation language” (see cvc4(5) ), which is similar in many
22       respects to CVC3's presentation language, but not identical.
23
24       If  file is unspecified, standard input is read (and the CVC4 presenta‐
25       tion language is assumed).  If file is unspecified  and  CVC4  is  con‐
26       nected to a terminal, interactive mode is assumed.
27
28

COMMON OPTIONS

30       Each  option  marked  with  [*]  has  a  --no-OPTIONNAME variant, which
31       reverses the sense of the option.
32
33
34       --lang=LANG | -L LANG
35              force input language (default is "auto"; see --lang help)
36
37       --output-lang=LANG
38              force output language  (default  is  "auto";  see  --output-lang
39              help)
40
41       --quiet | -q
42              decrease verbosity (may be repeated)
43
44       --stats
45              give statistics on exit [*]
46
47       --verbose | -v
48              increase verbosity (may be repeated)
49
50       --copyright
51              show CVC4 copyright information
52
53       --help | -h
54              full command line reference
55
56       --seed | -s
57              seed for random number generator
58
59       --show-config
60              show CVC4 static configuration
61
62       --version | -V
63              identify this CVC4 binary
64
65       --strict-parsing
66              be less tolerant of non-conforming inputs [*]
67
68       --cpu-time
69              measures CPU time if set to true and wall time if false (default
70              false) [*]
71
72       --dump-to=FILE
73              all dumping goes to FILE (instead of stdout)
74
75       --dump=MODE
76              dump preprocessed assertions, etc., see --dump=help
77
78       --hard-limit
79              the resource limit is hard potentially leaving the smtEngine  in
80              an  unsafe state (should be destroyed and rebuild after resourc‐
81              ing out) [*]
82
83       --incremental | -i
84              enable incremental solving [*]
85
86       --produce-assertions
87              keep an assertions list (enables get-assertions command) [*]
88
89       --produce-models | -m
90              support the get-value and get-model commands [*]
91
92       --rlimit-per=N
93              enable resource limiting per query
94
95       --rlimit=N
96              enable resource limiting (currently, roughly the number  of  SAT
97              conflicts)
98
99       --tlimit-per=MS
100              enable time limiting per query (give milliseconds)
101
102       --tlimit=MS
103              enable time limiting (give milliseconds)
104
105

ARITHMETIC THEORY OPTIONS

107       --approx-branch-depth
108              maximum branch depth the approximate solver is allowed to take
109
110       --arith-no-partial-fun
111              do  not  use  partial function semantics for arithmetic (not SMT
112              LIB compliant) [*]
113
114       --arith-prop-clauses
115              rows shorter than this are propagated as clauses
116
117       --arith-prop=MODE
118              turns  on  arithmetic  propagation  (default   is   'old',   see
119              --arith-prop=help)
120
121       --arith-rewrite-equalities
122              turns  on  the  preprocessing  rewrite turning equalities into a
123              conjunction of inequalities [*]
124
125       --collect-pivot-stats
126              collect the pivot history [*]
127
128       --cut-all-bounded
129              turns on the integer solving step of  periodically  cutting  all
130              integer variables that have both upper and lower bounds [*]
131
132       --dio-decomps
133              let  skolem  variables for integer divisibility constraints leak
134              from the dio solver [*]
135
136       --dio-repeat
137              handle dio solver constraints in mass or one at a time [*]
138
139       --dio-solver
140              turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)
141              [*]
142
143       --dio-turns
144              turns in a row dio solver cutting gets
145
146       --error-selection-rule=RULE
147              change  the pivot rule for the basic variable (default is 'min',
148              see --pivot-rule help)
149
150       --fc-penalties
151              turns on degenerate pivot penalties [*]
152
153       --heuristic-pivots=N
154              the number of times to apply the heuristic pivot rule; if N < 0,
155              this defaults to the number of variables; if this is unset, this
156              is tuned by the logic selection
157
158       --lemmas-on-replay-failure
159              attempt to use external  lemmas  if  approximate  solve  integer
160              failed [*]
161
162       --maxCutsInContext
163              maximum cuts in a given context before signalling a restart
164
165       --miplib-trick
166              turns on the preprocessing step of attempting to infer bounds on
167              miplib problems [*]
168
169       --miplib-trick-subs=N
170              do substitution for miplib 'tmp' vars if defined in <= N  elimi‐
171              nated vars
172
173       --new-prop
174              use the new row propagation system [*]
175
176       --nl-ext
177              extended approach to non-linear [*]
178
179       --nl-ext-ent-conf
180              check for entailed conflicts in non-linear solver [*]
181
182       --nl-ext-factor
183              use factoring inference in non-linear solver [*]
184
185       --nl-ext-inc-prec
186              whether  to increment the precision for irrational function con‐
187              straints [*]
188
189       --nl-ext-purify
190              purify non-linear terms at preprocess [*]
191
192       --nl-ext-rbound
193              use resolution-style inference for inferring new bounds [*]
194
195       --nl-ext-rewrite
196              do rewrites in non-linear solver [*]
197
198       --nl-ext-split-zero
199              intial splits on zero for all variables [*]
200
201       --nl-ext-tf-taylor-deg=N
202              initial degree of polynomials for Taylor approximation
203
204       --nl-ext-tf-tplanes
205              use non-terminating tangent plane  strategy  for  transcendental
206              functions for non-linear [*]
207
208       --nl-ext-tplanes
209              use non-terminating tangent plane strategy for non-linear [*]
210
211       --nl-ext-tplanes-interleave
212              interleave tangent plane strategy for non-linear [*]
213
214       --pb-rewrites
215              apply pseudo boolean rewrites [*]
216
217       --pivot-threshold=N
218              sets  the number of pivots using --pivot-rule per basic variable
219              per simplex instance before using variable order
220
221       --pp-assert-max-sub-size
222              threshold for substituting an equality in ppAssert
223
224       --prop-row-length=N
225              sets the maximum row length to be used in propagation
226
227       --replay-early-close-depth
228              multiples of the depths to try to close the approx log eagerly
229
230       --replay-failure-penalty
231              number of solve integer attempts to skips after a numeric  fail‐
232              ure
233
234       --replay-lemma-reject-cut
235              maximum complexity of any coefficient while outputting replaying
236              cut lemmas
237
238       --replay-num-err-penalty
239              number of solve integer attempts to skips after a numeric  fail‐
240              ure
241
242       --replay-reject-cut
243              maximum complexity of any coefficient while replaying cuts
244
245       --replay-soi-major-threshold
246              threshold  for  a  major  tolerance  failure  by the approximate
247              solver
248
249       --replay-soi-major-threshold-pen
250              threshold for a  major  tolerance  failure  by  the  approximate
251              solver
252
253       --replay-soi-minor-threshold
254              threshold  for  a  minor  tolerance  failure  by the approximate
255              solver
256
257       --replay-soi-minor-threshold-pen
258              threshold for a  minor  tolerance  failure  by  the  approximate
259              solver
260
261       --restrict-pivots
262              have  a  pivot cap for simplex at effort levels below fullEffort
263              [*]
264
265       --revert-arith-models-on-unsat
266              revert the arithmetic model to a known safe model  on  unsat  if
267              one is cached [*]
268
269       --rewrite-divk
270              rewrite  division  and  mod when by a constant into linear terms
271              [*]
272
273       --rr-turns
274              round robin turn
275
276       --se-solve-int
277              attempt to use the approximate solve integer method on  standard
278              effort [*]
279
280       --simplex-check-period=N
281              the  number  of  pivots to do in simplex before rechecking for a
282              conflict on all variables
283
284       --snorm-infer-eq
285              infer equalities based on Shostak normalization [*]
286
287       --soi-qe
288              use quick explain to minimize the sum of infeasibility conflicts
289              [*]
290
291       --standard-effort-variable-order-pivots=N
292              limits the number of pivots in a single invocation of check() at
293              a non-full effort level using Bland's pivot rule (EXPERTS only)
294
295       --unate-lemmas=MODE
296              determines which lemmas to add before solving (default is 'all',
297              see --unate-lemmas=help)
298
299       --use-approx
300              attempt to use an approximate solver [*]
301
302       --use-fcsimplex
303              use focusing and converging simplex (FMCAD 2013 submission) [*]
304
305       --use-soi
306              use sum of infeasibility simplex (FMCAD 2013 submission) [*]
307

ARRAYS THEORY OPTIONS

309       --arrays-config
310              set different array option configurations - for developers only
311
312       --arrays-eager-index
313              turn on eager index splitting for generated array lemmas [*]
314
315       --arrays-eager-lemmas
316              turn on eager lemma generation for arrays [*]
317
318       --arrays-lazy-rintro1
319              turn  on  optimization  to only perform RIntro1 rule lazily (see
320              Jovanovic/Barrett 2012: Being Careful with  Theory  Combination)
321              [*]
322
323       --arrays-model-based
324              turn on model-based array solver [*]
325
326       --arrays-optimize-linear
327              turn  on optimization for linear array terms (see de Moura FMCAD
328              09 arrays paper) [*]
329
330       --arrays-prop
331              propagation effort for arrays: 0 is none, 1 is some, 2 is full
332
333       --arrays-reduce-sharing
334              use model information to reduce size of care  graph  for  arrays
335              [*]
336
337       --arrays-weak-equiv
338              use algorithm from Christ/Hoenicke (SMT 2014) [*]
339

BASE OPTIONS

341       --debug=TAG | -d TAG
342              debug something (e.g. -d arith), can repeat
343
344       --parse-only
345              exit after parsing input [*]
346
347       --preprocess-only
348              exit after preprocessing input [*]
349
350       --print-success
351              print the "success" output required of SMT-LIBv2 [*]
352
353       --stats-every-query
354              in  incremental  mode, print stats after every satisfiability or
355              validity query [*]
356
357       --stats-hide-zeros
358              hide statistics which are zero [*]
359
360       --trace=TAG | -t TAG
361              trace something (e.g. -t pushpop), can repeat
362
363       --smtlib-strict
364              SMT-LIBv2 compliance mode (implies other options)
365

BITVECTOR THEORY OPTIONS

367       --bitblast-aig
368              bitblast by first converting to AIG  (implies  --bitblast=eager)
369              [*]
370
371       --bitblast=MODE
372              choose bitblasting mode, see --bitblast=help
373
374       --bool-to-bv
375              convert booleans to bit-vectors of size 1 when possible [*]
376
377       --bv-abstraction
378              mcm benchmark abstraction (EXPERTS only) [*]
379
380       --bv-aig-simp=COMMAND
381              abc  command to run AIG simplifications (implies --bitblast-aig,
382              default is "balance;drw") (EXPERTS only)
383
384       --bv-alg-extf
385              algebraic inferences for extended functions [*]
386
387       --bv-algebraic-budget
388              the budget allowed for the algebraic solver  in  number  of  SAT
389              conflicts (EXPERTS only)
390
391       --bv-algebraic-solver
392              turn  on the algebraic solver for the bit-vector theory (only if
393              --bitblast=lazy) [*]
394
395       --bv-div-zero-const
396              always return -1 on division by zero [*]
397
398       --bv-eager-explanations
399              compute bit-blasting propagation explanations  eagerly  (EXPERTS
400              only) [*]
401
402       --bv-eq-slicer=MODE
403              turn  on  the  slicing equality solver for the bit-vector theory
404              (only if --bitblast=lazy)
405
406       --bv-eq-solver
407              use the equality engine  for  the  bit-vector  theory  (only  if
408              --bitblast=lazy) [*]
409
410       --bv-extract-arith
411              enable  rewrite pushing extract [i:0] over arithmetic operations
412              (can blow up) (EXPERTS only) [*]
413
414       --bv-gauss-elim
415              simplify formula via Gaussian Elimination if applicable (EXPERTS
416              only) [*]
417
418       --bv-inequality-solver
419              turn on the inequality solver for the bit-vector theory (only if
420              --bitblast=lazy) [*]
421
422       --bv-intro-pow2
423              introduce bitvector  powers  of  two  as  a  preprocessing  pass
424              (EXPERTS only) [*]
425
426       --bv-lazy-reduce-extf
427              reduce  extended  functions  like bv2nat and int2bv at last call
428              instead of full effort [*]
429
430       --bv-lazy-rewrite-extf
431              lazily rewrite extended functions like bv2nat and int2bv [*]
432
433       --bv-num-func=NUM
434              number of function symbols in  conflicts  that  are  generalized
435              (EXPERTS only)
436
437       --bv-propagate
438              use bit-vector propagation in the bit-blaster [*]
439
440       --bv-quick-xplain
441              minimize  bv  conflicts using the QuickXplain algorithm (EXPERTS
442              only) [*]
443
444       --bv-sat-solver=MODE
445              choose  which  sat  solver  to  use,  see   --bv-sat-solver=help
446              (EXPERTS only)
447
448       --bv-skolemize
449              skolemize  arguments  for bv abstraction (only does something if
450              --bv-abstraction is on) (EXPERTS only) [*]
451
452       --bv-to-bool
453              lift bit-vectors of size 1 to booleans when possible [*]
454

DATATYPES THEORY OPTIONS

456       --cdt-bisimilar
457              do bisimilarity check for co-datatypes [*]
458
459       --dt-binary-split
460              do binary splits for datatype constructor types [*]
461
462       --dt-blast-splits
463              when applicable, blast splitting lemmas  for  all  variables  at
464              once [*]
465
466       --dt-cyclic
467              do cyclicity check for datatypes [*]
468
469       --dt-force-assignment
470              force  the  datatypes  solver  to  give  specific  values to all
471              datatypes terms before answering sat [*]
472
473       --dt-infer-as-lemmas
474              always send lemmas out instead of making internal inferences [*]
475
476       --dt-ref-sk-intro
477              introduce reference skolems for shorter explanations [*]
478
479       --dt-rewrite-error-sel
480              rewrite incorrectly applied selectors to arbitrary  ground  term
481              (EXPERTS only) [*]
482
483       --dt-share-sel
484              internally use shared selectors across multiple constructors [*]
485
486       --dt-use-testers
487              do not preprocess away tester predicates [*]
488
489       --sygus-abort-size=N
490              tells  enumerative  sygus  to only consider solutions up to term
491              size N (-1 == no limit, default)
492
493       --sygus-eval-builtin
494              use builtin kind for evaluation functions in sygus [*]
495
496       --sygus-fair-max
497              use max instead of sum for multi-function sygus conjectures [*]
498
499       --sygus-fair=MODE
500              if and how to apply fairness for sygus
501
502       --sygus-opt1
503              sygus experimental option [*]
504
505       --sygus-sym-break
506              simple sygus sym break lemmas [*]
507
508       --sygus-sym-break-dynamic
509              dynamic sygus sym break lemmas [*]
510
511       --sygus-sym-break-lazy
512              lazily add symmetry breaking lemmas for terms [*]
513
514       --sygus-sym-break-pbe
515              sygus sym break lemmas based on pbe conjectures [*]
516
517       --sygus-sym-break-rlv
518              add relevancy conditions to symmetry breaking lemmas [*]
519

DECISION HEURISTICS OPTIONS

521       --decision-random-weight=N
522              assign random weights to nodes between 0 and  N-1  (0:  disable)
523              (EXPERTS only)
524
525       --decision-threshold=N
526              ignore all nodes greater than threshold in first attempt to pick
527              decision (EXPERTS only)
528
529       --decision-use-weight
530              use the weight nodes (locally, by looking at children) to direct
531              recursive search (EXPERTS only) [*]
532
533       --decision-weight-internal=HOW
534              computer  weights  of  internal  nodes using children: off, max,
535              sum, usr1 (meaning evolving) (EXPERTS only)
536
537       --decision=MODE
538              choose decision mode, see --decision=help
539

EXPRESSION PACKAGE OPTIONS

541       --default-dag-thresh=N
542              dagify common subexprs appearing > N times (1 == default,  0  ==
543              don't dagify)
544
545       --default-expr-depth=N
546              print exprs to depth N (0 == default, -1 == no limit)
547
548       --eager-type-checking
549              type  check  expressions  immediately  on creation (debug builds
550              only) [*]
551
552       --print-expr-types
553              print types with variables when printing exprs [*]
554
555       --type-checking
556              never type check expressions
557

IDL OPTIONS

559       --idl-rewrite-equalities
560              enable rewriting equalities into two inequalities in IDL  solver
561              (default is disabled) [*]
562

DRIVER OPTIONS

564       --continued-execution
565              continue executing commands, even on error [*]
566
567       --early-exit
568              do  not  run  destructors  at  exit;  default on except in debug
569              builds (EXPERTS only) [*]
570
571       --fallback-sequential
572              Switch to sequential mode (instead of printing an error)  if  it
573              can't be solved in portfolio mode [*]
574
575       --filter-lemma-length=N
576              don't  share  (among  portfolio  threads) lemmas strictly longer
577              than N
578
579       --incremental-parallel
580              Use  parallel  solver  even  in  incremental  mode  (may   print
581              'unknown's at times) [*]
582
583       --interactive
584              force interactive/non-interactive mode [*]
585
586       --segv-spin
587              spin on segfault/other crash waiting for gdb [*]
588
589       --show-debug-tags
590              show all available tags for debugging
591
592       --show-trace-tags
593              show all available tags for tracing
594
595       --tear-down-incremental=N
596              implement  PUSH/POP/multi-query  by  destroying  and  recreating
597              SmtEngine every N queries (EXPERTS only)
598
599       --thread-stack=N
600              stack size for worker threads in MB (0  means  use  Boost/thread
601              lib default)
602
603       --threadN=string
604              configures portfolio thread N (0..#threads-1)
605
606       --threads=N
607              Total number of threads for portfolio
608
609       --wait-to-join
610              wait  for  other  threads to join before quitting (EXPERTS only)
611              [*]
612

PARSER OPTIONS

614       --mmap memory map file input [*]
615

PRINTING OPTIONS

617       --inst-format=MODE
618              print format mode for instantiations, see --inst-format=help
619
620       --model-format=MODE
621              print format mode for models, see --model-format=help
622

PROOF OPTIONS

624       --aggressive-core-min
625              turns on aggressive unsat core minimization (experimental) [*]
626
627       --allow-empty-dependencies
628              if unable to track the dependencies of a  rewritten/preprocessed
629              assertion, fail silently [*]
630
631       --fewer-preprocessing-holes
632              try to eliminate preprocessing holes in proofs [*]
633
634       --lfsc-letification
635              turns on global letification in LFSC proofs [*]
636

SAT LAYER OPTIONS

638       --minisat-dump-dimacs
639              instead  of solving minisat dumps the asserted clauses in Dimacs
640              format [*]
641
642       --minisat-elimination
643              use Minisat elimination [*]
644
645       --random-freq=P
646              sets the frequency of random decisions in the sat solver  (P=0.0
647              by default)
648
649       --random-seed=S
650              sets the random seed for the sat solver
651
652       --refine-conflicts
653              refine theory conflict clauses (default false) [*]
654
655       --restart-int-base=N
656              sets  the  base  restart  interval  for  the sat solver (N=25 by
657              default)
658
659       --restart-int-inc=F
660              sets the restart interval increase factor  for  the  sat  solver
661              (F=3.0 by default)
662

QUANTIFIERS OPTIONS

664       --ag-miniscope-quant
665              perform aggressive miniscoping for quantifiers [*]
666
667       --cbqi turns on counterexample-based quantifier instantiation [*]
668
669       --cbqi-all
670              apply  counterexample-based instantiation to all quantified for‐
671              mulas [*]
672
673       --cbqi-bv
674              use  word-level  inversion  approach  for  counterexample-guided
675              quantifier instantiation for bit-vectors [*]
676
677       --cbqi-bv-concat-inv
678              compute inverse for concat over equalities rather than producing
679              an invertibility condition [*]
680
681       --cbqi-bv-ineq=MODE
682              choose mode for handling bit-vector inequalities with counterex‐
683              ample-guided instantiation
684
685       --cbqi-bv-interleave-value
686              interleave  model  value instantiation with word-level inversion
687              approach [*]
688
689       --cbqi-bv-linear
690              linearize adder chains for variables [*]
691
692       --cbqi-bv-rm-extract
693              replaces extract terms with variables for  counterexample-guided
694              instantiation for bit-vectors [*]
695
696       --cbqi-bv-solve-nl
697              try  to  solve  non-linear bv literals using model value projec‐
698              tions [*]
699
700       --cbqi-full
701              turns on full effort counterexample-based quantifier  instantia‐
702              tion, which may resort to model-value instantiation [*]
703
704       --cbqi-innermost
705              only  process  innermost  quantified  formulas  in  counterexam‐
706              ple-based quantifier instantiation [*]
707
708       --cbqi-lit-dep
709              dependency lemmas for  quantifier  alternation  in  counterexam‐
710              ple-based quantifier instantiation [*]
711
712       --cbqi-midpoint
713              choose  substitutions  based  on  midpoints  of  lower and upper
714              bounds for counterexample-based quantifier instantiation [*]
715
716       --cbqi-min-bounds
717              use minimally constrained  lower/upper  bound  for  counterexam‐
718              ple-based quantifier instantiation [*]
719
720       --cbqi-model
721              guide  instantiations  by  model values for counterexample-based
722              quantifier instantiation [*]
723
724       --cbqi-multi-inst
725              when applicable, do  multi  instantiations  per  quantifier  per
726              round in counterexample-based quantifier instantiation [*]
727
728       --cbqi-nested-qe
729              process  nested  quantified formulas with quantifier elimination
730              in counterexample-based quantifier instantiation [*]
731
732       --cbqi-nopt
733              non-optimal bounds for counterexample-based quantifier instanti‐
734              ation [*]
735
736       --cbqi-prereg-inst
737              preregister  ground instantiations in counterexample-based quan‐
738              tifier instantiation [*]
739
740       --cbqi-recurse
741              turns on recursive counterexample-based quantifier instantiation
742              [*]
743
744       --cbqi-repeat-lit
745              solve literals more than once in counterexample-based quantifier
746              instantiation [*]
747
748       --cbqi-round-up-lia
749              round up integer lower bounds in substitutions for  counterexam‐
750              ple-based quantifier instantiation [*]
751
752       --cbqi-sat
753              answer  sat  when  quantifiers  are  asserted  with counterexam‐
754              ple-based quantifier instantiation [*]
755
756       --cbqi-use-inf-int
757              use integer infinity for vts in counterexample-based  quantifier
758              instantiation [*]
759
760       --cbqi-use-inf-real
761              use  real  infinity  for  vts in counterexample-based quantifier
762              instantiation [*]
763
764       --cegis-sample=MODE
765              mode for using samples in  the  counterexample-guided  inductive
766              synthesis loop
767
768       --cegqi
769              counterexample-guided quantifier instantiation for sygus [*]
770
771       --cegqi-si-abort
772              abort if synthesis conjecture is not single invocation [*]
773
774       --cegqi-si-partial
775              combined techniques for synthesis conjectures that are partially
776              single invocation [*]
777
778       --cegqi-si-reconstruct
779              reconstruct solutions for single invocation conjectures in orig‐
780              inal grammar [*]
781
782       --cegqi-si-reconstruct-const
783              include  constants when reconstruct solutions for single invoca‐
784              tion conjectures in original grammar [*]
785
786       --cegqi-si-sol-min-core
787              minimize solutions for single invocation  conjectures  based  on
788              unsat core [*]
789
790       --cegqi-si-sol-min-inst
791              minimize individual instantiations for single invocation conjec‐
792              tures based on unsat core [*]
793
794       --cegqi-si=MODE
795              mode for processing single invocation synthesis conjectures
796
797       --cond-rewrite-quant
798              conditional rewriting of quantified formulas [*]
799
800       --cond-var-split-agg-quant
801              aggressive split quantified formulas that lead to variable elim‐
802              inations [*]
803
804       --cond-var-split-quant
805              split quantified formulas that lead to variable eliminations [*]
806
807       --conjecture-filter-active-terms
808              filter based on active terms [*]
809
810       --conjecture-filter-canonical
811              filter based on canonicity [*]
812
813       --conjecture-filter-model
814              filter based on model [*]
815
816       --conjecture-gen
817              generate candidate conjectures for inductive proofs [*]
818
819       --conjecture-gen-gt-enum=N
820              number of ground terms to generate for model filtering
821
822       --conjecture-gen-max-depth=N
823              maximum depth of terms to consider for conjectures
824
825       --conjecture-gen-per-round=N
826              number of conjectures to generate per instantiation round
827
828       --conjecture-gen-uee-intro
829              more  aggressive  merging  for universal equality engine, intro‐
830              duces terms [*]
831
832       --conjecture-no-filter
833              do not filter conjectures [*]
834
835       --dt-stc-ind
836              apply  strengthening   for   existential   quantification   over
837              datatypes based on structural induction [*]
838
839       --dt-var-exp-quant
840              expand  datatype  variables  bound to one constructor in quanti‐
841              fiers [*]
842
843       --e-matching
844              whether to do heuristic E-matching [*]
845
846       --elim-ext-arith-quant
847              eliminate extended arithmetic symbols in quantified formulas [*]
848
849       --elim-taut-quant
850              eliminate tautological disjuncts of quantified formulas [*]
851
852       --finite-model-find
853              use finite model finding heuristic for quantifier  instantiation
854              [*]
855
856       --fmf-bound
857              finite model finding on bounded quantification [*]
858
859       --fmf-bound-int
860              finite model finding on bounded integer quantification [*]
861
862       --fmf-bound-lazy
863              enforce  bounds  for  bounded  quantification  lazily via use of
864              proxy variables [*]
865
866       --fmf-bound-min-mode=MODE
867              mode for which types of bounds to minimize  via  first  decision
868              heuristics
869
870       --fmf-empty-sorts
871              allow  finite model finding to assume sorts that do not occur in
872              ground assertions are empty [*]
873
874       --fmf-fmc-simple
875              simple models in full model check for finite model finding [*]
876
877       --fmf-fresh-dc
878              use fresh distinguished representative  when  applying  Inst-Gen
879              techniques [*]
880
881       --fmf-fun
882              find models for recursively defined functions, assumes functions
883              are admissible [*]
884
885       --fmf-fun-rlv
886              find models for recursively defined functions, assumes functions
887              are  admissible,  allows  empty type when function is irrelevant
888              [*]
889
890       --fmf-inst-engine
891              use instantiation engine in conjunction with finite model  find‐
892              ing [*]
893
894       --fmf-inst-gen
895              enable  Inst-Gen instantiation techniques for finite model find‐
896              ing [*]
897
898       --fmf-inst-gen-one-quant-per-round
899              only perform Inst-Gen instantiation techniques on one quantifier
900              per round [*]
901
902       --fs-interleave
903              interleave full saturate instantiation with other techniques [*]
904
905       --full-saturate-quant
906              when all other quantifier instantiation strategies fail, instan‐
907              tiate with ground terms from  relevant  domain,  then  arbitrary
908              ground terms before answering unknown [*]
909
910       --full-saturate-quant-rd
911              whether to use relevant domain first for full saturation instan‐
912              tiation strategy [*]
913
914       --global-negate
915              do global negation of input formula [*]
916
917       --ho-matching
918              do higher-order matching algorithm for  triggers  with  variable
919              operators [*]
920
921       --ho-matching-var-priority
922              give priority to variable arguments over constant arguments [*]
923
924       --ho-merge-term-db
925              merge term indices modulo equality [*]
926
927       --increment-triggers
928              generate additional triggers as needed during search [*]
929
930       --infer-arith-trigger-eq
931              infer  equalities  for trigger terms based on solving arithmetic
932              equalities [*]
933
934       --infer-arith-trigger-eq-exp
935              record explanations for inferArithTriggerEq [*]
936
937       --inst-level-input-only
938              only input terms are assigned instantiation level zero [*]
939
940       --inst-max-level=N
941              maximum inst level of terms used to instantiate quantified  for‐
942              mulas with (-1 == no limit, default)
943
944       --inst-no-entail
945              do  not  consider instances of quantified formulas that are cur‐
946              rently entailed [*]
947
948       --inst-no-model-true
949              do not consider instances of quantified formulas that  are  cur‐
950              rently true in model, if it is available [*]
951
952       --inst-prop
953              internal  propagation  for instantiations for selecting relevant
954              instances [*]
955
956       --inst-when-phase=N
957              instantiation rounds quantifiers  takes  (>=1)  before  allowing
958              theory combination to happen
959
960       --inst-when-strict-interleave
961              ensure theory combination and standard quantifier effort strate‐
962              gies take turns [*]
963
964       --inst-when-tc-first
965              allow theory combination to happen once initially, before  quan‐
966              tifier strategies are run [*]
967
968       --inst-when=MODE
969              when to apply instantiation
970
971       --int-wf-ind
972              apply strengthening for integers based on well-founded induction
973              [*]
974
975       --ite-dtt-split-quant
976              split ites with dt testers as conditions [*]
977
978       --ite-lift-quant=MODE
979              ite lifting mode for quantified formulas
980
981       --literal-matching=MODE
982              choose literal matching mode
983
984       --local-t-ext
985              do instantiation based on local theory extensions [*]
986
987       --lte-partial-inst
988              partially instantiate local theory quantifiers [*]
989
990       --lte-restrict-inst-closure
991              treat arguments of inst closure as restricted terms for  instan‐
992              tiation [*]
993
994       --macros-quant
995              perform quantifiers macro expansion [*]
996
997       --macros-quant-mode=MODE
998              mode for quantifiers macro expansion
999
1000       --mbqi-interleave
1001              interleave model-based quantifier instantiation with other tech‐
1002              niques [*]
1003
1004       --mbqi-one-inst-per-round
1005              only add one instantiation per quantifier per round for mbqi [*]
1006
1007       --mbqi-one-quant-per-round
1008              only add instantiations for one quantifier per  round  for  mbqi
1009              [*]
1010
1011       --mbqi=MODE
1012              choose mode for model-based quantifier instantiation
1013
1014       --miniscope-quant
1015              miniscope quantifiers [*]
1016
1017       --miniscope-quant-fv
1018              miniscope quantifiers for ground subformulas [*]
1019
1020       --multi-trigger-cache
1021              caching version of multi triggers [*]
1022
1023       --multi-trigger-linear
1024              implementation of multi triggers where maximum number of instan‐
1025              tiations is linear wrt number of ground terms [*]
1026
1027       --multi-trigger-priority
1028              only try multi triggers if single triggers  give  no  instantia‐
1029              tions [*]
1030
1031       --multi-trigger-when-single
1032              select multi triggers when single triggers exist [*]
1033
1034       --partial-triggers
1035              use triggers that do not contain all free variables [*]
1036
1037       --pre-skolem-quant
1038              apply skolemization eagerly to bodies of quantified formulas [*]
1039
1040       --pre-skolem-quant-agg
1041              apply skolemization to quantified formulas aggressively [*]
1042
1043       --pre-skolem-quant-nested
1044              apply skolemization to nested quantified formulas [*]
1045
1046       --prenex-quant-user
1047              prenex quantified formulas with user patterns [*]
1048
1049       --prenex-quant=MODE
1050              prenex mode for quantified formulas
1051
1052       --pure-th-triggers
1053              use pure theory terms as single triggers [*]
1054
1055       --purify-dt-triggers
1056              purify  dt  triggers,  match  all  constructors  of correct form
1057              instead of selectors [*]
1058
1059       --purify-triggers
1060              purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 [*]
1061
1062       --qcf-all-conflict
1063              add all available conflicting  instances  during  conflict-based
1064              instantiation [*]
1065
1066       --qcf-eager-check-rd
1067              optimization,  eagerly check relevant domain of matched position
1068              [*]
1069
1070       --qcf-eager-test
1071              optimization, test qcf instances eagerly [*]
1072
1073       --qcf-nested-conflict
1074              consider conflicts for nested quantifiers [*]
1075
1076       --qcf-skip-rd
1077              optimization, skip instances based on possibly  irrelevant  por‐
1078              tions of quantified formulas [*]
1079
1080       --qcf-tconstraint
1081              enable entailment checks for t-constraints in qcf algorithm [*]
1082
1083       --qcf-vo-exp
1084              qcf experimental variable ordering [*]
1085
1086       --quant-alpha-equiv
1087              infer alpha equivalence between quantified formulas [*]
1088
1089       --quant-anti-skolem
1090              perform anti-skolemization for quantified formulas [*]
1091
1092       --quant-cf
1093              enable conflict find mechanism for quantifiers [*]
1094
1095       --quant-cf-mode=MODE
1096              what effort to apply conflict find mechanism
1097
1098       --quant-cf-when=MODE
1099              when to invoke conflict find mechanism for quantifiers
1100
1101       --quant-dsplit-mode=MODE
1102              mode for dynamic quantifiers splitting
1103
1104       --quant-epr
1105              infer  whether  in  effectively  propositional fragment, use for
1106              cbqi [*]
1107
1108       --quant-epr-match
1109              use matching heuristics for EPR instantiation [*]
1110
1111       --quant-fun-wd
1112              assume that function defined by quantifiers are well defined [*]
1113
1114       --quant-ind
1115              use all available techniques for inductive reasoning [*]
1116
1117       --quant-model-ee
1118              use equality engine of model for last call effort [*]
1119
1120       --quant-rep-mode=MODE
1121              selection mode for representatives in quantifiers engine
1122
1123       --quant-split
1124              apply splitting to quantified formulas based  on  variable  dis‐
1125              joint disjuncts [*]
1126
1127       --register-quant-body-terms
1128              consider  ground  terms within bodies of quantified formulas for
1129              matching [*]
1130
1131       --relational-triggers
1132              choose relational triggers such as x = f(y), x >= f(y) [*]
1133
1134       --relevant-triggers
1135              prefer triggers that are more relevant based on SInE style anal‐
1136              ysis [*]
1137
1138       --rewrite-rules
1139              use rewrite rules module [*]
1140
1141       --rr-one-inst-per-round
1142              add one instance of rewrite rule per round [*]
1143
1144       --strict-triggers
1145              only  instantiate  quantifiers with user patterns based on trig‐
1146              gers [*]
1147
1148       --sygus-add-const-grammar
1149              statically add constants appearing in conjecture to grammars [*]
1150
1151       --sygus-auto-unfold
1152              enable approach which automatically unfolds  transition  systems
1153              for directly solving invariant synthesis problems [*]
1154
1155       --sygus-bool-ite-return-const
1156              Only  use  Boolean  constants  for  return  values  in  unifica‐
1157              tion-based function synthesis [*]
1158
1159       --sygus-eval-unfold
1160              do unfolding of sygus evaluation functions [*]
1161
1162       --sygus-eval-unfold-bool
1163              do unfolding of Boolean  evaluation  functions  that  appear  in
1164              refinement lemmas [*]
1165
1166       --sygus-ext-rew
1167              use extended rewriter for sygus [*]
1168
1169       --sygus-grammar-norm
1170              statically  normalize  sygus  grammars based on flattening (lin‐
1171              earization) [*]
1172
1173       --sygus-inference
1174              attempt to preprocess arbitrary inputs to sygus conjectures [*]
1175
1176       --sygus-inv-templ-when-sg
1177              use invariant templates (with solution reconstruction) for  syn‐
1178              tax guided problems [*]
1179
1180       --sygus-inv-templ=MODE
1181              template  mode  for sygus invariant synthesis (weaken pre-condi‐
1182              tion, strengthen post-condition, or none)
1183
1184       --sygus-min-grammar
1185              statically minimize sygus grammars [*]
1186
1187       --sygus-pbe
1188              enable approach which unifies conditional solutions, specialized
1189              for programming-by-examples (pbe) conjectures [*]
1190
1191       --sygus-qe-preproc
1192              use quantifier elimination as a preprocessing step for sygus [*]
1193
1194       --sygus-ref-eval
1195              direct evaluation of refinement lemmas for conflict analysis [*]
1196
1197       --sygus-repair-const
1198              use  approach  to  repair constants in sygus candidate solutions
1199              [*]
1200
1201       --sygus-rr
1202              use sygus to enumerate and verify correctness of  rewrite  rules
1203              via sampling [*]
1204
1205       --sygus-rr-synth
1206              use sygus to enumerate candidate rewrite rules via sampling [*]
1207
1208       --sygus-rr-synth-accel
1209              add   dynamic  symmetry  breaking  clauses  based  on  candidate
1210              rewrites [*]
1211
1212       --sygus-rr-synth-check
1213              use satisfiability check  to  verify  correctness  of  candidate
1214              rewrites [*]
1215
1216       --sygus-rr-synth-filter-cong
1217              filter candidate rewrites based on congruence [*]
1218
1219       --sygus-rr-synth-filter-match
1220              filter candidate rewrites based on matching [*]
1221
1222       --sygus-rr-synth-filter-order
1223              filter candidate rewrites based on variable ordering [*]
1224
1225       --sygus-rr-verify
1226              use  sygus  to  verify the correctness of rewrite rules via sam‐
1227              pling [*]
1228
1229       --sygus-rr-verify-abort
1230              abort when sygus-rr-verify finds an instance of unsoundness [*]
1231
1232       --sygus-sample-grammar
1233              when applicable, use grammar for choosing sample points [*]
1234
1235       --sygus-samples=N
1236              number of points to consider when doing  sygus  rewriter  sample
1237              testing
1238
1239       --sygus-stream
1240              enumerate a stream of solutions instead of terminating after the
1241              first one [*]
1242
1243       --sygus-templ-embed-grammar
1244              embed sygus templates into grammars [*]
1245
1246       --sygus-unif
1247              Unification-based function synthesis [*]
1248
1249       --term-db-mode
1250              which ground terms to consider for instantiation
1251
1252       --track-inst-lemmas
1253              track instantiation lemmas (for proofs, unsat cores, qe and syn‐
1254              thesis minimization) [*]
1255
1256       --trigger-active-sel
1257              selection mode to activate triggers
1258
1259       --trigger-sel
1260              selection mode for triggers
1261
1262       --user-pat=MODE
1263              policy   for  handling  user-provided  patterns  for  quantifier
1264              instantiation
1265
1266       --var-elim-quant
1267              enable simple variable elimination for quantified formulas [*]
1268
1269       --var-ineq-elim-quant
1270              enable variable elimination  based  on  infinite  projection  of
1271              unbound arithmetic variables [*]
1272

SEP OPTIONS

1274       --sep-check-neg
1275              check negated spatial assertions [*]
1276
1277       --sep-child-refine
1278              child-specific refinements of negated star, positive wand [*]
1279
1280       --sep-deq-c
1281              assume cardinality elements are distinct [*]
1282
1283       --sep-exp
1284              experimental flag for sep [*]
1285
1286       --sep-min-refine
1287              only  add  refinement  lemmas for minimal (innermost) assertions
1288              [*]
1289
1290       --sep-pre-skolem-emp
1291              eliminate emp constraint at preprocess time [*]
1292

SETS OPTIONS

1294       --sets-ext
1295              enable extended symbols such as complement and universe in  the‐
1296              ory of sets [*]
1297
1298       --sets-infer-as-lemmas
1299              send inferences as lemmas [*]
1300
1301       --sets-proxy-lemmas
1302              introduce proxy variables eagerly to shorten lemmas [*]
1303
1304       --sets-rel-eager
1305              standard effort checks for relations [*]
1306

SMT LAYER OPTIONS

1308       --abstract-values
1309              in  models,  output  arrays  (and in future, maybe others) using
1310              abstract values, as required by the SMT-LIB standard [*]
1311
1312       --bitblast-step
1313              amount of resources spent for each bitblast step (EXPERTS only)
1314
1315       --bv-sat-conflict-step
1316              amount of resources spent for  each  sat  conflict  (bitvectors)
1317              (EXPERTS only)
1318
1319       --check-models
1320              after SAT/INVALID/UNKNOWN, check that the generated model satis‐
1321              fies user assertions [*]
1322
1323       --check-proofs
1324              after UNSAT/VALID, machine-check the generated proof [*]
1325
1326       --check-synth-sol
1327              checks whether  produced  solutions  to  functions-to-synthesize
1328              satisfy the conjecture [*]
1329
1330       --check-unsat-cores
1331              after  UNSAT/VALID,  produce and check an unsat core (expensive)
1332              [*]
1333
1334       --cnf-step
1335              amount of resources  spent  for  each  call  to  cnf  conversion
1336              (EXPERTS only)
1337
1338       --decision-step
1339              amount of getNext decision calls in the decision engine (EXPERTS
1340              only)
1341
1342       --dump-instantiations
1343              output  instantiations  of  quantified  formulas   after   every
1344              UNSAT/VALID response [*]
1345
1346       --dump-models
1347              output models after every SAT/INVALID/UNKNOWN response [*]
1348
1349       --dump-proofs
1350              output proofs after every UNSAT/VALID response [*]
1351
1352       --dump-synth
1353              output   solution   for   synthesis   conjectures   after  every
1354              UNSAT/VALID response [*]
1355
1356       --dump-unsat-cores
1357              output unsat cores after every UNSAT/VALID response [*]
1358
1359       --dump-unsat-cores-full
1360              dump the full unsat core, including unlabeled assertions [*]
1361
1362       --ext-rew-prep
1363              use extended rewriter as a preprocessing pass [*]
1364
1365       --ext-rew-prep-agg
1366              use aggressive extended rewriter as a preprocessing pass [*]
1367
1368       --force-logic=LOGIC
1369              set the logic, and override all further user attempts to  change
1370              it (EXPERTS only)
1371
1372       --force-no-limit-cpu-while-dump
1373              Force no CPU limit when dumping models and proofs [*]
1374
1375       --ite-simp
1376              turn  on ite simplification (Kim (and Somenzi) et al., SAT 2009)
1377              [*]
1378
1379       --lemma-step
1380              amount of resources spent when adding lemmas (EXPERTS only)
1381
1382       --model-u-dt-enum
1383              in models, output uninterpreted sorts as  datatype  enumerations
1384              [*]
1385
1386       --omit-dont-cares
1387              When producing a model, omit variables whose value does not mat‐
1388              ter [*]
1389
1390       --on-repeat-ite-simp
1391              do the ite simplification pass again if repeating simplification
1392              [*]
1393
1394       --parse-step
1395              amount  of  resources  spent for each command/expression parsing
1396              (EXPERTS only)
1397
1398       --preprocess-step
1399              amount  of  resources  spent  for  each  preprocessing  step  in
1400              SmtEngine (EXPERTS only)
1401
1402       --produce-assignments
1403              support the get-assignment command [*]
1404
1405       --produce-unsat-assumptions
1406              turn on unsat assumptions generation [*]
1407
1408       --produce-unsat-cores
1409              turn on unsat core generation [*]
1410
1411       --proof
1412              turn on proof generation [*]
1413
1414       --quantifier-step
1415              amount of resources spent for quantifier instantiations (EXPERTS
1416              only)
1417
1418       --repeat-simp
1419              make multiple passes with nonclausal simplifier [*]
1420
1421       --restart-step
1422              amount of resources spent for each theory restart (EXPERTS only)
1423
1424       --rewrite-apply-to-const
1425              eliminate function applications, rewriting e.g. f(5)  to  a  new
1426              symbol f_5 (EXPERTS only) [*]
1427
1428       --rewrite-step
1429              amount of resources spent for each rewrite step (EXPERTS only)
1430
1431       --sat-conflict-step
1432              amount  of  resources  spent  for  each  sat  conflict (main sat
1433              solver) (EXPERTS only)
1434
1435       --simp-ite-compress
1436              enables compressing ites after ite simplification [*]
1437
1438       --simp-ite-hunt-zombies
1439              post ite compression enables zombie removal while the number  of
1440              nodes is above this threshold
1441
1442       --simp-with-care
1443              enables simplifyWithCare in ite simplificiation [*]
1444
1445       --simplification=MODE
1446              choose simplification mode, see --simplification=help
1447
1448       --sort-inference
1449              calculate  sort  inference  of  input problem, convert the input
1450              based on monotonic sorts [*]
1451
1452       --static-learning
1453              use static learning (on by default) [*]
1454
1455       --sygus-out=MODE
1456              output mode for sygus
1457
1458       --sygus-print-callbacks
1459              use sygus print callbacks to print sygus terms in the  user-pro‐
1460              vided form (disable for debugging) [*]
1461
1462       --symmetry-breaker-exp
1463              generate  symmetry breaking constraints after symmetry detection
1464              [*]
1465
1466       --theory-check-step
1467              amount of resources spent for each theory  check  call  (EXPERTS
1468              only)
1469
1470       --unconstrained-simp
1471              turn  on unconstrained simplification (see Bruttomesso/Brummayer
1472              PhD thesis) [*]
1473
1474       --no-simplification
1475              turn off all simplification (same as --simplification=none)
1476

STRINGS THEORY OPTIONS

1478       --strings-abort-loop
1479              abort when a looping word equation is encountered [*]
1480
1481       --strings-binary-csp
1482              use binary search when splitting strings [*]
1483
1484       --strings-check-entail-len
1485              check entailment between length terms to reduce splitting [*]
1486
1487       --strings-eager
1488              strings eager check [*]
1489
1490       --strings-eager-len
1491              strings eager length lemmas [*]
1492
1493       --strings-eit
1494              the eager intersection used by the theory of strings [*]
1495
1496       --strings-exp
1497              experimental features in the theory of strings [*]
1498
1499       --strings-fmf
1500              the finite model finding used by the theory of strings [*]
1501
1502       --strings-guess-model
1503              use model guessing to avoid string extended function  reductions
1504              [*]
1505
1506       --strings-infer-as-lemmas
1507              always send lemmas out instead of making internal inferences [*]
1508
1509       --strings-infer-sym
1510              strings split on empty string [*]
1511
1512       --strings-inm
1513              internal  for  strings:  ignore  negative membership constraints
1514              (fragment checking is needed, left to users for now) [*]
1515
1516       --strings-lazy-pp
1517              perform string preprocessing lazily [*]
1518
1519       --strings-lb=N
1520              the strategy of LB rule application: 0-lazy, 1-eager, 2-no
1521
1522       --strings-len-geqz
1523              strings length greater than zero lemmas [*]
1524
1525       --strings-len-norm
1526              strings length normalization lemma [*]
1527
1528       --strings-lprop-csp
1529              do length propagation based on constant splits [*]
1530
1531       --strings-min-prefix-explain
1532              minimize explanations for prefix of normal forms in strings [*]
1533
1534       --strings-opt1
1535              internal option1 for strings: normal form [*]
1536
1537       --strings-opt2
1538              internal option2 for strings: constant regexp splitting [*]
1539
1540       --strings-print-ascii
1541              the alphabet contains only printable characters from  the  stan‐
1542              dard extended ASCII [*]
1543
1544       --strings-process-loop
1545              reduce looping word equations to regular expressions [*]
1546
1547       --strings-rexplain-lemmas
1548              regression explanations for string lemmas [*]
1549
1550       --strings-sp-emp
1551              strings split on empty string [*]
1552
1553       --strings-uf-reduct
1554              use  uninterpreted  functions  when  applying  extended function
1555              reductions [*]
1556

THEORY LAYER OPTIONS

1558       --assign-function-values
1559              assign values for uninterpreted functions in models [*]
1560
1561       --condense-function-values
1562              condense values for functions in models rather  than  explicitly
1563              representing them [*]
1564
1565       --theoryof-mode=MODE
1566              mode for Theory::theoryof() (EXPERTS only)
1567
1568       --use-theory=NAME
1569              use  alternate theory implementation NAME (--use-theory=help for
1570              a list). This option may be repeated or a comma separated list.
1571

UNINTERPRETED FUNCTIONS THEORY OPTIONS

1573       --symmetry-breaker
1574              use UF symmetry breaker (Deharbe et al., CADE 2011) [*]
1575
1576       --uf-ho
1577              enable support for higher-order reasoning [*]
1578
1579       --uf-ho-ext
1580              apply extensionality on function symbols [*]
1581
1582       --uf-ss-abort-card=N
1583              tells the uf strong solver to only consider models  that  inter‐
1584              pret  uninterpreted  sorts  of  cardinality  at most N (-1 == no
1585              limit, default)
1586
1587       --uf-ss-clique-splits
1588              use cliques instead of splitting on demand to shrink model [*]
1589
1590       --uf-ss-eager-split
1591              add splits eagerly for uf strong solver [*]
1592
1593       --uf-ss-fair
1594              use fair strategy for finite model finding multiple sorts [*]
1595
1596       --uf-ss-fair-monotone
1597              group monotone sorts when enforcing fairness  for  finite  model
1598              finding [*]
1599
1600       --uf-ss-regions
1601              disable  region-based  method for discovering cliques and splits
1602              in uf strong solver [*]
1603
1604       --uf-ss-totality
1605              always use totality axioms for enforcing cardinality constraints
1606              [*]
1607
1608       --uf-ss-totality-limited=N
1609              apply  totality  axioms,  but only up to cardinality N (-1 == do
1610              not apply totality axioms, default)
1611
1612       --uf-ss-totality-sym-break
1613              apply symmetry breaking for totality axioms [*]
1614
1615       --uf-ss=MODE
1616              mode of operation for uf strong solver.
1617
1618
1619       Each option marked  with  [*]  has  a  --no-OPTIONNAME  variant,  which
1620       reverses the sense of the option.
1621
1622

DIAGNOSTICS

1624       CVC4 reports all syntactic and semantic errors on standard error.
1625

HISTORY

1627       The  CVC4 effort is the culmination of fifteen years of theorem proving
1628       research, starting with the Stanford Validity Checker (SVC) in 1996.
1629
1630       SVC's successor, the Cooperating Validity Checker  (CVC),  had  a  more
1631       optimized  internal design, produced proofs, used the Chaff SAT solver,
1632       and featured a number of usability enhancements.  Its name  comes  from
1633       the  cooperative  nature  of decision procedures in Nelson-Oppen theory
1634       combination, which share amongst each other equalities  between  shared
1635       terms.
1636
1637       CVC  Lite,  first  made  available  in  2003, was a rewrite of CVC that
1638       attempted to make CVC more flexible (hence the “lite”) while  extending
1639       the  feature  set: CVCLite supported quantifiers where its predecessors
1640       did not.  CVC3 was a major overhaul of portions of CVC Lite:  it  added
1641       better decision procedure implementations, added support for using Min‐
1642       iSat in the core, and had generally better performance.
1643
1644       CVC4 is the new version, the fifth generation of this validity  checker
1645       line  that is now celebrating fifteen years of heritage.  It represents
1646       a complete re-evaluation of the core architecture to be both performant
1647       and  to  serve  as a cutting-edge research vehicle for the next several
1648       years.  Rather than taking CVC3 and redesigning  problem  parts,  we've
1649       taken  a  clean-room approach, starting from scratch.  Before using any
1650       designs from CVC3, we have thoroughly scrutinized, vetted, and  updated
1651       them.   Many parts of CVC4 bear only a superficial resemblance, if any,
1652       to their correspondent in CVC3.
1653
1654       However, CVC4 is fundamentally similar to CVC3 and  many  other  modern
1655       SMT  solvers:  it  is a DPLL( T ) solver, with a SAT solver at its core
1656       and a delegation path to different decision procedure  implementations,
1657       each in charge of solving formulas in some background theory.
1658
1659       The  re-evaluation  and ground-up rewrite was necessitated, we felt, by
1660       the performance characteristics of CVC3.  CVC3  has  many  useful  fea‐
1661       tures,  but some core aspects of the design led to high memory use, and
1662       the use of  heavyweight  computation  (where  more  nimble  engineering
1663       approaches  could  suffice)  makes CVC3 a much slower prover than other
1664       tools.  As these designs are central to CVC3, a new version was prefer‐
1665       able to a selective re-engineering, which would have ballooned in short
1666       order.
1667

VERSION

1669       This manual page refers to CVC4 version 1.6.
1670

BUGS

1672       An  issue   tracker   for   the   CVC4   project   is   maintained   at
1673       https://github.com/CVC4/CVC4/issues.
1674

AUTHORS

1676       CVC4  is  developed by a team of researchers at Stanford University and
1677       the University of Iowa.  See the AUTHORS file in the distribution for a
1678       full list of contributors.
1679

SEE ALSO

1681       libcvc4(3), libcvc4parser(3), libcvc4compat(3)
1682
1683       Additionally,  the  CVC4  wiki  contains  useful  information about the
1684       design and internals of CVC4.  It is maintained at http://cvc4.cs.stan
1685       ford.edu/wiki/.
1686
1687
1688
1689CVC4 release 1.6                   July 2018                           CVC4(1)
Impressum