Options

cvc5 can be configured at runtime using a wide range of options. When cvc5 is used as a binary, options can be set on the command line. Also, options can be set and inspected using the respective commands of the input language and the corresponding API functions:

Generally, all options are identified by a name <name>, and (optionally) by a short name <short> (a single letter). Additionally, they can have one or more aliases, which can be used instead of <name>.

Internally, options are strongly typed and must be either Boolean, (signed or unsigned) integers, floating-point numbers, strings, or an enumeration type. Values for options with a numeric type may be restricted to an interval.

Some options have custom types (e.g., err) which require special treatment internally. The usage of such options is documented as part of the documentation for the corresponding options.

On the command line, a Boolean option can be set to true via --<name> or -<short>. Most Boolean options can also be set to false via --no-<name>. In cvc5’s APIs, this is done via setOption("<name>", "true" | "false").

For all other types, values are given on the command line using --<name>=<value> or --<name> <value>, and setOption("<name>", "<value>") in the APIs. The given value must be convertible to the appropriate type, in particular for numeric and enumeration types.

Below is an exhaustive list of options supported by cvc5.

Most Commonly-Used cvc5 Options

i | incremental [type bool, default true] (also --no-*)

enable incremental solving

L | lang | input-language [custom Language, default Language::LANG_AUTO]

force input language (default is “auto”; see –lang help)

o | output [none | inst | inst-strategy | oracles | sygus | sygus-grammar | sygus-enumerator | sygus-sol-gterm | trigger | raw-benchmark | learned-lits | subs | post-asserts | pre-asserts | deep-restart | incomplete | lemmas | trusted-proof-steps | timeout-core-benchmark | unsat-core-benchmark | unsat-core-lemmas-benchmark | portfolio | block-model | options-auto | rare-db, default none]

Enable output tag.

Output tags.

inst:

print instantiations during solving

inst-strategy:

prints a summary of the instantiation techniques as they are run.

oracles:

print calls to oracles and responses received

sygus:

print enumerated terms and candidates generated by the sygus solver

sygus-grammar:

print grammars automatically generated by the sygus solver

sygus-enumerator:

print enumerators generated by the sygus solver

sygus-sol-gterm:

print annotations for terms in sygus solutions that indicate the grammar used to generate them

trigger:

print selected triggers for quantified formulas

raw-benchmark:

print the benchmark back on the output verbatim as it is processed

learned-lits:

print input literals that hold globally

subs:

print top-level substitutions learned during preprocessing

post-asserts:

print a benchmark corresponding to the assertions of the input problem after preprocessing

pre-asserts:

print a benchmark corresponding to the assertions of the input problem before preprocessing

deep-restart:

print when cvc5 performs a deep restart along with the literals it has learned

incomplete:

print reason why cvc5 answers unknown for any given check-sat query

lemmas:

print lemmas as they are added to the SAT solver

trusted-proof-steps:

print formulas corresponding to trusted proof steps in final proofs

timeout-core-benchmark:

print the corresponding benchmark when successfully computing a timeout core.

unsat-core-benchmark:

print the corresponding benchmark when successfully computing an unsat core.

unsat-core-lemmas-benchmark:

print the corresponding benchmark when successfully computing an unsat core with theory lemmas.

portfolio:

prints the option strings tried in portfolio mode.

block-model:

prints the formulas used when block-model is run.

options-auto:

prints the options set during automatic configuration.

rare-db:

upon initialization, print the entire set of RARE rewrite rules as they are defined in the proof signature.

parse-only [type bool, default false] (also --no-*)

exit after parsing input

preprocess-only [type bool, default false] (also --no-*)

exit after preprocessing input

q | quiet [type bool]

decrease verbosity (may be repeated)

rlimit [type uint64_t, default 0]

set resource limit

rlimit-per | reproducible-resource-limit [type uint64_t, default 0]

set resource limit per query

stats [type bool, default false] (also --no-*)

give statistics on exit

tlimit [type uint64_t, default 0]

set time limit in milliseconds of wall clock time

tlimit-per [type uint64_t, default 0]

set time limit per query in milliseconds

v | verbose [type bool]

increase verbosity (may be repeated)

verbosity [type int64_t, default 0]

the verbosity level of cvc5

h | help [type bool, default false]

full command line reference

H | help-regular [type bool, default false]

regular command line reference

interactive [type bool, default false] (also --no-*)

force interactive shell/non-interactive mode

print-success [type bool, default false] (also --no-*)

print the “success” output required of SMT-LIBv2

s | seed | random-seed [type uint64_t, default 0]

seed for random number generator

show-config [type bool, default false]

show cvc5 static configuration

V | version [type bool, default false]

identify this cvc5 binary

force-logic [type string, default ""]

set the logic, and override all further user attempts to change it

strict-parsing [type bool, default false] (also --no-*)

be less tolerant of non-conforming inputs

dag-thresh [type int64_t, 0 <= N, default 1]

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

output-lang | output-language [custom Language, default Language::LANG_AUTO]

force output language (default is “auto”; see –output-lang help)

print-inst [list | num, default list]

print format for printing instantiations

Print format for printing instantiations.

list:

Print the list of instantiations per quantified formula, when non-empty.

num:

Print the total number of instantiations per quantified formula, when non-zero.

check-models [type bool, default false] (also --no-*)

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

m | produce-models [type bool, default false] (also --no-*)

support the get-value and get-model commands

Additional cvc5 Options

Arithmetic Theory Module

approx-branch-depth [type int64_t, default 200]

[experts only]

maximum branch depth the approximate solver is allowed to take

arith-brab [type bool, default true] (also --no-*)

whether to use simple rounding, similar to a unit-cube test, for integers

arith-eq-solver [type bool, default false] (also --no-*)

[experts only]

whether to use the equality solver in the theory of arithmetic

arith-no-partial-fun [type bool, default false] (also --no-*)

[experts only]

do not use partial function semantics for arithmetic (not SMT LIB compliant)

arith-prop [none | unate | bi | both, default both]

[experts only]

turns on arithmetic propagation (default is ‘old’, see –arith-prop=help)

This decides on kind of propagation arithmetic attempts to do during the search.

unate:

Use constraints to do unate propagation.

bi:

(Bounds Inference) infers bounds on basic variables using the upper and lower bounds of the non-basic variables in the tableau.

both:

Use bounds inference and unate.

arith-prop-clauses [type uint64_t, default 8]

[experts only]

rows shorter than this are propagated as clauses

arith-rewrite-equalities [type bool, default false] (also --no-*)

turns on the preprocessing rewrite turning equalities into a conjunction of inequalities

arith-static-learning [type bool, default true] (also --no-*)

do arithmetic static learning for ite terms based on bounds when static learning is enabled

collect-pivot-stats [type bool, default false] (also --no-*)

[experts only]

collect the pivot history

cut-all-bounded [type bool, default false] (also --no-*)

[experts only]

turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds

dio-decomps [type bool, default false] (also --no-*)

[experts only]

let skolem variables for integer divisibility constraints leak from the dio solver

dio-solver [type bool, default true] (also --no-*)

[experts only]

turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)

dio-turns [type int64_t, default 10]

[experts only]

turns in a row dio solver cutting gets

error-selection-rule [min | varord | max | sum, default min]

[experts only]

change the pivot rule for the basic variable (default is ‘min’, see –pivot-rule help)

This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select.

min:

The minimum abs() value of the variable’s violation of its bound.

varord:

The variable order.

max:

The maximum violation the bound.

fc-penalties [type bool, default false] (also --no-*)

[experts only]

turns on degenerate pivot penalties

heuristic-pivots [type int64_t, default 0]

[experts only]

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 [type bool, default false] (also --no-*)

[experts only]

attempt to use external lemmas if approximate solve integer failed

maxCutsInContext [type uint64_t, default 65535]

[experts only]

maximum cuts in a given context before signalling a restart

miplib-trick [type bool, default false] (also --no-*)

[experts only]

turns on the preprocessing step of attempting to infer bounds on miplib problems

miplib-trick-subs [type uint64_t, default 1]

[experts only]

do substitution for miplib ‘tmp’ vars if defined in <= N eliminated vars

new-prop [type bool, default true] (also --no-*)

[experts only]

use the new row propagation system

nl-cov [type bool, default false] (also --no-*)

whether to use the cylindrical algebraic coverings solver for non-linear arithmetic

nl-cov-force [type bool, default false] (also --no-*)

[experts only]

forces using the cylindrical algebraic coverings solver, even in cases where it is possibly not safe to do so

nl-cov-lift [regular | lazard, default regular]

[experts only]

choose the Coverings lifting mode

Modes for the Coverings lifting in non-linear arithmetic.

regular:

Regular lifting.

lazard:

Lazard’s lifting scheme.

nl-cov-linear-model [none | initial | persistent, default none]

whether to use the linear model as initial guess for the cylindrical algebraic coverings solver

Modes for the usage of the linear model in non-linear arithmetic.

none:

Do not use linear model to seed nonlinear model

initial:

Use linear model to seed nonlinear model initially, discard it when it does not work

persistent:

Use linear model to seed nonlinear model whenever possible

nl-cov-proj [mccallum | lazard | lazard-mod, default mccallum]

[experts only]

choose the Coverings projection operator

Modes for the Coverings projection operator in non-linear arithmetic.

mccallum:

McCallum’s projection operator.

lazard:

Lazard’s projection operator.

lazard-mod:

A modification of Lazard’s projection operator.

nl-cov-prune [type bool, default false] (also --no-*)

[experts only]

whether to prune intervals more aggressively

nl-cov-var-elim [type bool, default true] (also --no-*)

[experts only]

whether to eliminate variables using equalities before going into the cylindrical algebraic coverings solver. It can not be used when producing proofs right now.

nl-ext [none | light | full, default full]

