# Tactics Summary

## Tactic ackernannize_bv

### Short Description

A tactic for performing Ackermann reduction for bit-vector formulas

### Long Description

The Ackermann reduction replaces uninterpreted functions $f(t_1), f(t_2)$ by fresh variables $f_1, f_2$ and addes axioms $t_1 \simeq t_2 \implies f_1 \simeq f_2$. The reduction has the effect of eliminating uninterpreted functions. When the reduction produces a pure bit-vector benchmark, it allows Z3 to use a specialized SAT solver.

### Example

### Notes

- does not support proofs, does not support unsatisfiable cores

## Tactic add-bounds

### Short Description

Tactic for bounding unbounded variables.

### Long Description

The tactic creates a stronger sub-goal by adding bounds to variables. The new goal may not be satisfiable even if the original goal is.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

add_bound_lower | rational | (default: -2) lower bound to be added to unbounded variables. | |

add_bound_upper | rational | (default: 2) upper bound to be added to unbounded variables. |

## Tactic aig

### Short Description

Simplify Boolean structure using AIGs (And-inverter graphs).

### Long Description

And-inverter graphs (AIGs) uses just the Boolean connectives `and`

and `not`

to encode Boolean
formulas. The circuit representation using AIGs first converts formulas using other connectives to this normal form,
then performs local simplification steps to minimize the circuit representation.
Note that the simplification steps used by this tactic are heuristic, trading speed for power,
and do not represent a high-quality circuit minimization approach.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

## Tactic bit-blast

### Short Description

Apply bit-blasting to a given goal.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

blast_add | bool | bit-blast adders. | true |

blast_full | bool | bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms. | false |

blast_mul | bool | bit-blast multipliers (and dividers, remainders). | true |

blast_quant | bool | bit-blast quantified variables. | false |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | (default: infty) maximum number of steps. | 4294967295 |

## Tactic blast-term-ite

### Short Description:

Blast term if-then-else by hoisting them up.
This is expensive but useful in some cases, such as
for enforcing constraints being in difference logic.
Use `elim-term-ite`

elsewhere when possible.

### Example

### Notes

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_inflation | unsigned int | (default: infinity) multiplicative factor of initial term size. | 4294967295 |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | (default: infty) maximum number of steps. | 4294967295 |

## Tactic bv-slice

### Short Description

Slices bit-vectors into sub-ranges to allow simplifying sub-ranges.

### Long Description

It rewrites a state using bit-vector slices. Slices are extracted from bit-vector equality assertions. An equality assertion may equate a sub-range of a bit-vector with a constant. The tactic ensures that all occurrences of the subrange are replaced by the constants to allow additional simplification

### Example

## Tactic bv1-blast

### Short Description

Reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).

### Long Description

Rewriter for "blasting" bit-vectors of size n into bit-vectors of size 1. This rewriter only supports concat and extract operators. This transformation is useful for handling benchmarks that contain many BV equalities.

*Remark*: other operators can be mapped into concat/extract by using
the simplifiers.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | (default: infty) maximum number of steps. | 4294967295 |

## Tactic bv_bound_chk

### Short Description

Attempts to detect inconsistencies of bounds on bv expressions.

### Notes

- does not support proofs, does not support cores

## Tactic bvarray2uf

### Short Description

Tactic that rewrites bit-vector arrays into bit-vector (uninterpreted) functions.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

produce_models | bool | model generation. | false |

## Tactic card2bv

### Short Description

Tactic for converting Pseudo-Boolean constraints to bit-vectors.

### Long Description

The tactic implements a set of standard methods for converting cardinality and Pseudo-Boolean constraints into bit-vector or propositional formulas (using basic logical connectives, conjunction, disjunction, negation). The conversions from cardinality constraints are controlled separately from the conversions from Pseudo-Boolean constraints using different parameters.

### Example

### Notes

- supports cores
- does not support proofs

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

cardinality.encoding | symbol | encoding used for cardinality constraints: grouped, bimander, ordered, unate, circuit | none |

keep_cardinality_constraints | bool | retain cardinality constraints for solver | true |

pb.solver | symbol | encoding used for Pseudo-Boolean constraints: totalizer, sorting, binary_merge, bv, solver. PB constraints are retained if set to 'solver' | solver |

## Tactic cofactor-term-ite

### Short Description

Eliminate (ground) term if-then-else's using cofactors. It hoists nested if-then-else expressions inside terms into the top level of the formula.

### Notes

- does not support proofs, does not support cores

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

cofactor_equalities | bool | (default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive. |

## Tactic ctx-simplify

### Short Description:

The tactic performs simplifies sub-formulas using context built up by walking assertions and sub-formulas.

### Example

### Notes

- supports proof terms with limited features

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_depth | unsigned int | maximum term depth. | 1024 |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | (default: infty) maximum number of steps. | 4294967295 |

propagate_eq | bool | enable equality propagation from bounds. | false |

## Tactic ctx-solver-simplify

### Short Description

A heavy handed version of `ctx-simplify`

. It applies SMT checks on sub-formulas to check
if they can be simplified to `true`

or `false`

within their context.
Note that a sub-formula may occur within multiple contexts due to shared sub-terms.
In this case the tactic is partial and simplifies a limited number of context occurrences.

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

arith.auto_config_simplex | bool | force simplex solver in auto_config | false |

arith.bprop_on_pivoted_rows | bool | propagate bounds on rows changed by the pivot operation | true |

arith.branch_cut_ratio | unsigned int | branch/cut ratio for linear integer arithmetic | 2 |

arith.dump_lemmas | bool | dump arithmetic theory lemmas to files | false |

arith.eager_eq_axioms | bool | eager equality axioms | true |

arith.enable_hnf | bool | enable hnf (Hermite Normal Form) cuts | true |

arith.greatest_error_pivot | bool | Pivoting strategy | false |

arith.ignore_int | bool | treat integer variables as real | false |

arith.int_eq_branch | bool | branching using derived integer equations | false |

arith.min | bool | minimize cost | false |

arith.nl | bool | (incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2 | true |

arith.nl.branching | bool | branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2 | true |

arith.nl.delay | unsigned int | number of calls to final check before invoking bounded nlsat check | 500 |

arith.nl.expp | bool | expensive patching | false |

arith.nl.gr_q | unsigned int | grobner's quota | 10 |

arith.nl.grobner | bool | run grobner's basis heuristic | true |

arith.nl.grobner_cnfl_to_report | unsigned int | grobner's maximum number of conflicts to report | 1 |

arith.nl.grobner_eqs_growth | unsigned int | grobner's number of equalities growth | 10 |

arith.nl.grobner_expr_degree_growth | unsigned int | grobner's maximum expr degree growth | 2 |

arith.nl.grobner_expr_size_growth | unsigned int | grobner's maximum expr size growth | 2 |

arith.nl.grobner_frequency | unsigned int | grobner's call frequency | 4 |

arith.nl.grobner_max_simplified | unsigned int | grobner's maximum number of simplifications | 10000 |

arith.nl.grobner_subs_fixed | unsigned int | 0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 1 |

arith.nl.horner | bool | run horner's heuristic | true |

arith.nl.horner_frequency | unsigned int | horner's call frequency | 4 |

arith.nl.horner_row_length_limit | unsigned int | row is disregarded by the heuristic if its length is longer than the value | 10 |

arith.nl.horner_subs_fixed | unsigned int | 0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 2 |

arith.nl.nra | bool | call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6 | true |

arith.nl.order | bool | run order lemmas | true |

arith.nl.rounds | unsigned int | threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2 | 1024 |

arith.nl.tangents | bool | run tangent lemmas | true |

arith.print_ext_var_names | bool | print external variable names | false |

arith.print_stats | bool | print statistic | false |

arith.propagate_eqs | bool | propagate (cheap) equalities | true |

arith.propagation_mode | unsigned int | 0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds | 1 |

arith.random_initial_value | bool | use random initial values in the simplex-based procedure for linear arithmetic | false |

arith.rep_freq | unsigned int | the report frequency, in how many iterations print the cost and other info | 0 |

arith.simplex_strategy | unsigned int | simplex strategy for the solver | 0 |

arith.solver | unsigned int | arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 6 |

array.extensional | bool | extensional array theory | true |

array.weak | bool | weak array theory | false |

auto_config | bool | automatically configure solver | true |

bound_simplifier | bool | apply bounds simplification during pre-processing | true |

bv.delay | bool | delay internalize expensive bit-vector operations | false |

bv.enable_int2bv | bool | enable support for int2bv and bv2int operators | true |

bv.eq_axioms | bool | enable redundant equality axioms for bit-vectors | true |

bv.reflect | bool | create enode for every bit-vector term | true |

bv.size_reduce | bool | pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant | false |

bv.watch_diseq | bool | use watch lists instead of eager axioms for bit-vectors | false |

candidate_models | bool | create candidate models even when quantifier or theory reasoning is incomplete | false |

case_split | unsigned int | 0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity | 1 |

clause_proof | bool | record a clausal proof | false |

core.extend_nonlocal_patterns | bool | extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier's body | false |

core.extend_patterns | bool | extend unsat core with literals that trigger (potential) quantifier instances | false |

core.extend_patterns.max_distance | unsigned int | limits the distance of a pattern-extended unsat core | 4294967295 |

core.minimize | bool | minimize unsat core produced by SMT context | false |

core.validate | bool | [internal] validate unsat core produced by SMT context. This option is intended for debugging | false |

cube_depth | unsigned int | cube depth. | 1 |

dack | unsigned int | 0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution | 1 |

dack.eq | bool | enable dynamic ackermannization for transtivity of equalities | false |

dack.factor | double | number of instance per conflict | 0.1 |

dack.gc | unsigned int | Dynamic ackermannization garbage collection frequency (per conflict) | 2000 |

dack.gc_inv_decay | double | Dynamic ackermannization garbage collection decay | 0.8 |

dack.threshold | unsigned int | number of times the congruence rule must be used before Leibniz's axiom is expanded | 10 |

delay_units | bool | if true then z3 will not restart when a unit clause is learned | false |

delay_units_threshold | unsigned int | maximum number of learned unit clauses before restarting, ignored if delay_units is false | 32 |

dt_lazy_splits | unsigned int | How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy | 1 |

elim_unconstrained | bool | pre-processing: eliminate unconstrained subterms | true |

ematching | bool | E-Matching based quantifier instantiation | true |

induction | bool | enable generation of induction lemmas | false |

lemma_gc_strategy | unsigned int | lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none | 0 |

logic | symbol | logic used to setup the SMT solver | |

macro_finder | bool | try to find universally quantified formulas that can be viewed as macros | false |

max_conflicts | unsigned int | maximum number of conflicts before giving up. | 4294967295 |

mbqi | bool | model based quantifier instantiation (MBQI) | true |

mbqi.force_template | unsigned int | some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template | 10 |

mbqi.id | string | Only use model-based instantiation for quantifiers with id's beginning with string | |

mbqi.max_cexs | unsigned int | initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation | 1 |

mbqi.max_cexs_incr | unsigned int | increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI | 0 |

mbqi.max_iterations | unsigned int | maximum number of rounds of MBQI | 1000 |

mbqi.trace | bool | generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied | false |

pb.conflict_frequency | unsigned int | conflict frequency for Pseudo-Boolean theory | 1000 |

pb.learn_complements | bool | learn complement literals for Pseudo-Boolean theory | true |

phase_caching_off | unsigned int | number of conflicts while phase caching is off | 100 |

phase_caching_on | unsigned int | number of conflicts while phase caching is on | 400 |

phase_selection | unsigned int | phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory | 3 |

propagate_values | bool | pre-processing: propagate values | true |

pull_nested_quantifiers | bool | pre-processing: pull nested quantifiers | false |

q.lift_ite | unsigned int | 0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers | 0 |

q.lite | bool | Use cheap quantifier elimination during pre-processing | false |

qi.cost | string | expression specifying what is the cost of a given quantifier instantiation | (+ weight generation) |

qi.eager_threshold | double | threshold for eager quantifier instantiation | 10.0 |

qi.lazy_threshold | double | threshold for lazy quantifier instantiation | 20.0 |

qi.max_instances | unsigned int | maximum number of quantifier instantiations | 4294967295 |

qi.max_multi_patterns | unsigned int | specify the number of extra multi patterns | 0 |

qi.profile | bool | profile quantifier instantiation | false |

qi.profile_freq | unsigned int | how frequent results are reported by qi.profile | 4294967295 |

qi.quick_checker | unsigned int | specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances | 0 |

quasi_macros | bool | try to find universally quantified formulas that are quasi-macros | false |

random_seed | unsigned int | random seed for the smt solver | 0 |

refine_inj_axioms | bool | pre-processing: refine injectivity axioms | true |

relevancy | unsigned int | relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant | 2 |

restart.max | unsigned int | maximal number of restarts. | 4294967295 |

restart_factor | double | when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold | 1.1 |

restart_strategy | unsigned int | 0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic | 1 |

restricted_quasi_macros | bool | try to find universally quantified formulas that are restricted quasi-macros | false |

seq.max_unfolding | unsigned int | maximal unfolding depth for checking string equations and regular expressions | 1000000000 |

seq.min_unfolding | unsigned int | initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths | 1 |

seq.split_w_len | bool | enable splitting guided by length constraints | true |

seq.validate | bool | enable self-validation of theory axioms created by seq theory | false |

solve_eqs | bool | pre-processing: solve equalities | true |

str.aggressive_length_testing | bool | prioritize testing concrete length values over generating more options | false |

str.aggressive_unroll_testing | bool | prioritize testing concrete regex unroll counts over generating more options | true |

str.aggressive_value_testing | bool | prioritize testing concrete string constant values over generating more options | false |

str.fast_length_tester_cache | bool | cache length tester constants instead of regenerating them | false |

str.fast_value_tester_cache | bool | cache value tester constants instead of regenerating them | true |

str.fixed_length_naive_cex | bool | construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only) | true |

str.fixed_length_refinement | bool | use abstraction refinement in fixed-length equation solver (Z3str3 only) | false |

str.overlap_priority | double | theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true | -0.1 |

str.regex_automata_difficulty_threshold | unsigned int | difficulty threshold for regex automata heuristics | 1000 |

str.regex_automata_failed_automaton_threshold | unsigned int | number of failed automaton construction attempts after which a full automaton is automatically built | 10 |

str.regex_automata_failed_intersection_threshold | unsigned int | number of failed automaton intersection attempts after which intersection is always computed | 10 |

str.regex_automata_intersection_difficulty_threshold | unsigned int | difficulty threshold for regex intersection heuristics | 1000 |

str.regex_automata_length_attempt_threshold | unsigned int | number of length/path constraint attempts before checking unsatisfiability of regex terms | 10 |

str.string_constant_cache | bool | cache all generated string constants generated from anywhere in theory_str | true |

str.strong_arrangements | bool | assert equivalences instead of implications when generating string arrangement axioms | true |

string_solver | symbol | solver for string/sequence theories. options are: 'z3str3' (specialized string solver), 'seq' (sequence solver), 'auto' (use static features to choose best solver), 'empty' (a no-op solver that forces an answer unknown if strings were used), 'none' (no solver) | seq |

theory_aware_branching | bool | Allow the context to use extra information from theory solvers regarding literal branching prioritization. | false |

theory_case_split | bool | Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead. | false |

threads | unsigned int | maximal number of parallel threads. | 1 |

threads.cube_frequency | unsigned int | frequency for using cubing | 2 |

threads.max_conflicts | unsigned int | maximal number of conflicts between rounds of cubing for parallel SMT | 400 |

## Tactic degree-shift

### Short Description

The procedure reduces the degrees of variables.

### Long Description

Basic idea: if goal $G$ contains a real variable $x$, $x$ occurs with degrees $d_1, ..., d_k$ in $G$, and $n = \gcd(d_1, ..., d_k) > 1$. Then, replace $x^n$ with a new fresh variable $y$.

### Example

### Notes

- supports proofs and cores

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted | 4294967295 |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

ite_extra_rules | bool | extra ite simplifications, these additional simplifications may reduce size locally but increase globally | true |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

rewrite_patterns | bool | rewrite patterns. | false |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

## Tactic demodulator

### Short Description:

Extracts equalities from quantifiers and applies them for simplification

### Long Description

In first-order theorem proving (FOTP), a demodulator is a universally quantified formula of the form:

`Forall X1, ..., Xn. L[X1, ..., Xn] = R[X1, ..., Xn]`

Where `L[X1, ..., Xn]`

contains all variables in `R[X1, ..., Xn]`

, and
`L[X1, ..., Xn]`

is "bigger" than `R[X1, ...,Xn]`

.

The idea is to replace something big `L[X1, ..., Xn]`

with something smaller `R[X1, ..., Xn]`

.

After selecting the demodulators, we traverse the rest of the formula looking for instances of `L[X1, ..., Xn]`

.
Whenever we find an instance, we replace it with the associated instance of `R[X1, ..., Xn]`

.

For example, suppose we have

`Forall x, y. f(x+y, y) = y`

and

f(g(b) + h(c), h(c)) <= 0

The term `f(g(b) + h(c), h(c))`

is an instance of `f(x+y, y)`

if we replace `x <- g(b)`

and `y <- h(c)`

.
So, we can replace it with `y`

which is bound to `h(c)`

in this example. So, the result of the transformation is:

`Forall x, y. f(x+y, y) = y`

and

h(c) <= 0

### Example

` (declare-sort S 0)`

(declare-sort S1 0)

(declare-sort S2 0)

(declare-fun f () S)

(declare-fun f1 () S)

(declare-fun f2 (S1 S) S)

(declare-fun f3 (S2 S) S1)

(declare-fun f4 () S)

(declare-fun f5 () S2)

(assert (not (= f1 (f2 (f3 f5 f4) f))))

(assert (forall ((q S) (v S)) (or (= q v) (= f1 (f2 (f3 f5 q) v)) (= (f2 (f3 f5 v) q) f1))))

(assert (forall ((q S) (x S)) (not (= (f2 (f3 f5 q) x) f1))))

(apply demodulator)

It generates

` (goals`

(goal

(forall ((q S) (v S)) (= q v))

(forall ((q S) (x S)) (not (= (f2 (f3 f5 q) x) f1)))

:precision precise :depth 1)

)

