cvc4, pcvc4  an automated theorem prover
cvc4 [ options ] [ file ]
pcvc4 [ options ] [ file ]
cvc4 is an automated theorem prover for firstorder formulas with respect
to background theories of interest.
pcvc4 is CVC4's
"portfolio" variant, which is capable of running multiple CVC4
instances in parallel, configured differently.
With
file , commands are read from
file and executed. CVC4
supports the SMTLIB (versions 1.2 and 2.0) input format, as well as its own
native “presentation language” , which is similar in many
respects to CVC3's presentation language, but not identical.
If
file is unspecified, standard input is read (and the
CVC4
presentation language is assumed). If
file is unspecified and
CVC4 is connected to a terminal, interactive mode is assumed.
 Each option marked with [*] has a noOPTIONNAME variant,
which reverses the sense of the option.

 lang=LANG  L LANG
 force input language (default is "auto"; see
lang help)
 outputlang=LANG
 force output language (default is "auto"; see
outputlang help)
 verbose  v
 increase verbosity (may be repeated)
 quiet  q
 decrease verbosity (may be repeated)
 stats
 give statistics on exit [*]
 version  V
 identify this CVC4 binary
 help  h
 full command line reference
 showconfig
 show CVC4 static configuration
 strictparsing
 be less tolerant of nonconforming inputs [*]
 dump=MODE
 dump preprocessed assertions, etc., see dump=help
 dumpto=FILE
 all dumping goes to FILE (instead of stdout)
 producemodels  m
 support the getvalue and getmodel commands [*]
 produceassertions
 keep an assertions list (enables getassertions command)
[*]
 incremental  i
 enable incremental solving [*]
 tlimit=MS
 enable time limiting (give milliseconds)
 tlimitper=MS
 enable time limiting per query (give milliseconds)
 rlimit=N
 enable resource limiting (currently, roughly the number of
SAT conflicts)
 rlimitper=N
 enable resource limiting per query
 hardlimit
 the resource limit is hard potentially leaving the
smtEngine in an unsafe state (should be destroyed and rebuild after
resourcing out) [*]
 cputime
 measures CPU time if set to true and wall time if false
(default false) [*]
 unatelemmas=MODE
 determines which lemmas to add before solving (default is
'all', see unatelemmas=help)
 arithprop=MODE
 turns on arithmetic propagation (default is 'old', see
arithprop=help)
 heuristicpivots=N
 the number of times to apply the heuristic pivot rule; if N
< 0, this defaults to the number of variables; if this is unset, this
is tuned by the logic selection
 standardeffortvariableorderpivots=N
 limits the number of pivots in a single invocation of
check() at a nonfull effort level using Bland's pivot rule (EXPERTS
only)
 errorselectionrule=RULE
 change the pivot rule for the basic variable (default is
'min', see pivotrule help)
 simplexcheckperiod=N
 the number of pivots to do in simplex before rechecking for
a conflict on all variables
 pivotthreshold=N
 sets the number of pivots using pivotrule per basic
variable per simplex instance before using variable order
 proprowlength=N
 sets the maximum row length to be used in propagation
 enablediosolver
 turns on Linear Diophantine Equation solver (Griggio, JSAT
2012)
 disablediosolver
 turns off Linear Diophantine Equation solver (Griggio, JSAT
2012)
 enablearithrewriteequalities
 turns on the preprocessing rewrite turning equalities into
a conjunction of inequalities
 disablearithrewriteequalities
 turns off the preprocessing rewrite turning equalities into
a conjunction of inequalities
 enablemiplibtrick
 turns on the preprocessing step of attempting to infer
bounds on miplib problems
 disablemiplibtrick
 turns off the preprocessing step of attempting to infer
bounds on miplib problems
 miplibtricksubs=N
 do substitution for miplib 'tmp' vars if defined in <= N
eliminated vars
 cutallbounded
 turns on the integer solving step of periodically cutting
all integer variables that have both upper and lower bounds [*]
 nocutallbounded
 turns off the integer solving step of periodically cutting
all integer variables that have both upper and lower bounds
 maxCutsInContext
 maximum cuts in a given context before signalling a
restart
 revertarithmodelsonunsat
 revert the arithmetic model to a known safe model on unsat
if one is cached [*]
 fcpenalties
 turns on degenerate pivot penalties [*]
 nofcpenalties
 turns off degenerate pivot penalties
 usefcsimplex
 use focusing and converging simplex (FMCAD 2013 submission)
[*]
 usesoi
 use sum of infeasibility simplex (FMCAD 2013 submission)
[*]
 restrictpivots
 have a pivot cap for simplex at effort levels below