incremental linearization approach to non-linear

Modes for the non-linear linearization

none:

Disable linearization approach

light:

Only use a few light-weight lemma schemes

full:

Use all lemma schemes

nl-ext-ent-conf [type bool, default false] (also --no-*)

[experts only]

check for entailed conflicts in non-linear solver

nl-ext-factor [type bool, default true] (also --no-*)

use factoring inference in non-linear incremental linearization solver

nl-ext-inc-prec [type bool, default true] (also --no-*)

[experts only]

whether to increment the precision for irrational function constraints

nl-ext-purify [type bool, default false] (also --no-*)

[experts only]

purify non-linear terms at preprocess

nl-ext-rbound [type bool, default false] (also --no-*)

[experts only]

use resolution-style inference for inferring new bounds in non-linear incremental linearization solver

nl-ext-rewrite [type bool, default true] (also --no-*)

do context-dependent simplification based on rewrites in non-linear solver

nl-ext-split-zero [type bool, default false] (also --no-*)

[experts only]

initial splits on zero for all variables

nl-ext-tf-taylor-deg [type int64_t, default 4]

[experts only]

initial degree of polynomials for Taylor approximation

nl-ext-tf-tplanes [type bool, default true] (also --no-*)

use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver

nl-ext-tplanes [type bool, default true] (also --no-*)

use non-terminating tangent plane strategy for non-linear incremental linearization solver

nl-ext-tplanes-interleave [type bool, default false] (also --no-*)

interleave tangent plane strategy for non-linear incremental linearization solver

nl-icp [type bool, default false] (also --no-*)

[experts only]

whether to use ICP-style propagations for non-linear arithmetic

nl-rlv [none | interleave | always, default none]

[experts only]

choose mode for using relevance of assertions in non-linear arithmetic

Modes for using relevance of assertions in non-linear arithmetic.

none:

Do not use relevance.

interleave:

Alternate rounds using relevance.

always:

Always use relevance.

nl-rlv-assert-bounds [type bool, default false] (also --no-*)

[experts only]

use bound inference utility to prune when an assertion is entailed by another

pb-rewrites [type bool, default false] (also --no-*)

[experts only]

apply pseudo boolean rewrites

pivot-threshold [type uint64_t, default 2]

[experts only]

sets the number of pivots using –pivot-rule per basic variable per simplex instance before using variable order

pp-assert-max-sub-size [type uint64_t, default 2]

[experts only]

threshold for substituting an equality in ppAssert

prop-row-length [type uint64_t, default 16]

[experts only]

sets the maximum row length to be used in propagation

replay-early-close-depth [type int64_t, default 1]

[experts only]

multiples of the depths to try to close the approx log eagerly

replay-lemma-reject-cut [type uint64_t, default 25500]

[experts only]

maximum complexity of any coefficient while outputting replaying cut lemmas

replay-num-err-penalty [type int64_t, default 4194304]

[experts only]

number of solve integer attempts to skips after a numeric failure

replay-reject-cut [type uint64_t, default 25500]

[experts only]

maximum complexity of any coefficient while replaying cuts

restrict-pivots [type bool, default true] (also --no-*)

[experts only]

have a pivot cap for simplex at effort levels below fullEffort

revert-arith-models-on-unsat [type bool, default false] (also --no-*)

[experts only]

revert the arithmetic model to a known safe model on unsat if one is cached

rr-turns [type int64_t, default 3]

[experts only]

round robin turn

se-solve-int [type bool, default false] (also --no-*)

[experts only]

attempt to use the approximate solve integer method on standard effort

simplex-check-period [type uint64_t, default 200]

[experts only]

the number of pivots to do in simplex before rechecking for a conflict on all variables

soi-qe [type bool, default false] (also --no-*)

[experts only]

use quick explain to minimize the sum of infeasibility conflicts

standard-effort-variable-order-pivots [type int64_t, default -1]

[experts only]

limits the number of pivots in a single invocation of check() at a non-full effort level using Bland’s pivot rule

unate-lemmas [all | eqs | ineqs | none, default all]

[experts only]

determines which lemmas to add before solving (default is ‘all’, see –unate-lemmas=help)

Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials.

all:

A combination of inequalities and equalities.

eqs:

Outputs lemmas of the general forms (= p c) implies (<= p d) for c < d, or (= p c) implies (not (= p d)) for c != d.

ineqs:

Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.

none:

Do not add unate lemmas.

use-approx [type bool, default false] (also --no-*)

[experts only]

attempt to use an approximate solver

use-fcsimplex [type bool, default false] (also --no-*)

[experts only]

use focusing and converging simplex (FMCAD 2013 submission)

use-soi [type bool, default false] (also --no-*)

[experts only]

use sum of infeasibility simplex (FMCAD 2013 submission)

Arrays Theory Module

arrays-eager-index [type bool, default true] (also --no-*)

turn on eager index splitting for generated array lemmas

arrays-eager-lemmas [type bool, default false] (also --no-*)

[experts only]

turn on eager lemma generation for arrays

arrays-exp [type bool, default false] (also --no-*)

[experts only]

enable experimental features in the theory of arrays

arrays-optimize-linear [type bool, default true] (also --no-*)

[experts only]

turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)

arrays-prop [type int64_t, default 2]

[experts only]

propagation effort for arrays: 0 is none, 1 is some, 2 is full

arrays-reduce-sharing [type bool, default false] (also --no-*)

[experts only]

use model information to reduce size of care graph for arrays

arrays-weak-equiv [type bool, default false] (also --no-*)

[experts only]

use algorithm from Christ/Hoenicke (SMT 2014)

Base Module

err | diagnostic-output-channel [custom ManagedErr, default {}]

[experts only]

Set the error (or diagnostic) output channel. Writes to stderr for “stderr” or “–”, stdout for “stdout” or the given filename otherwise.

in [custom ManagedIn, default {}]

[experts only]

Set the error (or diagnostic) output channel. Reads from stdin for “stdin” or “–” and the given filename otherwise.

out | regular-output-channel [custom ManagedOut, default {}]

[experts only]

Set the error (or diagnostic) output channel. Writes to stdout for “stdout” or “–”, stderr for “stderr” or the given filename otherwise.

plugin-notify-sat-clause-in-solve [type bool, default true] (also --no-*)

[experts only]

only inform plugins of SAT clauses when we are in the main solving loop of the SAT solver

plugin-share-skolems [type bool, default true] (also --no-*)

[experts only]

true if we permit sharing theory lemmas and SAT clauses with skolems

rweight [type string]

[experts only]

set a single resource weight

safe-options [type bool, default false] (also --no-*)

[experts only]

do not allow setting any option that is not common or regular

stats-all [type bool, default false] (also --no-*)

[experts only]

print unchanged (defaulted) statistics as well

stats-every-query [type bool, default false] (also --no-*)

in incremental mode, print stats after every satisfiability or validity query

stats-internal [type bool, default false] (also --no-*)

[experts only]

print internal (non-public) statistics as well

t | trace [type string]

trace something (e.g. -t pushpop), can repeat and may contain wildcards like (e.g. -t theory::*)

Bitvector Theory Module

bitblast [lazy | eager, default lazy]

choose bitblasting mode, see –bitblast=help

Bit-blasting modes.

lazy:

Separate Boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver.

eager:

Bitblast eagerly to bit-vector SAT solver.

bitwise-eq [type bool, default true] (also --no-*)

lift equivalence with one-bit bit-vectors to be boolean operations

bool-to-bv [off | ite | all, default off]

convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see –bool-to-bv=help

BoolToBV preprocessing pass modes.

off:

Don’t push any booleans to width one bit-vectors.

ite:

Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula if not all sub-formulas can be turned to bit-vectors.

all:

Force all booleans to be bit-vectors of width one except at the top level. Most aggressive mode.

bv-assert-input [type bool, default false] (also --no-*)

[experts only]

assert input assertions on user-level 0 instead of assuming them in the bit-vector SAT solver

bv-eager-eval [type bool, default false] (also --no-*)

perform eager context-dependent evaluation for applications of bv kinds in the equality engine

bv-eq-engine [type bool, default true] (also --no-*)

[experts only]

enable equality engine when possible in bitvector theory

bv-gauss-elim [type bool, default false] (also --no-*)

[experts only]

simplify formula via Gaussian Elimination if applicable

bv-intro-pow2 [type bool, default false] (also --no-*)

[experts only]

introduce bitvector powers of two as a preprocessing pass

bv-propagate [type bool, default true] (also --no-*)

[experts only]

use bit-vector propagation in the bit-blaster

bv-rw-extend-eq [type bool, default false] (also --no-*)

[experts only]

enable additional rewrites over zero/sign extend over equalities with constants (useful on BV/2017-Preiner-scholl-smt08)

bv-sat-solver [minisat | cryptominisat | cadical | kissat, default cadical]

choose which sat solver to use, see –bv-sat-solver=help

SAT solver for bit-blasting backend.

bv-solver [bitblast | bitblast-internal, default bitblast]

choose bit-vector solver, see –bv-solver=help

Bit-vector solvers.

bitblast:

Enables bitblasting solver.

bitblast-internal:

Enables bitblasting to internal SAT solver with proof support.

bv-to-bool [type bool, default false] (also --no-*)

lift bit-vectors of size 1 to booleans when possible

Datatypes Theory Module

cdt-bisimilar [type bool, default true] (also --no-*)

[experts only]

do bisimilarity check for co-datatypes

dt-binary-split [type bool, default false] (also --no-*)

[experts only]

do binary splits for datatype constructor types

dt-blast-splits [type bool, default false] (also --no-*)

[experts only]

when applicable, blast splitting lemmas for all variables at once

dt-cyclic [type bool, default true] (also --no-*)

[experts only]

do cyclicity check for datatypes

