Provided by: cvc4_1.6-2build2_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)
--quiet | -q
decrease verbosity (may be repeated)
--stats
give statistics on exit [*]
--verbose | -v
increase verbosity (may be repeated)
--copyright
show CVC4 copyright information
--help | -h
full command line reference
--seed | -s
seed for random number generator
--show-config
show CVC4 static configuration
--version | -V
identify this CVC4 binary
--strict-parsing
be less tolerant of non-conforming inputs [*]
--cpu-time
measures CPU time if set to true and wall time if false (default false) [*]
--dump-to=FILE
all dumping goes to FILE (instead of stdout)
--dump=MODE
dump preprocessed assertions, etc., see --dump=help
--hard-limit
the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be
destroyed and rebuild after resourcing out) [*]
--incremental | -i
enable incremental solving [*]
--produce-assertions
keep an assertions list (enables get-assertions command) [*]
--produce-models | -m
support the get-value and get-model commands [*]
--rlimit-per=N
enable resource limiting per query
--rlimit=N
enable resource limiting (currently, roughly the number of SAT conflicts)
--tlimit-per=MS
enable time limiting per query (give milliseconds)
--tlimit=MS
enable time limiting (give milliseconds)
ARITHMETIC THEORY OPTIONS
--approx-branch-depth
maximum branch depth the approximate solver is allowed to take
--arith-no-partial-fun
do not use partial function semantics for arithmetic (not SMT LIB compliant) [*]
--arith-prop-clauses
rows shorter than this are propagated as clauses
--arith-prop=MODE
turns on arithmetic propagation (default is 'old', see --arith-prop=help)
--arith-rewrite-equalities
turns on the preprocessing rewrite turning equalities into a conjunction of inequalities [*]
--collect-pivot-stats
collect the pivot history [*]
--cut-all-bounded
turns on the integer solving step of periodically cutting all integer variables that have both
upper and lower bounds [*]
--dio-decomps
let skolem variables for integer divisibility constraints leak from the dio solver [*]
--dio-repeat
handle dio solver constraints in mass or one at a time [*]
--dio-solver
turns on Linear Diophantine Equation solver (Griggio, JSAT 2012) [*]
--dio-turns
turns in a row dio solver cutting gets
--error-selection-rule=RULE
change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)
--fc-penalties
turns on degenerate pivot penalties [*]
--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
--lemmas-on-replay-failure
attempt to use external lemmas if approximate solve integer failed [*]
--maxCutsInContext
maximum cuts in a given context before signalling a restart
--miplib-trick
turns on 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
--new-prop
use the new row propagation system [*]
--nl-ext
extended approach to non-linear [*]
--nl-ext-ent-conf
check for entailed conflicts in non-linear solver [*]
--nl-ext-factor
use factoring inference in non-linear solver [*]
--nl-ext-inc-prec
whether to increment the precision for irrational function constraints [*]
--nl-ext-purify
purify non-linear terms at preprocess [*]
--nl-ext-rbound
use resolution-style inference for inferring new bounds [*]
--nl-ext-rewrite
do rewrites in non-linear solver [*]
--nl-ext-split-zero
initial splits on zero for all variables [*]
--nl-ext-tf-taylor-deg=N
initial degree of polynomials for Taylor approximation
--nl-ext-tf-tplanes
use non-terminating tangent plane strategy for transcendental functions for non-linear [*]
--nl-ext-tplanes
use non-terminating tangent plane strategy for non-linear [*]
--nl-ext-tplanes-interleave
interleave tangent plane strategy for non-linear [*]
--pb-rewrites
apply pseudo boolean rewrites [*]
--pivot-threshold=N
sets the number of pivots using --pivot-rule per basic variable per simplex instance before using
variable order
--pp-assert-max-sub-size
threshold for substituting an equality in ppAssert
--prop-row-length=N
sets the maximum row length to be used in propagation
--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-lemma-reject-cut
maximum complexity of any coefficient while outputting replaying cut lemmas
--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-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
--restrict-pivots
have a pivot cap for simplex at effort levels below fullEffort [*]
--revert-arith-models-on-unsat
revert the arithmetic model to a known safe model on unsat if one is cached [*]
--rewrite-divk
rewrite division and mod when by a constant into linear terms [*]
--rr-turns
round robin turn
--se-solve-int
attempt to use the approximate solve integer method on standard effort [*]
--simplex-check-period=N
the number of pivots to do in simplex before rechecking for a conflict on all variables
--snorm-infer-eq
infer equalities based on Shostak normalization [*]
--soi-qe
use quick explain to minimize the sum of infeasibility conflicts [*]
--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)
--unate-lemmas=MODE
determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)
--use-approx
attempt to use an approximate solver [*]
--use-fcsimplex
use focusing and converging simplex (FMCAD 2013 submission) [*]
--use-soi
use sum of infeasibility simplex (FMCAD 2013 submission) [*]
ARRAYS THEORY OPTIONS
--arrays-config
set different array option configurations - for developers only
--arrays-eager-index
turn on eager index splitting for generated array lemmas [*]
--arrays-eager-lemmas
turn on eager lemma generation for arrays [*]
--arrays-lazy-rintro1
turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being
Careful with Theory Combination) [*]
--arrays-model-based
turn on model-based array solver [*]
--arrays-optimize-linear
turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper) [*]
--arrays-prop
propagation effort for arrays: 0 is none, 1 is some, 2 is full
--arrays-reduce-sharing
use model information to reduce size of care graph for arrays [*]
--arrays-weak-equiv
use algorithm from Christ/Hoenicke (SMT 2014) [*]
BASE OPTIONS
--debug=TAG | -d TAG
debug something (e.g. -d arith), can repeat
--parse-only
exit after parsing input [*]
--preprocess-only
exit after preprocessing input [*]
--print-success
print the "success" output required of SMT-LIBv2 [*]
--stats-every-query
in incremental mode, print stats after every satisfiability or validity query [*]
--stats-hide-zeros
hide statistics which are zero [*]
--trace=TAG | -t TAG
trace something (e.g. -t pushpop), can repeat
--smtlib-strict
SMT-LIBv2 compliance mode (implies other options)
BITVECTOR THEORY OPTIONS
--bitblast-aig
bitblast by first converting to AIG (implies --bitblast=eager) [*]
--bitblast=MODE
choose bitblasting mode, see --bitblast=help
--bool-to-bv
convert booleans to bit-vectors of size 1 when possible [*]
--bv-abstraction
mcm benchmark abstraction (EXPERTS only) [*]
--bv-aig-simp=COMMAND
abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") (EXPERTS
only)
--bv-alg-extf
algebraic inferences for extended functions [*]
--bv-algebraic-budget
the budget allowed for the algebraic solver in number of SAT conflicts (EXPERTS only)
--bv-algebraic-solver
turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy) [*]
--bv-div-zero-const
always return -1 on division by zero [*]
--bv-eager-explanations
compute bit-blasting propagation explanations eagerly (EXPERTS only) [*]
--bv-eq-slicer=MODE
turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)
--bv-eq-solver
use the equality engine for the bit-vector theory (only if --bitblast=lazy) [*]
--bv-extract-arith
enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) (EXPERTS only) [*]
--bv-gauss-elim
simplify formula via Gaussian Elimination if applicable (EXPERTS only) [*]
--bv-inequality-solver
turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy) [*]
--bv-intro-pow2
introduce bitvector powers of two as a preprocessing pass (EXPERTS only) [*]
--bv-lazy-reduce-extf
reduce extended functions like bv2nat and int2bv at last call instead of full effort [*]
--bv-lazy-rewrite-extf
lazily rewrite extended functions like bv2nat and int2bv [*]
--bv-num-func=NUM
number of function symbols in conflicts that are generalized (EXPERTS only)
--bv-propagate
use bit-vector propagation in the bit-blaster [*]
--bv-quick-xplain
minimize bv conflicts using the QuickXplain algorithm (EXPERTS only) [*]
--bv-sat-solver=MODE
choose which sat solver to use, see --bv-sat-solver=help (EXPERTS only)
--bv-skolemize
skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) (EXPERTS
only) [*]
--bv-to-bool
lift bit-vectors of size 1 to booleans when possible [*]
DATATYPES THEORY OPTIONS
--cdt-bisimilar
do bisimilarity check for co-datatypes [*]
--dt-binary-split
do binary splits for datatype constructor types [*]
--dt-blast-splits
when applicable, blast splitting lemmas for all variables at once [*]
--dt-cyclic
do cyclicity check for datatypes [*]
--dt-force-assignment
force the datatypes solver to give specific values to all datatypes terms before answering sat [*]
--dt-infer-as-lemmas
always send lemmas out instead of making internal inferences [*]
--dt-ref-sk-intro
introduce reference skolems for shorter explanations [*]
--dt-rewrite-error-sel
rewrite incorrectly applied selectors to arbitrary ground term (EXPERTS only) [*]
--dt-share-sel
internally use shared selectors across multiple constructors [*]
--dt-use-testers
do not preprocess away tester predicates [*]
--sygus-abort-size=N
tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)
--sygus-eval-builtin
use builtin kind for evaluation functions in sygus [*]
--sygus-fair-max
use max instead of sum for multi-function sygus conjectures [*]
--sygus-fair=MODE
if and how to apply fairness for sygus
--sygus-opt1
sygus experimental option [*]
--sygus-sym-break
simple sygus sym break lemmas [*]
--sygus-sym-break-dynamic
dynamic sygus sym break lemmas [*]
--sygus-sym-break-lazy
lazily add symmetry breaking lemmas for terms [*]
--sygus-sym-break-pbe
sygus sym break lemmas based on pbe conjectures [*]
--sygus-sym-break-rlv
add relevancy conditions to symmetry breaking lemmas [*]
DECISION HEURISTICS OPTIONS
--decision-random-weight=N
assign random weights to nodes between 0 and N-1 (0: disable) (EXPERTS only)
--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-weight-internal=HOW
computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) (EXPERTS
only)
--decision=MODE
choose decision mode, see --decision=help
EXPRESSION PACKAGE OPTIONS
--default-dag-thresh=N
dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
--default-expr-depth=N
print exprs to depth N (0 == default, -1 == no limit)
--eager-type-checking
type check expressions immediately on creation (debug builds only) [*]
--print-expr-types
print types with variables when printing exprs [*]
--type-checking
never type check expressions
IDL OPTIONS
--idl-rewrite-equalities
enable rewriting equalities into two inequalities in IDL solver (default is disabled) [*]
DRIVER OPTIONS
--continued-execution
continue executing commands, even on error [*]
--early-exit
do not run destructors at exit; default on except in debug builds (EXPERTS only) [*]
--fallback-sequential
Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode
[*]
--filter-lemma-length=N
don't share (among portfolio threads) lemmas strictly longer than N
--incremental-parallel
Use parallel solver even in incremental mode (may print 'unknown's at times) [*]
--interactive
force interactive/non-interactive mode [*]
--segv-spin
spin on segfault/other crash waiting for gdb [*]
--show-debug-tags
show all available tags for debugging
--show-trace-tags
show all available tags for tracing
--tear-down-incremental=N
implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries (EXPERTS
only)
--thread-stack=N
stack size for worker threads in MB (0 means use Boost/thread lib default)
--threadN=string
configures portfolio thread N (0..#threads-1)
--threads=N
Total number of threads for portfolio
--wait-to-join
wait for other threads to join before quitting (EXPERTS only) [*]
PARSER OPTIONS
--mmap memory map file input [*]
PRINTING OPTIONS
--inst-format=MODE
print format mode for instantiations, see --inst-format=help
--model-format=MODE
print format mode for models, see --model-format=help
PROOF OPTIONS
--aggressive-core-min
turns on aggressive unsat core minimization (experimental) [*]
--allow-empty-dependencies
if unable to track the dependencies of a rewritten/preprocessed assertion, fail silently [*]
--fewer-preprocessing-holes
try to eliminate preprocessing holes in proofs [*]
--lfsc-letification
turns on global letification in LFSC proofs [*]
SAT LAYER OPTIONS
--minisat-dump-dimacs
instead of solving minisat dumps the asserted clauses in Dimacs format [*]
--minisat-elimination
use Minisat elimination [*]
--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
--refine-conflicts
refine theory conflict clauses (default false) [*]
--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)
QUANTIFIERS OPTIONS
--ag-miniscope-quant
perform aggressive miniscoping for quantifiers [*]
--cbqi turns on counterexample-based quantifier instantiation [*]
--cbqi-all
apply counterexample-based instantiation to all quantified formulas [*]
--cbqi-bv
use word-level inversion approach for counterexample-guided quantifier instantiation for
bit-vectors [*]
--cbqi-bv-concat-inv
compute inverse for concat over equalities rather than producing an invertibility condition [*]
--cbqi-bv-ineq=MODE
choose mode for handling bit-vector inequalities with counterexample-guided instantiation
--cbqi-bv-interleave-value
interleave model value instantiation with word-level inversion approach [*]
--cbqi-bv-linear
linearize adder chains for variables [*]
--cbqi-bv-rm-extract
replaces extract terms with variables for counterexample-guided instantiation for bit-vectors [*]
--cbqi-bv-solve-nl
try to solve non-linear bv literals using model value projections [*]
--cbqi-full
turns on full effort counterexample-based quantifier instantiation, which may resort to
model-value instantiation [*]
--cbqi-innermost
only process innermost quantified formulas in counterexample-based quantifier instantiation [*]
--cbqi-lit-dep
dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation [*]
--cbqi-midpoint
choose substitutions based on midpoints of lower and upper bounds for counterexample-based
quantifier instantiation [*]
--cbqi-min-bounds
use minimally constrained lower/upper bound for counterexample-based quantifier instantiation [*]
--cbqi-model
guide instantiations by model values for counterexample-based quantifier instantiation [*]
--cbqi-multi-inst
when applicable, do multi instantiations per quantifier per round in counterexample-based
quantifier instantiation [*]
--cbqi-nested-qe
process nested quantified formulas with quantifier elimination in counterexample-based quantifier
instantiation [*]
--cbqi-nopt
non-optimal bounds for counterexample-based quantifier instantiation [*]
--cbqi-prereg-inst
preregister ground instantiations in counterexample-based quantifier instantiation [*]
--cbqi-recurse
turns on recursive counterexample-based quantifier instantiation [*]
--cbqi-repeat-lit
solve literals more than once in counterexample-based quantifier instantiation [*]
--cbqi-round-up-lia
round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
[*]
--cbqi-sat
answer sat when quantifiers are asserted with counterexample-based quantifier instantiation [*]
--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 [*]
--cegis-sample=MODE
mode for using samples in the counterexample-guided inductive synthesis loop
--cegqi
counterexample-guided quantifier instantiation for sygus [*]
--cegqi-si-abort
abort if synthesis conjecture is not single invocation [*]
--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-reconstruct-const
include constants when 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=MODE
mode for processing single invocation synthesis conjectures
--cond-rewrite-quant
conditional rewriting of quantified formulas [*]
--cond-var-split-agg-quant
aggressive split quantified formulas that lead to variable eliminations [*]
--cond-var-split-quant
split quantified formulas that lead to variable eliminations [*]
--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
generate candidate conjectures for inductive proofs [*]
--conjecture-gen-gt-enum=N
number of ground terms to generate for model filtering
--conjecture-gen-max-depth=N
maximum depth of terms to consider for conjectures
--conjecture-gen-per-round=N
number of conjectures to generate per instantiation round
--conjecture-gen-uee-intro
more aggressive merging for universal equality engine, introduces terms [*]
--conjecture-no-filter
do not filter conjectures [*]
--dt-stc-ind
apply strengthening for existential quantification over datatypes based on structural induction
[*]
--dt-var-exp-quant
expand datatype variables bound to one constructor in quantifiers [*]
--e-matching
whether to do heuristic E-matching [*]
--elim-ext-arith-quant
eliminate extended arithmetic symbols in quantified formulas [*]
--elim-taut-quant
eliminate tautological disjuncts of quantified formulas [*]
--finite-model-find
use finite model finding heuristic for quantifier instantiation [*]
--fmf-bound
finite model finding on bounded quantification [*]
--fmf-bound-int
finite model finding on bounded integer 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
--fmf-empty-sorts
allow finite model finding to assume sorts that do not occur in ground assertions are empty [*]
--fmf-fmc-simple
simple models in full model check for finite model finding [*]
--fmf-fresh-dc
use fresh distinguished representative when applying Inst-Gen techniques [*]
--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-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 [*]
--fs-interleave
interleave full saturate instantiation with other techniques [*]
--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 [*]
--global-negate
do global negation of input formula [*]
--ho-matching
do higher-order matching algorithm for triggers with variable operators [*]
--ho-matching-var-priority
give priority to variable arguments over constant arguments [*]
--ho-merge-term-db
merge term indices modulo equality [*]
--increment-triggers
generate additional triggers as needed during search [*]
--infer-arith-trigger-eq
infer equalities for trigger terms based on solving arithmetic equalities [*]
--infer-arith-trigger-eq-exp
record explanations for inferArithTriggerEq [*]
--inst-level-input-only
only input terms are assigned instantiation level zero [*]
--inst-max-level=N
maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
--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 [*]
--inst-when-phase=N
instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen
--inst-when-strict-interleave
ensure theory combination and standard quantifier effort strategies take turns [*]
--inst-when-tc-first
allow theory combination to happen once initially, before quantifier strategies are run [*]
--inst-when=MODE
when to apply instantiation
--int-wf-ind
apply strengthening for integers based on well-founded induction [*]
--ite-dtt-split-quant
split ites with dt testers as conditions [*]
--ite-lift-quant=MODE
ite lifting mode for quantified formulas
--literal-matching=MODE
choose literal matching mode
--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 [*]
--macros-quant
perform quantifiers macro expansion [*]
--macros-quant-mode=MODE
mode for quantifiers macro expansion
--mbqi-interleave
interleave model-based quantifier instantiation with other techniques [*]
--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 [*]
--mbqi=MODE
choose mode for model-based quantifier instantiation
--miniscope-quant
miniscope quantifiers [*]
--miniscope-quant-fv
miniscope quantifiers for ground subformulas [*]
--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 [*]
--multi-trigger-priority
only try multi triggers if single triggers give no instantiations [*]
--multi-trigger-when-single
select multi triggers when single triggers exist [*]
--partial-triggers
use triggers that do not contain all free variables [*]
--pre-skolem-quant
apply skolemization eagerly to bodies of quantified formulas [*]
--pre-skolem-quant-agg
apply skolemization to quantified formulas aggressively [*]
--pre-skolem-quant-nested
apply skolemization to nested quantified formulas [*]
--prenex-quant-user
prenex quantified formulas with user patterns [*]
--prenex-quant=MODE
prenex mode for quantified formulas
--pure-th-triggers
use pure theory terms as single triggers [*]
--purify-dt-triggers
purify dt triggers, match all constructors of correct form instead of selectors [*]
--purify-triggers
purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 [*]
--qcf-all-conflict
add all available conflicting instances during conflict-based instantiation [*]
--qcf-eager-check-rd
optimization, eagerly check relevant domain of matched position [*]
--qcf-eager-test
optimization, test qcf instances eagerly [*]
--qcf-nested-conflict
consider conflicts for nested quantifiers [*]
--qcf-skip-rd
optimization, skip instances based on possibly irrelevant portions of quantified formulas [*]
--qcf-tconstraint
enable entailment checks for t-constraints in qcf algorithm [*]
--qcf-vo-exp
qcf experimental variable ordering [*]
--quant-alpha-equiv
infer alpha equivalence between quantified formulas [*]
--quant-anti-skolem
perform anti-skolemization for quantified formulas [*]
--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
--quant-dsplit-mode=MODE
mode for dynamic quantifiers splitting
--quant-epr
infer whether in effectively propositional fragment, use for cbqi [*]
--quant-epr-match
use matching heuristics for EPR instantiation [*]
--quant-fun-wd
assume that function defined by quantifiers are well defined [*]
--quant-ind
use all available techniques for inductive reasoning [*]
--quant-model-ee
use equality engine of model for last call effort [*]
--quant-rep-mode=MODE
selection mode for representatives in quantifiers engine
--quant-split
apply splitting to quantified formulas based on variable disjoint disjuncts [*]
--register-quant-body-terms
consider ground terms within bodies of quantified formulas for matching [*]
--relational-triggers
choose relational triggers such as x = f(y), x >= f(y) [*]
--relevant-triggers
prefer triggers that are more relevant based on SInE style analysis [*]
--rewrite-rules
use rewrite rules module [*]
--rr-one-inst-per-round
add one instance of rewrite rule per round [*]
--strict-triggers
only instantiate quantifiers with user patterns based on triggers [*]
--sygus-add-const-grammar
statically add constants appearing in conjecture to grammars [*]
--sygus-auto-unfold
enable approach which automatically unfolds transition systems for directly solving invariant
synthesis problems [*]
--sygus-bool-ite-return-const
Only use Boolean constants for return values in unification-based function synthesis [*]
--sygus-eval-unfold
do unfolding of sygus evaluation functions [*]
--sygus-eval-unfold-bool
do unfolding of Boolean evaluation functions that appear in refinement lemmas [*]
--sygus-ext-rew
use extended rewriter for sygus [*]
--sygus-grammar-norm
statically normalize sygus grammars based on flattening (linearization) [*]
--sygus-inference
attempt to preprocess arbitrary inputs to sygus conjectures [*]
--sygus-inv-templ-when-sg
use invariant templates (with solution reconstruction) for syntax guided problems [*]
--sygus-inv-templ=MODE
template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or
none)
--sygus-min-grammar
statically minimize sygus grammars [*]
--sygus-pbe
enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe)
conjectures [*]
--sygus-qe-preproc
use quantifier elimination as a preprocessing step for sygus [*]
--sygus-ref-eval
direct evaluation of refinement lemmas for conflict analysis [*]
--sygus-repair-const
use approach to repair constants in sygus candidate solutions [*]
--sygus-rr
use sygus to enumerate and verify correctness of rewrite rules via sampling [*]
--sygus-rr-synth
use sygus to enumerate candidate rewrite rules via sampling [*]
--sygus-rr-synth-accel
add dynamic symmetry breaking clauses based on candidate rewrites [*]
--sygus-rr-synth-check
use satisfiability check to verify correctness of candidate rewrites [*]
--sygus-rr-synth-filter-cong
filter candidate rewrites based on congruence [*]
--sygus-rr-synth-filter-match
filter candidate rewrites based on matching [*]
--sygus-rr-synth-filter-order
filter candidate rewrites based on variable ordering [*]
--sygus-rr-verify
use sygus to verify the correctness of rewrite rules via sampling [*]
--sygus-rr-verify-abort
abort when sygus-rr-verify finds an instance of unsoundness [*]
--sygus-sample-grammar
when applicable, use grammar for choosing sample points [*]
--sygus-samples=N
number of points to consider when doing sygus rewriter sample testing
--sygus-stream
enumerate a stream of solutions instead of terminating after the first one [*]
--sygus-templ-embed-grammar
embed sygus templates into grammars [*]
--sygus-unif
Unification-based function synthesis [*]
--term-db-mode
which ground terms to consider for instantiation
--track-inst-lemmas
track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization) [*]
--trigger-active-sel
selection mode to activate triggers
--trigger-sel
selection mode for triggers
--user-pat=MODE
policy for handling user-provided patterns for quantifier instantiation
--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 [*]
SEP OPTIONS
--sep-check-neg
check negated spatial assertions [*]
--sep-child-refine
child-specific refinements of negated star, positive wand [*]
--sep-deq-c
assume cardinality elements are distinct [*]
--sep-exp
experimental flag for sep [*]
--sep-min-refine
only add refinement lemmas for minimal (innermost) assertions [*]
--sep-pre-skolem-emp
eliminate emp constraint at preprocess time [*]
SETS OPTIONS
--sets-ext
enable extended symbols such as complement and universe in theory of sets [*]
--sets-infer-as-lemmas
send inferences as lemmas [*]
--sets-proxy-lemmas
introduce proxy variables eagerly to shorten lemmas [*]
--sets-rel-eager
standard effort checks for relations [*]
SMT LAYER OPTIONS
--abstract-values
in models, output arrays (and in future, maybe others) using abstract values, as required by the
SMT-LIB standard [*]
--bitblast-step
amount of resources spent for each bitblast step (EXPERTS only)
--bv-sat-conflict-step
amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)
--check-models
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions [*]
--check-proofs
after UNSAT/VALID, machine-check the generated proof [*]
--check-synth-sol
checks whether produced solutions to functions-to-synthesize satisfy the conjecture [*]
--check-unsat-cores
after UNSAT/VALID, produce and check an unsat core (expensive) [*]
--cnf-step
amount of resources spent for each call to cnf conversion (EXPERTS only)
--decision-step
amount of getNext decision calls in the decision engine (EXPERTS only)
--dump-instantiations
output instantiations of quantified formulas after every UNSAT/VALID response [*]
--dump-models
output models after every SAT/INVALID/UNKNOWN response [*]
--dump-proofs
output proofs after every UNSAT/VALID response [*]
--dump-synth
output solution for synthesis conjectures after every UNSAT/VALID response [*]
--dump-unsat-cores
output unsat cores after every UNSAT/VALID response [*]
--dump-unsat-cores-full
dump the full unsat core, including unlabeled assertions [*]
--ext-rew-prep
use extended rewriter as a preprocessing pass [*]
--ext-rew-prep-agg
use aggressive extended rewriter as a preprocessing pass [*]
--force-logic=LOGIC
set the logic, and override all further user attempts to change it (EXPERTS only)
--force-no-limit-cpu-while-dump
Force no CPU limit when dumping models and proofs [*]
--ite-simp
turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) [*]
--lemma-step
amount of resources spent when adding lemmas (EXPERTS only)
--model-u-dt-enum
in models, output uninterpreted sorts as datatype enumerations [*]
--omit-dont-cares
When producing a model, omit variables whose value does not matter [*]
--on-repeat-ite-simp
do the ite simplification pass again if repeating simplification [*]
--parse-step
amount of resources spent for each command/expression parsing (EXPERTS only)
--preprocess-step
amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)
--produce-assignments
support the get-assignment command [*]
--produce-unsat-assumptions
turn on unsat assumptions generation [*]
--produce-unsat-cores
turn on unsat core generation [*]
--proof
turn on proof generation [*]
--quantifier-step
amount of resources spent for quantifier instantiations (EXPERTS only)
--repeat-simp
make multiple passes with nonclausal simplifier [*]
--restart-step
amount of resources spent for each theory restart (EXPERTS only)
--rewrite-apply-to-const
eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 (EXPERTS only) [*]
--rewrite-step
amount of resources spent for each rewrite step (EXPERTS only)
--sat-conflict-step
amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)
--simp-ite-compress
enables compressing ites after ite simplification [*]
--simp-ite-hunt-zombies
post ite compression enables zombie removal while the number of nodes is above this threshold
--simp-with-care
enables simplifyWithCare in ite simplificiation [*]
--simplification=MODE
choose simplification mode, see --simplification=help
--sort-inference
calculate sort inference of input problem, convert the input based on monotonic sorts [*]
--static-learning
use static learning (on by default) [*]
--sygus-out=MODE
output mode for sygus
--sygus-print-callbacks
use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)
[*]
--symmetry-breaker-exp
generate symmetry breaking constraints after symmetry detection [*]
--theory-check-step
amount of resources spent for each theory check call (EXPERTS only)
--unconstrained-simp
turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) [*]
--no-simplification
turn off all simplification (same as --simplification=none)
STRINGS THEORY OPTIONS
--strings-abort-loop
abort when a looping word equation is encountered [*]
--strings-binary-csp
use binary search when splitting strings [*]
--strings-check-entail-len
check entailment between length terms to reduce splitting [*]
--strings-eager
strings eager check [*]
--strings-eager-len
strings eager length lemmas [*]
--strings-eit
the eager intersection used by the theory of strings [*]
--strings-exp
experimental features in the theory of strings [*]
--strings-fmf
the finite model finding used by the theory of strings [*]
--strings-guess-model
use model guessing to avoid string extended function reductions [*]
--strings-infer-as-lemmas
always send lemmas out instead of making internal inferences [*]
--strings-infer-sym
strings split on empty string [*]
--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-lb=N
the strategy of LB rule application: 0-lazy, 1-eager, 2-no
--strings-len-geqz
strings length greater than zero lemmas [*]
--strings-len-norm
strings length normalization lemma [*]
--strings-lprop-csp
do length propagation based on constant splits [*]
--strings-min-prefix-explain
minimize explanations for prefix of normal forms in strings [*]
--strings-opt1
internal option1 for strings: normal form [*]
--strings-opt2
internal option2 for strings: constant regexp splitting [*]
--strings-print-ascii
the alphabet contains only printable characters from the standard extended ASCII [*]
--strings-process-loop
reduce looping word equations to regular expressions [*]
--strings-rexplain-lemmas
regression explanations for string lemmas [*]
--strings-sp-emp
strings split on empty string [*]
--strings-uf-reduct
use uninterpreted functions when applying extended function reductions [*]
THEORY LAYER OPTIONS
--assign-function-values
assign values for uninterpreted functions in models [*]
--condense-function-values
condense values for functions in models rather than explicitly representing them [*]
--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) [*]
--uf-ho
enable support for higher-order reasoning [*]
--uf-ho-ext
apply extensionality on function symbols [*]
--uf-ss-abort-card=N
tells the uf strong solver to only consider models that interpret uninterpreted sorts of
cardinality at most N (-1 == no limit, default)
--uf-ss-clique-splits
use cliques instead of splitting on demand to shrink model [*]
--uf-ss-eager-split
add splits eagerly for uf strong solver [*]
--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 [*]
--uf-ss-regions
disable region-based method for discovering cliques and splits in 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=MODE
mode of operation for uf strong solver.
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.6.
BUGS
An issue tracker for the CVC4 project is maintained at https://github.com/CVC4/CVC4/issues.
AUTHORS
CVC4 is developed by a team of researchers at Stanford 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.stanford.edu/wiki/.