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

[experts only]

enables non-standard extensions of the arithmetic solver

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

[experts only]

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

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

unate:

Use constraints to do unate propagation.

bi:

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

both:

Use bounds inference and unate.

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

[experts only]

rows shorter than this are propagated as clauses

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

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

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

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

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

[experts only]

collect the pivot history

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

[experts only]

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

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

[experts only]

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

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

[experts only]

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

dio-turns [type int64_t, default 10]

[experts only]

turns in a row dio solver cutting gets

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

[experts only]

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

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

min:

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

varord:

The variable order.

max:

The maximum violation the bound.

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

[experts only]

turns on degenerate pivot penalties

heuristic-pivots [type int64_t, default 0]

[experts only]

the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection

lemmas-on-replay-failure [type bool, default false] (also --no-*)

[experts only]

attempt to use external lemmas if approximate solve integer failed

maxCutsInContext [type uint64_t, default 65535]

[experts only]

maximum cuts in a given context before signalling a restart

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

[experts only]

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

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

[experts only]

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

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

[experts only]

use the new row propagation system

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

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

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

[experts only]

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

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

[experts only]

choose the Coverings lifting mode

Modes for the Coverings lifting in non-linear arithmetic.

regular:

Regular lifting.

lazard:

Lazard’s lifting scheme.

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

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

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

none:

Do not use linear model to seed nonlinear model

initial:

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

persistent:

Use linear model to seed nonlinear model whenever possible

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

[experts only]

choose the Coverings projection operator

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

mccallum:

McCallum’s projection operator.

lazard:

Lazard’s projection operator.

lazard-mod:

A modification of Lazard’s projection operator.

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

[experts only]

whether to prune intervals more aggressively

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

[experts only]

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

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

incremental linearization approach to non-linear

Modes for the non-linear linearization

none:

Disable linearization approach

light:

Only use a few light-weight lemma schemes

full:

Use all lemma schemes

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

[experts only]

check for entailed conflicts in non-linear solver

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

use factoring inference in non-linear incremental linearization solver

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

[experts only]

whether to increment the precision for irrational function constraints

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

[experts only]

purify non-linear terms at preprocess

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

[experts only]

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

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

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

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

[experts only]

initial splits on zero for all variables

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

[experts only]

initial degree of polynomials for Taylor approximation

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

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

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

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

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

interleave tangent plane strategy for non-linear incremental linearization solver

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

[experts only]

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

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

[experts only]

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

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

none:

Do not use relevance.

interleave:

Alternate rounds using relevance.

always:

Always use relevance.

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

[experts only]

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

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

[experts only]

apply pseudo boolean rewrites

pivot-threshold [type uint64_t, default 2]

[experts only]

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

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

[experts only]

threshold for substituting an equality in ppAssert

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

[experts only]

sets the maximum row length to be used in propagation

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

[experts only]

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

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

[experts only]

maximum complexity of any coefficient while outputting replaying cut lemmas

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

[experts only]

number of solve integer attempts to skips after a numeric failure

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

[experts only]

maximum complexity of any coefficient while replaying cuts

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

[experts only]

have a pivot cap for simplex at effort levels below fullEffort

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

[experts only]

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

rr-turns [type int64_t, default 3]

[experts only]

round robin turn

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

[experts only]

attempt to use the approximate solve integer method on standard effort

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

[experts only]

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

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

[experts only]

use quick explain to minimize the sum of infeasibility conflicts

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

[experts only]

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

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

[experts only]

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

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

all:

A combination of inequalities and equalities.

eqs:

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

ineqs:

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

none:

Do not add unate lemmas.

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

[experts only]

attempt to use an approximate solver

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

[experts only]

use focusing and converging simplex (FMCAD 2013 submission)

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

[experts only]

use sum of infeasibility simplex (FMCAD 2013 submission)

Arrays Theory Module

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

turn on eager index splitting for generated array lemmas

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

[experts only]

turn on eager lemma generation for arrays

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

[experts only]

enable experimental features in the theory of arrays

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

[experts only]

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

arrays-prop [type int64_t, default 2]

[experts only]

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

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

[experts only]

use model information to reduce size of care graph for arrays

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

[experts only]

use algorithm from Christ/Hoenicke (SMT 2014)

Bags Theory Module

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

[experts only]

enables the bags solver in applicable logics

Base Module

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

