options.3cvc man page

options — the options infrastructure

Available Internal Options

COMMON OPTIONS
inputLanguage

(InputLanguage, default = language::input::LANG_AUTO)
force input language (default is "auto"; see --lang help)

outputLanguage

(OutputLanguage, default = language::output::LANG_AUTO)
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

strictParsing

(bool)
be less tolerant of non-conforming inputs

dumpModeString

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

dumpToFileName

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

produceModels

(bool, default = false)
support the get-value and get-model commands

produceAssertions

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

incrementalSolving

(bool, default = true)
enable incremental solving

cumulativeMillisecondLimit

(unsigned long)
enable time limiting (give milliseconds)

perCallMillisecondLimit

(unsigned long)
enable time limiting per query (give milliseconds)

cumulativeResourceLimit

(unsigned long)
enable resource limiting (currently, roughly the number of SAT conflicts)

perCallResourceLimit

(unsigned long)
enable resource limiting per query

hardLimit

(bool, default = false)
the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)

cpuTime

(bool, default = false)
measures CPU time if set to true and wall time if false (default false)

ARITHMETIC THEORY OPTIONS
arithUnateLemmaMode

(ArithUnateLemmaMode, default = ALL_PRESOLVE_LEMMAS)
determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)

arithPropagationMode

(ArithPropagationMode, default = BOTH_PROP)
turns on arithmetic propagation (default is 'old', see --arith-prop=help)

arithHeuristicPivots

(int16_t, default = 0)
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

arithStandardCheckVarOrderPivots

(int16_t, default = -1)
limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule (EXPERTS only)

arithErrorSelectionRule

(ErrorSelectionRule, default = MINIMUM_AMOUNT)
change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)

arithSimplexCheckPeriod

(uint16_t, default = 200)
the number of pivots to do in simplex before rechecking for a conflict on all variables

arithPivotThreshold

(uint16_t, default = 2)
sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order

arithPropagateMaxLength

(uint16_t, default = 16)
sets the maximum row length to be used in propagation

arithDioSolver

(bool, default = true)
turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)

arithRewriteEq

(bool, default = false)
turns on the preprocessing rewrite turning equalities into a conjunction of inequalities

arithMLTrick

(bool, default = false)
turns on the preprocessing step of attempting to infer bounds on miplib problems

arithMLTrickSubstitutions

(unsigned, default = 1)
do substitution for miplib 'tmp' vars if defined in <= N eliminated vars

doCutAllBounded

(bool, default = false)
turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds

maxCutsInContext

(unsigned, default = 65535)
maximum cuts in a given context before signalling a restart

revertArithModels

(bool, default = false)
revert the arithmetic model to a known safe model on unsat if one is cached

havePenalties

(bool, default = false)
turns on degenerate pivot penalties

useFC

(bool, default = false)
use focusing and converging simplex (FMCAD 2013 submission)

useSOI

(bool, default = false)
use sum of infeasibility simplex (FMCAD 2013 submission)

restrictedPivots

(bool, default = true)
have a pivot cap for simplex at effort levels below fullEffort

collectPivots

(bool, default = false)
collect the pivot history

useApprox

(bool, default = false)
attempt to use an approximate solver

maxApproxDepth

(int16_t, default = 200)
maximum branch depth the approximate solver is allowed to take

exportDioDecompositions

(bool, default = false)
let skolem variables for integer divisibility constraints leak from the dio solver

newProp

(bool, default = false)
use the new row propagation system

arithPropAsLemmaLength

(uint16_t, default = 8)
rows shorter than this are propagated as clauses

soiQuickExplain

(bool, default = false)
use quick explain to minimize the sum of infeasibility conflicts

rewriteDivk

(bool, default = false)
rewrite division and mod when by a constant into linear terms

trySolveIntStandardEffort

(bool, default = false)
attempt to use the approximate solve integer method on standard effort

replayFailureLemma

(bool, default = false)
attempt to use external lemmas if approximate solve integer failed

dioSolverTurns

(int, default = 10)
turns in a row dio solver cutting gets

rrTurns

(int, default = 3)
round robin turn

dioRepeat

(bool, default = false)
handle dio solver constraints in mass or one at a time

replayEarlyCloseDepths

(int, default = 1)
multiples of the depths to try to close the approx log eagerly

replayFailurePenalty

(int, default = 100)
number of solve integer attempts to skips after a numeric failure

replayNumericFailurePenalty

(int, default = 4194304)
number of solve integer attempts to skips after a numeric failure

replayRejectCutSize

(unsigned, default = 25500)
maximum complexity of any coefficient while replaying cuts

lemmaRejectCutSize

(unsigned, default = 25500)
maximum complexity of any coefficient while outputting replaying cut lemmas

soiApproxMajorFailure

(double, default = .01)
threshold for a major tolerance failure by the approximate solver

soiApproxMajorFailurePen

