# 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

**version**(bool) identify this CVC4 binary

**help**(bool) full command line reference

**strict-parsing**(bool) be less tolerant of non-conforming inputs

**dump**(std::string) dump preprocessed assertions, etc., see --dump=help

**dump-to**(std::string) all dumping goes to FILE (instead of stdout)

**produce-models**(bool) support the get-value and get-model commands

**produce-assertions**(bool) keep an assertions list (enables get-assertions command)

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

**reproducible-resource-limit**(unsigned long) enable resource limiting per query

**hard-limit**(bool) the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)

**cpu-time**(bool) measures CPU time if set to true and wall time if false (default false)

*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-dio-solver**(bool) turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)

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

**snorm-infer-eq**(bool) infer equalities based on Shostak normalization

**nl-ext**(bool) extended approach to non-linear

**nl-ext-rbound**(bool) use resolution-style inference for inferring new bounds

**nl-ext-tplanes**(bool) use non-terminating tangent plane strategy for non-linear

**nl-ext-ent-conf**(bool) check for entailed conflicts in non-linear solver

**nl-ext-rewrite**(bool) do rewrites in non-linear solver

**nl-ext-solve-subs**(bool) do solving for determining constant substitutions

**nl-ext-purify**(bool) purify non-linear terms at preprocess

**nl-ext-split-zero**(bool) intial splits on zero for all variables

*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-weak-equiv**(bool) use algorithm from Christ/Hoenicke (SMT 2014)

**arrays-model-based**(bool) turn on model-based array 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

**arrays-config**(int) set different array option configurations - for developers only

**arrays-reduce-sharing**(bool) use model information to reduce size of care graph for arrays

**arrays-prop**(int) propagation effort for arrays: 0 is none, 1 is some, 2 is full

*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

*BITVECTOR THEORY OPTIONS***bv-sat-solver**(CVC4::theory::bv::SatSolverMode) choose which sat solver to use, see --bv-sat-solver=help (EXPERTS only)

**bitblast**(CVC4::theory::bv::BitblastMode) choose bitblasting mode, see --bitblast=help

**bitblast-aig**(bool) bitblast by first converting to AIG (implies --bitblast=eager)

- bv-aig-simp=
**COMMAND** (std::string) abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") (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

**bool-to-bv**(bool) convert booleans to bit-vectors of size 1 when possible

**bv-div-zero-const**(bool) always return -1 on division by zero

**bv-extract-arith**(bool) enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) (EXPERTS only)

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

**bv-lazy-rewrite-extf**(bool) lazily rewrite extended functions like bv2nat and int2bv

**bv-lazy-reduce-extf**(bool) reduce extended functions like bv2nat and int2bv at last call instead of full effort

**bv-alg-extf**(bool) algebraic inferences for extended functions

*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

**dt-binary-split**(bool) do binary splits for datatype constructor types

**dt-ref-sk-intro**(bool) introduce reference skolems for shorter explanations

**dt-use-testers**(bool) do not preprocess away tester predicates

**cdt-bisimilar**(bool) do bisimilarity check for co-datatypes

**dt-cyclic**(bool) do cyclicity check for datatypes

**dt-infer-as-lemmas**(bool) always send lemmas out instead of making internal inferences

**dt-blast-splits**(bool) when applicable, blast splitting lemmas for all variables at once

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

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

**print-expr-types**(bool) print types with variables when printing exprs

**eager-type-checking**(bool) type check expressions immediately on creation (debug builds only)

**type-checking**(bool) never type check expressions

*IDL OPTIONS***enable-idl-rewrite-equalities**(bool) enable rewriting equalities into two inequalities in IDL solver (default is disabled)

*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

**wait-to-join**(bool) wait for other threads to join before quitting (EXPERTS only)

*PARSER OPTIONS***mmap**(bool) memory map file input

**semantic-checks**(bool) disable ALL semantic checks, including type checks

**global-declarations**(bool) force all declarations and definitions to be global

*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

*PROOF OPTIONS***lfsc-letification**(bool) turns on global letification in LFSC proofs

