1OPTIONS(3cvc) CVC4 Internals Documentation OPTIONS(3cvc)
2
6 options - the options infrastructure
7
10 COMMON OPTIONS
11 inputLanguage
13 (InputLanguage, default = language::input::LANG_AUTO)
14 force input language (default is "auto"; see --lang
15 help)
16 outputLanguage
18 (OutputLanguage, default = language::out‐
19 put::LANG_AUTO)
20 force output language (default is "auto"; see --out‐
21 put-lang help)
22 statistics
24 (bool)
25 give statistics on exit
26 help (bool)
28 full command line reference
29 seed (uint64_t, default = 0)
31 seed for random number generator
32 version (bool)
34 identify this CVC4 binary
35 strictParsing
37 (bool)
38 be less tolerant of non-conforming inputs
39 cpuTime (bool, default = false)
41 measures CPU time if set to true and wall time if
42 false (default false)
43 dumpToFileName
45 (std::string)
46 all dumping goes to FILE (instead of stdout)
47 dumpModeString
49 (std::string)
50 dump preprocessed assertions, etc., see --dump=help
51 hardLimit (bool, default = false)
53 the resource limit is hard potentially leaving the
54 smtEngine in an unsafe state (should be destroyed and
55 rebuild after resourcing out)
56 incrementalSolving
58 (bool, default = true)
59 enable incremental solving
60 produceAssertions
62 (bool)
63 keep an assertions list (enables get-assertions com‐
64 mand)
65 produceModels
67 (bool, default = false)
68 support the get-value and get-model commands
69 perCallResourceLimit
71 (unsigned long)
72 enable resource limiting per query
73 cumulativeResourceLimit
75 (unsigned long)
76 enable resource limiting (currently, roughly the num‐
77 ber of SAT conflicts)
78 perCallMillisecondLimit
80 (unsigned long)
81 enable time limiting per query (give milliseconds)
82 cumulativeMillisecondLimit
84 (unsigned long)
85 enable time limiting (give milliseconds)
86 ARITHMETIC THEORY OPTIONS
89 maxApproxDepth
91 (int16_t, default = 200)
92 maximum branch depth the approximate solver is allowed
93 to take
94 arithNoPartialFun
96 (bool, default = false)
97 do not use partial function semantics for arithmetic
98 (not SMT LIB compliant)
99 arithPropAsLemmaLength
101 (uint16_t, default = 8)
102 rows shorter than this are propagated as clauses
103 arithPropagationMode
105 (ArithPropagationMode, default = BOTH_PROP)
106 turns on arithmetic propagation (default is 'old', see
107 --arith-prop=help)
108 arithRewriteEq
110 (bool, default = false)
111 turns on the preprocessing rewrite turning equalities
112 into a conjunction of inequalities
113 collectPivots
115 (bool, default = false)
116 collect the pivot history
117 doCutAllBounded
119 (bool, default = false)
120 turns on the integer solving step of periodically cut‐
121 ting all integer variables that have both upper and
122 lower bounds
123 exportDioDecompositions
125 (bool, default = false)
126 let skolem variables for integer divisibility con‐
127 straints leak from the dio solver
128 dioRepeat (bool, default = false)
130 handle dio solver constraints in mass or one at a time
131 arithDioSolver
133 (bool, default = true)
134 turns on Linear Diophantine Equation solver (Griggio,
135 JSAT 2012)
136 dioSolverTurns
138 (int, default = 10)
139 turns in a row dio solver cutting gets
140 arithErrorSelectionRule
142 (ErrorSelectionRule, default = MINIMUM_AMOUNT)
143 change the pivot rule for the basic variable (default
144 is 'min', see --pivot-rule help)
145 havePenalties
147 (bool, default = false)
148 turns on degenerate pivot penalties
149 arithHeuristicPivots
151 (int16_t, default = 0)
152 the number of times to apply the heuristic pivot rule;
153 if N < 0, this defaults to the number of variables; if
154 this is unset, this is tuned by the logic selection
155 replayFailureLemma
157 (bool, default = false)
158 attempt to use external lemmas if approximate solve
159 integer failed
160 maxCutsInContext
162 (unsigned, default = 65535)
163 maximum cuts in a given context before signalling a
164 restart
165 arithMLTrick
167 (bool, default = false)
168 turns on the preprocessing step of attempting to infer
169 bounds on miplib problems
170 arithMLTrickSubstitutions
172 (unsigned, default = 1)
173 do substitution for miplib 'tmp' vars if defined in <=
174 N eliminated vars
175 newProp (bool, default = false)
177 use the new row propagation system
178 nlExt (bool, default = true)
180 extended approach to non-linear
181 nlExtEntailConflicts
183 (bool, default = false)
184 check for entailed conflicts in non-linear solver
185 nlExtFactor
187 (bool, default = true)
188 use factoring inference in non-linear solver
189 nlExtIncPrecision
191 (bool, default = true)
192 whether to increment the precision for irrational
193 function constraints
194 nlExtPurify
196 (bool, default = false)
197 purify non-linear terms at preprocess
198 nlExtResBound
200 (bool, default = false)
201 use resolution-style inference for inferring new
202 bounds
203 nlExtRewrites
205 (bool, default = true)
206 do rewrites in non-linear solver
207 nlExtSplitZero
209 (bool, default = false)
210 intial splits on zero for all variables
211 nlExtTfTaylorDegree
213 (int16_t, default = 4)
214 initial degree of polynomials for Taylor approximation
215 nlExtTfTangentPlanes
217 (bool, default = true)
218 use non-terminating tangent plane strategy for tran‐
219 scendental functions for non-linear
220 nlExtTangentPlanes
222 (bool, default = false)
223 use non-terminating tangent plane strategy for
224 non-linear
225 nlExtTangentPlanesInterleave
227 (bool, default = false)
228 interleave tangent plane strategy for non-linear
229 pbRewrites
231 (bool, default = false)
232 apply pseudo boolean rewrites
233 arithPivotThreshold
235 (uint16_t, default = 2)
236 sets the number of pivots using --pivot-rule per basic
237 variable per simplex instance before using variable
238 order
239 ppAssertMaxSubSize
241 (unsigned, default = 2)
242 threshold for substituting an equality in ppAssert
243 arithPropagateMaxLength
245 (uint16_t, default = 16)
246 sets the maximum row length to be used in propagation
247 replayEarlyCloseDepths
249 (int, default = 1)
250 multiples of the depths to try to close the approx log
251 eagerly
252 replayFailurePenalty
254 (int, default = 100)
255 number of solve integer attempts to skips after a
256 numeric failure
257 lemmaRejectCutSize
259 (unsigned, default = 25500)
260 maximum complexity of any coefficient while outputting
261 replaying cut lemmas
262 replayNumericFailurePenalty
264 (int, default = 4194304)
265 number of solve integer attempts to skips after a
266 numeric failure
267 replayRejectCutSize
269 (unsigned, default = 25500)
270 maximum complexity of any coefficient while replaying
271 cuts
272 soiApproxMajorFailure
274 (double, default = .01)
275 threshold for a major tolerance failure by the approx‐
276 imate solver
277 soiApproxMajorFailurePen
279 (int, default = 50)
280 threshold for a major tolerance failure by the approx‐
281 imate solver
282 soiApproxMinorFailure
284 (double, default = .0001)
285 threshold for a minor tolerance failure by the approx‐
286 imate solver
287 soiApproxMinorFailurePen
289 (int, default = 10)
290 threshold for a minor tolerance failure by the approx‐
291 imate solver
292 restrictedPivots
294 (bool, default = true)
295 have a pivot cap for simplex at effort levels below
296 fullEffort
297 revertArithModels
299 (bool, default = false)
300 revert the arithmetic model to a known safe model on
301 unsat if one is cached
302 rewriteDivk
304 (bool, default = false)
305 rewrite division and mod when by a constant into lin‐
306 ear terms
307 rrTurns (int, default = 3)
309 round robin turn
310 trySolveIntStandardEffort
312 (bool, default = false)
313 attempt to use the approximate solve integer method on
314 standard effort
315 arithSimplexCheckPeriod
317 (uint16_t, default = 200)
318 the number of pivots to do in simplex before recheck‐
319 ing for a conflict on all variables
320 sNormInferEq
322 (bool, default = false)
323 infer equalities based on Shostak normalization
324 soiQuickExplain
326 (bool, default = false)
327 use quick explain to minimize the sum of infeasibility
328 conflicts
329 arithStandardCheckVarOrderPivots
331 (int16_t, default = -1)
332 limits the number of pivots in a single invocation of
333 check() at a non-full effort level using Bland's pivot
334 rule (EXPERTS only)
335 arithUnateLemmaMode
337 (ArithUnateLemmaMode, default = ALL_PRESOLVE_LEMMAS)
338 determines which lemmas to add before solving (default
339 is 'all', see --unate-lemmas=help)
340 useApprox (bool, default = false)
342 attempt to use an approximate solver
343 useFC (bool, default = false)
345 use focusing and converging simplex (FMCAD 2013 sub‐
346 mission)
347 useSOI (bool, default = false)
349 use sum of infeasibility simplex (FMCAD 2013 submis‐
350 sion)
351 ARRAYS THEORY OPTIONS
353 arraysConfig
355 (int, default = 0)
356 set different array option configurations - for devel‐
357 opers only
358 arraysEagerIndexSplitting
360 (bool, default = true)
361 turn on eager index splitting for generated array lem‐
362 mas
363 arraysEagerLemmas
365 (bool, default = false)
366 turn on eager lemma generation for arrays
367 arraysLazyRIntro1
369 (bool, default = true)
370 turn on optimization to only perform RIntro1 rule
371 lazily (see Jovanovic/Barrett 2012: Being Careful with
372 Theory Combination)
373 arraysModelBased
375 (bool, default = false)
376 turn on model-based array solver
377 arraysOptimizeLinear
379 (bool, default = true)
380 turn on optimization for linear array terms (see de
381 Moura FMCAD 09 arrays paper)
382 arraysPropagate
384 (int, default = 2)
385 propagation effort for arrays: 0 is none, 1 is some, 2
386 is full
387 arraysReduceSharing
389 (bool, default = false)
390 use model information to reduce size of care graph for
391 arrays
392 arraysWeakEquivalence
394 (bool, default = false)
395 use algorithm from Christ/Hoenicke (SMT 2014)
396 BASE OPTIONS
398 binary_name
400 (std::string)
401 [undocumented]
402 err (std::ostream*, default = &std::cerr)
404 [undocumented]
405 in (std::istream*, default = &std::cin)
407 [undocumented]
408 languageHelp
410 (bool)
411 [undocumented]
412 out (std::ostream*, default = &std::cout)
414 [undocumented]
415 parseOnly (bool)
417 exit after parsing input
418 preprocessOnly
420 (bool)
421 exit after preprocessing input
422 printSuccess
424 (bool)
425 print the "success" output required of SMT-LIBv2
426 statsEveryQuery
428 (bool, default = false)
429 in incremental mode, print stats after every satisfia‐
430 bility or validity query
431 statsHideZeros
433 (bool, default = false)
434 hide statistics which are zero
435 verbosity (int, default = 0)
437 the verbosity level of CVC4
438 BITVECTOR THEORY OPTIONS
440 bitvectorAig
442 (bool, default = false)
443 bitblast by first converting to AIG (implies --bit‐
444 blast=eager)
445 bitblastMode
447 (CVC4::theory::bv::BitblastMode, default = CVC4::the‐
448 ory::bv::BITBLAST_MODE_LAZY)
449 choose bitblasting mode, see --bitblast=help
450 boolToBitvector
452 (bool, default = false)
453 convert booleans to bit-vectors of size 1 when possi‐
454 ble
455 bvAbstraction
457 (bool, default = false)
458 mcm benchmark abstraction (EXPERTS only)
459 bitvectorAigSimplifications
461 (std::string)
462 abc command to run AIG simplifications (implies --bit‐
463 blast-aig, default is "balance;drw") (EXPERTS only)
464 bvAlgExtf (bool, default = true)
466 algebraic inferences for extended functions
467 bitvectorAlgebraicBudget
469 (unsigned, default = 1500)
470 the budget allowed for the algebraic solver in number
471 of SAT conflicts (EXPERTS only)
472 bitvectorAlgebraicSolver
474 (bool, default = true)
475 turn on the algebraic solver for the bit-vector theory
476 (only if --bitblast=lazy)
477 bitvectorDivByZeroConst
479 (bool, default = false)
480 always return -1 on division by zero
481 bvEagerExplanations
483 (bool, default = false)
484 compute bit-blasting propagation explanations eagerly
485 (EXPERTS only)
486 bitvectorEqualitySlicer
488 (CVC4::theory::bv::BvSlicerMode, default = CVC4::the‐
489 ory::bv::BITVECTOR_SLICER_OFF)
490 turn on the slicing equality solver for the bit-vector
491 theory (only if --bitblast=lazy)
492 bitvectorEqualitySolver
494 (bool, default = true)
495 use the equality engine for the bit-vector theory
496 (only if --bitblast=lazy)
497 bvExtractArithRewrite
499 (bool, default = false)
500 enable rewrite pushing extract [i:0] over arithmetic
501 operations (can blow up) (EXPERTS only)
502 bvGaussElim
504 (bool, default = false)
505 simplify formula via Gaussian Elimination if applica‐
506 ble (EXPERTS only)
507 bitvectorInequalitySolver
509 (bool, default = true)
510 turn on the inequality solver for the bit-vector the‐
511 ory (only if --bitblast=lazy)
512 bvIntroducePow2
514 (bool, default = false)
515 introduce bitvector powers of two as a preprocessing
516 pass (EXPERTS only)
517 bvLazyReduceExtf
519 (bool, default = false)
520 reduce extended functions like bv2nat and int2bv at
521 last call instead of full effort
522 bvLazyRewriteExtf
524 (bool, default = true)
525 lazily rewrite extended functions like bv2nat and
526 int2bv
527 bvNumFunc (unsigned, default = 1)
529 number of function symbols in conflicts that are gen‐
530 eralized (EXPERTS only)
531 bitvectorPropagate
533 (bool, default = true)
534 use bit-vector propagation in the bit-blaster
535 bitvectorQuickXplain
537 (bool, default = false)
538 minimize bv conflicts using the QuickXplain algorithm
539 (EXPERTS only)
540 bvSatSolver
542 (CVC4::theory::bv::SatSolverMode, default = CVC4::the‐
543 ory::bv::SAT_SOLVER_MINISAT)
544 choose which sat solver to use, see
545 --bv-sat-solver=help (EXPERTS only)
546 skolemizeArguments
548 (bool, default = false)
549 skolemize arguments for bv abstraction (only does
550 something if --bv-abstraction is on) (EXPERTS only)
551 bitvectorToBool
553 (bool, default = false)
554 lift bit-vectors of size 1 to booleans when possible
555 DATATYPES THEORY OPTIONS
557 cdtBisimilar
559 (bool, default = true)
560 do bisimilarity check for co-datatypes
561 dtBinarySplit
563 (bool, default = false)
564 do binary splits for datatype constructor types
565 dtBlastSplits
567 (bool, default = false)
568 when applicable, blast splitting lemmas for all vari‐
569 ables at once
570 dtCyclic (bool, default = true)
572 do cyclicity check for datatypes
573 dtForceAssignment
575 (bool, default = false)
576 force the datatypes solver to give specific values to
577 all datatypes terms before answering sat
578 dtInferAsLemmas
580 (bool, default = false)
581 always send lemmas out instead of making internal
582 inferences
583 dtRefIntro
585 (bool, default = false)
586 introduce reference skolems for shorter explanations
587 dtRewriteErrorSel
589 (bool, default = false)
590 rewrite incorrectly applied selectors to arbitrary
591 ground term (EXPERTS only)
592 dtSharedSelectors
594 (bool, default = true)
595 internally use shared selectors across multiple con‐
596 structors
597 dtUseTesters
599 (bool, default = true)
600 do not preprocess away tester predicates
601 sygusAbortSize
603 (int, default = -1)
604 tells enumerative sygus to only consider solutions up
605 to term size N (-1 == no limit, default)
606 sygusEvalBuiltin
608 (bool, default = true)
609 use builtin kind for evaluation functions in sygus
610 sygusFairMax
612 (bool, default = true)
613 use max instead of sum for multi-function sygus con‐
614 jectures
615 sygusFair (CVC4::theory::SygusFairMode, default = CVC4::the‐
617 ory::SYGUS_FAIR_DT_SIZE)
618 if and how to apply fairness for sygus
619 sygusOpt1 (bool, default = false)
621 sygus experimental option
622 sygusSymBreak
624 (bool, default = true)
625 simple sygus sym break lemmas
626 sygusSymBreakDynamic
628 (bool, default = true)
629 dynamic sygus sym break lemmas
630 sygusSymBreakLazy
632 (bool, default = true)
633 lazily add symmetry breaking lemmas for terms
634 sygusSymBreakPbe
636 (bool, default = true)
637 sygus sym break lemmas based on pbe conjectures
638 sygusSymBreakRlv
640 (bool, default = true)
641 add relevancy conditions to symmetry breaking lemmas
642 DECISION HEURISTICS OPTIONS
644 decisionRandomWeight
646 (int, default = 0)
647 assign random weights to nodes between 0 and N-1 (0:
648 disable) (EXPERTS only)
649 decisionThreshold
651 (decision::DecisionWeight, default = 0)
652 ignore all nodes greater than threshold in first
653 attempt to pick decision (EXPERTS only)
654 decisionUseWeight
656 (bool, default = false)
657 use the weight nodes (locally, by looking at children)
658 to direct recursive search (EXPERTS only)
659 decisionWeightInternal
661 (decision::DecisionWeightInternal, default = deci‐
662 sion::DECISION_WEIGHT_INTERNAL_OFF)
663 computer weights of internal nodes using children:
664 off, max, sum, usr1 (meaning evolving) (EXPERTS only)
665 decisionMode
667 (decision::DecisionMode, default = decision::DECI‐
668 SION_STRATEGY_INTERNAL)
669 choose decision mode, see --decision=help
670 decisionStopOnly
672 (bool)
673 [undocumented]
674 EXPRESSION PACKAGE OPTIONS
676 defaultDagThresh
678 (int, default = 1)
679 dagify common subexprs appearing > N times (1 ==
680 default, 0 == don't dagify)
681 defaultExprDepth
683 (int, default = 0)
684 print exprs to depth N (0 == default, -1 == no limit)
685 earlyTypeChecking
687 (bool, default = USE_EARLY_TYPE_CHECKING_BY_DEFAULT)
688 type check expressions immediately on creation (debug
689 builds only)
690 printExprTypes
692 (bool, default = false)
693 print types with variables when printing exprs
694 typeChecking
696 (bool, default = DO_SEMANTIC_CHECKS_BY_DEFAULT)
697 never type check expressions
698 IDL OPTIONS
700 idlRewriteEq
702 (bool, default = false)
703 enable rewriting equalities into two inequalities in
704 IDL solver (default is disabled)
705 DRIVER OPTIONS
707 continuedExecution
709 (bool, default = false)
710 continue executing commands, even on error
711 earlyExit (bool, default = true)
713 do not run destructors at exit; default on except in
714 debug builds (EXPERTS only)
715 fallbackSequential
717 (bool, default = false)
718 Switch to sequential mode (instead of printing an
719 error) if it can't be solved in portfolio mode
720 sharingFilterByLength
722 (int, default = -1)
723 don't share (among portfolio threads) lemmas strictly
724 longer than N
725 incrementalParallel
727 (bool, default = false)
728 Use parallel solver even in incremental mode (may
729 print 'unknown's at times)
730 interactive
732 (bool)
733 force interactive/non-interactive mode
734 interactivePrompt
736 (bool, default = true)
737 interactive prompting while in interactive mode
738 segvSpin (bool, default = false)
740 spin on segfault/other crash waiting for gdb
741 tearDownIncremental
743 (int, default = 0)
744 implement PUSH/POP/multi-query by destroying and
745 recreating SmtEngine every N queries (EXPERTS only)
746 threadStackSize
748 (unsigned, default = 0)
749 stack size for worker threads in MB (0 means use
750 Boost/thread lib default)
751 threadArgv
753 (std::vector<std::string>)
754 Thread configuration (a string to be passed to
755 parseOptions)
756 thread_id (int, default = -1)
758 Thread ID, for internal use in case of multi-threaded
759 run
760 threads (unsigned, default = 2)
762 Total number of threads for portfolio
763 waitToJoin
765 (bool, default = true)
766 wait for other threads to join before quitting
767 (EXPERTS only)
768 PARSER OPTIONS
770 filesystemAccess
772 (bool, default = true)
773 [undocumented]
774 globalDeclarations
776 (bool, default = false)
777 force all declarations and definitions to be global
778 memoryMap (bool)
780 memory map file input
781 semanticChecks
783 (bool, default = DO_SEMANTIC_CHECKS_BY_DEFAULT)
784 disable ALL semantic checks, including type checks
785 PRINTING OPTIONS
787 instFormatMode
789 (InstFormatMode, default = INST_FORMAT_MODE_DEFAULT)
790 print format mode for instantiations, see --inst-for‐
791 mat=help
792 modelFormatMode
794 (ModelFormatMode, default = MODEL_FORMAT_MODE_DEFAULT)
795 print format mode for models, see --model-format=help
796 PROOF OPTIONS
798 aggressiveCoreMin
800 (bool, default = false)
801 turns on aggressive unsat core minimization (experi‐
802 mental)
803 allowEmptyDependencies
805 (bool, default = false)
806 if unable to track the dependencies of a rewrit‐
807 ten/preprocessed assertion, fail silently
808 fewerPreprocessingHoles
810 (bool, default = false)
811 try to eliminate preprocessing holes in proofs
812 lfscLetification
814 (bool, default = true)
815 turns on global letification in LFSC proofs
816 SAT LAYER OPTIONS
818 minisatDumpDimacs
820 (bool, default = false)
821 instead of solving minisat dumps the asserted clauses
822 in Dimacs format
823 minisatUseElim
825 (bool, default = true)
826 use Minisat elimination
827 satRandomFreq
829 (double, default = 0.0)
830 sets the frequency of random decisions in the sat
831 solver (P=0.0 by default)
832 satRandomSeed
834 (uint32_t, default = 0)
835 sets the random seed for the sat solver
836 sat_refine_conflicts
838 (bool, default = false)
839 refine theory conflict clauses (default false)
840 satRestartFirst
842 (unsigned, default = 25)
843 sets the base restart interval for the sat solver
844 (N=25 by default)
845 satRestartInc
847 (double, default = 3.0)
848 sets the restart interval increase factor for the sat
849 solver (F=3.0 by default)
850 satClauseDecay
852 (double, default = 0.999)
853 clause activity decay factor for Minisat
854 satVarDecay
856 (double, default = 0.95)
857 variable activity decay factor for Minisat
858 QUANTIFIERS OPTIONS
860 aggressiveMiniscopeQuant
862 (bool, default = false)
863 perform aggressive miniscoping for quantifiers
864 cbqi (bool, default = false)
866 turns on counterexample-based quantifier instantiation
867 cbqiAll (bool, default = false)
869 apply counterexample-based instantiation to all quan‐
870 tified formulas
871 cbqiBv (bool, default = true)
873 use word-level inversion approach for counterexam‐
874 ple-guided quantifier instantiation for bit-vectors
875 cbqiBvConcInv
877 (bool, default = true)
878 compute inverse for concat over equalities rather than
879 producing an invertibility condition
880 cbqiBvIneqMode
882 (CVC4::theory::quantifiers::CbqiBvIneqMode, default =
883 CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY)
884 choose mode for handling bit-vector inequalities with
885 counterexample-guided instantiation
886 cbqiBvInterleaveValue
888 (bool, default = false)
889 interleave model value instantiation with word-level
890 inversion approach
891 cbqiBvLinearize
893 (bool, default = true)
894 linearize adder chains for variables
895 cbqiBvRmExtract
897 (bool, default = true)
898 replaces extract terms with variables for counterexam‐
899 ple-guided instantiation for bit-vectors
900 cbqiBvSolveNl
902 (bool, default = false)
903 try to solve non-linear bv literals using model value
904 projections
905 cbqiFullEffort
907 (bool, default = false)
908 turns on full effort counterexample-based quantifier
909 instantiation, which may resort to model-value instan‐
910 tiation
911 cbqiInnermost
913 (bool, default = true)
914 only process innermost quantified formulas in coun‐
915 terexample-based quantifier instantiation
916 cbqiLitDepend
918 (bool, default = true)
919 dependency lemmas for quantifier alternation in coun‐
920 terexample-based quantifier instantiation
921 cbqiMidpoint
923 (bool, default = false)
924 choose substitutions based on midpoints of lower and
925 upper bounds for counterexample-based quantifier
926 instantiation
927 cbqiMinBounds
929 (bool, default = false)
930 use minimally constrained lower/upper bound for coun‐
931 terexample-based quantifier instantiation
932 cbqiModel (bool, default = true)
934 guide instantiations by model values for counterexam‐
935 ple-based quantifier instantiation
936 cbqiMultiInst
938 (bool, default = false)
939 when applicable, do multi instantiations per quanti‐
940 fier per round in counterexample-based quantifier
941 instantiation
942 cbqiNestedQE
944 (bool, default = false)
945 process nested quantified formulas with quantifier
946 elimination in counterexample-based quantifier instan‐
947 tiation
948 cbqiNopt (bool, default = true)
950 non-optimal bounds for counterexample-based quantifier
951 instantiation
952 cbqiPreRegInst
954 (bool, default = false)
955 preregister ground instantiations in counterexam‐
956 ple-based quantifier instantiation
957 recurseCbqi
959 (bool, default = true)
960 turns on recursive counterexample-based quantifier
961 instantiation
962 cbqiRepeatLit
964 (bool, default = false)
965 solve literals more than once in counterexample-based
966 quantifier instantiation
967 cbqiRoundUpLowerLia
969 (bool, default = false)
970 round up integer lower bounds in substitutions for
971 counterexample-based quantifier instantiation
972 cbqiSat (bool, default = true)
974 answer sat when quantifiers are asserted with coun‐
975 terexample-based quantifier instantiation
976 cbqiUseInfInt
978 (bool, default = false)
979 use integer infinity for vts in counterexample-based
980 quantifier instantiation
981 cbqiUseInfReal
983 (bool, default = false)
984 use real infinity for vts in counterexample-based
985 quantifier instantiation
986 cegisSample
988 (CVC4::theory::quantifiers::CegisSampleMode, default =
989 CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE)
990 mode for using samples in the counterexample-guided
991 inductive synthesis loop
992 ceGuidedInst
994 (bool, default = false)
995 counterexample-guided quantifier instantiation for
996 sygus
997 cegqiSingleInvAbort
999 (bool, default = false)
1000 abort if synthesis conjecture is not single invocation
1001 cegqiSingleInvPartial
1003 (bool, default = false)
1004 combined techniques for synthesis conjectures that are
1005 partially single invocation
1006 cegqiSingleInvReconstruct
1008 (bool, default = true)
1009 reconstruct solutions for single invocation conjec‐
1010 tures in original grammar
1011 cegqiSingleInvReconstructConst
1013 (bool, default = true)
1014 include constants when reconstruct solutions for sin‐
1015 gle invocation conjectures in original grammar
1016 cegqiSolMinCore
1018 (bool, default = false)
1019 minimize solutions for single invocation conjectures
1020 based on unsat core
1021 cegqiSolMinInst
1023 (bool, default = true)
1024 minimize individual instantiations for single invoca‐
1025 tion conjectures based on unsat core
1026 cegqiSingleInvMode
1028 (CVC4::theory::quantifiers::CegqiSingleInvMode,
1029 default = CVC4::theory::quanti‐
1030 fiers::CEGQI_SI_MODE_NONE)
1031 mode for processing single invocation synthesis con‐
1032 jectures
1033 condRewriteQuant
1035 (bool, default = true)
1036 conditional rewriting of quantified formulas
1037 condVarSplitQuantAgg
1039 (bool, default = false)
1040 aggressive split quantified formulas that lead to
1041 variable eliminations
1042 condVarSplitQuant
1044 (bool, default = true)
1045 split quantified formulas that lead to variable elimi‐
1046 nations
1047 conjectureFilterActiveTerms
1049 (bool, default = true)
1050 filter based on active terms
1051 conjectureFilterCanonical
1053 (bool, default = true)
1054 filter based on canonicity
1055 conjectureFilterModel
1057 (bool, default = true)
1058 filter based on model
1059 conjectureGen
1061 (bool, default = false)
1062 generate candidate conjectures for inductive proofs
1063 conjectureGenGtEnum
1065 (int, default = 50)
1066 number of ground terms to generate for model filtering
1067 conjectureGenMaxDepth
1069 (int, default = 3)
1070 maximum depth of terms to consider for conjectures
1071 conjectureGenPerRound
1073 (int, default = 1)
1074 number of conjectures to generate per instantiation
1075 round
1076 conjectureUeeIntro
1078 (bool, default = false)
1079 more aggressive merging for universal equality engine,
1080 introduces terms
1081 conjectureNoFilter
1083 (bool, default = false)
1084 do not filter conjectures
1085 dtStcInduction
1087 (bool, default = false)
1088 apply strengthening for existential quantification
1089 over datatypes based on structural induction
1090 dtVarExpandQuant
1092 (bool, default = true)
1093 expand datatype variables bound to one constructor in
1094 quantifiers
1095 eMatching (bool, default = true)
1097 whether to do heuristic E-matching
1098 elimExtArithQuant
1100 (bool, default = true)
1101 eliminate extended arithmetic symbols in quantified
1102 formulas
1103 elimTautQuant
1105 (bool, default = true)
1106 eliminate tautological disjuncts of quantified formu‐
1107 las
1108 finiteModelFind
1110 (bool, default = false)
1111 use finite model finding heuristic for quantifier
1112 instantiation
1113 fmfBound (bool, default = false)
1115 finite model finding on bounded quantification
1116 fmfBoundInt
1118 (bool, default = false)
1119 finite model finding on bounded integer quantification
1120 fmfBoundLazy
1122 (bool, default = false)
1123 enforce bounds for bounded quantification lazily via
1124 use of proxy variables
1125 fmfBoundMinMode
1127 (CVC4::theory::quantifiers::FmfBoundMinMode, default =
1128 CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE)
1129 mode for which types of bounds to minimize via first
1130 decision heuristics
1131 fmfEmptySorts
1133 (bool, default = false)
1134 allow finite model finding to assume sorts that do not
1135 occur in ground assertions are empty
1136 fmfFmcSimple
1138 (bool, default = true)
1139 simple models in full model check for finite model
1140 finding
1141 fmfFreshDistConst
1143 (bool, default = false)
1144 use fresh distinguished representative when applying
1145 Inst-Gen techniques
1146 fmfFunWellDefined
1148 (bool, default = false)
1149 find models for recursively defined functions, assumes
1150 functions are admissible
1151 fmfFunWellDefinedRelevant
1153 (bool, default = false)
1154 find models for recursively defined functions, assumes
1155 functions are admissible, allows empty type when func‐
1156 tion is irrelevant
1157 fmfInstEngine
1159 (bool, default = false)
1160 use instantiation engine in conjunction with finite
1161 model finding
1162 fmfInstGen
1164 (bool, default = true)
1165 enable Inst-Gen instantiation techniques for finite
1166 model finding
1167 fmfInstGenOneQuantPerRound
1169 (bool, default = false)
1170 only perform Inst-Gen instantiation techniques on one
1171 quantifier per round
1172 fullSaturateInterleave
1174 (bool, default = false)
1175 interleave full saturate instantiation with other
1176 techniques
1177 fullSaturateQuant
1179 (bool, default = false)
1180 when all other quantifier instantiation strategies
1181 fail, instantiate with ground terms from relevant
1182 domain, then arbitrary ground terms before answering
1183 unknown
1184 fullSaturateQuantRd
1186 (bool, default = true)
1187 whether to use relevant domain first for full satura‐
1188 tion instantiation strategy
1189 globalNegate
1191 (bool, default = false)
1192 do global negation of input formula
1193 hoMatching
1195 (bool, default = true)
1196 do higher-order matching algorithm for triggers with
1197 variable operators
1198 hoMatchingVarArgPriority
1200 (bool, default = true)
1201 give priority to variable arguments over constant
1202 arguments
1203 hoMergeTermDb
1205 (bool, default = true)
1206 merge term indices modulo equality
1207 incrementTriggers
1209 (bool, default = true)
1210 generate additional triggers as needed during search
1211 inferArithTriggerEq
1213 (bool, default = false)
1214 infer equalities for trigger terms based on solving
1215 arithmetic equalities
1216 inferArithTriggerEqExp
1218 (bool, default = false)
1219 record explanations for inferArithTriggerEq
1220 instLevelInputOnly
1222 (bool, default = true)
1223 only input terms are assigned instantiation level zero
1224 instMaxLevel
1226 (int, default = -1)
1227 maximum inst level of terms used to instantiate quan‐
1228 tified formulas with (-1 == no limit, default)
1229 instNoEntail
1231 (bool, default = true)
1232 do not consider instances of quantified formulas that
1233 are currently entailed
1234 instNoModelTrue
1236 (bool, default = false)
1237 do not consider instances of quantified formulas that
1238 are currently true in model, if it is available
1239 instPropagate
1241 (bool, default = false)
1242 internal propagation for instantiations for selecting
1243 relevant instances
1244 instWhenPhase
1246 (int, default = 2)
1247 instantiation rounds quantifiers takes (>=1) before
1248 allowing theory combination to happen
1249 instWhenStrictInterleave
1251 (bool, default = true)
1252 ensure theory combination and standard quantifier
1253 effort strategies take turns
1254 instWhenTcFirst
1256 (bool, default = true)
1257 allow theory combination to happen once initially,
1258 before quantifier strategies are run
1259 instWhenMode
1261 (CVC4::theory::quantifiers::InstWhenMode, default =
1262 CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL)
1263 when to apply instantiation
1264 intWfInduction
1266 (bool, default = false)
1267 apply strengthening for integers based on well-founded
1268 induction
1269 iteDtTesterSplitQuant
1271 (bool, default = false)
1272 split ites with dt testers as conditions
1273 iteLiftQuant
1275 (CVC4::theory::quantifiers::IteLiftQuantMode, default
1276 = CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIM‐
1277 PLE)
1278 ite lifting mode for quantified formulas
1279 literalMatchMode
1281 (CVC4::theory::quantifiers::LiteralMatchMode, default
1282 = CVC4::theory::quantifiers::LITERAL_MATCH_USE)
1283 choose literal matching mode
1284 localTheoryExt
1286 (bool, default = false)
1287 do instantiation based on local theory extensions
1288 ltePartialInst
1290 (bool, default = false)
1291 partially instantiate local theory quantifiers
1292 lteRestrictInstClosure
1294 (bool, default = false)
1295 treat arguments of inst closure as restricted terms
1296 for instantiation
1297 macrosQuant
1299 (bool, default = false)
1300 perform quantifiers macro expansion
1301 macrosQuantMode
1303 (CVC4::theory::quantifiers::MacrosQuantMode, default =
1304 CVC4::theory::quanti‐
1305 fiers::MACROS_QUANT_MODE_GROUND_UF)
1306 mode for quantifiers macro expansion
1307 mbqiInterleave
1309 (bool, default = false)
1310 interleave model-based quantifier instantiation with
1311 other techniques
1312 fmfOneInstPerRound
1314 (bool, default = false)
1315 only add one instantiation per quantifier per round
1316 for mbqi
1317 fmfOneQuantPerRound
1319 (bool, default = false)
1320 only add instantiations for one quantifier per round
1321 for mbqi
1322 mbqiMode (CVC4::theory::quantifiers::MbqiMode, default =
1324 CVC4::theory::quantifiers::MBQI_FMC)
1325 choose mode for model-based quantifier instantiation
1326 miniscopeQuant
1328 (bool, default = true)
1329 miniscope quantifiers
1330 miniscopeQuantFreeVar
1332 (bool, default = true)
1333 miniscope quantifiers for ground subformulas
1334 multiTriggerCache
1336 (bool, default = false)
1337 caching version of multi triggers
1338 multiTriggerLinear
1340 (bool, default = true)
1341 implementation of multi triggers where maximum number
1342 of instantiations is linear wrt number of ground terms
1343 multiTriggerPriority
1345 (bool, default = false)
1346 only try multi triggers if single triggers give no
1347 instantiations
1348 multiTriggerWhenSingle
1350 (bool, default = false)
1351 select multi triggers when single triggers exist
1352 partialTriggers
1354 (bool, default = false)
1355 use triggers that do not contain all free variables
1356 preSkolemQuant
1358 (bool, default = false)
1359 apply skolemization eagerly to bodies of quantified
1360 formulas
1361 preSkolemQuantAgg
1363 (bool, default = true)
1364 apply skolemization to quantified formulas aggres‐
1365 sively
1366 preSkolemQuantNested
1368 (bool, default = true)
1369 apply skolemization to nested quantified formulas
1370 prenexQuantUser
1372 (bool, default = false)
1373 prenex quantified formulas with user patterns
1374 prenexQuant
1376 (CVC4::theory::quantifiers::PrenexQuantMode, default =
1377 CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE)
1378 prenex mode for quantified formulas
1379 pureThTriggers
1381 (bool, default = false)
1382 use pure theory terms as single triggers
1383 purifyDtTriggers
1385 (bool, default = false)
1386 purify dt triggers, match all constructors of correct
1387 form instead of selectors
1388 purifyTriggers
1390 (bool, default = false)
1391 purify triggers, e.g. f( x+1 ) becomes f( y ), x map‐
1392 sto y-1
1393 qcfAllConflict
1395 (bool, default = false)
1396 add all available conflicting instances during con‐
1397 flict-based instantiation
1398 qcfEagerCheckRd
1400 (bool, default = true)
1401 optimization, eagerly check relevant domain of matched
1402 position
1403 qcfEagerTest
1405 (bool, default = true)
1406 optimization, test qcf instances eagerly
1407 qcfNestedConflict
1409 (bool, default = false)
1410 consider conflicts for nested quantifiers
1411 qcfSkipRd (bool, default = false)
1413 optimization, skip instances based on possibly irrele‐
1414 vant portions of quantified formulas
1415 qcfTConstraint
1417 (bool, default = false)
1418 enable entailment checks for t-constraints in qcf
1419 algorithm
1420 qcfVoExp (bool, default = false)
1422 qcf experimental variable ordering
1423 quantAlphaEquiv
1425 (bool, default = true)
1426 infer alpha equivalence between quantified formulas
1427 quantAntiSkolem
1429 (bool, default = false)
1430 perform anti-skolemization for quantified formulas
1431 quantConflictFind
1433 (bool, default = true)
1434 enable conflict find mechanism for quantifiers
1435 qcfMode (CVC4::theory::quantifiers::QcfMode, default =
1437 CVC4::theory::quantifiers::QCF_PROP_EQ)
1438 what effort to apply conflict find mechanism
1439 qcfWhenMode
1441 (CVC4::theory::quantifiers::QcfWhenMode, default =
1442 CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT)
1443 when to invoke conflict find mechanism for quantifiers
1444 quantDynamicSplit
1446 (CVC4::theory::quantifiers::QuantDSplitMode, default =
1447 CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE)
1448 mode for dynamic quantifiers splitting
1449 quantEpr (bool, default = false)
1451 infer whether in effectively propositional fragment,
1452 use for cbqi
1453 quantEprMatching
1455 (bool, default = true)
1456 use matching heuristics for EPR instantiation
1457 quantFunWellDefined
1459 (bool, default = false)
1460 assume that function defined by quantifiers are well
1461 defined
1462 quantInduction
1464 (bool, default = false)
1465 use all available techniques for inductive reasoning
1466 quantModelEe
1468 (bool, default = false)
1469 use equality engine of model for last call effort
1470 quantRepMode
1472 (CVC4::theory::quantifiers::QuantRepMode, default =
1473 CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST)
1474 selection mode for representatives in quantifiers
1475 engine
1476 quantSplit
1478 (bool, default = true)
1479 apply splitting to quantified formulas based on vari‐
1480 able disjoint disjuncts
1481 registerQuantBodyTerms
1483 (bool, default = false)
1484 consider ground terms within bodies of quantified for‐
1485 mulas for matching
1486 relationalTriggers
1488 (bool, default = false)
1489 choose relational triggers such as x = f(y), x >= f(y)
1490 relevantTriggers
1492 (bool, default = false)
1493 prefer triggers that are more relevant based on SInE
1494 style analysis
1495 quantRewriteRules
1497 (bool, default = false)
1498 use rewrite rules module
1499 rrOneInstPerRound
1501 (bool, default = false)
1502 add one instance of rewrite rule per round
1503 strictTriggers
1505 (bool, default = false)
1506 only instantiate quantifiers with user patterns based
1507 on triggers
1508 sygusAddConstGrammar
1510 (bool, default = false)
1511 statically add constants appearing in conjecture to
1512 grammars
1513 sygusInvAutoUnfold
1515 (bool, default = true)
1516 enable approach which automatically unfolds transition
1517 systems for directly solving invariant synthesis prob‐
1518 lems
1519 sygusBoolIteReturnConst
1521 (bool, default = true)
1522 Only use Boolean constants for return values in unifi‐
1523 cation-based function synthesis
1524 sygusEvalUnfold
1526 (bool, default = true)
1527 do unfolding of sygus evaluation functions
1528 sygusEvalUnfoldBool
1530 (bool, default = true)
1531 do unfolding of Boolean evaluation functions that
1532 appear in refinement lemmas
1533 sygusExtRew
1535 (bool, default = true)
1536 use extended rewriter for sygus
1537 sygusGrammarNorm
1539 (bool, default = false)
1540 statically normalize sygus grammars based on flatten‐
1541 ing (linearization)
1542 sygusInference
1544 (bool, default = false)
1545 attempt to preprocess arbitrary inputs to sygus con‐
1546 jectures
1547 sygusInvTemplWhenSyntax
1549 (bool, default = false)
1550 use invariant templates (with solution reconstruction)
1551 for syntax guided problems
1552 sygusInvTemplMode
1554 (CVC4::theory::quantifiers::SygusInvTemplMode, default
1555 = CVC4::theory::quanti‐
1556 fiers::SYGUS_INV_TEMPL_MODE_POST)
1557 template mode for sygus invariant synthesis (weaken
1558 pre-condition, strengthen post-condition, or none)
1559 sygusMinGrammar
1561 (bool, default = true)
1562 statically minimize sygus grammars
1563 sygusUnifPbe
1565 (bool, default = true)
1566 enable approach which unifies conditional solutions,
1567 specialized for programming-by-examples (pbe) conjec‐
1568 tures
1569 sygusQePreproc
1571 (bool, default = false)
1572 use quantifier elimination as a preprocessing step for
1573 sygus
1574 sygusRefEval
1576 (bool, default = true)
1577 direct evaluation of refinement lemmas for conflict
1578 analysis
1579 sygusRepairConst
1581 (bool, default = true)
1582 use approach to repair constants in sygus candidate
1583 solutions
1584 sygusRew (bool, default = false)
1586 use sygus to enumerate and verify correctness of re‐
1587 write rules via sampling
1588 sygusRewSynth
1590 (bool, default = false)
1591 use sygus to enumerate candidate rewrite rules via
1592 sampling
1593 sygusRewSynthAccel
1595 (bool, default = false)
1596 add dynamic symmetry breaking clauses based on candi‐
1597 date rewrites
1598 sygusRewSynthCheck
1600 (bool, default = false)
1601 use satisfiability check to verify correctness of can‐
1602 didate rewrites
1603 sygusRewSynthFilterCong
1605 (bool, default = true)
1606 filter candidate rewrites based on congruence
1607 sygusRewSynthFilterMatch
1609 (bool, default = true)
1610 filter candidate rewrites based on matching
1611 sygusRewSynthFilterOrder
1613 (bool, default = true)
1614 filter candidate rewrites based on variable ordering
1615 sygusRewVerify
1617 (bool, default = false)
1618 use sygus to verify the correctness of rewrite rules
1619 via sampling
1620 sygusRewVerifyAbort
1622 (bool, default = true)
1623 abort when sygus-rr-verify finds an instance of
1624 unsoundness
1625 sygusSampleGrammar
1627 (bool, default = true)
1628 when applicable, use grammar for choosing sample
1629 points
1630 sygusSamples
1632 (int, default = 1000)
1633 number of points to consider when doing sygus rewriter
1634 sample testing
1635 sygusStream
1637 (bool, default = false)
1638 enumerate a stream of solutions instead of terminating
1639 after the first one
1640 sygusTemplEmbedGrammar
1642 (bool, default = false)
1643 embed sygus templates into grammars
1644 sygusUnif (bool, default = false)
1646 Unification-based function synthesis
1647 termDbMode
1649 (CVC4::theory::quantifiers::TermDbMode, default =
1650 CVC4::theory::quantifiers::TERM_DB_ALL)
1651 which ground terms to consider for instantiation
1652 trackInstLemmas
1654 (bool, default = false)
1655 track instantiation lemmas (for proofs, unsat cores,
1656 qe and synthesis minimization)
1657 triggerActiveSelMode
1659 (CVC4::theory::quantifiers::TriggerActiveSelMode,
1660 default = CVC4::theory::quantifiers::TRIG‐
1661 GER_ACTIVE_SEL_ALL)
1662 selection mode to activate triggers
1663 triggerSelMode
1665 (CVC4::theory::quantifiers::TriggerSelMode, default =
1666 CVC4::theory::quantifiers::TRIGGER_SEL_MIN)
1667 selection mode for triggers
1668 userPatternsQuant
1670 (CVC4::theory::quantifiers::UserPatMode, default =
1671 CVC4::theory::quantifiers::USER_PAT_MODE_TRUST)
1672 policy for handling user-provided patterns for quanti‐
1673 fier instantiation
1674 varElimQuant
1676 (bool, default = true)
1677 enable simple variable elimination for quantified for‐
1678 mulas
1679 varIneqElimQuant
1681 (bool, default = true)
1682 enable variable elimination based on infinite projec‐
1683 tion of unbound arithmetic variables
1684 SEP OPTIONS
1686 sepCheckNeg
1688 (bool, default = true)
1689 check negated spatial assertions
1690 sepChildRefine
1692 (bool, default = false)
1693 child-specific refinements of negated star, positive
1694 wand
1695 sepDisequalC
1697 (bool, default = true)
1698 assume cardinality elements are distinct
1699 sepExp (bool, default = false)
1701 experimental flag for sep
1702 sepMinimalRefine
1704 (bool, default = false)
1705 only add refinement lemmas for minimal (innermost)
1706 assertions
1707 sepPreSkolemEmp
1709 (bool, default = false)
1710 eliminate emp constraint at preprocess time
1711 SETS OPTIONS
1713 setsExt (bool, default = false)
1715 enable extended symbols such as complement and uni‐
1716 verse in theory of sets
1717 setsInferAsLemmas
1719 (bool, default = true)
1720 send inferences as lemmas
1721 setsProxyLemmas
1723 (bool, default = false)
1724 introduce proxy variables eagerly to shorten lemmas
1725 setsRelEager
1727 (bool, default = true)
1728 standard effort checks for relations
1729 SMT LAYER OPTIONS
1731 abstractValues
1733 (bool, default = false)
1734 in models, output arrays (and in future, maybe others)
1735 using abstract values, as required by the SMT-LIB
1736 standard
1737 bitblastStep
1739 (unsigned, default = 1)
1740 amount of resources spent for each bitblast step
1741 (EXPERTS only)
1742 bvSatConflictStep
1744 (unsigned, default = 1)
1745 amount of resources spent for each sat conflict
1746 (bitvectors) (EXPERTS only)
1747 checkModels
1749 (bool)
1750 after SAT/INVALID/UNKNOWN, check that the generated
1751 model satisfies user assertions
1752 checkProofs
1754 (bool)
1755 after UNSAT/VALID, machine-check the generated proof
1756 checkSynthSol
1758 (bool, default = false)
1759 checks whether produced solutions to functions-to-syn‐
1760 thesize satisfy the conjecture
1761 checkUnsatCores
1763 (bool)
1764 after UNSAT/VALID, produce and check an unsat core
1765 (expensive)
1766 cnfStep (unsigned, default = 1)
1768 amount of resources spent for each call to cnf conver‐
1769 sion (EXPERTS only)
1770 decisionStep
1772 (unsigned, default = 1)
1773 amount of getNext decision calls in the decision
1774 engine (EXPERTS only)
1775 diagnosticChannelName
1777 (std::string)
1778 set the diagnostic output channel of the solver
1779 dumpInstantiations
1781 (bool, default = false)
1782 output instantiations of quantified formulas after
1783 every UNSAT/VALID response
1784 dumpModels
1786 (bool, default = false)
1787 output models after every SAT/INVALID/UNKNOWN response
1788 dumpProofs
1790 (bool, default = false)
1791 output proofs after every UNSAT/VALID response
1792 dumpSynth (bool, default = false)
1794 output solution for synthesis conjectures after every
1795 UNSAT/VALID response
1796 dumpUnsatCores
1798 (bool, default = false)
1799 output unsat cores after every UNSAT/VALID response
1800 dumpUnsatCoresFull
1802 (bool, default = false)
1803 dump the full unsat core, including unlabeled asser‐
1804 tions
1805 expandDefinitions
1807 (bool, default = false)
1808 always expand symbol definitions in output
1809 extRewPrep
1811 (bool, default = false)
1812 use extended rewriter as a preprocessing pass
1813 extRewPrepAgg
1815 (bool, default = false)
1816 use aggressive extended rewriter as a preprocessing
1817 pass
1818 forceLogicString
1820 (std::string)
1821 set the logic, and override all further user attempts
1822 to change it (EXPERTS only)
1823 forceNoLimitCpuWhileDump
1825 (bool, default = false)
1826 Force no CPU limit when dumping models and proofs
1827 interactiveMode
1829 (bool)
1830 deprecated name for produce-assertions
1831 doITESimp (bool)
1833 turn on ite simplification (Kim (and Somenzi) et al.,
1834 SAT 2009)
1835 lemmaStep (unsigned, default = 1)
1837 amount of resources spent when adding lemmas (EXPERTS
1838 only)
1839 modelUninterpDtEnum
1841 (bool, default = false)
1842 in models, output uninterpreted sorts as datatype enu‐
1843 merations
1844 omitDontCares
1846 (bool, default = false)
1847 When producing a model, omit variables whose value
1848 does not matter
1849 doITESimpOnRepeat
1851 (bool, default = false)
1852 do the ite simplification pass again if repeating sim‐
1853 plification
1854 parseStep (unsigned, default = 1)
1856 amount of resources spent for each command/expression
1857 parsing (EXPERTS only)
1858 preprocessStep
1860 (unsigned, default = 1)
1861 amount of resources spent for each preprocessing step
1862 in SmtEngine (EXPERTS only)
1863 produceAssignments
1865 (bool, default = false)
1866 support the get-assignment command
1867 unsatAssumptions
1869 (bool, default = false)
1870 turn on unsat assumptions generation
1871 unsatCores
1873 (bool)
1874 turn on unsat core generation
1875 proof (bool, default = false)
1877 turn on proof generation
1878 quantifierStep
1880 (unsigned, default = 1)
1881 amount of resources spent for quantifier instantia‐
1882 tions (EXPERTS only)
1883 regularChannelName
1885 (std::string)
1886 set the regular output channel of the solver
1887 repeatSimp
1889 (bool)
1890 make multiple passes with nonclausal simplifier
1891 replayLogFilename
1893 (std::string)
1894 replay decisions from file
1895 replayInputFilename
1897 (std::string)
1898 replay decisions from file
1899 restartStep
1901 (unsigned, default = 1)
1902 amount of resources spent for each theory restart
1903 (EXPERTS only)
1904 rewriteApplyToConst
1906 (bool, default = false)
1907 eliminate function applications, rewriting e.g. f(5)
1908 to a new symbol f_5 (EXPERTS only)
1909 rewriteStep
1911 (unsigned, default = 1)
1912 amount of resources spent for each rewrite step
1913 (EXPERTS only)
1914 satConflictStep
1916 (unsigned, default = 1)
1917 amount of resources spent for each sat conflict (main
1918 sat solver) (EXPERTS only)
1919 compressItes
1921 (bool, default = false)
1922 enables compressing ites after ite simplification
1923 zombieHuntThreshold
1925 (uint32_t, default = 524288)
1926 post ite compression enables zombie removal while the
1927 number of nodes is above this threshold
1928 simplifyWithCareEnabled
1930 (bool, default = false)
1931 enables simplifyWithCare in ite simplificiation
1932 simplificationMode
1934 (SimplificationMode, default = SIMPLIFICA‐
1935 TION_MODE_BATCH)
1936 choose simplification mode, see --simplification=help
1937 solveIntAsBV
1939 (uint32_t, default = 0)
1940 attempt to solve a pure integer satisfiable problem by
1941 bitblasting in sufficient bitwidth (experimental)
1942 solveRealAsInt
1944 (bool, default = false)
1945 attempt to solve a pure real satisfiable problem as an
1946 integer problem (for non-linear)
1947 sortInference
1949 (bool, default = false)
1950 calculate sort inference of input problem, convert the
1951 input based on monotonic sorts
1952 doStaticLearning
1954 (bool, default = true)
1955 use static learning (on by default)
1956 sygusOut (SygusSolutionOutMode, default = SYGUS_SOL_OUT_STA‐
1958 TUS_AND_DEF)
1959 output mode for sygus
1960 sygusPrintCallbacks
1962 (bool, default = true)
1963 use sygus print callbacks to print sygus terms in the
1964 user-provided form (disable for debugging)
1965 symmetryBreakerExp
1967 (bool, default = false)
1968 generate symmetry breaking constraints after symmetry
1969 detection
1970 theoryCheckStep
1972 (unsigned, default = 1)
1973 amount of resources spent for each theory check call
1974 (EXPERTS only)
1975 unconstrainedSimp
1977 (bool, default = false)
1978 turn on unconstrained simplification (see Brut‐
1979 tomesso/Brummayer PhD thesis)
1980 STRINGS THEORY OPTIONS
1982 stringAbortLoop
1984 (bool, default = false)
1985 abort when a looping word equation is encountered
1986 stringBinaryCsp
1988 (bool, default = false)
1989 use binary search when splitting strings
1990 stringCheckEntailLen
1992 (bool, default = true)
1993 check entailment between length terms to reduce split‐
1994 ting
1995 stringEager
1997 (bool, default = false)
1998 strings eager check
1999 stringEagerLen
2001 (bool, default = true)
2002 strings eager length lemmas
2003 stringEIT (bool, default = false)
2005 the eager intersection used by the theory of strings
2006 stringExp (bool, default = false)
2008 experimental features in the theory of strings
2009 stringFMF (bool, default = false)
2011 the finite model finding used by the theory of strings
2012 stringGuessModel
2014 (bool, default = false)
2015 use model guessing to avoid string extended function
2016 reductions
2017 stringInferAsLemmas
2019 (bool, default = false)
2020 always send lemmas out instead of making internal
2021 inferences
2022 stringInferSym
2024 (bool, default = true)
2025 strings split on empty string
2026 stringIgnNegMembership
2028 (bool, default = false)
2029 internal for strings: ignore negative membership con‐
2030 straints (fragment checking is needed, left to users
2031 for now)
2032 stringLazyPreproc
2034 (bool, default = true)
2035 perform string preprocessing lazily
2036 stringLB (unsigned, default = 0)
2038 the strategy of LB rule application: 0-lazy, 1-eager,
2039 2-no
2040 stringLenGeqZ
2042 (bool, default = false)
2043 strings length greater than zero lemmas
2044 stringLenNorm
2046 (bool, default = true)
2047 strings length normalization lemma
2048 stringLenPropCsp
2050 (bool, default = false)
2051 do length propagation based on constant splits
2052 stringMinPrefixExplain
2054 (bool, default = true)
2055 minimize explanations for prefix of normal forms in
2056 strings
2057 stringOpt1
2059 (bool, default = true)
2060 internal option1 for strings: normal form
2061 stringOpt2
2063 (bool, default = false)
2064 internal option2 for strings: constant regexp split‐
2065 ting
2066 stdPrintASCII
2068 (bool, default = false)
2069 the alphabet contains only printable characters from
2070 the standard extended ASCII
2071 stringProcessLoop
2073 (bool, default = true)
2074 reduce looping word equations to regular expressions
2075 stringRExplainLemmas
2077 (bool, default = true)
2078 regression explanations for string lemmas
2079 stringSplitEmp
2081 (bool, default = true)
2082 strings split on empty string
2083 stringUfReduct
2085 (bool, default = false)
2086 use uninterpreted functions when applying extended
2087 function reductions
2088 THEORY LAYER OPTIONS
2090 assignFunctionValues
2092 (bool, default = true)
2093 assign values for uninterpreted functions in models
2094 condenseFunctionValues
2096 (bool, default = true)
2097 condense values for functions in models rather than
2098 explicitly representing them
2099 theoryOfMode
2101 (CVC4::theory::TheoryOfMode, default = CVC4::the‐
2102 ory::THEORY_OF_TYPE_BASED)
2103 mode for Theory::theoryof() (EXPERTS only)
2104 useTheoryList
2106 (std::string)
2107 use alternate theory implementation NAME (--use-the‐
2108 ory=help for a list). This option may be repeated or a
2109 comma separated list.
2110 UNINTERPRETED FUNCTIONS THEORY OPTIONS
2112 ufSymmetryBreaker
2114 (bool, default = true)
2115 use UF symmetry breaker (Deharbe et al., CADE 2011)
2116 ufHo (bool, default = false)
2118 enable support for higher-order reasoning
2119 ufHoExt (bool, default = true)
2121 apply extensionality on function symbols
2122 ufssAbortCardinality
2124 (int, default = -1)
2125 tells the uf strong solver to only consider models
2126 that interpret uninterpreted sorts of cardinality at
2127 most N (-1 == no limit, default)
2128 ufssCliqueSplits
2130 (bool, default = false)
2131 use cliques instead of splitting on demand to shrink
2132 model
2133 ufssEagerSplits
2135 (bool, default = false)
2136 add splits eagerly for uf strong solver
2137 ufssFairness
2139 (bool, default = true)
2140 use fair strategy for finite model finding multiple
2141 sorts
2142 ufssFairnessMonotone
2144 (bool, default = false)
2145 group monotone sorts when enforcing fairness for
2146 finite model finding
2147 ufssRegions
2149 (bool, default = true)
2150 disable region-based method for discovering cliques
2151 and splits in uf strong solver
2152 ufssTotality
2154 (bool, default = false)
2155 always use totality axioms for enforcing cardinality
2156 constraints
2157 ufssTotalityLimited
2159 (int, default = -1)
2160 apply totality axioms, but only up to cardinality N
2161 (-1 == do not apply totality axioms, default)
2162 ufssTotalitySymBreak
2164 (bool, default = false)
2165 apply symmetry breaking for totality axioms
2166 ufssMode (CVC4::theory::uf::UfssMode, default = CVC4::the‐
2168 ory::uf::UF_SS_FULL)
2169 mode of operation for uf strong solver.
2170
2174 This manual page refers to CVC4 version 1.6.
2175
2177 An issue tracker for the CVC4 project is maintained at
2178 https://github.com/CVC4/CVC4/issues.
2179
2181 CVC4 is developed by a team of researchers at Stanford University and
2182 the University of Iowa. See the AUTHORS file in the distribution for a
2183 full list of contributors.
2184
2186 libcvc4(3), libcvc4parser(3), libcvc4compat(3)
2187 Additionally, the CVC4 wiki contains useful information about the
2189 design and internals of CVC4. It is maintained at http://cvc4.cs.stan‐
2190 ford.edu/wiki/.
2191CVC4 release 1.6 February 2019 OPTIONS(3cvc)