(int, default = 50)
threshold for a major tolerance failure by the approximate solver

soiApproxMinorFailure

(double, default = .0001)
threshold for a minor tolerance failure by the approximate solver

soiApproxMinorFailurePen

(int, default = 10)
threshold for a minor tolerance failure by the approximate solver

ppAssertMaxSubSize

(unsigned, default = 2)
threshold for substituting an equality in ppAssert

maxReplayTree

(int, default = 512)
threshold for attempting to replay a tree

pbRewrites

(bool, default = false)
apply pseudo boolean rewrites

pbRewriteThreshold

(int, default = 256)
threshold of number of pseudoboolean variables to have before doing rewrites

sNormInferEq

(bool, default = false)
infer equalities based on Shostak normalization

nlExt

(bool, default = true)
extended approach to non-linear

nlExtResBound

(bool, default = false)
use resolution-style inference for inferring new bounds

nlExtTangentPlanes

(bool, default = false)
use non-terminating tangent plane strategy for non-linear

nlExtEntailConflicts

(bool, default = false)
check for entailed conflicts in non-linear solver

nlExtRewrites

(bool, default = true)
do rewrites in non-linear solver

nlExtSolveSubs

(bool, default = false)
do solving for determining constant substitutions

nlExtPurify

(bool, default = false)
purify non-linear terms at preprocess

nlExtSplitZero

(bool, default = false)
intial splits on zero for all variables

ARRAYS THEORY OPTIONS
arraysOptimizeLinear

(bool, default = true)
turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)

arraysLazyRIntro1

(bool, default = true)
turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)

arraysWeakEquivalence

(bool, default = false)
use algorithm from Christ/Hoenicke (SMT 2014)

arraysModelBased

(bool, default = false)
turn on model-based array solver

arraysEagerIndexSplitting

(bool, default = true)
turn on eager index splitting for generated array lemmas

arraysEagerLemmas

(bool, default = false)
turn on eager lemma generation for arrays

arraysConfig

(int, default = 0)
set different array option configurations - for developers only

arraysReduceSharing

(bool, default = false)
use model information to reduce size of care graph for arrays

arraysPropagate

(int, default = 2)
propagation effort for arrays: 0 is none, 1 is some, 2 is full

BASE OPTIONS
binary_name

(std::string)
[undocumented]

in

(std::istream*, default = &std::cin)
[undocumented]

out

(std::ostream*, default = &std::cout)
[undocumented]

err

(std::ostream*, default = &std::cerr)
[undocumented]

languageHelp

(bool)
[undocumented]

verbosity

(int, default = 0)
the verbosity level of CVC4

statsEveryQuery

(bool, default = false)
in incremental mode, print stats after every satisfiability or validity query

statsHideZeros

(bool, default = false)
hide statistics which are zero

parseOnly

(bool)
exit after parsing input

preprocessOnly

(bool)
exit after preprocessing input

printSuccess

(bool)
print the "success" output required of SMT-LIBv2

BITVECTOR THEORY OPTIONS
bvSatSolver

(CVC4::theory::bv::SatSolverMode, default = CVC4::theory::bv::SAT_SOLVER_MINISAT)
choose which sat solver to use, see --bv-sat-solver=help (EXPERTS only)

bitblastMode

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

bitvectorAig

(bool, default = false)
bitblast by first converting to AIG (implies --bitblast=eager)

bitvectorAigSimplifications

(std::string)
abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") (EXPERTS only)

bitvectorPropagate

(bool, default = true)
use bit-vector propagation in the bit-blaster

bitvectorEqualitySolver

(bool, default = true)
use the equality engine for the bit-vector theory (only if --bitblast=lazy)

bitvectorEqualitySlicer

(CVC4::theory::bv::BvSlicerMode, default = CVC4::theory::bv::BITVECTOR_SLICER_OFF)
turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)

bitvectorInequalitySolver

(bool, default = true)
turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)

bitvectorAlgebraicSolver

(bool, default = true)
turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy)

bitvectorAlgebraicBudget

(unsigned, default = 1500)
the budget allowed for the algebraic solver in number of SAT conflicts (EXPERTS only)

bitvectorToBool

(bool, default = false)
lift bit-vectors of size 1 to booleans when possible

boolToBitvector

(bool, default = false)
convert booleans to bit-vectors of size 1 when possible

bitvectorDivByZeroConst

(bool, default = false)
always return -1 on division by zero

bvExtractArithRewrite

(bool, default = false)
enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) (EXPERTS only)

bvAbstraction

(bool, default = false)
mcm benchmark abstraction (EXPERTS only)

skolemizeArguments

(bool, default = false)
skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) (EXPERTS only)

bvNumFunc

(unsigned, default = 1)
number of function symbols in conflicts that are generalized (EXPERTS only)

bvEagerExplanations

(bool, default = false)
compute bit-blasting propagation explanations eagerly (EXPERTS only)

