cvc4 man page

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” (see cvc4(5) ), 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 [*]
--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 [*]
--interactive
force interactive mode [*]
--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
--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 [*]

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)

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)
--no-type-checking
never type check expressions
--biased-ites
try the new remove ite pass that is biased against term ites appearing [*]

Boolean Theory Options

--boolean-term-conversion-mode=MODE
policy for converting Boolean terms

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)

Bitvector Theory Options

--bitblast=MODE
choose bitblasting mode, see --bitblast=help
--bitblast-aig
bitblast by first converting to AIG (only if --bitblast=eager) [*]
--bv-aig-simp=FILE
abc command to run AIG simplifications (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 [*]
--bv-div-zero-const
always return -1 on division by zero [*]
--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) [*]

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 [*]

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
--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 outputing 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

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 [*]
--disable-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 [*]
--disable-uf-ss-min-model
disable finding a minimal model in 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 [*]

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-model-based
turn on model-based arrray solver [*]
--arrays-eager-index
turn on eager index splitting for generated array lemmas [*]
--arrays-eager-lemmas
turn on eager lemma generation for arrays [*]

Quantifiers Options

--disable-miniscope-quant
disable miniscope quantifiers
--disable-miniscope-quant-fv
disable miniscope quantifiers for ground subformulas
--disable-prenex-quant
disable prenexing of quantified formulas
--disable-var-elim-quant
disable simple variable elimination for quantified formulas
--disable-ite-lift-quant
disable simple ite lifting for quantified formulas
--cnf-quant
apply CNF conversion to quantified formulas [*]
--nnf-quant
apply NNF conversion to quantified formulas [*]
--clause-split
apply clause splitting to quantified formulas [*]
--pre-skolem-quant
apply skolemization eagerly to bodies of quantified formulas [*]
--ag-miniscope-quant
perform aggressive miniscoping for quantifiers [*]
--macros-quant
perform quantifiers macro expansions [*]
--fo-prop-quant
perform first-order propagation on quantifiers [*]
--disable-smart-triggers
disable smart 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) [*]
--register-quant-body-terms
consider ground terms within bodies of quantified formulas for matching [*]
--inst-when=MODE
when to apply instantiation
--inst-max-level=N
maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
--eager-inst-quant
apply quantifier instantiation eagerly [*]
--full-saturate-quant
when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown [*]
--literal-matching=MODE
choose literal matching mode
--enable-cbqi
turns on counterexample-based quantifier instantiation [*]
--cbqi-recurse
turns on recursive counterexample-based quantifier instantiation [*]
--user-pat=MODE
policy for handling user-provided patterns for quantifier instantiation
--flip-decision
turns on flip decision heuristic
--disable-quant-internal-reps
disables instantiating with representatives chosen by quantifiers engine
--finite-model-find
use finite model finding heuristic for quantifier instantiation [*]
--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 [*]
--disable-fmf-inst-gen
disable 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 [*]
--disable-fmf-fmc-simple
disable simple models in full model check for finite model finding
--fmf-bound-int
finite model finding on bounded integer quantification [*]
--fmf-bound-int-lazy
enforce bounds for bounded integer quantification lazily via use of proxy variables [*]
--axiom-inst=MODE
policy for instantiating axioms
--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 [*]
--rewrite-rules
use rewrite rules module [*]
--rr-one-inst-per-round
add one instance of rewrite rule per round [*]
--dt-stc-ind
apply strengthening for existential quantification over datatypes based on structural induction [*]

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-fmf
the finite model finding used by the theory of strings [*]
--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-alphabet-card=N
the cardinality of the characters used by the theory of strings, default 256 (EXPERTS only)

Sat Layer Options

--show-sat-solvers
show all available SAT solvers
--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 [*]

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

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 [*]
--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 [*]
--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-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 [*]

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)

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) [*]
--continued-execution
continue executing commands, even on error
--segv-spin
spin on segfault/other crash waiting for gdb [*]
--tear-down-incremental
implement PUSH/POP/multi-query by destroying and recreating SmtEngine (EXPERTS only) [*]
--wait-to-join
wait for other threads to join before quitting (EXPERTS only) [*]

Parser Options

--mmap
memory map file input [*]
--no-checking
disable ALL semantic checks, including type checks

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)

Sets Options

--sets-propagate
determines whether to propagate learnt facts to Theory Engine / SAT solver [*]
--sets-eager-lemmas
add lemmas even at regular effort [*]

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.4.

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

libcvc4(3), libcvc4parser(3), libcvc4compat(3)

Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4. It is maintained at http://cvc4.cs.nyu.edu/wiki/.

Referenced By

cvc4(5), libcvc4(3), libcvc4compat(3), libcvc4parser(3).

pcvc4(1) is an alias of cvc4(1).

July 2014 CVC4 release 1.4 User Manuals