fullEffort [*]
 collectpivotstats
 collect the pivot history [*]
 useapprox
 attempt to use an approximate solver [*]
 approxbranchdepth
 maximum branch depth the approximate solver is allowed to
take
 diodecomps
 let skolem variables for integer divisibility constraints
leak from the dio solver [*]
 newprop
 use the new row propagation system [*]
 arithpropclauses
 rows shorter than this are propagated as clauses
 soiqe
 use quick explain to minimize the sum of infeasibility
conflicts [*]
 rewritedivk
 rewrite division and mod when by a constant into linear
terms [*]
 sesolveint
 attempt to use the approximate solve integer method on
standard effort [*]
 lemmasonreplayfailure
 attempt to use external lemmas if approximate solve integer
failed [*]
 dioturns
 turns in a row dio solver cutting gets
 rrturns
 round robin turn
 diorepeat
 handle dio solver constraints in mass or one at a time
[*]
 replayearlyclosedepth
 multiples of the depths to try to close the approx log
eagerly
 replayfailurepenalty
 number of solve integer attempts to skips after a numeric
failure
 replaynumerrpenalty
 number of solve integer attempts to skips after a numeric
failure
 replayrejectcut
 maximum complexity of any coefficient while replaying
cuts
 replaylemmarejectcut
 maximum complexity of any coefficient while outputting
replaying cut lemmas
 replaysoimajorthreshold
 threshold for a major tolerance failure by the approximate
solver
 replaysoimajorthresholdpen
 threshold for a major tolerance failure by the approximate
solver
 replaysoiminorthreshold
 threshold for a minor tolerance failure by the approximate
solver
 replaysoiminorthresholdpen
 threshold for a minor tolerance failure by the approximate
solver
 ppassertmaxsubsize
 threshold for substituting an equality in ppAssert
 maxreplaytree
 threshold for attempting to replay a tree
 pbrewrites
 apply pseudo boolean rewrites [*]
 pbrewritethreshold
 threshold of number of pseudoboolean variables to have
before doing rewrites
 snorminfereq
 infer equalities based on Shostak normalization [*]
 nlext
 extended approach to nonlinear [*]
 nlextrbound
 use resolutionstyle inference for inferring new bounds
[*]
 nlexttplanes
 use nonterminating tangent plane strategy for nonlinear
[*]
 nlextentconf
 check for entailed conflicts in nonlinear solver [*]
 nlextrewrite
 do rewrites in nonlinear solver [*]
 nlextsolvesubs
 do solving for determining constant substitutions [*]
 nlextpurify
 purify nonlinear terms at preprocess [*]
 nlextsplitzero
 intial splits on zero for all variables [*]
 arraysoptimizelinear
 turn on optimization for linear array terms (see de Moura
FMCAD 09 arrays paper) [*]
 arrayslazyrintro1
 turn on optimization to only perform RIntro1 rule lazily
(see Jovanovic/Barrett 2012: Being Careful with Theory Combination)
[*]
 arraysweakequiv
 use algorithm from Christ/Hoenicke (SMT 2014) [*]
 arraysmodelbased
 turn on modelbased array solver [*]
 arrayseagerindex
 turn on eager index splitting for generated array lemmas
[*]
 arrayseagerlemmas
 turn on eager lemma generation for arrays [*]
 arraysconfig
 set different array option configurations  for developers
only
 arraysreducesharing
 use model information to reduce size of care graph for
arrays [*]
 arraysprop
 propagation effort for arrays: 0 is none, 1 is some, 2 is
full
 statseveryquery
 in incremental mode, print stats after every satisfiability
or validity query [*]
 statshidezeros
 hide statistics which are zero
 statsshowzeros
 show statistics even when they are zero (default)
 parseonly
 exit after parsing input [*]
 preprocessonly
 exit after preprocessing input [*]
 trace=TAG  t TAG
 trace something (e.g. t pushpop), can repeat
 debug=TAG  d TAG
 debug something (e.g. d arith), can repeat
 printsuccess
 print the "success" output required of SMTLIBv2
[*]
 smtlibstrict
 SMTLIBv2 compliance mode (implies other options)
 bvsatsolver=MODE
 choose which sat solver to use, see bvsatsolver=help
(EXPERTS only)
 bitblast=MODE
 choose bitblasting mode, see bitblast=help
 bitblastaig
 bitblast by first converting to AIG (implies
bitblast=eager) [*]
 bvaigsimp=COMMAND
 abc command to run AIG simplifications (implies
bitblastaig, default is "balance;drw") (EXPERTS only)
 bvpropagate
 use bitvector propagation in the bitblaster [*]
 bveqsolver
 use the equality engine for the bitvector theory (only if
bitblast=lazy) [*]
 bveqslicer=MODE
 turn on the slicing equality solver for the bitvector
