From 93beaa37664f1a22f7ee4a224fd8a794cc89c27a Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 19 Apr 2021 10:23:34 +0200 Subject: [PATCH] Simplifying formulas in literals --- src/lib/frontend/cnf.ml | 7 +- src/lib/frontend/simple_reasoner_expr.ml | 531 ++++++++++++++-------- src/lib/frontend/simple_reasoner_expr.mli | 5 +- src/lib/reasoners/simplifiers.ml | 157 +++++-- 4 files changed, 445 insertions(+), 255 deletions(-) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index a7e71ee032..db148762b3 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -508,16 +508,19 @@ let make_form name f loc ~decl_kind = Util.SNo -> form | Util.SPreprocess | Util.SAll -> let module S = SimpExprPreproc () in + (*Format.printf "Simplifying@.";*) let smp_form = S.simp_expr form in - let () = + (* let () = (* Emptying the caches modified by the simplifier. St : This is necessary for having consistent results. *) Shostak.Combine.empty_cache (); - S.empty_caches () in + S.empty_caches (); () in *) if SRE.has_changed smp_form then + (*let () = Format.printf "Simplification over: success@." in*) let exp = SRE.get_expr smp_form in exp else begin + (*let () = Format.printf "Simplification over: fail@." in*) form end in diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index 8d559ed55f..c83ed389ab 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -64,8 +64,12 @@ type 'abs_val add_constraint_res = | AlreadyTrue (* The constraint is already true *) | AlreadyFalse (* The constraint is already false*) | NewConstraint of 'abs_val (* The new abstract value *) - -(** 2. Simplifyer *) +(* +let pp_add_constraint_res pp fmt = function + | AlreadyTrue -> Format.fprintf fmt "Already true" + | AlreadyFalse -> Format.fprintf fmt "Already false" + | NewConstraint v -> Format.fprintf fmt "New Constraint: %a" pp v *) + (** 2. Simplifyer *) (** As the simplifyer interacts with different components of alt-ergo, it is written to be as generic as possible. @@ -85,6 +89,8 @@ module type Dom = sig val _false : v val unknown : v + val to_bool : v -> bool option + (** (Partial) Compare function *) val compare : state -> state -> int option @@ -94,8 +100,7 @@ module type Dom = sig (** Add constraint *) val add_constraint : - Expr.t -> - Expr.t -> + Expr.t list -> Symbols.lit -> state -> state add_constraint_res @@ -128,17 +133,12 @@ module SimpleReasoner type state = D.state type v = D.v - let (simp_cache : (state * (Expr.t, v) simp) list Expr.Map.t ref) = + let (simp_cache : (state * (state * (Expr.t, v) simp)) list Expr.Map.t ref) = ref E.Map.empty let constraint_cache : (state * state add_constraint_res) list E.Map.t ref = ref E.Map.empty - - let empty_caches () = - simp_cache := E.Map.empty; - constraint_cache := E.Map.empty - let add_cache cache exp state smp = let c = !cache in cache := @@ -161,65 +161,140 @@ module SimpleReasoner let pp_simp = pp_simp D.pp_v - let identity v exp = {exp; diff = false; v = D.eval_expr exp v} + let identity s exp = {exp; diff = false; v = D.eval_expr exp s} let simp_true = {exp = E.vrai; diff = true; v = D._true} let simp_false = {exp = E.faux; diff = true; v = D._false} let is_true e = E.equal e.exp E.vrai let is_false e = E.equal e.exp E.faux + let bool_unknown = D.v_join D._true D._false + - let rec add_lit_constraint_no_cache (state : state) (e : Expr.t) = - let exception Stop of state add_constraint_res in + let rec add_lit_constraint (state : state) (e : Expr.t) + : state * (Expr.t, v) simp = + let exception Stop in match E.lit_view e with | Eq (e1, e2) -> - debug "[add_lit_constraint] Eq@."; - D.add_constraint e1 e2 Sy.L_eq state - + begin + debug "[add_lit_constraint] Eq@."; + let _, e1 = simp_expr state e1 in + let _, e2 = simp_expr state e2 in + match D.add_constraint [e1.exp; e2.exp] Sy.L_eq state with + | AlreadyTrue -> state, simp_true + | AlreadyFalse -> state, simp_false + | NewConstraint s -> + s, + if e1.diff || e2.diff then + {exp = E.mk_eq ~iff:false e1.exp e2.exp; diff = true; v = bool_unknown} + else + {exp = e; diff = false; v = bool_unknown} + end | Eql [] -> assert false - | Eql (hd :: tl) -> begin try + | Eql (hd :: tl) -> + begin + try debug "[add_lit_constraint] Eql@."; - NewConstraint ( + let _, hd = simp_expr state hd in + let state, tl = List.fold_left - (fun s e -> - match D.add_constraint hd e Sy.L_eq s with - | AlreadyTrue -> s - | AlreadyFalse -> raise (Stop AlreadyFalse) - | NewConstraint s' -> s' - ) state tl - ) - with Stop res -> res + (fun (state, e_list) e -> + let _, e = simp_expr state e in + match D.add_constraint [hd.exp; e.exp] Sy.L_eq state with + | AlreadyTrue -> state, e_list + | AlreadyFalse -> raise Stop + | NewConstraint s' -> s', e :: e_list + ) (state, []) tl in + match tl with + | [] -> (* No more elements to add to equality *) + state, simp_true + | [elt] -> (* Still one equality *) + state, {exp = E.mk_eq ~iff:false hd.exp elt.exp; diff = true; v = bool_unknown} + | _ -> (* Still some *) + let has_changed = + let length = ref 0 in + List.exists (fun e -> length := !length + 1; e.diff) tl + || !length + 1 <> List.length tl in + if has_changed then + let exp = + List.fold_left + (fun acc e -> E.mk_eq ~iff:false e.exp acc) + hd.exp + tl in + state, {exp; diff = true; v = bool_unknown} + else + state, {exp = e; diff = false; v = bool_unknown} + with Stop -> + state, simp_false end | Distinct [] -> assert false - | Distinct (hd :: tl) -> begin try + | Distinct (hd :: tl) -> + begin + try debug "[add_lit_constraint] Distinct@."; - NewConstraint ( + let _, hd = simp_expr state hd in + let state, tl = List.fold_left - (fun s e -> - match D.add_constraint hd e Sy.L_neg_eq s with - | AlreadyTrue -> s - | AlreadyFalse -> raise (Stop AlreadyFalse) - | NewConstraint s' -> s') state tl) - with Stop res -> res + (fun (state, e_list) e -> + let _, e = simp_expr state e in + match D.add_constraint [hd.exp; e.exp] Sy.L_neg_eq state with + | AlreadyTrue -> state, e_list + | AlreadyFalse -> raise Stop + | NewConstraint s' -> s', e :: e_list + ) (state, []) tl in + match tl with + | [] -> (* No more elements to add to equality *) + state, simp_true + | _ -> (* Still some *) + let has_changed = + let length = ref 0 in + List.exists (fun e -> length := !length + 1; e.diff) tl + || !length + 1 <> List.length tl in + if has_changed then + let exp = + E.mk_distinct + ~iff:false + (List.map (fun e -> e.exp) (hd :: List.rev tl)) + in + state, {exp; diff = true; v = bool_unknown} + else + state, {exp = e; diff = false; v = bool_unknown} + with Stop -> + state, simp_false end - | Builtin (_, btin, [e1; e2]) -> begin + | Builtin (is_pos, btin, l) -> begin debug "[add_lit_constraint] Builtin@."; - match D.add_constraint e1 e2 (Sy.L_built btin) state with + let l' = List.map (fun e -> snd @@ simp_expr state e) l in + let l_exp = List.map (fun e -> e.exp) l' in + match + D.add_constraint + l_exp + (if is_pos then Sy.L_built btin else Sy.L_neg_built btin) + state + with | AlreadyTrue -> debug "[add_lit_constraint] Already true@."; - AlreadyTrue + state, simp_true | AlreadyFalse -> debug "[add_lit_constraint] Already false@."; - AlreadyFalse + state, simp_false | NewConstraint s' -> debug "[add_lit_constraint] New constraint: %a@." D.pp s'; - NewConstraint s' + let has_changed = + let length = ref 0 in + List.exists (fun e -> length := !length + 1; e.diff) l' + || !length <> List.length l in + let exp = + if has_changed + then E.mk_builtin ~is_pos btin l_exp + else e in + s', {exp; diff = has_changed; v = bool_unknown} end - | Builtin (_, _, _) -> failwith "Unhandled builtin" - | Pred _ -> - debug "[add_lit_constraint] Pred@."; - NewConstraint state + | Pred (e', b) -> (* todo: rebuild an equivalent simplified expression *) + debug "[add_lit_constraint] Pred %a (%b) (not handled yet)@." E.print e b; + D.add_raw_value e' (if b then D._false else D._true) state, + {exp = e; diff = false; v = bool_unknown} | Not_a_lit {is_form} -> debug "[add_lit_constraint] Not a lit@."; if is_form then @@ -227,68 +302,93 @@ module SimpleReasoner else failwith "add_lit_constraint should be only called on litterals or formulas" - +(* and add_lit_constraint (state : state) (e : Expr.t) = match find_cache constraint_cache e state with | None -> let res = add_lit_constraint_no_cache state e in + debug "[add_lit_constraint] Adding constraint to %a : %a@." + E.print e (pp_add_constraint_res D.pp) res + ; add_cache constraint_cache e state res; res | Some (_, res) -> res +*) and (&&&) v e = - add_form_constraint v e + let state, res = add_form_constraint v e in + if is_true res then AlreadyTrue + else if is_false res then AlreadyFalse + else NewConstraint (state, res) - and add_form_view_constraint state = function - | E.Unit (e1, e2) -> begin + and add_form_constraint state e = + match E.form_view e with + | E.Unit (e1, e2) -> + begin debug "[add_form_constraint] Unit@."; match state &&& e1 with - | AlreadyTrue -> state &&& e2 - | AlreadyFalse -> AlreadyFalse - | NewConstraint state -> state &&& e2 + | AlreadyTrue -> add_form_constraint state e2 + | AlreadyFalse -> state, simp_false + | NewConstraint (state', e1') -> + match state' &&& e2 with + | AlreadyTrue -> state', e1' + | AlreadyFalse -> state, simp_false + | NewConstraint (state'', e2') -> + let diff = e1'.diff || e2'.diff in + let exp = if diff then E.mk_and e1'.exp e2'.exp false (-45) else e in + state'', {exp; diff; v = bool_unknown} end | Clause (e1, e2, _) -> begin debug "[add_form_constraint] Clause@."; match state &&& e1 with - | AlreadyTrue -> AlreadyTrue - | AlreadyFalse -> state &&& e2 - | NewConstraint state1 -> begin + | AlreadyTrue -> state, simp_true + | AlreadyFalse -> add_form_constraint state e2 + | NewConstraint (state1, e1') -> begin match state &&& e2 with - | AlreadyTrue -> AlreadyTrue - | AlreadyFalse -> AlreadyFalse - | NewConstraint state2 -> - NewConstraint (D.join state1 state2) + | AlreadyTrue -> state, simp_true + | AlreadyFalse -> state1, e1' + | NewConstraint (state2, e2') -> + let diff = e1'.diff || e2'.diff in + let exp = if diff then E.mk_and e1'.exp e2'.exp false (-46) else e in + D.join state1 state2, {exp; diff; v = bool_unknown} end end | Iff (e1, e2) -> begin (* = (e1 /\ e2) \/ (~e1 /\ ~e2) *) debug "[add_form_constraint] Iff@."; let c1 = state &&& e1 in (* Constraint on e1 *) match c1 with - | AlreadyTrue -> (* e1 is true *) state &&& e2 - | AlreadyFalse -> (* e1 is false *) state &&& E.neg e2 - | NewConstraint s1 -> begin - let nc1 = state &&& E.neg e1 in (* Constraint on ~e1 *) + | AlreadyTrue -> (* e1 is true *) add_form_constraint state e2 + | AlreadyFalse -> (* e1 is false *) add_form_constraint state (E.neg e2) + | NewConstraint (s1, e1') -> begin + let nc1 = state &&& E.neg e1'.exp in (* Constraint on ~e1 *) match nc1 with | AlreadyTrue -> (* e1 is false *) - state &&& E.neg e2 + add_form_constraint state (E.neg e2) | AlreadyFalse -> (* e1 is true *) - state &&& e2 - | NewConstraint ns1 -> + add_form_constraint state e2 + | NewConstraint (ns1, ne1') -> let c2 = s1 &&& e2 in (* Constraint on (e1 /\ e2) *) match c2 with - | AlreadyTrue -> (* (e1 /\ e2) is true *) - AlreadyTrue - | AlreadyFalse -> (* (e1 /\ e2) is false *) - ns1 &&& E.neg e2 - | NewConstraint s2 -> - let nc2 = ns1 &&& E.neg e2 in (* Constraint on (~e1 /\ ~e2) *) + | AlreadyTrue -> (* e2 is true *) + s1, e1' + | AlreadyFalse -> (* e2 is false *) + add_form_constraint ns1 (E.neg e2) + | NewConstraint (s2, e2') -> + let nc2 = ns1 &&& E.neg e2'.exp in (* Constraint on (~e1 /\ ~e2) *) match nc2 with - | AlreadyTrue -> (* (~e1 /\ ~e2) is true *) - AlreadyTrue - | AlreadyFalse -> (* (~e1 /\ ~e2) is false *) - c2 - | NewConstraint ns2 -> - NewConstraint (D.join s2 ns2) + | AlreadyTrue -> (* e2 is false *) + ns1, ne1' + | AlreadyFalse -> (* e2 is true *) + s1, e1' + | NewConstraint (ns2, _ne2') -> + D.join ns2 s2, (* Joining environments for s1 /\ s2 and ~s1 /\ ~s2 *) + let diff = e1'.diff || e2'.diff in + let exp = if diff then E.mk_iff e1'.exp e2'.exp (-47) else e in + { + exp; + diff; + v = bool_unknown + } end end | Xor (e1, e2) -> begin (* (e1 /\ ~e2) \/ (~e1 /\ e2) *) @@ -296,98 +396,98 @@ module SimpleReasoner let c1 = state &&& e1 in (* Constraint on e1 *) match c1 with | AlreadyTrue -> (* e1 is true *) - state &&& E.neg e2 + add_form_constraint state (E.neg e2) | AlreadyFalse -> (* e1 is false *) - state &&& e2 - | (NewConstraint s1) as c1 -> + add_form_constraint state e2 + | NewConstraint (s1, e1') -> let c2 = state &&& e2 in (* Constraint on e2 *) match c2 with | AlreadyTrue -> (* e2 is true *) - state &&& E.neg e1 + add_form_constraint state (E.neg e1) | AlreadyFalse -> (* e2 is false *) - c1 - | NewConstraint s2 -> (* State for e2 *) + s1, e1' + | NewConstraint (s2, e2') -> (* State for e2 *) let nc1 = s1 &&& E.neg e2 in (* Constraint on (e1 /\ ~e2) *) match nc1 with - | AlreadyTrue -> (* (e1 /\ ~e2) is true *) - AlreadyTrue - | AlreadyFalse -> (* (e1 /\ ~e2) is false *) - s2 &&& E.neg e1 - | NewConstraint ns1 -> + | AlreadyTrue -> (* e2 is false *) + s1, e1' + | AlreadyFalse -> (* e2 is true *) + add_form_constraint state (E.neg e1) + | NewConstraint (ns2, ne2') -> let nc2 = s2 &&& E.neg e1 in (* Constraint on (e2 /\ ~e1) *) match nc2 with - | AlreadyTrue -> (* (e2 /\ ~e1) is true *) - AlreadyTrue - | AlreadyFalse -> (* (e2 /\ ~e1) is false *) - nc1 - | NewConstraint ns2 -> NewConstraint (D.join ns1 ns2) + | AlreadyTrue -> (* e1 is false *) + s2, e2' + | AlreadyFalse -> (* e1 is true *) + ns2, ne2' + | NewConstraint (ns1, _ne1') -> + let diff = e1'.diff || e2'.diff in + let exp = if diff then E.mk_iff e1'.exp e2'.exp (-48) else e in + D.join ns1 ns2, + { + exp; + diff; + v = bool_unknown + } end - | Literal e -> - debug "[add_form_constraint] Litteral@."; + | Literal _ -> + debug "[add_form_constraint] Litteral %a@." E.print e; add_lit_constraint state e | Let _ -> debug "[add_form_constraint] Let binding: TODO@."; - NewConstraint state + state, identity state e | Lemma _ | Skolem _ -> debug "[add_form_constraint] Lemma/Skolem: not using it@."; - NewConstraint state + state, identity state e | Not_a_form -> failwith "add_form_constraint should be only called on litterals or formulas" - and add_form_constraint state e = - match find_cache constraint_cache e state with - | None -> - let res = add_form_view_constraint state (E.form_view e) in - add_cache constraint_cache e state res; - res - | Some (_, res) -> res - and simp_ite (state : state) (cond : E.t) (th : E.t) (el : E.t) : - (E.t, v) simp list = + state * (E.t, v) simp list = debug "[simp_ite] Simplifying condition %a with %a@." E.print cond D.pp state; - let scond = simp_expr state cond in + let _state_th, scond = simp_expr state cond in debug "[simp_ite] New condition %a ~~> %a@." E.print cond E.print scond.exp; if is_true scond then begin - debug "[simp_ite] It is true, ending@."; - let th : (E.t, v) simp = simp_expr state th in - [{th with diff = true}] + debug "[simp_ite] It is true, simplifying 'then' branch@."; + let state, th = simp_expr state th in + state, [{th with diff = true}] end else if is_false scond then begin - debug "[simp_ite] It is false, ending@."; - let el : (E.t, v) simp = simp_expr state el in - [{el with diff = true}] + debug "[simp_ite] It is false, simplifying 'else' branch@."; + let state, el = simp_expr state el in + state, [{el with diff = true}] end else begin (* Evaluating the condition *) let neg_cond = E.neg scond.exp in (* todo: split add constraint *) match state &&& scond.exp, state &&& neg_cond with - | AlreadyTrue, AlreadyTrue - | AlreadyFalse, AlreadyFalse -> - failwith "Both the condition and its negation are true/false" + | AlreadyFalse, AlreadyFalse + | AlreadyTrue, AlreadyTrue -> assert false | AlreadyFalse, _ | _, AlreadyTrue -> debug "[simp_ite] Negation is true, ending@."; - let el : (E.t, v) simp = simp_expr state el in - [{el with diff = true}] - | _, AlreadyFalse - | AlreadyTrue, _ -> - debug "[simp_ite] Negation is false, ending@."; - let th : (E.t, v) simp = simp_expr state th in - [{th with diff = true}] - | NewConstraint cth, NewConstraint cel -> - debug "[simp_ite] Cannot conclude, simplifying branches@."; - let sth : (E.t, v) simp = simp_expr cth th in - let sel : (E.t, v) simp = simp_expr cel el in - [scond; sth; sel] + let _, el = simp_expr state el in + state, [{el with diff = true}] + | AlreadyTrue, _ + | _, AlreadyFalse -> + let _, th = simp_expr state th in + state, [{th with diff = true}] + | NewConstraint (state_th, _), NewConstraint (state_el, _) -> + debug "[simp_ite] Cannot conclude, simplifying branches.@."; + debug "[simp_ite] Branch then %a with state %a.@." E.print th D.pp state_th; + debug "[simp_ite] Branch else %a with state %a.@." E.print el D.pp state_el; + let sth, th = simp_expr state_th th in + let sel, el = simp_expr state_el el in + D.join sth sel, [scond; th; el] end and simp_form @@ -400,10 +500,10 @@ module SimpleReasoner let () = debug "[simp_form] F_Unit@." in let _state,rev_res = fold_left_stop - (fun (state, simp_exps) e -> + (fun (acc_state, simp_exps) e -> debug "[simp_form] Simplifying %a in F_Unit@." E.print e; - let esimp : (E.t, v) simp = simp_expr state e in + let new_state, esimp = simp_expr acc_state e in debug "[simp_form] Simplified %a into %a in F_Unit@." E.print e pp_simp esimp; if is_false esimp then ( @@ -412,15 +512,11 @@ module SimpleReasoner ) else if is_true esimp then ( debug "[simp_form] %a = true@." E.print e; - (state, simp_exps), false + (new_state, simp_exps), false ) else ( debug "[simp_form] Keeping %a@." E.print e; - match state &&& esimp.exp with - | AlreadyTrue - | AlreadyFalse -> failwith "Should have simplify beforehand" - | NewConstraint state -> - (state, (esimp :: simp_exps))) + (new_state, (esimp :: simp_exps))) , false ) (state, []) @@ -440,7 +536,7 @@ module SimpleReasoner (fun (state, simp_exps) e -> debug "[simp_form] Simplifying %a in clause@." E.print e; - let (esimp : (E.t, v) simp) = simp_expr state e in + let _, esimp = simp_expr state e in debug "[simp_form] Simplified %a into %a in clause@." E.print e pp_simp esimp; if is_false esimp then ( @@ -468,38 +564,41 @@ module SimpleReasoner let () = debug "[simp_form] No additional simplification@." in List.map (identity state) elist - and simp_expr_no_cache state (e : E.t) : (E.t, v) simp = + and simp_expr_no_cache (state : state) (e : E.t) : state * (E.t, v) simp = debug "[simp_expr] Simplifying expression %a with %a@." E.print e D.pp state; - let res = + let new_state, res = let ty = E.type_info e in let elist = E.get_sub_expr e in let symb = E.get_symb e in match symb, elist with | Op Tite, [cond; th; el] -> begin debug "[simp_expr] Ite@."; - let simp = simp_ite state cond th el in + let _, simp = simp_ite state cond th el in debug "[simp_expr] Ite treated@."; match simp with | [branch] -> debug "[simp_expr] Simplification cut a branch, yielding %a@." Expr.print branch.exp; - branch + state, branch | [cond; th; el] -> if cond.diff || th.diff || el.diff then (* If by any luck, th == el... *) if Expr.equal th.exp el.exp then begin (* bingo *) debug "[simp_expr] Both branches are equal @."; - {th with diff = true} + state, {th with diff = true} end else begin (* A simplification has been made *) - debug "[simp_expr] Simplification worked on a branch@."; { + debug "[simp_expr] Simplification worked on a branch@."; + state, + { exp = E.mk_term (Op Tite) [cond.exp; th.exp; el.exp] ty; diff = true; v = D.v_join th.v el.v } end else begin debug "[simp_expr] Simplification failed@."; + state, { (* Simplification failed *) exp = e; diff = false; @@ -510,6 +609,7 @@ module SimpleReasoner | Op Tite, _ -> assert false | Symbols.Form (F_Skolem | F_Lemma), _ -> debug "[simp_expr] Skolem/Lemmas not simplified"; + state, { exp = e; diff = false; @@ -530,108 +630,135 @@ module SimpleReasoner | F_Iff -> E.mk_iff | F_Xor -> E.mk_xor | F_Skolem | F_Lemma -> assert false) in + state, List.fold_left (fun sexp term -> {sexp with exp = make sexp.exp term.exp (-44)}) hd tl end - else { - exp = e; - diff = false; - v = D.unknown - } + else + state, + { + exp = e; + diff = false; + v = D.unknown + } end | Symbols.Lit _, _ -> begin debug "[simp_expr] Litteral : %a@." Symbols.print symb; - match add_lit_constraint state e with + match state &&& e with | AlreadyTrue -> debug "[simp_expr] Litteral %a is true@." E.print e; - simp_true + state, simp_true | AlreadyFalse -> debug "[simp_expr] Litteral %a is false@." E.print e; - simp_false - | NewConstraint state -> { - exp = e; - diff = false; - v = D.eval_expr e state - } + state, simp_false + | NewConstraint state_and_exp -> + state_and_exp end | Symbols.Let, [] -> begin match Expr.form_view e with | E.Let {let_v; let_e; in_e; let_sko = _; is_bool = _} -> debug "[simp_expr] Let@."; let v_exp = E.mk_term let_v [] (E.type_info let_e) in - let simp_let = simp_expr state let_e in - let state = D.add_raw_value v_exp simp_let.v state in - let simp_in = simp_expr state in_e in + let _, simp_let = simp_expr state let_e in + let state' = D.add_raw_value v_exp simp_let.v state in + let _, simp_in = simp_expr state' in_e in let diff = simp_let.diff || simp_in.diff in let exp = if diff then E.mk_let let_v simp_let.exp simp_in.exp (-43) else e - in {exp; diff; v = simp_in.v} + in state, {exp; diff; v = simp_in.v} | _ -> assert false end | Symbols.Let, _ -> assert false + | Symbols.Name _, _ -> + begin + debug "[simp_expr] Name@."; + state, + match D.to_bool (D.eval_expr e state) with + | Some true -> simp_true + | Some false -> simp_false + | None -> identity state e + end | _ -> debug "[simp_expr] Other: %a@." Symbols.print symb; - let (l : (E.t, v) simp list) = List.map (simp_expr state) elist in - if List.exists (fun e -> e.diff) l then { - exp = E.mk_term symb (List.map (fun e -> e.exp) l) ty; - diff = true; - v = D.eval_expr e state - } - else {exp = e; diff = false; v = D.eval_expr e state} + let l = List.map (simp_expr state) elist in + if List.exists (fun (_, e) -> e.diff) l then + state, + { + exp = E.mk_term symb (List.map (fun (_, e) -> e.exp) l) ty; + diff = true; + v = D.eval_expr e state + } + else + state, + { + exp = e; + diff = false; + v = D.eval_expr e state + } in debug "[simp_expr] Simplification ENDED.@."; debug "[simp_expr] Old : %a@." E.print e; debug "[simp_expr] Result : %a@." pp_simp res; - res + debug "[simp_expr] New state : %a@." D.pp new_state; + new_state, res - and simp_expr state (e : E.t) : (E.t, v) simp = + and simp_expr state (e : E.t) : state * (E.t, v) simp = match find_cache simp_cache e state with | None -> debug "[simp_expr] Expression %a never simplified@." E.print e; - let res = simp_expr_no_cache state e in - add_cache simp_cache e state res; - res - | Some (_, se) -> - debug "[simp_expr] Expression %a already simplified by %a@." - E.print e pp_simp se; - se + let state', res = simp_expr_no_cache state e in + add_cache simp_cache e state (state', res); + state', res + | Some (_, (state, se)) -> + debug "[simp_expr] Expression %a already simplified by %a -- %a@." + E.print e pp_simp se D.pp state; + state, se + + let last_state = ref D.top (** Wrapper of simp_expr for verbose *) - let simp_expr e = - try - debug "START Simplifying %a@." E.print e; - let res = simp_expr D.top e in - if res.diff - then - let () = - debug - "Old expression = %a@." - E.print e; - debug - "New expression = %a@." - E.print res.exp in - res - else - let () = - debug - "No change on %a@." - E.print e in + let simp_expr = + fun e -> + try + debug "START Simplifying %a@." E.print e; + let new_state, res = simp_expr !last_state e in + last_state := new_state; + if res.diff + then + let () = + debug + "Old expression = %a@." + E.print e; + debug + "New expression = %a@." + E.print res.exp in + res + else + let () = + debug + "No change on %a@." + E.print e in + identity D.top e + with + Failure s -> + debug + "Error while simplifying %a\n%s\n\ + I will continue with the initial expression@." + E.print e + s; identity D.top e - with - Failure s -> - debug - "Error while simplifying %a\n%s\n\ - I will continue with the initial expression@." - E.print e - s; - identity D.top e + + let empty_caches () = + simp_cache := E.Map.empty; + constraint_cache := E.Map.empty; + last_state := D.top end diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli index a6a36dee5f..88cae94616 100644 --- a/src/lib/frontend/simple_reasoner_expr.mli +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -42,6 +42,8 @@ module type Dom = sig val _false : v val unknown : v + val to_bool : v -> bool option + (** (Partial) Compare function *) val compare : state -> state -> int option @@ -51,8 +53,7 @@ module type Dom = sig (** Add constraint *) val add_constraint : - Expr.t -> - Expr.t -> + Expr.t list -> Symbols.lit -> state -> state add_constraint_res diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index 9f8d3368c7..c634f88bea 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -41,11 +41,12 @@ module DummySimp = let bottom = () let compare _ _ = Some 0 let join _ _ = () - let add_constraint _ _ _ _ = SRE.NewConstraint () + let add_constraint _ _ _ = SRE.NewConstraint () let pp fmt _ = Format.fprintf fmt "()" let unknown = () let _false = () let _true = () + let to_bool _ = None let pp_v fmt _ = Format.fprintf fmt "()" let eval_expr _ _ = () let v_join _ _ = () @@ -73,21 +74,49 @@ let compare_abs_val cmp v1 v2 = | _, Bottom -> Some 1 | Value v1, Value v2 -> cmp v1 v2 +type abstract_bool = + | True + | False + | TrueOrFalse + +let pp_abstract_bool fmt = function + | True -> Format.fprintf fmt "{t}" + | False -> Format.fprintf fmt "{f}" + | TrueOrFalse -> Format.fprintf fmt "{t;f}" + + +type interval = + | Bool of bool + | Interval of Intervals.t + +let pp_interval fmt = function + | Interval i -> Intervals.print fmt i + | Bool b -> Format.fprintf fmt "%b" b + module IntervalsDomain : SRE.Dom - with type v = Intervals.t abstract_value - and type state = Intervals.t abstract_value M.t abstract_value = struct - type v = Intervals.t abstract_value + with type v = interval abstract_value + and type state = interval abstract_value M.t abstract_value = struct + type v = interval abstract_value type state = v M.t abstract_value let top = Top let bottom = Bottom - let _false = Value (Intervals.point Q.zero Ty.Tbool Explanation.empty) - let _true = Value (Intervals.point Q.one Ty.Tbool Explanation.empty) + let _false = Value (Bool false) + let _true = Value (Bool true) let unknown = Top - let pp_v = pp_abs_val Intervals.print + let to_bool = + function + | Top + | Bottom + | Value (Interval _) -> None + | Value (Bool b) -> Some b + + + let pp_v = pp_abs_val pp_interval + let pp fmt v = pp_abs_val (fun fmt -> M.iter @@ -98,14 +127,25 @@ module IntervalsDomain : fmt v + let compare_intervals_t i1 i2 = + if Intervals.contained_in i1 i2 + then if Intervals.equal i1 i2 + then Some 0 + else Some (-1) + else if Intervals.contained_in i2 i1 then Some 1 + else None + + let compare_bool b1 b2 = Some (Bool.compare b1 b2) + + let compare_intervals i1 i2 = + match i1, i2 with + | Interval i1, Interval i2 -> compare_intervals_t i1 i2 + | Bool b1, Bool b2 -> compare_bool b1 b2 + | Bool _, Interval _ -> Some 1 + | Interval _, Bool _ -> Some (-1) + let compare = - let compare_intervals = - compare_abs_val (fun i1 i2 -> - if Intervals.contained_in i1 i2 then - if Intervals.equal i1 i2 then Some 0 else Some (-1) - else if Intervals.contained_in i2 i1 then Some 1 - else None - ) in + let compare_intervals = compare_abs_val compare_intervals in fun m1 m2 -> (* Compares two maps. Maps are compared itetatively ; the result is saved on a reference @@ -160,7 +200,11 @@ module IntervalsDomain : | _, Top -> Top | v, Bottom | Bottom, v -> v - | Value v1, Value v2 -> Value (Intervals.merge v1 v2) + | Value (Interval v1), Value (Interval v2) -> Value (Interval (Intervals.merge v1 v2)) + | Value (Bool b1), Value (Bool b2) -> + if b1 = b2 then v1 else Top + | Value (Bool _), Value (Interval _) + | Value (Interval _), Value (Bool _) -> failwith "Cannot v_join boolean & integer" let join = M.merge @@ -183,40 +227,43 @@ module IntervalsDomain : let eval_constraint (ty : Ty.t) (s : state) - (p : P.t) : Intervals.t abstract_value = + (p : P.t) : interval abstract_value = match s with | Top -> begin match P.to_list p with - | [], q -> Value (Intervals.point q ty Explanation.empty) + | [], q -> Value (Interval (Intervals.point q ty Explanation.empty)) | _ -> Top end | Bottom -> Bottom | Value v -> let ty = P.type_info p in let module Ev = P.Eval (struct - type t = Intervals.t abstract_value - let one = Value (Intervals.point Q.one ty Explanation.empty) + type t = interval abstract_value + let one = Value (Interval (Intervals.point Q.one ty Explanation.empty)) let add i1 i2 = match i1, i2 with | Top, _ | _, Top -> Top | Bottom, _ | _, Bottom -> Bottom - | Value i1, Value i2 -> Value (Intervals.add i1 i2) + | Value (Bool _), _ + | _, Value (Bool _) -> failwith "[add] Cannot evaluate polynomial with boolean values" + | Value (Interval i1), Value (Interval i2) -> Value (Interval (Intervals.add i1 i2)) let mul coef i = match i with | Top -> if Q.equal coef Q.zero then - Value (Intervals.point Q.zero ty Explanation.empty) + Value (Interval (Intervals.point Q.zero ty Explanation.empty)) else Top | Bottom -> Bottom - | Value i -> - Value ( + | Value (Bool _) -> failwith "[mul] Cannot evaluate polynomial with boolean values" + | Value (Interval i) -> + Value (Interval ( Intervals.mult (Intervals.point coef ty Explanation.empty) i - ) - end) in (* todo: apply functor statically for each type *) + )) + end) in (* todo: apply functor statically for each possible interval type *) let map r = match M.find_opt r v with | None -> Top @@ -231,10 +278,11 @@ module IntervalsDomain : | None | Some Top -> Intervals.undefined ty | Some Bottom -> failwith "Internal value is bottom: Should have been checked beforehand" - | Some ((Value i) as v) -> + | Some ((Value (Interval i)) as v) -> debug "[rfind] Found %a in state %a, associated to %a@." R.print k pp s pp_v v; i + | Some (Value (Bool _)) -> failwith "[rfind] Cannot return interval associated to boolean" let radd k b s = match b with @@ -263,7 +311,8 @@ module IntervalsDomain : match eval_constraint ty s p with | Top | Bottom -> s, false - | Value i -> + | Value (Bool _) -> assert false + | Value (Interval i) -> (* Deducing the value of `r` *) debug "[fix_point] %a R %a@." P.print p Intervals.print i; @@ -289,7 +338,7 @@ module IntervalsDomain : debug "[fix_point] New interval of %a : %a@." R.print r Intervals.print ri; if change then - radd r (Value ri) s, change + radd r (Value (Interval ri)) s, change else s, keep_iterating end @@ -299,17 +348,6 @@ module IntervalsDomain : if keep_iterating then aux new_vars else s in aux s - (* todo: narrow on upper bound then on lower bound *) - let narrow_eq ~rinter ~prev_inter = - debug "[fix_point] Narrow EQ@."; - if - begin - Intervals.contained_in rinter prev_inter && - not (Intervals.equal rinter prev_inter) - end - then rinter, true - else prev_inter, false - let narrow_neq ~rinter ~prev_inter = (* If r <> p and p \in rinter, then if rinter is a point, then we can deduce informations, else we can't *) @@ -317,11 +355,14 @@ module IntervalsDomain : match Intervals.is_point rinter with | None -> prev_inter, false | Some (q, _) -> - if Intervals.contains prev_inter q then begin - let () = debug "Excluding %a from %a@." - Q.print q Intervals.print prev_inter in - Intervals.exclude rinter prev_inter, true - end else prev_inter, false + try + if Intervals.contains prev_inter q then begin + let () = debug "Excluding %a from %a@." + Q.print q Intervals.print prev_inter in + Intervals.exclude rinter prev_inter, true + end else prev_inter, false + with + | Intervals.NotConsistent _ -> raise EmptyInterval let narrow_le ~rinter ~prev_inter = debug "[fix_point] Narrow LE ; r_inter = %a -- previous_inter = %a@." @@ -407,6 +448,8 @@ module IntervalsDomain : end with | Intervals.No_finite_bound -> prev_inter, false + | Intervals.NotConsistent _ -> raise EmptyInterval + let narrow_gt ~rinter ~prev_inter = debug "[fix_point] Narrow GT@."; @@ -461,6 +504,14 @@ module IntervalsDomain : | Intervals.No_finite_bound -> prev_inter, false | Intervals.NotConsistent _ -> raise EmptyInterval + let narrow_eq ~rinter ~prev_inter = + debug "[fix_point] Narrow EQ@."; + let rinter', change1 = narrow_le ~rinter ~prev_inter in + debug "[fix_point] After LE: %a@." Intervals.print rinter; + let rinter, change2 = narrow_ge ~rinter ~prev_inter:rinter' in + debug "[fix_point] After GE: %a@." Intervals.print rinter; + rinter, change1 || change2 + let fix_point_eq = fix_point narrow_eq let fix_point_neq = fix_point narrow_neq let fix_point_le = fix_point narrow_le @@ -490,7 +541,8 @@ module IntervalsDomain : let interval = eval_constraint ty v p in match interval with | Top | Bottom -> None - | Value i -> begin + | Value (Bool _) -> assert false + | Value (Interval i) -> begin let inf = try let (inf, _, _) = Intervals.borne_inf i in inf with | Intervals.No_finite_bound -> Q.sub c Q.one in @@ -534,9 +586,6 @@ module IntervalsDomain : (* Adding constraint l1 R l2, with R = (lit). *) let add_constraint l1 l2 lit v = - match v with - | Bottom -> failwith "Add constraint with bottom is forbidden" - | _ -> let l = Symbols.Lit lit in (* Only for debug *) debug "[add_constraint] Adding constraint %a %a %a to environment@." E.print l1 Symbols.print l E.print l2; @@ -581,7 +630,7 @@ module IntervalsDomain : P.fold_on_vars (fun r q acc_cstr -> let p' = P.sub (P.create [q,r] mc ty) p in - debug "[add_constraint] Partial constraint for %a*%a: %a" + debug "[add_constraint] Partial constraint for %a*%a: %a@." Q.print q R.print r P.print p'; ((q, r, p') :: acc_cstr)) p @@ -596,6 +645,16 @@ module IntervalsDomain : debug "[add_constraint] Inconsistent interval, returning `false`@."; AlreadyFalse + let add_constraint elist lit v = + match v with + | Bottom -> failwith "Add constraint with bottom is forbidden" + | _ -> + match elist with + | [l1; l2] -> add_constraint l1 l2 lit v + | _ -> + debug "[add_constraint] Bad number of litterals, ending"; + NewConstraint v + let eval_expr e s = match E.term_view e with | Not_a_term _ -> unknown