假设我想检查公式x + y = z(x,y,z整数)是否可满足。使用Z3,我可以输入类似以下内容:
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= z (+ x y)))
(check-sat)
我可以等效地使用Ocaml api并编写以下代码:
let ctx=Z3.mk_context [("model", "true"); ("proof", "false")] in
let v1=(Z3.Arithmetic.Integer.mk_const_s ctx "x") in
let v2=(Z3.Arithmetic.Integer.mk_const_s ctx "y") in
let res=(Z3.Arithmetic.Integer.mk_const_s ctx "z") in
let sum=Z3.Arithmetic.mk_add ctx [ v1 ; v2] in
let phi=Z3.Boolean.mk_eq ctx sum res in
let solver = (Z3.Solver.mk_solver ctx None) in
let _= Z3.Solver.add solver [phi] in
let is_sat=Z3.Solver.check solver [] in
match is_sat with
| UNSATISFIABLE -> Printf.printf "unsat";
| SATISFIABLE -> Printf.printf "sat";
| UNKNOWN -> Printf.printf "unknown";
我想使用z3的ocaml api来检查以下阶乘实现,以便获得x的值(如果存在)。
(declare-fun x () Int)
(define-fun-rec f ((x Int)) Int
(ite (> x 1)
(* (f (- x 1))
x)
1))
(assert (= x (f 10)))
(check-sat)
(get-model)
不幸的是,我找不到使用z3的ml api进行递归定义的示例。
它运行我的计算机
let ctx=Z3.mk_context [("model", "true"); ("proof", "false")] in
let v1=(Z3.Arithmetic.Integer.mk_const_s ctx "x") in
let v2=(Z3.Arithmetic.Integer.mk_const_s ctx "y") in
let res=(Z3.Arithmetic.Integer.mk_const_s ctx "z") in
let sum=Z3.Arithmetic.mk_add ctx [ v1 ; v2] in
let phi=Z3.Boolean.mk_eq ctx sum res in
let solver = (Z3.Solver.mk_solver ctx None) in
let _= Z3.Solver.add solver [phi] in
let is_sat=Z3.Solver.check solver [] in
match is_sat with
| UNSATISFIABLE -> Printf.printf "unsat";
| SATISFIABLE -> let m = (get_model solver) in
match m with
| None -> raise (TestFailedException "")
| Some (m) ->
Printf.printf "Model: \n%s\n" (Model.to_string m);
********output*********
Model:
(define-fun x () Int
0)
(define-fun y () Int
0)
(define-fun z () Int
0)