Skip to content
Snippets Groups Projects
Commit dbab1fe5 authored by Pierre Loic Garoche's avatar Pierre Loic Garoche
Browse files

[lustrev] fixed some issues when calling Z3. Seems working for the moment:... 

[lustrev] fixed some issues when calling Z3. Seems working for the moment: basic call to Z3 and sat/unsat result
parent 9f3de818
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/tools/zustre/zustre_analyze.ml
+ 15
− 12
View file @ dbab1fe5
......@@ -42,12 +42,14 @@ let check machines node =
(* Init case *)
let decl_init = decl_rel "INIT_STATE" [] in
(* rule INIT_STATE *)
let _ = add_rule [] (Z3.Expr.mk_app
!ctx
decl_init
[]
) in
(* (special) rule INIT_STATE *)
let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
Z3.Fixedpoint.add_rule !fp init_expr None;
(* let _ = add_rule [] (Z3.Expr.mk_app *)
(* !ctx *)
(* decl_init *)
(* [] *)
(* ) in *)
(* Re-declaring variables *)
let _ = List.map decl_var main_memory_next in
......@@ -149,8 +151,10 @@ let check machines node =
Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
]
in
(* Vars contains all vars: in_out, current, mid, neXt memories *)
let vars = (step_vars_c_m_x machines machine) @ main_output_dummy in
let _ =
add_rule ~dont_touch:[decl_main] [] (Z3.Boolean.mk_implies !ctx horn_body horn_head)
add_rule ~dont_touch:[decl_main] vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
in
......@@ -164,7 +168,7 @@ let check machines node =
let not_prop =
Z3.Boolean.mk_not !ctx prop
in
add_rule ~dont_touch:[decl_main;decl_err] main_memory_next (Z3.Boolean.mk_implies !ctx
add_rule (*~dont_touch:[decl_main;decl_err]*) main_memory_next (Z3.Boolean.mk_implies !ctx
(
Z3.Boolean.mk_and !ctx
[not_prop;
......@@ -182,16 +186,15 @@ let check machines node =
(* Debug instructions *)
let rules_expr = Z3.Fixedpoint.get_rules !fp in
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
if false then
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
(Utils.fprintf_list ~sep:"@ "
(fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
rules_expr;
let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
(* Local Variables: *)
(* compile-command:"make -C ../.." *)
(* End: *)
src/tools/zustre/zustre_common.ml
+ 22
− 21
View file @ dbab1fe5
......@@ -111,7 +111,7 @@ let pp_fdecls fmt =
let decl_var id =
Format.eprintf "Declaring var %s@." id.var_id;
(* Format.eprintf "Declaring var %s@." id.var_id; *)
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
register_fdecl id.var_id fdecl;
fdecl
......@@ -644,7 +644,7 @@ let add_rule ?(dont_touch=[]) vars expr =
if nb_args <= 0 then (
let fdecl = Z3.Expr.get_func_decl e in
(* let params = Z3.FuncDecl.get_parameters fdecl in *)
Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e);
(* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *)
let dkind = Z3.FuncDecl.get_decl_kind fdecl in
match dkind with Z3enums.OP_UNINTERPRETED -> (
(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
......@@ -674,10 +674,10 @@ let add_rule ?(dont_touch=[]) vars expr =
let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
Format.eprintf "Declaring rule: %s with variables %a@."
(Z3.Expr.to_string expr)
(Utils.fprintf_list ~sep:", " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)
;
(* Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @." *)
(* (Z3.Expr.to_string expr) *)
(* (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) *)
(* ; *)
let expr = Z3.Quantifier.mk_forall_const
!ctx (* context *)
(List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
......@@ -690,7 +690,7 @@ let add_rule ?(dont_touch=[]) vars expr =
None (* ? *)
None (* ? *)
in
Format.eprintf "OK@.@?";
(* Format.eprintf "OK@.@?"; *)
(*
TODO: bizarre la declaration de INIT tout seul semble poser pb.
......@@ -845,8 +845,8 @@ let decl_machine machines m =
match m.mstep.step_asserts with
| [] ->
begin
(* Rule for single predicate *)
let vars = vars @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
(* Rule for single predicate *)
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
add_rule vars (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
end
......@@ -857,7 +857,7 @@ let decl_machine machines m =
Z3.Boolean.mk_and !ctx
(horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
in
let vars = vars @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
end
......@@ -870,8 +870,8 @@ let decl_machine machines m =
(* Debug functions *)
let rec extract_expr_fds e =
Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ "
(Z3.Expr.to_string e);
(* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
(* (Z3.Expr.to_string e); *)
(* Removing quantifier is there are some *)
let e = (* I didn't found a nicer way to do it than with an exception. My
......@@ -879,7 +879,7 @@ let rec extract_expr_fds e =
try
let eq = Z3.Quantifier.quantifier_of_expr e in
let e2 = Z3.Quantifier.get_body eq in
Format.eprintf "Extracted quantifier body@ ";
(* Format.eprintf "Extracted quantifier body@ "; *)
e2
with _ -> Format.eprintf "No quantifier info@ "; e
......@@ -892,15 +892,16 @@ let rec extract_expr_fds e =
let fd_name = Z3.Symbol.to_string fd_symbol in
if not (Hashtbl.mem decls fd_name) then
register_fdecl fd_name fd;
Format.eprintf "fdecls (%s): %s@ "
fd_name
(Z3.FuncDecl.to_string fd);
(* Format.eprintf "fdecls (%s): %s@ " *)
(* fd_name *)
(* (Z3.FuncDecl.to_string fd); *)
try
(
let args = Z3.Expr.get_args e in
Format.eprintf "@[<v>@ ";
List.iter extract_expr_fds args;
Format.eprintf "@]@ ";
(* Format.eprintf "@[<v>@ "; *)
(* List.iter extract_expr_fds args; *)
(* Format.eprintf "@]@ "; *)
()
)
with _ ->
Format.eprintf "Impossible to extract fundecl args for expression %s@ "
......@@ -910,8 +911,8 @@ let rec extract_expr_fds e =
Format.eprintf "Impossible to extract anything from expression %s@ "
(Z3.Expr.to_string e)
in
Format.eprintf "@]@ "
(* Format.eprintf "@]@ " *)
()
(* Local Variables: *)
(* compile-command:"make -C ../.." *)
......
src/tools/zustre/zustre_test.ml
+ 29
− 0
View file @ dbab1fe5
......@@ -135,6 +135,35 @@ let _ =
Z3.Fixedpoint.add_rule !fp expr_forall_main1 None;
(* Rule 2: forall x,y, MAIN(x,y) => MAIN(x+1, y+1) *)
let expr_main2_lhs = main_x_y_expr in
let plus_one x = Z3.Arithmetic.mk_add !ctx
[
x;
(* Z3.Arithmetic.Integer.mk_const_s !ctx "1" *)
Z3.Expr.mk_numeral_int !ctx 1 int_sort
] in
let main_x_y_plus_one_expr = Z3.Expr.mk_app !ctx decl_main [plus_one x_expr; plus_one y_expr] in
let expr_main2_rhs = main_x_y_plus_one_expr in
let expr_main2 = Z3.Boolean.mk_implies !ctx expr_main2_lhs expr_main2_rhs in
(* Adding forall as prefix *)
let expr_forall_main2 = Z3.Quantifier.mk_forall_const
!ctx (* context *)
(*
[int_sort; int_sort] (* sort list*)
[Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)
*)
(* [x_expr; y_expr] Second try with expr list "const" *)
[Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
expr_main2 (* expression *)
None (* quantifier weight, None means 1 *)
[] (* pattern list ? *)
[] (* ? *)
None (* ? *)
None (* ? *)
in
let expr_forall_main2 = Z3.Quantifier.expr_of_quantifier expr_forall_main2 in
Z3.Fixedpoint.add_rule !fp expr_forall_main2 None;
(* TODO: not implemented yet since the error is visible without it *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment