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: bugfixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-02-19 23:42:50 +00:00
parent 25615aedd9
commit 9142901efe
2 changed files with 67 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

54
examples/ml/ml_example.ml
View file

@ -7,6 +7,7 @@ open Z3
open Z3.Symbol open Z3.Symbol
open Z3.Sort open Z3.Sort
open Z3.Expr open Z3.Expr
open Z3.Boolean
open Z3.FuncDecl open Z3.FuncDecl
open Z3.Goal open Z3.Goal
open Z3.Tactic open Z3.Tactic
@ -22,12 +23,20 @@ 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 = ((mk_const ctx (Symbol.mk_string ctx "x") (mk_real_sort ctx )) :> arith_expr) in let xr = (arith_expr_of_expr
let yr = ((mk_const ctx (Symbol.mk_string ctx "y") (mk_real_sort ctx )) :> arith_expr) in (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 g4 = (mk_goal ctx true false false ) 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_gt ctx xr
(Goal.assert_ g4 [| (mk_eq ctx yr (mk_add ctx [| xr; (mk_real_numeral_nd ctx 1 1) |] )) |] ) ; (arith_expr_of_real_expr (real_expr_of_rat_num
(Goal.assert_ g4 [| (mk_gt ctx yr (mk_real_numeral_nd ctx 1 1)) |]) ; (Real.mk_numeral_nd ctx 10 1)))) |]) ;
(Goal.assert_ g4 [| (mk_eq ctx
(expr_of_arith_expr yr)
(expr_of_arith_expr (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)))) |]) ;
( (
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 &&
@ -67,15 +76,15 @@ let model_converter_test ( ctx : context ) =
*) *)
let basic_tests ( ctx : context ) = let basic_tests ( ctx : context ) =
Printf.printf "BasicTests\n" ; Printf.printf "BasicTests\n" ;
let qi = (mk_int ctx 1) in (* let qi = (mk_int ctx 1) in *)
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.mk_bool ctx) in let bs = (sort_of_bool_sort (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
[| (mk_const ctx x bs); (mk_const ctx y bs) |]) in [| (Expr.mk_const ctx x bs); (Expr.mk_const ctx y bs) |]) in
let fargs2 = [| (mk_fresh_const ctx "cp" bs) |] in let fargs2 = [| (mk_fresh_const ctx "cp" bs) |] in
let domain2 = [| bs |] in let domain2 = [| bs |] in
let fapp2 = (mk_app ctx (mk_fresh_func_decl ctx "fp" domain2 bs) fargs2) in let fapp2 = (mk_app ctx (mk_fresh_func_decl ctx "fp" domain2 bs) fargs2) in
@ -110,8 +119,11 @@ let basic_tests ( ctx : context ) =
else else
Printf.printf "Test passed.\n" Printf.printf "Test passed.\n"
); );
(Goal.assert_ g [| (mk_eq ctx (mk_numeral_int ctx 1 (BitVectors.mk_sort ctx 32)) (Goal.assert_ g [| (mk_eq ctx
(mk_numeral_int ctx 2 (BitVectors.mk_sort ctx 32))) |] ) (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)))) |] )
; ;
( (
let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in let ar = (Tactic.apply (mk_tactic ctx "smt") g None) in
@ -132,7 +144,7 @@ let basic_tests ( ctx : context ) =
); );
( (
let g2 = (mk_goal ctx true true false) in let g2 = (mk_goal ctx true true false) in
(Goal.assert_ g2 [| (mk_false ctx) |]) ; (Goal.assert_ g2 [| (Boolean.mk_false ctx) |]) ;
let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in let ar = (Tactic.apply (mk_tactic ctx "smt") g2 None) in
if ((get_num_subgoals ar) == 1 && if ((get_num_subgoals ar) == 1 &&
(not (is_decided_unsat (get_subgoal ar 0)))) then (not (is_decided_unsat (get_subgoal ar 0)))) then
@ -142,10 +154,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 = (mk_const ctx (Symbol.mk_string ctx "x") (mk_int_sort ctx)) 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 = (mk_const ctx (Symbol.mk_string ctx "y") (mk_int_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 (mk_int_sort ctx))) |]) ; (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 (mk_int_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 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
@ -208,14 +220,14 @@ let _ =
let ctx = (mk_context cfg) in let ctx = (mk_context cfg) in
let is = (Symbol.mk_int ctx 42) in let is = (Symbol.mk_int ctx 42) in
let ss = (Symbol.mk_string ctx "mySymbol") in let ss = (Symbol.mk_string ctx "mySymbol") in
let bs = (Sort.mk_bool ctx) in let bs = (Boolean.mk_sort ctx) in
let ints = (mk_int_sort ctx) in let ints = (Integer.mk_sort ctx) in
let rs = (mk_real_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 bs); Printf.printf "bool sort: %s\n" (Sort.to_string (sort_of_bool_sort bs));
Printf.printf "int sort: %s\n" (Sort.to_string ints); 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 rs); Printf.printf "real sort: %s\n" (Sort.to_string (sort_of_arith_sort (arith_sort_of_real_sort rs)));
basic_tests ctx ; basic_tests ctx ;
Printf.printf "Disposing...\n"; Printf.printf "Disposing...\n";
Gc.full_major () Gc.full_major ()

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

@ -240,7 +240,7 @@ struct
Expr(z3_native_object_of_ast_ptr ctx no) Expr(z3_native_object_of_ast_ptr ctx no)
else else
let s = Z3native.get_sort (context_gno ctx) no in let s = Z3native.get_sort (context_gno ctx) no in
let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in
if (Z3native.is_algebraic_number (context_gno ctx) no) then if (Z3native.is_algebraic_number (context_gno ctx) no) then
Expr(z3_native_object_of_ast_ptr ctx no) Expr(z3_native_object_of_ast_ptr ctx no)
else else
@ -376,92 +376,99 @@ let expr_of_ast a =
Expr(a) Expr(a)
let bool_expr_of_expr e = let bool_expr_of_expr e =
match e with Expr(no) -> match e with Expr(a) ->
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
if (q != Z3enums.BOOL_SORT) then if (q != Z3enums.BOOL_SORT) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
BoolExpr(e) BoolExpr(e)
let arith_expr_of_expr e = let arith_expr_of_expr e =
match e with Expr(no) -> match e with Expr(a) ->
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
if (q != Z3enums.INT_SORT && q != Z3enums.REAL_SORT) then if (q != Z3enums.INT_SORT && q != Z3enums.REAL_SORT) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
ArithExpr(e) ArithExpr(e)
let bitvec_expr_of_expr e = let bitvec_expr_of_expr e =
match e with Expr(no) -> match e with Expr(a) ->
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
if (q != Z3enums.BV_SORT) then if (q != Z3enums.BV_SORT) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
BitVecExpr(e) BitVecExpr(e)
let array_expr_of_expr e = let array_expr_of_expr e =
match e with Expr(no) -> match e with Expr(a) ->
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
if (q != Z3enums.ARRAY_SORT) then if (q != Z3enums.ARRAY_SORT) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
ArrayExpr(e) ArrayExpr(e)
let datatype_expr_of_expr e = let datatype_expr_of_expr e =
match e with Expr(no) -> match e with Expr(a) ->
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
if (q != Z3enums.DATATYPE_SORT) then if (q != Z3enums.DATATYPE_SORT) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
DatatypeExpr(e) DatatypeExpr(e)
let int_expr_of_arith_expr e = let int_expr_of_arith_expr e =
match e with ArithExpr(Expr(no)) -> match e with ArithExpr(Expr(a)) ->
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
if (q != Z3enums.INT_SORT) then if (q != Z3enums.INT_SORT) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
IntExpr(e) IntExpr(e)
let real_expr_of_arith_expr e = let real_expr_of_arith_expr e =
match e with ArithExpr(Expr(no)) -> match e with ArithExpr(Expr(a)) ->
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc no) (z3obj_gno no))) in let s = Z3native.get_sort (z3obj_gnc a) (z3obj_gno a) in
let q = (Z3enums.sort_kind_of_int (Z3native.get_sort_kind (z3obj_gnc a) s)) in
if (q != Z3enums.REAL_SORT) then if (q != Z3enums.REAL_SORT) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
RealExpr(e) RealExpr(e)
let int_num_of_int_expr e = let int_num_of_int_expr e =
match e with IntExpr(ArithExpr(Expr(no))) -> match e with IntExpr(ArithExpr(Expr(a))) ->
if (not (Z3native.is_numeral_ast (z3obj_gnc no) (z3obj_gno no))) then if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
IntNum(e) IntNum(e)
let rat_num_of_real_expr e = let rat_num_of_real_expr e =
match e with RealExpr(ArithExpr(Expr(no))) -> match e with RealExpr(ArithExpr(Expr(a))) ->
if (not (Z3native.is_numeral_ast (z3obj_gnc no) (z3obj_gno no))) then if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
RatNum(e) RatNum(e)
let algebraic_num_of_arith_expr e = let algebraic_num_of_arith_expr e =
match e with ArithExpr(Expr(no)) -> match e with ArithExpr(Expr(a)) ->
if (not (Z3native.is_algebraic_number (z3obj_gnc no) (z3obj_gno no))) then if (not (Z3native.is_algebraic_number (z3obj_gnc a) (z3obj_gno a))) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
AlgebraicNum(e) AlgebraicNum(e)
let bitvec_num_of_bitvec_expr e = let bitvec_num_of_bitvec_expr e =
match e with BitVecExpr(Expr(no)) -> match e with BitVecExpr(Expr(a)) ->
if (not (Z3native.is_numeral_ast (z3obj_gnc no) (z3obj_gno no))) then if (not (Z3native.is_numeral_ast (z3obj_gnc a) (z3obj_gno a))) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
BitVecNum(e) BitVecNum(e)
let quantifier_of_expr e = let quantifier_of_expr e =
match e with Expr(no) -> match e with Expr(a) ->
let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc no) (z3obj_gno no))) in let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in
if (q != Z3enums.QUANTIFIER_AST) then if (q != Z3enums.QUANTIFIER_AST) then
raise (Z3native.Exception "Invalid coercion") raise (Z3native.Exception "Invalid coercion")
else else
@ -4378,7 +4385,8 @@ struct
(** The formulas in the goal. *) (** The formulas in the goal. *)
let get_formulas ( x : goal ) = let get_formulas ( x : goal ) =
let n = get_size x in let n = get_size x in
let f i = bool_expr_of_expr (expr_of_ptr (z3obj_gc x) (Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i)) in let f i = (bool_expr_of_expr (expr_of_ptr (z3obj_gc x)
(Z3native.goal_formula (z3obj_gnc x) (z3obj_gno x) i))) in
Array.init n f Array.init n f
(** The number of formulas, subformulas and terms in the goal. *) (** The number of formulas, subformulas and terms in the goal. *)