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

ML API: flat & rich layer in place.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-02-21 13:25:31 +00:00
parent 79d0c32c91
commit d293b579f3
5 changed files with 7040 additions and 1390 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
examples/ml/ml_example.ml
View file

@ -26,20 +26,14 @@ exception TestFailedException of string
*) *)
let model_converter_test ( ctx : context ) = let model_converter_test ( ctx : context ) =
Printf.printf "ModelConverterTest\n"; Printf.printf "ModelConverterTest\n";
let xr = (arith_expr_of_expr let xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in
(Expr.mk_const ctx (Symbol.mk_string ctx "x") let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in
(sort_of_arith_sort (arith_sort_of_real_sort (Real.mk_sort ctx))))) in
let yr = (arith_expr_of_expr
(Expr.mk_const ctx (Symbol.mk_string ctx "y")
(sort_of_arith_sort (arith_sort_of_real_sort (Real.mk_sort ctx))))) in
let g4 = (mk_goal ctx true false false ) in let g4 = (mk_goal ctx true false false ) in
(Goal.assert_ g4 [ (mk_gt ctx xr (Goal.assert_ g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ;
(arith_expr_of_real_expr (real_expr_of_rat_num
(Real.mk_numeral_nd ctx 10 1)))) ]) ;
(Goal.assert_ g4 [ (mk_eq ctx (Goal.assert_ g4 [ (mk_eq ctx
(expr_of_arith_expr yr) yr
(expr_of_arith_expr (Arithmetic.mk_add ctx [ xr; (arith_expr_of_real_expr (real_expr_of_rat_num (Real.mk_numeral_nd ctx 1 1))) ]) ) ) ] ) ; (Arithmetic.mk_add ctx [ xr; (Real.mk_numeral_nd ctx 1 1) ])) ]) ;
(Goal.assert_ g4 [ (mk_gt ctx yr (arith_expr_of_real_expr (real_expr_of_rat_num (Real.mk_numeral_nd ctx 1 1)))) ]) ; (Goal.assert_ g4 [ (mk_gt ctx yr (Real.mk_numeral_nd ctx 1 1)) ]) ;
( (
let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in let ar = (Tactic.apply (mk_tactic ctx "simplify") g4 None) in
if ((get_num_subgoals ar) == 1 && if ((get_num_subgoals ar) == 1 &&
@ -83,7 +77,7 @@ let basic_tests ( ctx : context ) =
let fname = (mk_string ctx "f") in let fname = (mk_string ctx "f") in
let x = (mk_string ctx "x") in let x = (mk_string ctx "x") in
let y = (mk_string ctx "y") in let y = (mk_string ctx "y") in
let bs = (sort_of_bool_sort (Boolean.mk_sort ctx)) in let bs = (Boolean.mk_sort ctx) in
let domain = [ bs; bs ] in let domain = [ bs; bs ] in
let f = (FuncDecl.mk_func_decl ctx fname domain bs) in let f = (FuncDecl.mk_func_decl ctx fname domain bs) in
let fapp = (mk_app ctx f let fapp = (mk_app ctx f
@ -123,10 +117,8 @@ let basic_tests ( ctx : context ) =
Printf.printf "Test passed.\n" Printf.printf "Test passed.\n"
); );
(Goal.assert_ g [ (mk_eq ctx (Goal.assert_ g [ (mk_eq ctx
(mk_numeral_int ctx 1 (mk_numeral_int ctx 1 (BitVector.mk_sort ctx 32))
(sort_of_bitvec_sort (BitVector.mk_sort ctx 32))) (mk_numeral_int ctx 2 (BitVector.mk_sort ctx 32))) ] )
(mk_numeral_int ctx 2
(sort_of_bitvec_sort (BitVector.mk_sort ctx 32)))) ] )
; ;
( (
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
@ -157,10 +149,10 @@ let basic_tests ( ctx : context ) =
); );
( (
let g3 = (mk_goal ctx true true false) in let g3 = (mk_goal ctx true true false) in
let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (sort_of_arith_sort (arith_sort_of_int_sort (Integer.mk_sort ctx)))) in let xc = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Integer.mk_sort ctx)) in
let yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (sort_of_arith_sort (arith_sort_of_int_sort (Integer.mk_sort ctx)))) in let yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Integer.mk_sort ctx)) in
(Goal.assert_ g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (sort_of_arith_sort (arith_sort_of_int_sort (Integer.mk_sort ctx))))) ]) ; (Goal.assert_ g3 [ (mk_eq ctx xc (mk_numeral_int ctx 1 (Integer.mk_sort ctx))) ]) ;
(Goal.assert_ g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (sort_of_arith_sort (arith_sort_of_int_sort (Integer.mk_sort ctx))))) ]) ; (Goal.assert_ g3 [ (mk_eq ctx yc (mk_numeral_int ctx 2 (Integer.mk_sort ctx))) ]) ;
let constr = (mk_eq ctx xc yc) in let constr = (mk_eq ctx xc yc) in
(Goal.assert_ g3 [ constr ] ) ; (Goal.assert_ g3 [ constr ] ) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in let ar = (Tactic.apply (mk_tactic ctx "smt") g3 None) in
@ -228,9 +220,9 @@ let _ =
let rs = (Real.mk_sort ctx) in let rs = (Real.mk_sort ctx) in
Printf.printf "int symbol: %s\n" (Symbol.to_string is); Printf.printf "int symbol: %s\n" (Symbol.to_string is);
Printf.printf "string symbol: %s\n" (Symbol.to_string ss); Printf.printf "string symbol: %s\n" (Symbol.to_string ss);
Printf.printf "bool sort: %s\n" (Sort.to_string (sort_of_bool_sort bs)); Printf.printf "bool sort: %s\n" (Sort.to_string bs);
Printf.printf "int sort: %s\n" (Sort.to_string (sort_of_arith_sort (arith_sort_of_int_sort ints))); Printf.printf "int sort: %s\n" (Sort.to_string ints);
Printf.printf "real sort: %s\n" (Sort.to_string (sort_of_arith_sort (arith_sort_of_real_sort rs))); Printf.printf "real sort: %s\n" (Sort.to_string rs);
basic_tests ctx ; basic_tests ctx ;
Printf.printf "Disposing...\n"; Printf.printf "Disposing...\n";
Gc.full_major () Gc.full_major ()

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

File diff suppressed because it is too large Load diff

460
src/api/ml/z3.mli
View file

File diff suppressed because it is too large Load diff

3400
src/api/ml/z3_rich.ml Normal file
View file

File diff suppressed because it is too large Load diff

3072
src/api/ml/z3_rich.mli Normal file
View file

File diff suppressed because it is too large Load diff