**aggressive-core-min**(bool) turns on aggressive unsat core minimization (experimental)

**fewer-preprocessing-holes**(bool) try to eliminate preprocessing holes in proofs

**allow-empty-dependencies**(bool) if unable to track the dependencies of a rewritten/preprocessed assertion, fail silently

*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

*QUANTIFIERS OPTIONS***miniscope-quant**(bool) miniscope quantifiers

**miniscope-quant-fv**(bool) miniscope quantifiers for ground subformulas

**quant-split**(bool) apply splitting to quantified formulas based on variable disjoint disjuncts

- prenex-quant=
**MODE** (CVC4::theory::quantifiers::PrenexQuantMode) prenex mode for quantified formulas

**prenex-quant-user**(bool) prenex quantified formulas with user patterns

**var-elim-quant**(bool) enable simple variable elimination for quantified formulas

**var-ineq-elim-quant**(bool) enable variable elimination based on infinite projection of unbound arithmetic variables

**dt-var-exp-quant**(bool) expand datatype variables bound to one constructor in quantifiers

- ite-lift-quant=
**MODE** (CVC4::theory::quantifiers::IteLiftQuantMode) ite lifting mode for quantified formulas

**cond-var-split-quant**(bool) split quantified formulas that lead to variable eliminations

**cond-var-split-agg-quant**(bool) aggressive split quantified formulas that lead to variable eliminations

**ite-dtt-split-quant**(bool) split ites with dt testers as conditions

**pre-skolem-quant**(bool) apply skolemization eagerly to bodies of quantified formulas

**pre-skolem-quant-nested**(bool) apply skolemization to nested quantified formulas

**pre-skolem-quant-agg**(bool) apply skolemization to quantified formulas aggressively

**ag-miniscope-quant**(bool) perform aggressive miniscoping for quantifiers

**elim-taut-quant**(bool) eliminate tautological disjuncts of quantified formulas

**elim-ext-arith-quant**(bool) eliminate extended arithmetic symbols in quantified formulas

**cond-rewrite-quant**(bool) conditional rewriting of quantified formulas

**e-matching**(bool) whether to do heuristic E-matching

**term-db-mode**(CVC4::theory::quantifiers::TermDbMode) which ground terms to consider for instantiation

**register-quant-body-terms**(bool) consider ground terms within bodies of quantified formulas for matching

**infer-arith-trigger-eq**(bool) infer equalities for trigger terms based on solving arithmetic equalities

**infer-arith-trigger-eq-exp**(bool) record explanations for inferArithTriggerEq

**strict-triggers**(bool) only instantiate quantifiers with user patterns based on triggers

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

**purify-triggers**(bool) purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1

**purify-dt-triggers**(bool) purify dt triggers, match all constructors of correct form instead of selectors

**pure-th-triggers**(bool) use pure theory terms as single triggers

**partial-triggers**(bool) use triggers that do not contain all free variables

**multi-trigger-when-single**(bool) select multi triggers when single triggers exist

**multi-trigger-priority**(bool) only try multi triggers if single triggers give no instantiations

**multi-trigger-cache**(bool) caching version of multi triggers

**multi-trigger-linear**(bool) implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms

**trigger-sel**(CVC4::theory::quantifiers::TriggerSelMode) selection mode for triggers

**trigger-active-sel**(CVC4::theory::quantifiers::TriggerActiveSelMode) selection mode to activate triggers

- user-pat=
**MODE** (CVC4::theory::quantifiers::UserPatMode) policy for handling user-provided patterns for quantifier instantiation

**increment-triggers**(bool) generate additional triggers as needed during search

- inst-when=
**MODE** (CVC4::theory::quantifiers::InstWhenMode) when to apply instantiation

**inst-when-strict-interleave**(bool) ensure theory combination and standard quantifier effort strategies take turns

- inst-when-phase=
**N** (int) instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen

**inst-when-tc-first**(bool) allow theory combination to happen once initially, before quantifier strategies are run