dt-infer-as-lemmas [type bool, default false] (also --no-*)

[experts only]

always send lemmas out instead of making internal inferences

dt-nested-rec [type bool, default false] (also --no-*)

[experts only]

allow nested recursion in datatype definitions

dt-polite-optimize [type bool, default true] (also --no-*)

[experts only]

turn on optimization for polite combination

dt-share-sel [type bool, default true] (also --no-*)

internally use shared selectors across multiple constructors

sygus-abort-size [type int64_t, default -1]

tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)

sygus-fair [direct | dt-size | dt-height-bound | dt-size-bound | none, default dt-size]

if and how to apply fairness for sygus

Modes for enforcing fairness for counterexample guided quantifier instantion.

direct:

Enforce fairness using direct conflict lemmas.

dt-size:

Enforce fairness using size operator.

dt-height-bound:

Enforce fairness by height bound predicate.

dt-size-bound:

Enforce fairness by size bound predicate.

none:

Do not enforce fairness.

sygus-fair-max [type bool, default true] (also --no-*)

[experts only]

use max instead of sum for multi-function sygus conjectures

sygus-rewriter [none | basic | extended, default extended]

if and how to apply rewriting for sygus symmetry breaking

Modes for applying rewriting for sygus symmetry breaking.

none:

Do not use the rewriter.

basic:

Use the basic rewriter.

extended:

Use the extended rewriter.

sygus-simple-sym-break [none | basic | agg, default agg]

if and how to apply simple symmetry breaking based on the grammar for smart enumeration

Modes for applying simple symmetry breaking based on the grammar for smart enumeration.

none:

Do not apply simple symmetry breaking.

basic:

Apply basic simple symmetry breaking.

agg:

Apply aggressive simple symmetry breaking.

sygus-sym-break-lazy [type bool, default true] (also --no-*)

[experts only]

lazily add symmetry breaking lemmas for terms

sygus-sym-break-pbe [type bool, default true] (also --no-*)

sygus symmetry breaking lemmas based on pbe conjectures

sygus-sym-break-rlv [type bool, default true] (also --no-*)

[experts only]

add relevancy conditions to symmetry breaking lemmas

Decision Heuristics Module

decision | decision-mode [internal | justification | stoponly, default internal]

choose decision mode, see –decision=help

Decision modes.

internal:

Use the internal decision heuristics of the SAT solver.

justification:

An ATGP-inspired justification heuristic.

stoponly:

Use the justification heuristic only to stop early, not for decisions.

jh-rlv-order [type bool, default false] (also --no-*)

[experts only]

maintain activity-based ordering for decision justification heuristic

jh-skolem [first | last, default first]

[experts only]

policy for when to satisfy skolem definitions in justification heuristic

Policy for when to satisfy skolem definitions in justification heuristic

first:

satisfy pending relevant skolem definitions before input assertions

last:

satisfy pending relevant skolem definitions after input assertions

jh-skolem-rlv [assert | always, default assert]

[experts only]

policy for when to consider skolem definitions relevant in justification heuristic

Policy for when to consider skolem definitions relevant in justification heuristic

assert:

skolems are relevant when they occur in an asserted literal

always:

skolems are always relevant

Expression Module

type-checking [type bool, default DO_SEMANTIC_CHECKS_BY_DEFAULT] (also --no-*)

[experts only]

type check expressions

wf-checking [type bool, default true] (also --no-*)

[experts only]

check that terms passed to API methods are well formed (default false for text interface)

Finite Field Theory Module

ff-bitsum [type bool, default false] (also --no-*)

[experts only]

parse bitsums

ff-elim-disjunctive-bit [type bool, default true] (also --no-*)

[experts only]

rewrite disjunctive bit constraints (or (= x 1) (= x 0)) as (= (* x x) x)

ff-field-polys [type bool, default false] (also --no-*)

[experts only]

include field polynomials in Groebner basis computation; don’t do this

ff-solver [gb | split, default gb]

[experts only]

which field solver (default: ‘gb’; see –ff-solver=help)

Which field solver

gb:

use a groebner basis for the whole system

split:

use multiple groebner bases for partitions of the system

ff-trace-gb [type bool, default true] (also --no-*)

[experts only]

use a traced groebner basis engine

Floating-Point Module

fp-exp [type bool, default false] (also --no-*)

[experts only]

Allow floating-point sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental)

fp-lazy-wb [type bool, default false] (also --no-*)

[experts only]

Enable lazier word-blasting (on preNotifyFact instead of registerTerm)

Driver Module

dump-difficulty [type bool, default false] (also --no-*)

dump the difficulty measure after every response to check-sat

dump-instantiations [type bool, default false] (also --no-*)

output instantiations of quantified formulas after every UNSAT/VALID response

dump-instantiations-debug [type bool, default false] (also --no-*)

[experts only]

output instantiations of quantified formulas after every UNSAT/VALID response, with debug information

dump-models [type bool, default false] (also --no-*)

output models after every SAT/INVALID/UNKNOWN response

dump-proofs [type bool, default false] (also --no-*)

output proofs after every UNSAT/VALID response

dump-unsat-cores [type bool, default false] (also --no-*)

output unsat cores after every UNSAT/VALID response

dump-unsat-cores-lemmas [type bool, default false] (also --no-*)

output lemmas in unsat cores after every UNSAT/VALID response

early-exit [type bool, default true] (also --no-*)

[experts only]

do not run destructors at exit; default on except in debug builds

force-no-limit-cpu-while-dump [type bool, default false] (also --no-*)

[experts only]

Force no CPU limit when dumping models and proofs

portfolio-jobs [type uint64_t, default 1]

[experts only]

Number of parallel jobs the portfolio engine can run

segv-spin [type bool, default false] (also --no-*)

[experts only]

spin on segfault/other crash waiting for gdb

show-trace-tags [type bool, default false]

[experts only]

show all available tags for tracing

use-portfolio [type bool, default false] (also --no-*)

[experts only]

Use internal portfolio mode based on the logic

Parallel Module

append-learned-literals-to-cubes [type bool, default false] (also --no-*)

[experts only]

emit learned literals with the cubes

checks-before-partition [type uint64_t, default 1]

[experts only]

number of standard or full effort checks until partitioning

checks-between-partitions [type uint64_t, default 1]

[experts only]

number of checks between partitions

compute-partitions [type uint64_t, default 0]

[experts only]

make n partitions. n <2 disables computing partitions entirely

partition-check | check [standard | full, default standard]

[experts only]

select whether partitioning happens at full or standard check

Partition check modes.

standard:

create partitions at standard checks

full:

create partitions at full checks

partition-conflict-size [type uint64_t, default 0]

[experts only]

number of literals in a cube; if no partition size is set, then the partition conflict size is chosen to be log2(number of requested partitions)

partition-start-time [type uint64_t, default 30]

[experts only]

time to start creating partitions in seconds

partition-strategy | partition [decision-scatter | heap-scatter | lemma-scatter | decision-cube | heap-cube | lemma-cube, default decision-scatter]

[experts only]

choose partition strategy mode

Partition strategy modes.

decision-scatter:

For 4 partitions, creates partitions C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3, from decisions

heap-scatter:

For 4 partitions, creates partitions C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3, from heap

lemma-scatter:

For 4 partitions, creates partitions C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3, from lemmas

decision-cube:

Creates mutually exclusive cubes from the decisions in the SAT solver.

heap-cube:

Creates mutually exclusive cubes from the order heap in the SAT solver.

lemma-cube:

Creates mutually exclusive cubes from the lemmas sent to the SAT solver.

partition-time-interval [type double, default 1.0]

[experts only]

time to wait between scatter partitions

partition-tlimit [type uint64_t, default 60]

[experts only]

time limit for partitioning in seconds

partition-when [tlimit | climit, default tlimit]

[experts only]

choose when to partition

PartitionWhen modes.

tlimit:

Partition when the time limit is exceeded.

climit:

Partition when number of checks is exceeded.

random-partitioning [type bool, default false] (also --no-*)

[experts only]

create random partitions

write-partitions-to | partitions-out [custom ManagedOut, default ManagedOut()]

[experts only]

set the output channel for writing partitions

Parser Module

filesystem-access [type bool, default true] (also --no-*)

[experts only]

limits the file system access if set to false

fresh-declarations [type bool, default true] (also --no-*)

use API interface for fresh constants when parsing declarations and definitions

global-declarations [type bool, default false] (also --no-*)

force all declarations and definitions to be global when parsing

parse-skolem-definitions [type bool, default false] (also --no-*)

[experts only]

allows the parsing of skolems in the input file

semantic-checks [type bool, default DO_SEMANTIC_CHECKS_BY_DEFAULT] (also --no-*)

[experts only]

enable semantic checks, including type checks

Printing Module

bv-print-consts-as-indexed-symbols [type bool, default false] (also --no-*)

print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x

expr-depth [type int64_t, -1 <= N, default -1]

[experts only]

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

flatten-ho-chains [type bool, default false] (also --no-*)

[experts only]

print (binary) application chains in a flattened way, e.g. (a b c) rather than ((a b) c)

model-u-print [decl-sort-and-fun | decl-fun | none, default none]

determines how to print uninterpreted elements in models

uninterpreted elements in models printing modes.

decl-sort-and-fun:

print uninterpreted elements declare-fun, and also include a declare-sort for the sort

decl-fun:

print uninterpreted elements declare-fun, but don’t include a declare-sort for the sort

none:

(default) do not print declarations of uninterpreted elements in models.

print-arith-lit-token [type bool, default false] (also --no-*)

[experts only]

print rationals and negative arithmetic literals as lexed tokens, e.g. 1/4, -1.5

print-skolem-definitions [type bool, default false] (also --no-*)

[experts only]

print skolems based on their definitions e.g. @ARRAY_DIFF_N prints instead as (@array.diff A B)