[experts only]

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

in [custom ManagedIn, default {}]

[experts only]

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

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

[experts only]

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

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

[experts only]

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

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

[experts only]

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

rweight [type string]

[experts only]

set a single resource weight

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

[experts only]

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

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

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

t | trace [type string]

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

Bitvector Theory Module

bitblast [lazy | eager, default lazy]

choose bitblasting mode, see –bitblast=help

Bit-blasting modes.

lazy:

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

eager:

Bitblast eagerly to bit-vector SAT solver.

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

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

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

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

BoolToBV preprocessing pass modes.

off:

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

ite:

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

all:

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

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

[experts only]

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

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

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

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

[experts only]

enable equality engine when possible in bitvector theory

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

[experts only]

simplify formula via Gaussian Elimination if applicable

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

[experts only]

introduce bitvector powers of two as a preprocessing pass

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

[experts only]

use bit-vector propagation in the bit-blaster

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

[experts only]

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

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

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

SAT solver for bit-blasting backend.

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

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

Bit-vector solvers.

bitblast:

Enables bitblasting solver.

bitblast-internal:

Enables bitblasting to internal SAT solver with proof support.

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

lift bit-vectors of size 1 to booleans when possible

Datatypes Theory Module

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

[experts only]

do bisimilarity check for co-datatypes

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

[experts only]

enables reasoning about codatatypes

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

[experts only]

do binary splits for datatype constructor types

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

[experts only]

when applicable, blast splitting lemmas for all variables at once

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

[experts only]

do cyclicity check for datatypes

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

[experts only]

always send lemmas out instead of making internal inferences

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

[experts only]

allow nested recursion in datatype definitions

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

[experts only]

turn on optimization for polite combination

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

internally use shared selectors across multiple constructors

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

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

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

if and how to apply fairness for sygus

Modes for enforcing fairness for counterexample guided quantifier instantion.

direct:

Enforce fairness using direct conflict lemmas.

dt-size:

Enforce fairness using size operator.

dt-height-bound:

Enforce fairness by height bound predicate.

dt-size-bound:

Enforce fairness by size bound predicate.

none:

Do not enforce fairness.

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

[experts only]

use max instead of sum for multi-function sygus conjectures

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

if and how to apply rewriting for sygus symmetry breaking

Modes for applying rewriting for sygus symmetry breaking.

none:

Do not use the rewriter.

basic:

Use the basic rewriter.

extended:

Use the extended rewriter.

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

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

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

none:

Do not apply simple symmetry breaking.

basic:

Apply basic simple symmetry breaking.

agg:

Apply aggressive simple symmetry breaking.

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

[experts only]

lazily add symmetry breaking lemmas for terms

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

sygus symmetry breaking lemmas based on pbe conjectures

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

[experts only]

add relevancy conditions to symmetry breaking lemmas

Decision Heuristics Module

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

choose decision mode, see –decision=help

Decision modes.

internal:

Use the internal decision heuristics of the SAT solver.

justification:

An ATGP-inspired justification heuristic.

stoponly:

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

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

[experts only]

maintain activity-based ordering for decision justification heuristic

jh-skolem [first | last, default first]

[experts only]

policy for when to satisfy skolem definitions in justification heuristic

Policy for when to satisfy skolem definitions in justification heuristic

first:

satisfy pending relevant skolem definitions before input assertions

last:

satisfy pending relevant skolem definitions after input assertions

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

[experts only]

policy for when to consider skolem definitions relevant in justification heuristic

Policy for when to consider skolem definitions relevant in justification heuristic

assert:

skolems are relevant when they occur in an asserted literal

always:

skolems are always relevant

Expression Module

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

[experts only]

type check expressions

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

[experts only]

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

Finite Field Theory Module

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

[experts only]

enables the finite field solver in applicable logics

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

[experts only]

parse bitsums

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

[experts only]

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

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

[experts only]

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

ff-solver [gb | split, default gb]

[experts only]

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

Which field solver

gb:

use a groebner basis for the whole system

split:

use multiple groebner bases for partitions of the system

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

[experts only]

use a traced groebner basis engine

Floating-Point Module

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

[experts only]

enables the floating point theory in applicable logics

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

[experts only]

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

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

[experts only]

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

Driver Module

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

dump the difficulty measure after every response to check-sat

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