### Notes

- supports unsat cores
- does not support fine-grained proofs

## Tactic der

### Short Description:

The tactic performs *destructive equality resolution*.

### Long Description

Destructive equality resolution replaces bound variables that are
*solved* by their solutions in formulas. In short, the destructive
equality resolution rule takes the form:

` (forall (X Y) (or X /= s C[X])) --> (forall (Y) C[Y])`

### Example

### Notes

- supports unsat cores, proof terms

## Tactic diff-neq

### Short Description

A specialized solver for integer problems using only constant bounds and differences to constants.

### Long Description

Solver for integer problems that contains literals of the form

` k <= x`

x <= k

x - y != k

### Example

### Notes

- The tactic works only when the lower bounds are 0 and disequalities use multiplication with -1. Use normalize-bounds to ensure all lower bounds are 0.

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

diff_neq_max_k | unsigned int | maximum variable upper bound for diff neq solver. | 1024 |

## Tactic distribute-forall

### Short Description:

Distribute $\forall$ over conjunctions (and distribute $\exists$ over disjunctions)

### Example

### Notes

- supports unsat cores, proof terms

## Tactic dom-simplify

### Short Description

Apply dominator simplification rules

### Long Description

Dominator-based simplification is a context dependent simplification function that uses a dominator tree to control the number of paths it visits during simplification. The expression DAG may have an exponential number of paths, but only paths corresponding to a dominator tree are visited. Since the paths selected by the dominator trees are limited, the simplifier may easily fail to simplify within a context.

### Example

## Tactic dt2bv

### Short Description

Tactic that eliminates finite domain data-types.

### Example

## Tactic elim-predicates

### Short Description

Eliminates predicates and macros from a formula.

### Long Description

The tactic subsumes the functionality of `macro-finder`

and `quasi-macros`

.
Besides finding macros, it eliminates predicates using Davis-Putnam
resolution.

### Example

the predicate `p`

occurs once positively. All negative occurrences of `p`

are resolved against this positive occurrence.
The result of resolution is a set of equalities between arguments to `p`

. The function `f`

is replaced by a partial solution.

### Notes

- support unsat cores
- does not support proofs

## Tactic elim-small-bv

### Short Description

Eliminate small, quantified bit-vectors by expansion

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_bits | unsigned int | (default: 4) maximum bit-vector size of quantified bit-vectors to be eliminated. | |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | (default: infty) maximum number of steps. | 4294967295 |

## Tactic elim-term-ite

### Short Description:

Eliminate term if-then-else by adding new fresh auxiliary variables.

### Example

### Notes