Proof Module

alf-allow-trust [type bool, default true] (also --no-*)

[experts only]

Whether to allow trust in the ALF printer

alf-print-reference [type bool, default false] (also --no-*)

[experts only]

Print reference to original file instead of redeclaring

check-proof-steps [type bool, default false] (also --no-*)

[experts only]

Check proof steps for satisfiability, for refutation soundness testing. Note this checks only steps for non-core proof rules

drat-binary-format [type bool, default false] (also --no-*)

[experts only]

Print the DRAT proof in binary format

lfsc-expand-trust [type bool, default false] (also --no-*)

[experts only]

Print the children of trusted proof steps

lfsc-flatten [type bool, default false] (also --no-*)

[experts only]

Flatten steps in the LFSC proof

opt-res-reconstruction-size [type bool, default true] (also --no-*)

Optimize resolution reconstruction to reduce proof size

print-dot-clusters [type bool, default false] (also --no-*)

Whether the proof node clusters (e.g. SAT, CNF, INPUT) will be printed when using the dot format or not.

proof-alethe-experimental [type bool, default false] (also --no-*)

[experts only]

Enable the use of Alethe proofs (experimental)

proof-alethe-res-pivots [type bool, default false] (also --no-*)

[experts only]

Add pivots to Alethe resolution steps

proof-annotate [type bool, default false] (also --no-*)

[experts only]

add optional annotations to proofs, which enables statistics for inference ids for lemmas and conflicts appearing in final proof

proof-check [eager | eager-simple | lazy | none, default none]

[experts only]

select internal proof checking mode

Internal proof checking modes.

eager:

check rule applications and proofs from generators eagerly for local debugging

eager-simple:

check rule applications during construction

lazy:

check rule applications only during final proof construction

none:

do not check rule applications

proof-dag-global [type bool, default true] (also --no-*)

[experts only]

Dagify terms in proofs using global definitions

proof-dot-dag [type bool, default false] (also --no-*)

[experts only]

Indicates if the dot proof will be printed as a DAG or as a tree

proof-elim-subtypes [type bool, default false] (also --no-*)

[experts only]

Eliminate subtypes (mixed arithmetic) in proofs

proof-format-mode [none | dot | lfsc | alethe | alf, default alf]

[experts only]

select language of proof output

Proof format modes.

none:

Do not translate proof output

dot:

Output DOT proof

lfsc:

Output LFSC proof

alethe:

Output Alethe proof

alf:

Output AletheLF proof

proof-granularity [macro | rewrite | theory-rewrite | dsl-rewrite | dsl-rewrite-strict, default macro]

modes for proof granularity

Modes for proof granularity.

macro:

Allow macros. Do not improve the granularity of proofs.

rewrite:

Allow trusted rewrite or substitution steps, expand macros.

theory-rewrite:

Allow trusted theory rewrite steps, expand macros, rewrite and substitution steps.

dsl-rewrite:

Allow theory and DSL rewrite steps, expand macros, rewrite, substitution, and theory rewrite steps.

dsl-rewrite-strict:

Allow theory and DSL rewrite steps giving preference to DSL rewrite steps.

proof-pedantic [type uint64_t, N <= 100, default 0]

[experts only]

assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof

proof-pp-merge [type bool, default true] (also --no-*)

[experts only]

merge subproofs in final proof post-processor

proof-print-conclusion [type bool, default false] (also --no-*)

[experts only]

Print conclusion of proof steps when printing AST

proof-prune-input [type bool, default false] (also --no-*)

[experts only]

Prune unused input assumptions from final scope

proof-rewrite-rcons-rec-limit [type uint64_t, default 5]

the matching recursion limit for reconstructing proofs of theory rewrites

proof-rewrite-rcons-step-limit [type uint64_t, default 1000]

the limit of steps considered for reconstructing proofs of theory rewrites

prop-proof-mode [proof | sat-external-prove | sketch, default proof]

modes for proof granularity

Modes for proof granularity.

proof:

A proof computed by the SAT solver.

sat-external-prove:

A proof containing a step that will be proven externally.

sketch:

A sketch given by the SAT solver.

sat-proof-min-dimacs [type bool, default true] (also --no-*)

[experts only]

Minimize the DIMACs emitted when prop-proof-mode is set to sat-external-prove

SAT Layer Module

minisat-dump-dimacs [type bool, default false] (also --no-*)

[experts only]

instead of solving minisat dumps the asserted clauses in Dimacs format

minisat-simplification [all | clause-elim | none, default all]

[experts only]

Simplifications to be performed by Minisat.

Modes for Minisat simplifications.

all:

Variable and clause elimination, plus other simplifications.

clause-elim:

Caluse elimination and other simplifications, except variable elimination.

none:

No simplifications.

preregister-mode [eager | lazy, default eager]

[experts only]

Modes for when to preregister literals.

Modes for when to preregister literals.

eager:

Preregister literals when they are registered as literals in the SAT solver.

lazy:

Preregister literals when they are asserted by the SAT solver.

random-freq | random-frequency [type double, 0.0 <= P <= 1.0, default 0.0]

[experts only]

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

restart-int-base [type uint64_t, default 25]

[experts only]

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

restart-int-inc [type double, 0.0 <= F, default 3.0]

[experts only]

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

sat-random-seed [type uint64_t, default 0]

sets the random seed for the sat solver

sat-solver [minisat | cadical, default minisat]

[experts only]

choose which sat solver to use, see –sat-solver=help

CDCL(T) SAT solver backend.

Quantifiers Module

cbqi [type bool, default true] (also --no-*)

enable conflict-based quantifier instantiation

cbqi-all-conflict [type bool, default false] (also --no-*)

add all available conflicting instances during conflict-based instantiation

cbqi-mode [conflict | prop-eq, default prop-eq]

what effort to apply conflict find mechanism

Quantifier conflict find modes.

conflict:

Apply QCF algorithm to find conflicts only.

prop-eq:

Apply QCF algorithm to propagate equalities as well as conflicts.

cbqi-skip-rd [type bool, default false] (also --no-*)

[experts only]

optimization, skip instances based on possibly irrelevant portions of quantified formulas

cbqi-tconstraint [type bool, default false] (also --no-*)

[experts only]

enable entailment checks for t-constraints in cbqi algorithm

cbqi-vo-exp [type bool, default false] (also --no-*)

[experts only]

cbqi experimental variable ordering

cegis-sample [none | use | trust, default none]

mode for using samples in the counterexample-guided inductive synthesis loop

Modes for sampling with counterexample-guided inductive synthesis (CEGIS).

none:

Do not use sampling with CEGIS.

use:

Use sampling to accelerate CEGIS. This will rule out solutions for a conjecture when they are not satisfied by a sample point.

trust:

Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures.

cegqi [type bool, default false] (also --no-*)

turns on counterexample-based quantifier instantiation

cegqi-all [type bool, default false] (also --no-*)

[experts only]

apply counterexample-based instantiation to all quantified formulas

cegqi-bv [type bool, default true] (also --no-*)

use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors

cegqi-bv-concat-inv [type bool, default true] (also --no-*)

[experts only]

compute inverse for concat over equalities rather than producing an invertibility condition

cegqi-bv-ineq [eq-slack | eq-boundary | keep, default eq-boundary]

choose mode for handling bit-vector inequalities with counterexample-guided instantiation

Modes for handling bit-vector inequalities in counterexample-guided instantiation.

eq-slack:

Solve for the inequality using the slack value in the model, e.g., t > s becomes t = s + ( t-s )^M.

eq-boundary:

Solve for the boundary point of the inequality, e.g., t > s becomes t = s+1.

keep:

Solve for the inequality directly using side conditions for invertibility.

cegqi-bv-interleave-value [type bool, default false] (also --no-*)

[experts only]

interleave model value instantiation with word-level inversion approach

cegqi-bv-linear [type bool, default true] (also --no-*)

[experts only]

linearize adder chains for variables

cegqi-bv-rm-extract [type bool, default true] (also --no-*)

[experts only]

replaces extract terms with variables for counterexample-guided instantiation for bit-vectors

cegqi-bv-solve-nl [type bool, default false] (also --no-*)

[experts only]

try to solve non-linear bv literals using model value projections

cegqi-full [type bool, default false] (also --no-*)

[experts only]

turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation

cegqi-inf-int [type bool, default false] (also --no-*)

use integer infinity for vts in counterexample-based quantifier instantiation

cegqi-inf-real [type bool, default false] (also --no-*)

use real infinity for vts in counterexample-based quantifier instantiation

cegqi-innermost [type bool, default true] (also --no-*)

only process innermost quantified formulas in counterexample-based quantifier instantiation

cegqi-midpoint [type bool, default false] (also --no-*)

choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation

cegqi-min-bounds [type bool, default false] (also --no-*)

[experts only]

use minimally constrained lower/upper bound for counterexample-based quantifier instantiation

cegqi-multi-inst [type bool, default false] (also --no-*)

[experts only]

when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation

cegqi-nested-qe [type bool, default false] (also --no-*)

process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation

cegqi-nopt [type bool, default true] (also --no-*)

[experts only]

non-optimal bounds for counterexample-based quantifier instantiation

cegqi-round-up-lia [type bool, default false] (also --no-*)

[experts only]

round up integer lower bounds in substitutions for counterexample-based quantifier instantiation

cond-var-split-quant [off | on | agg, default on]

[experts only]

split quantified formulas that lead to variable eliminations

Modes for splitting quantified formulas that lead to variable eliminations.

off:

Do not split quantified formulas.

on:

Split quantified formulas that lead to variable eliminations.

agg:

Aggressively split quantified formulas that lead to variable eliminations.

conjecture-gen [type bool, default false] (also --no-*)

[experts only]

generate candidate conjectures for inductive proofs