output instantiations of quantified formulas after every UNSAT/VALID response

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

[experts only]

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

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

output models after every SAT/INVALID/UNKNOWN response

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

output proofs after every UNSAT/VALID response

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

output unsat cores after every UNSAT/VALID response

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

output lemmas in unsat cores after every UNSAT/VALID response

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

[experts only]

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

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

[experts only]

Force no CPU limit when dumping models and proofs

portfolio-jobs [type uint64_t, default 1]

[experts only]

Number of parallel jobs the portfolio engine can run

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

[experts only]

spin on segfault/other crash waiting for gdb

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

[experts only]

show all available tags for tracing

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

[experts only]

Use internal portfolio mode based on the logic

Parallel Module

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

[experts only]

emit learned literals with the cubes

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

[experts only]

number of standard or full effort checks until partitioning

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

[experts only]

number of checks between partitions

compute-partitions [type uint64_t, default 0]

[experts only]

make n partitions. n <2 disables computing partitions entirely

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

[experts only]

select whether partitioning happens at full or standard check

Partition check modes.

standard:

create partitions at standard checks

full:

create partitions at full checks

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

[experts only]

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

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

[experts only]

time to start creating partitions in seconds

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

[experts only]

choose partition strategy mode

Partition strategy modes.

decision-scatter:

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

heap-scatter:

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

lemma-scatter:

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

decision-cube:

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

heap-cube:

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

lemma-cube:

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

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

[experts only]

time to wait between scatter partitions

partition-tlimit [type uint64_t, default 60]

[experts only]

time limit for partitioning in seconds

partition-when [tlimit | climit, default tlimit]

[experts only]

choose when to partition

PartitionWhen modes.

tlimit:

Partition when the time limit is exceeded.

climit:

Partition when number of checks is exceeded.

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

[experts only]

create random partitions

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

[experts only]

set the output channel for writing partitions

Parser Module

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

[experts only]

limits the file system access if set to false

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

[experts only]

construct fresh variables always when parsing binders

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

use API interface for fresh constants when parsing declarations and definitions

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

force all declarations and definitions to be global when parsing

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

[experts only]

allows the parsing of skolems in the input file

parsing-mode [default | strict | lenient, default default]

[experts only]

choose parsing mode, see –parsing-mode=help

Parsing modes.

default:

Be reasonably tolerant of non-conforming inputs.

strict:

Be less tolerant of non-conforming inputs.

lenient:

Be more tolerant of non-conforming inputs.

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

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

dt:

print uninterpreted elements as a declare-datatype

none:

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

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

[experts only]

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

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

[experts only]

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

Proof Module

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

[experts only]

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

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

[experts only]

Print the DRAT proof in binary format

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

[experts only]

Print the children of trusted proof steps

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

[experts only]

Flatten steps in the LFSC proof

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

Optimize resolution reconstruction to reduce proof size

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

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

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

[experts only]

In Alethe proofs, use define-funs in proof preamble for Skolemization terms

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

[experts only]

Add pivots to Alethe resolution steps

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

[experts only]

Whether to allow trust in the proof printer (when applicable)

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

[experts only]

select internal proof checking mode

Internal proof checking modes.

eager:

check rule applications and proofs from generators eagerly for local debugging

eager-simple:

check rule applications during construction

lazy:

check rule applications only during final proof construction

none:

do not check rule applications

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

[experts only]

Dagify terms in proofs using global definitions

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

[experts only]

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

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

[experts only]

Eliminate subtypes (mixed arithmetic) in proofs

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

[experts only]

select language of proof output

Proof format modes.

none:

Do not translate proof output

dot:

Output DOT proof

lfsc:

Output LFSC proof

alethe:

Output Alethe proof

cpc:

Output Cooperating Proof Calculus proof

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

[experts only]

Print reference to original file instead of redeclaring

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

[experts only]

Prune unused input assumptions from final scope

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

the matching recursion limit for reconstructing proofs of theory rewrites

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

the limit of steps considered for reconstructing proofs of theory rewrites

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

modes for the type of proof generated by the SAT solver

Modes for the type of proof generated by the SAT solver.

proof:

A proof computed by the SAT solver.

sat-external-prove:

A proof containing a step that will be proven externally.

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

[experts only]

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

SAT Layer Module

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

[experts only]

instead of solving minisat dumps the asserted clauses in Dimacs format

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