**quant-model-ee**(bool) use equality engine of model for last call effort

- inst-max-level=
**N** (int) maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)

**inst-level-input-only**(bool) only input terms are assigned instantiation level zero

- quant-rep-mode=
**MODE** (CVC4::theory::quantifiers::QuantRepMode) selection mode for representatives in quantifiers engine

**inst-rlv-cond**(bool) add relevancy conditions for instantiations

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

**full-saturate-quant-rd**(bool) whether to use relevant domain first for full saturation instantiation strategy

**fs-inst**(bool) interleave full saturate instantiation with other techniques

- literal-matching=
**MODE** (CVC4::theory::quantifiers::LiteralMatchMode) choose literal matching mode

**finite-model-find**(bool) use finite model finding heuristic for quantifier instantiation

**quant-fun-wd**(bool) assume that function defined by quantifiers are well defined

**fmf-fun**(bool) find models for recursively defined functions, assumes functions are admissible

**fmf-fun-rlv**(bool) find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant

**fmf-empty-sorts**(bool) allow finite model finding to assume sorts that do not occur in ground assertions are empty

- 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**(bool) enable Inst-Gen instantiation techniques for 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-fmc-simple**(bool) simple models in full model check for finite model finding

**fmf-bound-int**(bool) finite model finding on bounded integer quantification

**fmf-bound**(bool) finite model finding on bounded quantification

**fmf-bound-lazy**(bool) enforce bounds for bounded quantification lazily via use of proxy variables

- fmf-bound-min-mode=
**MODE** (CVC4::theory::quantifiers::FmfBoundMinMode) mode for which types of bounds to minimize via first decision heuristics

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

**qcf-all-conflict**(bool) add all available conflicting instances during conflict-based instantiation

**qcf-nested-conflict**(bool) consider conflicts for nested quantifiers

**qcf-vo-exp**(bool) qcf experimental variable ordering

**inst-no-entail**(bool) do not consider instances of quantified formulas that are currently entailed

**inst-no-model-true**(bool) do not consider instances of quantified formulas that are currently true in model, if it is available

**inst-prop**(bool) internal propagation for instantiations for selecting relevant instances

**qcf-eager-test**(bool) optimization, test qcf instances eagerly

**qcf-eager-check-rd**(bool) optimization, eagerly check relevant domain of matched position

**qcf-skip-rd**(bool) optimization, skip instances based on possibly irrelevant portions of quantified formulas

**rewrite-rules**(bool) use rewrite rules module

**rr-one-inst-per-round**(bool) add one instance of rewrite rule per round

**quant-ind**(bool) use all available techniques for inductive reasoning

**dt-stc-ind**(bool) apply strengthening for existential quantification over datatypes based on structural induction

**int-wf-ind**(bool) apply strengthening for integers based on well-founded induction

**conjecture-gen**(bool) generate candidate conjectures for inductive proofs

- conjecture-gen-per-round=
**N** (int) number of conjectures to generate per instantiation round

**conjecture-no-filter**(bool) do not filter conjectures

**conjecture-filter-active-terms**(bool) filter based on active terms

**conjecture-filter-canonical**(bool) filter based on canonicity

**conjecture-filter-model**(bool) filter based on model

- conjecture-gen-gt-enum=
**N** (int) number of ground terms to generate for model filtering

**conjecture-gen-uee-intro**(bool) more aggressive merging for universal equality engine, introduces terms

- conjecture-gen-max-depth=
**N** (int) maximum depth of terms to consider for conjectures

**cegqi**(bool) counterexample-guided quantifier instantiation

- cegqi-fair=
**MODE** (CVC4::theory::quantifiers::CegqiFairMode) if and how to apply fairness for cegqi

- cegqi-si=
**MODE** (CVC4::theory::quantifiers::CegqiSingleInvMode) mode for processing single invocation synthesis conjectures

**cegqi-si-partial**(bool) combined techniques for synthesis conjectures that are partially single invocation

**cegqi-si-reconstruct**(bool) reconstruct solutions for single invocation conjectures in original grammar

