Simplifiers

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.

(help-simplifier)

To create a specialized solver use the command set-simplifier.

(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 then (or and-then) similar to tactics. You can also set parameters on simplifiers using the same syntax as for tactics.