theory (only if bitblast=lazy)
 bvinequalitysolver
 turn on the inequality solver for the bitvector theory
(only if bitblast=lazy) [*]
 bvalgebraicsolver
 turn on the algebraic solver for the bitvector theory
(only if bitblast=lazy) [*]
 bvalgebraicbudget
 the budget allowed for the algebraic solver in number of
SAT conflicts (EXPERTS only)
 bvtobool
 lift bitvectors of size 1 to booleans when possible
[*]
 booltobv
 convert booleans to bitvectors of size 1 when possible
[*]
 bvdivzeroconst
 always return 1 on division by zero [*]
 bvextractarith
 enable rewrite pushing extract [i:0] over arithmetic
operations (can blow up) (EXPERTS only) [*]
 bvabstraction
 mcm benchmark abstraction (EXPERTS only) [*]
 bvskolemize
 skolemize arguments for bv abstraction (only does something
if bvabstraction is on) (EXPERTS only) [*]
 bvnumfunc=NUM
 number of function symbols in conflicts that are
generalized (EXPERTS only)
 bveagerexplanations
 compute bitblasting propagation explanations eagerly
(EXPERTS only) [*]
 bvquickxplain
 minimize bv conflicts using the QuickXplain algorithm
(EXPERTS only) [*]
 bvintropow2
 introduce bitvector powers of two as a preprocessing pass
(EXPERTS only) [*]
 bvlazyrewriteextf
 lazily rewrite extended functions like bv2nat and int2bv
[*]
 bvlazyreduceextf
 reduce extended functions like bv2nat and int2bv at last
call instead of full effort [*]
 bvalgextf
 algebraic inferences for extended functions [*]
 dtrewriteerrorsel
 rewrite incorrectly applied selectors to arbitrary ground
term (EXPERTS only) [*]
 dtforceassignment
 force the datatypes solver to give specific values to all
datatypes terms before answering sat [*]
 dtbinarysplit
 do binary splits for datatype constructor types [*]
 dtrefskintro
 introduce reference skolems for shorter explanations
[*]
 dtusetesters
 do not preprocess away tester predicates [*]
 cdtbisimilar
 do bisimilarity check for codatatypes [*]
 dtcyclic
 do cyclicity check for datatypes [*]
 dtinferaslemmas
 always send lemmas out instead of making internal
inferences [*]
 dtblastsplits
 when applicable, blast splitting lemmas for all variables
at once [*]
 decision=MODE
 choose decision mode, see decision=help
 decisionthreshold=N
 ignore all nodes greater than threshold in first attempt to
pick decision (EXPERTS only)
 decisionuseweight
 use the weight nodes (locally, by looking at children) to
direct recursive search (EXPERTS only) [*]
 decisionrandomweight=N
 assign random weights to nodes between 0 and N1 (0:
disable) (EXPERTS only)
 decisionweightinternal=HOW
 computer weights of internal nodes using children: off,