[experts only]

Simplifications to be performed by Minisat.

Modes for Minisat simplifications.

all:

Variable and clause elimination, plus other simplifications.

clause-elim:

Caluse elimination and other simplifications, except variable elimination.

none:

No simplifications.

preregister-mode [eager | lazy, default eager]

[experts only]

Modes for when to preregister literals.

Modes for when to preregister literals.

eager:

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

lazy:

Preregister literals when they are asserted by the SAT solver.

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

[experts only]

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

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

[experts only]

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

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

[experts only]

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

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

sets the random seed for the sat solver

sat-solver [minisat | cadical, default minisat]

[experts only]

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

CDCL(T) SAT solver backend.

Quantifiers Module

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

enable conflict-based quantifier instantiation

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

add all available conflicting instances during conflict-based instantiation

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

what effort to apply conflict find mechanism

Quantifier conflict find modes.

conflict:

Apply QCF algorithm to find conflicts only.

prop-eq:

Apply QCF algorithm to propagate equalities as well as conflicts.

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

[experts only]

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

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

[experts only]

enable entailment checks for t-constraints in cbqi algorithm

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

[experts only]

cbqi experimental variable ordering

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

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

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

none:

Do not use sampling with CEGIS.

use:

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

trust:

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

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

turns on counterexample-based quantifier instantiation

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

[experts only]

apply counterexample-based instantiation to all quantified formulas

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

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

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

[experts only]

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

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

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

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

eq-slack:

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

eq-boundary:

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

keep:

Solve for the inequality directly using side conditions for invertibility.

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

[experts only]

interleave model value instantiation with word-level inversion approach

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

[experts only]

linearize adder chains for variables

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

[experts only]

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

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

[experts only]

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

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

[experts only]

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

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

use integer infinity for vts in counterexample-based quantifier instantiation

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

use real infinity for vts in counterexample-based quantifier instantiation

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

only process innermost quantified formulas in counterexample-based quantifier instantiation

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

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

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

[experts only]

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

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

[experts only]

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

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

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

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

[experts only]

non-optimal bounds for counterexample-based quantifier instantiation

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

[experts only]

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

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

[experts only]

split quantified formulas that lead to variable eliminations

Modes for splitting quantified formulas that lead to variable eliminations.

off:

Do not split quantified formulas.

on:

Split quantified formulas that lead to variable eliminations.

agg:

Aggressively split quantified formulas that lead to variable eliminations.

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

[experts only]

generate candidate conjectures for inductive proofs

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

[experts only]

number of ground terms to generate for model filtering

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

[experts only]

maximum depth of terms to consider for conjectures

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

[experts only]

number of conjectures to generate per instantiation round

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

[experts only]

use constructor expansion for single constructor datatypes triggers

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

[experts only]

apply strengthening for existential quantification over datatypes based on structural induction

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

[experts only]

expand datatype variables bound to one constructor in quantifiers

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

whether to do heuristic E-matching

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

eliminate tautological disjuncts of quantified formulas

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

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

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

interleave enumerative instantiation with other techniques

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

[experts only]

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

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

[experts only]

whether to use relevant domain first for enumerative instantiation strategy

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

[experts only]

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

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

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

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

apply extended rewriting to bodies of quantified formulas

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

use finite model finding heuristic for quantifier instantiation

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

finite model finding on bounded quantification

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

[experts only]

send all instantiations for bounded ranges in a single round

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

[experts only]

enforce bounds for bounded quantification lazily via use of proxy variables

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

[experts only]

find models for recursively defined functions, assumes functions are admissible

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

[experts only]

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

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

[experts only]

resort to full effort techniques instead of answering unknown when checking sygus candidates

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

[experts only]

do global negation of input formula

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

eagerly eliminate higher-order constraints

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

use store axiom during ho-elim

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

[experts only]

do higher-order matching algorithm for triggers with variable operators

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

[experts only]

merge term indices modulo equality

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

mode for using instantiation evaluation

Mode for using instantiation evaluation.

off:

Do not use instantiation evaluation.

use:

Use instantiation evaluation.

use-learn:

Use instantiation evaluation, and generalize learning.

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

[experts only]

generate additional triggers as needed during search

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

[experts only]

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

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

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

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

do not consider instances of quantified formulas that are currently entailed

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

when to apply instantiation

Instantiation modes.

full:

