Frédéric Bour 7765ede80c | 2 months ago | |
---|---|---|
attic | 9 months ago | |
lib | 2 months ago | |
.gitignore | 9 months ago | |
Makefile | 9 months ago | |
README.md | 9 months ago | |
dune-project | 6 months ago | |
ztl.opam | 6 months ago |
Z3 is a powerful tool for working with first-order 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.
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.
Assuming you have a working opam/ocaml installation:
opam install ztl
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;;
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 *)
Symbol.fresh domain codomain
.Symbol.const sort == Symbol.fresh [] sort
.(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 well-sorted terms can be built.(check-sat)
command.
In Ztl
, 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 *)
?
appended:
+?
, -?
, *?
, /?
, ...<>?
, ==?
, ...<?
, >?
, ...||?
, &&?
, <=>?
, ... @==>
to get the right associativity (OCaml precedence and associativity)%
:
f%[t1; t2]
a%[]
TODO: lighter syntax for application?!
TODO: it is not possible to retrieve the model yet from Ztl
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 *)
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 *)