Skip to content

Instantly share code, notes, and snippets.

@ashiato45
Last active September 6, 2018 08:26
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ashiato45/5eb612ee4b2512696d1622ecc84ec7c3 to your computer and use it in GitHub Desktop.
Save ashiato45/5eb612ee4b2512696d1622ecc84ec7c3 to your computer and use it in GitHub Desktop.
tried z3 wrapper in OCaml
./test.exe: symbol lookup error: ./test.exe: undefined symbol: Z3_get_full_version
open Core
open Z3
let () =
let ctx = mk_context [("model", "true"); ("proof", "false")] in
(* let solver = Solver.mk_solver cfg None in *)
let open Boolean in
let open Symbol in
let open FuncDecl in
let open Expr in
let open Goal in
let open Solver in
Printf.printf "BasicTests\n" ;
let fname = (mk_string ctx "f") in
let x = (mk_string ctx "x") in
let y = (mk_string ctx "y") in
let bs = (Boolean.mk_sort ctx) in
let domain = [ bs; bs ] in
let f = (FuncDecl.mk_func_decl ctx fname domain bs) in
let fapp = (mk_app ctx f
[ (Expr.mk_const ctx x bs); (Expr.mk_const ctx y bs) ]) in
let fargs2 = [ (mk_fresh_const ctx "cp" bs) ] in
let domain2 = [ bs ] in
let fapp2 = (mk_app ctx (mk_fresh_func_decl ctx "fp" domain2 bs) fargs2) in
let trivial_eq = (mk_eq ctx fapp fapp) in
let nontrivial_eq = (mk_eq ctx fapp fapp2) in
let g = (mk_goal ctx true false false) in
(Goal.add g [ trivial_eq ]) ;
(Goal.add g [ nontrivial_eq ]) ;
Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ;
(
let solver = (mk_solver ctx None) in
(List.iter ~f:(fun a -> (Solver.add solver [ a ])) (get_formulas g)) ;
if (check solver []) != SATISFIABLE then
assert false
else
Printf.printf "Test passed.\n";
);
open Core
open Z3
let () =
let cfg = [("model", "true"); ("proof", "false")] in
let ctx = (mk_context cfg) in
let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Arithmetic.Integer.mk_sort ctx)) in
let num i = Arithmetic.Integer.mk_numeral_i ctx i in
let lhs = Arithmetic.mk_add ctx [Arithmetic.mk_mul ctx [num 2; xc]; num 1] in
let rhs = num 3 in
let constr = Boolean.mk_eq ctx lhs rhs in
let solver = Solver.mk_solver ctx None in
Solver.add solver [constr];
let res = Solver.check solver [] in
match res with
| SATISFIABLE -> (
print_endline "sat";
let m = Solver.get_model solver in
match m with
| None -> assert false
| Some m -> (
Printf.printf "Model: \n%s\n" (Model.to_string m) ;
match Model.get_const_interp_e m xc with
| None -> ()
| Some xval -> (print_endline ("x="^(string_of_int (Arithmetic.Integer.get_int xval)))
)
))
| UNSATISFIABLE -> print_endline "unsat"
| UNKNOWN -> print_endline "unknonw"
@ashiato45
Copy link
Author

export LD_LIBRARY_PATH=/home/ashiato45/.opam/4.06.1/lib/z3

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment