ocaml上的Z3绑定 [英] Z3 bindings on ocaml

问题描述

我当前正在使用ocaml 4.06.0，并且正在尝试使用Z3 sat求解器.我正在使用opam的绿洲来编译文件(这将成功构建所有文件).但是，当我运行生成的本机代码时，出现以下错误:error while loading shared libraries: libz3.so.我尝试重新安装z3软件包，但错误仍然存​​在.有人可以帮我解决这个问题，因为我不知道还能尝试什么?

I am currently using ocaml 4.06.0 and I am trying to use the Z3 sat solver. I am using opam's oasis to compile the files (which is building everything successfully). However, when I run the native code produced I am getting the following error: error while loading shared libraries: libz3.so. I tried reinstalling the z3 package but the error still persists. Can anyone help me solve this please because I have no idea what else to try?

推荐答案

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

Here is what I did just now to install z3 under Ubuntu 18.04.1:

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

这些在opam外部安装了gmp和m4.令人印象深刻.

These installed gmp and m4 outside of opam. Pretty impressive.

$ opam install z3

现在已经安装了z3库，因此您可以从OCaml代码中使用它.但是没有安装可执行文件(我可以找到).

Now the z3 library is installed so you can use it from OCaml code. But there are no executables installed (that I can find).

$ 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成为可能.

The setting of LD_LIBRARY_PATH is what makes it possible to find libz3.so.

这是我目前所掌握的.也许这会有所帮助.

This is as far as I got for now. Maybe this will be helpful.

更新

这是我编译和链接测试程序的方式.

Here is how I compiled and linked a test program.

$ 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可以通过将x设为true来满足.

It works--i.e., it says that the trivial formula x can be satisfied by making x be true.

注意:最初，我认为此处不需要LD_LIBRARY_PATH设置.但是在以后的测试中，我发现这是必要的.所以这可能是解决您问题的关键.

Note: initially I thought the setting of LD_LIBRARY_PATH wasn't necessary here. But in later testing I've found that it is necessary. So that is probably the key to your problem.

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

It's a little cumbersome and error prone to set LD_LIBRARY_PATH for running your programs. It's good enough for personal testing, but probably not for any kind of wider deployment. There are ways to set the search path for shared libraries at link time.

我希望这会有所帮助.

这篇关于ocaml上的Z3绑定的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！