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