Frédéric Bour
4779f41ee4

2 years ago  

attic  2 years ago  
lib  2 years ago  
.gitignore  3 years ago  
Makefile  3 years ago  
README.md  3 years ago  
duneproject  3 years ago  
ztl.opam  3 years ago 
README.md
Z3 Type Layer
Z3 is a powerful tool for working with firstorder logic however the OCaml API is quite hard to work with: it is mostly untyped, all terms are represented by Z3.Expr.expr
, even though they might have very different types in the logic.
Ztl
implements a strongly typed layer on top of Z3 ML Api. The type system of Z3 logic as well as the syntax of sorts and terms are encoded quite faithfully in OCaml type system.
You might also be interested in Z3overlay, another typed interface to Z3.
Limitations
As of today the following Z3 sorts are supported: boolean, integers, reals, arrays, bitvectors and sets.
Only simple satisfiability checking is implemented. Advanced operations such as simplification, optimization and model extraction might be implemented in the future.
Installation
Assuming you have a working opam/ocaml installation:
opam install ztl
Ztl Guide
Here is a translation of a few examples from the Z3 Guide. Follow the explanation from the guide and use the code examples in an OCaml toplevel.
To setup the toplevel, after installing ztl:
$ utop
# #require "ztl";;
# open Ztl;;
Basic Commands
let a = Symbol.const Integer
(* val a : (unit, integer) symbol = <abstr> *)
let f = Symbol.fresh [Integer; Boolean] Integer
(* val f : (integer > boolean > unit, integer) symbol = <abstr> *)
let p1 = Numeral.gt (Term.const a) (Integer.of_int 10)
(* val p1 : boolean term = <abstr> *)
let p2 =
Numeral.lt
(Term.apply f [Term.const a; Boolean.of_bool true])
(Integer.of_int 100)
(* val p2 : boolean term = <abstr> *)
let sat = Context.check [p1; p2]
(* val sat : [ `Impossible  `Possible  `Unknown ] = `Possible *)
 Z3 functions are declared using
Symbol.fresh domain codomain
.  A constant is a function that takes no argument,
Symbol.const sort == Symbol.fresh [] sort
.  Z3 Sorts are reflected in OCaml values and OCaml types:
(integer > boolean > unit, integer) symbol
is the type of a function to integers that is parameterized by an integer and a boolean(unit, integer) symbol
is the symbol of an integer constant
'a term
is the type of a Z3 term of sort'a
. The encoding of Z3 sorts in OCaml type system guarantees that only wellsorted terms can be built. In Z3 native language, assertions are accumulated as a sideeffect and satisfiability is checked with the
(checksat)
command. InZtl
, terms are built, and checked for satisfiability in a context without implicit state. The API strives to be pure.
A few syntactic sugars are available in the Infix
module:
open Infix
let a = Symbol.const Integer
(* val a : (unit, integer) symbol = <abstr> *)
let f = Symbol.fresh [Integer; Boolean] Integer
(* val f : (integer > boolean > unit, integer) symbol = <abstr> *)
let p1 = (a%[]) >? (Integer.of_int 10)
(* val p1 : boolean term = <abstr> *)
let p2 =
(f%[a%[]; Boolean.of_bool true]) <? (Integer.of_int 100)
(* val p2 : boolean term = <abstr> *)
let sat = Context.check [p1; p2]
(* val sat : [ `Impossible  `Possible  `Unknown ] = `Possible *)
 operators lifted to the logic generally have a
?
appended: arithmetic:
+?
,?
,*?
,/?
, ...  comparison:
<>?
,==?
, ...  ordering of numbers:
<?
,>?
, ...  boolean:
?
,&&?
,<=>?
, ...  implication is
@==>
to get the right associativity (OCaml precedence and associativity)
 arithmetic:
 symbol application is done with
%
: functional are applied with
f%[t1; t2]
 constants are applied with
a%[]
 functional are applied with
TODO: lighter syntax for application?!
TODO: it is not possible to retrieve the model yet from Ztl
Propositional Logic
let p = Symbol.const Boolean
let q = Symbol.const Boolean
let r = Symbol.const Boolean
(* val p : (unit, boolean) symbol = <abstr>
val q : (unit, boolean) symbol = <abstr>
val r : (unit, boolean) symbol = <abstr> *)
let conjecture =
((p%[] @==> q%[]) &&? (q%[] @==> r%[]))
@==>
p%[] @==> r%[];;
(* val conjecture : boolean term = <abstr> *)
let sat = Context.check [Boolean.not conjecture]
(* val sat : [ `Impossible  `Possible  `Unknown ] = `Impossible *)
Satisfiability and Validity
let a = Symbol.const Boolean
let b = Symbol.const Boolean
let not_ = Boolean.not
let demorgan = (a%[] &&? b%[]) ==? not_ (not_ (a%[]) ? not_ (b%[]))
let sat = Context.check [not_ demorgan]
(* val sat : [ `Impossible  `Possible  `Unknown ] = `Impossible *)