diff --git a/configure.ac b/configure.ac
index 886ca896c28ef113d08d880cc0c6a27cbbecb205..8d5f93abcd1de0af7834d4bfc86f46a8bfa99ba0 100644
--- a/configure.ac
+++ b/configure.ac
@@ -79,7 +79,7 @@ AS_IF([test "x$seal" = "xyes"], [
# z3
AC_MSG_CHECKING(z3 library (optional))
-define([z3path], esyscmd([ocamlfind query z3]))
+define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
AS_IF([ocamlfind query z3 >/dev/null 2>&1],
[z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index 4b2e7b7b2a27bacbc2814c6e2742e9b688e5e54c..56af8f75c1ff14d364fb8b8db1f5f30dcc687fbc 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -48,7 +48,7 @@ let gen_files funs basename prog machines dependencies =
(match !Options.main_node with
| "" -> () (* No main node: we do not generate main *)
| main_node -> (
- match Machine_code_common.get_machine_opt main_node machines with
+ match Machine_code_common.get_machine_opt machines main_node with
| None -> begin
Global.main_node := main_node;
Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
@@ -70,7 +70,7 @@ let gen_files funs basename prog machines dependencies =
| "" -> ()
| mauve -> (
(* looking for the main node *)
- match Machine_code_common.get_machine_opt mauve machines with
+ match Machine_code_common.get_machine_opt machines mauve with
| None -> begin
Global.main_node := mauve;
Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
diff --git a/src/backends/Horn/horn_backend_collecting_sem.ml b/src/backends/Horn/horn_backend_collecting_sem.ml
index 9c28a488c3db27ba73b3db0bf90884a6a96dcd6c..88fdeac7b6660df2915e7f9717e141657376fd7b 100644
--- a/src/backends/Horn/horn_backend_collecting_sem.ml
+++ b/src/backends/Horn/horn_backend_collecting_sem.ml
@@ -49,7 +49,7 @@ let collecting_semantics machines fmt node machine =
(* Init case *)
let _ =
(* Special case when the main node is stateless *)
- if is_stateless machine then (
+ if Machine_code_common.is_stateless machine then (
let step_name = pp_machine_stateless_name in
fprintf fmt "; Initial set: One Step(m,x) -- Stateless node! @.";
fprintf fmt "(declare-rel INIT_STATE ())@.";
@@ -86,7 +86,7 @@ let collecting_semantics machines fmt node machine =
in
let step_name =
- if is_stateless machine then
+ if Machine_code_common.is_stateless machine then
pp_machine_stateless_name
else
pp_machine_step_name
@@ -142,7 +142,7 @@ let cex_computation machines fmt node machine =
(* Special case when the cex node is stateless *)
let reset_name, step_name =
- if is_stateless machine then
+ if Machine_code_common.is_stateless machine then
pp_machine_stateless_name, pp_machine_stateless_name
else
pp_machine_reset_name, pp_machine_step_name
diff --git a/src/backends/Horn/horn_backend_common.ml b/src/backends/Horn/horn_backend_common.ml
index 2c3f5a9d1a8699d023edd5e48c6a42af95ae8c91..872270bb954ae1e830cacc5f0d8f7345abee7e8f 100644
--- a/src/backends/Horn/horn_backend_common.ml
+++ b/src/backends/Horn/horn_backend_common.ml
@@ -14,6 +14,8 @@ open Lustre_types
open Machine_code_types
open Corelang
+let get_machine = Machine_code_common.get_machine
+
let machine_reset_name id = id ^ "_reset"
let machine_step_name id = id ^ "_step"
let machine_stateless_name id = id ^ "_fun"
@@ -78,13 +80,6 @@ let rename_mid_list = List.map rename_mid
let rename_next = rename (fun n -> n ^ "_x")
let rename_next_list = List.map rename_next
-let get_machine machines node_name =
-(* try *)
- List.find (fun m -> m.mname.node_id = node_name) machines
-(* with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?" *)
-(* node_name *)
-(* (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines *)
-(* ; assert false *)
let local_memory_vars machines machine =
rename_machine_list machine.mname.node_id machine.mmemory
@@ -153,6 +148,7 @@ let reset_vars machines m =
@ (rename_mid_list (full_memory_vars machines m))
+
(* Local Variables: *)
(* compile-command:"make -C ../.." *)
(* End: *)
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index 708b689eb53fb36ec4365633c01c9dad27b1fb97..4427ccfeda7f7e376d1435bdba4c86783250780c 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -419,7 +419,6 @@ let pp_machine_reset machines fmt m =
(**************************************************************)
-let is_stateless m = m.minstances = [] && m.mmemory = []
(* Print the machine m:
two functions: m_init and m_step
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index e35e3286a3d8693f3ae5cce0cbaa5a8c1c1369af..508047fce5708865d628b39ca4dd9fe24f6e73a7 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -116,6 +116,8 @@ let rec is_const_value v =
let get_stateless_status m =
(m.mname.node_dec_stateless, try Utils.desome m.mname.node_stateless with _ -> failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed"))
+let is_stateless m = m.minstances = [] && m.mmemory = []
+
let is_input m id =
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs
@@ -223,7 +225,7 @@ let new_instance =
end
-let get_machine_opt name machines =
+let get_machine_opt machines name =
List.fold_left
(fun res m ->
match res with
@@ -231,6 +233,15 @@ let get_machine_opt name machines =
| None -> if m.mname.node_id = name then Some m else None)
None machines
+let get_machine machines node_name =
+ try
+ List.find (fun m -> m.mname.node_id = node_name) machines
+ with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?"
+ node_name
+ (Utils.fprintf_list ~sep:", " (fun fmt m -> Format.pp_print_string fmt m.mname.node_id)) machines
+ ; assert false
+
+
let get_const_assign m id =
try
match get_instr_desc (List.find
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 2cb9f48c55dfd787fb7b7f9e395a5c6aa5c66953..74b02016b764d8ec0348bafd297f5e66f963ddef 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -4,6 +4,7 @@ val is_output: Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
val is_const_value: Machine_code_types.value_t -> bool
val get_const_assign: Machine_code_types.machine_t -> Lustre_types.var_decl -> Machine_code_types.value_t
val get_stateless_status: Machine_code_types.machine_t -> bool * bool
+val is_stateless: Machine_code_types.machine_t -> bool
val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_types.value_t
val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t
val empty_machine: Machine_code_types.machine_t
@@ -14,6 +15,11 @@ val dimension_of_value:Machine_code_types.value_t -> Dimension.dim_expr
val pp_instr: Format.formatter -> Machine_code_types.instr_t -> unit
val pp_instrs: Format.formatter -> Machine_code_types.instr_t list -> unit
val pp_machines: Format.formatter -> Machine_code_types.machine_t list -> unit
-val get_machine_opt: string -> Machine_code_types.machine_t list -> Machine_code_types.machine_t option
+val get_machine_opt: Machine_code_types.machine_t list -> string -> Machine_code_types.machine_t option
+
+(* Same function but fails if no such a machine exists *)
+val get_machine: Machine_code_types.machine_t list -> string -> Machine_code_types.machine_t
+
+
val get_node_def: string -> Machine_code_types.machine_t -> Lustre_types.node_desc
val join_guards_list: Machine_code_types.instr_t list -> Machine_code_types.instr_t list
diff --git a/src/tools/zustre_verifier.ml b/src/tools/zustre_verifier.ml
index 9980a9622af3772ecd5282d0f12a41f9c2cac391..89037415375ba9f50f368ee7a69a9421a82b7476 100644
--- a/src/tools/zustre_verifier.ml
+++ b/src/tools/zustre_verifier.ml
@@ -1,5 +1,6 @@
-open LustreSpec
-open Machine_code
+open Lustre_types
+open Machine_code_types
+open Machine_code_common
open Format
(* open Horn_backend_common
* open Horn_backend *)
@@ -16,12 +17,22 @@ let rename_current_list = HBC.rename_current_list
let rename_mid_list = HBC.rename_mid_list
let rename_next_list = HBC.rename_next_list
let full_memory_vars = HBC.full_memory_vars
-
-let active = ref false
-let ctx = ref (Z3.mk_context [])
+let inout_vars = HBC.inout_vars
+let reset_vars = HBC.reset_vars
+let step_vars = HBC.step_vars
+let local_memory_vars = HBC.local_memory_vars
+
let machine_reset_name = HBC.machine_reset_name
let machine_stateless_name = HBC.machine_stateless_name
+let rename_mid = HBC.rename_mid
+
+let preprocess = Horn_backend.preprocess
+
+let active = ref false
+let ctx = ref (Z3.mk_context [])
+let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
+
(** Sorts
A sort is introduced for each basic type and each enumerated type.
@@ -105,7 +116,7 @@ let decl_rel name args =
-(** conversion functions
+(** Conversion functions
The following is similar to the Horn backend. Each printing function
is rephrased from pp_xx to xx_to_expr and produces a Z3 value.
@@ -168,7 +179,8 @@ let rec horn_default_val t =
* | Types.Ttuple(l) -> assert false
* |_ -> *) assert false
-
+(* Conversion of basic library functions *)
+
let horn_basic_app i val_to_expr vl =
match i, vl with
| "ite", [v1; v2; v3] ->
@@ -445,10 +457,39 @@ let instance_call_to_exprs machines reset_instances m i inputs outputs =
in
[expr]
)
+
+
+
+(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
+(* let rec value_suffix_to_expr self value = *)
+(* match value.value_desc with *)
+(* | Fun (n, vl) -> *)
+(* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
+(* | _ -> *)
+(* horn_val_to_expr self value *)
+
+(* type_directed assignment: array vs. statically sized type
+ - [var_type]: type of variable to be assigned
+ - [var_name]: name of variable to be assigned
+ - [value]: assigned value
+ - [pp_var]: printer for variables
+*)
+let assign_to_exprs m var_name value =
+ let self = m.mname.node_id in
+ let e =
+ Z3.Boolean.mk_eq
+ !ctx
+ (horn_val_to_expr ~is_lhs:true self var_name)
+ (horn_val_to_expr self value)
+ (* was: TODO deal with array accesses (value_suffix_to_expr self value) *)
+ in
+ [e]
+
+
(* Convert instruction to Z3.Expr and update the set of reset instances *)
-let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
+let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
match Corelang.get_instr_desc instr with
| MComment _ -> [], reset_instances
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
@@ -459,12 +500,12 @@ let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.ex
i::reset_instances
| MLocalAssign (i,v) ->
assign_to_exprs
- m (horn_var_to_expr)
+ m
(mk_val (LocalVar i) i.var_type) v,
reset_instances
| MStateAssign (i,v) ->
assign_to_exprs
- m (horn_var_to_expr)
+ m
(mk_val (StateVar i) i.var_type) v,
reset_instances
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
@@ -487,82 +528,99 @@ let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.ex
statement. *)
let self = m.mname.node_id in
let branch_to_expr (tag, instrs) =
- Z3.Boolean.mk_implies
- (Z3.Boolean.mk_eq !ctx
- (horn_val_to_expr self g)
- (horn_tag_to_expr tag))
- (machine_instrs_to_exprs machines reset_instances m instrs)
+ let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
+ let e =
+ Z3.Boolean.mk_implies !ctx
+ (Z3.Boolean.mk_eq !ctx
+ (horn_val_to_expr self g)
+ (horn_tag_to_expr tag))
+ branch_def in
+
+ [e], branch_resets
+
in
- List.map branch_to_expr hl,
- reset_instances
+ List.fold_left (fun (instrs, resets) b ->
+ let b_instrs, b_resets = branch_to_expr b in
+ instrs@b_instrs, resets@b_resets
+ ) ([], reset_instances) hl
and instrs_to_expr machines reset_instances m instrs =
- let instr_to_expr rs i = instr_to_expr machines rs m i in
- match instrs with
- | [x] -> instr_to_expres reset_instances x
- | _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *)
-
- List.fold_left (fun (exprs, rs) i ->
- let exprs_i, rs = ppi rs i in
- expr@exprs_i, rs
- )
- ([], reset_instances) instrs
-
-
- | [] -> [], reset_instances
-
-
-let basic_library_to_horn_expr i vl =
- match i, vl with
- | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
-
- | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
- | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
- | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
- | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
- | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
- | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
- | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
- | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
- | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
- | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
- | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
- | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
- | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
-(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
-
-*)
+ let instr_to_exprs rs i = instr_to_exprs machines rs m i in
+ let e_list, rs =
+ match instrs with
+ | [x] -> instr_to_exprs reset_instances x
+ | _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *)
+
+ List.fold_left (fun (exprs, rs) i ->
+ let exprs_i, rs_i = instr_to_exprs rs i in
+ exprs@exprs_i, rs@rs_i
+ )
+ ([], reset_instances) instrs
+
+
+ | [] -> [], reset_instances
+ in
+ let e =
+ match e_list with
+ | [e] -> e
+ | [] -> Z3.Boolean.mk_true !ctx
+ | _ -> Z3.Boolean.mk_and !ctx e_list
+ in
+ e, rs
-(* Prints a [value] indexed by the suffix list [loop_vars] *)
-let rec value_suffix_to_expr self value =
- match value.value_desc with
- | Fun (n, vl) ->
- basic_library_to_horn_expr n (value_suffix_to_expr self vl)
- | _ ->
- horn_val_to_expr self value
+let machine_reset machines m =
+ let locals = local_memory_vars machines m in
+
+ (* print "x_m = x_c" for each local memory *)
+ let mid_mem_def =
+ List.map (fun v ->
+ Z3.Boolean.mk_eq !ctx
+ (horn_var_to_expr (rename_mid v))
+ (horn_var_to_expr (rename_current v))
+ ) locals
+ in
-
-(* type_directed assignment: array vs. statically sized type
- - [var_type]: type of variable to be assigned
- - [var_name]: name of variable to be assigned
- - [value]: assigned value
- - [pp_var]: printer for variables
-*)
-let assign_to_exprs m var_name value =
- let self = m.mname.node_id in
- let e =
- Z3.Boolean.mk_eq
- !ctx
- (horn_val_to_expr ~is_lhs:true self var_name)
- (value_suffix_to_expr self value)
+ (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
+ Special treatment for _arrow: _first = true
+ *)
+
+ let reset_instances =
+
+ List.map (fun (id, (n, _)) ->
+ let name = node_name n in
+ if name = "_arrow" then (
+ Z3.Boolean.mk_eq !ctx
+ (
+ let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
+ Z3.Expr.mk_const_f !ctx vdecl
+ )
+ (Z3.Boolean.mk_true !ctx)
+
+ ) else (
+ let machine_n = get_machine machines name in
+
+ Z3.Expr.mk_app
+ !ctx
+ (get_fdecl (name ^ "_reset"))
+ (List.map (horn_var_to_expr)
+ (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
+ )
+
+ )
+ ) m.minstances
+
+
in
- [e]
+
+ Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
+
+
-(* TODO: empty list means true statement *)
+(* TODO: empty list means true statement *)
let decl_machine machines m =
- if m.Machine_code.mname.node_id = Machine_code.arrow_id then
- (* We don't print arrow function *)
+ if m.mname.node_id = Arrow.arrow_id then
+ (* We don't do arrow function *)
()
else
begin
@@ -571,42 +629,47 @@ let decl_machine machines m =
(
(inout_vars machines m)@
(rename_current_list (full_memory_vars machines m)) @
- (rename_mid_list (full_memory_vars machines m)) @
- (rename_next_list (full_memory_vars machines m)) @
- (rename_machine_list m.mname.node_id m.mstep.step_locals)
+ (rename_mid_list (full_memory_vars machines m)) @
+ (rename_next_list (full_memory_vars machines m)) @
+ (rename_machine_list m.mname.node_id m.mstep.step_locals)
)
in
if is_stateless m then
begin
(* Declaring single predicate *)
- let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in
- match m.mstep.step_asserts with
+ let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in
+ let horn_body, _ (* don't care for reset here *) =
+ instrs_to_expr
+ machines
+ ([] (* No reset info for stateless nodes *) )
+ m
+ m.mstep.step_instrs
+ in
+ let horn_head =
+ Z3.Expr.mk_app
+ !ctx
+ (get_fdecl (machine_stateless_name m.mname.node_id))
+ (List.map (horn_var_to_expr) (inout_vars machines m))
+ in
+ match m.mstep.step_asserts with
| [] ->
begin
-
- (* Rule for single predicate *)
- fprintf fmt "; Stateless step rule @.";
- fprintf fmt "@[<v 2>(rule (=> @ ";
- ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs);
- fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
- pp_machine_stateless_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m);
+ (* Rule for single predicate : "; Stateless step rule @." *)
+ Z3.Fixedpoint.add_rule !fp
+ (Z3.Boolean.mk_implies !ctx horn_body horn_head)
+ None
end
| assertsl ->
begin
- let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
-
- fprintf fmt "; Stateless step rule with Assertions @.";
- (*Rule for step*)
- fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
- ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
- fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
- pp_machine_stateless_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
-
+ (*Rule for step "; Stateless step rule with Assertions @.";*)
+ let body_with_asserts =
+ Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
+ in
+ Z3.Fixedpoint.add_rule !fp
+ (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
+ None
end
-
end
else
begin
@@ -615,36 +678,54 @@ let decl_machine machines m =
let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in
(* Rule for reset *)
- fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
- (pp_machine_reset machines) m
- pp_machine_reset_name m.mname.node_id
- (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m);
- match m.mstep.step_asserts with
+ let horn_reset_body = machine_reset machines m in
+ let horn_reset_head =
+ Z3.Expr.mk_app
+ !ctx
+ (get_fdecl (machine_reset_name m.mname.node_id))
+ (List.map (horn_var_to_expr) (reset_vars machines m))
+ in
+
+ let _ =
+ Z3.Fixedpoint.add_rule !fp
+ (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
+ None
+ in
+
+ (* Rule for step*)
+ let horn_step_body, _ (* don't care for reset here *) =
+ instrs_to_expr
+ machines
+ []
+ m
+ m.mstep.step_instrs
+ in
+ let horn_step_head =
+ Z3.Expr.mk_app
+ !ctx
+ (get_fdecl (machine_step_name m.mname.node_id))
+ (List.map (horn_var_to_expr) (step_vars machines m))
+ in
+ match m.mstep.step_asserts with
| [] ->
begin
- fprintf fmt "; Step rule @.";
- (* Rule for step*)
- fprintf fmt "@[<v 2>(rule (=> @ ";
- ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
- fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
- pp_machine_step_name m.mname.node_id
- (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m);
+ (* Rule for single predicate *)
+ Z3.Fixedpoint.add_rule !fp
+ (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
+ None
end
- | assertsl ->
+ | assertsl ->
begin
- let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
- (* print_string pp_val; *)
- fprintf fmt "; Step rule with Assertions @.";
-
- (*Rule for step*)
- fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
- ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
- fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
- pp_machine_step_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
+ (* Rule for step Assertions @.; *)
+ let body_with_asserts =
+ Z3.Boolean.mk_and !ctx
+ (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
+ in
+ Z3.Fixedpoint.add_rule !fp
+ (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
+ None
end
-
end
end
@@ -679,7 +760,7 @@ module Verifier =
Backends.get_normalization_params ()
let setup_solver () =
- let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in
+ fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
(* let help = Z3.Fixedpoint.get_help fp in
* Format.eprintf "Fp help : %s@." help;
*
@@ -744,18 +825,18 @@ module Verifier =
P.add_bool params (mks "xform.inline_linear") false;
P.add_bool params (mks "xform.inline_eager") false
);
- Z3.Fixedpoint.set_parameters fp params
-
+ Z3.Fixedpoint.set_parameters !fp params
+
let run basename prog machines =
- let machines = Machine_code.arrow_machine::machines in
+ let machines = Machine_code_common.arrow_machine::machines in
let machines = preprocess machines in
setup_solver ();
decl_sorts ();
List.iter (decl_machine machines) (List.rev machines);
-
-
()
+
+
end: VerifierType.S)