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