conjecture-gen-gt-enum [type int64_t, default 50]

[experts only]

number of ground terms to generate for model filtering

conjecture-gen-max-depth [type int64_t, default 3]

[experts only]

maximum depth of terms to consider for conjectures

conjecture-gen-per-round [type int64_t, default 1]

[experts only]

number of conjectures to generate per instantiation round

cons-exp-triggers [type bool, default false] (also --no-*)

[experts only]

use constructor expansion for single constructor datatypes triggers

dt-stc-ind [type bool, default false] (also --no-*)

[experts only]

apply strengthening for existential quantification over datatypes based on structural induction

dt-var-exp-quant [type bool, default true] (also --no-*)

[experts only]

expand datatype variables bound to one constructor in quantifiers

e-matching [type bool, default true] (also --no-*)

whether to do heuristic E-matching

elim-taut-quant [type bool, default true] (also --no-*)

eliminate tautological disjuncts of quantified formulas

enum-inst [type bool, default false] (also --no-*)

enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown

enum-inst-interleave [type bool, default false] (also --no-*)

interleave enumerative instantiation with other techniques

enum-inst-limit [type int64_t, default -1]

[experts only]

maximum number of rounds of enumerative instantiation to apply (-1 means no limit)

enum-inst-rd [type bool, default true] (also --no-*)

[experts only]

whether to use relevant domain first for enumerative instantiation strategy

enum-inst-stratify [type bool, default false] (also --no-*)

[experts only]

stratify effort levels in enumerative instantiation, which favors speed over fairness

enum-inst-sum [type bool, default false] (also --no-*)

enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum

ext-rewrite-quant [type bool, default false] (also --no-*)

apply extended rewriting to bodies of quantified formulas

finite-model-find [type bool, default false] (also --no-*)

use finite model finding heuristic for quantifier instantiation

fmf-bound [type bool, default false] (also --no-*)

finite model finding on bounded quantification

fmf-bound-blast [type bool, default false] (also --no-*)

[experts only]

send all instantiations for bounded ranges in a single round

fmf-bound-lazy [type bool, default false] (also --no-*)

[experts only]

enforce bounds for bounded quantification lazily via use of proxy variables

fmf-fun [type bool, default false] (also --no-*)

find models for recursively defined functions, assumes functions are admissible

fmf-fun-rlv [type bool, default false] (also --no-*)

find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant

fmf-mbqi [none | fmc | trust, default fmc]

[experts only]

choose mode for model-based quantifier instantiation

Model-based quantifier instantiation modes.

none:

Disable model-based quantifier instantiation.

fmc:

Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability Modulo Theories.

trust:

Do not instantiate quantified formulas (incomplete technique).

fmf-type-completion-thresh [type int64_t, default 1000]

the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted

full-saturate-quant [type bool, default false] (also --no-*)

resort to full effort techniques instead of answering unknown due to limited quantifier reasoning. Currently enables enumerative instantiation

global-negate [type bool, default false] (also --no-*)

[experts only]

do global negation of input formula

ho-elim [type bool, default false] (also --no-*)

eagerly eliminate higher-order constraints

ho-elim-store-ax [type bool, default true] (also --no-*)

use store axiom during ho-elim

ho-matching [type bool, default true] (also --no-*)

[experts only]

do higher-order matching algorithm for triggers with variable operators

ho-merge-term-db [type bool, default true] (also --no-*)

[experts only]

merge term indices modulo equality

ieval [off | use | use-learn, default use]

mode for using instantiation evaluation

Mode for using instantiation evaluation.

off:

Do not use instantiation evaluation.

use:

Use instantiation evaluation.

use-learn:

Use instantiation evaluation, and generalize learning.

increment-triggers [type bool, default true] (also --no-*)

[experts only]

generate additional triggers as needed during search

inst-max-level [type int64_t, default -1]

[experts only]

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

inst-max-rounds [type int64_t, default -1]

maximum number of instantiation rounds (-1 == no limit, default)

inst-no-entail [type bool, default true] (also --no-*)

do not consider instances of quantified formulas that are currently entailed

inst-when [full | full-delay | full-last-call | full-delay-last-call | last-call, default full-last-call]

when to apply instantiation

Instantiation modes.

full:

Run instantiation round at full effort, before theory combination.

full-delay:

Run instantiation round at full effort, before theory combination, after all other theories have finished.

full-last-call:

Alternate running instantiation rounds at full effort and last call. In other words, interleave instantiation and theory combination.

full-delay-last-call:

Alternate running instantiation rounds at full effort after all other theories have finished, and last call.

last-call:

Run instantiation at last call effort, after theory combination and and theories report sat.

inst-when-phase [type int64_t, default 2]

[experts only]

instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen

int-wf-ind [type bool, default false] (also --no-*)

[experts only]

apply strengthening for integers based on well-founded induction

ite-dtt-split-quant [type bool, default false] (also --no-*)

[experts only]

split ites with dt testers as conditions

ite-lift-quant [none | simple | all, default simple]

ite lifting mode for quantified formulas

ITE lifting modes for quantified formulas.

none:

Do not lift if-then-else in quantified formulas.

simple:

Lift if-then-else in quantified formulas if results in smaller term size.

all:

Lift if-then-else in quantified formulas.

literal-matching [none | use | agg-predicate | agg, default use]

[experts only]

choose literal matching mode

Literal match modes.

none:

Do not use literal matching.

use:

Consider phase requirements of triggers conservatively. For example, the trigger P( x ) in forall( x ). ( P( x ) V ~Q( x ) ) will not be matched with terms in the equivalence class of true, and likewise Q( x ) will not be matched terms in the equivalence class of false. Extends to equality.

agg-predicate:

Consider phase requirements aggressively for predicates. In the above example, only match P( x ) with terms that are in the equivalence class of false.

agg:

Consider the phase requirements aggressively for all triggers.

macros-quant [type bool, default false] (also --no-*)

perform quantifiers macro expansion

macros-quant-mode [all | ground | ground-uf, default ground-uf]

mode for quantifiers macro expansion

Modes for quantifiers macro expansion.

all:

Infer definitions for functions, including those containing quantified formulas.

ground:

Only infer ground definitions for functions.

ground-uf:

Only infer ground definitions for functions that result in triggers for all free variables.

mbqi [type bool, default false] (also --no-*)

[experts only]

use model-based quantifier instantiation

mbqi-fast-sygus [type bool, default false] (also --no-*)

[experts only]

use fast enumeration to augment instantiations from MBQI

mbqi-interleave [type bool, default false] (also --no-*)

[experts only]

interleave model-based quantifier instantiation with other techniques

mbqi-one-inst-per-round [type bool, default false] (also --no-*)

only add one instantiation per quantifier per round for mbqi

miniscope-quant [off | conj | fv | conj-and-fv | agg, default conj-and-fv]

miniscope mode for quantified formulas

Miniscope quantifiers modes.

off:

Do not miniscope quantifiers.

conj:

Use miniscoping of conjunctions only.

fv:

Use free variable miniscoping only.

conj-and-fv:

Enable both conjunction and free variable miniscoping.

agg:

Enable aggressive miniscope, which further may rewrite quantified formulas into a form where miniscoping is possible.

miniscope-quant-user [type bool, default false] (also --no-*)

miniscope quantified formulas with user patterns

multi-trigger-cache [type bool, default false] (also --no-*)

caching version of multi triggers

multi-trigger-linear [type bool, default true] (also --no-*)

implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms

multi-trigger-priority [type bool, default false] (also --no-*)

only try multi triggers if single triggers give no instantiations

multi-trigger-when-single [type bool, default false] (also --no-*)

select multi triggers when single triggers exist

oracles [type bool, default false] (also --no-*)

[experts only]

Enable interface to external oracles

partial-triggers [type bool, default false] (also --no-*)

[experts only]

use triggers that do not contain all free variables

pool-inst [type bool, default true] (also --no-*)

[experts only]

pool-based instantiation: instantiate with ground terms occurring in user-specified pools

pre-skolem-quant [off | on | agg, default off]

modes to apply skolemization eagerly to bodies of quantified formulas

Modes to apply skolemization eagerly to bodies of quantified formulas.

off:

Do not apply Skolemization eagerly.

on:

Apply Skolemization eagerly to top-level (negatively asserted) quantified formulas.

agg:

Apply Skolemization eagerly and aggressively during preprocessing.

pre-skolem-quant-nested [type bool, default true] (also --no-*)

[experts only]

apply skolemization to nested quantified formulas

prenex-quant [none | simple | norm, default simple]

prenex mode for quantified formulas

Prenex quantifiers modes.

none:

Do not prenex nested quantifiers.

simple:

Do simple prenexing of same sign quantifiers.

norm:

Prenex to prenex normal form.

prenex-quant-user [type bool, default false] (also --no-*)

prenex quantified formulas with user patterns

print-inst-full [type bool, default true] (also --no-*)

print instantiations for formulas that do not have given identifiers

purify-triggers [type bool, default false] (also --no-*)

[experts only]

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

quant-alpha-equiv [type bool, default true] (also --no-*)

infer alpha equivalence between quantified formulas

quant-dsplit [none | default | agg, default default]

mode for dynamic quantifiers splitting

Modes for quantifiers splitting.

none:

Never split quantified formulas.

default:

Split quantified formulas over some finite datatypes when finite model finding is enabled.

agg:

Aggressively split quantified formulas.

quant-fun-wd [type bool, default false] (also --no-*)

[experts only]

assume that function defined by quantifiers are well defined

quant-ind [type bool, default false] (also --no-*)

[experts only]

use all available techniques for inductive reasoning

quant-rep-mode [ee | first | depth, default first]

[experts only]

selection mode for representatives in quantifiers engine

Modes for quantifiers representative selection.

ee:

Let equality engine choose representatives.

first:

