(*----------------------------------------------------------------------- ** Copyright (C) 2001 - Verimag. ** This file may only be copied under the terms of the GNU Library General ** Public License **----------------------------------------------------------------------- ** ** File: eval.ml ** Main author: jahier@imag.fr *) open Formula open Env_state open Wtree (****************************************************************************) let (lookup: env_in -> subst list -> var_name -> atomic_expr option) = fun input pre vn -> try Some(Hashtbl.find input vn) with Not_found -> try Some(List.assoc vn pre) with Not_found -> None (****************************************************************************) (****************************************************************************) let rec (eval : formula -> env_in -> formula) = (* ** [eval f input] returns an evaluated version of the formula f. Input ** variables (namely, sut outputs) as well as variables ``under a pre'' ** (in the environment memory) are replaced by their values. Then, ** the formula is simplified; e.g., `true and f' is simplified into `f'. *) fun f input -> match f with And(f1, f2) -> let ef1 = (eval f1 input) in if (ef1 = False) then False else let ef2 = (eval f2 input) in if ef1 = True then ef2 else if ef2 = False then False else if ef2 = True then ef1 else And(ef1, ef2) | Or(f1, f2) -> let ef1 = (eval f1 input) in if ef1 = True then True else let ef2 = (eval f2 input) in if ef1 = False then ef2 else if ef2 = True then True else if ef2 = False then ef1 else Or(ef1, ef2) | Not(f1) -> let ef1 = (eval f1 input) in if ef1 = True then False else if ef1 = False then True else Not(ef1) | True -> True | False -> False | Bvar(str) -> ( match (lookup input env_state.pre str) with Some(Bool(bool)) -> if bool then True else False | Some(_) -> print_string (str ^ " is not a boolean!\n"); assert false | None -> Bvar(str) ) | Eq(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> if (i1 = i2) then True else False | (Fval(f1), Fval(f2)) -> if (f1 = f2) then True else False | _ -> Eq(ee1, ee2) ) | Neq(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in Neq(ee1, ee2) ) | SupEq(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> if (i1 >= i2) then True else False | (Fval(f1), Fval(f2)) -> if (f1 >= f2) then True else False | _ -> SupEq(ee1, ee2) ) | Sup(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> if (i1 > i2) then True else False | (Fval(f1), Fval(f2)) -> if (f1 > f2) then True else False | _ -> Sup(ee1, ee2) ) | InfEq(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> if (i1 <= i2) then True else False | (Fval(f1), Fval(f2)) -> if (f1 <= f2) then True else False | _ -> InfEq(ee1, ee2) ) | Inf(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> if (i1 < i2) then True else False | (Fval(f1), Fval(f2)) -> if (f1 < f2) then True else False | _ -> Inf(ee1, ee2) ) and (eval_expr : expr -> env_in -> expr) = fun e input -> match e with Sum(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> Ival(i1+i2) | (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)+.f2) | (Fval(f1), Ival(i2)) -> Fval(f1+.float_of_int(i2)) | (Fval(f1), Fval(f2)) -> Fval(f1+.f2) | _ -> Sum(ee1, ee2) ) | Diff(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> Ival(i1-i2) | (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)-.f2) | (Fval(f1), Ival(i2)) -> Fval(f1-.float_of_int(i2)) | (Fval(f1), Fval(f2)) -> Fval(f1-.f2) | _ -> Diff(ee1, ee2) ) | Prod(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> Ival(i1*i2) | (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)*.f2) | (Fval(f1), Ival(i2)) -> Fval(f1*.float_of_int(i2)) | (Fval(f1), Fval(f2)) -> Fval(f1*.f2) | _ -> Prod(ee1, ee2) ) | Quot(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> Ival(i1/i2) | (Fval(f1), Fval(f2)) -> Fval(f1/.f2) | _ -> Quot(ee1, ee2) ) | Mod(e1, e2) -> ( let ee1 = eval_expr e1 input in let ee2 = eval_expr e2 input in match (ee1, ee2) with (Ival(i1), Ival(i2)) -> Ival(i1 mod i2) | (Fval(f1), Fval(f2)) -> Fval(mod_float f1 f2) | _ -> Mod(ee1, ee2) ) | Nvar(str) -> ( match (lookup input env_state.pre str) with Some(Int(i)) -> Ival(i) | Some(Float(f)) -> Fval(f) | Some(Bool(f)) -> print_string ((string_of_bool f) ^ "is a bool, not an int nor a float!\n"); assert false | None -> Nvar(str) ) | Ival(i) -> Ival(i) | Fval(f) -> Fval(f) (****************************************************************************) (****************************************************************************) let rec (eval_wtree_list: env_in -> wtree list -> node list list -> formula_table) = fun input wtl nfll -> (** Returns a table of formula appearing in `wtl'; the formula are evaluated w.r.t. `input'. `nfll' is the list of list of origin nodes corresponding to the trees in `wtl' (necessary to get formula associated to pair of nodes from env_state.formula_table). *) let ft = (Hashtbl.create (List.length wtl)) in (List.iter2 (eval_wtree input ft) wtl nfll); ft and (eval_wtree : env_in -> formula_table -> wtree -> node list -> unit) = fun input ft wt nl -> List.iter (eval_wnode input ft nl) wt and (eval_wnode : env_in -> formula_table -> node list -> wnode -> unit) = fun input ft nlf wn -> match wn with L(w, nlt) -> List.iter2 (add_formula input ft) nlf nlt | N(w, wt) -> (eval_wtree input ft wt nlf) and (add_formula : env_in -> formula_table -> node -> node -> unit) = fun input ft nf nt -> let f = Hashtbl.find env_state.formula_table (nf, nt) in let fe = eval f input in Hashtbl.add ft (nf, nt) fe (****************************************************************************) (****************************************************************************) (* exported *) let (expr_to_atomic: expr -> atomic_expr) = function Ival(i) -> Int(i) | Fval(f) -> Float(f) | _ -> assert false (* exported *) let (formula_to_atomic: formula -> atomic_expr) = function True -> Bool(true) | False -> Bool(false) | _ -> assert false (* exported *) let (update_pre: env_in -> env_out -> env_loc -> unit) = fun input output local -> let (update_one_pre_var : var_name -> subst) = fun pre_vn -> let vn = String.sub pre_vn 4 ((String.length pre_vn) -4) in let pre_value = try Hashtbl.find input vn with Not_found -> try List.assoc vn output with Not_found -> try List.assoc vn local with Not_found -> assert false in (pre_vn, pre_value) in env_state.pre <- List.map (update_one_pre_var) env_state.pre_var_names