1OPTIONS(3cvc)            CVC4 Internals Documentation            OPTIONS(3cvc)
2
3
4

NAME

6       options - the options infrastructure
7
8

AVAILABLE INTERNAL OPTIONS

10              COMMON OPTIONS
11
12              inputLanguage
13                        (InputLanguage, default = language::input::LANG_AUTO)
14                        force input language (default is "auto"; see --lang
15                        help)
16
17              outputLanguage
18                        (OutputLanguage, default = language::out‐
19                        put::LANG_AUTO)
20                        force output language (default is "auto"; see --out‐
21                        put-lang help)
22
23              statistics
24                        (bool)
25                        give statistics on exit
26
27              help      (bool)
28                        full command line reference
29
30              seed      (uint64_t, default = 0)
31                        seed for random number generator
32
33              version   (bool)
34                        identify this CVC4 binary
35
36              strictParsing
37                        (bool)
38                        be less tolerant of non-conforming inputs
39
40              cpuTime   (bool, default = false)
41                        measures CPU time if set to true and wall time if
42                        false (default false)
43
44              dumpToFileName
45                        (std::string)
46                        all dumping goes to FILE (instead of stdout)
47
48              dumpModeString
49                        (std::string)
50                        dump preprocessed assertions, etc., see --dump=help
51
52              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
57              incrementalSolving
58                        (bool, default = true)
59                        enable incremental solving
60
61              produceAssertions
62                        (bool)
63                        keep an assertions list (enables get-assertions com‐
64                        mand)
65
66              produceModels
67                        (bool, default = false)
68                        support the get-value and get-model commands
69
70              perCallResourceLimit
71                        (unsigned long)
72                        enable resource limiting per query
73
74              cumulativeResourceLimit
75                        (unsigned long)
76                        enable resource limiting (currently, roughly the num‐
77                        ber of SAT conflicts)
78
79              perCallMillisecondLimit
80                        (unsigned long)
81                        enable time limiting per query (give milliseconds)
82
83              cumulativeMillisecondLimit
84                        (unsigned long)
85                        enable time limiting (give milliseconds)
86
87
88              ARITHMETIC THEORY OPTIONS
89
90              maxApproxDepth
91                        (int16_t, default = 200)
92                        maximum branch depth the approximate solver is allowed
93                        to take
94
95              arithNoPartialFun
96                        (bool, default = false)
97                        do not use partial function semantics for arithmetic
98                        (not SMT LIB compliant)
99
100              arithPropAsLemmaLength
101                        (uint16_t, default = 8)
102                        rows shorter than this are propagated as clauses
103
104              arithPropagationMode
105                        (ArithPropagationMode, default = BOTH_PROP)
106                        turns on arithmetic propagation (default is 'old', see
107                        --arith-prop=help)
108
109              arithRewriteEq
110                        (bool, default = false)
111                        turns on the preprocessing rewrite turning equalities
112                        into a conjunction of inequalities
113
114              collectPivots
115                        (bool, default = false)
116                        collect the pivot history
117
118              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
124              exportDioDecompositions
125                        (bool, default = false)
126                        let skolem variables for integer divisibility con‐
127                        straints leak from the dio solver
128
129              dioRepeat (bool, default = false)
130                        handle dio solver constraints in mass or one at a time
131
132              arithDioSolver
133                        (bool, default = true)
134                        turns on Linear Diophantine Equation solver (Griggio,
135                        JSAT 2012)
136
137              dioSolverTurns
138                        (int, default = 10)
139                        turns in a row dio solver cutting gets
140
141              arithErrorSelectionRule
142                        (ErrorSelectionRule, default = MINIMUM_AMOUNT)
143                        change the pivot rule for the basic variable (default
144                        is 'min', see --pivot-rule help)
145
146              havePenalties
147                        (bool, default = false)
148                        turns on degenerate pivot penalties
149
150              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
156              replayFailureLemma
157                        (bool, default = false)
158                        attempt to use external lemmas if approximate solve
159                        integer failed
160
161              maxCutsInContext
162                        (unsigned, default = 65535)
163                        maximum cuts in a given context before signalling a
164                        restart
165
166              arithMLTrick
167                        (bool, default = false)
168                        turns on the preprocessing step of attempting to infer
169                        bounds on miplib problems
170
171              arithMLTrickSubstitutions
172                        (unsigned, default = 1)
173                        do substitution for miplib 'tmp' vars if defined in <=
174                        N eliminated vars
175
176              newProp   (bool, default = false)
177                        use the new row propagation system
178
179              nlExt     (bool, default = true)
180                        extended approach to non-linear
181
182              nlExtEntailConflicts
183                        (bool, default = false)
184                        check for entailed conflicts in non-linear solver
185
186              nlExtFactor
187                        (bool, default = true)
188                        use factoring inference in non-linear solver
189
190              nlExtIncPrecision
191                        (bool, default = true)
192                        whether to increment the precision for irrational
193                        function constraints
194
195              nlExtPurify
196                        (bool, default = false)
197                        purify non-linear terms at preprocess
198
199              nlExtResBound
200                        (bool, default = false)
201                        use resolution-style inference for inferring new
202                        bounds
203
204              nlExtRewrites
205                        (bool, default = true)
206                        do rewrites in non-linear solver
207
208              nlExtSplitZero
209                        (bool, default = false)
210                        intial splits on zero for all variables
211
212              nlExtTfTaylorDegree
213                        (int16_t, default = 4)
214                        initial degree of polynomials for Taylor approximation
215
216              nlExtTfTangentPlanes
217                        (bool, default = true)
218                        use non-terminating tangent plane strategy for tran‐
219                        scendental functions for non-linear
220
221              nlExtTangentPlanes
222                        (bool, default = false)
223                        use non-terminating tangent plane strategy for
224                        non-linear
225
226              nlExtTangentPlanesInterleave
227                        (bool, default = false)
228                        interleave tangent plane strategy for non-linear
229
230              pbRewrites
231                        (bool, default = false)
232                        apply pseudo boolean rewrites
233
234              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
240              ppAssertMaxSubSize
241                        (unsigned, default = 2)
242                        threshold for substituting an equality in ppAssert
243
244              arithPropagateMaxLength
245                        (uint16_t, default = 16)
246                        sets the maximum row length to be used in propagation
247
248              replayEarlyCloseDepths
249                        (int, default = 1)
250                        multiples of the depths to try to close the approx log
251                        eagerly
252
253              replayFailurePenalty
254                        (int, default = 100)
255                        number of solve integer attempts to skips after a
256                        numeric failure
257
258              lemmaRejectCutSize
259                        (unsigned, default = 25500)
260                        maximum complexity of any coefficient while outputting
261                        replaying cut lemmas
262
263              replayNumericFailurePenalty
264                        (int, default = 4194304)
265                        number of solve integer attempts to skips after a
266                        numeric failure
267
268              replayRejectCutSize
269                        (unsigned, default = 25500)
270                        maximum complexity of any coefficient while replaying
271                        cuts
272
273              soiApproxMajorFailure
274                        (double, default = .01)
275                        threshold for a major tolerance failure by the approx‐
276                        imate solver
277
278              soiApproxMajorFailurePen
279                        (int, default = 50)
280                        threshold for a major tolerance failure by the approx‐
281                        imate solver
282
283              soiApproxMinorFailure
284                        (double, default = .0001)
285                        threshold for a minor tolerance failure by the approx‐
286                        imate solver
287
288              soiApproxMinorFailurePen
289                        (int, default = 10)
290                        threshold for a minor tolerance failure by the approx‐
291                        imate solver
292
293              restrictedPivots
294                        (bool, default = true)
295                        have a pivot cap for simplex at effort levels below
296                        fullEffort
297
298              revertArithModels
299                        (bool, default = false)
300                        revert the arithmetic model to a known safe model on
301                        unsat if one is cached
302
303              rewriteDivk
304                        (bool, default = false)
305                        rewrite division and mod when by a constant into lin‐
306                        ear terms
307
308              rrTurns   (int, default = 3)
309                        round robin turn
310
311              trySolveIntStandardEffort
312                        (bool, default = false)
313                        attempt to use the approximate solve integer method on
314                        standard effort
315
316              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
321              sNormInferEq
322                        (bool, default = false)
323                        infer equalities based on Shostak normalization
324
325              soiQuickExplain
326                        (bool, default = false)
327                        use quick explain to minimize the sum of infeasibility
328                        conflicts
329
330              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
336              arithUnateLemmaMode
337                        (ArithUnateLemmaMode, default = ALL_PRESOLVE_LEMMAS)
338                        determines which lemmas to add before solving (default
339                        is 'all', see --unate-lemmas=help)
340
341              useApprox (bool, default = false)
342                        attempt to use an approximate solver
343
344              useFC     (bool, default = false)
345                        use focusing and converging simplex (FMCAD 2013 sub‐
346                        mission)
347
348              useSOI    (bool, default = false)
349                        use sum of infeasibility simplex (FMCAD 2013 submis‐
350                        sion)
351
352              ARRAYS THEORY OPTIONS
353
354              arraysConfig
355                        (int, default = 0)
356                        set different array option configurations - for devel‐
357                        opers only
358
359              arraysEagerIndexSplitting
360                        (bool, default = true)
361                        turn on eager index splitting for generated array lem‐
362                        mas
363
364              arraysEagerLemmas
365                        (bool, default = false)
366                        turn on eager lemma generation for arrays
367
368              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
374              arraysModelBased
375                        (bool, default = false)
376                        turn on model-based array solver
377
378              arraysOptimizeLinear
379                        (bool, default = true)
380                        turn on optimization for linear array terms (see de
381                        Moura FMCAD 09 arrays paper)
382
383              arraysPropagate
384                        (int, default = 2)
385                        propagation effort for arrays: 0 is none, 1 is some, 2
386                        is full
387
388              arraysReduceSharing
389                        (bool, default = false)
390                        use model information to reduce size of care graph for
391                        arrays
392
393              arraysWeakEquivalence
394                        (bool, default = false)
395                        use algorithm from Christ/Hoenicke (SMT 2014)
396
397              BASE OPTIONS
398
399              binary_name
400                        (std::string)
401                        [undocumented]
402
403              err       (std::ostream*, default = &std::cerr)
404                        [undocumented]
405
406              in        (std::istream*, default = &std::cin)
407                        [undocumented]
408
409              languageHelp
410                        (bool)
411                        [undocumented]
412
413              out       (std::ostream*, default = &std::cout)
414                        [undocumented]
415
416              parseOnly (bool)
417                        exit after parsing input
418
419              preprocessOnly
420                        (bool)
421                        exit after preprocessing input
422
423              printSuccess
424                        (bool)
425                        print the "success" output required of SMT-LIBv2
426
427              statsEveryQuery
428                        (bool, default = false)
429                        in incremental mode, print stats after every satisfia‐
430                        bility or validity query
431
432              statsHideZeros
433                        (bool, default = false)
434                        hide statistics which are zero
435
436              verbosity (int, default = 0)
437                        the verbosity level of CVC4
438
439              BITVECTOR THEORY OPTIONS
440
441              bitvectorAig
442                        (bool, default = false)
443                        bitblast by first converting to AIG (implies --bit‐
444                        blast=eager)
445
446              bitblastMode
447                        (CVC4::theory::bv::BitblastMode, default = CVC4::the‐
448                        ory::bv::BITBLAST_MODE_LAZY)
449                        choose bitblasting mode, see --bitblast=help
450
451              boolToBitvector
452                        (bool, default = false)
453                        convert booleans to bit-vectors of size 1 when possi‐
454                        ble
455
456              bvAbstraction
457                        (bool, default = false)
458                        mcm benchmark abstraction (EXPERTS only)
459
460              bitvectorAigSimplifications
461                        (std::string)
462                        abc command to run AIG simplifications (implies --bit‐
463                        blast-aig, default is "balance;drw") (EXPERTS only)
464
465              bvAlgExtf (bool, default = true)
466                        algebraic inferences for extended functions
467
468              bitvectorAlgebraicBudget
469                        (unsigned, default = 1500)
470                        the budget allowed for the algebraic solver in number
471                        of SAT conflicts (EXPERTS only)
472
473              bitvectorAlgebraicSolver
474                        (bool, default = true)
475                        turn on the algebraic solver for the bit-vector theory
476                        (only if --bitblast=lazy)
477
478              bitvectorDivByZeroConst
479                        (bool, default = false)
480                        always return -1 on division by zero
481
482              bvEagerExplanations
483                        (bool, default = false)
484                        compute bit-blasting propagation explanations eagerly
485                        (EXPERTS only)
486
487              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
493              bitvectorEqualitySolver
494                        (bool, default = true)
495                        use the equality engine for the bit-vector theory
496                        (only if --bitblast=lazy)
497
498              bvExtractArithRewrite
499                        (bool, default = false)
500                        enable rewrite pushing extract [i:0] over arithmetic
501                        operations (can blow up) (EXPERTS only)
502
503              bvGaussElim
504                        (bool, default = false)
505                        simplify formula via Gaussian Elimination if applica‐
506                        ble (EXPERTS only)
507
508              bitvectorInequalitySolver
509                        (bool, default = true)
510                        turn on the inequality solver for the bit-vector the‐
511                        ory (only if --bitblast=lazy)
512
513              bvIntroducePow2
514                        (bool, default = false)
515                        introduce bitvector powers of two as a preprocessing
516                        pass (EXPERTS only)
517
518              bvLazyReduceExtf
519                        (bool, default = false)
520                        reduce extended functions like bv2nat and int2bv at
521                        last call instead of full effort
522
523              bvLazyRewriteExtf
524                        (bool, default = true)
525                        lazily rewrite extended functions like bv2nat and
526                        int2bv
527
528              bvNumFunc (unsigned, default = 1)
529                        number of function symbols in conflicts that are gen‐
530                        eralized (EXPERTS only)
531
532              bitvectorPropagate
533                        (bool, default = true)
534                        use bit-vector propagation in the bit-blaster
535
536              bitvectorQuickXplain
537                        (bool, default = false)
538                        minimize bv conflicts using the QuickXplain algorithm
539                        (EXPERTS only)
540
541              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
547              skolemizeArguments
548                        (bool, default = false)
549                        skolemize arguments for bv abstraction (only does
550                        something if --bv-abstraction is on) (EXPERTS only)
551
552              bitvectorToBool
553                        (bool, default = false)
554                        lift bit-vectors of size 1 to booleans when possible
555
556              DATATYPES THEORY OPTIONS
557
558              cdtBisimilar
559                        (bool, default = true)
560                        do bisimilarity check for co-datatypes
561
562              dtBinarySplit
563                        (bool, default = false)
564                        do binary splits for datatype constructor types
565
566              dtBlastSplits
567                        (bool, default = false)
568                        when applicable, blast splitting lemmas for all vari‐
569                        ables at once
570
571              dtCyclic  (bool, default = true)
572                        do cyclicity check for datatypes
573
574              dtForceAssignment
575                        (bool, default = false)
576                        force the datatypes solver to give specific values to
577                        all datatypes terms before answering sat
578
579              dtInferAsLemmas
580                        (bool, default = false)
581                        always send lemmas out instead of making internal
582                        inferences
583
584              dtRefIntro
585                        (bool, default = false)
586                        introduce reference skolems for shorter explanations
587
588              dtRewriteErrorSel
589                        (bool, default = false)
590                        rewrite incorrectly applied selectors to arbitrary
591                        ground term (EXPERTS only)
592
593              dtSharedSelectors
594                        (bool, default = true)
595                        internally use shared selectors across multiple con‐
596                        structors
597
598              dtUseTesters
599                        (bool, default = true)
600                        do not preprocess away tester predicates
601
602              sygusAbortSize
603                        (int, default = -1)
604                        tells enumerative sygus to only consider solutions up
605                        to term size N (-1 == no limit, default)
606
607              sygusEvalBuiltin
608                        (bool, default = true)
609                        use builtin kind for evaluation functions in sygus
610
611              sygusFairMax
612                        (bool, default = true)
613                        use max instead of sum for multi-function sygus con‐
614                        jectures
615
616              sygusFair (CVC4::theory::SygusFairMode, default = CVC4::the‐
617                        ory::SYGUS_FAIR_DT_SIZE)
618                        if and how to apply fairness for sygus
619
620              sygusOpt1 (bool, default = false)
621                        sygus experimental option
622
623              sygusSymBreak
624                        (bool, default = true)
625                        simple sygus sym break lemmas
626
627              sygusSymBreakDynamic
628                        (bool, default = true)
629                        dynamic sygus sym break lemmas
630
631              sygusSymBreakLazy
632                        (bool, default = true)
633                        lazily add symmetry breaking lemmas for terms
634
635              sygusSymBreakPbe
636                        (bool, default = true)
637                        sygus sym break lemmas based on pbe conjectures
638
639              sygusSymBreakRlv
640                        (bool, default = true)
641                        add relevancy conditions to symmetry breaking lemmas
642
643              DECISION HEURISTICS OPTIONS
644
645              decisionRandomWeight
646                        (int, default = 0)
647                        assign random weights to nodes between 0 and N-1 (0:
648                        disable) (EXPERTS only)
649
650              decisionThreshold
651                        (decision::DecisionWeight, default = 0)
652                        ignore all nodes greater than threshold in first
653                        attempt to pick decision (EXPERTS only)
654
655              decisionUseWeight
656                        (bool, default = false)
657                        use the weight nodes (locally, by looking at children)
658                        to direct recursive search (EXPERTS only)
659
660              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
666              decisionMode
667                        (decision::DecisionMode, default = decision::DECI‐
668                        SION_STRATEGY_INTERNAL)
669                        choose decision mode, see --decision=help
670
671              decisionStopOnly
672                        (bool)
673                        [undocumented]
674
675              EXPRESSION PACKAGE OPTIONS
676
677              defaultDagThresh
678                        (int, default = 1)
679                        dagify common subexprs appearing > N times (1 ==
680                        default, 0 == don't dagify)
681
682              defaultExprDepth
683                        (int, default = 0)
684                        print exprs to depth N (0 == default, -1 == no limit)
685
686              earlyTypeChecking
687                        (bool, default = USE_EARLY_TYPE_CHECKING_BY_DEFAULT)
688                        type check expressions immediately on creation (debug
689                        builds only)
690
691              printExprTypes
692                        (bool, default = false)
693                        print types with variables when printing exprs
694
695              typeChecking
696                        (bool, default = DO_SEMANTIC_CHECKS_BY_DEFAULT)
697                        never type check expressions
698
699              IDL OPTIONS
700
701              idlRewriteEq
702                        (bool, default = false)
703                        enable rewriting equalities into two inequalities in
704                        IDL solver (default is disabled)
705
706              DRIVER OPTIONS
707
708              continuedExecution
709                        (bool, default = false)
710                        continue executing commands, even on error
711
712              earlyExit (bool, default = true)
713                        do not run destructors at exit; default on except in
714                        debug builds (EXPERTS only)
715
716              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
721              sharingFilterByLength
722                        (int, default = -1)
723                        don't share (among portfolio threads) lemmas strictly
724                        longer than N
725
726              incrementalParallel
727                        (bool, default = false)
728                        Use parallel solver even in incremental mode (may
729                        print 'unknown's at times)
730
731              interactive
732                        (bool)
733                        force interactive/non-interactive mode
734
735              interactivePrompt
736                        (bool, default = true)
737                        interactive prompting while in interactive mode
738
739              segvSpin  (bool, default = false)
740                        spin on segfault/other crash waiting for gdb
741
742              tearDownIncremental
743                        (int, default = 0)
744                        implement PUSH/POP/multi-query by destroying and
745                        recreating SmtEngine every N queries (EXPERTS only)
746
747              threadStackSize
748                        (unsigned, default = 0)
749                        stack size for worker threads in MB (0 means use
750                        Boost/thread lib default)
751
752              threadArgv
753                        (std::vector<std::string>)
754                        Thread configuration (a string to be passed to
755                        parseOptions)
756
757              thread_id (int, default = -1)
758                        Thread ID, for internal use in case of multi-threaded
759                        run
760
761              threads   (unsigned, default = 2)
762                        Total number of threads for portfolio
763
764              waitToJoin
765                        (bool, default = true)
766                        wait for other threads to join before quitting
767                        (EXPERTS only)
768
769              PARSER OPTIONS
770
771              filesystemAccess
772                        (bool, default = true)
773                        [undocumented]
774
775              globalDeclarations
776                        (bool, default = false)
777                        force all declarations and definitions to be global
778
779              memoryMap (bool)
780                        memory map file input
781
782              semanticChecks
783                        (bool, default = DO_SEMANTIC_CHECKS_BY_DEFAULT)
784                        disable ALL semantic checks, including type checks
785
786              PRINTING OPTIONS
787
788              instFormatMode
789                        (InstFormatMode, default = INST_FORMAT_MODE_DEFAULT)
790                        print format mode for instantiations, see --inst-for‐
791                        mat=help
792
793              modelFormatMode
794                        (ModelFormatMode, default = MODEL_FORMAT_MODE_DEFAULT)
795                        print format mode for models, see --model-format=help
796
797              PROOF OPTIONS
798
799              aggressiveCoreMin
800                        (bool, default = false)
801                        turns on aggressive unsat core minimization (experi‐
802                        mental)
803
804              allowEmptyDependencies
805                        (bool, default = false)
806                        if unable to track the dependencies of a rewrit‐
807                        ten/preprocessed assertion, fail silently
808
809              fewerPreprocessingHoles
810                        (bool, default = false)
811                        try to eliminate preprocessing holes in proofs
812
813              lfscLetification
814                        (bool, default = true)
815                        turns on global letification in LFSC proofs
816
817              SAT LAYER OPTIONS
818
819              minisatDumpDimacs
820                        (bool, default = false)
821                        instead of solving minisat dumps the asserted clauses
822                        in Dimacs format
823
824              minisatUseElim
825                        (bool, default = true)
826                        use Minisat elimination
827
828              satRandomFreq
829                        (double, default = 0.0)
830                        sets the frequency of random decisions in the sat
831                        solver (P=0.0 by default)
832
833              satRandomSeed
834                        (uint32_t, default = 0)
835                        sets the random seed for the sat solver
836
837              sat_refine_conflicts
838                        (bool, default = false)
839                        refine theory conflict clauses (default false)
840
841              satRestartFirst
842                        (unsigned, default = 25)
843                        sets the base restart interval for the sat solver
844                        (N=25 by default)
845
846              satRestartInc
847                        (double, default = 3.0)
848                        sets the restart interval increase factor for the sat
849                        solver (F=3.0 by default)
850
851              satClauseDecay
852                        (double, default = 0.999)
853                        clause activity decay factor for Minisat
854
855              satVarDecay
856                        (double, default = 0.95)
857                        variable activity decay factor for Minisat
858
859              QUANTIFIERS OPTIONS
860
861              aggressiveMiniscopeQuant
862                        (bool, default = false)
863                        perform aggressive miniscoping for quantifiers
864
865              cbqi      (bool, default = false)
866                        turns on counterexample-based quantifier instantiation
867
868              cbqiAll   (bool, default = false)
869                        apply counterexample-based instantiation to all quan‐
870                        tified formulas
871
872              cbqiBv    (bool, default = true)
873                        use word-level inversion approach for counterexam‐
874                        ple-guided quantifier instantiation for bit-vectors
875
876              cbqiBvConcInv
877                        (bool, default = true)
878                        compute inverse for concat over equalities rather than
879                        producing an invertibility condition
880
881              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
887              cbqiBvInterleaveValue
888                        (bool, default = false)
889                        interleave model value instantiation with word-level
890                        inversion approach
891
892              cbqiBvLinearize
893                        (bool, default = true)
894                        linearize adder chains for variables
895
896              cbqiBvRmExtract
897                        (bool, default = true)
898                        replaces extract terms with variables for counterexam‐
899                        ple-guided instantiation for bit-vectors
900
901              cbqiBvSolveNl
902                        (bool, default = false)
903                        try to solve non-linear bv literals using model value
904                        projections
905
906              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
912              cbqiInnermost
913                        (bool, default = true)
914                        only process innermost quantified formulas in coun‐
915                        terexample-based quantifier instantiation
916
917              cbqiLitDepend
918                        (bool, default = true)
919                        dependency lemmas for quantifier alternation in coun‐
920                        terexample-based quantifier instantiation
921
922              cbqiMidpoint
923                        (bool, default = false)
924                        choose substitutions based on midpoints of lower and
925                        upper bounds for counterexample-based quantifier
926                        instantiation
927
928              cbqiMinBounds
929                        (bool, default = false)
930                        use minimally constrained lower/upper bound for coun‐
931                        terexample-based quantifier instantiation
932
933              cbqiModel (bool, default = true)
934                        guide instantiations by model values for counterexam‐
935                        ple-based quantifier instantiation
936
937              cbqiMultiInst
938                        (bool, default = false)
939                        when applicable, do multi instantiations per quanti‐
940                        fier per round in counterexample-based quantifier
941                        instantiation
942
943              cbqiNestedQE
944                        (bool, default = false)
945                        process nested quantified formulas with quantifier
946                        elimination in counterexample-based quantifier instan‐
947                        tiation
948
949              cbqiNopt  (bool, default = true)
950                        non-optimal bounds for counterexample-based quantifier
951                        instantiation
952
953              cbqiPreRegInst
954                        (bool, default = false)
955                        preregister ground instantiations in counterexam‐
956                        ple-based quantifier instantiation
957
958              recurseCbqi
959                        (bool, default = true)
960                        turns on recursive counterexample-based quantifier
961                        instantiation
962
963              cbqiRepeatLit
964                        (bool, default = false)
965                        solve literals more than once in counterexample-based
966                        quantifier instantiation
967
968              cbqiRoundUpLowerLia
969                        (bool, default = false)
970                        round up integer lower bounds in substitutions for
971                        counterexample-based quantifier instantiation
972
973              cbqiSat   (bool, default = true)
974                        answer sat when quantifiers are asserted with coun‐
975                        terexample-based quantifier instantiation
976
977              cbqiUseInfInt
978                        (bool, default = false)
979                        use integer infinity for vts in counterexample-based
980                        quantifier instantiation
981
982              cbqiUseInfReal
983                        (bool, default = false)
984                        use real infinity for vts in counterexample-based
985                        quantifier instantiation
986
987              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
993              ceGuidedInst
994                        (bool, default = false)
995                        counterexample-guided quantifier instantiation for
996                        sygus
997
998              cegqiSingleInvAbort
999                        (bool, default = false)
1000                        abort if synthesis conjecture is not single invocation
1001
1002              cegqiSingleInvPartial
1003                        (bool, default = false)
1004                        combined techniques for synthesis conjectures that are
1005                        partially single invocation
1006
1007              cegqiSingleInvReconstruct
1008                        (bool, default = true)
1009                        reconstruct solutions for single invocation conjec‐
1010                        tures in original grammar
1011
1012              cegqiSingleInvReconstructConst
1013                        (bool, default = true)
1014                        include constants when reconstruct solutions for sin‐
1015                        gle invocation conjectures in original grammar
1016
1017              cegqiSolMinCore
1018                        (bool, default = false)
1019                        minimize solutions for single invocation conjectures
1020                        based on unsat core
1021
1022              cegqiSolMinInst
1023                        (bool, default = true)
1024                        minimize individual instantiations for single invoca‐
1025                        tion conjectures based on unsat core
1026
1027              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
1034              condRewriteQuant
1035                        (bool, default = true)
1036                        conditional rewriting of quantified formulas
1037
1038              condVarSplitQuantAgg
1039                        (bool, default = false)
1040                        aggressive split quantified formulas that lead to
1041                        variable eliminations
1042
1043              condVarSplitQuant
1044                        (bool, default = true)
1045                        split quantified formulas that lead to variable elimi‐
1046                        nations
1047
1048              conjectureFilterActiveTerms
1049                        (bool, default = true)
1050                        filter based on active terms
1051
1052              conjectureFilterCanonical
1053                        (bool, default = true)
1054                        filter based on canonicity
1055
1056              conjectureFilterModel
1057                        (bool, default = true)
1058                        filter based on model
1059
1060              conjectureGen
1061                        (bool, default = false)
1062                        generate candidate conjectures for inductive proofs
1063
1064              conjectureGenGtEnum
1065                        (int, default = 50)
1066                        number of ground terms to generate for model filtering
1067
1068              conjectureGenMaxDepth
1069                        (int, default = 3)
1070                        maximum depth of terms to consider for conjectures
1071
1072              conjectureGenPerRound
1073                        (int, default = 1)
1074                        number of conjectures to generate per instantiation
1075                        round
1076
1077              conjectureUeeIntro
1078                        (bool, default = false)
1079                        more aggressive merging for universal equality engine,
1080                        introduces terms
1081
1082              conjectureNoFilter
1083                        (bool, default = false)
1084                        do not filter conjectures
1085
1086              dtStcInduction
1087                        (bool, default = false)
1088                        apply strengthening for existential quantification
1089                        over datatypes based on structural induction
1090
1091              dtVarExpandQuant
1092                        (bool, default = true)
1093                        expand datatype variables bound to one constructor in
1094                        quantifiers
1095
1096              eMatching (bool, default = true)
1097                        whether to do heuristic E-matching
1098
1099              elimExtArithQuant
1100                        (bool, default = true)
1101                        eliminate extended arithmetic symbols in quantified
1102                        formulas
1103
1104              elimTautQuant
1105                        (bool, default = true)
1106                        eliminate tautological disjuncts of quantified formu‐
1107                        las
1108
1109              finiteModelFind
1110                        (bool, default = false)
1111                        use finite model finding heuristic for quantifier
1112                        instantiation
1113
1114              fmfBound  (bool, default = false)
1115                        finite model finding on bounded quantification
1116
1117              fmfBoundInt
1118                        (bool, default = false)
1119                        finite model finding on bounded integer quantification
1120
1121              fmfBoundLazy
1122                        (bool, default = false)
1123                        enforce bounds for bounded quantification lazily via
1124                        use of proxy variables
1125
1126              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
1132              fmfEmptySorts
1133                        (bool, default = false)
1134                        allow finite model finding to assume sorts that do not
1135                        occur in ground assertions are empty
1136
1137              fmfFmcSimple
1138                        (bool, default = true)
1139                        simple models in full model check for finite model
1140                        finding
1141
1142              fmfFreshDistConst
1143                        (bool, default = false)
1144                        use fresh distinguished representative when applying
1145                        Inst-Gen techniques
1146
1147              fmfFunWellDefined
1148                        (bool, default = false)
1149                        find models for recursively defined functions, assumes
1150                        functions are admissible
1151
1152              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
1158              fmfInstEngine
1159                        (bool, default = false)
1160                        use instantiation engine in conjunction with finite
1161                        model finding
1162
1163              fmfInstGen
1164                        (bool, default = true)
1165                        enable Inst-Gen instantiation techniques for finite
1166                        model finding
1167
1168              fmfInstGenOneQuantPerRound
1169                        (bool, default = false)
1170                        only perform Inst-Gen instantiation techniques on one
1171                        quantifier per round
1172
1173              fullSaturateInterleave
1174                        (bool, default = false)
1175                        interleave full saturate instantiation with other
1176                        techniques
1177
1178              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
1185              fullSaturateQuantRd
1186                        (bool, default = true)
1187                        whether to use relevant domain first for full satura‐
1188                        tion instantiation strategy
1189
1190              globalNegate
1191                        (bool, default = false)
1192                        do global negation of input formula
1193
1194              hoMatching
1195                        (bool, default = true)
1196                        do higher-order matching algorithm for triggers with
1197                        variable operators
1198
1199              hoMatchingVarArgPriority
1200                        (bool, default = true)
1201                        give priority to variable arguments over constant
1202                        arguments
1203
1204              hoMergeTermDb
1205                        (bool, default = true)
1206                        merge term indices modulo equality
1207
1208              incrementTriggers
1209                        (bool, default = true)
1210                        generate additional triggers as needed during search
1211
1212              inferArithTriggerEq
1213                        (bool, default = false)
1214                        infer equalities for trigger terms based on solving
1215                        arithmetic equalities
1216
1217              inferArithTriggerEqExp
1218                        (bool, default = false)
1219                        record explanations for inferArithTriggerEq
1220
1221              instLevelInputOnly
1222                        (bool, default = true)
1223                        only input terms are assigned instantiation level zero
1224
1225              instMaxLevel
1226                        (int, default = -1)
1227                        maximum inst level of terms used to instantiate quan‐
1228                        tified formulas with (-1 == no limit, default)
1229
1230              instNoEntail
1231                        (bool, default = true)
1232                        do not consider instances of quantified formulas that
1233                        are currently entailed
1234
1235              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
1240              instPropagate
1241                        (bool, default = false)
1242                        internal propagation for instantiations for selecting
1243                        relevant instances
1244
1245              instWhenPhase
1246                        (int, default = 2)
1247                        instantiation rounds quantifiers takes (>=1) before
1248                        allowing theory combination to happen
1249
1250              instWhenStrictInterleave
1251                        (bool, default = true)
1252                        ensure theory combination and standard quantifier
1253                        effort strategies take turns
1254
1255              instWhenTcFirst
1256                        (bool, default = true)
1257                        allow theory combination to happen once initially,
1258                        before quantifier strategies are run
1259
1260              instWhenMode
1261                        (CVC4::theory::quantifiers::InstWhenMode, default =
1262                        CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL)
1263                        when to apply instantiation
1264
1265              intWfInduction
1266                        (bool, default = false)
1267                        apply strengthening for integers based on well-founded
1268                        induction
1269
1270              iteDtTesterSplitQuant
1271                        (bool, default = false)
1272                        split ites with dt testers as conditions
1273
1274              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
1280              literalMatchMode
1281                        (CVC4::theory::quantifiers::LiteralMatchMode, default
1282                        = CVC4::theory::quantifiers::LITERAL_MATCH_USE)
1283                        choose literal matching mode
1284
1285              localTheoryExt
1286                        (bool, default = false)
1287                        do instantiation based on local theory extensions
1288
1289              ltePartialInst
1290                        (bool, default = false)
1291                        partially instantiate local theory quantifiers
1292
1293              lteRestrictInstClosure
1294                        (bool, default = false)
1295                        treat arguments of inst closure as restricted terms
1296                        for instantiation
1297
1298              macrosQuant
1299                        (bool, default = false)
1300                        perform quantifiers macro expansion
1301
1302              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
1308              mbqiInterleave
1309                        (bool, default = false)
1310                        interleave model-based quantifier instantiation with
1311                        other techniques
1312
1313              fmfOneInstPerRound
1314                        (bool, default = false)
1315                        only add one instantiation per quantifier per round
1316                        for mbqi
1317
1318              fmfOneQuantPerRound
1319                        (bool, default = false)
1320                        only add instantiations for one quantifier per round
1321                        for mbqi
1322
1323              mbqiMode  (CVC4::theory::quantifiers::MbqiMode, default =
1324                        CVC4::theory::quantifiers::MBQI_FMC)
1325                        choose mode for model-based quantifier instantiation
1326
1327              miniscopeQuant
1328                        (bool, default = true)
1329                        miniscope quantifiers
1330
1331              miniscopeQuantFreeVar
1332                        (bool, default = true)
1333                        miniscope quantifiers for ground subformulas
1334
1335              multiTriggerCache
1336                        (bool, default = false)
1337                        caching version of multi triggers
1338
1339              multiTriggerLinear
1340                        (bool, default = true)
1341                        implementation of multi triggers where maximum number
1342                        of instantiations is linear wrt number of ground terms
1343
1344              multiTriggerPriority
1345                        (bool, default = false)
1346                        only try multi triggers if single triggers give no
1347                        instantiations
1348
1349              multiTriggerWhenSingle
1350                        (bool, default = false)
1351                        select multi triggers when single triggers exist
1352
1353              partialTriggers
1354                        (bool, default = false)
1355                        use triggers that do not contain all free variables
1356
1357              preSkolemQuant
1358                        (bool, default = false)
1359                        apply skolemization eagerly to bodies of quantified
1360                        formulas
1361
1362              preSkolemQuantAgg
1363                        (bool, default = true)
1364                        apply skolemization to quantified formulas aggres‐
1365                        sively
1366
1367              preSkolemQuantNested
1368                        (bool, default = true)
1369                        apply skolemization to nested quantified formulas
1370
1371              prenexQuantUser
1372                        (bool, default = false)
1373                        prenex quantified formulas with user patterns
1374
1375              prenexQuant
1376                        (CVC4::theory::quantifiers::PrenexQuantMode, default =
1377                        CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE)
1378                        prenex mode for quantified formulas
1379
1380              pureThTriggers
1381                        (bool, default = false)
1382                        use pure theory terms as single triggers
1383
1384              purifyDtTriggers
1385                        (bool, default = false)
1386                        purify dt triggers, match all constructors of correct
1387                        form instead of selectors
1388
1389              purifyTriggers
1390                        (bool, default = false)
1391                        purify triggers, e.g. f( x+1 ) becomes f( y ), x map‐
1392                        sto y-1
1393
1394              qcfAllConflict
1395                        (bool, default = false)
1396                        add all available conflicting instances during con‐
1397                        flict-based instantiation
1398
1399              qcfEagerCheckRd
1400                        (bool, default = true)
1401                        optimization, eagerly check relevant domain of matched
1402                        position
1403
1404              qcfEagerTest
1405                        (bool, default = true)
1406                        optimization, test qcf instances eagerly
1407
1408              qcfNestedConflict
1409                        (bool, default = false)
1410                        consider conflicts for nested quantifiers
1411
1412              qcfSkipRd (bool, default = false)
1413                        optimization, skip instances based on possibly irrele‐
1414                        vant portions of quantified formulas
1415
1416              qcfTConstraint
1417                        (bool, default = false)
1418                        enable entailment checks for t-constraints in qcf
1419                        algorithm
1420
1421              qcfVoExp  (bool, default = false)
1422                        qcf experimental variable ordering
1423
1424              quantAlphaEquiv
1425                        (bool, default = true)
1426                        infer alpha equivalence between quantified formulas
1427
1428              quantAntiSkolem
1429                        (bool, default = false)
1430                        perform anti-skolemization for quantified formulas
1431
1432              quantConflictFind
1433                        (bool, default = true)
1434                        enable conflict find mechanism for quantifiers
1435
1436              qcfMode   (CVC4::theory::quantifiers::QcfMode, default =
1437                        CVC4::theory::quantifiers::QCF_PROP_EQ)
1438                        what effort to apply conflict find mechanism
1439
1440              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
1445              quantDynamicSplit
1446                        (CVC4::theory::quantifiers::QuantDSplitMode, default =
1447                        CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE)
1448                        mode for dynamic quantifiers splitting
1449
1450              quantEpr  (bool, default = false)
1451                        infer whether in effectively propositional fragment,
1452                        use for cbqi
1453
1454              quantEprMatching
1455                        (bool, default = true)
1456                        use matching heuristics for EPR instantiation
1457
1458              quantFunWellDefined
1459                        (bool, default = false)
1460                        assume that function defined by quantifiers are well
1461                        defined
1462
1463              quantInduction
1464                        (bool, default = false)
1465                        use all available techniques for inductive reasoning
1466
1467              quantModelEe
1468                        (bool, default = false)
1469                        use equality engine of model for last call effort
1470
1471              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
1477              quantSplit
1478                        (bool, default = true)
1479                        apply splitting to quantified formulas based on vari‐
1480                        able disjoint disjuncts
1481
1482              registerQuantBodyTerms
1483                        (bool, default = false)
1484                        consider ground terms within bodies of quantified for‐
1485                        mulas for matching
1486
1487              relationalTriggers
1488                        (bool, default = false)
1489                        choose relational triggers such as x = f(y), x >= f(y)
1490
1491              relevantTriggers
1492                        (bool, default = false)
1493                        prefer triggers that are more relevant based on SInE
1494                        style analysis
1495
1496              quantRewriteRules
1497                        (bool, default = false)
1498                        use rewrite rules module
1499
1500              rrOneInstPerRound
1501                        (bool, default = false)
1502                        add one instance of rewrite rule per round
1503
1504              strictTriggers
1505                        (bool, default = false)
1506                        only instantiate quantifiers with user patterns based
1507                        on triggers
1508
1509              sygusAddConstGrammar
1510                        (bool, default = false)
1511                        statically add constants appearing in conjecture to
1512                        grammars
1513
1514              sygusInvAutoUnfold
1515                        (bool, default = true)
1516                        enable approach which automatically unfolds transition
1517                        systems for directly solving invariant synthesis prob‐
1518                        lems
1519
1520              sygusBoolIteReturnConst
1521                        (bool, default = true)
1522                        Only use Boolean constants for return values in unifi‐
1523                        cation-based function synthesis
1524
1525              sygusEvalUnfold
1526                        (bool, default = true)
1527                        do unfolding of sygus evaluation functions
1528
1529              sygusEvalUnfoldBool
1530                        (bool, default = true)
1531                        do unfolding of Boolean evaluation functions that
1532                        appear in refinement lemmas
1533
1534              sygusExtRew
1535                        (bool, default = true)
1536                        use extended rewriter for sygus
1537
1538              sygusGrammarNorm
1539                        (bool, default = false)
1540                        statically normalize sygus grammars based on flatten‐
1541                        ing (linearization)
1542
1543              sygusInference
1544                        (bool, default = false)
1545                        attempt to preprocess arbitrary inputs to sygus con‐
1546                        jectures
1547
1548              sygusInvTemplWhenSyntax
1549                        (bool, default = false)
1550                        use invariant templates (with solution reconstruction)
1551                        for syntax guided problems
1552
1553              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
1560              sygusMinGrammar
1561                        (bool, default = true)
1562                        statically minimize sygus grammars
1563
1564              sygusUnifPbe
1565                        (bool, default = true)
1566                        enable approach which unifies conditional solutions,
1567                        specialized for programming-by-examples (pbe) conjec‐
1568                        tures
1569
1570              sygusQePreproc
1571                        (bool, default = false)
1572                        use quantifier elimination as a preprocessing step for
1573                        sygus
1574
1575              sygusRefEval
1576                        (bool, default = true)
1577                        direct evaluation of refinement lemmas for conflict
1578                        analysis
1579
1580              sygusRepairConst
1581                        (bool, default = true)
1582                        use approach to repair constants in sygus candidate
1583                        solutions
1584
1585              sygusRew  (bool, default = false)
1586                        use sygus to enumerate and verify correctness of re‐
1587                        write rules via sampling
1588
1589              sygusRewSynth
1590                        (bool, default = false)
1591                        use sygus to enumerate candidate rewrite rules via
1592                        sampling
1593
1594              sygusRewSynthAccel
1595                        (bool, default = false)
1596                        add dynamic symmetry breaking clauses based on candi‐
1597                        date rewrites
1598
1599              sygusRewSynthCheck
1600                        (bool, default = false)
1601                        use satisfiability check to verify correctness of can‐
1602                        didate rewrites
1603
1604              sygusRewSynthFilterCong
1605                        (bool, default = true)
1606                        filter candidate rewrites based on congruence
1607
1608              sygusRewSynthFilterMatch
1609                        (bool, default = true)
1610                        filter candidate rewrites based on matching
1611
1612              sygusRewSynthFilterOrder
1613                        (bool, default = true)
1614                        filter candidate rewrites based on variable ordering
1615
1616              sygusRewVerify
1617                        (bool, default = false)
1618                        use sygus to verify the correctness of rewrite rules
1619                        via sampling
1620
1621              sygusRewVerifyAbort
1622                        (bool, default = true)
1623                        abort when sygus-rr-verify finds an instance of
1624                        unsoundness
1625
1626              sygusSampleGrammar
1627                        (bool, default = true)
1628                        when applicable, use grammar for choosing sample
1629                        points
1630
1631              sygusSamples
1632                        (int, default = 1000)
1633                        number of points to consider when doing sygus rewriter
1634                        sample testing
1635
1636              sygusStream
1637                        (bool, default = false)
1638                        enumerate a stream of solutions instead of terminating
1639                        after the first one
1640
1641              sygusTemplEmbedGrammar
1642                        (bool, default = false)
1643                        embed sygus templates into grammars
1644
1645              sygusUnif (bool, default = false)
1646                        Unification-based function synthesis
1647
1648              termDbMode
1649                        (CVC4::theory::quantifiers::TermDbMode, default =
1650                        CVC4::theory::quantifiers::TERM_DB_ALL)
1651                        which ground terms to consider for instantiation
1652
1653              trackInstLemmas
1654                        (bool, default = false)
1655                        track instantiation lemmas (for proofs, unsat cores,
1656                        qe and synthesis minimization)
1657
1658              triggerActiveSelMode
1659                        (CVC4::theory::quantifiers::TriggerActiveSelMode,
1660                        default = CVC4::theory::quantifiers::TRIG‐
1661                        GER_ACTIVE_SEL_ALL)
1662                        selection mode to activate triggers
1663
1664              triggerSelMode
1665                        (CVC4::theory::quantifiers::TriggerSelMode, default =
1666                        CVC4::theory::quantifiers::TRIGGER_SEL_MIN)
1667                        selection mode for triggers
1668
1669              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
1675              varElimQuant
1676                        (bool, default = true)
1677                        enable simple variable elimination for quantified for‐
1678                        mulas
1679
1680              varIneqElimQuant
1681                        (bool, default = true)
1682                        enable variable elimination based on infinite projec‐
1683                        tion of unbound arithmetic variables
1684
1685              SEP OPTIONS
1686
1687              sepCheckNeg
1688                        (bool, default = true)
1689                        check negated spatial assertions
1690
1691              sepChildRefine
1692                        (bool, default = false)
1693                        child-specific refinements of negated star, positive
1694                        wand
1695
1696              sepDisequalC
1697                        (bool, default = true)
1698                        assume cardinality elements are distinct
1699
1700              sepExp    (bool, default = false)
1701                        experimental flag for sep
1702
1703              sepMinimalRefine
1704                        (bool, default = false)
1705                        only add refinement lemmas for minimal (innermost)
1706                        assertions
1707
1708              sepPreSkolemEmp
1709                        (bool, default = false)
1710                        eliminate emp constraint at preprocess time
1711
1712              SETS OPTIONS
1713
1714              setsExt   (bool, default = false)
1715                        enable extended symbols such as complement and uni‐
1716                        verse in theory of sets
1717
1718              setsInferAsLemmas
1719                        (bool, default = true)
1720                        send inferences as lemmas
1721
1722              setsProxyLemmas
1723                        (bool, default = false)
1724                        introduce proxy variables eagerly to shorten lemmas
1725
1726              setsRelEager
1727                        (bool, default = true)
1728                        standard effort checks for relations
1729
1730              SMT LAYER OPTIONS
1731
1732              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
1738              bitblastStep
1739                        (unsigned, default = 1)
1740                        amount of resources spent for each bitblast step
1741                        (EXPERTS only)
1742
1743              bvSatConflictStep
1744                        (unsigned, default = 1)
1745                        amount of resources spent for each sat conflict
1746                        (bitvectors) (EXPERTS only)
1747
1748              checkModels
1749                        (bool)
1750                        after SAT/INVALID/UNKNOWN, check that the generated
1751                        model satisfies user assertions
1752
1753              checkProofs
1754                        (bool)
1755                        after UNSAT/VALID, machine-check the generated proof
1756
1757              checkSynthSol
1758                        (bool, default = false)
1759                        checks whether produced solutions to functions-to-syn‐
1760                        thesize satisfy the conjecture
1761
1762              checkUnsatCores
1763                        (bool)
1764                        after UNSAT/VALID, produce and check an unsat core
1765                        (expensive)
1766
1767              cnfStep   (unsigned, default = 1)
1768                        amount of resources spent for each call to cnf conver‐
1769                        sion (EXPERTS only)
1770
1771              decisionStep
1772                        (unsigned, default = 1)
1773                        amount of getNext decision calls in the decision
1774                        engine (EXPERTS only)
1775
1776              diagnosticChannelName
1777                        (std::string)
1778                        set the diagnostic output channel of the solver
1779
1780              dumpInstantiations
1781                        (bool, default = false)
1782                        output instantiations of quantified formulas after
1783                        every UNSAT/VALID response
1784
1785              dumpModels
1786                        (bool, default = false)
1787                        output models after every SAT/INVALID/UNKNOWN response
1788
1789              dumpProofs
1790                        (bool, default = false)
1791                        output proofs after every UNSAT/VALID response
1792
1793              dumpSynth (bool, default = false)
1794                        output solution for synthesis conjectures after every
1795                        UNSAT/VALID response
1796
1797              dumpUnsatCores
1798                        (bool, default = false)
1799                        output unsat cores after every UNSAT/VALID response
1800
1801              dumpUnsatCoresFull
1802                        (bool, default = false)
1803                        dump the full unsat core, including unlabeled asser‐
1804                        tions
1805
1806              expandDefinitions
1807                        (bool, default = false)
1808                        always expand symbol definitions in output
1809
1810              extRewPrep
1811                        (bool, default = false)
1812                        use extended rewriter as a preprocessing pass
1813
1814              extRewPrepAgg
1815                        (bool, default = false)
1816                        use aggressive extended rewriter as a preprocessing
1817                        pass
1818
1819              forceLogicString
1820                        (std::string)
1821                        set the logic, and override all further user attempts
1822                        to change it (EXPERTS only)
1823
1824              forceNoLimitCpuWhileDump
1825                        (bool, default = false)
1826                        Force no CPU limit when dumping models and proofs
1827
1828              interactiveMode
1829                        (bool)
1830                        deprecated name for produce-assertions
1831
1832              doITESimp (bool)
1833                        turn on ite simplification (Kim (and Somenzi) et al.,
1834                        SAT 2009)
1835
1836              lemmaStep (unsigned, default = 1)
1837                        amount of resources spent when adding lemmas (EXPERTS
1838                        only)
1839
1840              modelUninterpDtEnum
1841                        (bool, default = false)
1842                        in models, output uninterpreted sorts as datatype enu‐
1843                        merations
1844
1845              omitDontCares
1846                        (bool, default = false)
1847                        When producing a model, omit variables whose value
1848                        does not matter
1849
1850              doITESimpOnRepeat
1851                        (bool, default = false)
1852                        do the ite simplification pass again if repeating sim‐
1853                        plification
1854
1855              parseStep (unsigned, default = 1)
1856                        amount of resources spent for each command/expression
1857                        parsing (EXPERTS only)
1858
1859              preprocessStep
1860                        (unsigned, default = 1)
1861                        amount of resources spent for each preprocessing step
1862                        in SmtEngine (EXPERTS only)
1863
1864              produceAssignments
1865                        (bool, default = false)
1866                        support the get-assignment command
1867
1868              unsatAssumptions
1869                        (bool, default = false)
1870                        turn on unsat assumptions generation
1871
1872              unsatCores
1873                        (bool)
1874                        turn on unsat core generation
1875
1876              proof     (bool, default = false)
1877                        turn on proof generation
1878
1879              quantifierStep
1880                        (unsigned, default = 1)
1881                        amount of resources spent for quantifier instantia‐
1882                        tions (EXPERTS only)
1883
1884              regularChannelName
1885                        (std::string)
1886                        set the regular output channel of the solver
1887
1888              repeatSimp
1889                        (bool)
1890                        make multiple passes with nonclausal simplifier
1891
1892              replayLogFilename
1893                        (std::string)
1894                        replay decisions from file
1895
1896              replayInputFilename
1897                        (std::string)
1898                        replay decisions from file
1899
1900              restartStep
1901                        (unsigned, default = 1)
1902                        amount of resources spent for each theory restart
1903                        (EXPERTS only)
1904
1905              rewriteApplyToConst
1906                        (bool, default = false)
1907                        eliminate function applications, rewriting e.g. f(5)
1908                        to a new symbol f_5 (EXPERTS only)
1909
1910              rewriteStep
1911                        (unsigned, default = 1)
1912                        amount of resources spent for each rewrite step
1913                        (EXPERTS only)
1914
1915              satConflictStep
1916                        (unsigned, default = 1)
1917                        amount of resources spent for each sat conflict (main
1918                        sat solver) (EXPERTS only)
1919
1920              compressItes
1921                        (bool, default = false)
1922                        enables compressing ites after ite simplification
1923
1924              zombieHuntThreshold
1925                        (uint32_t, default = 524288)
1926                        post ite compression enables zombie removal while the
1927                        number of nodes is above this threshold
1928
1929              simplifyWithCareEnabled
1930                        (bool, default = false)
1931                        enables simplifyWithCare in ite simplificiation
1932
1933              simplificationMode
1934                        (SimplificationMode, default = SIMPLIFICA‐
1935                        TION_MODE_BATCH)
1936                        choose simplification mode, see --simplification=help
1937
1938              solveIntAsBV
1939                        (uint32_t, default = 0)
1940                        attempt to solve a pure integer satisfiable problem by
1941                        bitblasting in sufficient bitwidth (experimental)
1942
1943              solveRealAsInt
1944                        (bool, default = false)
1945                        attempt to solve a pure real satisfiable problem as an
1946                        integer problem (for non-linear)
1947
1948              sortInference
1949                        (bool, default = false)
1950                        calculate sort inference of input problem, convert the
1951                        input based on monotonic sorts
1952
1953              doStaticLearning
1954                        (bool, default = true)
1955                        use static learning (on by default)
1956
1957              sygusOut  (SygusSolutionOutMode, default = SYGUS_SOL_OUT_STA‐
1958                        TUS_AND_DEF)
1959                        output mode for sygus
1960
1961              sygusPrintCallbacks
1962                        (bool, default = true)
1963                        use sygus print callbacks to print sygus terms in the
1964                        user-provided form (disable for debugging)
1965
1966              symmetryBreakerExp
1967                        (bool, default = false)
1968                        generate symmetry breaking constraints after symmetry
1969                        detection
1970
1971              theoryCheckStep
1972                        (unsigned, default = 1)
1973                        amount of resources spent for each theory check call
1974                        (EXPERTS only)
1975
1976              unconstrainedSimp
1977                        (bool, default = false)
1978                        turn on unconstrained simplification (see Brut‐
1979                        tomesso/Brummayer PhD thesis)
1980
1981              STRINGS THEORY OPTIONS
1982
1983              stringAbortLoop
1984                        (bool, default = false)
1985                        abort when a looping word equation is encountered
1986
1987              stringBinaryCsp
1988                        (bool, default = false)
1989                        use binary search when splitting strings
1990
1991              stringCheckEntailLen
1992                        (bool, default = true)
1993                        check entailment between length terms to reduce split‐
1994                        ting
1995
1996              stringEager
1997                        (bool, default = false)
1998                        strings eager check
1999
2000              stringEagerLen
2001                        (bool, default = true)
2002                        strings eager length lemmas
2003
2004              stringEIT (bool, default = false)
2005                        the eager intersection used by the theory of strings
2006
2007              stringExp (bool, default = false)
2008                        experimental features in the theory of strings
2009
2010              stringFMF (bool, default = false)
2011                        the finite model finding used by the theory of strings
2012
2013              stringGuessModel
2014                        (bool, default = false)
2015                        use model guessing to avoid string extended function
2016                        reductions
2017
2018              stringInferAsLemmas
2019                        (bool, default = false)
2020                        always send lemmas out instead of making internal
2021                        inferences
2022
2023              stringInferSym
2024                        (bool, default = true)
2025                        strings split on empty string
2026
2027              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
2033              stringLazyPreproc
2034                        (bool, default = true)
2035                        perform string preprocessing lazily
2036
2037              stringLB  (unsigned, default = 0)
2038                        the strategy of LB rule application: 0-lazy, 1-eager,
2039                        2-no
2040
2041              stringLenGeqZ
2042                        (bool, default = false)
2043                        strings length greater than zero lemmas
2044
2045              stringLenNorm
2046                        (bool, default = true)
2047                        strings length normalization lemma
2048
2049              stringLenPropCsp
2050                        (bool, default = false)
2051                        do length propagation based on constant splits
2052
2053              stringMinPrefixExplain
2054                        (bool, default = true)
2055                        minimize explanations for prefix of normal forms in
2056                        strings
2057
2058              stringOpt1
2059                        (bool, default = true)
2060                        internal option1 for strings: normal form
2061
2062              stringOpt2
2063                        (bool, default = false)
2064                        internal option2 for strings: constant regexp split‐
2065                        ting
2066
2067              stdPrintASCII
2068                        (bool, default = false)
2069                        the alphabet contains only printable characters from
2070                        the standard extended ASCII
2071
2072              stringProcessLoop
2073                        (bool, default = true)
2074                        reduce looping word equations to regular expressions
2075
2076              stringRExplainLemmas
2077                        (bool, default = true)
2078                        regression explanations for string lemmas
2079
2080              stringSplitEmp
2081                        (bool, default = true)
2082                        strings split on empty string
2083
2084              stringUfReduct
2085                        (bool, default = false)
2086                        use uninterpreted functions when applying extended
2087                        function reductions
2088
2089              THEORY LAYER OPTIONS
2090
2091              assignFunctionValues
2092                        (bool, default = true)
2093                        assign values for uninterpreted functions in models
2094
2095              condenseFunctionValues
2096                        (bool, default = true)
2097                        condense values for functions in models rather than
2098                        explicitly representing them
2099
2100              theoryOfMode
2101                        (CVC4::theory::TheoryOfMode, default = CVC4::the‐
2102                        ory::THEORY_OF_TYPE_BASED)
2103                        mode for Theory::theoryof() (EXPERTS only)
2104
2105              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
2111              UNINTERPRETED FUNCTIONS THEORY OPTIONS
2112
2113              ufSymmetryBreaker
2114                        (bool, default = true)
2115                        use UF symmetry breaker (Deharbe et al., CADE 2011)
2116
2117              ufHo      (bool, default = false)
2118                        enable support for higher-order reasoning
2119
2120              ufHoExt   (bool, default = true)
2121                        apply extensionality on function symbols
2122
2123              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
2129              ufssCliqueSplits
2130                        (bool, default = false)
2131                        use cliques instead of splitting on demand to shrink
2132                        model
2133
2134              ufssEagerSplits
2135                        (bool, default = false)
2136                        add splits eagerly for uf strong solver
2137
2138              ufssFairness
2139                        (bool, default = true)
2140                        use fair strategy for finite model finding multiple
2141                        sorts
2142
2143              ufssFairnessMonotone
2144                        (bool, default = false)
2145                        group monotone sorts when enforcing fairness for
2146                        finite model finding
2147
2148              ufssRegions
2149                        (bool, default = true)
2150                        disable region-based method for discovering cliques
2151                        and splits in uf strong solver
2152
2153              ufssTotality
2154                        (bool, default = false)
2155                        always use totality axioms for enforcing cardinality
2156                        constraints
2157
2158              ufssTotalityLimited
2159                        (int, default = -1)
2160                        apply totality axioms, but only up to cardinality N
2161                        (-1 == do not apply totality axioms, default)
2162
2163              ufssTotalitySymBreak
2164                        (bool, default = false)
2165                        apply symmetry breaking for totality axioms
2166
2167              ufssMode  (CVC4::theory::uf::UfssMode, default = CVC4::the‐
2168                        ory::uf::UF_SS_FULL)
2169                        mode of operation for uf strong solver.
2170
2171
2172

VERSION

2174       This manual page refers to CVC4 version 1.6.
2175

BUGS

2177       An   issue   tracker   for   the   CVC4   project   is   maintained  at
2178       https://github.com/CVC4/CVC4/issues.
2179

AUTHORS

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

SEE ALSO

2186       libcvc4(3), libcvc4parser(3), libcvc4compat(3)
2187
2188       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/.
2191
2192
2193
2194CVC4 release 1.6                 February 2019                   OPTIONS(3cvc)
Impressum