- supports proof terms and unsat cores

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_args | unsigned int | (default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic. | |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | (default: infty) maximum number of steps. | 4294967295 |

## Tactic elim-uncnstr

### Short Description

Eliminate Unconstrained uninterpreted constants

### Long Description

The tactic eliminates uninterpreted constants that occur only once in a goal and such that the immediate context
where they occur can be replaced by a fresh constant. We call these occurrences invertible.
It relies on a series of theory specific invertibility transformations.
In the following assume `x`

and `x'`

occur in a unique subterm and `y`

is a fresh uninterpreted constant.

#### Boolean Connectives

Original Context | New Term | Updated solution |
---|---|---|

`(if c x x')` | `y` | `x = x' = y` |

`(if x x' e)` | `y` | `x = true, x' = y` |

`(if x t x')` | `y` | `x = false, x' = y` |

`(not x)` | `y` | `x = (not y)` |

`(and x x')` | `y` | `x = y, x' = true` |

`(or x x')` | `y` | `x = y, x' = false` |

`(= x t)` | `y` | `x = (if y t (diff t))` |

where diff is a diagnonalization function available in domains of size `>`

1.

#### Arithmetic

Original Context | New Term | Updated solution |
---|---|---|

`(+ x t)` | `y` | `x = y - t` |

`(* x x')` | `y` | `x = y, x' = 1` |

`(* -1 x)` | `y` | `x = -y` |

`(<= x t)` | `y` | `x = (if y t (+ t 1))` |

`(<= t x)` | `y` | `x = (if y t (- t 1))` |

#### Bit-vectors

Original Context | New Term | Updated solution |
---|---|---|

`(bvadd x t)` | `y` | `x = y - t` |

`(bvmul x x')` | `y` | `x = y, x' = 1` |

`(bvmul odd x)` | `y` | `x = inv(odd)*y` |

`((extract sz-1 0) x)` | `y` | `x = y` |

`((extract hi lo) x)` | `y` | `x = (concat y1 y y2)` |

`(udiv x x')` | `y` | `x = y, x' = 1` |

`(concat x x')` | `y` | `x = (extract hi1 lo1 y)` |

`(bvule x t)` | `(or y (= t MAX))` | `x = (if y t (bvadd t 1))` |

`(bvule t x)` | `(or y (= t MIN))` | `x = (if y t (bvsub t 1))` |

`(bvnot x)` | `y` | `x = (bvnot y)` |

`(bvand x x')` | `y` | `x = y, x' = MAX` |

In addition there are conversions for shift and bit-wise or and signed comparison.

#### Arrays

Original Context | New Term | Updated solution |
---|---|---|

`(select x t)` | `y` | `x = (const y)` |

`(store x x1 x2)` | `y` | `x2 = (select x x1), x = y, x1 = arb` |

#### Algebraic Datatypes

Original Context | New Term | Updated solution |
---|---|---|

`(head x)` | `y` | `x = (cons y arb)` |

### Example

### Notes

- supports unsat cores
- does not support fine-grained proofs

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | (default: infty) maximum number of steps. | 4294967295 |

## Tactic eq2bv

### Short Description

Extract integer variables that are used as finite domain indicators. The integer variables can only occur in equalities.

### Example

### Notes

- does not support proofs

## Tactic euf-completion

### Short Description

Uses the ground equalities as a rewrite system. The formulas are simplified using the rewrite system.

### Long Description

The tactic uses congruence closure to represent and orient the rewrite system. Equalities from the formula are inserted in the an E-graph (congruence closure structure) and then a representative that is most shallow is extracted.

## Tactic factor

### Short Description

Factor polynomials in equalities and inequalities.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_prime | unsigned int | (default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step. | |

max_search_size | unsigned int | (default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space. | |

num_primes | unsigned int | (default: 1) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching. | |

split_factors | bool | apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)). | true |

## Tactic fix-dl-var

### Short Description

Fix a difference logic variable to `0`

.
If the problem is in the difference logic fragment, that is, all arithmetic terms
are of the form `(x + k)`

, and the arithmetic atoms are of the
form `x - y <= k`

or `x - y = k`

. Then, we can set one variable to `0`

.

This is useful because, many bounds can be exposed after this operation is performed.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted | 4294967295 |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

ite_extra_rules | bool | extra ite simplifications, these additional simplifications may reduce size locally but increase globally | true |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

rewrite_patterns | bool | rewrite patterns. | false |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

## Tactic fm

### Short Description

Use Fourier-Motzkin to eliminate variables. This strategy can handle conditional bounds (i.e., clauses with at most one constraint).

The tactic occf can be used to put the formula in OCC form.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | when blast_distinct is true, only distinct expressions with less than this number of arguments are blasted | 4294967295 |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

fm_cutoff1 | unsigned int | first cutoff for FM based on maximum number of lower/upper occurrences. | 8 |

fm_cutoff2 | unsigned int | second cutoff for FM based on num_lower * num_upper occurrences. | 256 |

fm_extra | unsigned int | max. increase on the number of inequalities for each FM variable elimination step. | 0 |

fm_limit | unsigned int | maximum number of constraints, monomials, clauses visited during FM. | 5000000 |

fm_occ | bool | consider inequalities occurring in clauses for FM. | false |

fm_real_only | bool | consider only real variables for fourier-motzkin elimination. | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

ite_extra_rules | bool | extra ite simplifications, these additional simplifications may reduce size locally but increase globally | true |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

produce_models | bool | model generation. | false |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

rewrite_patterns | bool | rewrite patterns. | false |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

## Tactic fpa2bv

### Short Description

Converts floating points to bit-vector representation.

## Tactic horn

### Short Description

Solve a set of Horn clauses using the SPACER engine.

### Long Description

The SPACER engine is specialized to solving Constrained Horn Clauses. This tactic instructs

## Tactic horn-simplify

### Short Description

Apply pre-processing simplification rules to a set of Horn clauses

### Long Description

This tactic exposes pre-processing simplification rules for Constrained Horn Clauses.
They include a repertoire of simplification options that can be controlled by toggling
the `fp`

parameters.

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

bmc.linear_unrolling_depth | unsigned int | Maximal level to explore | 4294967295 |

ctrl_c | bool | enable interrupts from ctrl-c | true |

datalog.all_or_nothing_deltas | bool | compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not | false |

datalog.check_relation | symbol | name of default relation to check. operations on the default relation will be verified using SMT solving | null |

datalog.compile_with_widening | bool | widening will be used to compile recursive rules | false |

datalog.dbg_fpr_nonempty_relation_signature | bool | if true, finite_product_relation will attempt to avoid creating inner relation with empty signature by putting in half of the table columns, if it would have been empty otherwise | false |

datalog.default_relation | symbol | default relation implementation: external_relation, pentagon | pentagon |

datalog.default_table | symbol | default table implementation: sparse, hashtable, bitvector, interval | sparse |

datalog.default_table_checked | bool | if true, the default table will be default_table inside a wrapper that checks that its results are the same as of default_table_checker table | false |

datalog.default_table_checker | symbol | see default_table_checked | null |

datalog.explanations_on_relation_level | bool | if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect) | false |

datalog.generate_explanations | bool | produce explanations for produced facts when using the datalog engine | false |

datalog.initial_restart_timeout | unsigned int | length of saturation run before the first restart (in ms), zero means no restarts | 0 |

datalog.magic_sets_for_queries | bool | magic set transformation will be used for queries | false |

datalog.output_profile | bool | determines whether profile information should be output when outputting Datalog rules or instructions | false |

datalog.print.tuples | bool | determines whether tuples for output predicates should be output | true |

datalog.profile_timeout_milliseconds | unsigned int | instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list | 0 |

datalog.similarity_compressor | bool | rules that differ only in values of constants will be merged into a single rule | true |

datalog.similarity_compressor_threshold | unsigned int | if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged | 11 |

datalog.subsumption | bool | if true, removes/filters predicates with total transitions | true |

datalog.timeout | unsigned int | Time limit used for saturation | 0 |

datalog.unbound_compressor | bool | auxiliary relations will be introduced to avoid unbound variables in rule heads | true |

datalog.use_map_names | bool | use names from map files when displaying tuples | true |

engine | symbol | Select: auto-config, datalog, bmc, spacer | auto-config |

generate_proof_trace | bool | trace for 'sat' answer as proof object | false |

print_aig | symbol | Dump clauses in AIG text format (AAG) to the given file name | |

print_answer | bool | print answer instance(s) to query | false |

print_boogie_certificate | bool | print certificate for reachability or non-reachability using a format understood by Boogie | false |

print_certificate | bool | print certificate for reachability or non-reachability | false |

print_fixedpoint_extensions | bool | use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules | true |

print_low_level_smt2 | bool | use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable) | false |

print_statistics | bool | print statistics | false |

print_with_variable_declarations | bool | use variable declarations when displaying rules (instead of attempting to use original names) | true |

spacer.arith.solver | unsigned int | arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 2 |

spacer.blast_term_ite_inflation | unsigned int | Maximum inflation for non-Boolean ite-terms expansion: 0 (none), k (multiplicative) | 3 |

spacer.ctp | bool | Enable counterexample-to-pushing | true |

spacer.dump_benchmarks | bool | Dump SMT queries as benchmarks | false |

spacer.dump_threshold | double | Threshold in seconds on dumping benchmarks | 5.0 |

spacer.elim_aux | bool | Eliminate auxiliary variables in reachability facts | true |

spacer.eq_prop | bool | Enable equality and bound propagation in arithmetic | true |

spacer.expand_bnd | bool | Enable expand-bound lemma generalization | false |

spacer.gg.concretize | bool | Enable global guidance concretize | true |

spacer.gg.conjecture | bool | Enable global guidance conjecture | true |

spacer.gg.subsume | bool | Enable global guidance subsume | true |

spacer.global | bool | Enable global guidance | false |

spacer.gpdr | bool | Use GPDR solving strategy for non-linear CHC | false |

spacer.gpdr.bfs | bool | Use BFS exploration strategy for expanding model search | true |

spacer.ground_pobs | bool | Ground pobs by using values from a model | true |

spacer.iuc | unsigned int | 0 = use old implementation of unsat-core-generation, 1 = use new implementation of IUC generation, 2 = use new implementation of IUC + min-cut optimization | 1 |

spacer.iuc.arith | unsigned int | 0 = use simple Farkas plugin, 1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin | 1 |

spacer.iuc.debug_proof | bool | prints proof used by unsat-core-learner for debugging purposes (debugging) | false |

spacer.iuc.old_hyp_reducer | bool | use old hyp reducer instead of new implementation, for debugging only | false |

spacer.iuc.print_farkas_stats | bool | prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging) | false |

spacer.iuc.split_farkas_literals | bool | Split Farkas literals | false |

spacer.keep_proxy | bool | keep proxy variables (internal parameter) | true |

spacer.logic | symbol | SMT-LIB logic to configure internal SMT solvers | |

spacer.max_level | unsigned int | Maximum level to explore | 4294967295 |

spacer.max_num_contexts | unsigned int | maximal number of contexts to create | 500 |

spacer.mbqi | bool | Enable mbqi | true |

spacer.min_level | unsigned int | Minimal level to explore | 0 |

spacer.native_mbp | bool | Use native mbp of Z3 | true |

spacer.order_children | unsigned int | SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse), 2 (random) | 0 |

spacer.p3.share_invariants | bool | Share invariants lemmas | false |

spacer.p3.share_lemmas | bool | Share frame lemmas | false |

spacer.propagate | bool | Enable propagate/pushing phase | true |

spacer.push_pob | bool | push blocked pobs to higher level | false |

spacer.push_pob_max_depth | unsigned int | Maximum depth at which push_pob is enabled | 4294967295 |

spacer.q3 | bool | Allow quantified lemmas in frames | true |

spacer.q3.instantiate | bool | Instantiate quantified lemmas | true |

spacer.q3.qgen.normalize | bool | normalize cube before quantified generalization | true |

spacer.q3.use_qgen | bool | use quantified lemma generalizer | false |

spacer.random_seed | unsigned int | Random seed to be used by SMT solver | 0 |

spacer.reach_dnf | bool | Restrict reachability facts to DNF | true |

spacer.reset_pob_queue | bool | SPACER: reset pob obligation queue when entering a new level | true |

spacer.restart_initial_threshold | unsigned int | Initial threshold for restarts | 10 |

spacer.restarts | bool | Enable resetting obligation queue | false |

spacer.simplify_lemmas_post | bool | simplify derived lemmas after inductive propagation | false |

spacer.simplify_lemmas_pre | bool | simplify derived lemmas before inductive propagation | false |

spacer.simplify_pob | bool | simplify pobs by removing redundant constraints | false |

spacer.trace_file | symbol | Log file for progress events | |

spacer.use_array_eq_generalizer | bool | SPACER: attempt to generalize lemmas with array equalities | true |

spacer.use_bg_invs | bool | Enable external background invariants | false |

spacer.use_derivations | bool | SPACER: using derivation mechanism to cache intermediate results for non-linear rules | true |

spacer.use_euf_gen | bool | Generalize lemmas and pobs using implied equalities | false |

spacer.use_inc_clause | bool | Use incremental clause to represent trans | true |

spacer.use_inductive_generalizer | bool | generalize lemmas using induction strengthening | true |

spacer.use_iuc | bool | Enable Interpolating Unsat Core(IUC) for lemma generalization | true |

spacer.use_lemma_as_cti | bool | SPACER: use a lemma instead of a CTI in flexible_trace | false |

spacer.use_lim_num_gen | bool | Enable limit numbers generalizer to get smaller numbers | false |

spacer.validate_lemmas | bool | Validate each lemma after generalization | false |

spacer.weak_abs | bool | Weak abstraction | true |

tab.selection | symbol | selection method for tabular strategy: weight (default), first, var-use | weight |

timeout | unsigned int | (default: infty) timeout in milliseconds. | 4294967295 |

validate | bool | validate result (by proof checking or model checking) | false |

xform.array_blast | bool | try to eliminate local array terms using Ackermannization -- some array terms may remain | false |

xform.array_blast_full | bool | eliminate all local array variables by QE | false |

xform.bit_blast | bool | bit-blast bit-vectors | false |

xform.coalesce_rules | bool | coalesce rules | false |

xform.coi | bool | use cone of influence simplification | true |

xform.compress_unbound | bool | compress tails with unbound variables | true |

xform.elim_term_ite | bool | Eliminate term-ite expressions | false |

xform.elim_term_ite.inflation | unsigned int | Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative) | 3 |

xform.fix_unbound_vars | bool | fix unbound variables in tail | false |

xform.inline_eager | bool | try eager inlining of rules | true |

xform.inline_linear | bool | try linear inlining method | true |

xform.inline_linear_branch | bool | try linear inlining method with potential expansion | false |

xform.instantiate_arrays | bool | Transforms P(a) into P(i, a[i] a) | false |

xform.instantiate_arrays.enforce | bool | Transforms P(a) into P(i, a[i]), discards a from predicate | false |

xform.instantiate_arrays.nb_quantifier | unsigned int | Gives the number of quantifiers per array | 1 |

