ocaml 上的 Z3 绑定答案

【问题标题】：Z3 bindings on ocamlocaml 上的 Z3 绑定
【发布时间】：2018-11-10 17:50:28
【问题描述】：

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

【问题讨论】：

你用的是什么系统？ Linux？苹果系统？视窗？请显示您正在运行的确切命令和错误输出。
就是这么说的吗？它是否也说类似：cannot open shared object file: No such file or directory?
@JeffreyScofield 我在 Windows 子系统上使用 Linux。我首先运行 make 然后简单地运行本机代码。
@LeventErkok 完整的错误消息是./main.native: error while loading shared libraries: libz3.so: cannot open shared object file: No such file or directory
我怀疑您的安装以某种方式走高线。遵循@JeffreyScofield 的建议可能是您最好的选择，因为他似乎已经成功安装了。

标签： ocaml z3 opam sat-solvers oasis

【解决方案1】：

这是我刚才在 Ubuntu 18.04.1 下安装 z3 所做的：

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

这些在 opam 之外安装了 gmp 和 m4。相当令人印象深刻。

$ 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 来满足琐碎的公式 x。

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

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

我希望这会有所帮助。

【讨论】：