Run instantiation round at full effort, before theory combination.

full-delay:

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

full-last-call:

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

full-delay-last-call:

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

last-call:

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

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

[experts only]

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

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

[experts only]

apply strengthening for integers based on well-founded induction

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

[experts only]

split ites with dt testers as conditions

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

ite lifting mode for quantified formulas

ITE lifting modes for quantified formulas.

none:

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

simple:

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

all:

Lift if-then-else in quantified formulas.

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

[experts only]

choose literal matching mode

Literal match modes.

none:

Do not use literal matching.

use:

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

agg-predicate:

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

agg:

Consider the phase requirements aggressively for all triggers.

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

perform quantifiers macro expansion

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

mode for quantifiers macro expansion

Modes for quantifiers macro expansion.

all:

Infer definitions for functions, including those containing quantified formulas.

ground:

Only infer ground definitions for functions.

ground-uf:

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

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

[experts only]

use model-based quantifier instantiation

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

[experts only]

use fast enumeration to augment instantiations from MBQI

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

[experts only]

interleave model-based quantifier instantiation with other techniques

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

only add one instantiation per quantifier per round for mbqi

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

miniscope mode for quantified formulas

Miniscope quantifiers modes.

off:

Do not miniscope quantifiers.

conj:

Use miniscoping of conjunctions only.

fv:

Use free variable miniscoping only.

conj-and-fv:

Enable both conjunction and free variable miniscoping.

agg:

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

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

miniscope quantified formulas with user patterns

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

caching version of multi triggers

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

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

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

only try multi triggers if single triggers give no instantiations

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

select multi triggers when single triggers exist

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

[experts only]

Enable interface to external oracles

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

[experts only]

use triggers that do not contain all free variables

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

[experts only]

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

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

modes to apply skolemization eagerly to bodies of quantified formulas

Modes to apply skolemization eagerly to bodies of quantified formulas.

off:

Do not apply Skolemization eagerly.

on:

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

agg:

Apply Skolemization eagerly and aggressively during preprocessing.

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

[experts only]

apply skolemization to nested quantified formulas

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

prenex mode for quantified formulas

Prenex quantifiers modes.

none:

Do not prenex nested quantifiers.

simple:

Do simple prenexing of same sign quantifiers.

norm:

Prenex to prenex normal form.

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

prenex quantified formulas with user patterns

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

print instantiations for formulas that do not have given identifiers

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

[experts only]

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

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

infer alpha equivalence between quantified formulas

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

mode for dynamic quantifiers splitting

Modes for quantifiers splitting.

none:

Never split quantified formulas.

default:

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

agg:

Aggressively split quantified formulas.

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

[experts only]

assume that function defined by quantifiers are well defined

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

[experts only]

use all available techniques for inductive reasoning

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

[experts only]

selection mode for representatives in quantifiers engine

Modes for quantifiers representative selection.

ee:

Let equality engine choose representatives.

first:

Choose terms that appear first.

depth:

Choose terms that are of minimal depth.

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

[experts only]

consider ground terms within bodies of quantified formulas for matching

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

[experts only]

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

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

prefer triggers that are more relevant based on SInE style analysis

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

Enable conflict-based instantiation subsolver strategy

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

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

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

support SyGuS commands

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

statically add constants appearing in conjecture to grammars

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

[experts only]

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

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

[experts only]

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

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

[experts only]

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

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

use unsat core analysis to construct Boolean connective to sygus conjectures

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

[experts only]

abort if constant repair techniques are not applicable

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

mode for sygus enumeration

Modes for sygus enumeration.

smart:

Use smart enumeration based on datatype constraints.

fast:

Use optimized enumerator for sygus enumeration.

random:

Use basic random enumerator for sygus enumeration.

var-agnostic:

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

auto:

Internally decide the best policy for each enumerator.

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

[experts only]

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

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

[experts only]

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

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

modes for sygus evaluation unfolding

Modes for sygus evaluation unfolding.

none:

Do not use sygus evaluation unfolding.

single:

Do single-step unfolding for all evaluation functions.

single-bool:

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

multi:

Do multi-step unfolding for all evaluation functions.

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

[experts only]

timeout (in milliseconds) for satisfiability checks in expression miners

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

[experts only]

mode for filtering sygus solutions

Modes for filtering sygus solutions.

none:

Do not filter sygus solutions.

