mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

ML API bugfixes

Browse source 
More ML examples

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-12-27 15:51:42 +00:00
parent cef9c2fa69
commit 597409c8ac
3 changed files with 124 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

165
examples/ml/ml_example.ml
View file

@ -17,6 +17,50 @@ open Z3.Arithmetic
exception TestFailedException of string exception TestFailedException of string
(**
Model Converter test
*)
let model_converter_test ( ctx : context ) =
Printf.printf "ModelConverterTest\n";
let xr = ((mk_const ctx ((Symbol.mk_string ctx "x") :> symbol) (mk_real_sort ctx )) :> arith_expr) in
let yr = ((mk_const ctx ((Symbol.mk_string ctx "y") :> symbol) (mk_real_sort ctx )) :> arith_expr) in
let g4 = (mk_goal ctx true false false ) in
(Goal.assert_ g4 [| (mk_gt ctx xr (mk_real_numeral_nd ctx 10 1)) |]) ;
(Goal.assert_ g4 [| (mk_eq ctx yr (mk_add ctx [| xr; (mk_real_numeral_nd ctx 1 1) |] )) |] ) ;
(Goal.assert_ g4 [| (mk_gt ctx yr (mk_real_numeral_nd ctx 1 1)) |]) ;
(
let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let ar = (Tactic.apply (and_then ctx (mk_tactic ctx ("simplify")) (mk_tactic ctx "solve-eqs") None) g4 None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
;
let solver = (mk_solver ctx None) in
let f e = (Solver.assert_ solver [| e |]) in
ignore (Array.map f (get_formulas (get_subgoal ar 0))) ;
let q = (check solver None) in
if q != SATISFIABLE then
raise (TestFailedException "")
else
let m = (get_model solver) in
match m with
| None -> raise (TestFailedException "")
| Some (m) ->
Printf.printf "Solver says: %s\n" (string_of_status q) ;
Printf.printf "Model: \n%s\n" (Model.to_string m) ;
Printf.printf "Converted Model: \n%s\n" (Model.to_string (convert_model ar 0 m))
)
(** (**
Some basic tests. Some basic tests.
@ -41,59 +85,78 @@ let basic_tests ( ctx : context ) =
(Goal.assert_ g [| trivial_eq |]) ; (Goal.assert_ g [| trivial_eq |]) ;
(Goal.assert_ g [| nontrivial_eq |]) ; (Goal.assert_ g [| nontrivial_eq |]) ;
Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ; Printf.printf "%s\n" ("Goal: " ^ (Goal.to_string g)) ;
let solver = (mk_solver ctx None) in (
(Array.iter (fun a -> (Solver.assert_ solver [| a |])) (get_formulas g)) ; let solver = (mk_solver ctx None) in
if (check solver None) != SATISFIABLE then (Array.iter (fun a -> (Solver.assert_ solver [| a |])) (get_formulas g)) ;
raise (TestFailedException "") if (check solver None) != SATISFIABLE then
else
Printf.printf "Test passed.\n" ;
() ;
let ar = (Tactic.apply (mk_tactic ctx "simplify") g None) in
if ((get_num_subgoals ar) == 1 &&
((is_decided_sat (get_subgoal ar 0)) ||
(is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "") raise (TestFailedException "")
else else
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in Printf.printf "Test passed.\n"
if ((get_num_subgoals ar) == 1 && );
(not (is_decided_sat (get_subgoal ar 0)))) then (
raise (TestFailedException "") let ar = (Tactic.apply (mk_tactic ctx "simplify") g None) in
else if ((get_num_subgoals ar) == 1 &&
(Goal.assert_ g [| (mk_eq ctx (mk_numeral_int ctx 1 (BitVectors.mk_sort ctx 32)) ((is_decided_sat (get_subgoal ar 0)) ||
(mk_numeral_int ctx 2 (BitVectors.mk_sort ctx 32))) |] ) (is_decided_unsat (get_subgoal ar 0)))) then
; raise (TestFailedException "")
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in else
if ((get_num_subgoals ar) == 1 && Printf.printf "Test passed.\n"
(not (is_decided_unsat (get_subgoal ar 0)))) then );
raise (TestFailedException "") (
else let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
let g2 = (mk_goal ctx true true false) in if ((get_num_subgoals ar) == 1 &&
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in (not (is_decided_sat (get_subgoal ar 0)))) then
if ((get_num_subgoals ar) == 1 && raise (TestFailedException "")
(not (is_decided_sat (get_subgoal ar 0)))) then else
raise (TestFailedException "") Printf.printf "Test passed.\n"
else );
() (Goal.assert_ g [| (mk_eq ctx (mk_numeral_int ctx 1 (BitVectors.mk_sort ctx 32))
(* (mk_numeral_int ctx 2 (BitVectors.mk_sort ctx 32))) |] )
g2 = ctx.MkGoal(true, true); ;
g2.Assert(ctx.MkFalse()); (
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g2); let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedUnsat) if ((get_num_subgoals ar) == 1 &&
throw new TestFailedException(); (not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
Goal g3 = ctx.MkGoal(true, true); else
Expr xc = ctx.MkConst(ctx.MkSymbol("x"), ctx.IntSort); Printf.printf "Test passed.\n"
Expr yc = ctx.MkConst(ctx.MkSymbol("y"), ctx.IntSort); );
g3.Assert(ctx.MkEq(xc, ctx.MkNumeral(1, ctx.IntSort))); (
g3.Assert(ctx.MkEq(yc, ctx.MkNumeral(2, ctx.IntSort))); let g2 = (mk_goal ctx true true false) in
BoolExpr constr = ctx.MkEq(xc, yc); let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
g3.Assert(constr); if ((get_num_subgoals ar) == 1 &&
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g3); (not (is_decided_sat (get_subgoal ar 0)))) then
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedUnsat) raise (TestFailedException "")
throw new TestFailedException(); else
Printf.printf "Test passed.\n"
ModelConverterTest(ctx); );
(
let g2 = (mk_goal ctx true true false) in
(Goal.assert_ g2 [| (mk_false ctx) |]) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
);
(
let g3 = (mk_goal ctx true true false) in
let xc = (mk_const ctx ((Symbol.mk_string ctx "x") :> symbol) (mk_int_sort ctx)) in
let yc = (mk_const ctx ((Symbol.mk_string ctx "y") :> symbol) (mk_int_sort ctx)) in
(Goal.assert_ g3 [| (mk_eq ctx xc (mk_numeral_int ctx 1 (mk_int_sort ctx))) |]) ;
(Goal.assert_ g3 [| (mk_eq ctx yc (mk_numeral_int ctx 2 (mk_int_sort ctx))) |]) ;
let constr = (mk_eq ctx xc yc) in
(Goal.assert_ g3 [| constr |] ) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in
if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then
raise (TestFailedException "")
else
Printf.printf "Test passed.\n"
) ;
model_converter_test ctx
(*
// Real num/den test. // Real num/den test.
RatNum rn = ctx.MkReal(42, 43); RatNum rn = ctx.MkReal(42, 43);
Expr inum = rn.Numerator; Expr inum = rn.Numerator;

6
scripts/mk_util.py
View file

@ -353,9 +353,13 @@ def check_ml():
r = exec_cmd([OCAMLC, 'hello.ml']) r = exec_cmd([OCAMLC, 'hello.ml'])
if r != 0: if r != 0:
raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler') raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler')
os.remove('hello.cmi')
os.remove('hello.cmo')
os.remove('a.out')
r = exec_cmd([OCAMLBUILD]) r = exec_cmd([OCAMLBUILD])
if r != 0: if r != 0:
raise MKException('Failed testing ocamlbuild. Set environment variable OCAMLBUILD with the path to ocamlbuild') raise MKException('Failed testing ocamlbuild. Set environment variable OCAMLBUILD with the path to ocamlbuild')
shutil.rmtree('_build')
find_ml_lib() find_ml_lib()
def find_ml_lib(): def find_ml_lib():
@ -499,7 +503,7 @@ def display_help(exit_code):
if IS_WINDOWS: if IS_WINDOWS:
print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.")
print(" -j, --java generate Java bindings.") print(" -j, --java generate Java bindings.")
print(" --ml generate Ocaml bindinds.") print(" --ml generate OCaml bindings.")
print(" --staticlib build Z3 static library.") print(" --staticlib build Z3 static library.")
if not IS_WINDOWS: if not IS_WINDOWS:
print(" -g, --gmp use GMP.") print(" -g, --gmp use GMP.")

5
src/api/ml/z3.ml
View file

@ -4684,6 +4684,11 @@ module Solver =
struct struct
type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
let string_of_status ( s : status) = match s with
| UNSATISFIABLE -> "unsatisfiable"
| SATISFIABLE -> "satisfiable"
| _ -> "unknown"
(** Objects that track statistical information about solvers. *) (** Objects that track statistical information about solvers. *)
module Statistics = module Statistics =
struct struct