bitvectorQuickXplain

(bool, default = false)
minimize bv conflicts using the QuickXplain algorithm (EXPERTS only)

bvIntroducePow2

(bool, default = false)
introduce bitvector powers of two as a preprocessing pass (EXPERTS only)

bvLazyRewriteExtf

(bool, default = true)
lazily rewrite extended functions like bv2nat and int2bv

bvLazyReduceExtf

(bool, default = false)
reduce extended functions like bv2nat and int2bv at last call instead of full effort

bvAlgExtf

(bool, default = true)
algebraic inferences for extended functions

DATATYPES THEORY OPTIONS
dtRewriteErrorSel

(bool, default = false)
rewrite incorrectly applied selectors to arbitrary ground term (EXPERTS only)

dtForceAssignment

(bool, default = false)
force the datatypes solver to give specific values to all datatypes terms before answering sat

dtBinarySplit

(bool, default = false)
do binary splits for datatype constructor types

dtRefIntro

(bool, default = false)
introduce reference skolems for shorter explanations

dtUseTesters

(bool, default = true)
do not preprocess away tester predicates

cdtBisimilar

(bool, default = true)
do bisimilarity check for co-datatypes

dtCyclic

(bool, default = true)
do cyclicity check for datatypes

dtInferAsLemmas

(bool, default = false)
always send lemmas out instead of making internal inferences

dtBlastSplits

(bool, default = false)
when applicable, blast splitting lemmas for all variables at once

DECISION HEURISTICS OPTIONS
decisionMode

(decision::DecisionMode, default = decision::DECISION_STRATEGY_INTERNAL)
choose decision mode, see --decision=help

decisionStopOnly

(bool)
[undocumented]

decisionThreshold

(decision::DecisionWeight, default = 0)
ignore all nodes greater than threshold in first attempt to pick decision (EXPERTS only)

decisionUseWeight

(bool, default = false)
use the weight nodes (locally, by looking at children) to direct recursive search (EXPERTS only)

decisionRandomWeight

(int, default = 0)
assign random weights to nodes between 0 and N-1 (0: disable) (EXPERTS only)

decisionWeightInternal

(decision::DecisionWeightInternal, default = decision::DECISION_WEIGHT_INTERNAL_OFF)
computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) (EXPERTS only)

EXPRESSION PACKAGE OPTIONS
defaultExprDepth

(int, default = 0)
print exprs to depth N (0 == default, -1 == no limit)

defaultDagThresh

(int, default = 1)
dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)

printExprTypes

(bool, default = false)
print types with variables when printing exprs

earlyTypeChecking

(bool, default = USE_EARLY_TYPE_CHECKING_BY_DEFAULT)
type check expressions immediately on creation (debug builds only)

typeChecking

(bool, default = DO_SEMANTIC_CHECKS_BY_DEFAULT)
never type check expressions

IDL OPTIONS
idlRewriteEq

(bool, default = false)
enable rewriting equalities into two inequalities in IDL solver (default is disabled)

DRIVER OPTIONS
earlyExit

(bool, default = true)
do not run destructors at exit; default on except in debug builds (EXPERTS only)

threads

(unsigned, default = 2)
Total number of threads for portfolio

threadStackSize

(unsigned, default = 0)
stack size for worker threads in MB (0 means use Boost/thread lib default)

threadArgv

(std::vector<std::string>)
Thread configuration (a string to be passed to parseOptions)

thread_id

(int, default = -1)
Thread ID, for internal use in case of multi-threaded run

sharingFilterByLength

(int, default = -1)
don't share (among portfolio threads) lemmas strictly longer than N

fallbackSequential

(bool, default = false)
Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode

incrementalParallel

(bool, default = false)
Use parallel solver even in incremental mode (may print 'unknown's at times)

interactive

(bool)
force interactive/non-interactive mode

interactivePrompt

(bool, default = true)
interactive prompting while in interactive mode

continuedExecution

(bool, default = false)
continue executing commands, even on error

segvSpin

(bool, default = false)
spin on segfault/other crash waiting for gdb

tearDownIncremental

(int, default = 0)
implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries (EXPERTS only)

waitToJoin

(bool, default = true)
wait for other threads to join before quitting (EXPERTS only)

PARSER OPTIONS
memoryMap

(bool)
memory map file input

semanticChecks

(bool, default = DO_SEMANTIC_CHECKS_BY_DEFAULT)
disable ALL semantic checks, including type checks

globalDeclarations

(bool, default = false)
force all declarations and definitions to be global

filesystemAccess

(bool, default = true)
[undocumented]

PRINTING OPTIONS
modelFormatMode

(ModelFormatMode, default = MODEL_FORMAT_MODE_DEFAULT)
print format mode for models, see --model-format=help

instFormatMode

(InstFormatMode, default = INST_FORMAT_MODE_DEFAULT)
print format mode for instantiations, see --inst-format=help