xform.instantiate_arrays.slice_technique | symbol | <no-slicing>=> GetId(i) = i, <smash> => GetId(i) = true | no-slicing |

xform.instantiate_quantifiers | bool | instantiate quantified Horn clauses using E-matching heuristic | false |

xform.magic | bool | perform symbolic magic set transformation | false |

xform.quantify_arrays | bool | create quantified Horn clauses from clauses with arrays | false |

xform.scale | bool | add scaling variable to linear real arithmetic clauses | false |

xform.slice | bool | simplify clause set using slicing | true |

xform.subsumption_checker | bool | Enable subsumption checker (no support for model conversion) | true |

xform.tail_simplifier_pve | bool | propagate_variable_equivalences | true |

xform.transform_arrays | bool | Rewrites arrays equalities and applies select over store | false |

xform.unfold_rules | unsigned int | unfold rules statically using iterative squaring | 0 |

## Tactic injectivity

### Short Description:

Discover axioms of the form

`forall x. (= (g (f x)) x`

Mark`f`

as injectiveRewrite (sub)terms of the form

`(= (f x) (f y))`

to`(= x y)`

whenever`f`

is injective.

### Example

### Notes

- does not support cores nor proofs

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

produce_models | bool | model generation. | false |

## Tactic lia2card

### Short Description

Extract 0-1 integer variables used in cardinality and pseudo-Boolean constraints and replace them by Booleans.

### Example

### Notes

- The tactic does not (properly) support proofs or cores.

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

compile_equality | bool | (default:false) compile equalities into pseudo-Boolean equality |

## Tactic lia2pb

### Short Description

Reduce bounded LIA benchmark into 0-1 LIA benchmark.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

lia2pb_max_bits | unsigned int | (default: 32) maximum number of bits to be used (per variable) in lia2pb. | |

lia2pb_partial | bool | (default: false) partial lia2pb conversion. | |

lia2pb_total_bits | unsigned int | (default: 2048) total number of bits to be used (per problem) in lia2pb. |

## Tactic macro-finder

### Short Description

Identifies and applies macros.

### Long Description

It finds implicit macro definitions in quantifiers.
A main instance of a macro an equality that defines a function `f`

using some term `t`

that does not contain `f`

.
Other instances of macros are also recognized by the macro finder.

`(forall (x) (= (f x) t))`

`not (= (p x) t)`

is recognized as`(p x) = (not t)`

`(iff (= (f x) t) cond)`

rewrites to`(f x) = (if cond t else (k x))`

- add clause
`(not (= (k x) t))`

- add clause
`(= (+ (f x) s) t)`

becomes`(= (f x) (- t s))`

`(= (+ (* -1 (f x)) x) t)`

becomes`(= (f x) (- (- t s)))`

### Example

### Notes

- Supports proofs, unsat cores, but not goals with recursive function definitions.

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

elim_and | bool | (default: false) eliminate conjunctions during (internal) calls to the simplifier. | |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

produce_models | bool | model generation. | false |

produce_proofs | bool | proof generation. | false |

## Tactic max-bv-sharing

### Short Description

Use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers

### Long Description

Rewriter for "maximing" the number of shared terms. The idea is to rewrite AC terms to maximize sharing. This rewriter is particularly useful for reducing the number of Adders and Multipliers before "bit-blasting".

## Tactic nla2bv

### Short Description

Convert quantified NIA problems to bounded bit-vector arithmetic problems.

### Example

### Notes

- The tactic creates an under-approximation (a stronger set of formulas)

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

nla2bv_bv_size | unsigned int | default bit-vector size used by nla2bv tactic. | 4 |

nla2bv_divisor | unsigned int | nla2bv tactic parameter. | 2 |

nla2bv_max_bv_size | unsigned int | (default: inf) maximum bit-vector size used by nla2bv tactic | |

nla2bv_root | unsigned int | nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding. | 2 |

## Tactic nlsat

### Short Description

(try to) solve goal using a nonlinear arithmetic solver

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

check_lemmas | bool | check lemmas on the fly using an independent nlsat solver | false |

factor | bool | (default: true) factor polynomials. | |

factor_max_prime | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step | 31 |

factor_num_primes | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching | 1 |

factor_search_size | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space | 5000 |

inline_vars | bool | inline variables that can be isolated from equations (not supported in incremental mode) | false |

lazy | unsigned int | how lazy the solver is. | 0 |

log_lemmas | bool | display lemmas as self-contained SMT formulas | false |

