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

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

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

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-strategy | partition [ revised | strict-cube | decision-trail | heap-trail , default revised ]

[experts only]

choose partition strategy mode

Partition strategy modes.

revised :

For 4 partitions, creates cubes C1, C2, C3, !C1 & !C2 & !C3

strict-cube :

For 4 partitions, creates cubes C1, !C1 & C2, !C1 & !C2 & C3, !C1 & !C2 & !C3

decision-trail :

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

heap-trail :

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

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

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 ¶

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.

Proof Module ¶

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

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

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

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

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

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 ]

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

when printing unsat cores, include unlabeled assertions

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 substituion during simplification

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

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

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