PROOF OPTIONS
lfscLetification

(bool, default = true)
turns on global letification in LFSC proofs

aggressiveCoreMin

(bool, default = false)
turns on aggressive unsat core minimization (experimental)

fewerPreprocessingHoles

(bool, default = false)
try to eliminate preprocessing holes in proofs

allowEmptyDependencies

(bool, default = false)
if unable to track the dependencies of a rewritten/preprocessed assertion, fail silently

SAT LAYER OPTIONS
satRandomFreq

(double, default = 0.0)
sets the frequency of random decisions in the sat solver (P=0.0 by default)

satRandomSeed

(uint32_t, default = 0)
sets the random seed for the sat solver

satVarDecay

(double, default = 0.95)
variable activity decay factor for Minisat

satClauseDecay

(double, default = 0.999)
clause activity decay factor for Minisat

satRestartFirst

(unsigned, default = 25)
sets the base restart interval for the sat solver (N=25 by default)

satRestartInc

(double, default = 3.0)
sets the restart interval increase factor for the sat solver (F=3.0 by default)

sat_refine_conflicts

(bool, default = false)
refine theory conflict clauses (default false)

minisatUseElim

(bool, default = true)
use Minisat elimination

minisatDumpDimacs

(bool, default = false)
instead of solving minisat dumps the asserted clauses in Dimacs format

QUANTIFIERS OPTIONS
miniscopeQuant

(bool, default = true)
miniscope quantifiers

miniscopeQuantFreeVar

(bool, default = true)
miniscope quantifiers for ground subformulas

quantSplit

(bool, default = true)
apply splitting to quantified formulas based on variable disjoint disjuncts

prenexQuant

(CVC4::theory::quantifiers::PrenexQuantMode, default = CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE)
prenex mode for quantified formulas

prenexQuantUser

(bool, default = false)
prenex quantified formulas with user patterns

varElimQuant

(bool, default = true)
enable simple variable elimination for quantified formulas

varIneqElimQuant

(bool, default = true)
enable variable elimination based on infinite projection of unbound arithmetic variables

dtVarExpandQuant

(bool, default = true)
expand datatype variables bound to one constructor in quantifiers

iteLiftQuant

(CVC4::theory::quantifiers::IteLiftQuantMode, default = CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE)
ite lifting mode for quantified formulas

condVarSplitQuant

(bool, default = true)
split quantified formulas that lead to variable eliminations

condVarSplitQuantAgg

(bool, default = false)
aggressive split quantified formulas that lead to variable eliminations

iteDtTesterSplitQuant

(bool, default = false)
split ites with dt testers as conditions

preSkolemQuant

(bool, default = false)
apply skolemization eagerly to bodies of quantified formulas

preSkolemQuantNested

(bool, default = true)
apply skolemization to nested quantified formulas

preSkolemQuantAgg

(bool, default = true)
apply skolemization to quantified formulas aggressively

aggressiveMiniscopeQuant

(bool, default = false)
perform aggressive miniscoping for quantifiers

elimTautQuant

(bool, default = true)
eliminate tautological disjuncts of quantified formulas

elimExtArithQuant

(bool, default = true)
eliminate extended arithmetic symbols in quantified formulas

condRewriteQuant

(bool, default = true)
conditional rewriting of quantified formulas

eMatching

(bool, default = true)
whether to do heuristic E-matching

termDbMode

(CVC4::theory::quantifiers::TermDbMode, default = CVC4::theory::quantifiers::TERM_DB_ALL)
which ground terms to consider for instantiation

registerQuantBodyTerms

(bool, default = false)
consider ground terms within bodies of quantified formulas for matching

inferArithTriggerEq

(bool, default = false)
infer equalities for trigger terms based on solving arithmetic equalities

inferArithTriggerEqExp

(bool, default = false)
record explanations for inferArithTriggerEq

strictTriggers

(bool, default = false)
only instantiate quantifiers with user patterns based on triggers

relevantTriggers

(bool, default = false)
prefer triggers that are more relevant based on SInE style analysis

relationalTriggers

(bool, default = false)
choose relational triggers such as x = f(y), x >= f(y)

purifyTriggers

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

purifyDtTriggers

(bool, default = false)
purify dt triggers, match all constructors of correct form instead of selectors

pureThTriggers

(bool, default = false)
use pure theory terms as single triggers

partialTriggers

(bool, default = false)
use triggers that do not contain all free variables

multiTriggerWhenSingle

(bool, default = false)
select multi triggers when single triggers exist

multiTriggerPriority

(bool, default = false)
only try multi triggers if single triggers give no instantiations

multiTriggerCache

(bool, default = false)
caching version of multi triggers

multiTriggerLinear

(bool, default = true)
implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms

triggerSelMode

(CVC4::theory::quantifiers::TriggerSelMode, default = CVC4::theory::quantifiers::TRIGGER_SEL_MIN)
selection mode for triggers