strong:

Filter solutions that are logically stronger than others.

weak:

Filter solutions that are logically weaker than others.

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

[experts only]

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

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

mode for SyGuS grammar construction

Modes for default SyGuS grammars.

simple:

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

any-const:

Use symoblic constant constructors.

any-term:

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

any-term-concise:

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

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

[experts only]

statically normalize sygus grammars based on flattening (linearization)

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

[experts only]

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

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

[experts only]

mode for preprocessing arbitrary inputs to sygus conjectures

Modes for preprocessing arbitrary inputs to sygus conjectures.

off:

Do not use sygus inference techniques.

try:

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

on:

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

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

Enable SyGuS instantiation quantifiers module

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

[experts only]

select instantiation lemma mode

SyGuS instantiation lemma modes.

priority-inst:

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

priority-eval:

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

interleave:

add instantiation and evaluation unfolding lemmas in the same step.

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

[experts only]

select scope of ground terms

scope for collecting ground terms for the grammar.

in:

use ground terms inside given quantified formula only.

out:

use ground terms outside of quantified formulas only.

both:

combines inside and outside.

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

[experts only]

granularity for ground terms

Ground term selection modes.

min:

collect minimal ground terms only.

max:

collect maximal ground terms only.

both:

combines minimal and maximal .

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

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

Template modes for sygus invariant synthesis.

none:

Synthesize invariant directly.

pre:

Synthesize invariant based on weakening of precondition.

post:

Synthesize invariant based on strengthening of postcondition.

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

[experts only]

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

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

statically minimize sygus grammars

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

output mode for sygus

Modes for sygus solution output.

status:

Print only status for check-synth calls.

status-and-def:

Print status followed by definition corresponding to solution.

sygus-standard:

Print based on SyGuS standard.

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

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

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

[experts only]

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

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

[experts only]

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

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

[experts only]

use quantifier elimination as a preprocessing step for sygus

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

[experts only]

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

Modes for generating interesting satisfiability queries using SyGuS.

basic:

Generate all queries using SyGuS enumeration of the given grammar

sample-sat:

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

unsat:

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

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

[experts only]

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

Query file options.

none:

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

all:

Dump all query files.

unsolved:

Dump query files that the subsolver did not solve.

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

[experts only]

do not print queries that are solved

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

[experts only]

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

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

[experts only]

enable efficient support for recursive functions in sygus grammars

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

[experts only]

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

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

use approach to repair constants in sygus candidate solutions

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

[experts only]

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

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

[experts only]

add dynamic symmetry breaking clauses based on candidate rewrites

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

[experts only]

use satisfiability check to verify correctness of candidate rewrites

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

[experts only]

filter candidate rewrites based on congruence

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

[experts only]

filter candidate rewrites based on matching

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

[experts only]

filter non-linear candidate rewrites

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

[experts only]

filter candidate rewrites based on variable ordering

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

[experts only]

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

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

[experts only]

synthesize rewrite rules over all sygus grammar types recursively

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

[experts only]

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

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

[experts only]

when applicable, use grammar for choosing sample points

sygus-samples [type int64_t, default 1000]

[experts only]

number of points to consider when doing sygus rewriter sample testing

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

mode for processing single invocation synthesis conjectures

Modes for single invocation techniques.

none:

Do not use single invocation techniques.

use:

Use single invocation techniques only if grammar is not restrictive.

all:

Always use single invocation techniques.

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

abort if synthesis conjecture is not single invocation

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

policy for reconstructing solutions for single invocation conjectures

Modes for reconstruction solutions while using single invocation techniques.

none:

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

try:

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

all-limit:

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

all:

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

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

[experts only]

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

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

[experts only]

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

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

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

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

[experts only]

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

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

mode for synthesis via piecewise-indepedent unification

Modes for piecewise-independent unification.

none:

Do not use piecewise-independent unification.

complete:

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

cond-enum:

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

cond-enum-igain:

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

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

[experts only]

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

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

[experts only]

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

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

timeout (in milliseconds) for verifying satisfiability of synthesized terms (0 == no limit)

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

which ground terms to consider for instantiation

Modes for terms included in the quantifiers term database.

all:

Quantifiers module considers all ground terms.

relevant:

Quantifiers module considers only ground terms connected to current assertions.

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

[experts only]

selection mode to activate triggers