max, sum, usr1 (meaning evolving) (EXPERTS only)
 defaultexprdepth=N
 print exprs to depth N (0 == default, 1 == no limit)
 defaultdagthresh=N
 dagify common subexprs appearing > N times (1 ==
default, 0 == don't dagify)
 printexprtypes
 print types with variables when printing exprs [*]
 eagertypechecking
 type check expressions immediately on creation (debug
builds only)
 lazytypechecking
 type check expressions only when necessary (default)
 enableidlrewriteequalities
 enable rewriting equalities into two inequalities in IDL
solver (default is disabled)
 disableidlrewriteequalities
 disable rewriting equalities into two inequalities in IDL
solver (default is disabled)
 showdebugtags
 show all available tags for debugging
 showtracetags
 show all available tags for tracing
 earlyexit
 do not run destructors at exit; default on except in debug
builds (EXPERTS only) [*]
 threads=N
 Total number of threads for portfolio
 threadN=string
 configures portfolio thread N (0..#threads1)
 threadstack=N
 stack size for worker threads in MB (0 means use
Boost/thread lib default)
 filterlemmalength=N
 don't share (among portfolio threads) lemmas strictly
longer than N
 fallbacksequential
 Switch to sequential mode (instead of printing an error) if
it can't be solved in portfolio mode [*]
 incrementalparallel
 Use parallel solver even in incremental mode (may print
'unknown's at times) [*]
 interactive
 force interactive/noninteractive mode [*]
 continuedexecution
 continue executing commands, even on error
 segvspin
 spin on segfault/other crash waiting for gdb [*]
 teardownincremental=N
 implement PUSH/POP/multiquery by destroying and recreating
SmtEngine every N queries (EXPERTS only)
 waittojoin
 wait for other threads to join before quitting (EXPERTS
only) [*]
 mmap
 memory map file input [*]
 modelformat=MODE
 print format mode for models, see modelformat=help
 instformat=MODE
 print format mode for instantiations, see
instformat=help
 lfscletification
 turns on global letification in LFSC proofs [*]
 aggressivecoremin
 turns on aggressive unsat core minimization (experimental)
[*]
 fewerpreprocessingholes
 try to eliminate preprocessing holes in proofs [*]
 allowemptydependencies
 if unable to track the dependencies of a
rewritten/preprocessed assertion, fail silently [*]
 randomfreq=P
 sets the frequency of random decisions in the sat solver
(P=0.0 by default)
 randomseed=S
 sets the random seed for the sat solver
 restartintbase=N
 sets the base restart interval for the sat solver (N=25 by
default)
 restartintinc=F
 sets the restart interval increase factor for the sat
solver (F=3.0 by default)
 refineconflicts
 refine theory conflict clauses (default false) [*]
 minisatelimination
 use Minisat elimination [*]
 minisatdumpdimacs
 instead of solving minisat dumps the asserted clauses in
Dimacs format [*]
 miniscopequant
 miniscope quantifiers [*]
 miniscopequantfv
 miniscope quantifiers for ground subformulas [*]
 quantsplit
 apply splitting to quantified formulas based on variable
disjoint disjuncts [*]
 prenexquant=MODE
 prenex mode for quantified formulas
 prenexquantuser
 prenex quantified formulas with user patterns [*]
 varelimquant
 enable simple variable elimination for quantified formulas
[*]
 varineqelimquant
 enable variable elimination based on infinite projection of
unbound arithmetic variables [*]
 dtvarexpquant
 expand datatype variables bound to one constructor in
quantifiers [*]
 iteliftquant=MODE
 ite lifting mode for quantified formulas
 condvarsplitquant
 split quantified formulas that lead to variable
eliminations [*]
 condvarsplitaggquant
 aggressive split quantified formulas that lead to variable
eliminations [*]
 itedttsplitquant
 split ites with dt testers as conditions [*]
 preskolemquant
 apply skolemization eagerly to bodies of quantified
formulas [*]
 preskolemquantnested
 apply skolemization to nested quantified formulas [*]
 preskolemquantagg
 apply skolemization to quantified formulas aggressively
[*]
 agminiscopequant
 perform aggressive miniscoping for quantifiers [*]
 elimtautquant
 eliminate tautological disjuncts of quantified formulas
[*]
 elimextarithquant
 eliminate extended arithmetic symbols in quantified
formulas [*]
 condrewritequant
 conditional rewriting of quantified formulas [*]
 ematching
 whether to do heuristic Ematching [*]
 termdbmode
 which ground terms to consider for instantiation
 registerquantbodyterms
 consider ground terms within bodies of quantified formulas
for matching [*]
 inferarithtriggereq
 infer equalities for trigger terms based on solving
arithmetic equalities [*]
 inferarithtriggereqexp
 record explanations for inferArithTriggerEq [*]
 stricttriggers
 only instantiate quantifiers with user patterns based on
triggers [*]
 relevanttriggers
 prefer triggers that are more relevant based on SInE style
analysis [*]
 relationaltriggers
 choose relational triggers such as x = f(y), x >= f(y)
[*]
 purifytriggers
 purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y1
[*]
 purifydttriggers
 purify dt triggers, match all constructors of correct form
instead of selectors [*]
 purethtriggers
 use pure theory terms as single triggers [*]
 partialtriggers
 use triggers that do not contain all free variables
[*]
 multitriggerwhensingle
 select multi triggers when single triggers exist [*]
 multitriggerpriority
 only try multi triggers if single triggers give no
instantiations [*]
 multitriggercache
 caching version of multi triggers [*]
 multitriggerlinear
 implementation of multi triggers where maximum number of
instantiations is linear wrt number of ground terms [*]
 triggersel
 selection mode for triggers
 triggeractivesel
 selection mode to activate triggers
 userpat=MODE
 policy for handling userprovided patterns for quantifier
instantiation
 incrementtriggers
 generate additional triggers as needed during search [*]
 instwhen=MODE
 when to apply instantiation
 instwhenstrictinterleave
 ensure theory combination and standard quantifier effort
strategies take turns [*]
 instwhenphase=N
 instantiation rounds quantifiers takes (>=1) before
allowing theory combination to happen
 instwhentcfirst
 allow theory combination to happen once initially, before
quantifier strategies are run [*]
 quantmodelee
 use equality engine of model for last call effort [*]
 instmaxlevel=N
 maximum inst level of terms used to instantiate quantified
formulas with (1 == no limit, default)
 instlevelinputonly
 only input terms are assigned instantiation level zero
[*]
 quantrepmode=MODE
 selection mode for representatives in quantifiers
engine
 instrlvcond
 add relevancy conditions for instantiations [*]
 fullsaturatequant
 when all other quantifier instantiation strategies fail,
instantiate with ground terms from relevant domain, then arbitrary ground
terms before answering unknown [*]
 fullsaturatequantrd
 whether to use relevant domain first for full saturation
instantiation strategy [*]
 fsinst
 interleave full saturate instantiation with other
techniques [*]
 literalmatching=MODE
 choose literal matching mode
 finitemodelfind
 use finite model finding heuristic for quantifier
instantiation [*]
 quantfunwd
 assume that function defined by quantifiers are well
defined [*]
 fmffun
 find models for recursively defined functions, assumes
functions are admissible [*]
 fmffunrlv
 find models for recursively defined functions, assumes
functions are admissible, allows empty type when function is irrelevant
[*]
 fmfemptysorts
 allow finite model finding to assume sorts that do not
occur in ground assertions are empty [*]
 mbqi=MODE
 choose mode for modelbased quantifier instantiation
 mbqioneinstperround
 only add one instantiation per quantifier per round for
mbqi [*]
 mbqionequantperround
 only add instantiations for one quantifier per round for
mbqi [*]
 fmfinstengine
 use instantiation engine in conjunction with finite model
finding [*]
 fmfinstgen
 enable InstGen instantiation techniques for finite model
finding [*]
 fmfinstgenonequantperround
 only perform InstGen instantiation techniques on one
quantifier per round [*]
 fmffreshdc
 use fresh distinguished representative when applying
InstGen techniques [*]
 fmffmcsimple
 simple models in full model check for finite model finding
[*]
 fmfboundint
 finite model finding on bounded integer quantification
[*]
 fmfbound
 finite model finding on bounded quantification [*]
 fmfboundlazy
 enforce bounds for bounded quantification lazily via use of
proxy variables [*]
 fmfboundminmode=MODE
 mode for which types of bounds to minimize via first
decision heuristics
 quantcf
 enable conflict find mechanism for quantifiers [*]
 quantcfmode=MODE
 what effort to apply conflict find mechanism
 quantcfwhen=MODE
 when to invoke conflict find mechanism for quantifiers
 qcftconstraint
 enable entailment checks for tconstraints in qcf algorithm
[*]
 qcfallconflict
 add all available conflicting instances during
conflictbased instantiation [*]
 qcfnestedconflict
 consider conflicts for nested quantifiers [*]
 qcfvoexp
 qcf experimental variable ordering [*]
 instnoentail
 do not consider instances of quantified formulas that are
currently entailed [*]
 instnomodeltrue
 do not consider instances of quantified formulas that are
currently true in model, if it is available [*]
 instprop
 internal propagation for instantiations for selecting
relevant instances [*]
 qcfeagertest
 optimization, test qcf instances eagerly [*]
 qcfeagercheckrd
 optimization, eagerly check relevant domain of matched
position [*]
 qcfskiprd
 optimization, skip instances based on possibly irrelevant
portions of quantified formulas [*]
 rewriterules
 use rewrite rules module [*]
 rroneinstperround
 add one instance of rewrite rule per round [*]
 quantind
 use all available techniques for inductive reasoning
[*]
 dtstcind
 apply strengthening for existential quantification over
datatypes based on structural induction [*]
 intwfind
 apply strengthening for integers based on wellfounded
induction [*]
 conjecturegen
 generate candidate conjectures for inductive proofs [*]
 conjecturegenperround=N
 number of conjectures to generate per instantiation
round
 conjecturenofilter
 do not filter conjectures [*]
 conjecturefilteractiveterms
 filter based on active terms [*]
 conjecturefiltercanonical
 filter based on canonicity [*]
 conjecturefiltermodel
 filter based on model [*]
 conjecturegengtenum=N
 number of ground terms to generate for model filtering
 conjecturegenueeintro
 more aggressive merging for universal equality engine,
introduces terms [*]
 conjecturegenmaxdepth=N
 maximum depth of terms to consider for conjectures
 cegqi

counterexampleguided quantifier instantiation [*]
 cegqifair=MODE

if and how to apply fairness for cegqi
 cegqisi=MODE

mode for processing single invocation synthesis conjectures
 cegqisipartial

combined techniques for synthesis conjectures that are partially single
invocation [*]
 cegqisireconstruct

reconstruct solutions for single invocation conjectures in original grammar
[*]
 cegqisisolmincore

minimize solutions for single invocation conjectures based on unsat core
[*]
 cegqisisolmininst

minimize individual instantiations for single invocation conjectures based
on unsat core [*]
 cegqisireconstructconst

include constants when reconstruct solutions for single invocation
conjectures in original grammar [*]
 cegqisiabort

abort if synthesis conjecture is not single invocation [*]
 sygusnf

only search for sygus builtin terms that are in normal form [*]
 sygusnfarg

account for relationship between arguments of operations in sygus normal
form [*]
 sygusnfsym

narrow sygus search space based on global state of current candidate
program [*]
 sygusnfsymgen

generalize lemmas for global search space narrowing [*]
 sygusnfsymarg

generalize based on arguments in global search space narrowing [*]
 sygusnfsymcontent

generalize based on content in global search space narrowing [*]
 sygusinvtempl=MODE

template mode for sygus invariant synthesis
 sygusunifcsol

enable approach which unifies conditional solutions [*]
 sygusdirecteval

direct unfolding of evaluation functions [*]
 syguscrefeval

direct evaluation of refinement lemmas for conflict analysis [*]
 cbqi
 turns on counterexamplebased quantifier instantiation
[*]
 cbqirecurse
 turns on recursive counterexamplebased quantifier
instantiation [*]
 cbqisat
 answer sat when quantifiers are asserted with
counterexamplebased quantifier instantiation [*]
 cbqimodel
 guide instantiations by model values for
counterexamplebased quantifier instantiation [*]
 cbqiall
 apply counterexamplebased instantiation to all quantified
formulas [*]
 cbqiuseinfint
 use integer infinity for vts in counterexamplebased
quantifier instantiation [*]
 cbqiuseinfreal
 use real infinity for vts in counterexamplebased
quantifier instantiation [*]
 cbqiprereginst

preregister ground instantiations in counterexamplebased quantifier
instantiation [*]
 cbqiminbounds

use minimally constrained lower/upper bound for counterexamplebased
quantifier instantiation [*]
 cbqirounduplia

round up integer lower bounds in substitutions for counterexamplebased
quantifier instantiation [*]
 cbqimidpoint

choose substitutions based on midpoints of lower and upper bounds for
counterexamplebased quantifier instantiation [*]
 cbqinopt

nonoptimal bounds for counterexamplebased quantifier instantiation
[*]
 cbqilitdep

dependency lemmas for quantifier alternation in counterexamplebased
quantifier instantiation [*]
 cbqiinnermost
 only process innermost quantified formulas in
counterexamplebased quantifier instantiation [*]
 cbqinestedqe
 process nested quantified formulas with quantifier
elimination in counterexamplebased quantifier instantiation [*]
 quantepr
 infer whether in effectively propositional fragment, use
for cbqi [*]
 quanteprmatch
 use matching heuristics for EPR instantiation [*]
 localtext

do instantiation based on local theory extensions [*]
 ltepartialinst

partially instantiate local theory quantifiers [*]
 lterestrictinstclosure

treat arguments of inst closure as restricted terms for instantiation [*]
 quantalphaequiv

infer alpha equivalence between quantified formulas [*]
 macrosquant
 perform quantifiers macro expansion [*]
 macrosquantmode=MODE
 mode for quantifiers macro expansion
 quantdsplitmode=MODE
 mode for dynamic quantifiers splitting
 quantantiskolem
 perform antiskolemization for quantified formulas [*]
 quantee

maintain congrunce closure over universal equalities [*]
 trackinstlemmas

track instantiation lemmas (for proofs, unsat cores, qe and synthesis
minimization) [*]
 sepcheckneg
 check negated spatial assertions [*]
 sepexp
 experimental flag for sep [*]
 sepminrefine
 only add refinement lemmas for minimal (innermost)
assertions [*]
 sepdeqc
 assume cardinality elements are distinct [*]
 seppreskolememp
 eliminate emp constraint at preprocess time [*]
 sepchildrefine
 childspecific refinements of negated star, positive wand
[*]
 setsproxylemmas
 introduce proxy variables eagerly to shorten lemmas
[*]
 setsinferaslemmas
 send inferences as lemmas [*]
 setsreleager
 standard effort checks for relations [*]
 setsext
 enable extended symbols such as complement and universe in
theory of sets [*]
 forcelogic=LOGIC
 set the logic, and override all further user attempts to
change it (EXPERTS only)
 simplification=MODE
 choose simplification mode, see simplification=help
 nosimplification
 turn off all simplification (same as
simplification=none)
 staticlearning
 use static learning (on by default) [*]
 checkmodels
 after SAT/INVALID/UNKNOWN, check that the generated model
satisfies user assertions [*]
 dumpmodels
 output models after every SAT/INVALID/UNKNOWN response
[*]
 omitdontcares
 When producing a model, omit variables whose value does not
matter [*]
 proof
 turn on proof generation [*]
 checkproofs
 after UNSAT/VALID, machinecheck the generated proof
[*]
 dumpproofs
 output proofs after every UNSAT/VALID response [*]
 dumpinstantiations
 output instantiations of quantified formulas after every
UNSAT/VALID response [*]
 dumpsynth
 output solution for synthesis conjectures after every
UNSAT/VALID response [*]
 produceunsatcores
 turn on unsat core generation [*]
 checkunsatcores
 after UNSAT/VALID, produce and check an unsat core
(expensive) [*]
 dumpunsatcores
 output unsat cores after every UNSAT/VALID response
[*]
 dumpunsatcoresfull
 dump the full unsat core, including unlabeled assertions
[*]
 produceassignments
 support the getassignment command [*]
 itesimp
 turn on ite simplification (Kim (and Somenzi) et al., SAT
2009) [*]
 onrepeatitesimp
 do the ite simplification pass again if repeating
simplification [*]
 simpwithcare
 enables simplifyWithCare in ite simplificiation [*]
 simpitecompress
 enables compressing ites after ite simplification [*]
 unconstrainedsimp
 turn on unconstrained simplification (see
Bruttomesso/Brummayer PhD thesis) [*]
 repeatsimp
 make multiple passes with nonclausal simplifier [*]
 simpitehuntzombies
 post ite compression enables zombie removal while the
number of nodes is above this threshold
 sortinference
 calculate sort inference of input problem, convert the
input based on monotonic sorts [*]
 abstractvalues
 in models, output arrays (and in future, maybe others)
using abstract values, as required by the SMTLIB standard [*]
 modeludtenum
 in models, output uninterpreted sorts as datatype
enumerations [*]
 rewritestep
 amount of resources spent for each rewrite step (EXPERTS
only)
 theorycheckstep
 amount of resources spent for each theory check call
(EXPERTS only)
 decisionstep
 amount of getNext decision calls in the decision engine
(EXPERTS only)
 bitblaststep
 amount of resources spent for each bitblast step (EXPERTS
only)
 parsestep
 amount of resources spent for each command/expression
parsing (EXPERTS only)
 lemmastep
 amount of resources spent when adding lemmas (EXPERTS
only)
 restartstep
 amount of resources spent for each theory restart (EXPERTS
only)
 cnfstep
 amount of resources spent for each call to cnf conversion
(EXPERTS only)
 preprocessstep
 amount of resources spent for each preprocessing step in
SmtEngine (EXPERTS only)
 quantifierstep
 amount of resources spent for quantifier instantiations
(EXPERTS only)
 satconflictstep
 amount of resources spent for each sat conflict (main sat
solver) (EXPERTS only)
 bvsatconflictstep
 amount of resources spent for each sat conflict
(bitvectors) (EXPERTS only)
 rewriteapplytoconst
 eliminate function applications, rewriting e.g. f(5) to a
new symbol f_5 (EXPERTS only) [*]
 forcenolimitcpuwhiledump
 Force no CPU limit when dumping models and proofs [*]
 stringsexp
 experimental features in the theory of strings [*]
 stringslb=N
 the strategy of LB rule application: 0lazy, 1eager,
2no
 stringsstdascii
 the alphabet contains only characters from the standard
ASCII or the extended one [*]
 stringsfmf
 the finite model finding used by the theory of strings [*]
 stringseager
 strings eager check [*]
 stringseit
 the eager intersection used by the theory of strings
[*]
 stringsopt1
 internal option1 for strings: normal form [*]
 stringsopt2
 internal option2 for strings: constant regexp splitting
[*]
 stringsinm
 internal for strings: ignore negative membership
constraints (fragment checking is needed, left to users for now) [*]
 stringslazypp
 perform string preprocessing lazily [*]
 stringslengeqz
 strings length greater than zero lemmas [*]
 stringslennorm
 strings length normalization lemma [*]
 stringsspemp
 strings split on empty string [*]
 stringsinfersym
 strings split on empty string [*]
 stringseagerlen
 strings eager length lemmas [*]
 stringscheckentaillen
 check entailment between length terms to reduce splitting
[*]
 stringsprocessloop
 reduce looping word equations to regular expressions
[*]
 stringsabortloop
 abort when a looping word equation is encountered [*]
 stringsinferaslemmas
 always send lemmas out instead of making internal
inferences [*]
 stringsrexplainlemmas
 regression explanations for string lemmas [*]
 stringsminprefixexplain
 minimize explanations for prefix of normal forms in strings
[*]
 stringsguessmodel
 use model guessing to avoid string extended function
reductions [*]
 stringsufreduct
 use uninterpreted functions when applying extended function
reductions [*]
 stringsbinarycsp
 use binary search when splitting strings [*]
 stringslpropcsp
 do length propagation based on constant splits [*]
 theoryofmode=MODE
 mode for Theory::theoryof() (EXPERTS only)
 usetheory=NAME
 use alternate theory implementation NAME (usetheory=help
for a list). This option may be repeated or a comma separated list.
 symmetrybreaker
 use UF symmetry breaker (Deharbe et al., CADE 2011)
[*]
 condensefunctionvalues
 condense models for functions rather than explicitly
representing them [*]
 ufssregions
 disable regionbased method for discovering cliques and
splits in uf strong solver [*]
 ufsseagersplit
 add splits eagerly for uf strong solver [*]
 ufsstotality
 always use totality axioms for enforcing cardinality
constraints [*]
 ufsstotalitylimited=N
 apply totality axioms, but only up to cardinality N (1 ==
do not apply totality axioms, default)
 ufsstotalitysymbreak
 apply symmetry breaking for totality axioms [*]
 ufssabortcard=N
 tells the uf strong solver a cardinality to abort at (1 ==
no limit, default)
 ufssexplainedcliques
 use explained clique lemmas for uf strong solver [*]
 ufsssimplecliques
 always use simple clique lemmas for uf strong solver
[*]
 ufssdeqprop
 eagerly propagate disequalities for uf strong solver
[*]
 ufss=MODE
 mode of operation for uf strong solver.
 ufsscliquesplits
 use cliques instead of splitting on demand to shrink model
[*]
 ufsssymbreak
 finite model finding symmetry breaking techniques [*]
 ufssfair
 use fair strategy for finite model finding multiple sorts
[*]
 ufssfairmonotone
 group monotone sorts when enforcing fairness for finite
model finding [*]
 Each option marked with [*] has a noOPTIONNAME variant,
which reverses the sense of the option.

CVC4 reports all syntactic and semantic errors on standard error.
The
CVC4 effort is the culmination of fifteen years of theorem proving
research, starting with the
Stanford Validity Checker (SVC) in 1996.
SVC's successor, the
Cooperating Validity Checker (CVC), had a more
optimized internal design, produced proofs, used the
Chaff SAT solver,
and featured a number of usability enhancements. Its name comes from the
cooperative nature of decision procedures in NelsonOppen theory combination,
which share amongst each other equalities between shared terms.
CVC Lite, first made available in 2003, was a rewrite of CVC that attempted to
make CVC more flexible (hence the “lite”) while extending the
feature set: CVCLite supported quantifiers where its predecessors did not.
CVC3 was a major overhaul of portions of CVC Lite: it added better decision
procedure implementations, added support for using MiniSat in the core, and
had generally better performance.
CVC4 is the new version, the fifth generation of this validity checker line that
is now celebrating fifteen years of heritage. It represents a complete
reevaluation of the core architecture to be both performant and to serve as a
cuttingedge research vehicle for the next several years. Rather than taking
CVC3 and redesigning problem parts, we've taken a cleanroom approach,
starting from scratch. Before using any designs from CVC3, we have thoroughly
scrutinized, vetted, and updated them. Many parts of CVC4 bear only a
superficial resemblance, if any, to their correspondent in CVC3.
However, CVC4 is fundamentally similar to CVC3 and many other modern SMT
solvers: it is a DPLL(
T ) solver, with a SAT solver at its core and a
delegation path to different decision procedure implementations, each in
charge of solving formulas in some background theory.
The reevaluation and groundup rewrite was necessitated, we felt, by the
performance characteristics of CVC3. CVC3 has many useful features, but some
core aspects of the design led to high memory use, and the use of heavyweight
computation (where more nimble engineering approaches could suffice) makes
CVC3 a much slower prover than other tools. As these designs are central to
CVC3, a new version was preferable to a selective reengineering, which would
have ballooned in short order.
This manual page refers to
CVC4 version 1.5.
A Bugzilla for the CVC4 project is maintained at
http://cvc4.cs.nyu.edu/bugzilla3/.
CVC4 is developed by a team of researchers at New York University and the
University of Iowa. See the AUTHORS file in the distribution for a full list
of contributors.
The CVC4 wiki contains useful information about the design and internals of
CVC4. It is maintained at
http://cvc4.cs.nyu.edu/wiki/.