Z3学习——Z3guide
Introduction
What is Z3
Z3 is a stateofart theorem prover from Microsoft Research.
Check sat of logical formulas. Match for software analysis and verification tools.
Low level tool.
Basic Commands
Input format (syntax) is an extension of one defined by the SMTLIB 2.0 standard.
(help)
: print the help(echo <string>)
: display the given string(declareconst <symbol> <sort>)
: declare a constant of a given type (aka sort)(declarefun <symbol> (<sort>*) <sort>)
: declare a function
The command assert
adds a formula into the Z3 internal stack. checksat
lets us know if there is an interpretation for all the declared constants and functions that makes all asserted formulas in Z3 stack true.
(assert <term>)
: assert term(checksat <booleanconstants>*)
: check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true.
When checksat
returns sat(satisfied), the command getmodel
can be used to retrieve an interpretation. The interpretation is provided using definitions.
(getmodel)
: retrieve model for the last checksat command(getproof)
: retrieve proof
E.g.
1 

Output.
1 

Using Scopes
push
and pop
commands are used for the purpose to share several definitions and assertions. The push and pop commands can optionally receive a numeral argument as specifed by the SMT 2 language.
(push <number>?)
: push 1 (or) scopes. (pop <number>?)
: pop 1 (or) scopes.
E.g. (TODO: need to test it).
1 

Configuration
The command setoption is used to configure Z3.
But I haven’t found the related OCaml API to these configurations. (TODO)
Additional commands
(display) <term>)
: display the given term(aka expression).(simplify <term> (<keyword> <value>)*)
: simplify the expr
From the [z3.mli] we can find the definition of simplify
in OCaml.
1 

create a boolean sort
(definesort [symbol] ([symbol]+) [sort])
: define an abbreviation for a sort expression
Maybe map to mk_sort
in [z3.mli].
Propositional Logic
So here we meet propositional logic in z3.
Satisfiability and Validity
We need to emphasize the differences between satisfiability and validity.
 Satifiability is about finding a solution to a set of constraints.
 Validity is about finding a proof of a statement.
In Coq, we always intros to get certain Hypotheses though when we try to prove a proposition with implication , we assumes the Hypotheses are right. So we often want to prove a theorm which notes a proposition is validity.
Back to Z3, consider a formula F with some uninterpreted constants, say a and b. We can ask whether F is valid, that is whether it is always true for any combination of values for a and b. If F is always true, then not F is always false, and then not F will not have any satisfying assignment; that is, not F is unsatisfiable. That is, F is valid precisely when not F is not satisfiable (is unsatisfiable). Alternately, F is satisfiable if and only if not F is not valid (is invalid). Z3 finds satisfying assignments (or report that there are none).
E.g. check the deMorgan’s law is valid.
1 

E.g. check the excluded middle law
1 

Verification with Python API (z3py)
1 

Uninterpreted functions and constants
Constants are just functions that take no arguments. So everything is really just a function.
1 

in Python API
1 

The notation of A!val!0
means $A_{val_0}$
Arithmetic
Builtin support for integer and real constants. These two types (sorts) represent the mathematical integers and reals.
Not convert automatically integers into reals and viceversa.
Nonlinear arithmetic
Nonlinear arithmetic is undecidable. Note that, this does not prevent Z3 from returning an answer for many nonlinear problems. The real limit is that there will always be a nonlinear integer arithmetic formula that it will fail produce an answer.
1 

Division
Support division
E.g. in Python API
1 

Bitvectors
(_ bv20 8)
: a bitvector of size 8 that representes the numeral 20. Desplay as#x14
(_ bv10 32)
: a bitvector of size 32 that representes the numeral 10. Desplay as#x0000000a
(a single num in hexadecimal format represent size 4).
By default, Z3 display bitvectors in hexadecimal format if the bitvector size is a multiple of 4, and in binary otherwise.
In Python API the function BitVecVal(10,32)
creates a bitvector of size 32 containing the value 10.
1 

We get the True.
Bitvector Arithmetic and Bitwise Operations
1 

and the print
1 

Prove a bitwise version of deMorgan’s law in Python API.
1 

A common trick
There is a fast way to check that fixed size numbers are powers of two.
A bitvector x is a power of two or zero if and only if x & (x  1) is zero.
1 

with Python API
1 

Arrays
Select and Store
exercise in Python API
1 

and the output
1 

We can get an array which maps all indices to fixed value using the const
construct in Z3. E.g. (as const (Array T1 T2))
Map functions on arrays using map
keyword.
Datatypes
Records
A record is specified as a datatype with a single constructor and as many arguments as record elements.
1 

with Python API
1 

Scalars
A scalar sort is a finate domain sort.
1 

The elements of the finite domain are enumerated as distinct constans.
with Python API
1 

Recursive datatypes
A recursive datatype declaration includes itself directly (or indirectly) as a component.
like define lst with Python API
1 

Z3 will not prove inductive facts. The ground decision procedures for recursive datatypes don’t lift to establing inductive facts. Z3 does not contain methods for producing proofs by induction. E.g. therom on all natural numbers.
Quantifiers
Apart from quantifierfree theories (Here Z3 is a decision procedure), Z3 also accepts and can work with formulas that use quantifiers. It is no longer a decision procedure for such formulas in general (and for good reasons, as there can be no decision procedure for firstorder logic).
Several approaches to handle quantifiers: patterbased quantifier(effective, inherently incomplete), saturation theorem proving.
Modeling with Quantifiers
本博客所有文章除特别声明外，均采用 CC BYSA 4.0 协议 ，转载请注明出处！