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

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

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

The man page pcvc4(1) is an alias of cvc4(1).

August 2017 CVC4 release 1.5 User Manuals