diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index d0a3f1ef3d..a7e71ee032 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -300,7 +300,7 @@ let rec make_term up_qv quant_basename t = | Util.SPreprocess | Util.SAll -> let module S = SimpExprPreproc () in let smp_term = S.simp_expr term in - if SRE.has_changed smp_term + if SRE.has_changed smp_term then SRE.get_expr smp_term else term *) diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index 93d2929a48..8d559ed55f 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -52,7 +52,9 @@ type ('expr, 'abs_val) simp = { } let pp_simp pp_abs_val fmt s = - Format.fprintf fmt "%a:%a" E.print s.exp pp_abs_val s.v + Format.fprintf fmt "%a:%a" + E.print s.exp + pp_abs_val s.v let get_expr e = e.exp let get_abs_val e = e.v @@ -91,7 +93,12 @@ module type Dom = sig val v_join : v -> v -> v (** Add constraint *) - val add_constraint : Expr.t -> Expr.t -> Symbols.lit -> state -> state add_constraint_res + val add_constraint : + Expr.t -> + Expr.t -> + Symbols.lit -> + state -> + state add_constraint_res (** If possible, adds `expr` to `state` with the value `v` *) val add_raw_value : Expr.t -> v -> state -> state @@ -121,7 +128,8 @@ module SimpleReasoner type state = D.state type v = D.v - let (simp_cache : (state * (Expr.t, v) simp) list Expr.Map.t ref) = ref E.Map.empty + let (simp_cache : (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 @@ -217,7 +225,8 @@ module SimpleReasoner if is_form then add_form_constraint state e else - failwith "add_lit_constraint should be only called on litterals or formulas" + 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 @@ -322,10 +331,12 @@ module SimpleReasoner | Lemma _ | Skolem _ -> - debug "[add_form_constraint] Lemma/Skolem: not using it@."; NewConstraint state + debug "[add_form_constraint] Lemma/Skolem: not using it@."; + NewConstraint state | Not_a_form -> - failwith "add_form_constraint should be only called on litterals or formulas" + 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 @@ -341,7 +352,9 @@ module SimpleReasoner (th : E.t) (el : E.t) : (E.t, v) simp list = - debug "[simp_ite] Simplifying condition %a with %a@." E.print cond D.pp state; + debug "[simp_ite] Simplifying condition %a with %a@." + E.print cond + D.pp state; let 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 @@ -404,7 +417,8 @@ module SimpleReasoner else ( debug "[simp_form] Keeping %a@." E.print e; match state &&& esimp.exp with - | AlreadyTrue | AlreadyFalse -> failwith "Should have simplify beforehand" + | AlreadyTrue + | AlreadyFalse -> failwith "Should have simplify beforehand" | NewConstraint state -> (state, (esimp :: simp_exps))) , false @@ -455,7 +469,8 @@ module SimpleReasoner List.map (identity state) elist and simp_expr_no_cache state (e : E.t) : (E.t, v) simp = - debug "[simp_expr] Simplifying expression %a with %a@." E.print e D.pp state; + debug "[simp_expr] Simplifying expression %a with %a@." + E.print e D.pp state; let res = let ty = E.type_info e in let elist = E.get_sub_expr e in @@ -467,7 +482,8 @@ module SimpleReasoner debug "[simp_expr] Ite treated@."; match simp with | [branch] -> - debug "[simp_expr] Simplification cut a branch, yielding %a@." Expr.print branch.exp; + debug "[simp_expr] Simplification cut a branch, yielding %a@." + Expr.print branch.exp; branch | [cond; th; el] -> if cond.diff || th.diff || el.diff then diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli index c589a3b3da..a6a36dee5f 100644 --- a/src/lib/frontend/simple_reasoner_expr.mli +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -50,7 +50,12 @@ module type Dom = sig val v_join : v -> v -> v (** Add constraint *) - val add_constraint : Expr.t -> Expr.t -> Symbols.lit -> state -> state add_constraint_res + val add_constraint : + Expr.t -> + Expr.t -> + Symbols.lit -> + state -> + state add_constraint_res (** If possible, adds `expr` to `state` with the value `v` *) val add_raw_value : Expr.t -> v -> state -> state diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index 4b05b43d5c..9f8d3368c7 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -118,7 +118,7 @@ module IntervalsDomain : (* !res = Some 0 => m1 = m2 *) let exception Stop in let set_res r = - (* Sets the res reference to the value in argument if it is consistent *) + (* Sets res to the value in argument if it is consistent *) match !res with | None -> (* First time comparing *) res := Some (Some r) @@ -136,16 +136,13 @@ module IntervalsDomain : | Some v -> v in try let () = ignore @@ - M.merge (* The result of this merge is ignored : it is only here to compare *) + (* The result of this merge is ignored : it is only here to compare *) + M.merge (fun _k v1 v2 -> match v1, v2 with | None, None -> assert false - | None, _ -> - (* Could be 'assert false', but assuming variable absent <=> equal to top *) - set_res 1; None - | _, None -> - (* Could be 'assert false', but assuming variable absent <=> equal to top *) - set_res (-1); None + | None, _ -> set_res 1 ; None + | _, None -> set_res (-1); None | Some v1, Some v2 -> match compare_intervals v1 v2 with | None -> res := Some None; raise Stop @@ -183,7 +180,10 @@ module IntervalsDomain : | v, Bottom -> v | Value i1, Value i2 -> Value (join i1 i2) - let eval_constraint (ty : Ty.t) (s : state) (p : P.t) : Intervals.t abstract_value = + let eval_constraint + (ty : Ty.t) + (s : state) + (p : P.t) : Intervals.t abstract_value = match s with | Top -> begin match P.to_list p with @@ -211,7 +211,11 @@ module IntervalsDomain : else Top | Bottom -> Bottom | Value i -> - Value (Intervals.mult (Intervals.point coef ty Explanation.empty) i) + Value ( + Intervals.mult + (Intervals.point coef ty Explanation.empty) + i + ) end) in (* todo: apply functor statically for each type *) let map r = match M.find_opt r v with @@ -225,9 +229,12 @@ module IntervalsDomain : | Value m -> match M.find_opt k m with | None | Some Top -> Intervals.undefined ty - | Some Bottom -> failwith "Internal value is bottom: Should have been checked beforehand" + | Some Bottom -> + failwith "Internal value is bottom: Should have been checked beforehand" | Some ((Value i) as v) -> - debug "[rfind] Found %a in state %a, associated to %a@." R.print k pp s pp_v v; i + debug "[rfind] Found %a in state %a, associated to %a@." + R.print k pp s pp_v v; + i let radd k b s = match b with @@ -237,8 +244,11 @@ module IntervalsDomain : | Value m -> Value (M.add k b m) | Bottom -> s + type narrow = + rinter:Intervals.t -> prev_inter:Intervals.t -> Intervals.t * bool + let fix_point - (narrow : rinter:Intervals.t -> prev_inter:Intervals.t -> Intervals.t * bool) + (narrow : narrow) (ty : Ty.t) (constraints : (Q.t * R.r * P.t) list) (s : state) = @@ -247,7 +257,8 @@ module IntervalsDomain : List.fold_left (fun ((s : state), keep_iterating) (q,r,p) -> (* Calculates the interval of `p` given the value of `vars` *) - debug "[fix_point] Constraint %a%a R %a@." Q.print q R.print r P.print p; + debug "[fix_point] Constraint %a%a R %a@." + Q.print q R.print r P.print p; debug "[fix_point] Evaluating with state %a@." pp s; match eval_constraint ty s p with | Top @@ -263,12 +274,15 @@ module IntervalsDomain : debug "[fix_point] Narrowing@."; debug "[fix_point] Dividing %a by %a@." Intervals.print i Q.print q; - let rinter = Intervals.div i (Intervals.point q ty Explanation.empty) in + let rinter = + Intervals.div i (Intervals.point q ty Explanation.empty) + in debug "[fix_point] Interval of %a by the constraint : %a@." R.print r Intervals.print rinter; let prev_inter = rfind ty r s in - debug "[fix_point] Interval of %a in %a: %a@." R.print r pp s Intervals.print prev_inter; + debug "[fix_point] Interval of %a in %a: %a@." + R.print r pp s Intervals.print prev_inter; let ri, change = narrow ~rinter ~prev_inter in debug "[fix_point] Old interval of %a : %a@." R.print r Intervals.print prev_inter; @@ -288,19 +302,24 @@ module IntervalsDomain : (* todo: narrow on upper bound then on lower bound *) let narrow_eq ~rinter ~prev_inter = debug "[fix_point] Narrow EQ@."; - if Intervals.contained_in rinter prev_inter && not (Intervals.equal rinter prev_inter) + 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 we can deduce informations, - otherwise we can't *) + (* If r <> p and p \in rinter, then if rinter is a point, + then we can deduce informations, else we can't *) debug "[fix_point] Narrow NEQ@."; 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 + 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 @@ -325,14 +344,16 @@ module IntervalsDomain : prev_inter, true | Some prev_sup -> if Q.compare bound prev_sup >= 0 then begin - debug "[fix_point] Constraint upper bound %a >= %a previous upper bound@." + debug + "[fix_point] Constraint upper bound %a >= %a previous upper bound@." Q.print bound Q.print prev_sup; debug "[fix_point] No need for more narrowing@."; prev_inter, false end else begin (* The new upper bound is lower than then previous one, replacing it *) - debug "[fix_point] Constraint upper bound %a < %a previous upper bound@." + debug + "[fix_point] Constraint upper bound %a < %a previous upper bound@." Q.print bound Q.print prev_sup; debug "[fix_point] Narrowing@."; Intervals.new_borne_sup @@ -366,14 +387,16 @@ module IntervalsDomain : if Q.compare bound prev_sup >= 0 then begin (* The new upper bound is higher then the previous one, keeping it *) - debug "[fix_point] Constraint upper bound %a >= %a previous upper bound@." + debug + "[fix_point] Constraint upper bound %a >= %a previous upper bound@." Q.print bound Q.print prev_sup; debug "[fix_point] No need for more narrowing"; prev_inter, false end else begin (* The new upper bound is lower than then previous one, replacing it *) - debug "[fix_point] Constraint upper bound %a < %a previous upper bound@." + debug + "[fix_point] Constraint upper bound %a < %a previous upper bound@." Q.print bound Q.print prev_sup; debug "[fix_point] Narrowing@."; Intervals.new_borne_sup @@ -398,12 +421,20 @@ module IntervalsDomain : in match prev_inf with | None -> - Intervals.new_borne_inf Explanation.empty bound ~is_le:false prev_inter, true + Intervals.new_borne_inf + Explanation.empty bound + ~is_le:false + prev_inter, + true | Some prev_inf -> if Q.compare prev_inf bound >= 0 then prev_inter, false else - Intervals.new_borne_inf Explanation.empty bound ~is_le:false prev_inter, true + Intervals.new_borne_inf + Explanation.empty bound + ~is_le:false + prev_inter, + true with | Intervals.No_finite_bound -> prev_inter, false | Intervals.NotConsistent _ -> raise EmptyInterval @@ -418,12 +449,14 @@ module IntervalsDomain : in match prev_inf with | None -> - Intervals.new_borne_inf Explanation.empty bound ~is_le prev_inter, true + Intervals.new_borne_inf Explanation.empty bound ~is_le prev_inter, + true | Some prev_inf -> if Q.compare prev_inf bound >= 0 then prev_inter, false else - Intervals.new_borne_inf Explanation.empty bound ~is_le prev_inter, true + Intervals.new_borne_inf Explanation.empty bound ~is_le prev_inter, + true with | Intervals.No_finite_bound -> prev_inter, false | Intervals.NotConsistent _ -> raise EmptyInterval @@ -446,10 +479,11 @@ module IntervalsDomain : | L_neg_built LE -> fix_point_gt | L_neg_built LT -> fix_point_ge | L_built (IsConstr _) - | L_neg_built (IsConstr _) -> (* Should be handled (at least doing nothing) *) - failwith "Arith Simplifier: do not handle IsConstr" + | L_neg_built (IsConstr _) -> + (* Should be handled (at least doing nothing) *) + failwith "Arith Simplifier does not handle IsConstr" | L_neg_pred -> - failwith "todo (even a better error message would be nice)" + failwith "Arith Simplifier does not handle L_neg_pred" (* todo: take into account types, open bounds & le/lt *) let check_constraint ty lit p c v = @@ -489,10 +523,11 @@ module IntervalsDomain : else None | L_built (IsConstr _) - | L_neg_built (IsConstr _) -> (* Should be handled (at least doing nothing) *) - failwith "Check constraint: do not handle IsConstr" + | L_neg_built (IsConstr _) -> + (* Should be handled (at least doing nothing) *) + failwith "Check constraint does not handle IsConstr" | L_neg_pred -> - failwith "Check constraint : todo (even a better error message would be nice)" + failwith "Check constraint does not handle L_neg_pred" end let to_arith e = A.embed @@ fst @@ R.make e @@ -529,20 +564,6 @@ module IntervalsDomain : else lit in -(* - let is_neg = Q.compare cst Q.zero < 0 in - let p, c, lit = - if is_neg then - P.mult_const Q.m_one p, - Q.mult Q.m_one c, - match lit with - | L_built LE -> Symbols.L_neg_built LT - | L_built LT -> L_neg_built LE - | L_neg_built LE -> L_built LT - | L_neg_built LT -> L_built LE - | l -> l - else p, c, lit in *) - debug "[add_constraint] Normalized constraint : %a + %a %a 0@." P.print p Q.print c Symbols.print (Lit lit); debug "[add_constraint] Known information: %a@." pp v; @@ -560,7 +581,8 @@ 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" Q.print q R.print r P.print p'; + debug "[add_constraint] Partial constraint for %a*%a: %a" + Q.print q R.print r P.print p'; ((q, r, p') :: acc_cstr)) p [] in diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 851d4134af..6111b81452 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -538,7 +538,8 @@ and print_term_binders ?(annot=no_print) fmt l = List.iter (fun (sy, t) -> fprintf fmt ", %a = %a" Symbols.print sy (print_term ~annot) t) l -and print_term_list ?(annot=no_print) fmt = List.iter (fprintf fmt "%a," (print_term ~annot)) +and print_term_list ?(annot=no_print) fmt = + List.iter (fprintf fmt "%a," (print_term ~annot)) and print_atom ?(annot=no_print) fmt a = match a.c with @@ -574,9 +575,14 @@ and print_formula ?(annot=no_print) fmt f = fprintf fmt "not %a" (print_formula ~annot) f | TFop(OPif, [cond; f1;f2]) -> fprintf fmt "if %a then %a else %a" - (print_formula ~annot) cond (print_formula ~annot) f1 (print_formula ~annot) f2 + (print_formula ~annot) cond + (print_formula ~annot) f1 + (print_formula ~annot) f2 | TFop(op, [f1; f2]) -> - fprintf fmt "%a %s %a" (print_formula ~annot) f1 (string_of_op op) (print_formula ~annot) f2 + fprintf fmt "%a %s %a" + (print_formula ~annot) f1 + (string_of_op op) + (print_formula ~annot) f2 | TFforall { qf_bvars = l; qf_triggers = t; qf_form = f; _ } -> fprintf fmt "forall %a [%a]. %a" print_binders l (print_triggers ~annot) t (print_formula ~annot) f