代码之家 › 专栏 › 技术社区 › CXB

ocaml上的Z3绑定

oasis sat-solvers opam z3 ocaml

CXB · 技术社区 · 6 年前

我目前正在使用ocaml4.06.0,并尝试使用z3sat解算器。我正在使用opam的oasis来编译文件(它正在成功地构建所有东西)。但是,当我运行生成的本机代码时,出现以下错误: error while loading shared libraries: libz3.so . 我尝试重新安装z3软件包,但错误仍然存在。有谁能帮我解决这个问题,因为我不知道还有什么可以尝试的?

1 回复 | 直到 6 年前

Jeffrey Scofield 6 年前

下面是我刚才在Ubuntu 18.04.1下安装z3的步骤:

$ opam depext conf-gmp.1
$ opam depext conf-m4.1

$ opam install z3

现在安装了z3库,您可以从OCaml代码中使用它。但是没有安装可执行文件(我可以找到)。

$ export LD_LIBRARY_PATH=~/.opam/4.06.0/lib/z3
$ ocaml -I ~/.opam/4.06.0/lib/z3
        OCaml version 4.06.0

# #load "nums.cma";;
# #load "z3ml.cma";;
# let ctx = Z3.mk_context [];;
val ctx : Z3.context = <abstr>

设置 LD_LIBRARY_PATH libz3.so .

这是我目前所能得到的。也许这会有帮助。

更新

下面是我如何编译和链接一个测试程序。

$ export LD_LIBRARY_PATH=~/.opam/4.06.0/lib/z3
$ cat tz3.ml
let context = Z3.mk_context []
let solver = Z3.Solver.mk_solver context None

let xsy = Z3.Symbol.mk_string context "x"
let x = Z3.Boolean.mk_const context xsy

let () = Z3.Solver.add solver [x]

let main () =
    match Z3.Solver.check solver [] with
    | UNSATISFIABLE -> Printf.printf "unsat\n"
    | UNKNOWN -> Printf.printf "unknown"
    | SATISFIABLE ->
        match Z3.Solver.get_model solver with
        | None -> ()
        | Some model ->
            Printf.printf "%s\n"
                (Z3.Model.to_string model)

let () = main ()

$ ocamlopt -I ~/.opam/4.06.0/lib/z3 -o tz3 \
     nums.cmxa z3ml.cmxa tz3.ml

$ ./tz3
(define-fun x () Bool
  true)
$ unset LD_LIBRARY_PATH
$ ./tz3
./tz3: error while loading shared libraries: libz3.so:
 cannot open shared object file: No such file or directory

它是有效的,也就是说,它说 x 可以通过制作是 true

注意 :最初我认为 LD\库\路径

运行你的程序。它对于个人测试来说已经足够好了,但是对于任何更广泛的部署来说可能都不行。有几种方法可以在链接时设置共享库的搜索路径。

我希望这有帮助。