max_conflicts | unsigned int | maximum number of conflicts. | 4294967295 |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_prime | unsigned int | (default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step. | |

max_search_size | unsigned int | (default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space. | |

min_mag | unsigned int | Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16 | 16 |

minimize_conflicts | bool | minimize conflicts | false |

num_primes | unsigned int | (default: 1) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching. | |

randomize | bool | randomize selection of a witness in nlsat. | true |

reorder | bool | reorder variables. | true |

seed | unsigned int | random seed. | 0 |

shuffle_vars | bool | use a random variable order. | false |

simplify_conflicts | bool | simplify conflicts using equalities before resolving them in nlsat solver. | true |

zero_accuracy | unsigned int | one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k) | 0 |

## Tactic nnf

### Short Description:

The tactic converts formulas to negation normal form (NNF)

### Long Description

In NNF, negations only appear in front of atomic formulas.

Standard rules for conversion into negation normal form are:

`(not (and p q))`

is converted to`(or (not p) (not q))`

`(not (or p q))`

is converted to`(and (not p) (not q))`

`(not (not p))`

is converted to`p`

`(not (exists x. p))`

is converted to`(forall x. (not p))`

`(not (forall x. p))`

is converted to`(exists x. (not p))`

Once all negations are pushed inside, the resulting formula is in NNF.

### Example

### Notes

- supports unsat cores, proof terms

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

ignore_labels | bool | remove/ignore labels in the input formula, this option is ignored if proofs are enabled | false |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

mode | symbol | NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full | skolem |

sk_hack | bool | hack for VCC | false |

## Tactic normalize-bounds

### Short Description

Replace $x$ with $x' + l$, when $l \leq x$ where $x'$ is a fresh variable. Note that, after the transformation $0 \leq x'$.

### Example

### Notes

- supports proofs and cores

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

norm_int_only | bool | normalize only the bounds of integer constants. | true |

produce_models | bool | model generation. | false |

## Tactic occf

### Short Description

Put goal in one constraint per clause normal form

### Long Description

Put clauses in the assertion set in
OOC (one constraint per clause) form.
Constraints occurring in formulas that
are not clauses are ignored.
The formula can be put into CNF by
using `mk_sat_preprocessor`

strategy.

### Example

### Notes

- Does not support proofs
- only clauses are considered

## Tactic pb2bv

### Short Description

Convert pseudo-boolean constraints to bit-vectors

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | 4294967295 | |

cardinality.encoding | symbol | encoding used for cardinality constraints: grouped, bimander, ordered, unate, circuit | none |

elim_ite | bool | eliminate ite in favor of and/or | true |

flat_and_or | bool | create nary applications for and,or | true |

ite_extra_rules | bool | true | |

keep_cardinality_constraints | bool | retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver | false |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

pb.solver | symbol | encoding used for Pseudo-Boolean constraints: totalizer, sorting, binary_merge, bv, solver. PB constraints are retained if set to 'solver' | solver |

pb2bv_all_clauses_limit | unsigned int | (default: 8) maximum number of literals for using equivalent CNF encoding of PB constraint. | |

pb2bv_cardinality_limit | unsigned int | (default: inf) limit for using arc-consistent cardinality constraint encoding. |

## Tactic propagate-bv-bounds

### Short Description

Contextual bounds simplification tactic.

### Example

### Notes

- assumes that bit-vector inequalities have been simplified to use bvule/bvsle

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

max_depth | unsigned int | maximum term depth. | 1024 |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | (default: infty) maximum number of steps. | 4294967295 |

propagate_eq | bool | enable equality propagation from bounds. | false |

## Tactic propagate-ineqs

### Short Description

Propagate ineqs/bounds, remove subsumed inequalities

### Long Description

This tactic performs the following tasks:

Propagate bounds using the bound_propagator.

Eliminate subsumed inequalities.

- For example:
`x - y >= 3`

can be replaced with true if we know that`x >= 3`

and`y <= 0`

- For example:
Convert inequalities of the form

`p <= k`

and`p >= k`

into`p = k`

, where`p`

is a polynomial and`k`

is a constant.

This strategy assumes the input is in arith LHS mode. This can be achieved by using option :arith-lhs true in the simplifier.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

bound_max_refinements | unsigned int | (default: 16) maximum number of bound refinements (per round) for unbounded variables. | |

bound_threshold | double | (default: 0.05) bound propagation improvement threshold ratio. |

## Tactic propagate-values

### Short Description:

Tactic for propagating equalities `(= t v)`

where `v`

is a value

### Long Description

In a context where terms are equated to constants it is invariably beneficial to replace terms, that can be compound, with the constants and then simplify the resulting formulas. The propagate-values tactic accomplishes the task of replacing such terms.

### Example

### Notes

- supports unsat cores

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | 4294967295 | |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

ite_extra_rules | bool | true | |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_rounds | unsigned int | maximum number of rounds. | 4 |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

rewrite_patterns | bool | rewrite patterns. | false |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

## Tactic purify-arith

### Short Description

Eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects. These operators can be replaced by introcing fresh variables and using multiplication and addition.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | 4294967295 | |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

complete | bool | add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root | true |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_inverses | bool | eliminate inverse trigonometric functions (asin, acos, atan). | true |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_root_objects | bool | eliminate root objects. | true |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_labels | bool | remove/ignore labels in the input formula, this option is ignored if proofs are enabled | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

ite_extra_rules | bool | true | |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mode | symbol | NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full | skolem |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

rewrite_patterns | bool | rewrite patterns. | false |

sk_hack | bool | hack for VCC | false |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

## Tactic qe

### Short Description

Apply quantifier elimination on quantified sub-formulas.

### Long Description

The tactic applies quantifier elimination procedures on quantified sub-formulas. It relies on theory plugins that can perform quanifier elimination for selected theories. These plugins include Booleans, bit-vectors, arithmetic (linear), arrays, and data-types (term algebra). It performs feasibility checks on cases to throttle the set of sub-formulas where quantifier elimination is applied.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

eliminate_variables_as_block | bool | (default: true) eliminate variables as a block (true) or one at a time (false) | |

qe_nonlinear | bool | (default: false) enable virtual term substitution. |

## Tactic qffp

### Short Description

Tactic for QF_FP formulas

## Tactic qffpbv

### Short Description

Tactic for QF_FPBV formulas

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

abce | bool | eliminate blocked clauses using asymmetric literals | false |

acce | bool | eliminate covered clauses using asymmetric added literals | false |

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

anf | bool | enable ANF based simplification in-processing | false |

anf.delay | unsigned int | delay ANF simplification by in-processing round | 2 |

anf.exlin | bool | enable extended linear simplification | false |

arith.auto_config_simplex | bool | force simplex solver in auto_config | false |

arith.bprop_on_pivoted_rows | bool | propagate bounds on rows changed by the pivot operation | true |

arith.branch_cut_ratio | unsigned int | branch/cut ratio for linear integer arithmetic | 2 |

arith.dump_lemmas | bool | dump arithmetic theory lemmas to files | false |

arith.eager_eq_axioms | bool | eager equality axioms | true |

arith.enable_hnf | bool | enable hnf (Hermite Normal Form) cuts | true |

arith.greatest_error_pivot | bool | Pivoting strategy | false |

arith.ignore_int | bool | treat integer variables as real | false |

arith.int_eq_branch | bool | branching using derived integer equations | false |

arith.min | bool | minimize cost | false |

arith.nl | bool | (incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2 | true |

arith.nl.branching | bool | branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2 | true |

arith.nl.delay | unsigned int | number of calls to final check before invoking bounded nlsat check | 500 |

arith.nl.expp | bool | expensive patching | false |

arith.nl.gr_q | unsigned int | grobner's quota | 10 |

arith.nl.grobner | bool | run grobner's basis heuristic | true |

arith.nl.grobner_cnfl_to_report | unsigned int | grobner's maximum number of conflicts to report | 1 |

arith.nl.grobner_eqs_growth | unsigned int | grobner's number of equalities growth | 10 |

arith.nl.grobner_expr_degree_growth | unsigned int | grobner's maximum expr degree growth | 2 |

arith.nl.grobner_expr_size_growth | unsigned int | grobner's maximum expr size growth | 2 |

arith.nl.grobner_frequency | unsigned int | grobner's call frequency | 4 |

arith.nl.grobner_max_simplified | unsigned int | grobner's maximum number of simplifications | 10000 |

arith.nl.grobner_subs_fixed | unsigned int | 0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 1 |

arith.nl.horner | bool | run horner's heuristic | true |

arith.nl.horner_frequency | unsigned int | horner's call frequency | 4 |

arith.nl.horner_row_length_limit | unsigned int | row is disregarded by the heuristic if its length is longer than the value | 10 |

arith.nl.horner_subs_fixed | unsigned int | 0 - no subs, 1 - substitute, 2 - substitute fixed zeros only | 2 |

arith.nl.nra | bool | call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6 | true |

arith.nl.order | bool | run order lemmas | true |

arith.nl.rounds | unsigned int | threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2 | 1024 |

arith.nl.tangents | bool | run tangent lemmas | true |

arith.print_ext_var_names | bool | print external variable names | false |

arith.print_stats | bool | print statistic | false |

arith.propagate_eqs | bool | propagate (cheap) equalities | true |

arith.propagation_mode | unsigned int | 0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds | 1 |

arith.random_initial_value | bool | use random initial values in the simplex-based procedure for linear arithmetic | false |

arith.rep_freq | unsigned int | the report frequency, in how many iterations print the cost and other info | 0 |

arith.simplex_strategy | unsigned int | simplex strategy for the solver | 0 |

arith.solver | unsigned int | arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver | 6 |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

array.extensional | bool | extensional array theory | true |

array.weak | bool | weak array theory | false |

asymm_branch | bool | asymmetric branching | true |

asymm_branch.all | bool | asymmetric branching on all literals per clause | false |

asymm_branch.delay | unsigned int | number of simplification rounds to wait until invoking asymmetric branch simplification | 1 |

asymm_branch.limit | unsigned int | approx. maximum number of literals visited during asymmetric branching | 100000000 |

asymm_branch.rounds | unsigned int | maximal number of rounds to run asymmetric branch simplifications if progress is made | 2 |

asymm_branch.sampled | bool | use sampling based asymmetric branching based on binary implication graph | true |

ate | bool | asymmetric tautology elimination | true |

auto_config | bool | automatically configure solver | true |

backtrack.conflicts | unsigned int | number of conflicts before enabling chronological backtracking | 4000 |

backtrack.scopes | unsigned int | number of scopes to enable chronological backtracking | 100 |

bca | bool | blocked clause addition - add blocked binary clauses | false |

bce | bool | eliminate blocked clauses | false |

bce_at | unsigned int | eliminate blocked clauses only once at the given simplification round | 2 |

bce_delay | unsigned int | delay eliminate blocked clauses until simplification round | 2 |

binspr | bool | enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_add | bool | bit-blast adders. | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | 4294967295 | |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_full | bool | bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms. | false |

blast_mul | bool | bit-blast multipliers (and dividers, remainders). | true |

blast_quant | bool | bit-blast quantified variables. | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

blocked_clause_limit | unsigned int | maximum number of literals visited during blocked clause elimination | 100000000 |

bound_simplifier | bool | apply bounds simplification during pre-processing | true |

branching.anti_exploration | bool | apply anti-exploration heuristic for branch selection | false |

branching.heuristic | symbol | branching heuristic vsids, chb | vsids |

burst_search | unsigned int | number of conflicts before first global simplification | 100 |

bv.delay | bool | delay internalize expensive bit-vector operations | false |

bv.enable_int2bv | bool | enable support for int2bv and bv2int operators | true |

bv.eq_axioms | bool | enable redundant equality axioms for bit-vectors | true |

bv.reflect | bool | create enode for every bit-vector term | true |

bv.size_reduce | bool | pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant | false |

bv.watch_diseq | bool | use watch lists instead of eager axioms for bit-vectors | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

candidate_models | bool | create candidate models even when quantifier or theory reasoning is incomplete | false |

cardinality.encoding | symbol | encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit | grouped |

cardinality.solver | bool | use cardinality solver | true |

case_split | unsigned int | 0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity | 1 |

cce | bool | eliminate covered clauses | false |

check_lemmas | bool | check lemmas on the fly using an independent nlsat solver | false |

clause_proof | bool | record a clausal proof | false |

common_patterns | bool | minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns | true |

complete | bool | add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root | true |

context_solve | bool | solve equalities under disjunctions. | false |

core.extend_nonlocal_patterns | bool | extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier's body | false |

core.extend_patterns | bool | extend unsat core with literals that trigger (potential) quantifier instances | false |

core.extend_patterns.max_distance | unsigned int | limits the distance of a pattern-extended unsat core | 4294967295 |

core.minimize | bool | minimize unsat core produced by SMT context | false |

core.minimize_partial | bool | apply partial (cheap) core minimization | false |

core.validate | bool | [internal] validate unsat core produced by SMT context. This option is intended for debugging | false |

cube_depth | unsigned int | cube depth. | 1 |

cut | bool | enable AIG based simplification in-processing | false |

cut.aig | bool | extract aigs (and ites) from cluases for cut simplification | false |

cut.delay | unsigned int | delay cut simplification by in-processing round | 2 |

cut.dont_cares | bool | integrate dont cares with cuts | true |

cut.force | bool | force redoing cut-enumeration until a fixed-point | false |

cut.lut | bool | extract luts from clauses for cut simplification | false |

cut.npn3 | bool | extract 3 input functions from clauses for cut simplification | false |

cut.redundancies | bool | integrate redundancy checking of cuts | true |

cut.xor | bool | extract xors from clauses for cut simplification | false |

dack | unsigned int | 0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution | 1 |

dack.eq | bool | enable dynamic ackermannization for transtivity of equalities | false |

dack.factor | double | number of instance per conflict | 0.1 |

dack.gc | unsigned int | Dynamic ackermannization garbage collection frequency (per conflict) | 2000 |

dack.gc_inv_decay | double | Dynamic ackermannization garbage collection decay | 0.8 |

dack.threshold | unsigned int | number of times the congruence rule must be used before Leibniz's axiom is expanded | 10 |

ddfw.init_clause_weight | unsigned int | initial clause weight for DDFW local search | 8 |

ddfw.reinit_base | unsigned int | increment basis for geometric backoff scheme of re-initialization of weights | 10000 |

ddfw.restart_base | unsigned int | number of flips used a starting point for hessitant restart backoff | 100000 |

ddfw.threads | unsigned int | number of ddfw threads to run in parallel with sat solver | 0 |

ddfw.use_reward_pct | unsigned int | percentage to pick highest reward variable when it has reward 0 | 15 |

ddfw_search | bool | use ddfw local search instead of CDCL | false |

delay_units | bool | if true then z3 will not restart when a unit clause is learned | false |

delay_units_threshold | unsigned int | maximum number of learned unit clauses before restarting, ignored if delay_units is false | 32 |

dimacs.core | bool | extract core from DIMACS benchmarks | false |

distributivity | bool | minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas | true |

distributivity_blowup | unsigned int | maximum overhead for applying distributivity during CNF encoding | 32 |

div0_ackermann_limit | unsigned int | a bound for number of congruence Ackermann lemmas for div0 modelling | 1000 |

drat.activity | bool | dump variable activities | false |

drat.binary | bool | use Binary DRAT output format | false |

drat.check_sat | bool | build up internal trace, check satisfying model | false |

drat.check_unsat | bool | build up internal proof and check | false |

drat.disable | bool | override anything that enables DRAT | false |

drat.file | symbol | file to dump DRAT proofs | |

dt_lazy_splits | unsigned int | How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy | 1 |

dyn_sub_res | bool | dynamic subsumption resolution for minimizing learned clauses | true |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_inverses | bool | eliminate inverse trigonometric functions (asin, acos, atan). | true |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_root_objects | bool | eliminate root objects. | true |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

elim_unconstrained | bool | pre-processing: eliminate unconstrained subterms | true |

elim_vars | bool | enable variable elimination using resolution during simplification | true |

elim_vars_bdd | bool | enable variable elimination using BDD recompilation during simplification | true |

elim_vars_bdd_delay | unsigned int | delay elimination of variables using BDDs until after simplification round | 3 |

eliminate_mod | bool | eliminate modulus from equations | true |

ematching | bool | E-Matching based quantifier instantiation | true |

enable_pre_simplify | bool | enable pre simplifications before the bounded search | false |

eq2ineq | bool | expand equalities into two inequalities | false |

euf | bool | enable euf solver (this feature is preliminary and not ready for general consumption) | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

factor | bool | (default: true) factor polynomials. | |

factor_max_prime | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step | 31 |

factor_num_primes | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching | 1 |

factor_search_size | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space | 5000 |

fail_if_inconclusive | bool | (default: true) fail if found unsat (sat) for under (over) approximated goal. | |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

force_cleanup | bool | force cleanup to remove tautologies and simplify clauses | false |

gc | symbol | garbage collection strategy: psm, glue, glue_psm, dyn_psm | glue_psm |

gc.burst | bool | perform eager garbage collection during initialization | false |

gc.defrag | bool | defragment clauses when garbage collecting | true |

gc.increment | unsigned int | increment to the garbage collection threshold | 500 |

gc.initial | unsigned int | learned clauses garbage collection frequency | 20000 |

gc.k | unsigned int | learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm) | 7 |

gc.small_lbd | unsigned int | learned clauses with small LBD are never deleted (only used in dyn_psm) | 3 |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_labels | bool | remove/ignore labels in the input formula, this option is ignored if proofs are enabled | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

induction | bool | enable generation of induction lemmas | false |

inline_vars | bool | inline variables that can be isolated from equations (not supported in incremental mode) | false |

inprocess.max | unsigned int | maximal number of inprocessing passes | 4294967295 |

inprocess.out | symbol | file to dump result of the first inprocessing step and exit | |

ite_chaing | bool | minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains | true |

ite_extra | bool | (default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas | |

ite_extra_rules | bool | true | |

ite_solver | bool | use if-then-else solver. | true |

lazy | unsigned int | how lazy the solver is. | 0 |

learned | bool | (default: false) collect also learned clauses. | |

lemma_gc_strategy | unsigned int | lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none | 0 |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

local_search | bool | use local search instead of CDCL | false |

local_search_dbg_flips | bool | write debug information for number of flips | false |

local_search_mode | symbol | local search algorithm, either default wsat or qsat | wsat |

local_search_threads | unsigned int | number of local search threads to find satisfiable solution | 0 |

log_lemmas | bool | display lemmas as self-contained SMT formulas | false |

logic | symbol | logic used to setup the SMT solver | |

lookahead.cube.cutoff | symbol | cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat | depth |

lookahead.cube.depth | unsigned int | cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth. | 1 |

lookahead.cube.fraction | double | adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat | 0.4 |

lookahead.cube.freevars | double | cube free variable fraction. Used when lookahead.cube.cutoff is freevars | 0.8 |

lookahead.cube.psat.clause_base | double | clause base for PSAT cutoff | 2 |

lookahead.cube.psat.trigger | double | trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat | 5 |

lookahead.cube.psat.var_exp | double | free variable exponent for PSAT cutoff | 1 |

lookahead.delta_fraction | double | number between 0 and 1, the smaller the more literals are selected for double lookahead | 1.0 |

lookahead.double | bool | enable doubld lookahead | true |

lookahead.global_autarky | bool | prefer to branch on variables that occur in clauses that are reduced | false |

lookahead.preselect | bool | use pre-selection of subset of variables for branching | false |

lookahead.reward | symbol | select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu | march_cu |

lookahead.use_learned | bool | use learned clauses when selecting lookahead literal | false |

lookahead_scores | bool | extract lookahead scores. A utility that can only be used from the DIMACS front-end | false |

lookahead_simplify | bool | use lookahead solver during simplification | false |

lookahead_simplify.bca | bool | add learned binary clauses as part of lookahead simplification | true |

macro_finder | bool | try to find universally quantified formulas that can be viewed as macros | false |

max_args | unsigned int | (default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic. | |

max_conflicts | unsigned int | maximum number of conflicts before giving up. | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_prime | unsigned int | (default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step. | |

max_rounds | unsigned int | maximum number of rounds. | 4 |

max_search_size | unsigned int | (default: infty) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space. | |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mbqi | bool | model based quantifier instantiation (MBQI) | true |

mbqi.force_template | unsigned int | some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template | 10 |

mbqi.id | string | Only use model-based instantiation for quantifiers with id's beginning with string | |

mbqi.max_cexs | unsigned int | initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation | 1 |

mbqi.max_cexs_incr | unsigned int | increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI | 0 |

mbqi.max_iterations | unsigned int | maximum number of rounds of MBQI | 1000 |

mbqi.trace | bool | generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied | false |

min_mag | unsigned int | Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16 | 16 |

minimize_conflicts | bool | minimize conflicts | false |

minimize_lemmas | bool | minimize learned clauses | true |

mode | symbol | NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full | skolem |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

nla2bv_bv_size | unsigned int | default bit-vector size used by nla2bv tactic. | 4 |

nla2bv_divisor | unsigned int | nla2bv tactic parameter. | 2 |

nla2bv_max_bv_size | unsigned int | (default: inf) maximum bit-vector size used by nla2bv tactic | |

nla2bv_root | unsigned int | nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding. | 2 |

num_primes | unsigned int | (default: 1) Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching. | |

override_incremental | bool | override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused | false |

pb.conflict_frequency | unsigned int | conflict frequency for Pseudo-Boolean theory | 1000 |

pb.learn_complements | bool | learn complement literals for Pseudo-Boolean theory | true |

pb.lemma_format | symbol | generate either cardinality or pb lemmas | cardinality |

pb.min_arity | unsigned int | minimal arity to compile pb/cardinality constraints to CNF | 9 |

pb.resolve | symbol | resolution strategy for boolean algebra solver: cardinality, rounding | cardinality |

pb.solver | symbol | method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver) | solver |

phase | symbol | phase selection strategy: always_false, always_true, basic_caching, random, caching, local_search | caching |

phase.sticky | bool | use sticky phase caching | true |

phase_caching_off | unsigned int | number of conflicts while phase caching is off | 100 |

phase_caching_on | unsigned int | number of conflicts while phase caching is on | 400 |

phase_selection | unsigned int | phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory | 3 |

prob_search | bool | use probsat local search instead of CDCL | false |

probing | bool | apply failed literal detection during simplification | true |

probing_binary | bool | probe binary clauses | true |

probing_cache | bool | add binary literals as lemmas | true |

probing_cache_limit | unsigned int | cache binaries unless overall memory usage exceeds cache limit | 1024 |

probing_limit | unsigned int | limit to the number of probe calls | 5000000 |

propagate.prefetch | bool | prefetch watch lists for assigned literals | true |

propagate_values | bool | pre-processing: propagate values | true |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

pull_nested_quantifiers | bool | pre-processing: pull nested quantifiers | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

q.lift_ite | unsigned int | 0 - don not lift non-ground if-then-else, 1 - use conservative ite lifting, 2 - use full lifting of if-then-else under quantifiers | 0 |

q.lite | bool | Use cheap quantifier elimination during pre-processing | false |

qi.cost | string | expression specifying what is the cost of a given quantifier instantiation | (+ weight generation) |

qi.eager_threshold | double | threshold for eager quantifier instantiation | 10.0 |

qi.lazy_threshold | double | threshold for lazy quantifier instantiation | 20.0 |

qi.max_instances | unsigned int | maximum number of quantifier instantiations | 4294967295 |

qi.max_multi_patterns | unsigned int | specify the number of extra multi patterns | 0 |

qi.profile | bool | profile quantifier instantiation | false |

qi.profile_freq | unsigned int | how frequent results are reported by qi.profile | 4294967295 |

qi.quick_checker | unsigned int | specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances | 0 |

quasi_macros | bool | try to find universally quantified formulas that are quasi-macros | false |

random_freq | double | frequency of random case splits | 0.01 |

random_seed | unsigned int | random seed for the smt solver | 0 |

randomize | bool | randomize selection of a witness in nlsat. | true |

refine_inj_axioms | bool | pre-processing: refine injectivity axioms | true |

relevancy | unsigned int | relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant | 2 |

reorder | bool | reorder variables. | true |

reorder.activity_scale | unsigned int | scaling factor for activity update | 100 |

reorder.base | unsigned int | number of conflicts per random reorder | 4294967295 |

reorder.itau | double | inverse temperature for softmax | 4.0 |

rephase.base | unsigned int | number of conflicts per rephase | 1000 |

resolution.cls_cutoff1 | unsigned int | limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination | 100000000 |

resolution.cls_cutoff2 | unsigned int | limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination | 700000000 |

resolution.limit | unsigned int | approx. maximum number of literals visited during variable elimination | 500000000 |

resolution.lit_cutoff_range1 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 700 |

resolution.lit_cutoff_range2 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 400 |

resolution.lit_cutoff_range3 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 300 |

resolution.occ_cutoff | unsigned int | first cutoff (on number of positive/negative occurrences) for Boolean variable elimination | 10 |

resolution.occ_cutoff_range1 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 8 |

resolution.occ_cutoff_range2 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 5 |

resolution.occ_cutoff_range3 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 3 |

restart | symbol | restart strategy: static, luby, ema or geometric | ema |

restart.emafastglue | double | ema alpha factor for fast moving average | 0.03 |

restart.emaslowglue | double | ema alpha factor for slow moving average | 1e-05 |

restart.factor | double | restart increment factor for geometric strategy | 1.5 |

restart.fast | bool | use fast restart approach only removing less active literals. | true |

restart.initial | unsigned int | initial restart (number of conflicts) | 2 |

restart.margin | double | margin between fast and slow restart factors. For ema | 1.1 |

restart.max | unsigned int | maximal number of restarts. | 4294967295 |

restart_factor | double | when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold | 1.1 |

restart_strategy | unsigned int | 0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic | 1 |

restricted_quasi_macros | bool | try to find universally quantified formulas that are restricted quasi-macros | false |

retain_blocked_clauses | bool | retain blocked clauses as lemmas | true |

rewrite_patterns | bool | rewrite patterns. | false |

scc | bool | eliminate Boolean variables by computing strongly connected components | true |

scc.tr | bool | apply transitive reduction, eliminate redundant binary clauses | true |

search.sat.conflicts | unsigned int | period for solving for sat (in number of conflicts) | 400 |

search.unsat.conflicts | unsigned int | period for solving for unsat (in number of conflicts) | 400 |

seed | unsigned int | random seed. | 0 |

seq.max_unfolding | unsigned int | maximal unfolding depth for checking string equations and regular expressions | 1000000000 |

seq.min_unfolding | unsigned int | initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths | 1 |

seq.split_w_len | bool | enable splitting guided by length constraints | true |

seq.validate | bool | enable self-validation of theory axioms created by seq theory | false |

shuffle_vars | bool | use a random variable order. | false |

simplify.delay | unsigned int | set initial delay of simplification by a conflict count | 0 |

simplify_conflicts | bool | simplify conflicts using equalities before resolving them in nlsat solver. | true |

sk_hack | bool | hack for VCC | false |

smt | bool | use the SAT solver based incremental SMT core | false |

smt.proof.check | bool | check proofs on the fly during SMT search | false |

solve_eqs | bool | pre-processing: solve equalities | true |

solve_eqs_max_occs | unsigned int | (default: infty) maximum number of occurrences for considering a variable for gaussian eliminations. | 4294967295 |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

split_factors | bool | apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)). | true |

str.aggressive_length_testing | bool | prioritize testing concrete length values over generating more options | false |

str.aggressive_unroll_testing | bool | prioritize testing concrete regex unroll counts over generating more options | true |

str.aggressive_value_testing | bool | prioritize testing concrete string constant values over generating more options | false |

str.fast_length_tester_cache | bool | cache length tester constants instead of regenerating them | false |

str.fast_value_tester_cache | bool | cache value tester constants instead of regenerating them | true |

str.fixed_length_naive_cex | bool | construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only) | true |

