GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages
SMTENGINE(3cvc) CVC4 Library Interfaces SMTENGINE(3cvc)

SmtEngine - the primary interface to CVC4's theorem-proving 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
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)
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
show-config
(void) show CVC4 static configuration
version
(bool) identify this CVC4 binary
strict-parsing
(bool) be less tolerant of non-conforming inputs
cpu-time
(bool) measures CPU time if set to true and wall time if false (default false)
dump-to
(std::string) all dumping goes to FILE (instead of stdout)
dump
(std::string) dump preprocessed assertions, etc., see --dump=help
hard-limit
(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
produce-assertions
(bool) keep an assertions list (enables get-assertions command)
produce-models
(bool) support the get-value and get-model commands
reproducible-resource-limit
(unsigned long) enable resource limiting per query
rlimit
(unsigned long) enable resource limiting (currently, roughly the number of SAT conflicts)
tlimit-per
(unsigned long) enable time limiting per query (give milliseconds)
tlimit
(unsigned long) enable time limiting (give milliseconds)
ARITHMETIC THEORY OPTIONS
approx-branch-depth
(int16_t) maximum branch depth the approximate solver is allowed to take
arith-no-partial-fun
(bool) do not use partial function semantics for arithmetic (not SMT LIB compliant)
arith-prop-clauses
(uint16_t) rows shorter than this are propagated as clauses
arith-prop
(ArithPropagationMode) turns on arithmetic propagation (default is 'old', see --arith-prop=help)
arith-rewrite-equalities
(bool) turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
collect-pivot-stats
(bool) collect the pivot history
cut-all-bounded
(bool) turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
dio-decomps
(bool) let skolem variables for integer divisibility constraints leak from the dio solver
dio-repeat
(bool) handle dio solver constraints in mass or one at a time
dio-solver
(bool) turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)
dio-turns
(int) turns in a row dio solver cutting gets
error-selection-rule
(ErrorSelectionRule) change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)
fc-penalties
(bool) turns on degenerate pivot penalties
heuristic-pivots
(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
lemmas-on-replay-failure
(bool) attempt to use external lemmas if approximate solve integer failed
maxCutsInContext
(unsigned) maximum cuts in a given context before signalling a restart
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
new-prop
(bool) use the new row propagation system
nl-ext
(bool) extended approach to non-linear
nl-ext-ent-conf
(bool) check for entailed conflicts in non-linear solver
nl-ext-factor
(bool) use factoring inference in non-linear solver
nl-ext-inc-prec
(bool) whether to increment the precision for irrational function constraints
nl-ext-purify
(bool) purify non-linear terms at preprocess
nl-ext-rbound
(bool) use resolution-style inference for inferring new bounds
nl-ext-rewrite
(bool) do rewrites in non-linear solver
nl-ext-split-zero
(bool) intial splits on zero for all variables
nl-ext-tf-taylor-deg
(int16_t) initial degree of polynomials for Taylor approximation
nl-ext-tf-tplanes
(bool) use non-terminating tangent plane strategy for transcendental functions for non-linear
nl-ext-tplanes
(bool) use non-terminating tangent plane strategy for non-linear
nl-ext-tplanes-interleave
(bool) interleave tangent plane strategy for non-linear
pb-rewrites
(bool) apply pseudo boolean rewrites
pivot-threshold
(uint16_t) sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order
pp-assert-max-sub-size
(unsigned) threshold for substituting an equality in ppAssert
prop-row-length
(uint16_t) sets the maximum row length to be used in propagation
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-lemma-reject-cut
(unsigned) maximum complexity of any coefficient while outputting replaying cut lemmas
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-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
restrict-pivots
(bool) have a pivot cap for simplex at effort levels below fullEffort
revert-arith-models-on-unsat
(bool) revert the arithmetic model to a known safe model on unsat if one is cached
rewrite-divk
(bool) rewrite division and mod when by a constant into linear terms
rr-turns
(int) round robin turn
se-solve-int
(bool) attempt to use the approximate solve integer method on standard effort
simplex-check-period
(uint16_t) the number of pivots to do in simplex before rechecking for a conflict on all variables
snorm-infer-eq
(bool) infer equalities based on Shostak normalization
soi-qe
(bool) use quick explain to minimize the sum of infeasibility conflicts
standard-effort-variable-order-pivots
(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)
unate-lemmas
(ArithUnateLemmaMode) determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)
use-approx
(bool) attempt to use an approximate solver
use-fcsimplex
(bool) use focusing and converging simplex (FMCAD 2013 submission)
use-soi
(bool) use sum of infeasibility simplex (FMCAD 2013 submission)
ARRAYS THEORY OPTIONS
arrays-config
(int) set different array option configurations - for developers only
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-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 array solver
arrays-optimize-linear
(bool) turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)
arrays-prop
(int) propagation effort for arrays: 0 is none, 1 is some, 2 is full
arrays-reduce-sharing
(bool) use model information to reduce size of care graph for arrays
arrays-weak-equiv
(bool) use algorithm from Christ/Hoenicke (SMT 2014)
BASE OPTIONS
debug
(std::string) debug something (e.g. -d arith), can repeat
parse-only
(bool) exit after parsing input
preprocess-only
(bool) exit after preprocessing input
print-success
(bool) print the "success" output required of SMT-LIBv2
stats-every-query
(bool) in incremental mode, print stats after every satisfiability or validity query
stats-hide-zeros
(bool) hide statistics which are zero
trace
(std::string) trace something (e.g. -t pushpop), can repeat
verbosity
(int) the verbosity level of CVC4
hide-zero-stats
[undocumented]
language
[undocumented]
no-statistics
[undocumented]
no-statistics-every-query
[undocumented]
output-language
[undocumented]
show-zero-stats
[undocumented]
smtlib-strict
SMT-LIBv2 compliance mode (implies other options)
statistics
[undocumented]
statistics-every-query
[undocumented]
stats-show-zeros
[undocumented]
BITVECTOR THEORY OPTIONS
bitblast-aig
(bool) bitblast by first converting to AIG (implies --bitblast=eager)
bitblast
(CVC4::theory::bv::BitblastMode) choose bitblasting mode, see --bitblast=help
bool-to-bv
(bool) convert booleans to bit-vectors of size 1 when possible
bv-abstraction
(bool) mcm benchmark abstraction (EXPERTS only)
bv-aig-simp
(std::string) abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") (EXPERTS only)
bv-alg-extf
(bool) algebraic inferences for extended functions
bv-algebraic-budget
(unsigned) the budget allowed for the algebraic solver in number of SAT conflicts (EXPERTS only)
bv-algebraic-solver
(bool) turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy)
bv-div-zero-const
(bool) always return -1 on division by zero
bv-eager-explanations
(bool) compute bit-blasting propagation explanations eagerly (EXPERTS only)
bv-eq-slicer
(CVC4::theory::bv::BvSlicerMode) turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)
bv-eq-solver
(bool) use the equality engine for the bit-vector theory (only if --bitblast=lazy)
bv-extract-arith
(bool) enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) (EXPERTS only)
bv-gauss-elim
(bool) simplify formula via Gaussian Elimination if applicable (EXPERTS only)
bv-inequality-solver
(bool) turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)
bv-intro-pow2
(bool) introduce bitvector powers of two as a preprocessing pass (EXPERTS only)
bv-lazy-reduce-extf
(bool) reduce extended functions like bv2nat and int2bv at last call instead of full effort
bv-lazy-rewrite-extf
(bool) lazily rewrite extended functions like bv2nat and int2bv
bv-num-func
(unsigned) number of function symbols in conflicts that are generalized (EXPERTS only)
bv-propagate
(bool) use bit-vector propagation in the bit-blaster
bv-quick-xplain
(bool) minimize bv conflicts using the QuickXplain algorithm (EXPERTS only)
bv-sat-solver
(CVC4::theory::bv::SatSolverMode) choose which sat solver to use, see --bv-sat-solver=help (EXPERTS only)
bv-skolemize
(bool) skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) (EXPERTS only)
bv-to-bool
(bool) lift bit-vectors of size 1 to booleans when possible
DATATYPES THEORY OPTIONS
cdt-bisimilar
(bool) do bisimilarity check for co-datatypes
dt-binary-split
(bool) do binary splits for datatype constructor types
dt-blast-splits
(bool) when applicable, blast splitting lemmas for all variables at once
dt-cyclic
(bool) do cyclicity check for datatypes
dt-force-assignment
(bool) force the datatypes solver to give specific values to all datatypes terms before answering sat
dt-infer-as-lemmas
(bool) always send lemmas out instead of making internal inferences
dt-ref-sk-intro
(bool) introduce reference skolems for shorter explanations
dt-rewrite-error-sel
(bool) rewrite incorrectly applied selectors to arbitrary ground term (EXPERTS only)
dt-share-sel
(bool) internally use shared selectors across multiple constructors
dt-use-testers
(bool) do not preprocess away tester predicates
sygus-abort-size
(int) tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)
sygus-eval-builtin
(bool) use builtin kind for evaluation functions in sygus
sygus-fair-max
(bool) use max instead of sum for multi-function sygus conjectures
sygus-fair
(CVC4::theory::SygusFairMode) if and how to apply fairness for sygus
sygus-opt1
(bool) sygus experimental option
sygus-sym-break
(bool) simple sygus sym break lemmas
sygus-sym-break-dynamic
(bool) dynamic sygus sym break lemmas
sygus-sym-break-lazy
(bool) lazily add symmetry breaking lemmas for terms
sygus-sym-break-pbe
(bool) sygus sym break lemmas based on pbe conjectures
sygus-sym-break-rlv
(bool) add relevancy conditions to symmetry breaking lemmas
DECISION HEURISTICS OPTIONS
decision-random-weight
(int) assign random weights to nodes between 0 and N-1 (0: disable) (EXPERTS only)
decision-threshold
(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-weight-internal
(decision::DecisionWeightInternal) computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) (EXPERTS only)
decision-mode
(decision::DecisionMode) choose decision mode, see --decision=help
EXPRESSION PACKAGE OPTIONS
default-dag-thresh
(int) dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
default-expr-depth
(int) print exprs to depth N (0 == default, -1 == no limit)
eager-type-checking
(bool) type check expressions immediately on creation (debug builds only)
print-expr-types
(bool) print types with variables when printing exprs
type-checking
(bool) never type check expressions
dag-thresh
[undocumented]
dag-threshold
[undocumented]
expr-depth
[undocumented]
no-type-checking
[undocumented]
IDL OPTIONS
idl-rewrite-equalities
(bool) enable rewriting equalities into two inequalities in IDL solver (default is disabled)
DRIVER OPTIONS
continued-execution
(bool) continue executing commands, even on error
early-exit
(bool) do not run destructors at exit; default on except in debug builds (EXPERTS only)
fallback-sequential
(bool) Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode
filter-lemma-length
(int) don't share (among portfolio threads) lemmas strictly longer than N
incremental-parallel
(bool) Use parallel solver even in incremental mode (may print 'unknown's at times)
interactive
(bool) force interactive/non-interactive mode
interactive-prompt
(bool) interactive prompting while in interactive mode
segv-spin
(bool) spin on segfault/other crash waiting for gdb
show-debug-tags
(void) show all available tags for debugging
show-trace-tags
(void) show all available tags for tracing
tear-down-incremental
(int) implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries (EXPERTS only)
thread-stack
(unsigned) stack size for worker threads in MB (0 means use Boost/thread lib default)
threadN
(void) configures portfolio thread N (0..#threads-1)
threads
(unsigned) Total number of threads for portfolio
wait-to-join
(bool) wait for other threads to join before quitting (EXPERTS only)
license
[undocumented]
segv-nospin
[undocumented]
PARSER OPTIONS
filesystem-access
(bool) [undocumented]
global-declarations
(bool) force all declarations and definitions to be global
mmap
(bool) memory map file input
semantic-checks
(bool) disable ALL semantic checks, including type checks
no-checking
[undocumented]
no-include-file
[undocumented]
PRINTING OPTIONS
inst-format
(InstFormatMode) print format mode for instantiations, see --inst-format=help
model-format
(ModelFormatMode) print format mode for models, see --model-format=help
PROOF OPTIONS
aggressive-core-min
(bool) turns on aggressive unsat core minimization (experimental)
allow-empty-dependencies
(bool) if unable to track the dependencies of a rewritten/preprocessed assertion, fail silently
fewer-preprocessing-holes
(bool) try to eliminate preprocessing holes in proofs
lfsc-letification
(bool) turns on global letification in LFSC proofs
SAT LAYER OPTIONS
minisat-dump-dimacs
(bool) instead of solving minisat dumps the asserted clauses in Dimacs format
minisat-elimination
(bool) use Minisat elimination
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
refine-conflicts
(bool) refine theory conflict clauses (default false)
restart-int-base
(unsigned) sets the base restart interval for the sat solver (N=25 by default)
restart-int-inc
(double) sets the restart interval increase factor for the sat solver (F=3.0 by default)
QUANTIFIERS OPTIONS
ag-miniscope-quant
(bool) perform aggressive miniscoping for quantifiers
cbqi
(bool) turns on counterexample-based quantifier instantiation
cbqi-all
(bool) apply counterexample-based instantiation to all quantified formulas
cbqi-bv
(bool) use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors
cbqi-bv-concat-inv
(bool) compute inverse for concat over equalities rather than producing an invertibility condition
cbqi-bv-ineq
(CVC4::theory::quantifiers::CbqiBvIneqMode) choose mode for handling bit-vector inequalities with counterexample-guided instantiation
cbqi-bv-interleave-value
(bool) interleave model value instantiation with word-level inversion approach
cbqi-bv-linear
(bool) linearize adder chains for variables
cbqi-bv-rm-extract
(bool) replaces extract terms with variables for counterexample-guided instantiation for bit-vectors
cbqi-bv-solve-nl
(bool) try to solve non-linear bv literals using model value projections
cbqi-full
(bool) turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation
cbqi-innermost
(bool) only process innermost quantified formulas in counterexample-based quantifier instantiation
cbqi-lit-dep
(bool) dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation
cbqi-midpoint
(bool) choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation
cbqi-min-bounds
(bool) use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
cbqi-model
(bool) guide instantiations by model values for counterexample-based quantifier instantiation
cbqi-multi-inst
(bool) when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation
cbqi-nested-qe
(bool) process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation
cbqi-nopt
(bool) non-optimal bounds for counterexample-based quantifier instantiation
cbqi-prereg-inst
(bool) preregister ground instantiations in counterexample-based quantifier instantiation
cbqi-recurse
(bool) turns on recursive counterexample-based quantifier instantiation
cbqi-repeat-lit
(bool) solve literals more than once in counterexample-based quantifier instantiation
cbqi-round-up-lia
(bool) round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
cbqi-sat
(bool) answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
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
cegis-sample
(CVC4::theory::quantifiers::CegisSampleMode) mode for using samples in the counterexample-guided inductive synthesis loop
cegqi
(bool) counterexample-guided quantifier instantiation for sygus
cegqi-si-abort
(bool) abort if synthesis conjecture is not single invocation
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-reconstruct-const
(bool) include constants when 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
(CVC4::theory::quantifiers::CegqiSingleInvMode) mode for processing single invocation synthesis conjectures
cond-rewrite-quant
(bool) conditional rewriting of quantified formulas
cond-var-split-agg-quant
(bool) aggressive split quantified formulas that lead to variable eliminations
cond-var-split-quant
(bool) split quantified formulas that lead to variable eliminations
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
(bool) generate candidate conjectures for inductive proofs
conjecture-gen-gt-enum
(int) number of ground terms to generate for model filtering
conjecture-gen-max-depth
(int) maximum depth of terms to consider for conjectures
conjecture-gen-per-round
(int) number of conjectures to generate per instantiation round
conjecture-gen-uee-intro
(bool) more aggressive merging for universal equality engine, introduces terms
conjecture-no-filter
(bool) do not filter conjectures
dt-stc-ind
(bool) apply strengthening for existential quantification over datatypes based on structural induction
dt-var-exp-quant
(bool) expand datatype variables bound to one constructor in quantifiers
e-matching
(bool) whether to do heuristic E-matching
elim-ext-arith-quant
(bool) eliminate extended arithmetic symbols in quantified formulas
elim-taut-quant
(bool) eliminate tautological disjuncts of quantified formulas
finite-model-find
(bool) use finite model finding heuristic for quantifier instantiation
fmf-bound
(bool) finite model finding on bounded quantification
fmf-bound-int
(bool) finite model finding on bounded integer quantification
fmf-bound-lazy
(bool) enforce bounds for bounded quantification lazily via use of proxy variables
fmf-bound-min-mode
(CVC4::theory::quantifiers::FmfBoundMinMode) mode for which types of bounds to minimize via first decision heuristics
fmf-empty-sorts
(bool) allow finite model finding to assume sorts that do not occur in ground assertions are empty
fmf-fmc-simple
(bool) simple models in full model check for finite model finding
fmf-fresh-dc
(bool) use fresh distinguished representative when applying Inst-Gen techniques
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-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
fs-interleave
(bool) interleave full saturate instantiation with other techniques
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
global-negate
(bool) do global negation of input formula
ho-matching
(bool) do higher-order matching algorithm for triggers with variable operators
ho-matching-var-priority
(bool) give priority to variable arguments over constant arguments
ho-merge-term-db
(bool) merge term indices modulo equality
increment-triggers
(bool) generate additional triggers as needed during search
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
inst-level-input-only
(bool) only input terms are assigned instantiation level zero
inst-max-level
(int) maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
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
inst-when-phase
(int) instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen
inst-when-strict-interleave
(bool) ensure theory combination and standard quantifier effort strategies take turns
inst-when-tc-first
(bool) allow theory combination to happen once initially, before quantifier strategies are run
inst-when
(CVC4::theory::quantifiers::InstWhenMode) when to apply instantiation
int-wf-ind
(bool) apply strengthening for integers based on well-founded induction
ite-dtt-split-quant
(bool) split ites with dt testers as conditions
ite-lift-quant
(CVC4::theory::quantifiers::IteLiftQuantMode) ite lifting mode for quantified formulas
literal-matching
(CVC4::theory::quantifiers::LiteralMatchMode) choose literal matching mode
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
macros-quant
(bool) perform quantifiers macro expansion
macros-quant-mode
(CVC4::theory::quantifiers::MacrosQuantMode) mode for quantifiers macro expansion
mbqi-interleave
(bool) interleave model-based quantifier instantiation with other techniques
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
mbqi
(CVC4::theory::quantifiers::MbqiMode) choose mode for model-based quantifier instantiation
miniscope-quant
(bool) miniscope quantifiers
miniscope-quant-fv
(bool) miniscope quantifiers for ground subformulas
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
multi-trigger-priority
(bool) only try multi triggers if single triggers give no instantiations
multi-trigger-when-single
(bool) select multi triggers when single triggers exist
partial-triggers
(bool) use triggers that do not contain all free variables
pre-skolem-quant
(bool) apply skolemization eagerly to bodies of quantified formulas
pre-skolem-quant-agg
(bool) apply skolemization to quantified formulas aggressively
pre-skolem-quant-nested
(bool) apply skolemization to nested quantified formulas
prenex-quant-user
(bool) prenex quantified formulas with user patterns
prenex-quant
(CVC4::theory::quantifiers::PrenexQuantMode) prenex mode for quantified formulas
pure-th-triggers
(bool) use pure theory terms as single triggers
purify-dt-triggers
(bool) purify dt triggers, match all constructors of correct form instead of selectors
purify-triggers
(bool) purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1
qcf-all-conflict
(bool) add all available conflicting instances during conflict-based instantiation
qcf-eager-check-rd
(bool) optimization, eagerly check relevant domain of matched position
qcf-eager-test
(bool) optimization, test qcf instances eagerly
qcf-nested-conflict
(bool) consider conflicts for nested quantifiers
qcf-skip-rd
(bool) optimization, skip instances based on possibly irrelevant portions of quantified formulas
qcf-tconstraint
(bool) enable entailment checks for t-constraints in qcf algorithm
qcf-vo-exp
(bool) qcf experimental variable ordering
quant-alpha-equiv
(bool) infer alpha equivalence between quantified formulas
quant-anti-skolem
(bool) perform anti-skolemization for quantified formulas
quant-cf
(bool) enable conflict find mechanism for quantifiers
quant-cf-mode
(CVC4::theory::quantifiers::QcfMode) what effort to apply conflict find mechanism
quant-cf-when
(CVC4::theory::quantifiers::QcfWhenMode) when to invoke conflict find mechanism for quantifiers
quant-dsplit-mode
(CVC4::theory::quantifiers::QuantDSplitMode) mode for dynamic quantifiers splitting
quant-epr
(bool) infer whether in effectively propositional fragment, use for cbqi
quant-epr-match
(bool) use matching heuristics for EPR instantiation
quant-fun-wd
(bool) assume that function defined by quantifiers are well defined
quant-ind
(bool) use all available techniques for inductive reasoning
quant-model-ee
(bool) use equality engine of model for last call effort
quant-rep-mode
(CVC4::theory::quantifiers::QuantRepMode) selection mode for representatives in quantifiers engine
quant-split
(bool) apply splitting to quantified formulas based on variable disjoint disjuncts
register-quant-body-terms
(bool) consider ground terms within bodies of quantified formulas for matching
relational-triggers
(bool) choose relational triggers such as x = f(y), x >= f(y)
relevant-triggers
(bool) prefer triggers that are more relevant based on SInE style analysis
rewrite-rules
(bool) use rewrite rules module
rr-one-inst-per-round
(bool) add one instance of rewrite rule per round
strict-triggers
(bool) only instantiate quantifiers with user patterns based on triggers
sygus-add-const-grammar
(bool) statically add constants appearing in conjecture to grammars
sygus-auto-unfold
(bool) enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems
sygus-bool-ite-return-const
(bool) Only use Boolean constants for return values in unification-based function synthesis
sygus-eval-unfold
(bool) do unfolding of sygus evaluation functions
sygus-eval-unfold-bool
(bool) do unfolding of Boolean evaluation functions that appear in refinement lemmas
sygus-ext-rew
(bool) use extended rewriter for sygus
sygus-grammar-norm
(bool) statically normalize sygus grammars based on flattening (linearization)
sygus-inference
(bool) attempt to preprocess arbitrary inputs to sygus conjectures
sygus-inv-templ-when-sg
(bool) use invariant templates (with solution reconstruction) for syntax guided problems
sygus-inv-templ
(CVC4::theory::quantifiers::SygusInvTemplMode) template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)
sygus-min-grammar
(bool) statically minimize sygus grammars
sygus-pbe
(bool) enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures
sygus-qe-preproc
(bool) use quantifier elimination as a preprocessing step for sygus
sygus-ref-eval
(bool) direct evaluation of refinement lemmas for conflict analysis
sygus-repair-const
(bool) use approach to repair constants in sygus candidate solutions
sygus-rr
(bool) use sygus to enumerate and verify correctness of rewrite rules via sampling
sygus-rr-synth
(bool) use sygus to enumerate candidate rewrite rules via sampling
sygus-rr-synth-accel
(bool) add dynamic symmetry breaking clauses based on candidate rewrites
sygus-rr-synth-check
(bool) use satisfiability check to verify correctness of candidate rewrites
sygus-rr-synth-filter-cong
(bool) filter candidate rewrites based on congruence
sygus-rr-synth-filter-match
(bool) filter candidate rewrites based on matching
sygus-rr-synth-filter-order
(bool) filter candidate rewrites based on variable ordering
sygus-rr-verify
(bool) use sygus to verify the correctness of rewrite rules via sampling
sygus-rr-verify-abort
(bool) abort when sygus-rr-verify finds an instance of unsoundness
sygus-sample-grammar
(bool) when applicable, use grammar for choosing sample points
sygus-samples
(int) number of points to consider when doing sygus rewriter sample testing
sygus-stream
(bool) enumerate a stream of solutions instead of terminating after the first one
sygus-templ-embed-grammar
(bool) embed sygus templates into grammars
sygus-unif
(bool) Unification-based function synthesis
term-db-mode
(CVC4::theory::quantifiers::TermDbMode) which ground terms to consider for instantiation
track-inst-lemmas
(bool) track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)
trigger-active-sel
(CVC4::theory::quantifiers::TriggerActiveSelMode) selection mode to activate triggers
trigger-sel
(CVC4::theory::quantifiers::TriggerSelMode) selection mode for triggers
user-pat
(CVC4::theory::quantifiers::UserPatMode) policy for handling user-provided patterns for quantifier instantiation
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
SEP OPTIONS
sep-check-neg
(bool) check negated spatial assertions
sep-child-refine
(bool) child-specific refinements of negated star, positive wand
sep-deq-c
(bool) assume cardinality elements are distinct
sep-exp
(bool) experimental flag for sep
sep-min-refine
(bool) only add refinement lemmas for minimal (innermost) assertions
sep-pre-skolem-emp
(bool) eliminate emp constraint at preprocess time
SETS OPTIONS
sets-ext
(bool) enable extended symbols such as complement and universe in theory of sets
sets-infer-as-lemmas
(bool) send inferences as lemmas
sets-proxy-lemmas
(bool) introduce proxy variables eagerly to shorten lemmas
sets-rel-eager
(bool) standard effort checks for relations
SMT LAYER OPTIONS
abstract-values
(bool) in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
bitblast-step
(unsigned) amount of resources spent for each bitblast step (EXPERTS only)
bv-sat-conflict-step
(unsigned) amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)
check-models
(bool) after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
check-proofs
(bool) after UNSAT/VALID, machine-check the generated proof
check-synth-sol
(bool) checks whether produced solutions to functions-to-synthesize satisfy the conjecture
check-unsat-cores
(bool) after UNSAT/VALID, produce and check an unsat core (expensive)
cnf-step
(unsigned) amount of resources spent for each call to cnf conversion (EXPERTS only)
decision-step
(unsigned) amount of getNext decision calls in the decision engine (EXPERTS only)
diagnostic-output-channel
(std::string) set the diagnostic output channel of the solver
dump-instantiations
(bool) output instantiations of quantified formulas after every UNSAT/VALID response
dump-models
(bool) output models after every SAT/INVALID/UNKNOWN response
dump-proofs
(bool) output proofs after every UNSAT/VALID response
dump-synth
(bool) output solution for synthesis conjectures after every UNSAT/VALID response
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
expand-definitions
(bool) always expand symbol definitions in output
ext-rew-prep
(bool) use extended rewriter as a preprocessing pass
ext-rew-prep-agg
(bool) use aggressive extended rewriter as a preprocessing pass
force-logic
(std::string) set the logic, and override all further user attempts to change it (EXPERTS only)
force-no-limit-cpu-while-dump
(bool) Force no CPU limit when dumping models and proofs
interactive-mode
(bool) deprecated name for produce-assertions
ite-simp
(bool) turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
lemma-step
(unsigned) amount of resources spent when adding lemmas (EXPERTS only)
model-u-dt-enum
(bool) in models, output uninterpreted sorts as datatype enumerations
omit-dont-cares
(bool) When producing a model, omit variables whose value does not matter
on-repeat-ite-simp
(bool) do the ite simplification pass again if repeating simplification
parse-step
(unsigned) amount of resources spent for each command/expression parsing (EXPERTS only)
preprocess-step
(unsigned) amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)
produce-assignments
(bool) support the get-assignment command
produce-unsat-assumptions
(bool) turn on unsat assumptions generation
produce-unsat-cores
(bool) turn on unsat core generation
produce-proofs
(bool) turn on proof generation
quantifier-step
(unsigned) amount of resources spent for quantifier instantiations (EXPERTS only)
regular-output-channel
(std::string) set the regular output channel of the solver
repeat-simp
(bool) make multiple passes with nonclausal simplifier
replay-log
(std::string) replay decisions from file
replay
(std::string) replay decisions from file
restart-step
(unsigned) amount of resources spent for each theory restart (EXPERTS only)
rewrite-apply-to-const
(bool) eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 (EXPERTS only)
rewrite-step
(unsigned) amount of resources spent for each rewrite step (EXPERTS only)
sat-conflict-step
(unsigned) amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)
simp-ite-compress
(bool) enables compressing ites after ite simplification
simp-ite-hunt-zombies
(uint32_t) post ite compression enables zombie removal while the number of nodes is above this threshold
simp-with-care
(bool) enables simplifyWithCare in ite simplificiation
simplification-mode
(SimplificationMode) choose simplification mode, see --simplification=help
solve-int-as-bv
(uint32_t) attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)
solve-real-as-int
(bool) attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)
sort-inference
(bool) calculate sort inference of input problem, convert the input based on monotonic sorts
static-learning
(bool) use static learning (on by default)
sygus-out
(SygusSolutionOutMode) output mode for sygus
sygus-print-callbacks
(bool) use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)
symmetry-breaker-exp
(bool) generate symmetry breaking constraints after symmetry detection
theory-check-step
(unsigned) amount of resources spent for each theory check call (EXPERTS only)
unconstrained-simp
(bool) turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
no-simplification
turn off all simplification (same as --simplification=none)
STRINGS THEORY OPTIONS
strings-abort-loop
(bool) abort when a looping word equation is encountered
strings-binary-csp
(bool) use binary search when splitting strings
strings-check-entail-len
(bool) check entailment between length terms to reduce splitting
strings-eager
(bool) strings eager check
strings-eager-len
(bool) strings eager length lemmas
strings-eit
(bool) the eager intersection used by the theory of strings
strings-exp
(bool) experimental features in the theory of strings
strings-fmf
(bool) the finite model finding used by the theory of strings
strings-guess-model
(bool) use model guessing to avoid string extended function reductions
strings-infer-as-lemmas
(bool) always send lemmas out instead of making internal inferences
strings-infer-sym
(bool) strings split on empty string
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-lb
(unsigned) the strategy of LB rule application: 0-lazy, 1-eager, 2-no
strings-len-geqz
(bool) strings length greater than zero lemmas
strings-len-norm
(bool) strings length normalization lemma
strings-lprop-csp
(bool) do length propagation based on constant splits
strings-min-prefix-explain
(bool) minimize explanations for prefix of normal forms in strings
strings-opt1
(bool) internal option1 for strings: normal form
strings-opt2
(bool) internal option2 for strings: constant regexp splitting
strings-print-ascii
(bool) the alphabet contains only printable characters from the standard extended ASCII
strings-process-loop
(bool) reduce looping word equations to regular expressions
strings-rexplain-lemmas
(bool) regression explanations for string lemmas
strings-sp-emp
(bool) strings split on empty string
strings-uf-reduct
(bool) use uninterpreted functions when applying extended function reductions
THEORY LAYER OPTIONS
assign-function-values
(bool) assign values for uninterpreted functions in models
condense-function-values
(bool) condense values for functions in models rather than explicitly representing them
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)
uf-ho
(bool) enable support for higher-order reasoning
uf-ho-ext
(bool) apply extensionality on function symbols
uf-ss-abort-card
(int) tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)
uf-ss-clique-splits
(bool) use cliques instead of splitting on demand to shrink model
uf-ss-eager-split
(bool) add splits eagerly for uf strong solver
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
uf-ss-regions
(bool) disable region-based method for discovering cliques and splits in uf strong solver
uf-ss-totality
(bool) always use totality axioms for enforcing cardinality constraints
uf-ss-totality-limited
(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
(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/.
January 2019 CVC4 release 1.6

Search for    or go to Top of page |  Section other |  Main Index

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with ManDoc.