Trigger active selection modes.

all:

Make all triggers active.

min:

Activate triggers with minimal ground terms.

max:

Activate triggers with maximal ground terms.

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

selection mode for triggers

Trigger selection modes.

min:

Consider only minimal subterms that meet criteria for triggers.

max:

Consider only maximal subterms that meet criteria for triggers.

min-s-max:

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

min-s-all:

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

all:

Consider all subterms that meet criteria for triggers.

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

policy for handling user-provided patterns for quantifier instantiation

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

use:

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

trust:

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

strict:

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

resort:

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

ignore:

Ignore user-provided patterns.

interleave:

Alternate between use/resort.

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

[experts only]

policy for handling user-provided pools for quantifier instantiation

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

use:

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

trust:

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

ignore:

Ignore user-provided pool.

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

enable simple variable elimination for quantified formulas

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

enable variable elimination based on infinite projection of unbound arithmetic variables

Separation Logic Theory Module

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

[experts only]

enables the separation logic solver in applicable logics

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

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

[experts only]

enable the relations extension of the theory of sets

sets-card-exp [type bool, default true] (also --no-*)

[experts only]

enable the cardinality extension of the theory of sets

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

[experts only]

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

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

[experts only]

introduce proxy variables eagerly to shorten lemmas

SMT Layer Module

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

[experts only]

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

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

eliminate functions by ackermannization

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

[experts only]

use internal pow2 operator when translating shift notes

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

[experts only]

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

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

checks whether produced solutions to get-abduct are correct

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

checks whether produced solutions to get-interpolant are correct

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

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

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

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

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

[experts only]

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

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

[experts only]

mode for deep restarts

Mode for deep restarts

none:

do not use deep restart

input:

learn literals that appear in the input

input-and-solvable:

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

input-and-prop:

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

all:

learn all literals

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

[experts only]

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

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

[experts only]

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

difficulty output modes.

lemma-literal:

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

lemma-literal-all:

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

model-check:

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

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

[experts only]

remove ITEs early in preprocessing

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

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

extended rewriter preprocessing pass modes.

off:

do not use extended rewriter as a preprocessing pass.

use:

use extended rewriter as a preprocessing pass.

agg:

use aggressive extended rewriter as a preprocessing pass.

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

[experts only]

Cross-theory rewrites

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

[experts only]

Set the refinement scheme for integer AND

Refinement modes for integer AND

value:

value-based refinement

sum:

use sum to represent integer AND in refinement

bitwise:

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

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

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

Interpolants grammar mode

default:

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

assumptions:

use only operators that occur in the assumptions

conjecture:

use only operators that occur in the conjecture

shared:

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

all:

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

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

[experts only]

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

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

rewrite the input based on learned literals

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

[experts only]

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

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

mode for producing model cores

Model cores modes.

none:

Do not compute model cores.

simple:

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

non-implied:

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

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

[experts only]

allow variable elimination based on unevaluatable terms to variables

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

[experts only]

do the ite simplification pass again if repeating simplification

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

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

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

support the get-abduct command

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

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

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

support the get-assignment command

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

enable tracking of difficulty.

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

turn on interpolation generation.

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

produce learned literals, support get-learned-literals

produce-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 | full-proof-strict, default off]

[experts only]

choose proof mode, see –proof-mode=help

proof modes.

off:

Do not produce proofs.

pp-only:

Only produce proofs for preprocessing.

sat-proof:

Produce proofs for preprocessing and for the SAT solver.

full-proof:

Produce full proofs of preprocessing, SAT and theory lemmas.

full-proof-strict:

Produce full proofs of preprocessing, SAT and theory lemmas. Additionally disable techniques that will lead to incomplete proofs.

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

[experts only]

make multiple passes with nonclausal simplifier

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

[experts only]

enables compressing ites after ite simplification

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

[experts only]

enables simplifyWithCare in ite simplificiation

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

choose simplification mode, see –simplification=help

Simplification modes.

none:

Do not perform nonclausal simplification.

batch:

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

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

[experts only]

apply Boolean constant propagation as a substitution during simplification

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

mode for translating BVAnd to integer

solve-bv-as-int modes.

off:

Do not translate bit-vectors to integers

sum:

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

iand:

Translate bvand to the iand operator

bv:

Translate bvand back to bit-vectors

bitwise:

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

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

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

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

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

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

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