小编sh0*_*h0t的帖子

假设我想检查公式 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 …