# Goals

Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic reasoning steps are represented as functions known as *tactics*, and tactics are composed using combinators known as *tacticals*. Tactics process sets of formulas called Goals.

When a tactic is applied to some goal G, four different outcomes are possible. In SMT 2.0, the goal is the conjunction of all assertions. The tactic succeeds in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, we face the problem of model conversion. A model converter constructs a model for G using a model for some subgoal Gi.

In the following example, we use the command `apply`

to execute a tactic composed of two built-in tactics: `simplify`

and `solve-eqs`

. The tactic `simplify`

applies transformations equivalent to the ones found in the `simplify`

command.
The tactic `solve-eqs`

eliminates variables using Gaussian elimination.
Actually, `solve-eqs`

is not restricted linear arithmetic, but can also eliminate arbitrary variables. The combinator `then`

applies `simplify`

to the input goal and `solve-eqs`

to each subgoal produced by `simplify`

. In this example, only one subgoal is produced.

In the example above, variable x is eliminated, and is not present in the resultant goal.

In Z3, a *clause* is any constraint of the form `(or f_1 ... f_n)`

.
The tactic `split-clause`

will select a clause `(or f_1 ... f_n)`

in the input goal, and split it into n subgoals, one for each subformula `f_i`

.