# Basic Commands

The Z3 input format is an extension of the one defined by the SMT-LIB format.

A Z3 script is a sequence of commands. As an extension of the SMT-LIB format, this means that Z3 is not technically a programming language in the same way that Java, Python, or Javascript are; there are no loops or variables as they are commonly understood, for example. The `help`

command displays a list of all available commands. The command `echo`

displays a message.

Internally, Z3 maintains a stack of user provided formulas and declarations. We say these are the assertions provided by the user. The command `declare-const`

declares a constant of a given type (aka sort). The command `declare-fun`

declares a function. In the following example, we declare a function `f`

that receives an integer and a Boolean and returns an integer.

The `assert`

command adds a formula to the Z3 internal stack. We say that the set of formulas in the Z3 stack is *satisfiable* if there is an interpretation (for the user declared constants and functions) that makes all asserted formulas true.

The first asserted formula states that the constant `a`

must be less than 10. The second one states that the function `f`

applied to `a`

and `true`

must return a value less than 100.
The `check-sat`

command determines whether the current formulas on the Z3 stack are satisfiable or not. If the formulas are satisfiable, Z3 returns `sat`

. If they are not satisfiable, Z3 returns `unsat`

.
Z3 may also return `unknown`

if it can't determine whether a formula is satisfiable or not.

When the `check-sat`

command returns `sat`

, the `get-model`

command can be used to retrieve an interpretation that makes all formulas on the Z3 internal stack true.

The interpretation is provided using definitions. For example, the definition

(define-fun a () Int [val])

states that the value of a in the model is [val]. The definition

(define-fun f ((x!1 Int) (x!2 Bool)) Int ... )

is very similar to a function definition used in programming languages. In this example, x!1 and x!2 are the arguments of the function interpretation created by Z3. For this simple example, the definition of f is based on ite's (aka if-then-elses or conditional expressions). For example, the expression

(ite (and (= x!1 11) (= x!2 false)) 21 0)

evaluates to (returns) 21 when x!1 is equal to 11, and x!2 is equal to false. Otherwise, it returns 0.

## Using Scopes

In some applications, we want to explore several similar problems that share several definitions and assertions.
We can use the commands `push`

and `pop`

for doing that. Z3 maintains a global stack of declarations and assertions.
The `push`

command creates a new scope by saving the current stack size.
The `pop`

command removes any assertion or declaration performed between it and the matching `push`

.
The `check-sat`

and `get-assertions`

commands always operate on the content of the global stack.

In the following example, the command `(assert p)`

gives an error because `pop`

removed the declaration for p.
If the last `pop`

command is removed, then the error is corrected.

The `push`

and `pop`

commands can optionally receive a numeral argument
indicating how many stack levels to push or pop,
as specified by the SMT 2 language.

## Configuration

The `set-option`

command is used to configure Z3.
Z3 has several options to control its behavior.
Some of these options (e.g., produce-proofs) can only be set before any declaration or assertion. We use the `reset`

command to erase all assertions and declarations. After `reset`

, all configuration options can be set.

The `print-success true`

option is particularly useful when Z3 is being controlled by another application using pipes. In this mode, commands that otherwise would not print any output, will print `success`

.

Here is a summary of all parameters

### Additional commands

The command `(display t)`

just applies the Z3 pretty printer to the given expression. The command `(simplify t)`

displays a possibly simpler expression equivalent to t. This command accepts many different options, and `(help simplify)`

will display all available options.

The define-sort command defines a new sort symbol that is an abbreviation for a sort expression. The new sort symbol can be parameterized, in which case the names of the parameters are specified in the command and the sort expression uses the sort parameters. The form of the command is this

(define-sort [symbol] ([symbol]+) [sort])

The following example defines several abbreviations for sort expressions: