1CVC4(1) User Manuals CVC4(1)
2
6 cvc4, pcvc4 - an automated theorem prover
7
9 cvc4 [ options ] [ file ]
10 pcvc4 [ options ] [ file ]
12
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 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 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
30 Each option marked with [*] has a --no-OPTIONNAME variant, which
31 reverses the sense of the option.
32 --lang=LANG | -L LANG
35 force input language (default is "auto"; see --lang help)
36 --output-lang=LANG
38 force output language (default is "auto"; see --output-lang
39 help)
40 --quiet | -q
42 decrease verbosity (may be repeated)
43 --stats
45 give statistics on exit [*]
46 --verbose | -v
48 increase verbosity (may be repeated)
49 --copyright
51 show CVC4 copyright information
52 --help | -h
54 full command line reference
55 --seed | -s
57 seed for random number generator
58 --show-config
60 show CVC4 static configuration
61 --version | -V
63 identify this CVC4 binary
64 --strict-parsing
66 be less tolerant of non-conforming inputs [*]
67 --cpu-time
69 measures CPU time if set to true and wall time if false (default
70 false) [*]
71 --dump-to=FILE
73 all dumping goes to FILE (instead of stdout)
74 --dump=MODE
76 dump preprocessed assertions, etc., see --dump=help
77 --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 --incremental | -i
84 enable incremental solving [*]
85 --produce-assertions
87 keep an assertions list (enables get-assertions command) [*]
88 --produce-models | -m
90 support the get-value and get-model commands [*]
91 --rlimit-per=N
93 enable resource limiting per query
94 --rlimit=N
96 enable resource limiting (currently, roughly the number of SAT
97 conflicts)
98 --tlimit-per=MS
100 enable time limiting per query (give milliseconds)
101 --tlimit=MS
103 enable time limiting (give milliseconds)
104
107 --approx-branch-depth
108 maximum branch depth the approximate solver is allowed to take
109 --arith-no-partial-fun
111 do not use partial function semantics for arithmetic (not SMT
112 LIB compliant) [*]
113 --arith-prop-clauses
115 rows shorter than this are propagated as clauses
116 --arith-prop=MODE
118 turns on arithmetic propagation (default is 'old', see
119 --arith-prop=help)
120 --arith-rewrite-equalities
122 turns on the preprocessing rewrite turning equalities into a
123 conjunction of inequalities [*]
124 --collect-pivot-stats
126 collect the pivot history [*]
127 --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 --dio-decomps
133 let skolem variables for integer divisibility constraints leak
134 from the dio solver [*]
135 --dio-repeat
137 handle dio solver constraints in mass or one at a time [*]
138 --dio-solver
140 turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)
141 [*]
142 --dio-turns
144 turns in a row dio solver cutting gets
145 --error-selection-rule=RULE
147 change the pivot rule for the basic variable (default is 'min',
148 see --pivot-rule help)
149 --fc-penalties
151 turns on degenerate pivot penalties [*]
152 --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 --lemmas-on-replay-failure
159 attempt to use external lemmas if approximate solve integer
160 failed [*]
161 --maxCutsInContext
163 maximum cuts in a given context before signalling a restart
164 --miplib-trick
166 turns on the preprocessing step of attempting to infer bounds on
167 miplib problems [*]
168 --miplib-trick-subs=N
170 do substitution for miplib 'tmp' vars if defined in <= N elimi‐
171 nated vars
172 --new-prop
174 use the new row propagation system [*]
175 --nl-ext
177 extended approach to non-linear [*]
178 --nl-ext-ent-conf
180 check for entailed conflicts in non-linear solver [*]
181 --nl-ext-factor
183 use factoring inference in non-linear solver [*]
184 --nl-ext-inc-prec
186 whether to increment the precision for irrational function con‐
187 straints [*]
188 --nl-ext-purify
190 purify non-linear terms at preprocess [*]
191 --nl-ext-rbound
193 use resolution-style inference for inferring new bounds [*]
194 --nl-ext-rewrite
196 do rewrites in non-linear solver [*]
197 --nl-ext-split-zero
199 intial splits on zero for all variables [*]
200 --nl-ext-tf-taylor-deg=N
202 initial degree of polynomials for Taylor approximation
203 --nl-ext-tf-tplanes
205 use non-terminating tangent plane strategy for transcendental
206 functions for non-linear [*]
207 --nl-ext-tplanes
209 use non-terminating tangent plane strategy for non-linear [*]
210 --nl-ext-tplanes-interleave
212 interleave tangent plane strategy for non-linear [*]
213 --pb-rewrites
215 apply pseudo boolean rewrites [*]
216 --pivot-threshold=N
218 sets the number of pivots using --pivot-rule per basic variable
219 per simplex instance before using variable order
220 --pp-assert-max-sub-size
222 threshold for substituting an equality in ppAssert
223 --prop-row-length=N
225 sets the maximum row length to be used in propagation
226 --replay-early-close-depth
228 multiples of the depths to try to close the approx log eagerly
229 --replay-failure-penalty
231 number of solve integer attempts to skips after a numeric fail‐
232 ure
233 --replay-lemma-reject-cut
235 maximum complexity of any coefficient while outputting replaying
236 cut lemmas
237 --replay-num-err-penalty
239 number of solve integer attempts to skips after a numeric fail‐
240 ure
241 --replay-reject-cut
243 maximum complexity of any coefficient while replaying cuts
244 --replay-soi-major-threshold
246 threshold for a major tolerance failure by the approximate
247 solver
248 --replay-soi-major-threshold-pen
250 threshold for a major tolerance failure by the approximate
251 solver
252 --replay-soi-minor-threshold
254 threshold for a minor tolerance failure by the approximate
255 solver
256 --replay-soi-minor-threshold-pen
258 threshold for a minor tolerance failure by the approximate
259 solver
260 --restrict-pivots
262 have a pivot cap for simplex at effort levels below fullEffort
263 [*]
264 --revert-arith-models-on-unsat
266 revert the arithmetic model to a known safe model on unsat if
267 one is cached [*]
268 --rewrite-divk
270 rewrite division and mod when by a constant into linear terms
271 [*]
272 --rr-turns
274 round robin turn
275 --se-solve-int
277 attempt to use the approximate solve integer method on standard
278 effort [*]
279 --simplex-check-period=N
281 the number of pivots to do in simplex before rechecking for a
282 conflict on all variables
283 --snorm-infer-eq
285 infer equalities based on Shostak normalization [*]
286 --soi-qe
288 use quick explain to minimize the sum of infeasibility conflicts
289 [*]
290 --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 --unate-lemmas=MODE
296 determines which lemmas to add before solving (default is 'all',
297 see --unate-lemmas=help)
298 --use-approx
300 attempt to use an approximate solver [*]
301 --use-fcsimplex
303 use focusing and converging simplex (FMCAD 2013 submission) [*]
304 --use-soi
306 use sum of infeasibility simplex (FMCAD 2013 submission) [*]
307
309 --arrays-config
310 set different array option configurations - for developers only
311 --arrays-eager-index
313 turn on eager index splitting for generated array lemmas [*]
314 --arrays-eager-lemmas
316 turn on eager lemma generation for arrays [*]
317 --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 --arrays-model-based
324 turn on model-based array solver [*]
325 --arrays-optimize-linear
327 turn on optimization for linear array terms (see de Moura FMCAD
328 09 arrays paper) [*]
329 --arrays-prop
331 propagation effort for arrays: 0 is none, 1 is some, 2 is full
332 --arrays-reduce-sharing
334 use model information to reduce size of care graph for arrays
335 [*]
336 --arrays-weak-equiv
338 use algorithm from Christ/Hoenicke (SMT 2014) [*]
339
341 --debug=TAG | -d TAG
342 debug something (e.g. -d arith), can repeat
343 --parse-only
345 exit after parsing input [*]
346 --preprocess-only
348 exit after preprocessing input [*]
349 --print-success
351 print the "success" output required of SMT-LIBv2 [*]
352 --stats-every-query
354 in incremental mode, print stats after every satisfiability or
355 validity query [*]
356 --stats-hide-zeros
358 hide statistics which are zero [*]
359 --trace=TAG | -t TAG
361 trace something (e.g. -t pushpop), can repeat
362 --smtlib-strict
364 SMT-LIBv2 compliance mode (implies other options)
365
367 --bitblast-aig
368 bitblast by first converting to AIG (implies --bitblast=eager)
369 [*]
370 --bitblast=MODE
372 choose bitblasting mode, see --bitblast=help
373 --bool-to-bv
375 convert booleans to bit-vectors of size 1 when possible [*]
376 --bv-abstraction
378 mcm benchmark abstraction (EXPERTS only) [*]
379 --bv-aig-simp=COMMAND
381 abc command to run AIG simplifications (implies --bitblast-aig,
382 default is "balance;drw") (EXPERTS only)
383 --bv-alg-extf
385 algebraic inferences for extended functions [*]
386 --bv-algebraic-budget
388 the budget allowed for the algebraic solver in number of SAT
389 conflicts (EXPERTS only)
390 --bv-algebraic-solver
392 turn on the algebraic solver for the bit-vector theory (only if
393 --bitblast=lazy) [*]
394 --bv-div-zero-const
396 always return -1 on division by zero [*]
397 --bv-eager-explanations
399 compute bit-blasting propagation explanations eagerly (EXPERTS
400 only) [*]
401 --bv-eq-slicer=MODE
403 turn on the slicing equality solver for the bit-vector theory
404 (only if --bitblast=lazy)
405 --bv-eq-solver
407 use the equality engine for the bit-vector theory (only if
408 --bitblast=lazy) [*]
409 --bv-extract-arith
411 enable rewrite pushing extract [i:0] over arithmetic operations
412 (can blow up) (EXPERTS only) [*]
413 --bv-gauss-elim
415 simplify formula via Gaussian Elimination if applicable (EXPERTS
416 only) [*]
417 --bv-inequality-solver
419 turn on the inequality solver for the bit-vector theory (only if
420 --bitblast=lazy) [*]
421 --bv-intro-pow2
423 introduce bitvector powers of two as a preprocessing pass
424 (EXPERTS only) [*]
425 --bv-lazy-reduce-extf
427 reduce extended functions like bv2nat and int2bv at last call
428 instead of full effort [*]
429 --bv-lazy-rewrite-extf
431 lazily rewrite extended functions like bv2nat and int2bv [*]
432 --bv-num-func=NUM
434 number of function symbols in conflicts that are generalized
435 (EXPERTS only)
436 --bv-propagate
438 use bit-vector propagation in the bit-blaster [*]
439 --bv-quick-xplain
441 minimize bv conflicts using the QuickXplain algorithm (EXPERTS
442 only) [*]
443 --bv-sat-solver=MODE
445 choose which sat solver to use, see --bv-sat-solver=help
446 (EXPERTS only)
447 --bv-skolemize
449 skolemize arguments for bv abstraction (only does something if
450 --bv-abstraction is on) (EXPERTS only) [*]
451 --bv-to-bool
453 lift bit-vectors of size 1 to booleans when possible [*]
454
456 --cdt-bisimilar
457 do bisimilarity check for co-datatypes [*]
458 --dt-binary-split
460 do binary splits for datatype constructor types [*]
461 --dt-blast-splits
463 when applicable, blast splitting lemmas for all variables at
464 once [*]
465 --dt-cyclic
467 do cyclicity check for datatypes [*]
468 --dt-force-assignment
470 force the datatypes solver to give specific values to all
471 datatypes terms before answering sat [*]
472 --dt-infer-as-lemmas
474 always send lemmas out instead of making internal inferences [*]
475 --dt-ref-sk-intro
477 introduce reference skolems for shorter explanations [*]
478 --dt-rewrite-error-sel
480 rewrite incorrectly applied selectors to arbitrary ground term
481 (EXPERTS only) [*]
482 --dt-share-sel
484 internally use shared selectors across multiple constructors [*]
485 --dt-use-testers
487 do not preprocess away tester predicates [*]
488 --sygus-abort-size=N
490 tells enumerative sygus to only consider solutions up to term
491 size N (-1 == no limit, default)
492 --sygus-eval-builtin
494 use builtin kind for evaluation functions in sygus [*]
495 --sygus-fair-max
497 use max instead of sum for multi-function sygus conjectures [*]
498 --sygus-fair=MODE
500 if and how to apply fairness for sygus
501 --sygus-opt1
503 sygus experimental option [*]
504 --sygus-sym-break
506 simple sygus sym break lemmas [*]
507 --sygus-sym-break-dynamic
509 dynamic sygus sym break lemmas [*]
510 --sygus-sym-break-lazy
512 lazily add symmetry breaking lemmas for terms [*]
513 --sygus-sym-break-pbe
515 sygus sym break lemmas based on pbe conjectures [*]
516 --sygus-sym-break-rlv
518 add relevancy conditions to symmetry breaking lemmas [*]
519
521 --decision-random-weight=N
522 assign random weights to nodes between 0 and N-1 (0: disable)
523 (EXPERTS only)
524 --decision-threshold=N
526 ignore all nodes greater than threshold in first attempt to pick
527 decision (EXPERTS only)
528 --decision-use-weight
530 use the weight nodes (locally, by looking at children) to direct
531 recursive search (EXPERTS only) [*]
532 --decision-weight-internal=HOW
534 computer weights of internal nodes using children: off, max,
535 sum, usr1 (meaning evolving) (EXPERTS only)
536 --decision=MODE
538 choose decision mode, see --decision=help
539
541 --default-dag-thresh=N
542 dagify common subexprs appearing > N times (1 == default, 0 ==
543 don't dagify)
544 --default-expr-depth=N
546 print exprs to depth N (0 == default, -1 == no limit)
547 --eager-type-checking
549 type check expressions immediately on creation (debug builds
550 only) [*]
551 --print-expr-types
553 print types with variables when printing exprs [*]
554 --type-checking
556 never type check expressions
557
559 --idl-rewrite-equalities
560 enable rewriting equalities into two inequalities in IDL solver
561 (default is disabled) [*]
562
564 --continued-execution
565 continue executing commands, even on error [*]
566 --early-exit
568 do not run destructors at exit; default on except in debug
569 builds (EXPERTS only) [*]
570 --fallback-sequential
572 Switch to sequential mode (instead of printing an error) if it
573 can't be solved in portfolio mode [*]
574 --filter-lemma-length=N
576 don't share (among portfolio threads) lemmas strictly longer
577 than N
578 --incremental-parallel
580 Use parallel solver even in incremental mode (may print
581 'unknown's at times) [*]
582 --interactive
584 force interactive/non-interactive mode [*]
585 --segv-spin
587 spin on segfault/other crash waiting for gdb [*]
588 --show-debug-tags
590 show all available tags for debugging
591 --show-trace-tags
593 show all available tags for tracing
594 --tear-down-incremental=N
596 implement PUSH/POP/multi-query by destroying and recreating
597 SmtEngine every N queries (EXPERTS only)
598 --thread-stack=N
600 stack size for worker threads in MB (0 means use Boost/thread
601 lib default)
602 --threadN=string
604 configures portfolio thread N (0..#threads-1)
605 --threads=N
607 Total number of threads for portfolio
608 --wait-to-join
610 wait for other threads to join before quitting (EXPERTS only)
611 [*]
612
614 --mmap memory map file input [*]
615
617 --inst-format=MODE
618 print format mode for instantiations, see --inst-format=help
619 --model-format=MODE
621 print format mode for models, see --model-format=help
622
624 --aggressive-core-min
625 turns on aggressive unsat core minimization (experimental) [*]
626 --allow-empty-dependencies
628 if unable to track the dependencies of a rewritten/preprocessed
629 assertion, fail silently [*]
630 --fewer-preprocessing-holes
632 try to eliminate preprocessing holes in proofs [*]
633 --lfsc-letification
635 turns on global letification in LFSC proofs [*]
636
638 --minisat-dump-dimacs
639 instead of solving minisat dumps the asserted clauses in Dimacs
640 format [*]
641 --minisat-elimination
643 use Minisat elimination [*]
644 --random-freq=P
646 sets the frequency of random decisions in the sat solver (P=0.0
647 by default)
648 --random-seed=S
650 sets the random seed for the sat solver
651 --refine-conflicts
653 refine theory conflict clauses (default false) [*]
654 --restart-int-base=N
656 sets the base restart interval for the sat solver (N=25 by
657 default)
658 --restart-int-inc=F
660 sets the restart interval increase factor for the sat solver
661 (F=3.0 by default)
662
664 --ag-miniscope-quant
665 perform aggressive miniscoping for quantifiers [*]
666 --cbqi turns on counterexample-based quantifier instantiation [*]
668 --cbqi-all
670 apply counterexample-based instantiation to all quantified for‐
671 mulas [*]
672 --cbqi-bv
674 use word-level inversion approach for counterexample-guided
675 quantifier instantiation for bit-vectors [*]
676 --cbqi-bv-concat-inv
678 compute inverse for concat over equalities rather than producing
679 an invertibility condition [*]
680 --cbqi-bv-ineq=MODE
682 choose mode for handling bit-vector inequalities with counterex‐
683 ample-guided instantiation
684 --cbqi-bv-interleave-value
686 interleave model value instantiation with word-level inversion
687 approach [*]
688 --cbqi-bv-linear
690 linearize adder chains for variables [*]
691 --cbqi-bv-rm-extract
693 replaces extract terms with variables for counterexample-guided
694 instantiation for bit-vectors [*]
695 --cbqi-bv-solve-nl
697 try to solve non-linear bv literals using model value projec‐
698 tions [*]
699 --cbqi-full
701 turns on full effort counterexample-based quantifier instantia‐
702 tion, which may resort to model-value instantiation [*]
703 --cbqi-innermost
705 only process innermost quantified formulas in counterexam‐
706 ple-based quantifier instantiation [*]
707 --cbqi-lit-dep
709 dependency lemmas for quantifier alternation in counterexam‐
710 ple-based quantifier instantiation [*]
711 --cbqi-midpoint
713 choose substitutions based on midpoints of lower and upper
714 bounds for counterexample-based quantifier instantiation [*]
715 --cbqi-min-bounds
717 use minimally constrained lower/upper bound for counterexam‐
718 ple-based quantifier instantiation [*]
719 --cbqi-model
721 guide instantiations by model values for counterexample-based
722 quantifier instantiation [*]
723 --cbqi-multi-inst
725 when applicable, do multi instantiations per quantifier per
726 round in counterexample-based quantifier instantiation [*]
727 --cbqi-nested-qe
729 process nested quantified formulas with quantifier elimination
730 in counterexample-based quantifier instantiation [*]
731 --cbqi-nopt
733 non-optimal bounds for counterexample-based quantifier instanti‐
734 ation [*]
735 --cbqi-prereg-inst
737 preregister ground instantiations in counterexample-based quan‐
738 tifier instantiation [*]
739 --cbqi-recurse
741 turns on recursive counterexample-based quantifier instantiation
742 [*]
743 --cbqi-repeat-lit
745 solve literals more than once in counterexample-based quantifier
746 instantiation [*]
747 --cbqi-round-up-lia
749 round up integer lower bounds in substitutions for counterexam‐
750 ple-based quantifier instantiation [*]
751 --cbqi-sat
753 answer sat when quantifiers are asserted with counterexam‐
754 ple-based quantifier instantiation [*]
755 --cbqi-use-inf-int
757 use integer infinity for vts in counterexample-based quantifier
758 instantiation [*]
759 --cbqi-use-inf-real
761 use real infinity for vts in counterexample-based quantifier
762 instantiation [*]
763 --cegis-sample=MODE
765 mode for using samples in the counterexample-guided inductive
766 synthesis loop
767 --cegqi
769 counterexample-guided quantifier instantiation for sygus [*]
770 --cegqi-si-abort
772 abort if synthesis conjecture is not single invocation [*]
773 --cegqi-si-partial
775 combined techniques for synthesis conjectures that are partially
776 single invocation [*]
777 --cegqi-si-reconstruct
779 reconstruct solutions for single invocation conjectures in orig‐
780 inal grammar [*]
781 --cegqi-si-reconstruct-const
783 include constants when reconstruct solutions for single invoca‐
784 tion conjectures in original grammar [*]
785 --cegqi-si-sol-min-core
787 minimize solutions for single invocation conjectures based on
788 unsat core [*]
789 --cegqi-si-sol-min-inst
791 minimize individual instantiations for single invocation conjec‐
792 tures based on unsat core [*]
793 --cegqi-si=MODE
795 mode for processing single invocation synthesis conjectures
796 --cond-rewrite-quant
798 conditional rewriting of quantified formulas [*]
799 --cond-var-split-agg-quant
801 aggressive split quantified formulas that lead to variable elim‐
802 inations [*]
803 --cond-var-split-quant
805 split quantified formulas that lead to variable eliminations [*]
806 --conjecture-filter-active-terms
808 filter based on active terms [*]
809 --conjecture-filter-canonical
811 filter based on canonicity [*]
812 --conjecture-filter-model
814 filter based on model [*]
815 --conjecture-gen
817 generate candidate conjectures for inductive proofs [*]
818 --conjecture-gen-gt-enum=N
820 number of ground terms to generate for model filtering
821 --conjecture-gen-max-depth=N
823 maximum depth of terms to consider for conjectures
824 --conjecture-gen-per-round=N
826 number of conjectures to generate per instantiation round
827 --conjecture-gen-uee-intro
829 more aggressive merging for universal equality engine, intro‐
830 duces terms [*]
831 --conjecture-no-filter
833 do not filter conjectures [*]
834 --dt-stc-ind
836 apply strengthening for existential quantification over
837 datatypes based on structural induction [*]
838 --dt-var-exp-quant
840 expand datatype variables bound to one constructor in quanti‐
841 fiers [*]
842 --e-matching
844 whether to do heuristic E-matching [*]
845 --elim-ext-arith-quant
847 eliminate extended arithmetic symbols in quantified formulas [*]
848 --elim-taut-quant
850 eliminate tautological disjuncts of quantified formulas [*]
851 --finite-model-find
853 use finite model finding heuristic for quantifier instantiation
854 [*]
855 --fmf-bound
857 finite model finding on bounded quantification [*]
858 --fmf-bound-int
860 finite model finding on bounded integer quantification [*]
861 --fmf-bound-lazy
863 enforce bounds for bounded quantification lazily via use of
864 proxy variables [*]
865 --fmf-bound-min-mode=MODE
867 mode for which types of bounds to minimize via first decision
868 heuristics
869 --fmf-empty-sorts
871 allow finite model finding to assume sorts that do not occur in
872 ground assertions are empty [*]
873 --fmf-fmc-simple
875 simple models in full model check for finite model finding [*]
876 --fmf-fresh-dc
878 use fresh distinguished representative when applying Inst-Gen
879 techniques [*]
880 --fmf-fun
882 find models for recursively defined functions, assumes functions
883 are admissible [*]
884 --fmf-fun-rlv
886 find models for recursively defined functions, assumes functions
887 are admissible, allows empty type when function is irrelevant
888 [*]
889 --fmf-inst-engine
891 use instantiation engine in conjunction with finite model find‐
892 ing [*]
893 --fmf-inst-gen
895 enable Inst-Gen instantiation techniques for finite model find‐
896 ing [*]
897 --fmf-inst-gen-one-quant-per-round
899 only perform Inst-Gen instantiation techniques on one quantifier
900 per round [*]
901 --fs-interleave
903 interleave full saturate instantiation with other techniques [*]
904 --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 --full-saturate-quant-rd
911 whether to use relevant domain first for full saturation instan‐
912 tiation strategy [*]
913 --global-negate
915 do global negation of input formula [*]
916 --ho-matching
918 do higher-order matching algorithm for triggers with variable
919 operators [*]
920 --ho-matching-var-priority
922 give priority to variable arguments over constant arguments [*]
923 --ho-merge-term-db
925 merge term indices modulo equality [*]
926 --increment-triggers
928 generate additional triggers as needed during search [*]
929 --infer-arith-trigger-eq
931 infer equalities for trigger terms based on solving arithmetic
932 equalities [*]
933 --infer-arith-trigger-eq-exp
935 record explanations for inferArithTriggerEq [*]
936 --inst-level-input-only
938 only input terms are assigned instantiation level zero [*]
939 --inst-max-level=N
941 maximum inst level of terms used to instantiate quantified for‐
942 mulas with (-1 == no limit, default)
943 --inst-no-entail
945 do not consider instances of quantified formulas that are cur‐
946 rently entailed [*]
947 --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 --inst-prop
953 internal propagation for instantiations for selecting relevant
954 instances [*]
955 --inst-when-phase=N
957 instantiation rounds quantifiers takes (>=1) before allowing
958 theory combination to happen
959 --inst-when-strict-interleave
961 ensure theory combination and standard quantifier effort strate‐
962 gies take turns [*]
963 --inst-when-tc-first
965 allow theory combination to happen once initially, before quan‐
966 tifier strategies are run [*]
967 --inst-when=MODE
969 when to apply instantiation
970 --int-wf-ind
972 apply strengthening for integers based on well-founded induction
973 [*]
974 --ite-dtt-split-quant
976 split ites with dt testers as conditions [*]
977 --ite-lift-quant=MODE
979 ite lifting mode for quantified formulas
980 --literal-matching=MODE
982 choose literal matching mode
983 --local-t-ext
985 do instantiation based on local theory extensions [*]
986 --lte-partial-inst
988 partially instantiate local theory quantifiers [*]
989 --lte-restrict-inst-closure
991 treat arguments of inst closure as restricted terms for instan‐
992 tiation [*]
993 --macros-quant
995 perform quantifiers macro expansion [*]
996 --macros-quant-mode=MODE
998 mode for quantifiers macro expansion
999 --mbqi-interleave
1001 interleave model-based quantifier instantiation with other tech‐
1002 niques [*]
1003 --mbqi-one-inst-per-round
1005 only add one instantiation per quantifier per round for mbqi [*]
1006 --mbqi-one-quant-per-round
1008 only add instantiations for one quantifier per round for mbqi
1009 [*]
1010 --mbqi=MODE
1012 choose mode for model-based quantifier instantiation
1013 --miniscope-quant
1015 miniscope quantifiers [*]
1016 --miniscope-quant-fv
1018 miniscope quantifiers for ground subformulas [*]
1019 --multi-trigger-cache
1021 caching version of multi triggers [*]
1022 --multi-trigger-linear
1024 implementation of multi triggers where maximum number of instan‐
1025 tiations is linear wrt number of ground terms [*]
1026 --multi-trigger-priority
1028 only try multi triggers if single triggers give no instantia‐
1029 tions [*]
1030 --multi-trigger-when-single
1032 select multi triggers when single triggers exist [*]
1033 --partial-triggers
1035 use triggers that do not contain all free variables [*]
1036 --pre-skolem-quant
1038 apply skolemization eagerly to bodies of quantified formulas [*]
1039 --pre-skolem-quant-agg
1041 apply skolemization to quantified formulas aggressively [*]
1042 --pre-skolem-quant-nested
1044 apply skolemization to nested quantified formulas [*]
1045 --prenex-quant-user
1047 prenex quantified formulas with user patterns [*]
1048 --prenex-quant=MODE
1050 prenex mode for quantified formulas
1051 --pure-th-triggers
1053 use pure theory terms as single triggers [*]
1054 --purify-dt-triggers
1056 purify dt triggers, match all constructors of correct form
1057 instead of selectors [*]
1058 --purify-triggers
1060 purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 [*]
1061 --qcf-all-conflict
1063 add all available conflicting instances during conflict-based
1064 instantiation [*]
1065 --qcf-eager-check-rd
1067 optimization, eagerly check relevant domain of matched position
1068 [*]
1069 --qcf-eager-test
1071 optimization, test qcf instances eagerly [*]
1072 --qcf-nested-conflict
1074 consider conflicts for nested quantifiers [*]
1075 --qcf-skip-rd
1077 optimization, skip instances based on possibly irrelevant por‐
1078 tions of quantified formulas [*]
1079 --qcf-tconstraint
1081 enable entailment checks for t-constraints in qcf algorithm [*]
1082 --qcf-vo-exp
1084 qcf experimental variable ordering [*]
1085 --quant-alpha-equiv
1087 infer alpha equivalence between quantified formulas [*]
1088 --quant-anti-skolem
1090 perform anti-skolemization for quantified formulas [*]
1091 --quant-cf
1093 enable conflict find mechanism for quantifiers [*]
1094 --quant-cf-mode=MODE
1096 what effort to apply conflict find mechanism
1097 --quant-cf-when=MODE
1099 when to invoke conflict find mechanism for quantifiers
1100 --quant-dsplit-mode=MODE
1102 mode for dynamic quantifiers splitting
1103 --quant-epr
1105 infer whether in effectively propositional fragment, use for
1106 cbqi [*]
1107 --quant-epr-match
1109 use matching heuristics for EPR instantiation [*]
1110 --quant-fun-wd
1112 assume that function defined by quantifiers are well defined [*]
1113 --quant-ind
1115 use all available techniques for inductive reasoning [*]
1116 --quant-model-ee
1118 use equality engine of model for last call effort [*]
1119 --quant-rep-mode=MODE
1121 selection mode for representatives in quantifiers engine
1122 --quant-split
1124 apply splitting to quantified formulas based on variable dis‐
1125 joint disjuncts [*]
1126 --register-quant-body-terms
1128 consider ground terms within bodies of quantified formulas for
1129 matching [*]
1130 --relational-triggers
1132 choose relational triggers such as x = f(y), x >= f(y) [*]
1133 --relevant-triggers
1135 prefer triggers that are more relevant based on SInE style anal‐
1136 ysis [*]
1137 --rewrite-rules
1139 use rewrite rules module [*]
1140 --rr-one-inst-per-round
1142 add one instance of rewrite rule per round [*]
1143 --strict-triggers
1145 only instantiate quantifiers with user patterns based on trig‐
1146 gers [*]
1147 --sygus-add-const-grammar
1149 statically add constants appearing in conjecture to grammars [*]
1150 --sygus-auto-unfold
1152 enable approach which automatically unfolds transition systems
1153 for directly solving invariant synthesis problems [*]
1154 --sygus-bool-ite-return-const
1156 Only use Boolean constants for return values in unifica‐
1157 tion-based function synthesis [*]
1158 --sygus-eval-unfold
1160 do unfolding of sygus evaluation functions [*]
1161 --sygus-eval-unfold-bool
1163 do unfolding of Boolean evaluation functions that appear in
1164 refinement lemmas [*]
1165 --sygus-ext-rew
1167 use extended rewriter for sygus [*]
1168 --sygus-grammar-norm
1170 statically normalize sygus grammars based on flattening (lin‐
1171 earization) [*]
1172 --sygus-inference
1174 attempt to preprocess arbitrary inputs to sygus conjectures [*]
1175 --sygus-inv-templ-when-sg
1177 use invariant templates (with solution reconstruction) for syn‐
1178 tax guided problems [*]
1179 --sygus-inv-templ=MODE
1181 template mode for sygus invariant synthesis (weaken pre-condi‐
1182 tion, strengthen post-condition, or none)
1183 --sygus-min-grammar
1185 statically minimize sygus grammars [*]
1186 --sygus-pbe
1188 enable approach which unifies conditional solutions, specialized
1189 for programming-by-examples (pbe) conjectures [*]
1190 --sygus-qe-preproc
1192 use quantifier elimination as a preprocessing step for sygus [*]
1193 --sygus-ref-eval
1195 direct evaluation of refinement lemmas for conflict analysis [*]
1196 --sygus-repair-const
1198 use approach to repair constants in sygus candidate solutions
1199 [*]
1200 --sygus-rr
1202 use sygus to enumerate and verify correctness of rewrite rules
1203 via sampling [*]
1204 --sygus-rr-synth
1206 use sygus to enumerate candidate rewrite rules via sampling [*]
1207 --sygus-rr-synth-accel
1209 add dynamic symmetry breaking clauses based on candidate
1210 rewrites [*]
1211 --sygus-rr-synth-check
1213 use satisfiability check to verify correctness of candidate
1214 rewrites [*]
1215 --sygus-rr-synth-filter-cong
1217 filter candidate rewrites based on congruence [*]
1218 --sygus-rr-synth-filter-match
1220 filter candidate rewrites based on matching [*]
1221 --sygus-rr-synth-filter-order
1223 filter candidate rewrites based on variable ordering [*]
1224 --sygus-rr-verify
1226 use sygus to verify the correctness of rewrite rules via sam‐
1227 pling [*]
1228 --sygus-rr-verify-abort
1230 abort when sygus-rr-verify finds an instance of unsoundness [*]
1231 --sygus-sample-grammar
1233 when applicable, use grammar for choosing sample points [*]
1234 --sygus-samples=N
1236 number of points to consider when doing sygus rewriter sample
1237 testing
1238 --sygus-stream
1240 enumerate a stream of solutions instead of terminating after the
1241 first one [*]
1242 --sygus-templ-embed-grammar
1244 embed sygus templates into grammars [*]
1245 --sygus-unif
1247 Unification-based function synthesis [*]
1248 --term-db-mode
1250 which ground terms to consider for instantiation
1251 --track-inst-lemmas
1253 track instantiation lemmas (for proofs, unsat cores, qe and syn‐
1254 thesis minimization) [*]
1255 --trigger-active-sel
1257 selection mode to activate triggers
1258 --trigger-sel
1260 selection mode for triggers
1261 --user-pat=MODE
1263 policy for handling user-provided patterns for quantifier
1264 instantiation
1265 --var-elim-quant
1267 enable simple variable elimination for quantified formulas [*]
1268 --var-ineq-elim-quant
1270 enable variable elimination based on infinite projection of
1271 unbound arithmetic variables [*]
1272
1274 --sep-check-neg
1275 check negated spatial assertions [*]
1276 --sep-child-refine
1278 child-specific refinements of negated star, positive wand [*]
1279 --sep-deq-c
1281 assume cardinality elements are distinct [*]
1282 --sep-exp
1284 experimental flag for sep [*]
1285 --sep-min-refine
1287 only add refinement lemmas for minimal (innermost) assertions
1288 [*]
1289 --sep-pre-skolem-emp
1291 eliminate emp constraint at preprocess time [*]
1292
1294 --sets-ext
1295 enable extended symbols such as complement and universe in the‐
1296 ory of sets [*]
1297 --sets-infer-as-lemmas
1299 send inferences as lemmas [*]
1300 --sets-proxy-lemmas
1302 introduce proxy variables eagerly to shorten lemmas [*]
1303 --sets-rel-eager
1305 standard effort checks for relations [*]
1306
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 --bitblast-step
1313 amount of resources spent for each bitblast step (EXPERTS only)
1314 --bv-sat-conflict-step
1316 amount of resources spent for each sat conflict (bitvectors)
1317 (EXPERTS only)
1318 --check-models
1320 after SAT/INVALID/UNKNOWN, check that the generated model satis‐
1321 fies user assertions [*]
1322 --check-proofs
1324 after UNSAT/VALID, machine-check the generated proof [*]
1325 --check-synth-sol
1327 checks whether produced solutions to functions-to-synthesize
1328 satisfy the conjecture [*]
1329 --check-unsat-cores
1331 after UNSAT/VALID, produce and check an unsat core (expensive)
1332 [*]
1333 --cnf-step
1335 amount of resources spent for each call to cnf conversion
1336 (EXPERTS only)
1337 --decision-step
1339 amount of getNext decision calls in the decision engine (EXPERTS
1340 only)
1341 --dump-instantiations
1343 output instantiations of quantified formulas after every
1344 UNSAT/VALID response [*]
1345 --dump-models
1347 output models after every SAT/INVALID/UNKNOWN response [*]
1348 --dump-proofs
1350 output proofs after every UNSAT/VALID response [*]
1351 --dump-synth
1353 output solution for synthesis conjectures after every
1354 UNSAT/VALID response [*]
1355 --dump-unsat-cores
1357 output unsat cores after every UNSAT/VALID response [*]
1358 --dump-unsat-cores-full
1360 dump the full unsat core, including unlabeled assertions [*]
1361 --ext-rew-prep
1363 use extended rewriter as a preprocessing pass [*]
1364 --ext-rew-prep-agg
1366 use aggressive extended rewriter as a preprocessing pass [*]
1367 --force-logic=LOGIC
1369 set the logic, and override all further user attempts to change
1370 it (EXPERTS only)
1371 --force-no-limit-cpu-while-dump
1373 Force no CPU limit when dumping models and proofs [*]
1374 --ite-simp
1376 turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
1377 [*]
1378 --lemma-step
1380 amount of resources spent when adding lemmas (EXPERTS only)
1381 --model-u-dt-enum
1383 in models, output uninterpreted sorts as datatype enumerations
1384 [*]
1385 --omit-dont-cares
1387 When producing a model, omit variables whose value does not mat‐
1388 ter [*]
1389 --on-repeat-ite-simp
1391 do the ite simplification pass again if repeating simplification
1392 [*]
1393 --parse-step
1395 amount of resources spent for each command/expression parsing
1396 (EXPERTS only)
1397 --preprocess-step
1399 amount of resources spent for each preprocessing step in
1400 SmtEngine (EXPERTS only)
1401 --produce-assignments
1403 support the get-assignment command [*]
1404 --produce-unsat-assumptions
1406 turn on unsat assumptions generation [*]
1407 --produce-unsat-cores
1409 turn on unsat core generation [*]
1410 --proof
1412 turn on proof generation [*]
1413 --quantifier-step
1415 amount of resources spent for quantifier instantiations (EXPERTS
1416 only)
1417 --repeat-simp
1419 make multiple passes with nonclausal simplifier [*]
1420 --restart-step
1422 amount of resources spent for each theory restart (EXPERTS only)
1423 --rewrite-apply-to-const
1425 eliminate function applications, rewriting e.g. f(5) to a new
1426 symbol f_5 (EXPERTS only) [*]
1427 --rewrite-step
1429 amount of resources spent for each rewrite step (EXPERTS only)
1430 --sat-conflict-step
1432 amount of resources spent for each sat conflict (main sat
1433 solver) (EXPERTS only)
1434 --simp-ite-compress
1436 enables compressing ites after ite simplification [*]
1437 --simp-ite-hunt-zombies
1439 post ite compression enables zombie removal while the number of
1440 nodes is above this threshold
1441 --simp-with-care
1443 enables simplifyWithCare in ite simplificiation [*]
1444 --simplification=MODE
1446 choose simplification mode, see --simplification=help
1447 --sort-inference
1449 calculate sort inference of input problem, convert the input
1450 based on monotonic sorts [*]
1451 --static-learning
1453 use static learning (on by default) [*]
1454 --sygus-out=MODE
1456 output mode for sygus
1457 --sygus-print-callbacks
1459 use sygus print callbacks to print sygus terms in the user-pro‐
1460 vided form (disable for debugging) [*]
1461 --symmetry-breaker-exp
1463 generate symmetry breaking constraints after symmetry detection
1464 [*]
1465 --theory-check-step
1467 amount of resources spent for each theory check call (EXPERTS
1468 only)
1469 --unconstrained-simp
1471 turn on unconstrained simplification (see Bruttomesso/Brummayer
1472 PhD thesis) [*]
1473 --no-simplification
1475 turn off all simplification (same as --simplification=none)
1476
1478 --strings-abort-loop
1479 abort when a looping word equation is encountered [*]
1480 --strings-binary-csp
1482 use binary search when splitting strings [*]
1483 --strings-check-entail-len
1485 check entailment between length terms to reduce splitting [*]
1486 --strings-eager
1488 strings eager check [*]
1489 --strings-eager-len
1491 strings eager length lemmas [*]
1492 --strings-eit
1494 the eager intersection used by the theory of strings [*]
1495 --strings-exp
1497 experimental features in the theory of strings [*]
1498 --strings-fmf
1500 the finite model finding used by the theory of strings [*]
1501 --strings-guess-model
1503 use model guessing to avoid string extended function reductions
1504 [*]
1505 --strings-infer-as-lemmas
1507 always send lemmas out instead of making internal inferences [*]
1508 --strings-infer-sym
1510 strings split on empty string [*]
1511 --strings-inm
1513 internal for strings: ignore negative membership constraints
1514 (fragment checking is needed, left to users for now) [*]
1515 --strings-lazy-pp
1517 perform string preprocessing lazily [*]
1518 --strings-lb=N
1520 the strategy of LB rule application: 0-lazy, 1-eager, 2-no
1521 --strings-len-geqz
1523 strings length greater than zero lemmas [*]
1524 --strings-len-norm
1526 strings length normalization lemma [*]
1527 --strings-lprop-csp
1529 do length propagation based on constant splits [*]
1530 --strings-min-prefix-explain
1532 minimize explanations for prefix of normal forms in strings [*]
1533 --strings-opt1
1535 internal option1 for strings: normal form [*]
1536 --strings-opt2
1538 internal option2 for strings: constant regexp splitting [*]
1539 --strings-print-ascii
1541 the alphabet contains only printable characters from the stan‐
1542 dard extended ASCII [*]
1543 --strings-process-loop
1545 reduce looping word equations to regular expressions [*]
1546 --strings-rexplain-lemmas
1548 regression explanations for string lemmas [*]
1549 --strings-sp-emp
1551 strings split on empty string [*]
1552 --strings-uf-reduct
1554 use uninterpreted functions when applying extended function
1555 reductions [*]
1556
1558 --assign-function-values
1559 assign values for uninterpreted functions in models [*]
1560 --condense-function-values
1562 condense values for functions in models rather than explicitly
1563 representing them [*]
1564 --theoryof-mode=MODE
1566 mode for Theory::theoryof() (EXPERTS only)
1567 --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
1573 --symmetry-breaker
1574 use UF symmetry breaker (Deharbe et al., CADE 2011) [*]
1575 --uf-ho
1577 enable support for higher-order reasoning [*]
1578 --uf-ho-ext
1580 apply extensionality on function symbols [*]
1581 --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 --uf-ss-clique-splits
1588 use cliques instead of splitting on demand to shrink model [*]
1589 --uf-ss-eager-split
1591 add splits eagerly for uf strong solver [*]
1592 --uf-ss-fair
1594 use fair strategy for finite model finding multiple sorts [*]
1595 --uf-ss-fair-monotone
1597 group monotone sorts when enforcing fairness for finite model
1598 finding [*]
1599 --uf-ss-regions
1601 disable region-based method for discovering cliques and splits
1602 in uf strong solver [*]
1603 --uf-ss-totality
1605 always use totality axioms for enforcing cardinality constraints
1606 [*]
1607 --uf-ss-totality-limited=N
1609 apply totality axioms, but only up to cardinality N (-1 == do
1610 not apply totality axioms, default)
1611 --uf-ss-totality-sym-break
1613 apply symmetry breaking for totality axioms [*]
1614 --uf-ss=MODE
1616 mode of operation for uf strong solver.
1617 Each option marked with [*] has a --no-OPTIONNAME variant, which
1620 reverses the sense of the option.
1621
1624 CVC4 reports all syntactic and semantic errors on standard error.
1625
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 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 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 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 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 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
1669 This manual page refers to CVC4 version 1.6.
1670
1672 An issue tracker for the CVC4 project is maintained at
1673 https://github.com/CVC4/CVC4/issues.
1674
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
1681 libcvc4(3), libcvc4parser(3), libcvc4compat(3)
1682 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/.
1686CVC4 release 1.6 February 2019 CVC4(1)