Choose terms that appear first.

depth:

Choose terms that are of minimal depth.

register-quant-body-terms [type bool, default false] (also --no-*)

[experts only]

consider ground terms within bodies of quantified formulas for matching

relational-triggers [type bool, default false] (also --no-*)

[experts only]

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

relevant-triggers [type bool, default false] (also --no-*)

prefer triggers that are more relevant based on SInE style analysis

sub-cbqi [type bool, default false] (also --no-*)

Enable conflict-based instantiation subsolver strategy

sub-cbqi-timeout [type uint64_t, default 0]

Timeout (in milliseconds) for subsolver calls for sub-cbqi

sygus [type bool, default false] (also --no-*)

support SyGuS commands

sygus-add-const-grammar [type bool, default true] (also --no-*)

statically add constants appearing in conjecture to grammars

sygus-arg-relevant [type bool, default false] (also --no-*)

[experts only]

static inference techniques for computing whether arguments of functions-to-synthesize are relevant

sygus-auto-unfold [type bool, default true] (also --no-*)

[experts only]

enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems

sygus-bool-ite-return-const [type bool, default true] (also --no-*)

[experts only]

Only use Boolean constants for return values in unification-based function synthesis

sygus-core-connective [type bool, default true] (also --no-*)

use unsat core analysis to construct Boolean connective to sygus conjectures

sygus-crepair-abort [type bool, default false] (also --no-*)

[experts only]

abort if constant repair techniques are not applicable

sygus-enum [smart | fast | random | var-agnostic | auto, default auto]

mode for sygus enumeration

Modes for sygus enumeration.

smart:

Use smart enumeration based on datatype constraints.

fast:

Use optimized enumerator for sygus enumeration.

random:

Use basic random enumerator for sygus enumeration.

var-agnostic:

Use sygus solver to enumerate terms that are agnostic to variables.

auto:

Internally decide the best policy for each enumerator.

sygus-enum-fast-num-consts [type uint64_t, default 5]

[experts only]

the branching factor for the number of interpreted constants to consider for each size when using –sygus-enum=fast

sygus-enum-random-p [type double, 0.0 <= P <= 1.0, default 0.5]

[experts only]

the parameter of the geometric distribution used to determine the size of terms generated by –sygus-enum=random

sygus-eval-unfold [none | single | single-bool | multi, default single-bool]

modes for sygus evaluation unfolding

Modes for sygus evaluation unfolding.

none:

Do not use sygus evaluation unfolding.

single:

Do single-step unfolding for all evaluation functions.

single-bool:

Do single-step unfolding for Boolean functions and ITEs, and multi-step unfolding for all others.

multi:

Do multi-step unfolding for all evaluation functions.

sygus-expr-miner-check-timeout [type uint64_t, default 0]

[experts only]

timeout (in milliseconds) for satisfiability checks in expression miners

sygus-filter-sol [none | strong | weak, default none]

[experts only]

mode for filtering sygus solutions

Modes for filtering sygus solutions.

none:

Do not filter sygus solutions.

strong:

Filter solutions that are logically stronger than others.

weak:

Filter solutions that are logically weaker than others.

sygus-filter-sol-rev [type bool, default false] (also --no-*)

[experts only]

compute backwards filtering to compute whether previous solutions are filtered based on later ones

sygus-grammar-cons [simple | any-const | any-term | any-term-concise, default simple]

mode for SyGuS grammar construction

Modes for default SyGuS grammars.

simple:

Use simple grammar construction (no symbolic terms or constants).

any-const:

Use symoblic constant constructors.

any-term:

When applicable, use constructors corresponding to any symbolic term. This option enables a sum-of-monomials grammar for arithmetic. For all other types, it enables symbolic constant constructors.

any-term-concise:

When applicable, use constructors corresponding to any symbolic term, favoring conciseness over generality. This option is equivalent to any-term but enables a polynomial grammar for arithmetic when not in a combined theory.

sygus-grammar-norm [type bool, default false] (also --no-*)

[experts only]

statically normalize sygus grammars based on flattening (linearization)

sygus-grammar-use-disj [type bool, default true] (also --no-*)

[experts only]

use disjunctions in internally generated grammars. this is set to false when solving abduction queries.

sygus-inference [off | try | on, default off]

[experts only]

mode for preprocessing arbitrary inputs to sygus conjectures

Modes for preprocessing arbitrary inputs to sygus conjectures.

off:

Do not use sygus inference techniques.

try:

Try to use sygus inference techniques but resort to ordinary SMT solving if it does not apply.

on:

Try to sygus inference and abort if it does not apply.

sygus-inst [type bool, default false] (also --no-*)

Enable SyGuS instantiation quantifiers module

sygus-inst-mode [priority-inst | priority-eval | interleave, default priority-inst]

[experts only]

select instantiation lemma mode

SyGuS instantiation lemma modes.

priority-inst:

add instantiation lemmas first, add evaluation unfolding if instantiation fails.

priority-eval:

add evaluation unfolding lemma first, add instantiation lemma if unfolding lemmas already added.

interleave:

add instantiation and evaluation unfolding lemmas in the same step.

sygus-inst-scope [in | out | both, default in]

[experts only]

select scope of ground terms

scope for collecting ground terms for the grammar.

in:

use ground terms inside given quantified formula only.

out:

use ground terms outside of quantified formulas only.

both:

combines inside and outside.

sygus-inst-term-sel [min | max | both, default min]

[experts only]

granularity for ground terms

Ground term selection modes.

min:

collect minimal ground terms only.

max:

collect maximal ground terms only.

both:

combines minimal and maximal .

sygus-inv-templ [none | pre | post, default post]

template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)

Template modes for sygus invariant synthesis.

none:

Synthesize invariant directly.

pre:

Synthesize invariant based on weakening of precondition.

post:

Synthesize invariant based on strengthening of postcondition.

sygus-inv-templ-when-sg [type bool, default false] (also --no-*)

[experts only]

use invariant templates (with solution reconstruction) for syntax guided problems

sygus-min-grammar [type bool, default true] (also --no-*)

statically minimize sygus grammars

sygus-out [status | status-and-def | sygus-standard, default sygus-standard]

output mode for sygus

Modes for sygus solution output.

status:

Print only status for check-synth calls.

status-and-def:

Print status followed by definition corresponding to solution.

sygus-standard:

Print based on SyGuS standard.

sygus-pbe [type bool, default true] (also --no-*)

enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures

sygus-pbe-multi-fair [type bool, default false] (also --no-*)

[experts only]

when using multiple enumerators, ensure that we only register value of minimial term size

sygus-pbe-multi-fair-diff [type int64_t, default 0]

[experts only]

when using multiple enumerators, ensure that we only register values of minimial term size plus this value (default 0)

sygus-qe-preproc [type bool, default false] (also --no-*)

[experts only]

use quantifier elimination as a preprocessing step for sygus

sygus-query-gen [basic | sample-sat | unsat, default basic]

[experts only]

mode for generating interesting satisfiability queries using SyGuS, for internal fuzzing

Modes for generating interesting satisfiability queries using SyGuS.

basic:

Generate all queries using SyGuS enumeration of the given grammar

sample-sat:

Generate interesting SAT queries based on sampling, for e.g. soundness testing.

unsat:

Generate interesting UNSAT queries, for e.g. proof testing.

sygus-query-gen-dump-files [none | all | unsolved, default none]

[experts only]

mode for dumping external files corresponding to interesting satisfiability queries with sygus-query-gen

Query file options.

none:

Do not dump query files when using –sygus-query-gen.

all:

Dump all query files.

unsolved:

Dump query files that the subsolver did not solve.

sygus-query-gen-filter-solved [type bool, default false] (also --no-*)

[experts only]

do not print queries that are solved

sygus-query-gen-thresh [type uint64_t, default 5]

[experts only]

number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen

sygus-rec-fun [type bool, default true] (also --no-*)

[experts only]

enable efficient support for recursive functions in sygus grammars

sygus-rec-fun-eval-limit [type uint64_t, default 1000]

[experts only]

use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)

sygus-repair-const [type bool, default true] (also --no-*)

use approach to repair constants in sygus candidate solutions

sygus-repair-const-timeout [type uint64_t, default 0]

[experts only]

timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions

sygus-rr-synth-accel [type bool, default false] (also --no-*)

[experts only]

add dynamic symmetry breaking clauses based on candidate rewrites

sygus-rr-synth-check [type bool, default true] (also --no-*)

[experts only]

use satisfiability check to verify correctness of candidate rewrites

sygus-rr-synth-filter-cong [type bool, default true] (also --no-*)

[experts only]

filter candidate rewrites based on congruence

sygus-rr-synth-filter-match [type bool, default true] (also --no-*)

[experts only]

filter candidate rewrites based on matching

sygus-rr-synth-filter-nl [type bool, default false] (also --no-*)

[experts only]

filter non-linear candidate rewrites

sygus-rr-synth-filter-order [type bool, default true] (also --no-*)

[experts only]

filter candidate rewrites based on variable ordering

sygus-rr-synth-input-nvars [type int64_t, default 3]

[experts only]

the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input

sygus-rr-synth-rec [type bool, default false] (also --no-*)

[experts only]

synthesize rewrite rules over all sygus grammar types recursively

sygus-sample-fp-uniform [type bool, default false] (also --no-*)

[experts only]

sample floating-point values uniformly instead of in a biased fashion

sygus-sample-grammar [type bool, default true] (also --no-*)

[experts only]

when applicable, use grammar for choosing sample points

sygus-samples [type int64_t, default 1000]

[experts only]

number of points to consider when doing sygus rewriter sample testing

sygus-si [none | use | all, default none]

mode for processing single invocation synthesis conjectures

Modes for single invocation techniques.

none:

Do not use single invocation techniques.

use:

Use single invocation techniques only if grammar is not restrictive.

