SmtEngine.3cvc man page

SmtEngine — the primary interface to CVC4's theorem-proving capabilities

Description

SmtEngine is the main entry point into the CVC4 theorem prover API.

Smtengine Options

The SmtEngine is in charge of setting and getting information and options. Numerous options are available via the SmtEngine::setOption() call. SmtEngine::setOption() and SmtEngine::getOption() use the following option keys.

COMMON OPTIONS
input-language
(InputLanguage) force input language (default is "auto"; see --lang help)
output-language
(OutputLanguage) force output language (default is "auto"; see --output-lang help)
statistics
(bool) give statistics on exit
dump
(void) dump preprocessed assertions, etc., see --dump=help
dump-to
(void) all dumping goes to FILE (instead of stdout)
produce-models
(bool) support the get-value and get-model commands
interactive-mode
(bool) force interactive mode
incremental
(bool) enable incremental solving
tlimit
(unsigned long) enable time limiting (give milliseconds)
tlimit-per
(unsigned long) enable time limiting per query (give milliseconds)
rlimit
(unsigned long) enable resource limiting (currently, roughly the number of SAT conflicts)
rlimit-per
(unsigned long) enable resource limiting per query
version
(bool) identify this CVC4 binary
help
(bool) full command line reference
strict-parsing
(bool) be less tolerant of non-conforming inputs
BASE OPTIONS
verbosity
(int) the verbosity level of CVC4
stats-every-query
(bool) in incremental mode, print stats after every satisfiability or validity query
stats-hide-zeros
(bool) hide statistics which are zero
parse-only
(bool) exit after parsing input
preprocess-only
(bool) exit after preprocessing input
trace
(void) trace something (e.g. -t pushpop), can repeat
debug
(void) debug something (e.g. -d arith), can repeat
print-success
(bool) print the "success" output required of SMT-LIBv2
EXPRESSION PACKAGE OPTIONS
default-expr-depth=N
(int) print exprs to depth N (0 == default, -1 == no limit)
default-dag-thresh
(int) dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
eager-type-checking
(bool) type check expressions immediately on creation (debug builds only)
biased-ites
(bool) try the new remove ite pass that is biased against term ites appearing
BOOLEAN THEORY OPTIONS
boolean-term-conversion-mode
(CVC4::theory::booleans::BooleanTermConversionMode) policy for converting Boolean terms
THEORY LAYER OPTIONS
theoryof-mode
(CVC4::theory::TheoryOfMode) mode for Theory::theoryof() (EXPERTS only)
use-theory
(void) use alternate theory implementation NAME (--use-theory=help for a list)
BITVECTOR THEORY OPTIONS
bitblast
(CVC4::theory::bv::BitblastMode) choose bitblasting mode, see --bitblast=help
bitblast-aig
(bool) bitblast by first converting to AIG (only if --bitblast=eager)
bv-aig-simp=FILE
(std::string) abc command to run AIG simplifications (EXPERTS only)
bv-propagate
(bool) use bit-vector propagation in the bit-blaster
bv-eq-solver
(bool) use the equality engine for the bit-vector theory (only if --bitblast=lazy)
bv-eq-slicer=MODE
(CVC4::theory::bv::BvSlicerMode) turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)
bv-inequality-solver
(bool) turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)
bv-algebraic-solver
(bool) turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy)
bv-algebraic-budget
(unsigned) the budget allowed for the algebraic solver in number of SAT conflicts (EXPERTS only)
bv-to-bool
(bool) lift bit-vectors of size 1 to booleans when possible
bv-div-zero-const
(bool) always return -1 on division by zero
bv-abstraction
(bool) mcm benchmark abstraction (EXPERTS only)
bv-skolemize
(bool) skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) (EXPERTS only)
bv-num-func=NUM
(unsigned) number of function symbols in conflicts that are generalized (EXPERTS only)
bv-eager-explanations
(bool) compute bit-blasting propagation explanations eagerly (EXPERTS only)
bv-quick-xplain
(bool) minimize bv conflicts using the QuickXplain algorithm (EXPERTS only)
bv-intro-pow2
(bool) introduce bitvector powers of two as a preprocessing pass (EXPERTS only)
DATATYPES THEORY OPTIONS
dt-rewrite-error-sel
(bool) rewrite incorrectly applied selectors to arbitrary ground term (EXPERTS only)
dt-force-assignment
(bool) force the datatypes solver to give specific values to all datatypes terms before answering sat
ARITHMETIC THEORY OPTIONS
unate-lemmas=MODE
(ArithUnateLemmaMode) determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)
arith-prop=MODE
(ArithPropagationMode) turns on arithmetic propagation (default is 'old', see --arith-prop=help)
heuristic-pivots=N
(int16_t) 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
(int16_t) 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
(ErrorSelectionRule) change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)
simplex-check-period=N
(uint16_t) the number of pivots to do in simplex before rechecking for a conflict on all variables
pivot-threshold=N
(uint16_t) sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order
prop-row-length=N
(uint16_t) sets the maximum row length to be used in propagation
enable-arith-rewrite-equalities
(bool) turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
miplib-trick
(bool) turns on the preprocessing step of attempting to infer bounds on miplib problems
miplib-trick-subs
(unsigned) do substitution for miplib 'tmp' vars if defined in <= N eliminated vars
cut-all-bounded
(bool) turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
maxCutsInContext
(unsigned) maximum cuts in a given context before signalling a restart
revert-arith-models-on-unsat
(bool) revert the arithmetic model to a known safe model on unsat if one is cached
fc-penalties
(bool) turns on degenerate pivot penalties
use-fcsimplex
(bool) use focusing and converging simplex (FMCAD 2013 submission)
use-soi
(bool) use sum of infeasibility simplex (FMCAD 2013 submission)
restrict-pivots
(bool) have a pivot cap for simplex at effort levels below fullEffort
collect-pivot-stats
(bool) collect the pivot history
use-approx
(bool) attempt to use an approximate solver
approx-branch-depth
(int16_t) maximum branch depth the approximate solver is allowed to take
dio-decomps
(bool) let skolem variables for integer divisibility constraints leak from the dio solver
new-prop
(bool) use the new row propagation system
arith-prop-clauses
(uint16_t) rows shorter than this are propagated as clauses
soi-qe
(bool) use quick explain to minimize the sum of infeasibility conflicts
rewrite-divk
(bool) rewrite division and mod when by a constant into linear terms
se-solve-int
(bool) attempt to use the approximate solve integer method on standard effort
lemmas-on-replay-failure
(bool) attempt to use external lemmas if approximate solve integer failed
dio-turns
(int) turns in a row dio solver cutting gets
rr-turns
(int) round robin turn
dio-repeat
(bool) handle dio solver constraints in mass or one at a time
replay-early-close-depth
(int) multiples of the depths to try to close the approx log eagerly
replay-failure-penalty
(int) number of solve integer attempts to skips after a numeric failure
replay-num-err-penalty
(int) number of solve integer attempts to skips after a numeric failure
replay-reject-cut
(unsigned) maximum complexity of any coefficient while replaying cuts
replay-lemma-reject-cut
(unsigned) maximum complexity of any coefficient while outputing replaying cut lemmas
replay-soi-major-threshold
(double) threshold for a major tolerance failure by the approximate solver
replay-soi-major-threshold-pen
(int) threshold for a major tolerance failure by the approximate solver
replay-soi-minor-threshold
(double) threshold for a minor tolerance failure by the approximate solver
replay-soi-minor-threshold-pen
(int) threshold for a minor tolerance failure by the approximate solver
pp-assert-max-sub-size
(unsigned) threshold for substituting an equality in ppAssert
max-replay-tree
(int) threshold for attempting to replay a tree
pb-rewrites
(bool) apply pseudo boolean rewrites
pb-rewrite-threshold
(int) threshold of number of pseudoboolean variables to have before doing rewrites
UNINTERPRETED FUNCTIONS THEORY OPTIONS
uf-symmetry-breaker
(bool) use UF symmetry breaker (Deharbe et al., CADE 2011)
condense-function-values
(bool) condense models for functions rather than explicitly representing them
uf-ss-eager-split
(bool) add splits eagerly for uf strong solver
uf-ss-totality
(bool) always use totality axioms for enforcing cardinality constraints
uf-ss-totality-limited=N
(int) apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
uf-ss-totality-sym-break
(bool) apply symmetry breaking for totality axioms
uf-ss-abort-card=N
(int) tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
uf-ss-explained-cliques
(bool) use explained clique lemmas for uf strong solver
uf-ss-simple-cliques
(bool) always use simple clique lemmas for uf strong solver
uf-ss-deq-prop
(bool) eagerly propagate disequalities for uf strong solver
uf-ss-clique-splits
(bool) use cliques instead of splitting on demand to shrink model
uf-ss-sym-break
(bool) finite model finding symmetry breaking techniques
uf-ss-fair
(bool) use fair strategy for finite model finding multiple sorts
ARRAYS THEORY OPTIONS
arrays-optimize-linear
(bool) turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)
arrays-lazy-rintro1
(bool) turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)
arrays-model-based
(bool) turn on model-based arrray solver
arrays-eager-index
(bool) turn on eager index splitting for generated array lemmas
arrays-eager-lemmas
(bool) turn on eager lemma generation for arrays
QUANTIFIERS OPTIONS
cnf-quant
(bool) apply CNF conversion to quantified formulas
nnf-quant
(bool) apply NNF conversion to quantified formulas
clause-split
(bool) apply clause splitting to quantified formulas
pre-skolem-quant
(bool) apply skolemization eagerly to bodies of quantified formulas
ag-miniscope-quant
(bool) perform aggressive miniscoping for quantifiers
macros-quant
(bool) perform quantifiers macro expansions
fo-prop-quant
(bool) perform first-order propagation on quantifiers
relevant-triggers
(bool) prefer triggers that are more relevant based on SInE style analysis
relational-triggers
(bool) choose relational triggers such as x = f(y), x >= f(y)
register-quant-body-terms
(bool) consider ground terms within bodies of quantified formulas for matching
inst-when=MODE
(CVC4::theory::quantifiers::InstWhenMode) when to apply instantiation
inst-max-level=N
(int) maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
eager-inst-quant
(bool) apply quantifier instantiation eagerly
full-saturate-quant
(bool) when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
literal-matching=MODE
(CVC4::theory::quantifiers::LiteralMatchMode) choose literal matching mode
enable-cbqi
(bool) turns on counterexample-based quantifier instantiation
cbqi-recurse
(bool) turns on recursive counterexample-based quantifier instantiation
user-pat=MODE
(CVC4::theory::quantifiers::UserPatMode) policy for handling user-provided patterns for quantifier instantiation
flip-decision
(bool) turns on flip decision heuristic
finite-model-find
(bool) use finite model finding heuristic for quantifier instantiation
mbqi=MODE
(CVC4::theory::quantifiers::MbqiMode) choose mode for model-based quantifier instantiation
mbqi-one-inst-per-round
(bool) only add one instantiation per quantifier per round for mbqi
mbqi-one-quant-per-round
(bool) only add instantiations for one quantifier per round for mbqi
fmf-inst-engine
(bool) use instantiation engine in conjunction with finite model finding
fmf-inst-gen-one-quant-per-round
(bool) only perform Inst-Gen instantiation techniques on one quantifier per round
fmf-fresh-dc
(bool) use fresh distinguished representative when applying Inst-Gen techniques
fmf-bound-int
(bool) finite model finding on bounded integer quantification
fmf-bound-int-lazy
(bool) enforce bounds for bounded integer quantification lazily via use of proxy variables
axiom-inst=MODE
(CVC4::theory::quantifiers::AxiomInstMode) policy for instantiating axioms
quant-cf
(bool) enable conflict find mechanism for quantifiers
quant-cf-mode=MODE
(CVC4::theory::quantifiers::QcfMode) what effort to apply conflict find mechanism
quant-cf-when=MODE
(CVC4::theory::quantifiers::QcfWhenMode) when to invoke conflict find mechanism for quantifiers
qcf-tconstraint
(bool) enable entailment checks for t-constraints in qcf algorithm
rewrite-rules
(bool) use rewrite rules module
rr-one-inst-per-round
(bool) add one instance of rewrite rule per round
dt-stc-ind
(bool) apply strengthening for existential quantification over datatypes based on structural induction
STRINGS THEORY OPTIONS
strings-exp
(bool) experimental features in the theory of strings
strings-lb
(unsigned) the strategy of LB rule application: 0-lazy, 1-eager, 2-no
strings-fmf
(bool) the finite model finding used by the theory of strings
strings-eit
(bool) the eager intersection used by the theory of strings
strings-opt1
(bool) internal option1 for strings: normal form
strings-opt2
(bool) internal option2 for strings: constant regexp splitting
strings-alphabet-card
(int16_t) the cardinality of the characters used by the theory of strings, default 256 (EXPERTS only)
SAT LAYER OPTIONS
random-frequency
(double) sets the frequency of random decisions in the sat solver (P=0.0 by default)
random-seed
(uint32_t) sets the random seed for the sat solver
restart-int-base=N
(unsigned) sets the base restart interval for the sat solver (N=25 by default)
restart-int-inc=F
(double) sets the restart interval increase factor for the sat solver (F=3.0 by default)
refine-conflicts
(bool) refine theory conflict clauses (default false)
minisat-elimination
(bool) use Minisat elimination
minisat-dump-dimacs
(bool) instead of solving minisat dumps the asserted clauses in Dimacs format
PRINTING OPTIONS
model-format=MODE
(ModelFormatMode) print format mode for models, see --model-format=help
inst-format=MODE
(InstFormatMode) print format mode for instantiations, see --inst-format=help
SMT LAYER OPTIONS
force-logic
(LogicInfo) set the logic, and override all further user attempts to change it (EXPERTS only)
simplification-mode
(SimplificationMode) choose simplification mode, see --simplification=help
static-learning
(bool) use static learning (on by default)
expand-definitions
(bool) always expand symbol definitions in output
check-models
(bool) after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
dump-models
(bool) output models after every SAT/INVALID/UNKNOWN response
produce-proofs
(bool) turn on proof generation
check-proofs
(bool) after UNSAT/VALID, machine-check the generated proof
dump-proofs
(bool) output proofs after every UNSAT/VALID response
dump-instantiations
(bool) output instantiations of quantified formulas after every UNSAT/VALID response
produce-assignments
(bool) support the get-assignment command
ite-simp
(bool) turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
on-repeat-ite-simp
(bool) do the ite simplification pass again if repeating simplification
simp-with-care
(bool) enables simplifyWithCare in ite simplificiation
simp-ite-compress
(bool) enables compressing ites after ite simplification
unconstrained-simp
(bool) turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
repeat-simp
(bool) make multiple passes with nonclausal simplifier
simp-ite-hunt-zombies
(uint32_t) post ite compression enables zombie removal while the number of nodes is above this threshold
sort-inference
(bool) calculate sort inference of input problem, convert the input based on monotonic sorts
abstract-values
(bool) in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
model-u-dt-enum
(bool) in models, output uninterpreted sorts as datatype enumerations
regular-output-channel
(void) set the regular output channel of the solver
diagnostic-output-channel
(void) set the diagnostic output channel of the solver
rewrite-apply-to-const
(bool) eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 (EXPERTS only)
force-no-limit-cpu-while-dump
(bool) Force no CPU limit when dumping models and proofs
DECISION HEURISTICS OPTIONS
decision-mode
(decision::DecisionMode) choose decision mode, see --decision=help
decision-threshold=N
(decision::DecisionWeight) ignore all nodes greater than threshold in first attempt to pick decision (EXPERTS only)
decision-use-weight
(bool) use the weight nodes (locally, by looking at children) to direct recursive search (EXPERTS only)
decision-random-weight=N
(int) assign random weights to nodes between 0 and N-1 (0: disable) (EXPERTS only)
decision-weight-internal=HOW
(decision::DecisionWeightInternal) computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) (EXPERTS only)
DRIVER OPTIONS
early-exit
(bool) do not run destructors at exit; default on except in debug builds (EXPERTS only)
threads=N
(unsigned) Total number of threads for portfolio
thread-stack=N
(unsigned) stack size for worker threads in MB (0 means use Boost/thread lib default)
filter-lemma-length=N
(int) don't share (among portfolio threads) lemmas strictly longer than N
fallback-sequential
(bool) Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode
incremental-parallel
(bool) Use parallel solver even in incremental mode (may print 'unknown's at times)
continued-execution
(bool) continue executing commands, even on error
segv-spin
(bool) spin on segfault/other crash waiting for gdb
tear-down-incremental
(bool) implement PUSH/POP/multi-query by destroying and recreating SmtEngine (EXPERTS only)
wait-to-join
(bool) wait for other threads to join before quitting (EXPERTS only)
PARSER OPTIONS
mmap
(bool) memory map file input
IDL OPTIONS
enable-idl-rewrite-equalities
(bool) enable rewriting equalities into two inequalities in IDL solver (default is disabled)
SETS OPTIONS
sets-propagate
(bool) determines whether to propagate learnt facts to Theory Engine / SAT solver
sets-eager-lemmas
(bool) add lemmas even at regular effort

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

Info

July 2014 CVC4 release 1.4 CVC4 Library Interfaces