# describe_tactics() gives a list of all z3 tactics

ackermannize_bv : A tactic for performing full Ackermannization on bv instances.

subpaving : tactic for testing subpaving module.

horn : apply tactic for horn clauses.

horn-simplify : simplify horn clauses.

nlsat : (try to) solve goal using a nonlinear arithmetic solver.

qfnra-nlsat : builtin strategy for solving QF_NRA problems using only nlsat.

nlqsat : apply a NL-QSAT solver.

qe-light : apply light-weight quantifier elimination.

qe-sat : check satisfiability of quantified formulas using quantifier elimination.

qe : apply quantifier elimination.

qsat : apply a QSAT solver.

qe2 : apply a QSAT based quantifier elimination.

qe_rec : apply a QSAT based quantifier elimination recursively.

psat : (try to) solve goal using a parallel SAT solver.

sat : (try to) solve goal using a SAT solver.

sat-preprocess : Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution).

ctx-solver-simplify : apply solver-based contextual simplification rules.

smt : apply a SAT based SMT solver.

psmt : builtin strategy for SMT tactic in parallel.

unit-subsume-simplify : unit subsumption simplification.

aig : simplify Boolean structure using AIGs.

add-bounds : add bounds to unbounded variables (under approximation).

card2bv : convert pseudo-boolean constraints to bit-vectors.

degree-shift : try to reduce degree of polynomials (remark: :mul2power simplification is automatically applied).

diff-neq : specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numeral, and all constants are bounded.

eq2bv : convert integer variables used as finite domain elements to bit-vectors.

factor : polynomial factorization.

fix-dl-var : if goal is in the difference logic fragment, then fix the variable with the most number of occurrences at 0.

fm : eliminate variables using fourier-motzkin elimination.

lia2card : introduce cardinality constraints from 0-1 integer.

lia2pb : convert bounded integer variables into a sequence of 0-1 variables.

nla2bv : convert a nonlinear arithmetic problem into a bit-vector problem, in most cases the resultant goal is an under approximation and is useul for finding models.

normalize-bounds : replace a variable x with lower bound k <= x with x' = x - k.

pb2bv : convert pseudo-boolean constraints to bit-vectors.

propagate-ineqs : propagate ineqs/bounds, remove subsumed inequalities.

purify-arith : eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.

recover-01 : recover 0-1 variables hidden as Boolean variables.

bit-blast : reduce bit-vector expressions into SAT.

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

bv_bound_chk : attempts to detect inconsistencies of bounds on bv expressions.

propagate-bv-bounds : propagate bit-vector bounds by simplifying implied or contradictory bounds.

propagate-bv-bounds-new : propagate bit-vector bounds by simplifying implied or contradictory bounds.

reduce-bv-size : try to reduce bit-vector sizes using inequalities.

bvarray2uf : Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.

dt2bv : eliminate finite domain data-types. Replace by bit-vectors.

elim-small-bv : eliminate small, quantified bit-vectors by expansion.

max-bv-sharing : use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers.

blast-term-ite : blast term if-then-else by hoisting them.

cofactor-term-ite : eliminate term if-the-else using cofactors.

collect-statistics : Collects various statistics.

ctx-simplify : apply contextual simplification rules.

der : destructive equality resolution.

distribute-forall : distribute forall over conjunctions.

dom-simplify : apply dominator simplification rules.

elim-term-ite : eliminate term if-then-else by adding fresh auxiliary declarations.

elim-uncnstr : eliminate application containing unconstrained variables.

injectivity : Identifies and applies injectivity axioms.

snf : put goal in skolem normal form.

nnf : put goal in negation normal form.

occf : put goal in one constraint per clause normal form (notes: fails if proof generation is enabled; only clauses are considered).

pb-preprocess : pre-process pseudo-Boolean constraints a la Davis Putnam.

propagate-values : propagate constants.

reduce-args : reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.

reduce-invertible : reduce invertible variable occurrences.

simplify : apply simplification rules.

elim-and : convert (and a b) into (not (or (not a) (not b))).

solve-eqs : eliminate variables by solving equations.

special-relations : detect and replace by special relations.

split-clause : split a clause in many subgoals.

symmetry-reduce : apply symmetry reduction.

tseitin-cnf : convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored).

tseitin-cnf-core : convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored). This tactic does not apply required simplifications to the input goal like the tseitin-cnf tactic.

qffd : builtin strategy for solving QF_FD problems.

pqffd : builtin strategy for solving QF_FD problems in parallel.

smtfd : builtin strategy for solving SMT problems by reduction to FD.

fpa2bv : convert floating point numbers to bit-vectors.

qffp : (try to) solve goal using the tactic for QF_FP.

qffpbv : (try to) solve goal using the tactic for QF_FPBV (floats+bit-vectors).

qffplra : (try to) solve goal using the tactic for QF_FPLRA.

default : default strategy used when no logic is specified.

sine-filter : eliminate premises using Sine Qua Non

qfbv-sls : (try to) solve using stochastic local search for QF_BV.

nra : builtin strategy for solving NRA problems.

qfaufbv : builtin strategy for solving QF_AUFBV problems.

qfauflia : builtin strategy for solving QF_AUFLIA problems.

qfbv : builtin strategy for solving QF_BV problems.

qfidl : builtin strategy for solving QF_IDL problems.

qflia : builtin strategy for solving QF_LIA problems.

qflra : builtin strategy for solving QF_LRA problems.

qfnia : builtin strategy for solving QF_NIA problems.

qfnra : builtin strategy for solving QF_NRA problems.

qfuf : builtin strategy for solving QF_UF problems.

qfufbv : builtin strategy for solving QF_UFBV problems.

qfufbv_ackr : A tactic for solving QF_UFBV based on Ackermannization.

ufnia : builtin strategy for solving UFNIA problems.

uflra : builtin strategy for solving UFLRA problems.

auflia : builtin strategy for solving AUFLIA problems.

auflira : builtin strategy for solving AUFLIRA problems.

aufnira : builtin strategy for solving AUFNIRA problems.

lra : builtin strategy for solving LRA problems.

lia : builtin strategy for solving LIA problems.

lira : builtin strategy for solving LIRA problems.

skip : do nothing tactic.

fail : always fail tactic.

fail-if-undecided : fail if goal is undecided.

macro-finder : Identifies and applies macros.

quasi-macros : Identifies and applies quasi-macros.

ufbv-rewriter : Applies UFBV-specific rewriting rules, mainly demodulation.

bv : builtin strategy for solving BV problems (with quantifiers).

ufbv : builtin strategy for solving UFBV problems (with quantifiers).