str.fixed_length_refinement | bool | use abstraction refinement in fixed-length equation solver (Z3str3 only) | false |

str.overlap_priority | double | theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true | -0.1 |

str.regex_automata_difficulty_threshold | unsigned int | difficulty threshold for regex automata heuristics | 1000 |

str.regex_automata_failed_automaton_threshold | unsigned int | number of failed automaton construction attempts after which a full automaton is automatically built | 10 |

str.regex_automata_failed_intersection_threshold | unsigned int | number of failed automaton intersection attempts after which intersection is always computed | 10 |

str.regex_automata_intersection_difficulty_threshold | unsigned int | difficulty threshold for regex intersection heuristics | 1000 |

str.regex_automata_length_attempt_threshold | unsigned int | number of length/path constraint attempts before checking unsatisfiability of regex terms | 10 |

str.string_constant_cache | bool | cache all generated string constants generated from anywhere in theory_str | true |

str.strong_arrangements | bool | assert equivalences instead of implications when generating string arrangement axioms | true |

string_solver | symbol | solver for string/sequence theories. options are: 'z3str3' (specialized string solver), 'seq' (sequence solver), 'auto' (use static features to choose best solver), 'empty' (a no-op solver that forces an answer unknown if strings were used), 'none' (no solver) | seq |

subsumption | bool | eliminate subsumed clauses | true |

subsumption.limit | unsigned int | approx. maximum number of literals visited during subsumption (and subsumption resolution) | 100000000 |

theory_aware_branching | bool | Allow the context to use extra information from theory solvers regarding literal branching prioritization. | false |

theory_case_split | bool | Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead. | false |

theory_solver | bool | theory solvers. | true |

threads | unsigned int | maximal number of parallel threads. | 1 |

threads.cube_frequency | unsigned int | frequency for using cubing | 2 |

threads.max_conflicts | unsigned int | maximal number of conflicts between rounds of cubing for parallel SMT | 400 |

variable_decay | unsigned int | multiplier (divided by 100) for the VSIDS activity increment | 110 |

zero_accuracy | unsigned int | one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k) | 0 |

## Tactic qfnra-nlsat

### Short Description

Self-contained tactic that attempts to solve goal using a nonlinear arithmetic solver.
It first applies tactics, such as `purify-arith`

to convert the goal into a format
where the `nlsat`

tactic applies.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | 4294967295 | |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

check_lemmas | bool | check lemmas on the fly using an independent nlsat solver | false |

common_patterns | bool | minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns | true |

complete | bool | add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root | true |

context_solve | bool | solve equalities under disjunctions. | false |

distributivity | bool | minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas | true |

distributivity_blowup | unsigned int | maximum overhead for applying distributivity during CNF encoding | 32 |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_inverses | bool | eliminate inverse trigonometric functions (asin, acos, atan). | true |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_root_objects | bool | eliminate root objects. | true |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eliminate_mod | bool | eliminate modulus from equations | true |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

factor | bool | (default: true) factor polynomials. | |

factor_max_prime | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter limits the maximum prime number p to be used in the first step | 31 |

factor_num_primes | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. The search space may be reduced by factoring the polynomial in different GF(p)'s. This parameter specify the maximum number of finite factorizations to be considered, before lifiting and searching | 1 |

factor_search_size | unsigned int | parameter for the polynomial factorization procedure in the algebraic number module. Z3 polynomial factorization is composed of three steps: factorization in GF(p), lifting and search. This parameter can be used to limit the search space | 5000 |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_labels | bool | remove/ignore labels in the input formula, this option is ignored if proofs are enabled | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

