ocaml上的Z3绑定

Question

我目前正在使用ocaml 4.06.0，并尝试使用Z3 sat解算器。我正在使用opam的oasis来编译文件(这成功地构建了所有内容(。但是，当我运行生成的本机代码时，我会得到以下错误：error while loading shared libraries: libz3.so。我尝试重新安装z3软件包，但错误仍然存在。有人能帮我解决这个问题吗？因为我不知道还能做什么？

Answer 1

以下是我刚才在Ubuntu 18.04.1:下安装z3的操作

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

他们把gmp和m4安装在了opam之外。令人印象深刻。

$ 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 "unsatn"
| UNKNOWN -> Printf.printf "unknown"
| SATISFIABLE ->
match Z3.Solver.get_model solver with
| None -> ()
| Some model ->
Printf.printf "%sn"
(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可以通过使x为true来满足。

注意：起初我认为这里没有必要设置LD_LIBRARY_PATH。但在后来的测试中，我发现这是必要的。所以这可能是你问题的关键。

为运行程序设置LD_LIBRARY_PATH有点麻烦并且容易出错。它对于个人测试来说已经足够好了，但可能不适合任何更广泛的部署。有一些方法可以在链接时设置共享库的搜索路径。

我希望这能有所帮助。