triggerActiveSelMode

(CVC4::theory::quantifiers::TriggerActiveSelMode, default = CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL)
selection mode to activate triggers

userPatternsQuant

(CVC4::theory::quantifiers::UserPatMode, default = CVC4::theory::quantifiers::USER_PAT_MODE_TRUST)
policy for handling user-provided patterns for quantifier instantiation

incrementTriggers

(bool, default = true)
generate additional triggers as needed during search

instWhenMode

(CVC4::theory::quantifiers::InstWhenMode, default = CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL)
when to apply instantiation

instWhenStrictInterleave

(bool, default = true)
ensure theory combination and standard quantifier effort strategies take turns

instWhenPhase

(int, default = 2)
instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen

instWhenTcFirst

(bool, default = true)
allow theory combination to happen once initially, before quantifier strategies are run

quantModelEe

(bool, default = false)
use equality engine of model for last call effort

instMaxLevel

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

instLevelInputOnly

(bool, default = true)
only input terms are assigned instantiation level zero

quantRepMode

(CVC4::theory::quantifiers::QuantRepMode, default = CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST)
selection mode for representatives in quantifiers engine

instRelevantCond

(bool, default = false)
add relevancy conditions for instantiations

fullSaturateQuant

(bool, default = false)
when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown

fullSaturateQuantRd

(bool, default = true)
whether to use relevant domain first for full saturation instantiation strategy

fullSaturateInst

(bool, default = false)
interleave full saturate instantiation with other techniques

literalMatchMode

(CVC4::theory::quantifiers::LiteralMatchMode, default = CVC4::theory::quantifiers::LITERAL_MATCH_USE)
choose literal matching mode

finiteModelFind

(bool, default = false)
use finite model finding heuristic for quantifier instantiation

quantFunWellDefined

(bool, default = false)
assume that function defined by quantifiers are well defined

fmfFunWellDefined

(bool, default = false)
find models for recursively defined functions, assumes functions are admissible

fmfFunWellDefinedRelevant

(bool, default = false)
find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant

fmfEmptySorts

(bool, default = false)
allow finite model finding to assume sorts that do not occur in ground assertions are empty

mbqiMode

(CVC4::theory::quantifiers::MbqiMode, default = CVC4::theory::quantifiers::MBQI_FMC)
choose mode for model-based quantifier instantiation

fmfOneInstPerRound

(bool, default = false)
only add one instantiation per quantifier per round for mbqi

fmfOneQuantPerRound

(bool, default = false)
only add instantiations for one quantifier per round for mbqi

fmfInstEngine

(bool, default = false)
use instantiation engine in conjunction with finite model finding

fmfInstGen

(bool, default = true)
enable Inst-Gen instantiation techniques for finite model finding

fmfInstGenOneQuantPerRound

(bool, default = false)
only perform Inst-Gen instantiation techniques on one quantifier per round

fmfFreshDistConst

(bool, default = false)
use fresh distinguished representative when applying Inst-Gen techniques

fmfFmcSimple

(bool, default = true)
simple models in full model check for finite model finding

fmfBoundInt

(bool, default = false)
finite model finding on bounded integer quantification

fmfBound

(bool, default = false)
finite model finding on bounded quantification

fmfBoundLazy

(bool, default = false)
enforce bounds for bounded quantification lazily via use of proxy variables

fmfBoundMinMode

(CVC4::theory::quantifiers::FmfBoundMinMode, default = CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE)
mode for which types of bounds to minimize via first decision heuristics

quantConflictFind

(bool, default = true)
enable conflict find mechanism for quantifiers

qcfMode

(CVC4::theory::quantifiers::QcfMode, default = CVC4::theory::quantifiers::QCF_PROP_EQ)
what effort to apply conflict find mechanism

qcfWhenMode

(CVC4::theory::quantifiers::QcfWhenMode, default = CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT)
when to invoke conflict find mechanism for quantifiers

qcfTConstraint

(bool, default = false)
enable entailment checks for t-constraints in qcf algorithm

qcfAllConflict

(bool, default = false)
add all available conflicting instances during conflict-based instantiation

qcfNestedConflict

(bool, default = false)
consider conflicts for nested quantifiers

qcfVoExp

(bool, default = false)
qcf experimental variable ordering

instNoEntail

(bool, default = true)
do not consider instances of quantified formulas that are currently entailed

instNoModelTrue

(bool, default = false)
do not consider instances of quantified formulas that are currently true in model, if it is available

instPropagate

(bool, default = false)
internal propagation for instantiations for selecting relevant instances

qcfEagerTest

(bool, default = true)
optimization, test qcf instances eagerly

qcfEagerCheckRd

(bool, default = true)
optimization, eagerly check relevant domain of matched position

qcfSkipRd

(bool, default = false)
optimization, skip instances based on possibly irrelevant portions of quantified formulas

quantRewriteRules