**cegqi-si-sol-min-core**(bool) minimize solutions for single invocation conjectures based on unsat core

**cegqi-si-sol-min-inst**(bool) minimize individual instantiations for single invocation conjectures based on unsat core

**cegqi-si-reconstruct-const**(bool) include constants when reconstruct solutions for single invocation conjectures in original grammar

**cegqi-si-abort**(bool) abort if synthesis conjecture is not single invocation

**sygus-nf**(bool) only search for sygus builtin terms that are in normal form

**sygus-nf-arg**(bool) account for relationship between arguments of operations in sygus normal form

**sygus-nf-sym**(bool) narrow sygus search space based on global state of current candidate program

**sygus-nf-sym-gen**(bool) generalize lemmas for global search space narrowing

**sygus-nf-sym-arg**(bool) generalize based on arguments in global search space narrowing

**sygus-nf-sym-content**(bool) generalize based on content in global search space narrowing

- sygus-inv-templ=
**MODE** (CVC4::theory::quantifiers::SygusInvTemplMode) template mode for sygus invariant synthesis

**sygus-unif-csol**(bool) enable approach which unifies conditional solutions

**sygus-direct-eval**(bool) direct unfolding of evaluation functions

**sygus-cref-eval**(bool) direct evaluation of refinement lemmas for conflict analysis

**cbqi**(bool) turns on counterexample-based quantifier instantiation

**cbqi-recurse**(bool) turns on recursive counterexample-based quantifier instantiation

**cbqi-sat**(bool) answer sat when quantifiers are asserted with counterexample-based quantifier instantiation

**cbqi-model**(bool) guide instantiations by model values for counterexample-based quantifier instantiation

**cbqi-all**(bool) apply counterexample-based instantiation to all quantified formulas

**cbqi-use-inf-int**(bool) use integer infinity for vts in counterexample-based quantifier instantiation

**cbqi-use-inf-real**(bool) use real infinity for vts in counterexample-based quantifier instantiation

**cbqi-prereg-inst**(bool) preregister ground instantiations in counterexample-based quantifier instantiation

**cbqi-min-bounds**(bool) use minimally constrained lower/upper bound for counterexample-based quantifier instantiation

**cbqi-round-up-lia**(bool) round up integer lower bounds in substitutions for counterexample-based quantifier instantiation

**cbqi-midpoint**(bool) choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation

**cbqi-nopt**(bool) non-optimal bounds for counterexample-based quantifier instantiation

**cbqi-lit-dep**(bool) dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation

**cbqi-innermost**(bool) only process innermost quantified formulas in counterexample-based quantifier instantiation

**cbqi-nested-qe**(bool) process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation

**quant-epr**(bool) infer whether in effectively propositional fragment, use for cbqi

**quant-epr-match**(bool) use matching heuristics for EPR instantiation

**local-t-ext**(bool) do instantiation based on local theory extensions

**lte-partial-inst**(bool) partially instantiate local theory quantifiers

**lte-restrict-inst-closure**(bool) treat arguments of inst closure as restricted terms for instantiation

**quant-alpha-equiv**(bool) infer alpha equivalence between quantified formulas

**macros-quant**(bool) perform quantifiers macro expansion

- macros-quant-mode=
**MODE** (CVC4::theory::quantifiers::MacrosQuantMode) mode for quantifiers macro expansion

- quant-dsplit-mode=
**MODE** (CVC4::theory::quantifiers::QuantDSplitMode) mode for dynamic quantifiers splitting

**quant-anti-skolem**(bool) perform anti-skolemization for quantified formulas

**quant-ee**(bool) maintain congrunce closure over universal equalities

**track-inst-lemmas**(bool) track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)

*SEP OPTIONS***sep-check-neg**(bool) check negated spatial assertions

**sep-exp**(bool) experimental flag for sep

**sep-min-refine**(bool) only add refinement lemmas for minimal (innermost) assertions

**sep-deq-c**(bool) assume cardinality elements are distinct

**sep-pre-skolem-emp**(bool) eliminate emp constraint at preprocess time

