mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +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 a0f6d1d3df
commit 6417f9e648
4 changed files with 6865 additions and 1105 deletions
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 ) =
Printf.printf "ModelConverterTest\n";
let xr = (arith_expr_of_expr
(Expr.mk_const ctx (Symbol.mk_string ctx "x")
(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 xr = (Expr.mk_const ctx (Symbol.mk_string ctx "x") (Real.mk_sort ctx)) in
let yr = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (Real.mk_sort ctx)) in
let g4 = (mk_goal ctx true false false ) in
(Goal.assert_ g4 [ (mk_gt ctx xr
(arith_expr_of_real_expr (real_expr_of_rat_num
(Real.mk_numeral_nd ctx 10 1)))) ]) ;
(Goal.assert_ g4 [ (mk_gt ctx xr (Real.mk_numeral_nd ctx 10 1)) ]) ;
(Goal.assert_ g4 [ (mk_eq ctx
(expr_of_arith_expr 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))) ]) ) ) ] ) ;
(Goal.assert_ g4 [ (mk_gt ctx yr (arith_expr_of_real_expr (real_expr_of_rat_num (Real.mk_numeral_nd ctx 1 1)))) ]) ;
yr
(Arithmetic.mk_add ctx [ xr; (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
if ((get_num_subgoals ar) == 1 &&
@ -83,7 +77,7 @@ let basic_tests ( ctx : context ) =
let fname = (mk_string ctx "f") in
let x = (mk_string ctx "x") 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 f = (FuncDecl.mk_func_decl ctx fname domain bs) in
let fapp = (mk_app ctx f
@ -123,10 +117,8 @@ let basic_tests ( ctx : context ) =
Printf.printf "Test passed.\n"
);
(Goal.assert_ g [ (mk_eq ctx
(mk_numeral_int ctx 1
(sort_of_bitvec_sort (BitVector.mk_sort ctx 32)))
(mk_numeral_int ctx 2
(sort_of_bitvec_sort (BitVector.mk_sort ctx 32)))) ] )
(mk_numeral_int ctx 1 (BitVector.mk_sort ctx 32))
(mk_numeral_int ctx 2 (BitVector.mk_sort ctx 32))) ] )
;
(
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 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 yc = (Expr.mk_const ctx (Symbol.mk_string ctx "y") (sort_of_arith_sort (arith_sort_of_int_sort (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 yc (mk_numeral_int ctx 2 (sort_of_arith_sort (arith_sort_of_int_sort (Integer.mk_sort ctx))))) ]) ;
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") (Integer.mk_sort ctx)) in
(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 (Integer.mk_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
@ -228,9 +220,9 @@ let _ =
let rs = (Real.mk_sort ctx) in
Printf.printf "int symbol: %s\n" (Symbol.to_string is);
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 "int sort: %s\n" (Sort.to_string (sort_of_arith_sort (arith_sort_of_int_sort ints)));
Printf.printf "real sort: %s\n" (Sort.to_string (sort_of_arith_sort (arith_sort_of_real_sort rs)));
Printf.printf "bool sort: %s\n" (Sort.to_string bs);
Printf.printf "int sort: %s\n" (Sort.to_string ints);
Printf.printf "real sort: %s\n" (Sort.to_string rs);
basic_tests ctx ;
Printf.printf "Disposing...\n";
Gc.full_major ()

1458
src/api/ml/z3.ml
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