Commit 29e79219 authored by Erwan Jahier's avatar Erwan Jahier

ldbg: add support to hint the user when a constraint fails.

GBDDML: add forall and exist in the caml API
parent 6fbc504c
......@@ -51,9 +51,27 @@ external ite : t -> t -> t -> t = "gbdd_cml_ite"
external size : t -> int = "gbdd_cml_size"
external supportsize : t -> int = "gbdd_cml_supportsize"
(* quantification *)
external exist_local : t -> t -> t = "gbdd_cml_exist"
external forall_local : t -> t -> t = "gbdd_cml_forall"
let support_of_list vars =
assert (vars <> []);
List.fold_left
(fun acc i -> dand acc (idy i))
(idy (List.hd vars))
(List.tl vars)
let rec (exist : int list -> t -> t) =
fun vars bdd ->
exist_local (support_of_list vars) bdd
let rec (forall : int list -> t -> t) =
fun vars bdd ->
forall_local(support_of_list vars) bdd
(* Extra *)
external print_mons : t -> unit = "gbdd_cml_print_mons"
(* compatibilit cudd *)
external topvar : t -> int = "gbdd_cml_root_var"
external dthen : t -> t = "gbdd_cml_high_part"
......
......@@ -447,4 +447,31 @@ CHECK_NOT_NULL(b);
CAMLreturn(Val_unit);
}
value gbdd_cml_exist (value b1, value b2){
CAMLparam2(b1,b2);
CAMLlocal1(res);
CHECK_NOT_NULL(b1);
CHECK_NOT_NULL(b2);
res = alloc_gdbb_block();
#ifdef GBDD_CML_DBG
printf("creating %lx = exist %lx %lx\n", res, b1, b2);
#endif
set_gbdd_value(res, exist(*GBdd_value(b1), *GBdd_value(b2)));
CHECK_NOT_NULL(res);
CAMLreturn(res);
}
value gbdd_cml_forall (value b1, value b2){
CAMLparam2(b1,b2);
CAMLlocal1(res);
CHECK_NOT_NULL(b1);
CHECK_NOT_NULL(b2);
res = alloc_gdbb_block();
#ifdef GBDD_CML_DBG
printf("creating %lx = forall %lx %lx\n", res, b1, b2);
#endif
set_gbdd_value(res, forall(*GBdd_value(b1), *GBdd_value(b2)));
CHECK_NOT_NULL(res);
CAMLreturn(res);
}
}
......@@ -288,9 +288,12 @@ LUTIN_SOURCES = \
$(OBJDIR)/util.ml \
$(OBJDIR)/data.ml \
$(OBJDIR)/data.mli \
$(OBJDIR)/expr.ml \
$(OBJDIR)/failure.mli \
$(OBJDIR)/event.ml \
$(LURETTE_SOURCES_C) \
$(LURETTE_SOURCES) \
$(OBJDIR)/failure.ml \
$(OBJDIR)/expEval.mli \
$(OBJDIR)/expEval.ml \
$(OBJDIR)/verbose.ml \
......
......@@ -101,8 +101,9 @@ del_hooks "print_event";;
let src =
match e.kind with
| Node {port=Exit(cstr,_,src)}
| Node {port=Fail(cstr,_,src)} ->
List.iter (fun si -> print_string si.str) (src());
| Node {port=Fail(cstr,_,src,_)} ->
List.iter (fun si -> print_string si.str) (src());
explain_failure e
| _ -> ()
;;
......
open Event;;
open Ldbg;;
open Ldbg_utils;;
set_sim2chro false;;
set_gnuplot false;;
ltop "set_seed 1";;
add_rp "env:lutin:choice.lut:main" ;;
stl 10;;
show_trace := true;;
let is_fail e =
match e.kind with
| Node { port = Fail(_,_cstr,_,_) } -> true
| _ -> false
;;
let rec next_failure e =
let e = next_cond e is_fail in
explain_failure e;
next_failure e
;;
let e =
try
next_failure(run ())
with _ ->
exit 0;;
......@@ -9,19 +9,6 @@ type ctx = (* herited debug info *)
ctx_outputs : string list;
}
(* Expressions *)
type exp =
| Op of oper * exp list
| True | False
| Ival of Num.num | Fval of float
| Var of string
and
oper =
| And | Or | Xor | Impl | Not | Eq | Ite
| Sup | SupEq | Inf | InfEq
| Sum | Diff | Prod | Quot | Mod | Div | Uminus
| Call of string
type src_info = {
str : string ;
......@@ -32,22 +19,13 @@ type src_info = {
}
(* Try to explain why a constraint is not satisfiable. It can be due
to a pure Boolean reason (in which case we provide xxx); Or there
do exist Boolean solution, but no numeric ones (in which case we
provide the list of monomes) *)
type failure_info =
| Boolean of exp list
| Numeric of exp list
(* Source info related to the elected constraint *)
type cstr_lazy_src_info = (unit -> src_info list)
type port =
| Call
| Exit of string * exp (* The elected contraint that produced the outputs *) * cstr_lazy_src_info
| Fail of string * exp (* The elected contraint that failed *) * cstr_lazy_src_info
(* * (unit -> failure_info) *)
| Exit of string * Expr.t (* The elected contraint that produced the outputs *) * cstr_lazy_src_info
| Fail of string * Expr.t (* The elected contraint that failed *) * cstr_lazy_src_info *
(unit -> Failure.info)
type node_info = {
......
(* Expressions *)
type t =
| Op of oper * t list
| True | False
| Ival of Num.num | Fval of float
| Var of string
and
oper =
| And | Or | Xor | Impl | Not | Eq | Ite
| Sup | SupEq | Inf | InfEq
| Sum | Diff | Prod | Quot | Mod | Div | Uminus
| Call of string
let (to_string : t -> string) =
fun t ->
let rec aux b t =
let b = " "^b in
(match t with
| Op(And,[e1;e2]) -> (aux b e1)^" and " ^(aux b e2)
| Op(Or,[e1;e2]) -> "("^(aux b e1)^" or " ^(aux b e2) ^ ")"
| Op(Xor,[e1;e2]) -> "("^(aux b e1)^" xor" ^(aux b e2) ^ ")"
| Op(Impl,[e1;e2]) -> "("^(aux b e1)^" =>" ^(aux b e2) ^ ")"
| Op(Not,[e]) -> "not(" ^(aux b e) ^")"
| Op(Eq,[e1;e2]) -> (aux b e1)^ "=" ^(aux b e2)
(* | Op(Ite,[c;e1;e2]) -> "("^(aux b e1)^"ite" ^(aux b e2) *)
| Op(Sup,[e1;e2]) -> (aux b e1)^">" ^(aux b e2)
| Op(SupEq,[e1;e2]) -> (aux b e1)^">=" ^(aux b e2)
| Op(Inf,[e1;e2]) -> (aux b e1)^"<" ^(aux b e2)
| Op(InfEq,[e1;e2]) -> (aux b e1)^"<=" ^(aux b e2)
| Op(Sum,[e1;e2]) -> "("^(aux b e1)^"+" ^(aux b e2) ^ ")"
| Op(Diff,[e1;e2]) -> "("^(aux b e1)^"-" ^(aux b e2) ^ ")"
| Op(Prod,[e1;e2]) -> (aux b e1)^"*" ^(aux b e2)
| Op(Quot,[e1;e2]) -> (aux b e1)^"/" ^(aux b e2)
| Op(Mod,[e1;e2]) -> "("^(aux b e1)^"mod" ^(aux b e2) ^ ")"
| Op(Div,[e1;e2]) -> (aux b e1)^"/" ^(aux b e2)
| Op (op,l) -> (oper_aux b op) ^ "(\n"^b ^
((String.concat (",\n"^b) (List.map (aux b) l))^"\n"^b^")")
| True -> "t"
| False -> "f"
| Ival(n) -> Num.string_of_num n
| Fval(f) -> string_of_float f
| Var(str) -> str
)
and
oper_aux b = function
| And -> "and"
| Or -> "or"
| Xor -> "xor"
| Impl -> "impl"
| Not -> "not"
| Eq -> "eq"
| Ite -> "ite"
| Sup -> "sup"
| SupEq -> "supeq"
| Inf -> "inf"
| InfEq -> "infeq"
| Sum -> "sum"
| Diff -> "diff"
| Prod -> "prod"
| Quot -> "quot"
| Mod -> "mod"
| Div -> "div"
| Uminus -> "uminus"
| Call str -> str
in
aux "" t
let dump e =
print_string ((to_string e)^ "\n")
let rec (simplify : t -> t) =
fun t ->
match t with
| Op(And, (Op(And,l)::tail)) -> simplify (Op(And, (l@tail)))
| Op(Or, (Op(Or,l)::tail)) -> simplify (Op(Or, (l@tail)))
| Op(Sum, (Op(Sum,l)::tail)) -> simplify (Op(Sum, (l@tail)))
| Op(Not,[Op(Not, [e])]) -> simplify e
| Op(Not,[Op(Sup, [e1;e2])]) -> Op(InfEq, [simplify e1;simplify e2])
| Op(Not,[Op(Inf, [e1;e2])]) -> Op(SupEq, [simplify e1;simplify e2])
| Op(Not,[Op(SupEq, [e1;e2])]) -> Op(Inf, [simplify e1;simplify e2])
| Op(Not,[Op(InfEq, [e1;e2])]) -> Op(Sup, [simplify e1;simplify e2])
| Op (op,l) -> Op (op, List.map simplify l)
| e -> e
(* exported *)
type info =
| Boolean of Expr.t
| Numeric of Expr.t
open Expr
open Constraint
let (index_to_exp : int -> Expr.t * bool) =
fun i ->
let aux ne =
[Ne.to_expr ne; if Ne.is_int ne then Ival (Num.Int 0) else Fval 0.0]
in
match Formula_to_bdd.index_to_linear_constraint i with
| Bv(v) -> Var (Var.name v), false
| EqZ(ne) -> Op (Eq, aux ne), true
| Ineq(GZ(ne)) -> Op (Sup, aux ne), true
| Ineq(GeqZ(ne)) -> Op (SupEq, aux ne), true
let impl a b = not a || b
let (collect : bool -> Bdd.t -> Expr.t) =
fun num bdd ->
(* Collect the set of paths leading to true. If the [num] flag is
true, collect only the numeric constraints. *)
let rec (aux: Bdd.t -> Expr.t list list) =
(* collect the disjunction of conjunction as a list of list *)
fun bdd ->
assert(not(Bdd.is_true bdd));
assert(not(Bdd.is_false bdd));
let t,e = Bdd.dthen bdd, Bdd.delse bdd in
let v,is_num = index_to_exp (Bdd.topvar bdd) in
let not_v = Op(Not,[v]) in
let res_t =
if (Bdd.is_true t) then (if (impl num is_num) then [[v]] else []) else
if (Bdd.is_false t) then [] else
List.map (fun x -> (if (impl num is_num) then v::x else x)) (aux t)
in
let res_e =
if (Bdd.is_true e) then (if (impl num is_num) then [[not_v]] else []) else
if (Bdd.is_false e) then [] else
List.map (fun x -> (if (impl num is_num) then not_v::x else x)) (aux e)
in
List.rev_append res_e res_t
in
let res =
match aux bdd with
| [] -> assert false
| [[e]] -> e
| [l] -> Op(And, l)
| ll -> Op(Or, List.map (fun l -> Op(And, l)) ll)
in
Expr.simplify res
(* substracting list *)
let lminus l1 l2 = List.filter (fun x -> not (List.mem x l2)) l1
(* exported *)
let (get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> info) =
fun bdd bdd1 (expr2,bdd2) ->
assert (not(Bdd.is_false bdd1));
let is_sat = not (Bdd.is_false bdd) in
if is_sat then
Numeric (collect true bdd)
else if Bdd.is_false bdd2 then
Boolean expr2
else
(* try to simplify the formula associated to bdd by projet *)
let s1 = Bdd.list_of_support (Bdd.support bdd1)
and s2 = Bdd.list_of_support (Bdd.support bdd2) in
let non_contributing_var = List.rev_append (lminus s1 s2)(lminus s2 s1) in
let non_contributing_var = Bdd.support_of_list non_contributing_var in
let bdd1 = Bdd.exist_local non_contributing_var bdd1
and bdd2 = Bdd.exist_local non_contributing_var bdd2 in
assert (not(Bdd.is_false bdd1));
assert (not(Bdd.is_false bdd2));
assert (Bdd.is_false (Bdd.dand bdd1 bdd2));
Boolean (Expr.Op(Expr.And, [collect false bdd1; collect false bdd2]))
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: failure.ml
** Main author: jahier@imag.fr
*)
type info =
| Boolean of Expr.t
| Numeric of Expr.t
(* Try to explain why a constraint is not satisfiable. It can be due
to:
- a pure Boolean reason, in which case we provide a (minimal)
expression representing the list of monomes that makes it false);
- Or there do exist Boolean solution, but there do not hold to
satisfiable numeric constraint, in which case we provide an
expression representing the list of monomes that makes its true *)
(* [get_info bdd bdd1 (bdd2,e2)] tries to explain as concisely as
possible why bdd is false
hyp: bdd=bdd1^bdd2=false ; bdd2=to_bdd(e2).
*)
val get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> info
......@@ -31,7 +31,7 @@ let (print_src : Event.t -> unit) =
fun e ->
match e.kind with
| Node { port = Exit(_,_,src) }
| Node { port = Fail(_,_,src) } ->
| Node { port = Fail(_,_,src,_) } ->
List.iter print_src_info (src())
|_ -> ();;
......@@ -39,14 +39,14 @@ let (print_cstr : Event.t -> unit) =
fun e ->
match e.kind with
| Node { port = Exit(cstr,_,_) }
| Node { port = Fail(cstr,_,_) } ->
| Node { port = Fail(cstr,_,_,_) } ->
print_string (" \"" ^cstr ^ "\"")
|_ -> ();;
let (port2str: Event.port -> string) =
function
| Exit (_,_,_)-> "exit"
| Fail (_,_,_) -> "fail"
| Fail (_,_,_,_) -> "fail"
| Call -> "call"
let print_event (e:t) =
......@@ -139,7 +139,7 @@ let rec (next_line : Event.t -> string -> int -> Event.t) =
let the_line e =
match e.kind with
| Node { port = Exit(_,_,src)}
| Node { port = Fail(_,_,src)} ->
| Node { port = Fail(_,_,src,_)} ->
List.exists
(fun si ->
Filename.basename si.file = f &&
......@@ -169,7 +169,7 @@ let (break_matches : Event.t -> string -> bool) =
| (Ltop),_ -> false
| Node _, [] -> false
| Node { port = Call}, _ -> false
| Node { name=name; port = Fail(_,_,src)}, str::tail
| Node { name=name; port = Fail(_,_,src,_)}, str::tail
| Node { name=name; port = Exit(_,_,src)}, str::tail ->
if Sys.file_exists str then
match tail with
......@@ -243,7 +243,7 @@ let (prof_add: Event.t -> unit) =
fun e ->
match e.kind with
| Node { port = Exit(_,_,src) }
| Node { port = Fail(_,_,src) } ->
| Node { port = Fail(_,_,src,_) } ->
List.iter incr_prof (src())
| _ -> ()
......@@ -362,3 +362,20 @@ let (goto : Event.t -> int -> Event.t) =
Event.set_nb e.nb;
rev_cond e (fun e -> e.nb = i)
let (explain_failure : Event.t -> unit) =
fun e ->
match e.kind with
| Node { port = Fail(_,cstr,src,li) } -> (
let expr = match li () with
| Failure.Numeric expr -> expr
| Failure.Boolean expr -> expr
in
print_string "\n\nThe current constraint is unsatisfiable:\n";
Expr.dump cstr;
print_string "\nBecause this one is unsatisfiable:\n";
Expr.dump expr;
flush stdout;
)
| _ -> print_string "Current Event is not a fail\n"
......@@ -95,3 +95,6 @@ val back : Event.t -> Event.t
(** go to event nb i (backward or forward) *)
val goto : Event.t -> int -> Event.t
(** Try to hint why the current constraint failed (at fail event) *)
val explain_failure : Event.t -> unit
......@@ -196,20 +196,20 @@ let lus_dumps ae = (
res
)
(*
let rec (to_event_exp : t -> Event.exp) =
(* *)
let rec (to_expr : t -> Expr.t) =
fun ae ->
match ae.ae_val with
AE_true -> Event.True
| AE_false -> Event.False
| AE_const str -> Event.Const str
| AE_iconst i -> Event.Const i
| AE_rconst i -> Event.Const i
| AE_ival i -> Event.Ival i
| AE_rval r -> Event.Fval r
| AE_support s -> Event.var s
| AE_pre s -> pr "pre "; pr (CoIdent.to_string s)
| AE_alias s -> Event.var (CoIdent.to_string s)
| AE_external_call (s, _, _,args)
| AE_call (s, args) ->
*)
AE_true -> Expr.True
| AE_false -> Expr.False
| AE_const str -> assert false
| AE_iconst i -> Expr.Ival (Num.num_of_string i)
| AE_rconst r -> Expr.Fval (float_of_string r)
| AE_ival i -> Expr.Ival (Num.num_of_int i)
| AE_rval r -> Expr.Fval r
| AE_support s -> Expr.Var s
| AE_alias s -> Expr.Var (CoIdent.to_string s)
| AE_pre s -> assert false (* pr "pre "; pr (CoIdent.to_string s) *)
| AE_external_call (s, _, _,args) -> assert false
| AE_call (s, args) -> assert false
......@@ -322,6 +322,7 @@ type solutions = (Var.env_out * Var.env_loc) list
type guard = {
g_form : Exp.formula;
mutable g_sol : solutions option;
mutable g_bdd : Bdd.t option;
g_src : CoIdent.src_stack list
}
......@@ -331,7 +332,7 @@ let (guard_to_string : guard -> string) =
fun g ->
rm_ctrl_nt(Exp.formula_to_string g.g_form)
let empty_guard = {g_form = Exp.True; g_sol = None; g_src=[] }
let empty_guard = {g_form = Exp.True; g_sol = None; g_bdd=None; g_src=[] }
let ws = Str.regexp "[ \t\n]+"
let string_of_guard g = (
......@@ -419,10 +420,10 @@ let find_some_sols
= match g.g_sol with
| Some s -> s
| None ->
let zesol = (
let zesol,bdd = (
let solver_vl = ref 0 in
Verbose.exe ~flag:dbg (fun _ -> solver_vl := 3);
let is_bool_sat = Solver.is_satisfiable
let is_bool_sat,bdd = Solver.is_satisfiable_bdd
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl *)
......@@ -432,7 +433,7 @@ let find_some_sols
"LutExe.is_bool_sat" (* msg: string (?) *)
in
if not is_bool_sat then (
[]
[],bdd
) else (
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
......@@ -447,10 +448,11 @@ let find_some_sols
it.num_vars_to_gen (* num_vars_to_gen: var list *)
g.g_form (* f: formula *)
in
sols
sols,bdd
)
) in (
g.g_sol <- Some zesol;
g.g_bdd <- Some bdd;
zesol
)
......@@ -553,6 +555,7 @@ let add_to_guard_nc it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info)
{
g_form = nf;
g_sol = None;
g_bdd = None;
g_src = if snd si = [] then acc.g_src else (snd si)::acc.g_src
}
......@@ -1475,7 +1478,16 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
let lazy_si () = List.map to_src_info (
if snd si = [] then acc.g_src else (snd si)::acc.g_src)
in
let cstr = Exp.to_event_formula new_acc.g_form in
let lazy_ci = fun () ->
let cc = add_to_guard_nc it data ae empty_guard si in
ignore (check_satisfiablity it cc);
let bdd = match new_acc.g_bdd with None -> assert false | Some bdd -> bdd in
let bdd_cc = match cc.g_bdd with None -> assert false | Some bdd -> bdd in
let bdd_acc = match acc.g_bdd with None -> assert false | Some bdd -> bdd in
let expr_cc = Exp.to_expr cc.g_form in
Failure.get_info bdd bdd_acc (expr_cc, bdd_cc)
in
let cstr = Exp.to_expr new_acc.g_form in
let event =
{
Event.step = ctx.Event.ctx_step;
......@@ -1486,7 +1498,7 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
{
Event.lang = "lutin";
Event.name = ctx.Event.ctx_name;
Event.port = Event.Fail (CoAlgExp.lus_dumps ae,cstr,lazy_si);
Event.port = Event.Fail (CoAlgExp.lus_dumps ae,cstr,lazy_si,lazy_ci);
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
};
......@@ -2175,7 +2187,7 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
in
let enb = Event.incr_nb (); Event.get_nb () in
let lazy_si () = List.map to_src_info zeguard.g_src in
let cstr = Exp.to_event_formula zeguard.g_form in
let cstr = Exp.to_expr zeguard.g_form in
let event =
{
Event.step = ctx.Event.ctx_step;
......@@ -2362,7 +2374,7 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
let edata = edata @ (get_sl (loc_var_list prog) locs) in
let enb = Event.incr_nb (); Event.get_nb () in
let lazy_si () = List.map to_src_info zeguard.g_src in
let cstr = Exp.to_event_formula zeguard.g_form in
let cstr = Exp.to_expr zeguard.g_form in
{
Event.step = ctx.Event.ctx_step;
Event.nb = enb;
......
......@@ -699,6 +699,10 @@ cp:
cp Lurettetop/ldbg_utils.ml $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/ldbg_utils.cmo $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/ldbg_utils.cmi $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/expr.cmo $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/expr.cmi $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/failure.cmo $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/failure.cmi $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/event.cmo $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/event.cmi $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/lexeme.cmi $(LIB_INSTALL_DIR) ;\
......
......@@ -180,23 +180,22 @@ let (build_sol_nb_table: var list -> Bdd.t -> Bdd.t -> unit) =
()
else
let rec skip_unconstraint_bool_var_at_top comb v =
(* [build_sol_nb_table] supposes that the bdd and its comb
have the same top var.
*)
if Bdd.is_true comb then comb
else
let topvar = (Bdd.topvar comb) in
if v = topvar then comb
else skip_unconstraint_bool_var_at_top (Bdd.dthen comb) v
(* [build_sol_nb_table] supposes that the bdd and its comb have
the same top var. *)
if Bdd.is_true comb then comb
else
let topvar = (Bdd.topvar comb) in
if v = topvar then comb
else skip_unconstraint_bool_var_at_top (Bdd.dthen comb) v
in
if Bdd.is_true bdd then
let _ = build_sol_nb_table_rec bdd comb (!snt_ref) in
()
else
let tvar = Bdd.topvar bdd in
let comb2 = skip_unconstraint_bool_var_at_top comb tvar in
let _ = build_sol_nb_table_rec bdd comb2 (!snt_ref) in
()
if Bdd.is_true bdd then
let _ = build_sol_nb_table_rec bdd comb (!snt_ref) in
()
else
let tvar = Bdd.topvar bdd in
let comb2 = skip_unconstraint_bool_var_at_top comb tvar in
let _ = build_sol_nb_table_rec bdd comb2 (!snt_ref) in
()
(****************************************************************************)
(****************************************************************************)
......
......@@ -414,42 +414,48 @@ let (weight_to_string : weight -> string) =
(****************************************************************************)
let (to_event_formula : formula -> Event.exp) =
let rec(flat_the_top_and : Expr.t -> Expr.t list) =
fun e ->
match e with
| Expr.Op(Expr.And, l) -> List.flatten (List.map flat_the_top_and l)
| _ -> [e]
let (to_expr : formula -> Expr.t) =
fun f ->
let op oper args = Event.Op(oper,args) in
let op oper args = Expr.Op(oper,args) in
let rec aux f = match f with
| And (f1, f2) -> op Event.And [aux f1; aux f2]
| Or (f1, f2) -> op Event.Or [aux f1; aux f2]
| Xor (f1, f2) -> op Event.Xor [aux f1; aux f2]
| Impl(f1, f2) -> op Event.Impl [aux f1; aux f2]
| IteB(c, f1, f2) -> op Event.Ite [aux c; aux f1; aux f2]
| Not (f) -> op Event.Not [aux f]
| EqB (f1, f2) -> op Event.Eq [aux f1; aux f2]
| True -> Event.True
| False -> Event.False
| Bvar var -> Event.Var (Var.name var)
| Eq (n1, n2) -> op Event.Eq [auxe n1; auxe n2]
| Sup (n1, n2) -> op Event.Sup [auxe n1; auxe n2]
| SupEq(n1, n2) -> op Event.SupEq [auxe n1; auxe n2]
| Inf (n1, n2) -> op Event.Inf [auxe n1; auxe n2]
| InfEq(n1, n2) -> op Event.InfEq [auxe n1; auxe n2]
| And (f1, f2) -> op Expr.And [aux f1; aux f2]
| Or (f1, f2) -> op Expr.Or [aux f1; aux f2]
| Xor (f1, f2) -> op Expr.Xor [aux f1; aux f2]
| Impl(f1, f2) -> op Expr.Impl [aux f1; aux f2]
| IteB(c, f1, f2) -> op Expr.Ite [aux c; aux f1; aux f2]
| Not (f) -> op Expr.Not [aux f]
| EqB (f1, f2) -> op Expr.Eq [aux f1; aux f2]