

 
SMTENGINE(3cvc) 
CVC4 Library Interfaces 
SMTENGINE(3cvc) 
SmtEngine  the primary interface to CVC4's theoremproving capabilities
SmtEngine is the main entry point into the CVC4 theorem prover API.
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
 inputlanguage
 (InputLanguage) force input language (default is "auto"; see
lang help)
 outputlanguage
 (OutputLanguage) force output language (default is "auto"; see
outputlang help)
 quiet
 (void) decrease verbosity (may be repeated)
 statistics
 (bool) give statistics on exit
 verbose
 (void) increase verbosity (may be repeated)
 copyright
 (void) show CVC4 copyright information
 help
 (bool) full command line reference
 seed
 (uint64_t) seed for random number generator
 showconfig
 (void) show CVC4 static configuration
 version
 (bool) identify this CVC4 binary
 strictparsing
 (bool) be less tolerant of nonconforming inputs
 cputime
 (bool) measures CPU time if set to true and wall time if false (default
false)
 dumpto
 (std::string) all dumping goes to FILE (instead of stdout)
 dump
 (std::string) dump preprocessed assertions, etc., see dump=help
 hardlimit
 (bool) the resource limit is hard potentially leaving the smtEngine in an
unsafe state (should be destroyed and rebuild after resourcing out)
 incremental
 (bool) enable incremental solving
 produceassertions
 (bool) keep an assertions list (enables getassertions command)
 producemodels
 (bool) support the getvalue and getmodel commands
 reproducibleresourcelimit
 (unsigned long) enable resource limiting per query
 rlimit
 (unsigned long) enable resource limiting (currently, roughly the number of
SAT conflicts)
 tlimitper
 (unsigned long) enable time limiting per query (give milliseconds)
 tlimit
 (unsigned long) enable time limiting (give milliseconds)
 ARITHMETIC THEORY OPTIONS
 approxbranchdepth
 (int16_t) maximum branch depth the approximate solver is allowed to
take
 arithnopartialfun
 (bool) do not use partial function semantics for arithmetic (not SMT LIB
compliant)
 arithpropclauses
 (uint16_t) rows shorter than this are propagated as clauses
 arithprop
 (ArithPropagationMode) turns on arithmetic propagation (default is 'old',
see arithprop=help)
 arithrewriteequalities
 (bool) turns on the preprocessing rewrite turning equalities into a
conjunction of inequalities
 collectpivotstats
 (bool) collect the pivot history
 cutallbounded
 (bool) turns on the integer solving step of periodically cutting all
integer variables that have both upper and lower bounds
 diodecomps
 (bool) let skolem variables for integer divisibility constraints leak from