(bool, default = false)
use rewrite rules module

rrOneInstPerRound

(bool, default = false)
add one instance of rewrite rule per round

quantInduction

(bool, default = false)
use all available techniques for inductive reasoning

dtStcInduction

(bool, default = false)
apply strengthening for existential quantification over datatypes based on structural induction

intWfInduction

(bool, default = false)
apply strengthening for integers based on well-founded induction

conjectureGen

(bool, default = false)
generate candidate conjectures for inductive proofs

conjectureGenPerRound

(int, default = 1)
number of conjectures to generate per instantiation round

conjectureNoFilter

(bool, default = false)
do not filter conjectures

conjectureFilterActiveTerms

(bool, default = true)
filter based on active terms

conjectureFilterCanonical

(bool, default = true)
filter based on canonicity

conjectureFilterModel

(bool, default = true)
filter based on model

conjectureGenGtEnum

(int, default = 50)
number of ground terms to generate for model filtering

conjectureUeeIntro

(bool, default = false)
more aggressive merging for universal equality engine, introduces terms

conjectureGenMaxDepth

(int, default = 3)
maximum depth of terms to consider for conjectures

ceGuidedInst

(bool, default = false)
counterexample-guided quantifier instantiation

ceGuidedInstFair

(CVC4::theory::quantifiers::CegqiFairMode, default = CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE)
if and how to apply fairness for cegqi

cegqiSingleInvMode

(CVC4::theory::quantifiers::CegqiSingleInvMode, default = CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE)
mode for processing single invocation synthesis conjectures

cegqiSingleInvPartial

(bool, default = false)
combined techniques for synthesis conjectures that are partially single invocation

cegqiSingleInvReconstruct

(bool, default = true)
reconstruct solutions for single invocation conjectures in original grammar

cegqiSolMinCore

(bool, default = false)
minimize solutions for single invocation conjectures based on unsat core

cegqiSolMinInst

(bool, default = true)
minimize individual instantiations for single invocation conjectures based on unsat core

cegqiSingleInvReconstructConst

(bool, default = true)
include constants when reconstruct solutions for single invocation conjectures in original grammar

cegqiSingleInvAbort

(bool, default = false)
abort if synthesis conjecture is not single invocation

sygusNormalForm

(bool, default = true)
only search for sygus builtin terms that are in normal form

sygusNormalFormArg

(bool, default = true)
account for relationship between arguments of operations in sygus normal form

sygusNormalFormGlobal

(bool, default = true)
narrow sygus search space based on global state of current candidate program

sygusNormalFormGlobalGen

(bool, default = true)
generalize lemmas for global search space narrowing

sygusNormalFormGlobalArg

(bool, default = true)
generalize based on arguments in global search space narrowing

sygusNormalFormGlobalContent

(bool, default = true)
generalize based on content in global search space narrowing

sygusInvTemplMode

(CVC4::theory::quantifiers::SygusInvTemplMode, default = CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE)
template mode for sygus invariant synthesis

sygusUnifCondSol

(bool, default = false)
enable approach which unifies conditional solutions

sygusDirectEval

(bool, default = true)
direct unfolding of evaluation functions

sygusCRefEval

(bool, default = false)
direct evaluation of refinement lemmas for conflict analysis

cbqi

(bool, default = false)
turns on counterexample-based quantifier instantiation

recurseCbqi

(bool, default = true)
turns on recursive counterexample-based quantifier instantiation

cbqiSat

(bool, default = true)
answer sat when quantifiers are asserted with counterexample-based quantifier instantiation

cbqiModel

(bool, default = true)
guide instantiations by model values for counterexample-based quantifier instantiation

cbqiAll

(bool, default = false)
apply counterexample-based instantiation to all quantified formulas

cbqiUseInfInt

(bool, default = false)
use integer infinity for vts in counterexample-based quantifier instantiation

cbqiUseInfReal

(bool, default = false)
use real infinity for vts in counterexample-based quantifier instantiation

cbqiPreRegInst

(bool, default = false)
preregister ground instantiations in counterexample-based quantifier instantiation

cbqiMinBounds

(bool, default = false)
use minimally constrained lower/upper bound for counterexample-based quantifier instantiation

cbqiRoundUpLowerLia

(bool, default = false)
round up integer lower bounds in substitutions for counterexample-based quantifier instantiation

cbqiMidpoint

(bool, default = false)
choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation

cbqiNopt

(bool, default = true)
non-optimal bounds for counterexample-based quantifier instantiation

cbqiLitDepend

(bool, default = true)
dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation

cbqiInnermost

(bool, default = true)
only process innermost quantified formulas in counterexample-based quantifier instantiation

cbqiNestedQE

(bool, default = false)
process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation

quantEpr

(bool, default = false)
infer whether in effectively propositional fragment, use for cbqi

quantEprMatching

(bool, default = true)
use matching heuristics for EPR instantiation