inline_vars | bool | inline variables that can be isolated from equations (not supported in incremental mode) | false |

ite_chaing | bool | minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains | true |

ite_extra | bool | add redundant clauses (that improve unit propagation) when encoding if-then-else formulas | true |

ite_extra_rules | bool | true | |

ite_solver | bool | use if-then-else solver. | true |

lazy | unsigned int | how lazy the solver is. | 0 |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

log_lemmas | bool | display lemmas as self-contained SMT formulas | false |

max_args | unsigned int | (default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic. | |

max_conflicts | unsigned int | maximum number of conflicts. | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_prime | unsigned int | ||

max_rounds | unsigned int | maximum number of rounds. | 4 |

max_search_size | unsigned int | ||

max_steps | unsigned int | maximum number of steps | 4294967295 |

min_mag | unsigned int | Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16 | 16 |

minimize_conflicts | bool | minimize conflicts | false |

mode | symbol | skolem | |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

num_primes | unsigned int | ||

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

randomize | bool | randomize selection of a witness in nlsat. | true |

reorder | bool | reorder variables. | true |

rewrite_patterns | bool | rewrite patterns. | false |

seed | unsigned int | random seed. | 0 |

shuffle_vars | bool | use a random variable order. | false |

simplify_conflicts | bool | simplify conflicts using equalities before resolving them in nlsat solver. | true |

sk_hack | bool | hack for VCC | false |

solve_eqs_max_occs | unsigned int | (default: infty) maximum number of occurrences for considering a variable for gaussian eliminations. | 4294967295 |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

split_factors | bool | apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)). | true |

theory_solver | bool | theory solvers. | true |

zero_accuracy | unsigned int | one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k) | 0 |

## Tactic quasi-macro-finder

### Short Description

dentifies and applies quasi-macros.

### Long Description

A quasi macro defines a function symbol that contains more arguments than the number of bound variables it defines. The additional arguments are functions of the bound variables.

### Example

### Notes

- Supports proofs and cores

## Tactic recover-01

### Short Description

Recover 01 variables from propositional constants.

### Long Description

Search for clauses of the form

` p or q or x = 0`

~p or q or x = k1

p or ~q or x = k2

~p or ~q or x = k1+k2

Then, replaces

`x`

with`k1*y1 + k2*y2`

`p`

with`y1 = 1`

`q`

with`y2 = 1`

where `y1`

and `y2`

are fresh 01 variables.

The clauses are also removed.

### Example

### Notes

- does not support proofs, does not support cores

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | 4294967295 | |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

ite_extra_rules | bool | true | |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

recover_01_max_bits | unsigned int | maximum number of bits to consider in a clause. | 10 |

rewrite_patterns | bool | rewrite patterns. | false |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

## Tactic reduce-args

### Short Description:

Reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.

### Long Description

Example, suppose we have a function $f$ with 2 arguments. There are 1000 applications of this function, but the first argument is always $a$, $b$ or $c$. Thus, we replace the $f(t_1, t_2)$ with

- $f_a(t_2)$ if $t_1 = a$
- $f_b(t_2)$ if $t_2 = b$
- $f_c(t_2)$ if $t_2 = c$

Since $f_a$, $f_b$, $f_c$ are new symbols, satisfiability is preserved.

This transformation is very similar in spirit to the Ackermman's reduction.
For each function `f`

and argument position of `f`

it checks if all occurrences of `f`

uses a value at position `i`

.
The values may be different, but all occurrences have to be values for the reduction to be applicable.
It creates a fresh function for each of the different values at position `i`

.

### Example

### Notes

- supports unsat cores
- does not support proof terms

## Tactic reduce-bv-size

### Short Description

Rry to reduce bit-vector sizes using inequalities.

### Long Description

Reduce the number of bits used to encode constants, by using signed bounds. Example: suppose $x$ is a bit-vector of size 8, and we have signed bounds for $x$ such that:

` -2 <= x <= 2`

Then, $x$ can be replaced by `((sign-extend 5) k)`

where `k`

is a fresh bit-vector constant of size 3.

### Example

### Notes

- does not support proofs, nor unsat cores

## Tactic sat

### Short Description

Try to solve goal using a SAT solver

## Tactic sat-preprocess

### Short Description

Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution).

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

abce | bool | eliminate blocked clauses using asymmetric literals | false |

acce | bool | eliminate covered clauses using asymmetric added literals | false |

anf | bool | enable ANF based simplification in-processing | false |

anf.delay | unsigned int | delay ANF simplification by in-processing round | 2 |

anf.exlin | bool | enable extended linear simplification | false |

asymm_branch | bool | asymmetric branching | true |

asymm_branch.all | bool | asymmetric branching on all literals per clause | false |

asymm_branch.delay | unsigned int | number of simplification rounds to wait until invoking asymmetric branch simplification | 1 |

asymm_branch.limit | unsigned int | approx. maximum number of literals visited during asymmetric branching | 100000000 |

asymm_branch.rounds | unsigned int | maximal number of rounds to run asymmetric branch simplifications if progress is made | 2 |

asymm_branch.sampled | bool | use sampling based asymmetric branching based on binary implication graph | true |

ate | bool | asymmetric tautology elimination | true |

backtrack.conflicts | unsigned int | number of conflicts before enabling chronological backtracking | 4000 |

backtrack.scopes | unsigned int | number of scopes to enable chronological backtracking | 100 |

bca | bool | blocked clause addition - add blocked binary clauses | false |

bce | bool | eliminate blocked clauses | false |

bce_at | unsigned int | eliminate blocked clauses only once at the given simplification round | 2 |

bce_delay | unsigned int | delay eliminate blocked clauses until simplification round | 2 |

binspr | bool | enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models | false |

blocked_clause_limit | unsigned int | maximum number of literals visited during blocked clause elimination | 100000000 |

branching.anti_exploration | bool | apply anti-exploration heuristic for branch selection | false |

branching.heuristic | symbol | branching heuristic vsids, chb | vsids |

burst_search | unsigned int | number of conflicts before first global simplification | 100 |

cardinality.encoding | symbol | encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit | grouped |

cardinality.solver | bool | use cardinality solver | true |

cce | bool | eliminate covered clauses | false |

core.minimize | bool | minimize computed core | false |

core.minimize_partial | bool | apply partial (cheap) core minimization | false |

cut | bool | enable AIG based simplification in-processing | false |

cut.aig | bool | extract aigs (and ites) from cluases for cut simplification | false |

cut.delay | unsigned int | delay cut simplification by in-processing round | 2 |

cut.dont_cares | bool | integrate dont cares with cuts | true |

cut.force | bool | force redoing cut-enumeration until a fixed-point | false |

cut.lut | bool | extract luts from clauses for cut simplification | false |

cut.npn3 | bool | extract 3 input functions from clauses for cut simplification | false |

cut.redundancies | bool | integrate redundancy checking of cuts | true |

cut.xor | bool | extract xors from clauses for cut simplification | false |

ddfw.init_clause_weight | unsigned int | initial clause weight for DDFW local search | 8 |

ddfw.reinit_base | unsigned int | increment basis for geometric backoff scheme of re-initialization of weights | 10000 |

ddfw.restart_base | unsigned int | number of flips used a starting point for hessitant restart backoff | 100000 |

ddfw.threads | unsigned int | number of ddfw threads to run in parallel with sat solver | 0 |

ddfw.use_reward_pct | unsigned int | percentage to pick highest reward variable when it has reward 0 | 15 |

ddfw_search | bool | use ddfw local search instead of CDCL | false |

dimacs.core | bool | extract core from DIMACS benchmarks | false |

drat.activity | bool | dump variable activities | false |

drat.binary | bool | use Binary DRAT output format | false |

drat.check_sat | bool | build up internal trace, check satisfying model | false |

drat.check_unsat | bool | build up internal proof and check | false |

drat.disable | bool | override anything that enables DRAT | false |

drat.file | symbol | file to dump DRAT proofs | |

dyn_sub_res | bool | dynamic subsumption resolution for minimizing learned clauses | true |

elim_vars | bool | enable variable elimination using resolution during simplification | true |

elim_vars_bdd | bool | enable variable elimination using BDD recompilation during simplification | true |

elim_vars_bdd_delay | unsigned int | delay elimination of variables using BDDs until after simplification round | 3 |

enable_pre_simplify | bool | enable pre simplifications before the bounded search | false |

euf | bool | enable euf solver (this feature is preliminary and not ready for general consumption) | false |

force_cleanup | bool | force cleanup to remove tautologies and simplify clauses | false |

gc | symbol | garbage collection strategy: psm, glue, glue_psm, dyn_psm | glue_psm |

gc.burst | bool | perform eager garbage collection during initialization | false |

gc.defrag | bool | defragment clauses when garbage collecting | true |

gc.increment | unsigned int | increment to the garbage collection threshold | 500 |

gc.initial | unsigned int | learned clauses garbage collection frequency | 20000 |

gc.k | unsigned int | learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm) | 7 |

gc.small_lbd | unsigned int | learned clauses with small LBD are never deleted (only used in dyn_psm) | 3 |

inprocess.max | unsigned int | maximal number of inprocessing passes | 4294967295 |

inprocess.out | symbol | file to dump result of the first inprocessing step and exit | |

ite_extra | bool | (default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas | |

learned | bool | (default: false) collect also learned clauses. | |

local_search | bool | use local search instead of CDCL | false |

local_search_dbg_flips | bool | write debug information for number of flips | false |

local_search_mode | symbol | local search algorithm, either default wsat or qsat | wsat |

local_search_threads | unsigned int | number of local search threads to find satisfiable solution | 0 |

lookahead.cube.cutoff | symbol | cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat | depth |

lookahead.cube.depth | unsigned int | cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth. | 1 |

lookahead.cube.fraction | double | adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat | 0.4 |

lookahead.cube.freevars | double | cube free variable fraction. Used when lookahead.cube.cutoff is freevars | 0.8 |

lookahead.cube.psat.clause_base | double | clause base for PSAT cutoff | 2 |

lookahead.cube.psat.trigger | double | trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat | 5 |

lookahead.cube.psat.var_exp | double | free variable exponent for PSAT cutoff | 1 |

lookahead.delta_fraction | double | number between 0 and 1, the smaller the more literals are selected for double lookahead | 1.0 |

lookahead.double | bool | enable doubld lookahead | true |

lookahead.global_autarky | bool | prefer to branch on variables that occur in clauses that are reduced | false |

lookahead.preselect | bool | use pre-selection of subset of variables for branching | false |

lookahead.reward | symbol | select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu | march_cu |

lookahead.use_learned | bool | use learned clauses when selecting lookahead literal | false |

lookahead_scores | bool | extract lookahead scores. A utility that can only be used from the DIMACS front-end | false |

lookahead_simplify | bool | use lookahead solver during simplification | false |

lookahead_simplify.bca | bool | add learned binary clauses as part of lookahead simplification | true |

max_conflicts | unsigned int | maximum number of conflicts | 4294967295 |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

minimize_lemmas | bool | minimize learned clauses | true |

override_incremental | bool | override incremental safety gaps. Enable elimination of blocked clauses and variables even if solver is reused | false |

pb.lemma_format | symbol | generate either cardinality or pb lemmas | cardinality |

pb.min_arity | unsigned int | minimal arity to compile pb/cardinality constraints to CNF | 9 |

pb.resolve | symbol | resolution strategy for boolean algebra solver: cardinality, rounding | cardinality |

pb.solver | symbol | method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), binary_merge, segmented, solver (use native solver) | solver |

phase | symbol | phase selection strategy: always_false, always_true, basic_caching, random, caching, local_search | caching |

phase.sticky | bool | use sticky phase caching | true |

prob_search | bool | use probsat local search instead of CDCL | false |

probing | bool | apply failed literal detection during simplification | true |

probing_binary | bool | probe binary clauses | true |

probing_cache | bool | add binary literals as lemmas | true |

probing_cache_limit | unsigned int | cache binaries unless overall memory usage exceeds cache limit | 1024 |

probing_limit | unsigned int | limit to the number of probe calls | 5000000 |

