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