all:

Always use single invocation techniques.

sygus-si-abort [type bool, default false] (also --no-*)

abort if synthesis conjecture is not single invocation

sygus-si-rcons [none | try | all-limit | all, default all]

policy for reconstructing solutions for single invocation conjectures

Modes for reconstruction solutions while using single invocation techniques.

none:

Do not try to reconstruct solutions in the original (user-provided) grammar when using single invocation techniques. In this mode, solutions produced by cvc5 may violate grammar restrictions.

try:

Try to reconstruct solutions in the original grammar when using single invocation techniques in an incomplete (fail-fast) manner.

all-limit:

Try to reconstruct solutions in the original grammar, but terminate if a maximum number of rounds for reconstruction is exceeded.

all:

Try to reconstruct solutions in the original grammar. In this mode, we do not terminate until a solution is successfully reconstructed.

sygus-si-rcons-limit [type int64_t, default 10000]

[experts only]

number of rounds of enumeration to use during solution reconstruction (negative means unlimited)

sygus-si-rcons-p [type double, 0.0 <= P <= 1.0, default 0.5]

[experts only]

the parameter of the geometric distribution used to determine the number of unification patterns generated by single invocation techniques.

sygus-stream [type bool, default false] (also --no-*)

enumerate a stream of solutions instead of terminating after the first one

sygus-unif-cond-independent-no-repeat-sol [type bool, default true] (also --no-*)

[experts only]

Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis

sygus-unif-pi [none | complete | cond-enum | cond-enum-igain, default none]

mode for synthesis via piecewise-indepedent unification

Modes for piecewise-independent unification.

none:

Do not use piecewise-independent unification.

complete:

Use complete approach for piecewise-independent unification (see Section 3 of Barbosa et al FMCAD 2019)

cond-enum:

Use unconstrained condition enumeration for piecewise-independent unification (see Section 4 of Barbosa et al FMCAD 2019).

cond-enum-igain:

Same as cond-enum, but additionally uses an information gain heuristic when doing decision tree learning.

sygus-unif-shuffle-cond [type bool, default false] (also --no-*)

[experts only]

Shuffle condition pool when building solutions (may change solutions sizes)

sygus-verify-inst-max-rounds [type int64_t, default 10]

[experts only]

maximum number of instantiation rounds for sygus verification calls (-1 == no limit, default is 10)

sygus-verify-timeout [type uint64_t, default 0]

timeout (in milliseconds) for verifying satisfiability of synthesized terms

term-db-mode [all | relevant, default all]

which ground terms to consider for instantiation

Modes for terms included in the quantifiers term database.

all:

Quantifiers module considers all ground terms.

relevant:

Quantifiers module considers only ground terms connected to current assertions.

trigger-active-sel [all | min | max, default all]

[experts only]

selection mode to activate triggers

Trigger active selection modes.

all:

Make all triggers active.

min:

Activate triggers with minimal ground terms.

max:

Activate triggers with maximal ground terms.

trigger-sel [min | max | min-s-max | min-s-all | all, default min]

selection mode for triggers

Trigger selection modes.

min:

Consider only minimal subterms that meet criteria for triggers.

max:

Consider only maximal subterms that meet criteria for triggers.

min-s-max:

Consider only minimal subterms that meet criteria for single triggers, maximal otherwise.

min-s-all:

Consider only minimal subterms that meet criteria for single triggers, all otherwise.

all:

Consider all subterms that meet criteria for triggers.

user-pat [use | trust | strict | resort | ignore | interleave, default trust]

policy for handling user-provided patterns for quantifier instantiation

These modes determine how user provided patterns (triggers) are used during E-matching. The modes vary on when instantiation based on user-provided triggers is combined with instantiation based on automatically selected triggers.

use:

Use both user-provided and auto-generated patterns when patterns are provided for a quantified formula.

trust:

When provided, use only user-provided patterns for a quantified formula.

strict:

When provided, use only user-provided patterns for a quantified formula, and do not use any other instantiation techniques.

resort:

Use user-provided patterns only after auto-generated patterns saturate.

ignore:

Ignore user-provided patterns.

interleave:

Alternate between use/resort.

user-pool [use | trust | ignore, default trust]

[experts only]

policy for handling user-provided pools for quantifier instantiation

These modes determine how user provided pools are used in combination with other instantiation techniques.

use:

Use both user-provided pool and other instantiation strategies when pools are provided for a quantified formula.

trust:

When provided, use only user-provided pool for a quantified formula.

ignore:

Ignore user-provided pool.

var-elim-quant [type bool, default true] (also --no-*)

enable simple variable elimination for quantified formulas

var-ineq-elim-quant [type bool, default true] (also --no-*)

enable variable elimination based on infinite projection of unbound arithmetic variables

Separation Logic Theory Module

sep-min-refine [type bool, default false] (also --no-*)

[experts only]

only add refinement lemmas for minimal (innermost) assertions

sep-pre-skolem-emp [type bool, default false] (also --no-*)

[experts only]

eliminate emp constraint at preprocess time

Sets Theory Module

sets-ext [type bool, default false] (also --no-*)

enable extended symbols such as complement and universe in theory of sets

sets-proxy-lemmas [type bool, default false] (also --no-*)

[experts only]

introduce proxy variables eagerly to shorten lemmas

SMT Layer Module

abstract-values [type bool, default false] (also --no-*)

[experts only]

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

ackermann [type bool, default false] (also --no-*)

eliminate functions by ackermannization

bv-to-int-use-pow2 [type bool, default false] (also --no-*)

[experts only]

use internal pow2 operator when translating shift notes

bvand-integer-granularity [type uint64_t, 1 <= N <= 8, default 1]

[experts only]

granularity to use in –solve-bv-as-int mode and for iand operator (experimental)

check-abducts [type bool, default false] (also --no-*)

checks whether produced solutions to get-abduct are correct

check-interpolants [type bool, default false] (also --no-*)

checks whether produced solutions to get-interpolant are correct

check-proofs [type bool, default false] (also --no-*)

after UNSAT/VALID, check the generated proof (with proof)

check-synth-sol [type bool, default false] (also --no-*)

checks whether produced solutions to functions-to-synthesize satisfy the conjecture

check-unsat-cores [type bool, default false] (also --no-*)

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

debug-check-models [type bool, default false] (also --no-*)

[experts only]

after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions

deep-restart [none | input | input-and-solvable | input-and-prop | all, default none]

[experts only]

mode for deep restarts

Mode for deep restarts

none:

do not use deep restart

input:

learn literals that appear in the input

input-and-solvable:

learn literals that appear in the input and those that can be solved for variables that appear in the input

input-and-prop:

learn literals that appear in the input and those that can be solved for variables, or correspond to constant propagations for terms that appear in the input

all:

learn all literals

deep-restart-factor [type double, 0.0 <= F <= 1000.0, default 3.0]

[experts only]

sets the threshold for average assertions per literal before a deep restart

difficulty-mode [lemma-literal | lemma-literal-all | model-check, default lemma-literal-all]

[experts only]

choose output mode for get-difficulty, see –difficulty-mode=help

difficulty output modes.

lemma-literal:

Difficulty of an assertion is how many lemmas (at full effort) use a literal that the assertion depends on to be satisfied.

lemma-literal-all:

Difficulty of an assertion is how many lemmas use a literal that the assertion depends on to be satisfied.

model-check:

Difficulty of an assertion is how many times it was not satisfied in a candidate model.

early-ite-removal [type bool, default false] (also --no-*)

[experts only]

remove ITEs early in preprocessing

ext-rew-prep [off | use | agg, default off]

mode for using extended rewriter as a preprocessing pass, see –ext-rew-prep=help

extended rewriter preprocessing pass modes.

off:

do not use extended rewriter as a preprocessing pass.

use:

use extended rewriter as a preprocessing pass.

agg:

use aggressive extended rewriter as a preprocessing pass.

foreign-theory-rewrite [type bool, default false] (also --no-*)

[experts only]

Cross-theory rewrites

iand-mode [value | sum | bitwise, default value]

[experts only]

Set the refinement scheme for integer AND

Refinement modes for integer AND

value:

value-based refinement

sum:

use sum to represent integer AND in refinement

bitwise:

use bitwise comparisons on binary representation of integer for refinement (experimental)

interpolants-mode [default | assumptions | conjecture | shared | all, default default]

choose interpolants production mode, see –interpolants-mode=help

Interpolants grammar mode

default:

use the default grammar for the theory or the user-defined grammar if given

assumptions:

use only operators that occur in the assumptions

conjecture:

use only operators that occur in the conjecture

shared:

use only operators that occur both in the assumptions and the conjecture

all:

use only operators that occur either in the assumptions or the conjecture

ite-simp [type bool, default false] (also --no-*)

[experts only]

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

learned-rewrite [type bool, default false] (also --no-*)

rewrite the input based on learned literals

minimal-unsat-cores [type bool, default false] (also --no-*)

[experts only]

if an unsat core is produced, it is reduced to a minimal unsat core

model-cores [none | simple | non-implied, default none]

mode for producing model cores

Model cores modes.

none:

Do not compute model cores.

simple:

Only include a subset of variables whose values are sufficient to show the input formula is satisfied by the given model.

non-implied:

Only include a subset of variables whose values, in addition to the values of variables whose values are implied, are sufficient to show the input formula is satisfied by the given model.

model-var-elim-uneval [type bool, default true] (also --no-*)

[experts only]

allow variable elimination based on unevaluatable terms to variables

on-repeat-ite-simp [type bool, default false] (also --no-*)

[experts only]

do the ite simplification pass again if repeating simplification

print-cores-full [type bool, default false] (also --no-*)

print all formulas regardless of whether they are named, e.g. in unsat cores

produce-abducts [type bool, default false] (also --no-*)