localTheoryExt

(bool, default = false)
do instantiation based on local theory extensions

ltePartialInst

(bool, default = false)
partially instantiate local theory quantifiers

lteRestrictInstClosure

(bool, default = false)
treat arguments of inst closure as restricted terms for instantiation

quantAlphaEquiv

(bool, default = true)
infer alpha equivalence between quantified formulas

macrosQuant

(bool, default = false)
perform quantifiers macro expansion

macrosQuantMode

(CVC4::theory::quantifiers::MacrosQuantMode, default = CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF)
mode for quantifiers macro expansion

quantDynamicSplit

(CVC4::theory::quantifiers::QuantDSplitMode, default = CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE)
mode for dynamic quantifiers splitting

quantAntiSkolem

(bool, default = false)
perform anti-skolemization for quantified formulas

quantEqualityEngine

(bool, default = false)
maintain congrunce closure over universal equalities

trackInstLemmas

(bool, default = false)
track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization)

SEP OPTIONS
sepCheckNeg

(bool, default = true)
check negated spatial assertions

sepExp

(bool, default = false)
experimental flag for sep

sepMinimalRefine

(bool, default = false)
only add refinement lemmas for minimal (innermost) assertions

sepDisequalC

(bool, default = true)
assume cardinality elements are distinct

sepPreSkolemEmp

(bool, default = false)
eliminate emp constraint at preprocess time

sepChildRefine

(bool, default = false)
child-specific refinements of negated star, positive wand

SETS OPTIONS
setsProxyLemmas

(bool, default = false)
introduce proxy variables eagerly to shorten lemmas

setsInferAsLemmas

(bool, default = true)
send inferences as lemmas

setsRelEager

(bool, default = true)
standard effort checks for relations

setsExt

(bool, default = false)
enable extended symbols such as complement and universe in theory of sets

SMT LAYER OPTIONS
forceLogicString

(std::string)
set the logic, and override all further user attempts to change it (EXPERTS only)

simplificationMode

(SimplificationMode, default = SIMPLIFICATION_MODE_BATCH)
choose simplification mode, see --simplification=help

doStaticLearning

(bool, default = true)
use static learning (on by default)

expandDefinitions

(bool, default = false)
always expand symbol definitions in output

checkModels

(bool)
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions

dumpModels

(bool, default = false)
output models after every SAT/INVALID/UNKNOWN response

omitDontCares

(bool, default = false)
When producing a model, omit variables whose value does not matter

proof

(bool, default = false)
turn on proof generation

checkProofs

(bool)
after UNSAT/VALID, machine-check the generated proof

dumpProofs

(bool, default = false)
output proofs after every UNSAT/VALID response

dumpInstantiations

(bool, default = false)
output instantiations of quantified formulas after every UNSAT/VALID response

dumpSynth

(bool, default = false)
output solution for synthesis conjectures after every UNSAT/VALID response

unsatCores

(bool)
turn on unsat core generation

checkUnsatCores

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

dumpUnsatCores

(bool, default = false)
output unsat cores after every UNSAT/VALID response

dumpUnsatCoresFull

(bool, default = false)
dump the full unsat core, including unlabeled assertions

produceAssignments

(bool, default = false)
support the get-assignment command

interactiveMode

(bool)
deprecated name for produce-assertions

doITESimp

(bool)
turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)

doITESimpOnRepeat

(bool, default = false)
do the ite simplification pass again if repeating simplification

simplifyWithCareEnabled

(bool, default = false)
enables simplifyWithCare in ite simplificiation

compressItes

(bool, default = false)
enables compressing ites after ite simplification

unconstrainedSimp

(bool, default = false)
turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)

repeatSimp

(bool)
make multiple passes with nonclausal simplifier

zombieHuntThreshold

(uint32_t, default = 524288)
post ite compression enables zombie removal while the number of nodes is above this threshold

sortInference

(bool, default = false)
calculate sort inference of input problem, convert the input based on monotonic sorts

abstractValues

(bool, default = false)
in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard

modelUninterpDtEnum

(bool, default = false)
in models, output uninterpreted sorts as datatype enumerations

regularChannelName

(std::string)
set the regular output channel of the solver

diagnosticChannelName

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

rewriteStep

(unsigned, default = 1)
amount of resources spent for each rewrite step (EXPERTS only)

theoryCheckStep

(unsigned, default = 1)
amount of resources spent for each theory check call (EXPERTS only)

decisionStep

(unsigned, default = 1)
amount of getNext decision calls in the decision engine (EXPERTS only)

bitblastStep

(unsigned, default = 1)
amount of resources spent for each bitblast step (EXPERTS only)

parseStep

(unsigned, default = 1)
amount of resources spent for each command/expression parsing (EXPERTS only)

lemmaStep

(unsigned, default = 1)
amount of resources spent when adding lemmas (EXPERTS only)

restartStep

