Z3 theories

Basics

There is a single basic sort, bool, which has op-code 0. The basic operators are, listed with their codes in the table below.

Op-code	Mnmonics	Description
0	true	the constant true
1	false	the constant false
2	=	equality
3	distinct	distincinctness
4	ite	if-then-else
5	and	n-ary conjunction
6	or	n-ary disjunction
7	iff	bi-impliciation
8	xor	exclusive or
9	not	negation
10	implies	implication

Arithmetic

Built-in operators

Arithmetical expression can be built from reals or integers. The arithmetical sorts are listed below and the supported operations are listed in the table thereafter.

Op-code	Mnmonics	Description
0	real	sort of reals
1	int	sort of integers

Op-code	Mnmonics	Description
0	<=	less-than or equal
1	>=	greater-than or equal
2	<	less-than
3	>	greater-than
4	+	n-ary addition
5	-	binary minus
6	~	unary minus
7	*	n-ary multiplication
8	/	rational division
9	div	integer division
10	rem	integer remainder
11	mod	integer modulus

Bit-vectors

To indicate the bit-vector length one adds a numeral parameter with the number of bits the bit-vector holds. For instance, a declaration of the form:

  Type $1 bv [ 32 ] 

declares a 32-bit bit-vector type.

Op-code	Mnmonics	Parameters	Description
0	bit1		constant comprising of a single bit set to 1
1	bit0		constant comprising of a single bit set to 0.
2	bvneg		Unary subtraction.
3	bvadd		addition.
4	bvsub		subtraction.
5	bvmul		multiplication.
6	bvsdiv		signed division.
7	bvudiv		unsigned division. The operands are treated as unsigned numbers.
8	bvsrem		signed remainder.
9	bvurem		unsigned remainder.
10	bvsmod		signed modulus.
11	bvule		unsigned <=.
12	bvsle		signed <=.
13	bvuge		unsigned >=.
14	bvsge		signed >=.
15	bvult		unsigned <.
16	bvslt		signed <.
17	bvugt		unsigned >.
18	bvsgt		signed >.
19	bvand		n-ary (associative/commutative) bit-wise and.
20	bvor		n-ary (associative/commutative) bit-wise or.
21	bvnot		bit-wise not.
22	bvxor		n-ary bit-wise xor.
23	bvnand		bit-wise nand.
24	bvnor		bit-wise nor.
25	bvxnor		bit-wise exclusive nor.
26	concat		bit-vector concatentaion.
27	sign	n	n-bit sign extension.
28	zero	n	n-bit zero extension.
29	extract	hi:low	hi-low bit-extraction.
30	repeat	n	repeat $n$ times.
31	bvredor		or-reduction.
32	bvredand		and-reducdtion.
33	bvcomp		bit-vector comparison.
34	bvshl		shift-left.
35	bvlshr		logical shift-right.
36	bvrshr		arithmetical shift-right.
37	bvrotate	n	n-bit left rotation.
38	bvrotate	n	n-bit right rotation.

Arrays

Built-in operators

There is a single built-in sort constructor for arrays with code 0. It is followed by a sequence of parameters indicating the domain sorts and the range of the array.

Op-code	Mnmonics	Description
0	store	array store
1	select	array select

In the low-level input format, array types are accompanied by a sequence of identifiers corresponding to the domain and range of the array the operations operate upon. In more detail, the contract is that the supplied parameters to the type declaration of an array are of the form:

• parameter_0 - 1'st dimension
• parameter_{n-1} - n'th dimension
• parameter_n - range

The constant array function symbol const needs a parameter in order to infer the types of the indices of the constant array. We pass the array type as the parameter to const. The other array operations do not need parameters.

We summarize the arities and semantics of the operators:

• store -

  Updates an array at a given index with a value: store(A, i0, ... i_{n-1}, v) has the same contents as A, except on index i0, ... , i_{n-1}, where the value is v.

• select -

  Selects the value from an array: select(A, i0, ... , i_{n-}) selects the value stored at index i0, ... , i_{n-1}.