the dio solver
 diorepeat
 (bool) handle dio solver constraints in mass or one at a time
 diosolver
 (bool) turns on Linear Diophantine Equation solver (Griggio, JSAT
2012)
 dioturns
 (int) turns in a row dio solver cutting gets
 errorselectionrule
 (ErrorSelectionRule) change the pivot rule for the basic variable (default
is 'min', see pivotrule help)
 fcpenalties
 (bool) turns on degenerate pivot penalties
 heuristicpivots
 (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
 lemmasonreplayfailure
 (bool) attempt to use external lemmas if approximate solve integer
failed
 maxCutsInContext
 (unsigned) maximum cuts in a given context before signalling a
restart
 miplibtrick
 (bool) turns on the preprocessing step of attempting to infer bounds on
miplib problems
 miplibtricksubs
 (unsigned) do substitution for miplib 'tmp' vars if defined in <= N
eliminated vars
 newprop
 (bool) use the new row propagation system
 nlext
 (bool) extended approach to nonlinear
 nlextentconf
 (bool) check for entailed conflicts in nonlinear solver
 nlextfactor
 (bool) use factoring inference in nonlinear solver
 nlextincprec
 (bool) whether to increment the precision for irrational function
constraints
 nlextpurify
 (bool) purify nonlinear terms at preprocess
 nlextrbound
 (bool) use resolutionstyle inference for inferring new bounds
 nlextrewrite
 (bool) do rewrites in nonlinear solver
 nlextsplitzero
 (bool) intial splits on zero for all variables
 nlexttftaylordeg
 (int16_t) initial degree of polynomials for Taylor approximation
 nlexttftplanes
 (bool) use nonterminating tangent plane strategy for transcendental
functions for nonlinear
 nlexttplanes
 (bool) use nonterminating tangent plane strategy for nonlinear
 nlexttplanesinterleave
 (bool) interleave tangent plane strategy for nonlinear
 pbrewrites
 (bool) apply pseudo boolean rewrites
 pivotthreshold
 (uint16_t) sets the number of pivots using pivotrule per basic variable
per simplex instance before using variable order
 ppassertmaxsubsize
 (unsigned) threshold for substituting an equality in ppAssert
 proprowlength
 (uint16_t) sets the maximum row length to be used in propagation
 replayearlyclosedepth
 (int) multiples of the depths to try to close the approx log eagerly
 replayfailurepenalty
 (int) number of solve integer attempts to skips after a numeric
failure
 replaylemmarejectcut
 (unsigned) maximum complexity of any coefficient while outputting
replaying cut lemmas
 replaynumerrpenalty
 (int) number of solve integer attempts to skips after a numeric
failure
 replayrejectcut
 (unsigned) maximum complexity of any coefficient while replaying cuts
 replaysoimajorthreshold
 (double) threshold for a major tolerance failure by the approximate
solver
 replaysoimajorthresholdpen
 (int) threshold for a major tolerance failure by the approximate
solver
 replaysoiminorthreshold
 (double) threshold for a minor tolerance failure by the approximate
solver
 replaysoiminorthresholdpen
 (int) threshold for a minor tolerance failure by the approximate
solver
 restrictpivots
 (bool) have a pivot cap for simplex at effort levels below fullEffort
 revertarithmodelsonunsat
 (bool) revert the arithmetic model to a known safe model on unsat if one
is cached
 rewritedivk
 (bool) rewrite division and mod when by a constant into linear terms
 rrturns
 (int) round robin turn
 sesolveint
 (bool) attempt to use the approximate solve integer method on standard
effort
 simplexcheckperiod
 (uint16_t) the number of pivots to do in simplex before rechecking for a
conflict on all variables
 snorminfereq
 (bool) infer equalities based on Shostak normalization
 soiqe
 (bool) use quick explain to minimize the sum of infeasibility
conflicts
 standardeffortvariableorderpivots
 (int16_t) limits the number of pivots in a single invocation of check() at
a nonfull effort level using Bland's pivot rule (EXPERTS only)
 unatelemmas
 (ArithUnateLemmaMode) determines which lemmas to add before solving
(default is 'all', see unatelemmas=help)
 useapprox
 (bool) attempt to use an approximate solver
 usefcsimplex
 (bool) use focusing and converging simplex (FMCAD 2013 submission)
 usesoi
 (bool) use sum of infeasibility simplex (FMCAD 2013 submission)
 ARRAYS THEORY OPTIONS
 arraysconfig
 (int) set different array option configurations  for developers only
 arrayseagerindex
 (bool) turn on eager index splitting for generated array lemmas
 arrayseagerlemmas
 (bool) turn on eager lemma generation for arrays
 arrayslazyrintro1
 (bool) turn on optimization to only perform RIntro1 rule lazily (see
Jovanovic/Barrett 2012: Being Careful with Theory Combination)
 arraysmodelbased
 (bool) turn on modelbased array solver
 arraysoptimizelinear
 (bool) turn on optimization for linear array terms (see de Moura FMCAD 09
arrays paper)
 arraysprop
 (int) propagation effort for arrays: 0 is none, 1 is some, 2 is full
 arraysreducesharing
 (bool) use model information to reduce size of care graph for arrays
 arraysweakequiv
 (bool) use algorithm from Christ/Hoenicke (SMT 2014)
 BASE OPTIONS
 debug
 (std::string) debug something (e.g. d arith), can repeat
 parseonly
 (bool) exit after parsing input
 preprocessonly
 (bool) exit after preprocessing input
 printsuccess
 (bool) print the "success" output required of SMTLIBv2
 statseveryquery
 (bool) in incremental mode, print stats after every satisfiability or
validity query
 statshidezeros
 (bool) hide statistics which are zero
 trace
 (std::string) trace something (e.g. t pushpop), can repeat
 verbosity
 (int) the verbosity level of CVC4
 hidezerostats
 [undocumented]
 language
 [undocumented]
 nostatistics
 [undocumented]
 nostatisticseveryquery
 [undocumented]
 outputlanguage
 [undocumented]
 showzerostats
 [undocumented]
 smtlibstrict
 SMTLIBv2 compliance mode (implies other options)
 statistics
 [undocumented]
 statisticseveryquery
 [undocumented]
 statsshowzeros
 [undocumented]
 BITVECTOR THEORY OPTIONS
 bitblastaig
 (bool) bitblast by first converting to AIG (implies bitblast=eager)
 bitblast
 (CVC4::theory::bv::BitblastMode) choose bitblasting mode, see
bitblast=help
 booltobv
 (bool) convert booleans to bitvectors of size 1 when possible
 bvabstraction
 (bool) mcm benchmark abstraction (EXPERTS only)
 bvaigsimp
 (std::string) abc command to run AIG simplifications (implies
bitblastaig, default is "balance;drw") (EXPERTS only)
 bvalgextf
 (bool) algebraic inferences for extended functions
 bvalgebraicbudget
 (unsigned) the budget allowed for the algebraic solver in number of SAT
conflicts (EXPERTS only)
 bvalgebraicsolver
 (bool) turn on the algebraic solver for the bitvector theory (only if
bitblast=lazy)
 bvdivzeroconst
 (bool) always return 1 on division by zero
 bveagerexplanations
 (bool) compute bitblasting propagation explanations eagerly (EXPERTS
only)
 bveqslicer
 (CVC4::theory::bv::BvSlicerMode) turn on the slicing equality solver for
the bitvector theory (only if bitblast=lazy)
 bveqsolver
 (bool) use the equality engine for the bitvector theory (only if
bitblast=lazy)
 bvextractarith
 (bool) enable rewrite pushing extract [i:0] over arithmetic operations
(can blow up) (EXPERTS only)
 bvgausselim
 (bool) simplify formula via Gaussian Elimination if applicable (EXPERTS
only)
 bvinequalitysolver
 (bool) turn on the inequality solver for the bitvector theory (only if
bitblast=lazy)
 bvintropow2
 (bool) introduce bitvector powers of two as a preprocessing pass (EXPERTS
only)
 bvlazyreduceextf
 (bool) reduce extended functions like bv2nat and int2bv at last call
instead of full effort
 bvlazyrewriteextf
 (bool) lazily rewrite extended functions like bv2nat and int2bv
 bvnumfunc
 (unsigned) number of function symbols in conflicts that are generalized
(EXPERTS only)
 bvpropagate
 (bool) use bitvector propagation in the bitblaster
 bvquickxplain
 (bool) minimize bv conflicts using the QuickXplain algorithm (EXPERTS
only)
 bvsatsolver
 (CVC4::theory::bv::SatSolverMode) choose which sat solver to use, see
bvsatsolver=help (EXPERTS only)
 bvskolemize
 (bool) skolemize arguments for bv abstraction (only does something if
bvabstraction is on) (EXPERTS only)
 bvtobool
 (bool) lift bitvectors of size 1 to booleans when possible
 DATATYPES THEORY OPTIONS
 cdtbisimilar
 (bool) do bisimilarity check for codatatypes
 dtbinarysplit
 (bool) do binary splits for datatype constructor types
 dtblastsplits
 (bool) when applicable, blast splitting lemmas for all variables at
once
 dtcyclic
 (bool) do cyclicity check for datatypes
 dtforceassignment
 (bool) force the datatypes solver to give specific values to all datatypes
terms before answering sat
 dtinferaslemmas
 (bool) always send lemmas out instead of making internal inferences
 dtrefskintro
 (bool) introduce reference skolems for shorter explanations
 dtrewriteerrorsel
 (bool) rewrite incorrectly applied selectors to arbitrary ground term
(EXPERTS only)
 dtsharesel
 (bool) internally use shared selectors across multiple constructors
 dtusetesters
 (bool) do not preprocess away tester predicates
 sygusabortsize
 (int) tells enumerative sygus to only consider solutions up to term size N
(1 == no limit, default)
 sygusevalbuiltin
 (bool) use builtin kind for evaluation functions in sygus
 sygusfairmax
 (bool) use max instead of sum for multifunction sygus conjectures
 sygusfair
 (CVC4::theory::SygusFairMode) if and how to apply fairness for sygus
 sygusopt1
 (bool) sygus experimental option
 sygussymbreak
 (bool) simple sygus sym break lemmas
 sygussymbreakdynamic
 (bool) dynamic sygus sym break lemmas
 sygussymbreaklazy
 (bool) lazily add symmetry breaking lemmas for terms
 sygussymbreakpbe
 (bool) sygus sym break lemmas based on pbe conjectures
 sygussymbreakrlv
 (bool) add relevancy conditions to symmetry breaking lemmas
 DECISION HEURISTICS OPTIONS
 decisionrandomweight
 (int) assign random weights to nodes between 0 and N1 (0: disable)
(EXPERTS only)
 decisionthreshold
 (decision::DecisionWeight) ignore all nodes greater than threshold in
first attempt to pick decision (EXPERTS only)
 decisionuseweight
 (bool) use the weight nodes (locally, by looking at children) to direct
recursive search (EXPERTS only)
 decisionweightinternal
 (decision::DecisionWeightInternal) computer weights of internal nodes
using children: off, max, sum, usr1 (meaning evolving) (EXPERTS only)
 decisionmode
 (decision::DecisionMode) choose decision mode, see decision=help
 EXPRESSION PACKAGE OPTIONS
 defaultdagthresh
 (int) dagify common subexprs appearing > N times (1 == default, 0 ==
don't dagify)
 defaultexprdepth
 (int) print exprs to depth N (0 == default, 1 == no limit)
 eagertypechecking
 (bool) type check expressions immediately on creation (debug builds
only)
 printexprtypes
 (bool) print types with variables when printing exprs
 typechecking
 (bool) never type check expressions
 dagthresh
 [undocumented]
 dagthreshold
 [undocumented]
 exprdepth
 [undocumented]
 notypechecking
 [undocumented]
 IDL OPTIONS
 idlrewriteequalities
 (bool) enable rewriting equalities into two inequalities in IDL solver
(default is disabled)
 DRIVER OPTIONS
 continuedexecution
 (bool) continue executing commands, even on error
 earlyexit
 (bool) do not run destructors at exit; default on except in debug builds
(EXPERTS only)
 fallbacksequential
 (bool) Switch to sequential mode (instead of printing an error) if it
can't be solved in portfolio mode
 filterlemmalength
 (int) don't share (among portfolio threads) lemmas strictly longer than
N
 incrementalparallel
 (bool) Use parallel solver even in incremental mode (may print 'unknown's
at times)
 interactive
 (bool) force interactive/noninteractive mode
 interactiveprompt
 (bool) interactive prompting while in interactive mode
 segvspin
 (bool) spin on segfault/other crash waiting for gdb
 showdebugtags
 (void) show all available tags for debugging
 showtracetags
 (void) show all available tags for tracing
 teardownincremental
 (int) implement PUSH/POP/multiquery by destroying and recreating
SmtEngine every N queries (EXPERTS only)
 threadstack
 (unsigned) stack size for worker threads in MB (0 means use Boost/thread
lib default)
 threadN
 (void) configures portfolio thread N (0..#threads1)
 threads
 (unsigned) Total number of threads for portfolio
 waittojoin
 (bool) wait for other threads to join before quitting (EXPERTS only)
 license
 [undocumented]
 segvnospin
 [undocumented]
 PARSER OPTIONS
 filesystemaccess
 (bool) [undocumented]
 globaldeclarations
 (bool) force all declarations and definitions to be global
 mmap
 (bool) memory map file input
 semanticchecks
 (bool) disable ALL semantic checks, including type checks
 nochecking
 [undocumented]
 noincludefile
 [undocumented]
 PRINTING OPTIONS
 instformat
 (InstFormatMode) print format mode for instantiations, see
instformat=help
 modelformat
 (ModelFormatMode) print format mode for models, see
modelformat=help
 PROOF OPTIONS
 aggressivecoremin
 (bool) turns on aggressive unsat core minimization (experimental)
 allowemptydependencies
 (bool) if unable to track the dependencies of a rewritten/preprocessed
assertion, fail silently
 fewerpreprocessingholes
 (bool) try to eliminate preprocessing holes in proofs
 lfscletification
 (bool) turns on global letification in LFSC proofs
 SAT LAYER OPTIONS
 minisatdumpdimacs
 (bool) instead of solving minisat dumps the asserted clauses in Dimacs
format
 minisatelimination
 (bool) use Minisat elimination
 randomfrequency
 (double) sets the frequency of random decisions in the sat solver (P=0.0
by default)
 randomseed
 (uint32_t) sets the random seed for the sat solver
 refineconflicts
 (bool) refine theory conflict clauses (default false)
 restartintbase
 (unsigned) sets the base restart interval for the sat solver (N=25 by
default)
 restartintinc
 (double) sets the restart interval increase factor for the sat solver
(F=3.0 by default)
 QUANTIFIERS OPTIONS
 agminiscopequant
 (bool) perform aggressive miniscoping for quantifiers
 cbqi
 (bool) turns on counterexamplebased quantifier instantiation
 cbqiall
 (bool) apply counterexamplebased instantiation to all quantified
formulas
 cbqibv
 (bool) use wordlevel inversion approach for counterexampleguided
quantifier instantiation for bitvectors
 cbqibvconcatinv
 (bool) compute inverse for concat over equalities rather than producing an
invertibility condition
 cbqibvineq
 (CVC4::theory::quantifiers::CbqiBvIneqMode) choose mode for handling
bitvector inequalities with counterexampleguided instantiation
 cbqibvinterleavevalue
 (bool) interleave model value instantiation with wordlevel inversion
approach
 cbqibvlinear
 (bool) linearize adder chains for variables
 cbqibvrmextract
 (bool) replaces extract terms with variables for counterexampleguided
instantiation for bitvectors
 cbqibvsolvenl
 (bool) try to solve nonlinear bv literals using model value
projections
 cbqifull
 (bool) turns on full effort counterexamplebased quantifier instantiation,
which may resort to modelvalue instantiation
 cbqiinnermost
 (bool) only process innermost quantified formulas in counterexamplebased
quantifier instantiation
 cbqilitdep
 (bool) dependency lemmas for quantifier alternation in
counterexamplebased quantifier instantiation
 cbqimidpoint
 (bool) choose substitutions based on midpoints of lower and upper bounds
for counterexamplebased quantifier instantiation
 cbqiminbounds
 (bool) use minimally constrained lower/upper bound for
counterexamplebased quantifier instantiation
 cbqimodel
 (bool) guide instantiations by model values for counterexamplebased
quantifier instantiation
 cbqimultiinst
 (bool) when applicable, do multi instantiations per quantifier per round
in counterexamplebased quantifier instantiation
 cbqinestedqe
 (bool) process nested quantified formulas with quantifier elimination in
counterexamplebased quantifier instantiation
 cbqinopt
 (bool) nonoptimal bounds for counterexamplebased quantifier
instantiation
 cbqiprereginst
 (bool) preregister ground instantiations in counterexamplebased
quantifier instantiation
 cbqirecurse
 (bool) turns on recursive counterexamplebased quantifier
instantiation
 cbqirepeatlit
 (bool) solve literals more than once in counterexamplebased quantifier
instantiation
 cbqirounduplia
 (bool) round up integer lower bounds in substitutions for
counterexamplebased quantifier instantiation
 cbqisat
 (bool) answer sat when quantifiers are asserted with counterexamplebased
quantifier instantiation
 cbqiuseinfint
 (bool) use integer infinity for vts in counterexamplebased quantifier
instantiation
 cbqiuseinfreal
 (bool) use real infinity for vts in counterexamplebased quantifier
instantiation
 cegissample
 (CVC4::theory::quantifiers::CegisSampleMode) mode for using samples in the
counterexampleguided inductive synthesis loop
 cegqi
 (bool) counterexampleguided quantifier instantiation for sygus
 cegqisiabort
 (bool) abort if synthesis conjecture is not single invocation
 cegqisipartial
 (bool) combined techniques for synthesis conjectures that are partially
single invocation
 cegqisireconstruct
 (bool) reconstruct solutions for single invocation conjectures in original
grammar
 cegqisireconstructconst
 (bool) include constants when reconstruct solutions for single invocation
conjectures in original grammar
 cegqisisolmincore
 (bool) minimize solutions for single invocation conjectures based on unsat
core
 cegqisisolmininst
 (bool) minimize individual instantiations for single invocation
conjectures based on unsat core
 cegqisi
 (CVC4::theory::quantifiers::CegqiSingleInvMode) mode for processing single
invocation synthesis conjectures
 condrewritequant
 (bool) conditional rewriting of quantified formulas
 condvarsplitaggquant
 (bool) aggressive split quantified formulas that lead to variable
eliminations
 condvarsplitquant
 (bool) split quantified formulas that lead to variable eliminations
 conjecturefilteractiveterms
 (bool) filter based on active terms
 conjecturefiltercanonical
 (bool) filter based on canonicity
 conjecturefiltermodel
 (bool) filter based on model
 conjecturegen
 (bool) generate candidate conjectures for inductive proofs
 conjecturegengtenum
 (int) number of ground terms to generate for model filtering
 conjecturegenmaxdepth
 (int) maximum depth of terms to consider for conjectures
 conjecturegenperround
 (int) number of conjectures to generate per instantiation round
 conjecturegenueeintro
 (bool) more aggressive merging for universal equality engine, introduces
terms
 conjecturenofilter
 (bool) do not filter conjectures
 dtstcind
 (bool) apply strengthening for existential quantification over datatypes
based on structural induction
 dtvarexpquant
 (bool) expand datatype variables bound to one constructor in
quantifiers
 ematching
 (bool) whether to do heuristic Ematching
 elimextarithquant
 (bool) eliminate extended arithmetic symbols in quantified formulas
 elimtautquant
 (bool) eliminate tautological disjuncts of quantified formulas
 finitemodelfind
 (bool) use finite model finding heuristic for quantifier
instantiation
 fmfbound
 (bool) finite model finding on bounded quantification
 fmfboundint
 (bool) finite model finding on bounded integer quantification
 fmfboundlazy
 (bool) enforce bounds for bounded quantification lazily via use of proxy
variables
 fmfboundminmode
 (CVC4::theory::quantifiers::FmfBoundMinMode) mode for which types of
bounds to minimize via first decision heuristics
 fmfemptysorts
 (bool) allow finite model finding to assume sorts that do not occur in
ground assertions are empty
 fmffmcsimple
 (bool) simple models in full model check for finite model finding
 fmffreshdc
 (bool) use fresh distinguished representative when applying InstGen
techniques
 fmffun
 (bool) find models for recursively defined functions, assumes functions
are admissible
 fmffunrlv
 (bool) find models for recursively defined functions, assumes functions
are admissible, allows empty type when function is irrelevant
 fmfinstengine
 (bool) use instantiation engine in conjunction with finite model
finding
 fmfinstgen
 (bool) enable InstGen instantiation techniques for finite model
finding
 fmfinstgenonequantperround
 (bool) only perform InstGen instantiation techniques on one quantifier
per round
 fsinterleave
 (bool) interleave full saturate instantiation with other techniques
 fullsaturatequant
 (bool) when all other quantifier instantiation strategies fail,
instantiate with ground terms from relevant domain, then arbitrary ground
terms before answering unknown
 fullsaturatequantrd
 (bool) whether to use relevant domain first for full saturation
instantiation strategy
 globalnegate
 (bool) do global negation of input formula
 homatching
 (bool) do higherorder matching algorithm for triggers with variable
operators
 homatchingvarpriority
 (bool) give priority to variable arguments over constant arguments
 homergetermdb
 (bool) merge term indices modulo equality
 incrementtriggers
 (bool) generate additional triggers as needed during search
 inferarithtriggereq
 (bool) infer equalities for trigger terms based on solving arithmetic
equalities
 inferarithtriggereqexp
 (bool) record explanations for inferArithTriggerEq
 instlevelinputonly
 (bool) only input terms are assigned instantiation level zero
 instmaxlevel
 (int) maximum inst level of terms used to instantiate quantified formulas
with (1 == no limit, default)
 instnoentail
 (bool) do not consider instances of quantified formulas that are currently
entailed
 instnomodeltrue
 (bool) do not consider instances of quantified formulas that are currently
true in model, if it is available
 instprop
 (bool) internal propagation for instantiations for selecting relevant
instances
 instwhenphase
 (int) instantiation rounds quantifiers takes (>=1) before allowing
theory combination to happen
 instwhenstrictinterleave
 (bool) ensure theory combination and standard quantifier effort strategies
take turns
 instwhentcfirst
 (bool) allow theory combination to happen once initially, before
quantifier strategies are run
 instwhen
 (CVC4::theory::quantifiers::InstWhenMode) when to apply instantiation
 intwfind
 (bool) apply strengthening for integers based on wellfounded
induction
 itedttsplitquant
 (bool) split ites with dt testers as conditions
 iteliftquant
 (CVC4::theory::quantifiers::IteLiftQuantMode) ite lifting mode for
quantified formulas
 literalmatching
 (CVC4::theory::quantifiers::LiteralMatchMode) choose literal matching
mode
 localtext
 (bool) do instantiation based on local theory extensions
 ltepartialinst
 (bool) partially instantiate local theory quantifiers
 lterestrictinstclosure
 (bool) treat arguments of inst closure as restricted terms for
instantiation
 macrosquant
 (bool) perform quantifiers macro expansion
 macrosquantmode
 (CVC4::theory::quantifiers::MacrosQuantMode) mode for quantifiers macro
expansion
 mbqiinterleave
 (bool) interleave modelbased quantifier instantiation with other
techniques
 mbqioneinstperround
 (bool) only add one instantiation per quantifier per round for mbqi
 mbqionequantperround
 (bool) only add instantiations for one quantifier per round for mbqi
 mbqi
 (CVC4::theory::quantifiers::MbqiMode) choose mode for modelbased
quantifier instantiation
 miniscopequant
 (bool) miniscope quantifiers
 miniscopequantfv
 (bool) miniscope quantifiers for ground subformulas
 multitriggercache
 (bool) caching version of multi triggers
 multitriggerlinear
 (bool) implementation of multi triggers where maximum number of
instantiations is linear wrt number of ground terms
 multitriggerpriority
 (bool) only try multi triggers if single triggers give no
instantiations
 multitriggerwhensingle
 (bool) select multi triggers when single triggers exist
 partialtriggers
 (bool) use triggers that do not contain all free variables
 preskolemquant
 (bool) apply skolemization eagerly to bodies of quantified formulas
 preskolemquantagg
 (bool) apply skolemization to quantified formulas aggressively
 preskolemquantnested
 (bool) apply skolemization to nested quantified formulas
 prenexquantuser
 (bool) prenex quantified formulas with user patterns
 prenexquant
 (CVC4::theory::quantifiers::PrenexQuantMode) prenex mode for quantified
formulas
 purethtriggers
 (bool) use pure theory terms as single triggers
 purifydttriggers
 (bool) purify dt triggers, match all constructors of correct form instead
of selectors
 purifytriggers
 (bool) purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y1
 qcfallconflict
 (bool) add all available conflicting instances during conflictbased
instantiation
 qcfeagercheckrd
 (bool) optimization, eagerly check relevant domain of matched
position
 qcfeagertest
 (bool) optimization, test qcf instances eagerly
 qcfnestedconflict
 (bool) consider conflicts for nested quantifiers
 qcfskiprd
 (bool) optimization, skip instances based on possibly irrelevant portions
of quantified formulas
 qcftconstraint
 (bool) enable entailment checks for tconstraints in qcf algorithm
 qcfvoexp
 (bool) qcf experimental variable ordering
 quantalphaequiv
 (bool) infer alpha equivalence between quantified formulas
 quantantiskolem
 (bool) perform antiskolemization for quantified formulas
 quantcf
 (bool) enable conflict find mechanism for quantifiers
 quantcfmode
 (CVC4::theory::quantifiers::QcfMode) what effort to apply conflict find
mechanism
 quantcfwhen
 (CVC4::theory::quantifiers::QcfWhenMode) when to invoke conflict find
mechanism for quantifiers
 quantdsplitmode
 (CVC4::theory::quantifiers::QuantDSplitMode) mode for dynamic quantifiers
splitting
 quantepr
 (bool) infer whether in effectively propositional fragment, use for
cbqi
 quanteprmatch
 (bool) use matching heuristics for EPR instantiation
 quantfunwd
 (bool) assume that function defined by quantifiers are well defined
 quantind
 (bool) use all available techniques for inductive reasoning
 quantmodelee
 (bool) use equality engine of model for last call effort
 quantrepmode
 (CVC4::theory::quantifiers::QuantRepMode) selection mode for
representatives in quantifiers engine
 quantsplit
 (bool) apply splitting to quantified formulas based on variable disjoint
disjuncts
 registerquantbodyterms
 (bool) consider ground terms within bodies of quantified formulas for
matching
 relationaltriggers
 (bool) choose relational triggers such as x = f(y), x >= f(y)
 relevanttriggers
 (bool) prefer triggers that are more relevant based on SInE style
analysis
 rewriterules
 (bool) use rewrite rules module
 rroneinstperround
 (bool) add one instance of rewrite rule per round
 stricttriggers
 (bool) only instantiate quantifiers with user patterns based on
triggers
 sygusaddconstgrammar
 (bool) statically add constants appearing in conjecture to grammars
 sygusautounfold
 (bool) enable approach which automatically unfolds transition systems for
directly solving invariant synthesis problems
 sygusboolitereturnconst
 (bool) Only use Boolean constants for return values in unificationbased
function synthesis
 sygusevalunfold
 (bool) do unfolding of sygus evaluation functions
 sygusevalunfoldbool
 (bool) do unfolding of Boolean evaluation functions that appear in
refinement lemmas
 sygusextrew
 (bool) use extended rewriter for sygus
 sygusgrammarnorm
 (bool) statically normalize sygus grammars based on flattening
(linearization)
 sygusinference
 (bool) attempt to preprocess arbitrary inputs to sygus conjectures
 sygusinvtemplwhensg
 (bool) use invariant templates (with solution reconstruction) for syntax
guided problems
 sygusinvtempl
 (CVC4::theory::quantifiers::SygusInvTemplMode) template mode for sygus
invariant synthesis (weaken precondition, strengthen postcondition, or
none)
 sygusmingrammar
 (bool) statically minimize sygus grammars
 syguspbe
 (bool) enable approach which unifies conditional solutions, specialized
for programmingbyexamples (pbe) conjectures
 sygusqepreproc
 (bool) use quantifier elimination as a preprocessing step for sygus
 sygusrefeval
 (bool) direct evaluation of refinement lemmas for conflict analysis
 sygusrepairconst
 (bool) use approach to repair constants in sygus candidate solutions
 sygusrr
 (bool) use sygus to enumerate and verify correctness of rewrite rules via
sampling
 sygusrrsynth
 (bool) use sygus to enumerate candidate rewrite rules via sampling
 sygusrrsynthaccel
 (bool) add dynamic symmetry breaking clauses based on candidate
rewrites
 sygusrrsynthcheck
 (bool) use satisfiability check to verify correctness of candidate
rewrites
 sygusrrsynthfiltercong
 (bool) filter candidate rewrites based on congruence
 sygusrrsynthfiltermatch
 (bool) filter candidate rewrites based on matching
 sygusrrsynthfilterorder
 (bool) filter candidate rewrites based on variable ordering
 sygusrrverify
 (bool) use sygus to verify the correctness of rewrite rules via
sampling
 sygusrrverifyabort
 (bool) abort when sygusrrverify finds an instance of unsoundness
 sygussamplegrammar
 (bool) when applicable, use grammar for choosing sample points
 sygussamples
 (int) number of points to consider when doing sygus rewriter sample
testing
 sygusstream
 (bool) enumerate a stream of solutions instead of terminating after the
first one
 sygustemplembedgrammar
 (bool) embed sygus templates into grammars
 sygusunif
 (bool) Unificationbased function synthesis
 termdbmode
 (CVC4::theory::quantifiers::TermDbMode) which ground terms to consider for
instantiation
 trackinstlemmas
 (bool) track instantiation lemmas (for proofs, unsat cores, qe and
synthesis minimization)
 triggeractivesel
 (CVC4::theory::quantifiers::TriggerActiveSelMode) selection mode to
activate triggers
 triggersel
 (CVC4::theory::quantifiers::TriggerSelMode) selection mode for
triggers
 userpat
 (CVC4::theory::quantifiers::UserPatMode) policy for handling userprovided
patterns for quantifier instantiation
 varelimquant
 (bool) enable simple variable elimination for quantified formulas
 varineqelimquant
 (bool) enable variable elimination based on infinite projection of unbound
arithmetic variables
 SEP OPTIONS
 sepcheckneg
 (bool) check negated spatial assertions
 sepchildrefine
 (bool) childspecific refinements of negated star, positive wand
 sepdeqc
 (bool) assume cardinality elements are distinct
 sepexp
 (bool) experimental flag for sep
 sepminrefine
 (bool) only add refinement lemmas for minimal (innermost) assertions
 seppreskolememp
 (bool) eliminate emp constraint at preprocess time
 SETS OPTIONS
 setsext
 (bool) enable extended symbols such as complement and universe in theory
of sets
 setsinferaslemmas
 (bool) send inferences as lemmas
 setsproxylemmas
 (bool) introduce proxy variables eagerly to shorten lemmas
 setsreleager
 (bool) standard effort checks for relations
 SMT LAYER OPTIONS
 abstractvalues
 (bool) in models, output arrays (and in future, maybe others) using
abstract values, as required by the SMTLIB standard
 bitblaststep
 (unsigned) amount of resources spent for each bitblast step (EXPERTS
only)
 bvsatconflictstep
 (unsigned) amount of resources spent for each sat conflict (bitvectors)
(EXPERTS only)
 checkmodels
 (bool) after SAT/INVALID/UNKNOWN, check that the generated model satisfies
user assertions
 checkproofs
 (bool) after UNSAT/VALID, machinecheck the generated proof
 checksynthsol
 (bool) checks whether produced solutions to functionstosynthesize
satisfy the conjecture
 checkunsatcores
 (bool) after UNSAT/VALID, produce and check an unsat core (expensive)
 cnfstep
 (unsigned) amount of resources spent for each call to cnf conversion
(EXPERTS only)
 decisionstep
 (unsigned) amount of getNext decision calls in the decision engine
(EXPERTS only)
 diagnosticoutputchannel
 (std::string) set the diagnostic output channel of the solver
 dumpinstantiations
 (bool) output instantiations of quantified formulas after every
UNSAT/VALID response
 dumpmodels
 (bool) output models after every SAT/INVALID/UNKNOWN response
 dumpproofs
 (bool) output proofs after every UNSAT/VALID response
 dumpsynth
 (bool) output solution for synthesis conjectures after every UNSAT/VALID
response
 dumpunsatcores
 (bool) output unsat cores after every UNSAT/VALID response
 dumpunsatcoresfull
 (bool) dump the full unsat core, including unlabeled assertions
 expanddefinitions
 (bool) always expand symbol definitions in output
 extrewprep
 (bool) use extended rewriter as a preprocessing pass
 extrewprepagg
 (bool) use aggressive extended rewriter as a preprocessing pass
 forcelogic
 (std::string) set the logic, and override all further user attempts to
change it (EXPERTS only)
 forcenolimitcpuwhiledump
 (bool) Force no CPU limit when dumping models and proofs
 interactivemode
 (bool) deprecated name for produceassertions
 itesimp
 (bool) turn on ite simplification (Kim (and Somenzi) et al., SAT
2009)
 lemmastep
 (unsigned) amount of resources spent when adding lemmas (EXPERTS
only)
 modeludtenum
 (bool) in models, output uninterpreted sorts as datatype enumerations
 omitdontcares
 (bool) When producing a model, omit variables whose value does not
matter
 onrepeatitesimp
 (bool) do the ite simplification pass again if repeating
simplification
 parsestep
 (unsigned) amount of resources spent for each command/expression parsing
(EXPERTS only)
 preprocessstep
 (unsigned) amount of resources spent for each preprocessing step in
SmtEngine (EXPERTS only)
 produceassignments
 (bool) support the getassignment command
 produceunsatassumptions
 (bool) turn on unsat assumptions generation
 produceunsatcores
 (bool) turn on unsat core generation
 produceproofs
 (bool) turn on proof generation
 quantifierstep
 (unsigned) amount of resources spent for quantifier instantiations
(EXPERTS only)
 regularoutputchannel
 (std::string) set the regular output channel of the solver
 repeatsimp
 (bool) make multiple passes with nonclausal simplifier
 replaylog
 (std::string) replay decisions from file
 replay
 (std::string) replay decisions from file
 restartstep
 (unsigned) amount of resources spent for each theory restart (EXPERTS
only)
 rewriteapplytoconst
 (bool) eliminate function applications, rewriting e.g. f(5) to a new
symbol f_5 (EXPERTS only)
 rewritestep
 (unsigned) amount of resources spent for each rewrite step (EXPERTS
only)
 satconflictstep
 (unsigned) amount of resources spent for each sat conflict (main sat
solver) (EXPERTS only)
 simpitecompress
 (bool) enables compressing ites after ite simplification
 simpitehuntzombies
 (uint32_t) post ite compression enables zombie removal while the number of
nodes is above this threshold
 simpwithcare
 (bool) enables simplifyWithCare in ite simplificiation
 simplificationmode
 (SimplificationMode) choose simplification mode, see
simplification=help
 solveintasbv
 (uint32_t) attempt to solve a pure integer satisfiable problem by
bitblasting in sufficient bitwidth (experimental)
 solverealasint
 (bool) attempt to solve a pure real satisfiable problem as an integer
problem (for nonlinear)
 sortinference
 (bool) calculate sort inference of input problem, convert the input based
on monotonic sorts
 staticlearning
 (bool) use static learning (on by default)
 sygusout
 (SygusSolutionOutMode) output mode for sygus
 sygusprintcallbacks
 (bool) use sygus print callbacks to print sygus terms in the userprovided
form (disable for debugging)
 symmetrybreakerexp
 (bool) generate symmetry breaking constraints after symmetry
detection
 theorycheckstep
 (unsigned) amount of resources spent for each theory check call (EXPERTS
only)
 unconstrainedsimp
 (bool) turn on unconstrained simplification (see Bruttomesso/Brummayer PhD
thesis)
 nosimplification
 turn off all simplification (same as simplification=none)
 STRINGS THEORY OPTIONS
 stringsabortloop
 (bool) abort when a looping word equation is encountered
 stringsbinarycsp
 (bool) use binary search when splitting strings
 stringscheckentaillen
 (bool) check entailment between length terms to reduce splitting
 stringseager
 (bool) strings eager check
 stringseagerlen
 (bool) strings eager length lemmas
 stringseit
 (bool) the eager intersection used by the theory of strings
 stringsexp
 (bool) experimental features in the theory of strings
 stringsfmf
 (bool) the finite model finding used by the theory of strings
 stringsguessmodel
 (bool) use model guessing to avoid string extended function
reductions
 stringsinferaslemmas
 (bool) always send lemmas out instead of making internal inferences
 stringsinfersym
 (bool) strings split on empty string
 stringsinm
 (bool) internal for strings: ignore negative membership constraints
(fragment checking is needed, left to users for now)
 stringslazypp
 (bool) perform string preprocessing lazily
 stringslb
 (unsigned) the strategy of LB rule application: 0lazy, 1eager, 2no
 stringslengeqz
 (bool) strings length greater than zero lemmas
 stringslennorm
 (bool) strings length normalization lemma
 stringslpropcsp
 (bool) do length propagation based on constant splits
 stringsminprefixexplain
 (bool) minimize explanations for prefix of normal forms in strings
 stringsopt1
 (bool) internal option1 for strings: normal form
 stringsopt2
 (bool) internal option2 for strings: constant regexp splitting
 stringsprintascii
 (bool) the alphabet contains only printable characters from the standard
extended ASCII
 stringsprocessloop
 (bool) reduce looping word equations to regular expressions
 stringsrexplainlemmas
 (bool) regression explanations for string lemmas
 stringsspemp
 (bool) strings split on empty string
 stringsufreduct
 (bool) use uninterpreted functions when applying extended function
reductions
 THEORY LAYER OPTIONS
 assignfunctionvalues
 (bool) assign values for uninterpreted functions in models
 condensefunctionvalues
 (bool) condense values for functions in models rather than explicitly
representing them
 theoryofmode
 (CVC4::theory::TheoryOfMode) mode for Theory::theoryof() (EXPERTS
only)
 usetheory
 (std::string) use alternate theory implementation NAME (usetheory=help
for a list). This option may be repeated or a comma separated list.
 UNINTERPRETED FUNCTIONS THEORY OPTIONS
 ufsymmetrybreaker
 (bool) use UF symmetry breaker (Deharbe et al., CADE 2011)
 ufho
 (bool) enable support for higherorder reasoning
 ufhoext
 (bool) apply extensionality on function symbols
 ufssabortcard
 (int) tells the uf strong solver to only consider models that interpret
uninterpreted sorts of cardinality at most N (1 == no limit,
default)
 ufsscliquesplits
 (bool) use cliques instead of splitting on demand to shrink model
 ufsseagersplit
 (bool) add splits eagerly for uf strong solver
 ufssfair
 (bool) use fair strategy for finite model finding multiple sorts
 ufssfairmonotone
 (bool) group monotone sorts when enforcing fairness for finite model
finding
 ufssregions
 (bool) disable regionbased method for discovering cliques and splits in
uf strong solver
 ufsstotality
 (bool) always use totality axioms for enforcing cardinality
constraints
 ufsstotalitylimited
 (int) apply totality axioms, but only up to cardinality N (1 == do not
apply totality axioms, default)
 ufsstotalitysymbreak
 (bool) apply symmetry breaking for totality axioms
 ufss
 (CVC4::theory::uf::UfssMode) mode of operation for uf strong solver.
This manual page refers to CVC4 version 1.6.
An issue tracker for the CVC4 project is maintained at
https://github.com/CVC4/CVC4/issues.
CVC4 is developed by a team of researchers at Stanford University and the
University of Iowa. See the AUTHORS file in the distribution for a full list
of contributors.
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.stanford.edu/wiki/.
Visit the GSP FreeBSD Man Page Interface. Output converted with ManDoc. 