(unsigned, default = 1)
amount of resources spent for each theory restart (EXPERTS only)

cnfStep

(unsigned, default = 1)
amount of resources spent for each call to cnf conversion (EXPERTS only)

preprocessStep

(unsigned, default = 1)
amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)

quantifierStep

(unsigned, default = 1)
amount of resources spent for quantifier instantiations (EXPERTS only)

satConflictStep

(unsigned, default = 1)
amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)

bvSatConflictStep

(unsigned, default = 1)
amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)

rewriteApplyToConst

(bool, default = false)
eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 (EXPERTS only)

replayInputFilename

(std::string)
replay decisions from file

replayLogFilename

(std::string)
replay decisions from file

forceNoLimitCpuWhileDump

(bool, default = false)
Force no CPU limit when dumping models and proofs

solveIntAsBV

(uint32_t, default = 0)
attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)

solveRealAsInt

(bool, default = false)
attempt to solve a pure real satisfiable problem as a integer problem (for non-linear)

STRINGS THEORY OPTIONS
stringExp

(bool, default = false)
experimental features in the theory of strings

stringLB

(unsigned, default = 0)
the strategy of LB rule application: 0-lazy, 1-eager, 2-no

stdASCII

(bool, default = true)
the alphabet contains only characters from the standard ASCII or the extended one

stringFMF

(bool, default = false)
the finite model finding used by the theory of strings

stringEager

(bool, default = false)
strings eager check

stringEIT

(bool, default = false)
the eager intersection used by the theory of strings

stringOpt1

(bool, default = true)
internal option1 for strings: normal form

stringOpt2

(bool, default = false)
internal option2 for strings: constant regexp splitting

stringIgnNegMembership

(bool, default = false)
internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)

stringLazyPreproc

(bool, default = true)
perform string preprocessing lazily

stringLenGeqZ

(bool, default = false)
strings length greater than zero lemmas

stringLenNorm

(bool, default = true)
strings length normalization lemma

stringSplitEmp

(bool, default = true)
strings split on empty string

stringInferSym

(bool, default = true)
strings split on empty string

stringEagerLen

(bool, default = true)
strings eager length lemmas

stringCheckEntailLen

(bool, default = true)
check entailment between length terms to reduce splitting

stringProcessLoop

(bool, default = true)
reduce looping word equations to regular expressions

stringAbortLoop

(bool, default = false)
abort when a looping word equation is encountered

stringInferAsLemmas

(bool, default = false)
always send lemmas out instead of making internal inferences

stringRExplainLemmas

(bool, default = true)
regression explanations for string lemmas

stringMinPrefixExplain

(bool, default = true)
minimize explanations for prefix of normal forms in strings

stringGuessModel

(bool, default = false)
use model guessing to avoid string extended function reductions

stringUfReduct

(bool, default = false)
use uninterpreted functions when applying extended function reductions

stringBinaryCsp

(bool, default = false)
use binary search when splitting strings

stringLenPropCsp

(bool, default = false)
do length propagation based on constant splits

THEORY LAYER OPTIONS
theoryOfMode

(CVC4::theory::TheoryOfMode, default = CVC4::theory::THEORY_OF_TYPE_BASED)
mode for Theory::theoryof() (EXPERTS only)

useTheoryList

(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
ufSymmetryBreaker

(bool, default = true)
use UF symmetry breaker (Deharbe et al., CADE 2011)

condenseFunctionValues

(bool, default = true)
condense models for functions rather than explicitly representing them

ufssRegions

(bool, default = true)
disable region-based method for discovering cliques and splits in uf strong solver

ufssEagerSplits

(bool, default = false)
add splits eagerly for uf strong solver

ufssTotality

(bool, default = false)
always use totality axioms for enforcing cardinality constraints

ufssTotalityLimited

(int, default = -1)
apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)

ufssTotalitySymBreak

(bool, default = false)
apply symmetry breaking for totality axioms

ufssAbortCardinality

(int, default = -1)
tells the uf strong solver a cardinality to abort at (-1 == no limit, default)

ufssExplainedCliques

(bool, default = false)
use explained clique lemmas for uf strong solver

ufssSimpleCliques

(bool, default = true)
always use simple clique lemmas for uf strong solver

ufssDiseqPropagation

(bool, default = false)
eagerly propagate disequalities for uf strong solver

ufssMode

(CVC4::theory::uf::UfssMode, default = CVC4::theory::uf::UF_SS_FULL)
mode of operation for uf strong solver.

ufssCliqueSplits

(bool, default = false)
use cliques instead of splitting on demand to shrink model

ufssSymBreak

(bool, default = false)
finite model finding symmetry breaking techniques

ufssFairness

(bool, default = true)
use fair strategy for finite model finding multiple sorts

ufssFairnessMonotone

(bool, default = false)
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/.

Info

August 2017 CVC4 release 1.5 CVC4 Internals Documentation