**sep-child-refine**(bool) child-specific refinements of negated star, positive wand

*SETS OPTIONS***sets-proxy-lemmas**(bool) introduce proxy variables eagerly to shorten lemmas

**sets-infer-as-lemmas**(bool) send inferences as lemmas

**sets-rel-eager**(bool) standard effort checks for relations

**sets-ext**(bool) enable extended symbols such as complement and universe in theory of sets

*SMT LAYER OPTIONS***force-logic**(std::string) 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

**omit-dont-cares**(bool) When producing a model, omit variables whose value does not matter

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

**dump-synth**(bool) output solution for synthesis conjectures after every UNSAT/VALID response

**produce-unsat-cores**(bool) turn on unsat core generation

**check-unsat-cores**(bool) after UNSAT/VALID, produce and check an unsat core (expensive)

**dump-unsat-cores**(bool) output unsat cores after every UNSAT/VALID response

**dump-unsat-cores-full**(bool) dump the full unsat core, including unlabeled assertions

**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**(std::string) set the regular output channel of the solver

**diagnostic-output-channel**(std::string) set the diagnostic output channel of the solver

**rewrite-step**(unsigned) amount of resources spent for each rewrite step (EXPERTS only)

**theory-check-step**(unsigned) amount of resources spent for each theory check call (EXPERTS only)

**decision-step**(unsigned) amount of getNext decision calls in the decision engine (EXPERTS only)

**bitblast-step**(unsigned) amount of resources spent for each bitblast step (EXPERTS only)

**parse-step**(unsigned) amount of resources spent for each command/expression parsing (EXPERTS only)

**lemma-step**(unsigned) amount of resources spent when adding lemmas (EXPERTS only)

**restart-step**(unsigned) amount of resources spent for each theory restart (EXPERTS only)

**cnf-step**(unsigned) amount of resources spent for each call to cnf conversion (EXPERTS only)

**preprocess-step**(unsigned) amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)

**quantifier-step**(unsigned) amount of resources spent for quantifier instantiations (EXPERTS only)

**sat-conflict-step**(unsigned) amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)

**bv-sat-conflict-step**(unsigned) amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)

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

*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-std-ascii**(bool) the alphabet contains only characters from the standard ASCII or the extended one

**strings-fmf**(bool) the finite model finding used by the theory of strings

**strings-eager**(bool) strings eager check

**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-inm**(bool) internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)

**strings-lazy-pp**(bool) perform string preprocessing lazily

**strings-len-geqz**(bool) strings length greater than zero lemmas

**strings-len-norm**(bool) strings length normalization lemma

**strings-sp-emp**(bool) strings split on empty string

**strings-infer-sym**(bool) strings split on empty string

**strings-eager-len**(bool) strings eager length lemmas

**strings-check-entail-len**(bool) check entailment between length terms to reduce splitting

**strings-process-loop**(bool) reduce looping word equations to regular expressions

**strings-abort-loop**(bool) abort when a looping word equation is encountered

**strings-infer-as-lemmas**(bool) always send lemmas out instead of making internal inferences

**strings-rexplain-lemmas**(bool) regression explanations for string lemmas

**strings-min-prefix-explain**(bool) minimize explanations for prefix of normal forms in strings

**strings-guess-model**(bool) use model guessing to avoid string extended function reductions

**strings-uf-reduct**(bool) use uninterpreted functions when applying extended function reductions

**strings-binary-csp**(bool) use binary search when splitting strings

**strings-lprop-csp**(bool) do length propagation based on constant splits

*THEORY LAYER OPTIONS***theoryof-mode**(CVC4::theory::TheoryOfMode) mode for Theory::theoryof() (EXPERTS only)

**use-theory**(std::string) 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***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-regions**(bool) disable region-based method for discovering cliques and splits in uf strong solver

**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=
**MODE** (CVC4::theory::uf::UfssMode) mode of operation 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

**uf-ss-fair-monotone**(bool) group monotone sorts when enforcing fairness for finite model finding

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