Provided by: cvc4_1.5-1_amd64 
NAME
cvc4, pcvc4 - an automated theorem prover
SYNOPSIS
cvc4 [ options ] [ file ]
pcvc4 [ options ] [ file ]
DESCRIPTION
cvc4 is an automated theorem prover for first-order 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 SMT-LIB (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.
COMMON OPTIONS
Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the
option.
--lang=LANG | -L LANG
force input language (default is "auto"; see --lang help)
--output-lang=LANG
force output language (default is "auto"; see --output-lang 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
--show-config
show CVC4 static configuration
--strict-parsing
be less tolerant of non-conforming inputs [*]
--dump=MODE
dump preprocessed assertions, etc., see --dump=help
--dump-to=FILE
all dumping goes to FILE (instead of stdout)
--produce-models | -m
support the get-value and get-model commands [*]
--produce-assertions
keep an assertions list (enables get-assertions command) [*]
--incremental | -i
enable incremental solving [*]
--tlimit=MS
enable time limiting (give milliseconds)
--tlimit-per=MS
enable time limiting per query (give milliseconds)
--rlimit=N
enable resource limiting (currently, roughly the number of SAT conflicts)
--rlimit-per=N
enable resource limiting per query
--hard-limit
the resource limit is hard potentially leaving the smtEngine in an unsafe state
(should be destroyed and rebuild after resourcing out) [*]
--cpu-time
measures CPU time if set to true and wall time if false (default false) [*]
ARITHMETIC THEORY OPTIONS
--unate-lemmas=MODE
determines which lemmas to add before solving (default is 'all', see
--unate-lemmas=help)
--arith-prop=MODE
turns on arithmetic propagation (default is 'old', see --arith-prop=help)
--heuristic-pivots=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
--standard-effort-variable-order-pivots=N
limits the number of pivots in a single invocation of check() at a non-full effort
level using Bland's pivot rule (EXPERTS only)
--error-selection-rule=RULE
change the pivot rule for the basic variable (default is 'min', see --pivot-rule
help)
--simplex-check-period=N
the number of pivots to do in simplex before rechecking for a conflict on all
variables
--pivot-threshold=N
sets the number of pivots using --pivot-rule per basic variable per simplex
instance before using variable order
--prop-row-length=N
sets the maximum row length to be used in propagation
--enable-dio-solver
turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)
--disable-dio-solver
turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)
--enable-arith-rewrite-equalities
turns on the preprocessing rewrite turning equalities into a conjunction of
inequalities
--disable-arith-rewrite-equalities
turns off the preprocessing rewrite turning equalities into a conjunction of
inequalities
--enable-miplib-trick
turns on the preprocessing step of attempting to infer bounds on miplib problems
--disable-miplib-trick
turns off the preprocessing step of attempting to infer bounds on miplib problems
--miplib-trick-subs=N
do substitution for miplib 'tmp' vars if defined in <= N eliminated vars
--cut-all-bounded
turns on the integer solving step of periodically cutting all integer variables
that have both upper and lower bounds [*]
--no-cut-all-bounded
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
--revert-arith-models-on-unsat
revert the arithmetic model to a known safe model on unsat if one is cached [*]
--fc-penalties
turns on degenerate pivot penalties [*]
--no-fc-penalties
turns off degenerate pivot penalties
--use-fcsimplex
use focusing and converging simplex (FMCAD 2013 submission) [*]
--use-soi
use sum of infeasibility simplex (FMCAD 2013 submission) [*]
--restrict-pivots
have a pivot cap for simplex at effort levels below fullEffort [*]
--collect-pivot-stats
collect the pivot history [*]
--use-approx
attempt to use an approximate solver [*]
--approx-branch-depth
maximum branch depth the approximate solver is allowed to take
--dio-decomps
let skolem variables for integer divisibility constraints leak from the dio solver
[*]
--new-prop
use the new row propagation system [*]
--arith-prop-clauses
rows shorter than this are propagated as clauses
--soi-qe
use quick explain to minimize the sum of infeasibility conflicts [*]
--rewrite-divk
rewrite division and mod when by a constant into linear terms [*]
--se-solve-int
attempt to use the approximate solve integer method on standard effort [*]
--lemmas-on-replay-failure
attempt to use external lemmas if approximate solve integer failed [*]
--dio-turns
turns in a row dio solver cutting gets
--rr-turns
round robin turn
--dio-repeat
handle dio solver constraints in mass or one at a time [*]
--replay-early-close-depth
multiples of the depths to try to close the approx log eagerly
--replay-failure-penalty
number of solve integer attempts to skips after a numeric failure
--replay-num-err-penalty
number of solve integer attempts to skips after a numeric failure
--replay-reject-cut
maximum complexity of any coefficient while replaying cuts
--replay-lemma-reject-cut
maximum complexity of any coefficient while outputting replaying cut lemmas
--replay-soi-major-threshold
threshold for a major tolerance failure by the approximate solver
--replay-soi-major-threshold-pen
threshold for a major tolerance failure by the approximate solver
--replay-soi-minor-threshold
threshold for a minor tolerance failure by the approximate solver
--replay-soi-minor-threshold-pen
threshold for a minor tolerance failure by the approximate solver
--pp-assert-max-sub-size
threshold for substituting an equality in ppAssert
--max-replay-tree
threshold for attempting to replay a tree
--pb-rewrites
apply pseudo boolean rewrites [*]
--pb-rewrite-threshold
threshold of number of pseudoboolean variables to have before doing rewrites
--snorm-infer-eq
infer equalities based on Shostak normalization [*]
--nl-ext
extended approach to non-linear [*]
--nl-ext-rbound
use resolution-style inference for inferring new bounds [*]
--nl-ext-tplanes
use non-terminating tangent plane strategy for non-linear [*]
--nl-ext-ent-conf
check for entailed conflicts in non-linear solver [*]
--nl-ext-rewrite
do rewrites in non-linear solver [*]
--nl-ext-solve-subs
do solving for determining constant substitutions [*]
--nl-ext-purify
purify non-linear terms at preprocess [*]
--nl-ext-split-zero
intial splits on zero for all variables [*]
ARRAYS THEORY OPTIONS
--arrays-optimize-linear
turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)
[*]
--arrays-lazy-rintro1
turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett
2012: Being Careful with Theory Combination) [*]
--arrays-weak-equiv
use algorithm from Christ/Hoenicke (SMT 2014) [*]
--arrays-model-based
turn on model-based array solver [*]
--arrays-eager-index
turn on eager index splitting for generated array lemmas [*]
--arrays-eager-lemmas
turn on eager lemma generation for arrays [*]
--arrays-config
set different array option configurations - for developers only
--arrays-reduce-sharing
use model information to reduce size of care graph for arrays [*]
--arrays-prop
propagation effort for arrays: 0 is none, 1 is some, 2 is full
BASE OPTIONS
--stats-every-query
in incremental mode, print stats after every satisfiability or validity query [*]
--stats-hide-zeros
hide statistics which are zero
--stats-show-zeros
show statistics even when they are zero (default)
--parse-only
exit after parsing input [*]
--preprocess-only
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
--print-success
print the "success" output required of SMT-LIBv2 [*]
--smtlib-strict
SMT-LIBv2 compliance mode (implies other options)
BITVECTOR THEORY OPTIONS
--bv-sat-solver=MODE
choose which sat solver to use, see --bv-sat-solver=help (EXPERTS only)
--bitblast=MODE
choose bitblasting mode, see --bitblast=help
--bitblast-aig
bitblast by first converting to AIG (implies --bitblast=eager) [*]
--bv-aig-simp=COMMAND
abc command to run AIG simplifications (implies --bitblast-aig, default is
"balance;drw") (EXPERTS only)
--bv-propagate
use bit-vector propagation in the bit-blaster [*]
--bv-eq-solver
use the equality engine for the bit-vector theory (only if --bitblast=lazy) [*]
--bv-eq-slicer=MODE
turn on the slicing equality solver for the bit-vector theory (only if
--bitblast=lazy)
--bv-inequality-solver
turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)
[*]
--bv-algebraic-solver
turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy)
[*]
--bv-algebraic-budget
the budget allowed for the algebraic solver in number of SAT conflicts (EXPERTS
only)
--bv-to-bool
lift bit-vectors of size 1 to booleans when possible [*]
--bool-to-bv
convert booleans to bit-vectors of size 1 when possible [*]
--bv-div-zero-const
always return -1 on division by zero [*]
--bv-extract-arith
enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)
(EXPERTS only) [*]
--bv-abstraction
mcm benchmark abstraction (EXPERTS only) [*]
--bv-skolemize
skolemize arguments for bv abstraction (only does something if --bv-abstraction is
on) (EXPERTS only) [*]
--bv-num-func=NUM
number of function symbols in conflicts that are generalized (EXPERTS only)
--bv-eager-explanations
compute bit-blasting propagation explanations eagerly (EXPERTS only) [*]
--bv-quick-xplain
minimize bv conflicts using the QuickXplain algorithm (EXPERTS only) [*]
--bv-intro-pow2
introduce bitvector powers of two as a preprocessing pass (EXPERTS only) [*]
--bv-lazy-rewrite-extf
lazily rewrite extended functions like bv2nat and int2bv [*]
--bv-lazy-reduce-extf
reduce extended functions like bv2nat and int2bv at last call instead of full
effort [*]
--bv-alg-extf
algebraic inferences for extended functions [*]
DATATYPES THEORY OPTIONS
--dt-rewrite-error-sel
rewrite incorrectly applied selectors to arbitrary ground term (EXPERTS only) [*]
--dt-force-assignment
force the datatypes solver to give specific values to all datatypes terms before
answering sat [*]
--dt-binary-split
do binary splits for datatype constructor types [*]
--dt-ref-sk-intro
introduce reference skolems for shorter explanations [*]
--dt-use-testers
do not preprocess away tester predicates [*]
--cdt-bisimilar
do bisimilarity check for co-datatypes [*]
--dt-cyclic
do cyclicity check for datatypes [*]
--dt-infer-as-lemmas
always send lemmas out instead of making internal inferences [*]
--dt-blast-splits
when applicable, blast splitting lemmas for all variables at once [*]
DECISION HEURISTICS OPTIONS
--decision=MODE
choose decision mode, see --decision=help
--decision-threshold=N
ignore all nodes greater than threshold in first attempt to pick decision (EXPERTS
only)
--decision-use-weight
use the weight nodes (locally, by looking at children) to direct recursive search
(EXPERTS only) [*]
--decision-random-weight=N
assign random weights to nodes between 0 and N-1 (0: disable) (EXPERTS only)
--decision-weight-internal=HOW
computer weights of internal nodes using children: off, max, sum, usr1 (meaning
evolving) (EXPERTS only)
EXPRESSION PACKAGE OPTIONS
--default-expr-depth=N
print exprs to depth N (0 == default, -1 == no limit)
--default-dag-thresh=N
dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
--print-expr-types
print types with variables when printing exprs [*]
--eager-type-checking
type check expressions immediately on creation (debug builds only)
--lazy-type-checking
type check expressions only when necessary (default)
IDL OPTIONS
--enable-idl-rewrite-equalities
enable rewriting equalities into two inequalities in IDL solver (default is
disabled)
--disable-idl-rewrite-equalities
disable rewriting equalities into two inequalities in IDL solver (default is
disabled)
DRIVER OPTIONS
--show-debug-tags
show all available tags for debugging
--show-trace-tags
show all available tags for tracing
--early-exit
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..#threads-1)
--thread-stack=N
stack size for worker threads in MB (0 means use Boost/thread lib default)
--filter-lemma-length=N
don't share (among portfolio threads) lemmas strictly longer than N
--fallback-sequential
Switch to sequential mode (instead of printing an error) if it can't be solved in
portfolio mode [*]
--incremental-parallel
Use parallel solver even in incremental mode (may print 'unknown's at times) [*]
--interactive
force interactive/non-interactive mode [*]
--continued-execution
continue executing commands, even on error
--segv-spin
spin on segfault/other crash waiting for gdb [*]
--tear-down-incremental=N
implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N
queries (EXPERTS only)
--wait-to-join
wait for other threads to join before quitting (EXPERTS only) [*]
PARSER OPTIONS
--mmap memory map file input [*]
PRINTING OPTIONS
--model-format=MODE
print format mode for models, see --model-format=help
--inst-format=MODE
print format mode for instantiations, see --inst-format=help
PROOF OPTIONS
--lfsc-letification
turns on global letification in LFSC proofs [*]
--aggressive-core-min
turns on aggressive unsat core minimization (experimental) [*]
--fewer-preprocessing-holes
try to eliminate preprocessing holes in proofs [*]
--allow-empty-dependencies
if unable to track the dependencies of a rewritten/preprocessed assertion, fail
silently [*]
SAT LAYER OPTIONS
--random-freq=P
sets the frequency of random decisions in the sat solver (P=0.0 by default)
--random-seed=S
sets the random seed for the sat solver
--restart-int-base=N
sets the base restart interval for the sat solver (N=25 by default)
--restart-int-inc=F
sets the restart interval increase factor for the sat solver (F=3.0 by default)
--refine-conflicts
refine theory conflict clauses (default false) [*]
--minisat-elimination
use Minisat elimination [*]
--minisat-dump-dimacs
instead of solving minisat dumps the asserted clauses in Dimacs format [*]
QUANTIFIERS OPTIONS
--miniscope-quant
miniscope quantifiers [*]
--miniscope-quant-fv
miniscope quantifiers for ground subformulas [*]
--quant-split
apply splitting to quantified formulas based on variable disjoint disjuncts [*]
--prenex-quant=MODE
prenex mode for quantified formulas
--prenex-quant-user
prenex quantified formulas with user patterns [*]
--var-elim-quant
enable simple variable elimination for quantified formulas [*]
--var-ineq-elim-quant
enable variable elimination based on infinite projection of unbound arithmetic
variables [*]
--dt-var-exp-quant
expand datatype variables bound to one constructor in quantifiers [*]
--ite-lift-quant=MODE
ite lifting mode for quantified formulas
--cond-var-split-quant
split quantified formulas that lead to variable eliminations [*]
--cond-var-split-agg-quant
aggressive split quantified formulas that lead to variable eliminations [*]
--ite-dtt-split-quant
split ites with dt testers as conditions [*]
--pre-skolem-quant
apply skolemization eagerly to bodies of quantified formulas [*]
--pre-skolem-quant-nested
apply skolemization to nested quantified formulas [*]
--pre-skolem-quant-agg
apply skolemization to quantified formulas aggressively [*]
--ag-miniscope-quant
perform aggressive miniscoping for quantifiers [*]
--elim-taut-quant
eliminate tautological disjuncts of quantified formulas [*]
--elim-ext-arith-quant
eliminate extended arithmetic symbols in quantified formulas [*]
--cond-rewrite-quant
conditional rewriting of quantified formulas [*]
--e-matching
whether to do heuristic E-matching [*]
--term-db-mode
which ground terms to consider for instantiation
--register-quant-body-terms
consider ground terms within bodies of quantified formulas for matching [*]
--infer-arith-trigger-eq
infer equalities for trigger terms based on solving arithmetic equalities [*]
--infer-arith-trigger-eq-exp
record explanations for inferArithTriggerEq [*]
--strict-triggers
only instantiate quantifiers with user patterns based on triggers [*]
--relevant-triggers
prefer triggers that are more relevant based on SInE style analysis [*]
--relational-triggers
choose relational triggers such as x = f(y), x >= f(y) [*]
--purify-triggers
purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 [*]
--purify-dt-triggers
purify dt triggers, match all constructors of correct form instead of selectors [*]
--pure-th-triggers
use pure theory terms as single triggers [*]
--partial-triggers
use triggers that do not contain all free variables [*]
--multi-trigger-when-single
select multi triggers when single triggers exist [*]
--multi-trigger-priority
only try multi triggers if single triggers give no instantiations [*]
--multi-trigger-cache
caching version of multi triggers [*]
--multi-trigger-linear
implementation of multi triggers where maximum number of instantiations is linear
wrt number of ground terms [*]
--trigger-sel
selection mode for triggers
--trigger-active-sel
selection mode to activate triggers
--user-pat=MODE
policy for handling user-provided patterns for quantifier instantiation
--increment-triggers
generate additional triggers as needed during search [*]
--inst-when=MODE
when to apply instantiation
--inst-when-strict-interleave
ensure theory combination and standard quantifier effort strategies take turns [*]
--inst-when-phase=N
instantiation rounds quantifiers takes (>=1) before allowing theory combination to
happen
--inst-when-tc-first
allow theory combination to happen once initially, before quantifier strategies are
run [*]
--quant-model-ee
use equality engine of model for last call effort [*]
--inst-max-level=N
maximum inst level of terms used to instantiate quantified formulas with (-1 == no
limit, default)
--inst-level-input-only
only input terms are assigned instantiation level zero [*]
--quant-rep-mode=MODE
selection mode for representatives in quantifiers engine
--inst-rlv-cond
add relevancy conditions for instantiations [*]
--full-saturate-quant
when all other quantifier instantiation strategies fail, instantiate with ground
terms from relevant domain, then arbitrary ground terms before answering unknown
[*]
--full-saturate-quant-rd
whether to use relevant domain first for full saturation instantiation strategy [*]
--fs-inst
interleave full saturate instantiation with other techniques [*]
--literal-matching=MODE
choose literal matching mode
--finite-model-find
use finite model finding heuristic for quantifier instantiation [*]
--quant-fun-wd
assume that function defined by quantifiers are well defined [*]
--fmf-fun
find models for recursively defined functions, assumes functions are admissible [*]
--fmf-fun-rlv
find models for recursively defined functions, assumes functions are admissible,
allows empty type when function is irrelevant [*]
--fmf-empty-sorts
allow finite model finding to assume sorts that do not occur in ground assertions
are empty [*]
--mbqi=MODE
choose mode for model-based quantifier instantiation
--mbqi-one-inst-per-round
only add one instantiation per quantifier per round for mbqi [*]
--mbqi-one-quant-per-round
only add instantiations for one quantifier per round for mbqi [*]
--fmf-inst-engine
use instantiation engine in conjunction with finite model finding [*]
--fmf-inst-gen
enable Inst-Gen instantiation techniques for finite model finding [*]
--fmf-inst-gen-one-quant-per-round
only perform Inst-Gen instantiation techniques on one quantifier per round [*]
--fmf-fresh-dc
use fresh distinguished representative when applying Inst-Gen techniques [*]
--fmf-fmc-simple
simple models in full model check for finite model finding [*]
--fmf-bound-int
finite model finding on bounded integer quantification [*]
--fmf-bound
finite model finding on bounded quantification [*]
--fmf-bound-lazy
enforce bounds for bounded quantification lazily via use of proxy variables [*]
--fmf-bound-min-mode=MODE
mode for which types of bounds to minimize via first decision heuristics
--quant-cf
enable conflict find mechanism for quantifiers [*]
--quant-cf-mode=MODE
what effort to apply conflict find mechanism
--quant-cf-when=MODE
when to invoke conflict find mechanism for quantifiers
--qcf-tconstraint
enable entailment checks for t-constraints in qcf algorithm [*]
--qcf-all-conflict
add all available conflicting instances during conflict-based instantiation [*]
--qcf-nested-conflict
consider conflicts for nested quantifiers [*]
--qcf-vo-exp
qcf experimental variable ordering [*]
--inst-no-entail
do not consider instances of quantified formulas that are currently entailed [*]
--inst-no-model-true
do not consider instances of quantified formulas that are currently true in model,
if it is available [*]
--inst-prop
internal propagation for instantiations for selecting relevant instances [*]
--qcf-eager-test
optimization, test qcf instances eagerly [*]
--qcf-eager-check-rd
optimization, eagerly check relevant domain of matched position [*]
--qcf-skip-rd
optimization, skip instances based on possibly irrelevant portions of quantified
formulas [*]
--rewrite-rules
use rewrite rules module [*]
--rr-one-inst-per-round
add one instance of rewrite rule per round [*]
--quant-ind
use all available techniques for inductive reasoning [*]
--dt-stc-ind
apply strengthening for existential quantification over datatypes based on
structural induction [*]
--int-wf-ind
apply strengthening for integers based on well-founded induction [*]
--conjecture-gen
generate candidate conjectures for inductive proofs [*]
--conjecture-gen-per-round=N
number of conjectures to generate per instantiation round
--conjecture-no-filter
do not filter conjectures [*]
--conjecture-filter-active-terms
filter based on active terms [*]
--conjecture-filter-canonical
filter based on canonicity [*]
--conjecture-filter-model
filter based on model [*]
--conjecture-gen-gt-enum=N
number of ground terms to generate for model filtering
--conjecture-gen-uee-intro
more aggressive merging for universal equality engine, introduces terms [*]
--conjecture-gen-max-depth=N
maximum depth of terms to consider for conjectures
--cegqi
counterexample-guided quantifier instantiation [*]
--cegqi-fair=MODE
if and how to apply fairness for cegqi
--cegqi-si=MODE
mode for processing single invocation synthesis conjectures
--cegqi-si-partial
combined techniques for synthesis conjectures that are partially single invocation
[*]
--cegqi-si-reconstruct
reconstruct solutions for single invocation conjectures in original grammar [*]
--cegqi-si-sol-min-core
minimize solutions for single invocation conjectures based on unsat core [*]
--cegqi-si-sol-min-inst
minimize individual instantiations for single invocation conjectures based on
unsat core [*]
--cegqi-si-reconstruct-const
include constants when reconstruct solutions for single invocation conjectures in
original grammar [*]
--cegqi-si-abort
abort if synthesis conjecture is not single invocation [*]
--sygus-nf
only search for sygus builtin terms that are in normal form [*]
--sygus-nf-arg
account for relationship between arguments of operations in sygus normal form [*]
--sygus-nf-sym
narrow sygus search space based on global state of current candidate program [*]
--sygus-nf-sym-gen
generalize lemmas for global search space narrowing [*]
--sygus-nf-sym-arg
generalize based on arguments in global search space narrowing [*]
--sygus-nf-sym-content
generalize based on content in global search space narrowing [*]
--sygus-inv-templ=MODE
template mode for sygus invariant synthesis
--sygus-unif-csol
enable approach which unifies conditional solutions [*]
--sygus-direct-eval
direct unfolding of evaluation functions [*]
--sygus-cref-eval
direct evaluation of refinement lemmas for conflict analysis [*]
--cbqi turns on counterexample-based quantifier instantiation [*]
--cbqi-recurse
turns on recursive counterexample-based quantifier instantiation [*]
--cbqi-sat
answer sat when quantifiers are asserted with counterexample-based quantifier
instantiation [*]
--cbqi-model
guide instantiations by model values for counterexample-based quantifier
instantiation [*]
--cbqi-all
apply counterexample-based instantiation to all quantified formulas [*]
--cbqi-use-inf-int
use integer infinity for vts in counterexample-based quantifier instantiation [*]
--cbqi-use-inf-real
use real infinity for vts in counterexample-based quantifier instantiation [*]
--cbqi-prereg-inst
preregister ground instantiations in counterexample-based quantifier instantiation
[*]
--cbqi-min-bounds
use minimally constrained lower/upper bound for counterexample-based quantifier
instantiation [*]
--cbqi-round-up-lia
round up integer lower bounds in substitutions for counterexample-based quantifier
instantiation [*]
--cbqi-midpoint
choose substitutions based on midpoints of lower and upper bounds for
counterexample-based quantifier instantiation [*]
--cbqi-nopt
non-optimal bounds for counterexample-based quantifier instantiation [*]
--cbqi-lit-dep
dependency lemmas for quantifier alternation in counterexample-based quantifier
instantiation [*]
--cbqi-innermost
only process innermost quantified formulas in counterexample-based quantifier
instantiation [*]
--cbqi-nested-qe
process nested quantified formulas with quantifier elimination in
counterexample-based quantifier instantiation [*]
--quant-epr
infer whether in effectively propositional fragment, use for cbqi [*]
--quant-epr-match
use matching heuristics for EPR instantiation [*]
--local-t-ext
do instantiation based on local theory extensions [*]
--lte-partial-inst
partially instantiate local theory quantifiers [*]
--lte-restrict-inst-closure
treat arguments of inst closure as restricted terms for instantiation [*]
--quant-alpha-equiv
infer alpha equivalence between quantified formulas [*]
--macros-quant
perform quantifiers macro expansion [*]
--macros-quant-mode=MODE
mode for quantifiers macro expansion
--quant-dsplit-mode=MODE
mode for dynamic quantifiers splitting
--quant-anti-skolem
perform anti-skolemization for quantified formulas [*]
--quant-ee
maintain congrunce closure over universal equalities [*]
--track-inst-lemmas
track instantiation lemmas (for proofs, unsat cores, qe and synthesis
minimization) [*]
SEP OPTIONS
--sep-check-neg
check negated spatial assertions [*]
--sep-exp
experimental flag for sep [*]
--sep-min-refine
only add refinement lemmas for minimal (innermost) assertions [*]
--sep-deq-c
assume cardinality elements are distinct [*]
--sep-pre-skolem-emp
eliminate emp constraint at preprocess time [*]
--sep-child-refine
child-specific refinements of negated star, positive wand [*]
SETS OPTIONS
--sets-proxy-lemmas
introduce proxy variables eagerly to shorten lemmas [*]
--sets-infer-as-lemmas
send inferences as lemmas [*]
--sets-rel-eager
standard effort checks for relations [*]
--sets-ext
enable extended symbols such as complement and universe in theory of sets [*]
SMT LAYER OPTIONS
--force-logic=LOGIC
set the logic, and override all further user attempts to change it (EXPERTS only)
--simplification=MODE
choose simplification mode, see --simplification=help
--no-simplification
turn off all simplification (same as --simplification=none)
--static-learning
use static learning (on by default) [*]
--check-models
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
[*]
--dump-models
output models after every SAT/INVALID/UNKNOWN response [*]
--omit-dont-cares
When producing a model, omit variables whose value does not matter [*]
--proof
turn on proof generation [*]
--check-proofs
after UNSAT/VALID, machine-check the generated proof [*]
--dump-proofs
output proofs after every UNSAT/VALID response [*]
--dump-instantiations
output instantiations of quantified formulas after every UNSAT/VALID response [*]
--dump-synth
output solution for synthesis conjectures after every UNSAT/VALID response [*]
--produce-unsat-cores
turn on unsat core generation [*]
--check-unsat-cores
after UNSAT/VALID, produce and check an unsat core (expensive) [*]
--dump-unsat-cores
output unsat cores after every UNSAT/VALID response [*]
--dump-unsat-cores-full
dump the full unsat core, including unlabeled assertions [*]
--produce-assignments
support the get-assignment command [*]
--ite-simp
turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) [*]
--on-repeat-ite-simp
do the ite simplification pass again if repeating simplification [*]
--simp-with-care
enables simplifyWithCare in ite simplificiation [*]
--simp-ite-compress
enables compressing ites after ite simplification [*]
--unconstrained-simp
turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) [*]
--repeat-simp
make multiple passes with nonclausal simplifier [*]
--simp-ite-hunt-zombies
post ite compression enables zombie removal while the number of nodes is above this
threshold
--sort-inference
calculate sort inference of input problem, convert the input based on monotonic
sorts [*]
--abstract-values
in models, output arrays (and in future, maybe others) using abstract values, as
required by the SMT-LIB standard [*]
--model-u-dt-enum
in models, output uninterpreted sorts as datatype enumerations [*]
--rewrite-step
amount of resources spent for each rewrite step (EXPERTS only)
--theory-check-step
amount of resources spent for each theory check call (EXPERTS only)
--decision-step
amount of getNext decision calls in the decision engine (EXPERTS only)
--bitblast-step
amount of resources spent for each bitblast step (EXPERTS only)
--parse-step
amount of resources spent for each command/expression parsing (EXPERTS only)
--lemma-step
amount of resources spent when adding lemmas (EXPERTS only)
--restart-step
amount of resources spent for each theory restart (EXPERTS only)
--cnf-step
amount of resources spent for each call to cnf conversion (EXPERTS only)
--preprocess-step
amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)
--quantifier-step
amount of resources spent for quantifier instantiations (EXPERTS only)
--sat-conflict-step
amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)
--bv-sat-conflict-step
amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)
--rewrite-apply-to-const
eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 (EXPERTS
only) [*]
--force-no-limit-cpu-while-dump
Force no CPU limit when dumping models and proofs [*]
STRINGS THEORY OPTIONS
--strings-exp
experimental features in the theory of strings [*]
--strings-lb=N
the strategy of LB rule application: 0-lazy, 1-eager, 2-no
--strings-std-ascii
the alphabet contains only characters from the standard ASCII or the extended one
[*]
--strings-fmf
the finite model finding used by the theory of strings [*]
--strings-eager
strings eager check [*]
--strings-eit
the eager intersection used by the theory of strings [*]
--strings-opt1
internal option1 for strings: normal form [*]
--strings-opt2
internal option2 for strings: constant regexp splitting [*]
--strings-inm
internal for strings: ignore negative membership constraints (fragment checking is
needed, left to users for now) [*]
--strings-lazy-pp
perform string preprocessing lazily [*]
--strings-len-geqz
strings length greater than zero lemmas [*]
--strings-len-norm
strings length normalization lemma [*]
--strings-sp-emp
strings split on empty string [*]
--strings-infer-sym
strings split on empty string [*]
--strings-eager-len
strings eager length lemmas [*]
--strings-check-entail-len
check entailment between length terms to reduce splitting [*]
--strings-process-loop
reduce looping word equations to regular expressions [*]
--strings-abort-loop
abort when a looping word equation is encountered [*]
--strings-infer-as-lemmas
always send lemmas out instead of making internal inferences [*]
--strings-rexplain-lemmas
regression explanations for string lemmas [*]
--strings-min-prefix-explain
minimize explanations for prefix of normal forms in strings [*]
--strings-guess-model
use model guessing to avoid string extended function reductions [*]
--strings-uf-reduct
use uninterpreted functions when applying extended function reductions [*]
--strings-binary-csp
use binary search when splitting strings [*]
--strings-lprop-csp
do length propagation based on constant splits [*]
THEORY LAYER OPTIONS
--theoryof-mode=MODE
mode for Theory::theoryof() (EXPERTS only)
--use-theory=NAME
use alternate theory implementation NAME (--use-theory=help for a list). This
option may be repeated or a comma separated list.
UNINTERPRETED FUNCTIONS THEORY OPTIONS
--symmetry-breaker
use UF symmetry breaker (Deharbe et al., CADE 2011) [*]
--condense-function-values
condense models for functions rather than explicitly representing them [*]
--uf-ss-regions
disable region-based method for discovering cliques and splits in uf strong solver
[*]
--uf-ss-eager-split
add splits eagerly for uf strong solver [*]
--uf-ss-totality
always use totality axioms for enforcing cardinality constraints [*]
--uf-ss-totality-limited=N
apply totality axioms, but only up to cardinality N (-1 == do not apply totality
axioms, default)
--uf-ss-totality-sym-break
apply symmetry breaking for totality axioms [*]
--uf-ss-abort-card=N
tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
--uf-ss-explained-cliques
use explained clique lemmas for uf strong solver [*]
--uf-ss-simple-cliques
always use simple clique lemmas for uf strong solver [*]
--uf-ss-deq-prop
eagerly propagate disequalities for uf strong solver [*]
--uf-ss=MODE
mode of operation for uf strong solver.
--uf-ss-clique-splits
use cliques instead of splitting on demand to shrink model [*]
--uf-ss-sym-break
finite model finding symmetry breaking techniques [*]
--uf-ss-fair
use fair strategy for finite model finding multiple sorts [*]
--uf-ss-fair-monotone
group monotone sorts when enforcing fairness for finite model finding [*]
Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the
option.
DIAGNOSTICS
CVC4 reports all syntactic and semantic errors on standard error.
HISTORY
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
Nelson-Oppen 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 re-evaluation of the core
architecture to be both performant and to serve as a cutting-edge research vehicle for the
next several years. Rather than taking CVC3 and redesigning problem parts, we've taken a
clean-room 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 re-evaluation and ground-up 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 re-
engineering, which would have ballooned in short order.
VERSION
This manual page refers to CVC4 version 1.5.
BUGS
A Bugzilla for the CVC4 project is maintained at http://cvc4.cs.nyu.edu/bugzilla3/.
AUTHORS
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.
SEE ALSO
The CVC4 wiki contains useful information about the design and internals of CVC4. It is
maintained at http://cvc4.cs.nyu.edu/wiki/.