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

[experts only]

(experimental) whether to use the congruence manager when the equality solver is enabled

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

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 agressively

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 

d | debug [type string ]

debug something (e.g. -d arith), can repeat

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.

rweight [type string ]

[experts only]

set a single resource weight

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

[experts only]

enable rewrite pushing extract [i:0] over arithmetic operations (can blow up)

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

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 

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

[experts only]

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

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)

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

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

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

[experts only]

spin on segfault/other crash waiting for gdb

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

[experts only]

show all available tags for debugging

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

[experts only]

show all available tags for tracing

Parser Module 

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

[experts only]

limits the file system access if set to false

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

force all declarations and definitions to be global

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

[experts only]

enable semantic checks, including type checks

Printing Module 

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

print instantiations for formulas that do not have given identifiers

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

when printing unsat cores, include unlabeled assertions

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.

Proof Module 

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 lazy ]

[experts only]

select proof checking mode

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-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-format-mode [ none | dot | lfsc | alethe | tptp , default none ]

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

tptp

Output TPTP proof (work in progress)

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

modes for proof granularity

Modes for proof granularity.

macro

Allow macros. Do not improve the granularity of proofs.

rewrite

Allow rewrite or substitution steps, expand macros.

theory-rewrite

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

dsl-rewrite

Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory 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

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.

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

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-eager-check-rd [type bool , default true ] (also --no-* )

[experts only]

optimization, eagerly check relevant domain of matched position

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

[experts only]

optimization, test cbqi instances eagerly

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-filter-active-terms [type bool , default true ] (also --no-* )

[experts only]

filter based on active terms

conjecture-filter-canonical [type bool , default true ] (also --no-* )

[experts only]

filter based on canonicity

conjecture-filter-model [type bool , default true ] (also --no-* )

[experts only]

filter based on model

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

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 [ 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).

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.

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

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

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

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

[experts only]

attempt to preprocess arbitrary inputs to sygus conjectures

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-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 [ none | basic | sample-sat | unsat , default none ]

[experts only]

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

Modes for generating interesting satisfiability queries using SyGuS.

none

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

[experts only]

use sygus to enumerate candidate rewrite rules

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

[experts only]

synthesize rewrite rules based on the input formula

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

[experts only]

synthesize Boolean rewrite rules based on the input formula

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

[experts only]

synthesize rewrite rules over all sygus grammar types recursively

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

[experts only]

use sygus to verify the correctness of rewrite rules via sampling

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-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 3 ]

[experts only]

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

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

timeout (in milliseconds) for verifying satisfiability of synthesized terms

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

[experts only]

register terms in term database based on the SAT context

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.

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-infer-as-lemmas [type bool , default true ] (also --no-* )

[experts only]

send inferences as lemmas

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

bvand-integer-granularity [type uint64_t , 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

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

[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

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

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

[experts only]

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 –solbv-bv-as-int-granularity

iand

Translate bvand to the iand operator (experimental)

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

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 constant ]

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

use extensionality for string disequalities

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

[experts only]

strings eager check

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

perform eager context-dependent evaluation for applications of string kinds

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

[experts only]

strings eager length lemmas

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

use regular expressions for eager length conflicts

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-min-prefix-explain [type bool , default true ] (also --no-* )

[experts only]

minimize explanations for prefix of normal forms in strings

strings-model-max-len [type uint64_t , 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-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

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

[experts only]

use a single skolem for the variable splitting rule

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.

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 

symmetry-breaker [type bool , default true ] (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-lazy-ll [type bool , default false ] (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