A subset of tactics can be applied in incremental mode as pre-processing simplification to solvers. The SMTLIB interface provides a way to specialize solvers using a sequence of pre-processing simplification steps.
You can list the set of available simplifiers with information about their parameters using the command.
To create a specialized solver use the command
(set-simplifier (then simplify solve-eqs elim-unconstrained propagate-values simplify qe-light simplify qe-light))
Simplifiers are a special case of tactics. Not all tactics can be used as a simplifier.
The tactic language for composing simplifiers is also more rudimentary. The only operations are
sequential composition and parameter adjustment.
You can sequence simplifiers using
and-then) similar to tactics. You can also set parameters on
simplifiers using the same syntax as for tactics.