propagate.prefetch | bool | prefetch watch lists for assigned literals | true |

random_freq | double | frequency of random case splits | 0.01 |

random_seed | unsigned int | random seed | 0 |

reorder.activity_scale | unsigned int | scaling factor for activity update | 100 |

reorder.base | unsigned int | number of conflicts per random reorder | 4294967295 |

reorder.itau | double | inverse temperature for softmax | 4.0 |

rephase.base | unsigned int | number of conflicts per rephase | 1000 |

resolution.cls_cutoff1 | unsigned int | limit1 - total number of problems clauses for the second cutoff of Boolean variable elimination | 100000000 |

resolution.cls_cutoff2 | unsigned int | limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination | 700000000 |

resolution.limit | unsigned int | approx. maximum number of literals visited during variable elimination | 500000000 |

resolution.lit_cutoff_range1 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 700 |

resolution.lit_cutoff_range2 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 400 |

resolution.lit_cutoff_range3 | unsigned int | second cutoff (total number of literals) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 300 |

resolution.occ_cutoff | unsigned int | first cutoff (on number of positive/negative occurrences) for Boolean variable elimination | 10 |

resolution.occ_cutoff_range1 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing less than res_cls_cutoff1 clauses | 8 |

resolution.occ_cutoff_range2 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff1 and less than res_cls_cutoff2 | 5 |

resolution.occ_cutoff_range3 | unsigned int | second cutoff (number of positive/negative occurrences) for Boolean variable elimination, for problems containing more than res_cls_cutoff2 | 3 |

restart | symbol | restart strategy: static, luby, ema or geometric | ema |

restart.emafastglue | double | ema alpha factor for fast moving average | 0.03 |

restart.emaslowglue | double | ema alpha factor for slow moving average | 1e-05 |

restart.factor | double | restart increment factor for geometric strategy | 1.5 |

restart.fast | bool | use fast restart approach only removing less active literals. | true |

restart.initial | unsigned int | initial restart (number of conflicts) | 2 |

restart.margin | double | margin between fast and slow restart factors. For ema | 1.1 |

restart.max | unsigned int | maximal number of restarts. | 4294967295 |

retain_blocked_clauses | bool | retain blocked clauses as lemmas | true |

scc | bool | eliminate Boolean variables by computing strongly connected components | true |

scc.tr | bool | apply transitive reduction, eliminate redundant binary clauses | true |

search.sat.conflicts | unsigned int | period for solving for sat (in number of conflicts) | 400 |

search.unsat.conflicts | unsigned int | period for solving for unsat (in number of conflicts) | 400 |

simplify.delay | unsigned int | set initial delay of simplification by a conflict count | 0 |

smt | bool | use the SAT solver based incremental SMT core | false |

smt.proof.check | bool | check proofs on the fly during SMT search | false |

subsumption | bool | eliminate subsumed clauses | true |

subsumption.limit | unsigned int | approx. maximum number of literals visited during subsumption (and subsumption resolution) | 100000000 |

threads | unsigned int | number of parallel threads to use | 1 |

variable_decay | unsigned int | multiplier (divided by 100) for the VSIDS activity increment | 110 |

## Tactic simplify

### Short Description:

The tactic performs algebraic simplifcations on formulas

### Long Description

The simplify tactic invokes z3's main rewriting engine. The rewriting engine contains support for theory specific simplifications. The set of simplifications invoked is open ended. Useful algebraic simplifications are added to the rewrite engine as they are discovered to be useful.

Note that the simplifier does not ensure that equivalent formulas are simplified to the same form. In other words it does not guarantee canonicity. This contrasts with BDD packages where BDDs constructed from two equivalent formulas are guaranteed to be equal.

### Example

The simplifier is also exposed as a stand-alone command. There are several options to control its behavior.

### Notes

- supports unsat cores, proof terms

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | 4294967295 | |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

ite_extra_rules | bool | true | |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | maximum amount of memory in megabytes | 4294967295 |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

rewrite_patterns | bool | rewrite patterns. | false |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

## Tactic solve-eqs

### Short Description

Solve for variables

### Long Description

The tactic eliminates variables that can be brought into solved form.
For example, the assertion `x = f(y + z)`

can be solved for `x`

, replacing `x`

everywhere by `f(x + y)`

. It depends on a set of theory specific equality solvers

Basic equations

- equations between uninterpreted constants and terms.
- equations written as
`(if p (= x t) (= x s))`

are solved as`(= x (if p t s))`

. - asserting
`p`

or`(not p)`

where`p`

is uninterpreted, causes`p`

to be replaced by`true`

(or`false`

).

Arithmetic equations

- It solves
`x mod k = s`

to`x = k * m' + s`

, where m'` is a fresh constant. - It finds variables with unit coefficients in integer linear equations.
- It solves for
`x * Y = Z`

under the side-condition`Y != 0`

as`x = Z/Y`

.

- It solves

It also allows solving for uninterpreted constants that only appear in a single disjuction. For example,
`(or (= x (+ 5 y)) (= y (+ u z)))`

allows solving for `x`

.

### Example

`(declare-const x Int)`

(declare-const y Int)

(declare-const z Int)

(declare-const u Int)

(assert (or (and (= x (+ 5 y)) (> u z)) (= y (+ u z))))

(apply solve-eqs)

It produces the goal

`(goal`

(or (not (<= u z)) (= y (+ u z)))

:precision precise :depth 1)

where `x`

was solved as `(+ 5 y)`

.

### Notes

- supports unsat cores
- does not support fine-grained proofs

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

context_solve | bool | solve equalities under disjunctions. | false |

eliminate_mod | bool | eliminate modulus from equations | true |

ite_solver | bool | use if-then-else solver. | true |

solve_eqs_max_occs | unsigned int | (default: infty) maximum number of occurrences for considering a variable for gaussian eliminations. | 4294967295 |

theory_solver | bool | theory solvers. | true |

## Tactic split-clause

### Short Description

Tactic that creates a subgoal for each literal in a clause `(l_1 or ... or l_n)`

.
The tactic fails if the main goal does not contain any clause.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

split_largest_clause | bool | (default: false) split the largest clause in the goal. |

## Tactic symmetry-reduce

### Short Description

Apply symmetry reduction

### Long Description

The tactic applies symmetry reduction for uninterpreted functions and equalities. It applies a straight-forward adaption of an algorithm proposed for veriT.

## Tactic tseitin-cnf

### Short Description

Convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored).

### Long Description

Puts an assertion set in CNF. Auxiliary variables are used to avoid blowup.

Features:

Efficient encoding is used for commonly used patterns such as:

`(iff a (iff b c))`

`(or (not (or a b)) (not (or a c)) (not (or b c)))`

Efficient encoding is used for chains of if-then-elses

Distributivity is applied to non-shared nodes if the blowup is acceptable.

The features above can be disabled/enabled using parameters.

The assertion-set is only modified if the resultant set of clauses is "acceptable".

Notes:

Term-if-then-else expressions are not handled by this strategy. This kind of expression should be processed by other strategies.

Quantifiers are treated as "theory" atoms. They are viewed as propositional variables by this strategy.

The assertion set may contain free variables.

This strategy assumes the assertion_set_rewriter was used before invoking it. In particular, it is more effective when "and" operators were eliminated.

### Example

### Parameters

Parameter | Type | Description | Default |
---|---|---|---|

algebraic_number_evaluator | bool | simplify/evaluate expressions containing (algebraic) irrational numbers. | true |

arith_ineq_lhs | bool | rewrite inequalities so that right-hand-side is a constant. | false |

arith_lhs | bool | all monomials are moved to the left-hand-side, and the right-hand-side is just a constant. | false |

bit2bool | bool | try to convert bit-vector terms of size 1 into Boolean terms | true |

blast_distinct | bool | expand a distinct predicate into a quadratic number of disequalities | false |

blast_distinct_threshold | unsigned int | 4294967295 | |

blast_eq_value | bool | blast (some) Bit-vector equalities into bits | false |

blast_select_store | bool | eagerly replace all (select (store ..) ..) term by an if-then-else term | false |

bv_extract_prop | bool | attempt to partially propagate extraction inwards | false |

bv_ineq_consistency_test_max | unsigned int | max size of conjunctions on which to perform consistency test based on inequalities on bitvectors. | 0 |

bv_ite2id | bool | rewrite ite that can be simplified to identity | false |

bv_le2extract | bool | disassemble bvule to extract | true |

bv_le_extra | bool | additional bu_(u/s)le simplifications | false |

bv_not_simpl | bool | apply simplifications for bvnot | false |

bv_sort_ac | bool | sort the arguments of all AC operators | false |

cache_all | bool | cache all intermediate results. | false |

common_patterns | bool | minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns | true |

distributivity | bool | minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas | true |

distributivity_blowup | unsigned int | maximum overhead for applying distributivity during CNF encoding | 32 |

elim_and | bool | conjunctions are rewritten using negation and disjunctions | false |

elim_ite | bool | eliminate ite in favor of and/or | true |

elim_rem | bool | replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))). | false |

elim_sign_ext | bool | expand sign-ext operator using concat and extract | true |

elim_to_real | bool | eliminate to_real from arithmetic predicates that contain only integers. | false |

eq2ineq | bool | expand equalities into two inequalities | false |

expand_nested_stores | bool | replace nested stores by a lambda expression | false |

expand_power | bool | expand (^ t k) into (* t ... t) if 1 < k <= max_degree. | false |

expand_select_ite | bool | expand select over ite expressions | false |

expand_select_store | bool | conservatively replace a (select (store ...) ...) term by an if-then-else term | false |

expand_store_eq | bool | reduce (store ...) = (store ...) with a common base into selects | false |

expand_tan | bool | replace (tan x) with (/ (sin x) (cos x)). | false |

flat | bool | create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor | true |

flat_and_or | bool | create nary applications for and,or | true |

gcd_rounding | bool | use gcd rounding on integer arithmetic atoms. | false |

hi_div0 | bool | use the 'hardware interpretation' for division by zero (for bit-vector terms) | true |

hoist_ite | bool | hoist shared summands under ite expressions | false |

hoist_mul | bool | hoist multiplication over summation to minimize number of multiplications | false |

ignore_patterns_on_ground_qbody | bool | ignores patterns on quantifiers that don't mention their bound variables. | true |

ite_chaing | bool | minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains | true |

ite_extra | bool | add redundant clauses (that improve unit propagation) when encoding if-then-else formulas | true |

ite_extra_rules | bool | true | |

local_ctx | bool | perform local (i.e., cheap) context simplifications | false |

local_ctx_limit | unsigned int | limit for applying local context simplifier | 4294967295 |

max_degree | unsigned int | max degree of algebraic numbers (and power operators) processed by simplifier. | 64 |

max_memory | unsigned int | (default: infty) maximum amount of memory in megabytes. | 4294967295 |

max_steps | unsigned int | maximum number of steps | 4294967295 |

mul2concat | bool | replace multiplication by a power of two into a concatenation | false |

mul_to_power | bool | collpase (* t ... t) into (^ t k), it is ignored if expand_power is true. | false |

pull_cheap_ite | bool | pull if-then-else terms when cheap. | false |

push_ite_arith | bool | push if-then-else over arithmetic terms. | false |

push_ite_bv | bool | push if-then-else over bit-vector terms. | false |

push_to_real | bool | distribute to_real over * and +. | true |

rewrite_patterns | bool | rewrite patterns. | false |

som | bool | put polynomials in sum-of-monomials form | false |

som_blowup | unsigned int | maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form | 10 |

sort_store | bool | sort nested stores when the indices are known to be different | false |

sort_sums | bool | sort the arguments of + application. | false |

split_concat_eq | bool | split equalities of the form (= (concat t1 t2) t3) | false |

## Tactic unit-subsume-simplify

### Short Description

implify goal using subsumption based on unit propagation

### Long Description

Background: PDR generates several clauses that subsume each-other. Simplify a goal assuming it is a conjunction of clauses. Subsumed clauses are simplified by using unit-propagation It uses the default SMT solver.