Z3 крепления на ocaml - PullRequest
Новая
       66

Z3 крепления на ocaml

0 голосов
/ 10 ноября 2018

В настоящее время я использую ocaml 4.06.0 и пытаюсь использовать спутниковый решатель Z3.Я использую оазис opam для компиляции файлов (который строит все успешно).Тем не менее, когда я запускаю собственный код, я получаю следующую ошибку: error while loading shared libraries: libz3.so.Я попытался переустановить пакет z3, но ошибка все еще сохраняется.Может кто-нибудь помочь мне решить это, пожалуйста, потому что я не знаю, что еще попробовать?

1 Ответ

0 голосов
/ 10 ноября 2018

Вот что я сделал сейчас, чтобы установить z3 под Ubuntu 18.04.1: 

$ 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 "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.

Примечание : изначально я думал, что настройка LD_LIBRARY_PATH здесь не нужна. Но в последующем тестировании я обнаружил, что это необходимо. Так что это, вероятно, ключ к вашей проблеме.

Немного громоздко и подвержено ошибкам устанавливать LD_LIBRARY_PATH для запуска ваших программ. Это достаточно для личного тестирования, но, вероятно, не для более широкого развертывания. Есть способы установить путь поиска для разделяемых библиотек во время ссылки.

Надеюсь, это поможет.

...