support the get-abduct command

produce-assertions | interactive-mode [type bool, default true] (also --no-*)

keep an assertions list. Note this option is always enabled.

produce-assignments [type bool, default false] (also --no-*)

support the get-assignment command

produce-difficulty [type bool, default false] (also --no-*)

enable tracking of difficulty.

produce-interpolants [type bool, default false] (also --no-*)

turn on interpolation generation.

produce-learned-literals [type bool, default false] (also --no-*)

produce learned literals, support get-learned-literals

produce-proofs [type bool, default false] (also --no-*)

produce proofs, support check-proofs and get-proof

produce-unsat-assumptions [type bool, default false] (also --no-*)

turn on unsat assumptions generation

produce-unsat-cores [type bool, default false] (also --no-*)

turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs.

proof-mode [off | pp-only | sat-proof | full-proof, default off]

[experts only]

choose proof mode, see –proof-mode=help

proof modes.

repeat-simp [type bool, default false] (also --no-*)

[experts only]

make multiple passes with nonclausal simplifier

simp-ite-compress [type bool, default false] (also --no-*)

[experts only]

enables compressing ites after ite simplification

simp-with-care [type bool, default false] (also --no-*)

[experts only]

enables simplifyWithCare in ite simplificiation

simplification | simplification-mode [none | batch, default batch]

choose simplification mode, see –simplification=help

Simplification modes.

none:

Do not perform nonclausal simplification.

batch:

Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (CHECKSAT or QUERY or predicate SUBTYPE declaration).

simplification-bcp [type bool, default false] (also --no-*)

[experts only]

apply Boolean constant propagation as a substitution during simplification

solve-bv-as-int [off | sum | iand | bv | bitwise, default off]

mode for translating BVAnd to integer

solve-bv-as-int modes.

off:

Do not translate bit-vectors to integers

sum:

Generate a sum expression for each bvand instance, based on the value in –solve-bv-as-int-granularity

iand:

Translate bvand to the iand operator

bv:

Translate bvand back to bit-vectors

bitwise:

Introduce a UF operator for bvand, and eagerly add bitwise lemmas

solve-int-as-bv [type uint64_t, N <= 4294967295, default 0]

attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)

solve-real-as-int [type bool, default false] (also --no-*)

attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)

sort-inference [type bool, default false] (also --no-*)

calculate sort inference of input problem, convert the input based on monotonic sorts

static-learning [type bool, default true] (also --no-*)

use static learning (on by default)

timeout-core-timeout [type uint64_t, default 10000]

[experts only]

timeout (in milliseconds) for satisfiability checks for timeout cores

unconstrained-simp [type bool, default false] (also --no-*)

turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis). Fully supported only in (subsets of) the logic QF_ABV.

unsat-cores-mode [off | sat-proof | assumptions, default off]

[experts only]

choose unsat core mode, see –unsat-cores-mode=help

unsat cores modes.

off:

Do not produce unsat cores.

sat-proof:

Produce unsat cores from the SAT proof and prepocessing proofs.

assumptions:

Produce unsat cores using solving under assumptions and preprocessing proofs.

Strings Theory Module

re-elim [off | on | agg, default off]

regular expression elimination mode

Regular expression elimination modes.

off:

Do not use regular expression elimination.

on:

Use regular expression elimination.

agg:

Use aggressive regular expression elimination.

re-inter-mode [all | constant | one-constant | none, default none]

[experts only]

determines which regular expressions intersections to compute

Regular expression intersection modes.

all:

Compute intersections for all regular expressions.

constant:

Compute intersections only between regular expressions that do not contain re.allchar or re.range.

one-constant:

Compute intersections only between regular expressions such that at least one side does not contain re.allchar or re.range.

none:

Do not compute intersections for regular expressions.

seq-array [lazy | eager | none, default none]

[experts only]

use array-inspired solver for sequence updates in eager or lazy mode

use array-inspired solver for sequence updates in eager or lazy mode

lazy:

use array-inspired solver for sequence updates in lazy mode

eager:

use array-inspired solver for sequence updates in eager mode

none:

do not use array-inspired solver for sequence updates

strings-alpha-card [type uint64_t, N <= 196608, default 196608]

[experts only]

the assumed cardinality of the alphabet of characters for strings, which is a prefix of the interval of unicode code points in the SMT-LIB standard

strings-check-entail-len [type bool, default true] (also --no-*)

check entailment between length terms to reduce splitting

strings-code-elim [type bool, default false] (also --no-*)

[experts only]

eliminate code points during preprocessing

strings-deq-ext [type bool, default false] (also --no-*)

use extensionality for string disequalities

strings-eager-eval [type bool, default true] (also --no-*)

perform eager context-dependent evaluation for applications of string kinds in the equality engine

strings-eager-len-re [type bool, default false] (also --no-*)

use regular expressions for eager length conflicts

strings-eager-reg [type bool, default true] (also --no-*)

[experts only]

do registration lemmas for terms during preregistration. If false, do registration lemmas for terms when they appear in asserted literals

strings-eager-solver [type bool, default true] (also --no-*)

use the eager solver

strings-exp [type bool, default false] (also --no-*)

experimental features in the theory of strings

strings-ff [type bool, default true] (also --no-*)

[experts only]

do flat form inferences

strings-fmf [type bool, default false] (also --no-*)

the finite model finding used by the theory of strings

strings-infer-as-lemmas [type bool, default false] (also --no-*)

[experts only]

always send lemmas out instead of making internal inferences

strings-infer-sym [type bool, default true] (also --no-*)

[experts only]

generalized inferences in strings based on proxy symbols

strings-lazy-pp [type bool, default true] (also --no-*)

perform string preprocessing lazily

strings-len-norm [type bool, default true] (also --no-*)

[experts only]

strings length normalization lemma

strings-mbr [type bool, default true] (also --no-*)

use models to avoid reductions for extended functions that introduce quantified formulas

strings-model-max-len [type uint64_t, N <= 2147483647, default 65536]

[experts only]

The maximum size of string values in models

strings-process-loop-mode [full | simple | simple-abort | none | abort, default full]

determines how to process looping string equations

Loop processing modes.

full:

Perform full processing of looping word equations.

simple:

Omit normal loop breaking (default with –strings-fmf).

simple-abort:

Abort when normal loop breaking is required.

none:

Omit loop processing.

abort:

Abort if looping word equations are encountered.

strings-re-posc-eager [type bool, default false] (also --no-*)

[experts only]

eager reduction of positive membership into concatenation

strings-regexp-inclusion [type bool, default true] (also --no-*)

use regular expression inclusion for finding conflicts and avoiding regular expression unfolding

strings-rexplain-lemmas [type bool, default true] (also --no-*)

[experts only]

regression explanations for string lemmas

Theory Layer Module

assign-function-values [type bool, default true] (also --no-*)

[experts only]

assign values for uninterpreted functions in models

condense-function-values [type bool, default true] (also --no-*)

[experts only]

condense values for functions in models rather than explicitly representing them

ee-mode [distributed | central, default distributed]

[experts only]

mode for managing equalities across theory solvers

Defines mode for managing equalities across theory solvers.

distributed:

Each theory maintains its own equality engine.

central:

All applicable theories use the central equality engine.

lemma-inprocess [full | light | none, default none]

[experts only]

Modes for inprocessing lemmas.

Modes for inprocessing lemmas.

full:

Full inprocessing.

light:

Light inprocessing.

none:

No inprocessing.

lemma-inprocess-infer-eq-lit [type bool, default false] (also --no-*)

[experts only]

Infer equivalent literals when using lemma inprocess

lemma-inprocess-subs [all | simple, default simple]

[experts only]

Modes for substitutions for inprocessing lemmas.

Modes for substitutions for inprocessing lemmas.

all:

All substitutions.

simple:

Simple substitutions.

relevance-filter [type bool, default false] (also --no-*)

[experts only]

enable analysis of relevance of asserted literals with respect to the input formula

tc-mode [care-graph, default care-graph]

[experts only]

mode for theory combination

Defines mode for theory combination.

care-graph:

Use care graphs for theory combination.

theoryof-mode [type | term, default type]

[experts only]

mode for Theory::theoryof()

Defines how we associate theories with terms.

type:

Type variables, constants and equalities by type.

term:

Type variables as uninterpreted, type constants by theory, equalities by the parametric theory.

Uninterpreted Functions Theory Module

eager-arith-bv-conv [type bool, default false] (also --no-*)

[experts only]

eagerly expand bit-vector to arithmetic conversions during preprocessing

model-based-arith-bv-conv [type bool, default false] (also --no-*)

[experts only]

model-based inferences for bit-vector to arithmetic conversions

symmetry-breaker [type bool, default false] (also --no-*)

[experts only]

use UF symmetry breaker (Deharbe et al., CADE 2011)

uf-ho-ext [type bool, default true] (also --no-*)

[experts only]

apply extensionality on function symbols

uf-lambda-qe [type bool, default false] (also --no-*)

[experts only]

apply quantifier elimination eagerly when two lambdas are equated

uf-lazy-ll [type bool, default true] (also --no-*)

do lambda lifting lazily

uf-ss [full | no-minimal | none, default full]

mode of operation for uf with cardinality solver.

UF with cardinality options currently supported by the –uf-ss option when combined with finite model finding.

full:

Default, use UF with cardinality to find minimal models for uninterpreted sorts.

no-minimal:

Use UF with cardinality to shrink models, but do no enforce minimality.

none:

Do not use UF with cardinality to shrink model sizes.

uf-ss-abort-card [type int64_t, default -1]

tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)

uf-ss-fair [type bool, default true] (also --no-*)

use fair strategy for finite model finding multiple sorts

uf-ss-fair-monotone [type bool, default false] (also --no-*)

[experts only]

group monotone sorts when enforcing fairness for finite model finding