[Ocaml] z3 패키지 설치

https://github.com/Z3Prover/z3

Z3Prover/z3

을 그대로 git clone 해서 설치 방법을 그대로 따라가면 zarith 에대한 오류가 여러개 발생한다.

ocaml 에대해서 num에서 zarith 패키지로 이동하면서 생긴 오류같다.

z3-0b06a9b5d8beca9d0ee6037b23c78a684272f2a4.zip

5.25MB

커밋을 패키지 이동하기 전상태로 돌렸을때의 프로젝트이다. 이것을 풀어서 위에 깃헙에 있는 내용을

그대로 따라하면 쉽게 실행시킬 수 있다.

# make example을 한번 한 후에 이후에는
$ ocamlc -custom -o ml_example.byte -I api/ml -cclib "-L. -lz3" nums.cma z3ml.cma ../examples/ml/ml_example.ml
$ DLD_LIBRARY_PATH=. ./ml_example.byte
# 을 통해 코드를 실행시킬 수 있다.

 

ocaml 에서 z3를 사용하려면 ocaml 만의 문법과 메소드를 사용해서 구현을 해야하는데 이게 쉽지 않다.

문자열로 z3 스크립트를 작성하고 이를 실행시켜주는 코드를 구현할 수 있다.

let _ =
let ctx=Z3.mk_context  [("model", "true"); ("proof", "false")] in
let str = "(declare-const i0 Int)
(assert (= 0 (rem i0 3 ) ) )
(assert (= 2 (rem i0 5 ) ) )
(assert (= 1 (rem i0 7 ) ) )
(declare-const i1 Int)
(assert (= 0 (rem i1 3 ) ) )
(assert (= 3 (rem i1 5 ) ) )
(assert (= 5 (rem i1 7 ) ) )
(declare-const i2 Int)
(assert (> i2 0))
(declare-const i3 Int)
(assert (> i3 0))
(assert ( = ( + ( *  i0  5 ) ( +  i1  7 ))i2 ) )
(assert ( = ( + ( *  i0  2 ) ( +  i1  2 ))i3 ) ) " in
let exprSMT =Z3.SMT.parse_smtlib2_string ctx str [] [] [] [] in 
let sat = Z3.AST.ASTVector.to_expr_list exprSMT in
let solver = (Z3.Solver.mk_solver ctx None) in
(add solver sat) ;
  let q = (check solver []) in
  match q with
    | UNSATISFIABLE -> print_endline "unsat"
    | UNKNOWN -> print_endline "unknown"; 
    | SATISFIABLE -> let m = (get_model solver) in    
                      match m with 
                      | None -> raise (TestFailedException "")
                      | Some (m) -> 
                      prerr_endline (Model.to_string m);