From 40e42bafac2a52fe15f64b6e09d3931e30c8abd5 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 15 Apr 2019 14:45:36 +0200 Subject: [PATCH 01/18] Formula simplification at preprocessing --- src/bin/gui/annoted_ast.ml | 19 +- src/lib/dune | 1 + src/lib/frontend/cnf.ml | 58 ++- src/lib/frontend/simple_reasoner_expr.ml | 535 ++++++++++++++++++++++ src/lib/frontend/simple_reasoner_expr.mli | 81 ++++ src/lib/reasoners/fun_sat.ml | 3 - src/lib/reasoners/th_util.ml | 2 + src/lib/reasoners/th_util.mli | 2 + src/lib/structures/commands.ml | 2 +- src/lib/structures/commands.mli | 2 +- src/lib/structures/expr.ml | 73 ++- src/lib/structures/expr.mli | 7 + src/lib/structures/symbols.ml | 16 +- src/lib/structures/typed.ml | 472 ++++++++++++++----- src/lib/structures/typed.mli | 75 ++- src/lib/util/options.ml | 9 + src/lib/util/options.mli | 21 + src/lib/util/util.ml | 5 + src/lib/util/util.mli | 5 + 19 files changed, 1241 insertions(+), 147 deletions(-) create mode 100644 src/lib/frontend/simple_reasoner_expr.ml create mode 100644 src/lib/frontend/simple_reasoner_expr.mli diff --git a/src/bin/gui/annoted_ast.ml b/src/bin/gui/annoted_ast.ml index 345dd0be5..859330a48 100644 --- a/src/bin/gui/annoted_ast.ml +++ b/src/bin/gui/annoted_ast.ml @@ -717,15 +717,18 @@ and print_tt_desc fmt = function | TTnamed (lbl, t) -> fprintf fmt "%s:%a" (Hstring.view lbl) print_tterm t | TTinInterval(e, lb, ub) -> fprintf fmt "%a in %a, %a" - print_term e + (print_term ~annot:no_print) e Symbols.print_bound lb Symbols.print_bound ub - | TTmapsTo(x,e) -> fprintf fmt "%a |-> %a" Var.print x print_term e + | TTmapsTo(x,e) -> + fprintf fmt "%a |-> %a" Var.print x (print_term ~annot:no_print) e | TTite(f,t1, t2) -> fprintf fmt "(if %a then %a else %a)" - print_tform f print_term t1 print_term t2 + print_tform f + (print_term ~annot:no_print) t1 + (print_term ~annot:no_print) t2 | TTproject (_, _, _) | TTmatch (_, _) -> Gui_config.not_supported "Algebraic datatypes" @@ -737,9 +740,13 @@ and print_term_binders fmt l = match l with | [] -> assert false | (sy, t) :: l -> - fprintf fmt "%a = %a" Symbols.print_clean sy print_term t; + fprintf fmt "%a = %a" Symbols.print_clean sy (print_term ~annot:no_print) t; List.iter (fun (sy, t) -> - fprintf fmt ",\n%a = %a" Symbols.print_clean sy print_term t) l + fprintf + fmt + ",\n%a = %a" + Symbols.print_clean sy + (print_term ~annot:no_print) t) l and print_tatom fmt a = match a.Typed.c with | TAtrue -> fprintf fmt "true" @@ -792,7 +799,7 @@ and print_tform2 fmt f = match f.Typed.c with and print_mixed_binders = let aux fmt e = match e with - | TletTerm t -> fprintf fmt "%a" print_term t + | TletTerm t -> fprintf fmt "%a" (print_term ~annot:no_print) t | TletForm f -> fprintf fmt "%a" print_tform2 f in fun fmt binders -> match binders with diff --git a/src/lib/dune b/src/lib/dune index 91399d1e2..5980a6b5e 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -29,6 +29,7 @@ ; modules that make up the lib (modules ; frontend + Simple_reasoner_expr Cnf Input Frontend Parsed_interface Typechecker ; reasoners Ac Arith Arrays Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 2bd85a159..54d74e145 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -34,6 +34,32 @@ open Commands module E = Expr module Sy = Symbols module SE = E.Set +module SRE = Simple_reasoner_expr + +(** Simplifyer not using the theory *) +module DummySimp = + Expr.SimpExpr + (struct + type expr = Expr.t + type v = unit + let top = () + let bottom = () + let compare _ _ = Some 0 + let join _ _ = () + let add_constraint _ _ = () + let vrai = () + let faux = () + end + ) + +let choose_preproc () : + (module Simple_reasoner_expr.S with type expr = Expr.t and type v = unit) = + if not (Options.get_simplify_th ()) then + (module DummySimp) + else + (module DummySimp) + +module SimpExprPreproc () = (val (choose_preproc ())) [@@ocaml.ppwarning "TODO: Change Symbols.Float to store FP numeral \ constants (eg, <24, -149> for single) instead of \ @@ -283,8 +309,15 @@ let rec make_term up_qv quant_basename t = ~decl_kind:E.Daxiom (* not correct, but not a problem *) ~toplevel:false in - mk_term t - + let term = mk_term t in + match Options.get_simplify () with + | Util.SNo -> term + | Util.SPreprocess | Util.SAll -> + let module S = SimpExprPreproc () in + let smp_term = S.simp_expr term in + if SRE.has_changed smp_term + then SRE.get_expr smp_term + else term and make_trigger ~in_theory name up_qv quant_basename hyp (e, from_user) = let content, guard = match e with @@ -496,7 +529,14 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t = (* wrapper of function make_form *) let make_form name f loc ~decl_kind = let ff = - make_form Sy.Map.empty name f loc ~decl_kind ~toplevel:true + let form = make_form Sy.Map.empty name f loc ~decl_kind ~toplevel:true in + match Options.get_simplify () with + Util.SNo -> form + | Util.SPreprocess | Util.SAll -> + let module S = SimpExprPreproc () in + let smp_form = S.simp_expr form in + if SRE.has_changed smp_form then SRE.get_expr smp_form + else form in assert (Sy.Map.is_empty (E.free_vars ff Sy.Map.empty)); let ff = E.purify_form ff in @@ -522,7 +562,7 @@ let mk_assume acc f name loc = *) let defining_term f = if get_verbose () then - Format.eprintf "defining term of %a@." Typed.print_formula f; + Format.eprintf "defining term of %a@." (Typed.print_formula ?annot:None) f; match f.c with | TFforall {qf_form={c=TFop(OPiff,[{c=TFatom {c=TApred(d,_);_};_};_]); _}; _} | TFforall {qf_form={c=TFatom {c=TAeq[d;_];_}; _}; _} @@ -565,12 +605,16 @@ let mk_theory acc l th_name extends _loc = | TAxiom (loc, name, ax_kd, f) -> loc, name, f, ax_kd | _ -> assert false in - let ax_form = make_form ax_name f loc ~decl_kind:E.Dtheory in + let ax_form = + make_form ax_name f loc ~decl_kind:E.Dtheory + in let th_elt = {Expr.th_name; axiom_kind; extends; ax_form; ax_name} in {st_decl=ThAssume th_elt ; st_loc=loc} :: acc - )acc l + ) + acc + l -let make acc d = +let make acc (d : (int Typed.tdecl, 'a) Typed.annoted) = match d.c with | TPush (loc,n) -> {st_decl=Push n; st_loc=loc} :: acc | TPop (loc,n) -> {st_decl=Pop n; st_loc=loc} :: acc diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml new file mode 100644 index 000000000..4d94104a2 --- /dev/null +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -0,0 +1,535 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2018 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +let verb = Options.get_simplify_verbose + +let silent (msg : ('a, Format.formatter, unit) format) = + Format.ifprintf Format.std_formatter msg + +let talk (msg : ('a, Format.formatter, unit) format) = + Format.printf "[Preprocess] "; + Format.printf msg + +let debug (msg : ('a, Format.formatter, unit) format) = + if verb () + then talk msg + else silent msg + +(** 1. Utils *) + +(** Values are representations of expressions + that have been "solved", in the sense that they can + be reduced to a boolean or a float/int. +type value = + | Bool of bool + | Num of Q.t + +let (++) v1 v2 = + match v1, v2 with + Bool b1, Bool b2 -> Bool (b1 || b2) + | Num n1, Num n2 -> Num (Q.add n1 n2) + | _,_ -> assert false + +let (--) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> Num (Q.sub n1 n2) + | _,_ -> assert false + +let ( ** ) v1 v2 = + match v1, v2 with + Bool b1, Bool b2 -> Bool (b1 && b2) + | Num n1, Num n2 -> Num (Q.mul n1 n2) + | _,_ -> assert false + +let (|=) v1 v2 = + match v1, v2 with + Bool b1, Bool b2 -> b1 == b2 + | Num n1, Num n2 -> (Stdlib.(=)) n1 n2 + | _,_ -> false + +let (|<>) v1 v2 = not (v1 |= v2) + +let (|<) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> n1 < n2 + | _,_ -> assert false + +let (|<=) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> n1 <= n2 + | _,_ -> assert false + +let (|>) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> n1 > n2 + | _,_ -> assert false + +let (|>=) v1 v2 = + match v1, v2 with + | Num n1, Num n2 -> n1 >= n2 + | _,_ -> assert false + + +let pp_val fmt v = + match v with + Bool b -> Format.fprintf fmt "Bool %b" b + | Num n -> Format.fprintf fmt "Num %a" Q.pp_print n*) + +(** A simplified formula/expr/... type. + The diff field is set to false if the operation did not change the + input. + As queries may provide explanations, the third field correspond to the + explanation behind the simplification. *) + +(** Same as List.fold_left, but f returns + a tuple (acc, stop) where stop is a boolean + stating that the loop has to stop. *) +let fold_left_stop + (f : 'a -> 'b -> ('a * bool)) + (acc : 'a) + (l : 'b list) : 'a + = + let rec __fold acc l = + match l with + [] -> acc + | hd :: tl -> + let acc, stop = f acc hd in + if stop then acc + else __fold acc tl + in __fold acc l + +type ('expr, 'abs_val) simp = { + exp : 'expr; + diff : bool; + v : 'abs_val + } + +let get_expr e = e.exp +let get_abs_val e = e.v +let has_changed e = e.diff + +(** 2. Simplifyer *) + +(** As the simplifyer interacts with different components of alt-ergo, + it is written to be as generic as possible. + The simplifyer is then a functor of different modules which type is + defined below. *) + +(** Dom is the signature of the abstact domain. *) +module type Dom = +sig + type v + type expr + + (** Top/Bottom value *) + val top : v + val bottom : v + + (** (Partial) Compare function *) + val compare : v -> v -> int option + + (** Join operator *) + val join : v -> v -> v + + (** Add constraint *) + val add_constraint : expr -> v -> v + + (** Constants *) + val vrai : v + val faux : v +end + +module type Expr = sig + type t + val equal : t -> t -> bool + val mk_term : Symbols.t -> t list -> Ty.t -> t + val get_comp : t -> Symbols.t + val get_sub_expr : t -> t list + val get_type : t -> Ty.t + val neg : t -> t + val vrai : t + val faux : t + val int : string -> t + val real : string -> t + val print : Format.formatter -> t -> unit +end + +(** This is the signature of the simplifyer. *) +module type S = +sig + type v + type expr + + (** Simplifies an expression. *) + val simp_expr : expr -> (expr, v) simp +end + + +module SimpleReasoner + (E : Expr) + (D : Dom with type expr = E.t) + : S with type v = D.v and type expr = E.t = struct + type expr = E.t + type v = D.v + + let identity v exp = {exp; diff = false; v} + + (* + + let diff_list (l : ('a, 'expl) simp list) : (('a list), 'expl) simp = + let rev = + List.fold_left + (fun acc s -> + {exp = s.exp :: acc.exp; + diff = acc.diff || s.diff; + v = D.join acc.v s.v + } + ) + (identity []) + l + in + {rev with exp = List.rev rev.exp} + (* Check is an expression has an arithmetic type (Some true), + a boolean type (Some false) or else (None). *) + let is_arith (e : expr) : bool option = + match E.get_type e with + Ty.Tbool -> Some false + | Ty.Tint | Ty.Treal + | Ty.Tvar {value = Some Ty.Tint;_} + | Ty.Tvar {value = Some Ty.Treal;_} -> Some true + | _ -> None + + let value_from_query (e : expr) : (value * expl) option = + match is_arith e with + Some true -> ( + match T.q_query e !env with + Some (res_query, expl) -> + Some ((Num res_query), expl) + | None -> None + ) + | Some false -> ( + match T.bool_query e !env with + Some (res_query, expl) -> + Some ((Bool res_query), expl) + | None -> None + ) + | None -> None + + let expr_to_value (e : expr) : (value * expl) option = + match E.get_comp e with + True -> Some ((Bool true), no_reason) + | False -> Some ((Bool false), no_reason) + | Int s -> Some ((Num (Q.of_string (Hstring.view s))), no_reason) + | Real s -> Some ((Num (Q.of_string (Hstring.view s))), no_reason) + | _ -> value_from_query e + + let value_to_expr (ty : Ty.t) (v : value) : expr = + debug "Type = %a@." Ty.print ty; + match v with + Bool true -> E._true + | Bool false -> E._false + | Num i -> + let i' = Q.to_string i in + if ty == Ty.Treal + then E.real i' + else E.int i' + + let arith + (ty : Ty.t) + (op : value -> value -> value) + (e_list : expr list): (expr list, expl) simp = + (* Wrapper for op. Checks that it has been called. + If it has never been called, then there have been no + simplification. *) + let op_has_been_called = ref 0 in + let op v1 v2 = + op_has_been_called := !op_has_been_called + 1 ; + debug "Calling operator@."; + op v1 v2 + in + + let vals,expl,exprs = + fold_left + (fun (acc_solved,acc_expl,acc_remain) v -> + match expr_to_value v with + None -> (acc_solved, acc_expl, v :: acc_remain) + | Some (v, expl) -> + let new_expl = Expl.union expl acc_expl in + match acc_solved with + None -> + (Some v, new_expl, acc_remain) + | Some old_v -> (Some (op old_v v), new_expl, acc_remain) + ) + (None, Expl.empty, []) + e_list + in + if !op_has_been_called = 0 + then + begin + debug "Operator has not been called.@."; + identity e_list + end + else + match vals with + None -> identity e_list + | Some v -> + let cst_expr = value_to_expr ty v in + debug "Result of simplifyable operations : %a@." E.pretty cst_expr; + {v = List.rev exprs @ [value_to_expr ty v]; diff = true; expl} + + let oper (op : value -> value -> bool) (l : expr list) : bool * bool * expl = + (* all_true is a boolean stating that every call of 'op' returned 'true'. + set to true at the beginning, it is set to false if one of the + list term. + last_val is the last value that has been accepted by the test + acc_expl is the accumulated explanations of each value tested + *) + let rec _oper + (all_true : bool) + (last_val : value option) + (acc_expl : expl) + (l : expr list) : bool * bool * expl = + match l with + [] -> (* No more elements, and none failed the test. *) + false, all_true, acc_expl + | hd :: tl -> + let hd_val = expr_to_value hd in + match hd_val, last_val with + | None, None -> + _oper false None acc_expl tl + + | Some (v, expl), None -> + _oper + all_true + (Some v) + (Expl.union expl acc_expl) + tl + + | None, Some v -> + _oper false (Some v) acc_expl tl + + | Some (v, expl), Some v' -> + let res = op v v' in + debug "Result : %a (op) %a = %b@." + pp_val v' pp_val v res; + if op v' v + then ( + _oper all_true (Some v') (Expl.union expl acc_expl) tl + ) + else (* The operation is not respected *) ( + true, false, (Expl.union expl acc_expl) + ) + in + _oper true None no_reason l + + let apply_op + (op : value -> value -> bool) + (l : expr list) : (expr list, expl) simp = + let falsify,all_true,expl = oper op l in + if falsify + then {v = [E._false]; diff = true; expl} + else if all_true + then {v = [E._true]; diff = true; expl} + else {v = l; diff = false; expl} + + let is_unary (o : Symbols.operator) : bool = + let open Symbols in + match o with + | Plus | Minus | Mult | Div | Modulo + | Concat | Extract | Get | Set | Fixed | Float + | Reach | Record | Min_real | Min_int | Max_real | Max_int + | Integer_log2 | Pow | Tite -> false + + | Access _ + | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil + | Sqrt_real_default | Sqrt_real_excess | Integer_round + | Constr _ + | Destruct (_,_) -> true *) + + let (|=) v1 v2 = + match D.compare v1 v2 with + | Some i -> i = 0 + | None -> false + + let (&&&) v e = D.add_constraint e v + + let is_true v = v |= D.vrai + let is_false v = v |= D.faux + + let simp_true = {exp = E.vrai; diff = true; v = D.vrai} + let simp_false = {exp = E.faux; diff = true; v = D.faux} + + (* + let is_constr (constr : Hstring.t) (e : expr) : bool option = + match E.get_comp e with + | Op (Constr s') -> Some (Hstring.equal constr s') + | _ -> None*) + + let rec simp_ite + (state : v) + (cond : expr) + (th : expr) + (el : expr) : + (expr, v) simp list = + let scond : (expr, v) simp = simp_expr state cond in + if is_true scond.v then + let th : (expr, v) simp = simp_expr state th in + [{th with diff = true}] + else if is_false scond.v then + let el : (expr, v) simp = simp_expr state el in + [{el with diff = true}] + else + let neg_cond = E.neg scond.exp in + let sth : (expr, v) simp = simp_expr (state &&& scond.exp) th in + let sel : (expr, v) simp = simp_expr (state &&& neg_cond) el in + if scond.diff || sth.diff || sel.diff then + [scond; sth; sel] + else [ + identity scond.v cond; + identity sth.v th; + identity sel.v el] + + and simp_form + (state : v) + (f : Symbols.form) + (elist : expr list) + : v * (expr, v) simp list = + match f with + | Symbols.F_Unit _ -> begin (* <=> AND *) + let () = debug "F_Unit@." in + let state,rev_res = + fold_left_stop + (fun (state, simp_exps) e -> + let esimp : (expr, v) simp = simp_expr state e in + if is_true esimp.v then ( + debug "%a = true@." E.print e; + (state, simp_exps), false + ) + else if is_false esimp.v then ( + debug "%a = false@." E.print e; + (D.faux, [simp_false]), true + ) else ( + debug "Keeping %a@." E.print e; + (state &&& esimp.exp, esimp :: simp_exps), false + ) + ) + (state, []) + elist + in + match rev_res with + | [] -> D.vrai, [simp_true] + | _ -> state, List.rev rev_res + end + + | F_Clause _ -> begin (* <=> OR *) + let () = debug "F_Clause@." in + let state, rev_res = + fold_left_stop + (fun (state, simp_exps) e -> + let (esimp : (expr, v) simp) = simp_expr state e in + if is_false esimp.v then ( + debug "%a = false@." E.print e; + (state, simp_exps), false + ) + else if is_true esimp.v then ( + debug "%a = true@." E.print e; + (D.vrai, [simp_true]), true + ) + else ( + debug "Keeping %a@." E.print e; + (D.join state esimp.v, (esimp :: simp_exps))) + , false) + (state, []) + elist + in + match rev_res with + | [] -> D.faux, [simp_false] + | _ -> state, List.rev rev_res + end + | _ -> + let () = debug "No additional simplification@." in + D.top, List.map (identity D.top) elist + + and simp_expr state (e : expr) : (expr, v) simp = + let ty = E.get_type e in + let elist = E.get_sub_expr e in + let symb = E.get_comp e in + match symb, elist with + | Op Tite, [cond; th; el] -> begin + debug "Ite"; + let simp = simp_ite state cond th el in + match simp with + | [branch] -> branch + | [cond; th; el] -> + if cond.diff || th.diff || el.diff then { (* A simplification has been made *) + exp = E.mk_term (Op Tite) [cond.exp; th.exp; el.exp] ty; + diff = true; + v = D.join th.v el.v + } else { (* No simplification has been done *) + exp = e; + diff = false; + v = D.join th.v el.v + } + | _ -> assert false + end + | Op Tite, _ -> assert false + | Symbols.Form f, _ -> + debug "Formula: %a@." Symbols.print symb; + let v, l = simp_form state f 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 + } + else {exp = e; diff = false; v = D.top} + | _ -> + debug + "Other: %a@." + Symbols.print symb; + let (l : (expr, 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.top + } + else {exp = e; diff = false; v = D.top} + ) + + (** Wrapper of simp_expr for verbose *) + let simp_expr e = + try + debug "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 + identity res.v e + with + Failure s -> + talk + "Error while simplifying %a\n%s\n\ + I will continue with the initial expression@." + E.print e + s; + identity D.top e +end diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli new file mode 100644 index 000000000..e0a86ea99 --- /dev/null +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -0,0 +1,81 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2018 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the license indicated *) +(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *) +(* present, please contact us to clarify licensing. *) +(* *) +(******************************************************************************) + +(** A simplified formula/expr/... type. + the diff field is set to false if the operation did not change the + input. +*) +type ('expr, 'abs_val) simp +val get_expr : ('e,_) simp -> 'e +val get_abs_val : (_, 'v) simp -> 'v +val has_changed : _ simp -> bool + +(** As the simplifyer interacts with different components of alt-ergo, + it is written to be as generic as possible. + The simplifyer is then a functor of different modules which type is + defined below. +*) + +module type Dom = +sig + type v + type expr + + (** Top/Bottom value *) + val top : v + val bottom : v + + (** (Partial) Compare function *) + val compare : v -> v -> int option + + (** Join operator *) + val join : v -> v -> v + + (** Add constraint *) + val add_constraint : expr -> v -> v + + (** Constants *) + val vrai : v + val faux : v +end + +(** Expr is the signature of the module dedicated to + the representation of expressions that are to be + simplified. *) +module type Expr = sig + type t + val equal : t -> t -> bool + val mk_term : Symbols.t -> t list -> Ty.t -> t + val get_comp : t -> Symbols.t + val get_sub_expr : t -> t list + val get_type : t -> Ty.t + val neg : t -> t + val vrai : t + val faux : t + val int : string -> t + val real : string -> t + val print : Format.formatter -> t -> unit +end + +(** This is the signature of the simplifyer. *) +module type S = +sig + type v + type expr + + (** Simplifies an expression and returns its associated abstract value. *) + val simp_expr : expr -> (expr, v) simp +end + +module SimpleReasoner + (E : Expr) + (D : Dom with type expr = E.t) + : S with type expr = E.t and type v = D.v diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 4b04cddb2..792767e7f 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -34,7 +34,6 @@ module SE = E.Set module ME = E.Map module Ex = Explanation - module Make (Th : Theory.S) : Sat_solver_sig.S = struct module Inst = Instances.Make(Th) module CDCL = Satml_frontend_hybrid.Make(Th) @@ -974,7 +973,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct nb_related_to_goal = t.nb_related_to_goal + 1; nb_related_to_hypo = t.nb_related_to_hypo + 1} - let rec asm_aux acc list = List.fold_left (fun @@ -1122,7 +1120,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct env.heuristics := Heuristics.bump_activity !(env.heuristics) expl; raise (IUnsat (expl, classes)) - let new_inst_level env = let new_ilevel = env.ilevel + 1 in let env = {env with ilevel = new_ilevel} in diff --git a/src/lib/reasoners/th_util.ml b/src/lib/reasoners/th_util.ml index e0bc7301c..f1a13b5f2 100644 --- a/src/lib/reasoners/th_util.ml +++ b/src/lib/reasoners/th_util.ml @@ -26,6 +26,8 @@ (* *) (******************************************************************************) +(** An answer type. If it is Some (thing), then the answer is yes, + otherwise it is unknown. *) type answer = (Explanation.t * Expr.Set.t list) option diff --git a/src/lib/reasoners/th_util.mli b/src/lib/reasoners/th_util.mli index e0bc7301c..f1a13b5f2 100644 --- a/src/lib/reasoners/th_util.mli +++ b/src/lib/reasoners/th_util.mli @@ -26,6 +26,8 @@ (* *) (******************************************************************************) +(** An answer type. If it is Some (thing), then the answer is yes, + otherwise it is unknown. *) type answer = (Explanation.t * Expr.Set.t list) option diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index 9cf6287a6..b1d58be6d 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -31,7 +31,7 @@ open Typed (* Sat entry *) type sat_decl_aux = - | Assume of string * Expr.t * bool + | Assume of string * Expr.t * bool (* axioms / asserts *) | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t rwt_rule) list | Query of string * Expr.t * goal_sort diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index e77228dbe..8c4d038e2 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -32,7 +32,7 @@ open Typed (* Sat entry *) type sat_decl_aux = - | Assume of string * Expr.t * bool + | Assume of string * Expr.t * bool (* axioms / asserts *) | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t rwt_rule) list | Query of string * Expr.t * goal_sort diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index dd7e4400c..c378849fc 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -43,9 +43,9 @@ type t = view and view = { f: Sy.t; xs: t list; - ty: Ty.t; + ty: Ty.t; (* expression type *) bind : bind_kind; - tag: int; + tag: int; (* always = -42 *) vars : (Ty.t * int) SMap.t; (* vars to types and nb of occurences *) vty : Ty.Svty.t; depth: int; @@ -124,14 +124,14 @@ type lit_view = | Not_a_lit of { is_form : bool } type form_view = - | Unit of t*t (* unit clauses *) - | Clause of t*t*bool (* a clause (t1 or t2) bool <-> is implication *) + | Unit of t * t (* unit clauses *) + | Clause of t * t * bool (* a clause (t1 or t2) bool <-> is implication *) | Iff of t * t | Xor of t * t - | Literal of t (* an atom *) - | Lemma of quantified (* a lemma *) - | Skolem of quantified (* lazy skolemization *) - | Let of letin (* a binding of an expr *) + | Literal of t (* an atom *) + | Lemma of quantified (* a lemma *) + | Skolem of quantified (* lazy skolemization *) + | Let of letin (* a binding of an expr *) | Not_a_form @@ -2567,3 +2567,60 @@ type th_elt = let print_th_elt fmt t = Format.fprintf fmt "%s/%s: @[%a@]" t.th_name t.ax_name print t.ax_form + +module SimpExpr = + Simple_reasoner_expr.SimpleReasoner ( + struct + type nonrec t = t + let equal = equal + + let mk_term sy l typ = + match sy,l with + Sy.Form (Sy.F_Unit is_impl), f1 :: f2 :: [] -> + mk_and f1 f2 is_impl 0 + | Sy.Form (Sy.F_Unit _), _ -> + failwith "F_Unit not supported by simplifyer"; + + | Sy.Form (Sy.F_Clause is_impl), f1 :: f2 :: [] -> + mk_or f1 f2 is_impl 0 + | Sy.Form (Sy.F_Clause _), _ -> + failwith "F_Clause not supported by simplifyer"; + + | Sy.Form (Sy.F_Iff), [f1;f2] -> mk_iff f1 f2 0 + | Sy.Form (Sy.F_Iff), _ -> mk_nary_eq l + + | Sy.Form (Sy.F_Xor), f1 :: f2 :: [] -> mk_xor f1 f2 0 + | Sy.Form (Sy.F_Xor), _ -> + Format.eprintf "F_Xor not supported by simplifyer"; + assert false + + | Sy.Form (Sy.F_Lemma),_ + | Sy.Form (Sy.F_Skolem),_ -> failwith "Formula undefined." + + | Sy.Lit (Sy.L_eq),_ -> + mk_positive_lit sy (Sy.Lit (Sy.L_neg_eq)) l + | Sy.Lit (Sy.L_built b),_ -> + mk_positive_lit sy (Sy.Lit (Sy.L_neg_built b)) l + | Sy.Lit (Sy.L_neg_eq), _ -> + mk_positive_lit (Sy.Lit Sy.L_eq) (Sy.Lit Sy.L_neg_eq) l |> neg + | Sy.Lit (Sy.L_neg_built n), _ -> + mk_builtin ~is_pos:false n l + | Sy.Lit (Sy.L_neg_pred), _ -> + failwith "Lit (L_neg_pred) not supported by simplifyer" + | _ -> mk_term sy l typ + + let get_comp e = e.f + let get_sub_expr e = e.xs + let get_type e = e.ty + + let vrai = vrai + let faux = faux + + let real = real + let int = int + + let print = print + + let neg = neg + end + ) diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index db7607e0d..c9598c2a2 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -319,3 +319,10 @@ val is_pure : t -> bool val const_term : t -> bool (** return true iff the given argument is a term without arguments *) + +(** SimpExpr defines a simplifyer functor for expressions of type t + (defined in this file). *) +module SimpExpr : + functor + (D : Simple_reasoner_expr.Dom with type expr = t) + -> Simple_reasoner_expr.S with type expr = t and type v = D.v diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 579148f18..47032c427 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -30,9 +30,10 @@ open Format open Options type builtin = - LE | LT (* arithmetic *) - | IsConstr of Hstring.t (* ADT tester *) + LE | LT (** Arithmetic *) + | IsConstr of Hstring.t (** ADT tester *) +(** Operators on integer and reals, plus constructors/destructors & ITEs *) type operator = Plus | Minus | Mult | Div | Modulo | Concat | Extract | Get | Set | Fixed | Float @@ -45,18 +46,20 @@ type operator = | Destruct of Hstring.t * bool | Tite +(** Literals : relations between values *) type lit = - (* literals *) | L_eq | L_built of builtin | L_neg_eq | L_neg_built of builtin | L_neg_pred +(** Formulas : composition of expressions *) type form = - (* formulas *) - | F_Unit of bool - | F_Clause of bool + | F_Unit of bool (** F_Unit b <=> (AND), + b = true => the formula was an implication *) + | F_Clause of bool (** F_Clause b <=> (OR), + b = true => the formula was an implication *) | F_Iff | F_Xor | F_Lemma @@ -69,7 +72,6 @@ type bound_kind = VarBnd of Var.t | ValBnd of Numbers.Q.t type bound = (* private *) { kind : bound_kind; sort : Ty.t; is_open : bool; is_lower : bool } - type t = | True | False diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 13b48e548..3bf2726b5 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -136,6 +136,22 @@ and 'a tlet_kind = | TletTerm of 'a atterm | TletForm of 'a atform +(** Toplevel common components *) + +let true_atatom = {c=TAtrue; annot = new_id ()} +let false_atatom = {c=TAfalse; annot = new_id ()} + +let true_tform = TFatom true_atatom +let false_tform = TFatom false_atatom + +let true_atform = {c = true_tform; annot = new_id()} +let false_atform = {c = false_tform; annot = new_id()} + +let true_term = {tt_desc = TTconst Ttrue; tt_ty=Ty.Tbool} +let false_term = {tt_desc = TTconst Tfalse; tt_ty=Ty.Tbool} + +let true_atterm = {c = true_term; annot = new_id ()} +let false_atterm = {c = false_term; annot = new_id ()} (** Rewrite rules *) @@ -189,6 +205,200 @@ and 'a tdecl = | TPush of Loc.t * int | TPop of Loc.t * int +let eq_list eq l1 l2 = + let rec loop l1 l2 = + match l1, l2 with + [],[] -> true + | hd1 :: tl1, hd2 :: tl2 -> + if eq hd1 hd2 + then loop tl1 tl2 + else false + | _,_ -> false + in loop l1 l2 + +let eq_tconstant (c1 : tconstant) (c2 : tconstant) : bool = + match c1, c2 with + Tint s1, Tint s2 + | Tbitv s1, Tbitv s2 -> String.equal s1 s2 + | Treal n1, Treal n2 -> Num.eq_num n1 n2 + | Ttrue, Ttrue | Tfalse, Tfalse | Tvoid, Tvoid -> true + | _ -> false + +let eq_pattern (p1 : pattern) (p2 : pattern) : bool = + match p1, p2 with + Constr {name = name1; args = args1}, + Constr {name = name2; args = args2} -> + Hstring.equal name1 name2 + && + eq_list + (fun (x1,s1,t1) (x2,s2,t2) -> + Var.equal x1 x2 && + Hstring.equal s1 s2 && + Ty.equal t1 t2) + args1 + args2 + + | Var x1, Var x2 -> Var.equal x1 x2 + | _,_ -> false + +let rec eq_tterm (t1 : 'a tterm) (t2 : 'a tterm) : bool = + Ty.equal t1.tt_ty t2.tt_ty && eq_tt_desc t1.tt_desc t2.tt_desc + +and eq_tt_desc (e1 : 'a tt_desc) (e2 : 'a tt_desc) : bool = + match e1, e2 with + TTconst c1, TTconst c2 -> eq_tconstant c1 c2 + | TTvar v1, TTvar v2 -> Symbols.equal v1 v2 + | TTinfix (t11, symb1, t12), TTinfix (t21, symb2, t22) -> + Symbols.equal symb1 symb2 && + eq_tterm t11.c t21.c && + eq_tterm t12.c t22.c + + | TTprefix (s1,t1), TTprefix (s2, t2) -> + Symbols.equal s1 s2 && + eq_tterm t1.c t2.c + + | TTapp (s1, l1), TTapp (s2, l2) -> + Symbols.equal s1 s2 && + eq_list + (fun t1 t2 -> eq_tterm t1.c t2.c) + l1 l2 + + | TTmapsTo (x1, t1), TTmapsTo (x2, t2) -> + Var.equal x1 x2 && + eq_tterm t1.c t2.c + + | TTget (t11, t12), TTget (t21, t22) + | TTconcat (t11, t12), TTconcat (t21, t22) -> + eq_tterm t11.c t21.c && + eq_tterm t12.c t22.c + + | TTset (t11, t12, t13), TTset (t21, t22, t23) + | TTextract (t11, t12, t13), TTextract (t21, t22, t23) -> + eq_tterm t11.c t21.c && + eq_tterm t12.c t22.c && + eq_tterm t13.c t23.c + + | TTdot (t1, s1), TTdot (t2, s2) + | TTnamed (s1, t1), TTnamed (s2, t2) -> + Hstring.equal s1 s2 && + eq_tterm t1.c t2.c + + | TTrecord l1, TTrecord l2 -> + eq_list + (fun (s1,t1) (s2,t2) -> Hstring.equal s1 s2 && eq_tterm t1.c t2.c) + l1 l2 + + | TTlet (l1, t1), TTlet (l2, t2) -> + eq_tterm t1.c t2.c && + eq_list + (fun (s1, t1) (s2, t2) -> + Symbols.equal s1 s2 && eq_tterm t1.c t2.c) + l1 + l2 + + | TTite (c1,th1,el1), TTite (c2,th2,el2) -> + eq_tform c1.c c2.c && eq_tterm th1.c th2.c && eq_tterm el1.c el2.c + + | TTproject (b1,t1,s1), TTproject (b2,t2,s2) -> + (b1 && (not b2) || (not b1) && b2) + && eq_tterm t1.c t2.c && Hstring.equal s1 s2 + + | TTmatch (t1, l1), TTmatch (t2, l2) -> + eq_tterm t1.c t2.c && + eq_list + (fun (p1,t1) (p2,t2) -> + eq_pattern p1 p2 && eq_tterm t1.c t2.c + ) + l1 + l2 + + | TTform f1, TTform f2 -> eq_tform f1.c f2.c + | _,_ -> false + +and eq_tatom (a1 : 'a tatom) (a2 : 'a tatom) : bool = + match a1, a2 with + TAtrue, TAtrue + | TAfalse, TAfalse -> true + | TAeq l1, TAeq l2 + | TAdistinct l1, TAdistinct l2 + | TAneq l1, TAneq l2 + | TAle l1, TAle l2 + | TAlt l1, TAlt l2 -> + eq_list + (fun t1 t2 -> eq_tterm t1.c t2.c) + l1 + l2 + | TApred (t1, b1), TApred (t2, b2) -> + (b1 && (not b2) || (not b1) && b2) && + eq_tterm t1.c t2.c + | TTisConstr (t1, s1), TTisConstr (t2, s2) -> + Hstring.equal s1 s2 && eq_tterm t1.c t2.c + | _,_ -> false + +and eq_quant_form (q1 : 'a quant_form) (q2 : 'a quant_form) : bool = + let stylist = + eq_list + (fun (s1,t1) (s2, t2) -> Symbols.equal s1 s2 && Ty.equal t1 t2) + in + stylist q1.qf_bvars q2.qf_bvars && + stylist q1.qf_upvars q2.qf_upvars && + eq_list (fun f1 f2 -> eq_tform f1.c f2.c) q1.qf_hyp q2.qf_hyp && + eq_tform q1.qf_form.c q2.qf_form.c && + eq_list + (fun (tlist1,b1) (tlist2,b2) -> + (b1 && (not b2) || (not b1) && b2) && + eq_list + (fun t1 t2 -> eq_tterm t1.c t2.c) + tlist1 + tlist2) + q1.qf_triggers + q2.qf_triggers + +and eq_tform (f1 : 'a tform) (f2 : 'a tform) : bool = + match f1, f2 with + | TFatom a1, TFatom a2 -> eq_tatom a1.c a2.c + + | TFop (op1, l1), TFop (op2, l2) -> + (Stdlib.(=)) op1 op2 && + eq_list + (fun f1 f2 -> eq_tform f1.c f2.c) + l1 + l2 + + | TFforall q1, TFforall q2 + | TFexists q1, TFexists q2 -> + eq_quant_form q1 q2 + + | TFlet (stlist1, slklist1,f1), TFlet (stlist2, slklist2,f2) -> + let stylist = + eq_list + (fun (s1,t1) (s2, t2) -> Symbols.equal s1 s2 && Ty.equal t1 t2) + in + stylist stlist1 stlist2 && + eq_list + (fun (s1,lf1) (s2, lf2) -> Symbols.equal s1 s2 && eq_tlet_kind lf1 lf2) + slklist1 slklist2 + && + eq_tform f1.c f2.c + + | TFnamed (s1, f1), TFnamed (s2, f2) -> + Hstring.equal s1 s2 && eq_tform f1.c f2.c + + | TFmatch (t1, pfl1), TFmatch (t2, pfl2) -> + eq_tterm t1.c t2.c && + eq_list + (fun (p1, f1) (p2, f2) -> eq_pattern p1 p2 && eq_tform f1.c f2.c) + pfl1 + pfl2 + + | _,_ -> false + +and eq_tlet_kind (k1 : 'a tlet_kind) (k2 : 'a tlet_kind) : bool = + match k1, k2 with + TletTerm t1, TletTerm t2 -> eq_tterm t1.c t2.c + | TletForm f1, TletForm f2 -> eq_tform f1.c f2.c + | _,_ -> false + (*****) let string_of_op = function @@ -196,164 +406,211 @@ let string_of_op = function | OPor -> "or" | OPimp -> "->" | OPiff -> "<->" + | OPxor -> "xor" + | OPif -> "ite" | _ -> assert false +type 'annot annot_printer = Format.formatter -> 'annot -> unit +type ('a,'annot) annoted_printer = + Format.formatter -> ('a,'annot) annoted -> unit + +let (no_print : _ annot_printer) = fun fmt _ -> fprintf fmt "" +let (int_print : int annot_printer) = fun fmt -> fprintf fmt ".%i" + +let print_annot + (pp_annot : 'annot annot_printer) + (print : ('a,'annot) annoted_printer) + (fmt : Format.formatter) (t : ('a, 'annot) annoted) = + fprintf fmt "%a%a" print t pp_annot t.annot + let print_binder fmt (s, t) = fprintf fmt "%a :%a" Symbols.print s Ty.print t let print_binders fmt l = List.iter (fun c -> fprintf fmt "%a, " print_binder c) l -let rec print_term fmt t = match t.c.tt_desc with - | TTconst Ttrue -> - fprintf fmt "true" - | TTconst Tfalse -> - fprintf fmt "false" - | TTconst Tvoid -> - fprintf fmt "void" - | TTconst (Tint n) -> - fprintf fmt "%s" n - | TTconst (Treal n) -> - fprintf fmt "%s" (Num.string_of_num n) - | TTconst Tbitv s -> - fprintf fmt "%s" s - | TTvar s -> - fprintf fmt "%a" Symbols.print s - | TTapp(s,l) -> - fprintf fmt "%a(%a)" Symbols.print s print_term_list l - | TTinfix(t1,s,t2) -> - fprintf fmt "%a %a %a" print_term t1 Symbols.print s print_term t2 - | TTprefix (s, t') -> - fprintf fmt "%a %a" Symbols.print s print_term t' - | TTget (t1, t2) -> - fprintf fmt "%a[%a]" print_term t1 print_term t2 - | TTset (t1, t2, t3) -> - fprintf fmt "%a[%a<-%a]" print_term t1 print_term t2 print_term t3 - | TTextract (t1, t2, t3) -> - fprintf fmt "%a^{%a,%a}" print_term t1 print_term t2 print_term t3 - | TTconcat (t1, t2) -> - fprintf fmt "%a @ %a" print_term t1 print_term t2 - | TTdot (t1, s) -> - fprintf fmt "%a.%s" print_term t1 (Hstring.view s) - | TTrecord l -> - fprintf fmt "{ "; - List.iter - (fun (s, t) -> fprintf fmt "%s = %a" (Hstring.view s) print_term t) l; - fprintf fmt " }" - | TTlet (binders, t2) -> - fprintf fmt "let %a in %a" print_term_binders binders print_term t2 - | TTnamed (_, t) -> - fprintf fmt "%a" print_term t - - | TTinInterval(e, i, j) -> - fprintf fmt "%a in %a, %a" - print_term e - Symbols.print_bound i - Symbols.print_bound j - - | TTmapsTo(x,e) -> - fprintf fmt "%a |-> %a" Var.print x print_term e - - | TTite(cond, t1, t2) -> - fprintf fmt "(if %a then %a else %a)" - print_formula cond print_term t1 print_term t2 - | TTproject (grded, t1, s) -> - fprintf fmt "%a#%s%s" - print_term t1 (if grded then "" else "!") (Hstring.view s) - - | TTform f -> - fprintf fmt "%a" print_formula f - - | TTmatch (e, cases) -> - let pp_vars fmt l = - match l with - [] -> () - | [e,_,_] -> Var.print fmt e - | (e,_,_) :: l -> - fprintf fmt "(%a" Var.print e; - List.iter (fun (e,_,_) -> fprintf fmt ", %a" Var.print e) l; - fprintf fmt ")" - in - fprintf fmt "match %a with\n" print_term e; - List.iter - (fun (p, v) -> - match p with - | Constr {name = n; args = l} -> - fprintf fmt "| %a %a -> %a\n" Hstring.print n pp_vars l print_term v - | Var x -> - fprintf fmt "| %a -> %a\n" Var.print x print_term v; - )cases; - fprintf fmt "end@." - -and print_term_binders fmt l = +let rec print_term ?(annot=no_print) fmt t = + let printer fmt t = + match t.c.tt_desc with + | TTconst Ttrue -> + fprintf fmt "true" + | TTconst Tfalse -> + fprintf fmt "false" + | TTconst Tvoid -> + fprintf fmt "void" + | TTconst (Tint n) -> + fprintf fmt "%s" n + | TTconst (Treal n) -> + fprintf fmt "%s" (Num.string_of_num n) + | TTconst Tbitv s -> + fprintf fmt "%s" s + | TTvar s -> + fprintf fmt "%a" Symbols.print s + | TTapp(s,l) -> + fprintf fmt "%a(%a)" Symbols.print s (print_term_list ~annot) l + | TTinfix(t1,s,t2) -> + fprintf + fmt + "%a %a %a" + (print_term ~annot) t1 + Symbols.print s + (print_term ~annot) t2 + | TTprefix (s, t') -> + fprintf fmt "%a %a" Symbols.print s (print_term ~annot) t' + | TTget (t1, t2) -> + fprintf fmt "%a[%a]" (print_term ~annot) t1 (print_term ~annot) t2 + | TTset (t1, t2, t3) -> + fprintf + fmt + "%a[%a<-%a]" + (print_term ~annot) t1 + (print_term ~annot) t2 + (print_term ~annot) t3 + | TTextract (t1, t2, t3) -> + fprintf + fmt + "%a^{%a,%a}" + (print_term ~annot) t1 + (print_term ~annot) t2 + (print_term ~annot) t3 + | TTconcat (t1, t2) -> + fprintf fmt "%a @ %a" (print_term ~annot) t1 (print_term ~annot) t2 + | TTdot (t1, s) -> + fprintf fmt "%a.%s" (print_term ~annot) t1 (Hstring.view s) + | TTrecord l -> + fprintf fmt "{ "; + List.iter + (fun (s, t) -> + fprintf fmt "%s = %a" (Hstring.view s) (print_term ~annot) t) l; + fprintf fmt " }" + | TTlet (binders, t2) -> + fprintf + fmt + "let %a in %a" + (print_term_binders ~annot) binders + (print_term ~annot) t2 + | TTnamed (_, t) -> + fprintf fmt "%a" (print_term ~annot) t + + | TTinInterval(e, i, j) -> + fprintf fmt "%a in %a, %a" + (print_term ~annot) e + Symbols.print_bound i + Symbols.print_bound j + + | TTmapsTo(x,e) -> + fprintf fmt "%a |-> %a" Var.print x (print_term ~annot) e + + | TTite(cond, t1, t2) -> + fprintf fmt "(if %a then %a else %a)" + (print_formula ~annot) cond + (print_term ~annot) t1 + (print_term ~annot) t2 + | TTproject (grded, t1, s) -> + fprintf fmt "%a#%s%s" + (print_term ~annot) t1 (if grded then "" else "!") (Hstring.view s) + + | TTform f -> + fprintf fmt "%a" (print_formula ~annot) f + + | TTmatch (e, cases) -> + let pp_vars fmt l = + match l with + [] -> () + | [e,_,_] -> Var.print fmt e + | (e,_,_) :: l -> + fprintf fmt "(%a" Var.print e; + List.iter (fun (e,_,_) -> fprintf fmt ", %a" Var.print e) l; + fprintf fmt ")" + in + fprintf fmt "match %a with\n" (print_term ~annot) e; + List.iter + (fun (p, v) -> + match p with + | Constr {name = n; args = l} -> + fprintf + fmt + "| %a %a -> %a\n" + Hstring.print n + pp_vars l + (print_term ~annot) v + | Var x -> + fprintf fmt "| %a -> %a\n" Var.print x (print_term ~annot) v; + )cases; + fprintf fmt "end@." + in + print_annot annot printer fmt t + +and print_term_binders ?(annot=no_print) fmt l = match l with | [] -> assert false | (sy, t) :: l -> - fprintf fmt "%a = %a" Symbols.print sy print_term t; + fprintf fmt "%a = %a" Symbols.print sy (print_term ~annot) t; List.iter (fun (sy, t) -> - fprintf fmt ", %a = %a" Symbols.print sy print_term t) l + fprintf fmt ", %a = %a" Symbols.print sy (print_term ~annot) t) l -and print_term_list fmt = List.iter (fprintf fmt "%a," print_term) +and print_term_list ?(annot=no_print) fmt = List.iter (fprintf fmt "%a," (print_term ~annot)) -and print_atom fmt a = +and print_atom ?(annot=no_print) fmt a = match a.c with | TAtrue -> fprintf fmt "True" | TAfalse -> fprintf fmt "True" | TAeq [t1; t2] -> - fprintf fmt "%a = %a" print_term t1 print_term t2 + fprintf fmt "%a = %a" (print_term ~annot) t1 (print_term ~annot) t2 | TAneq [t1; t2] -> - fprintf fmt "%a <> %a" print_term t1 print_term t2 + fprintf fmt "%a <> %a" (print_term ~annot) t1 (print_term ~annot) t2 | TAle [t1; t2] -> - fprintf fmt "%a <= %a" print_term t1 print_term t2 + fprintf fmt "%a <= %a" (print_term ~annot) t1 (print_term ~annot) t2 | TAlt [t1; t2] -> - fprintf fmt "%a < %a" print_term t1 print_term t2 + fprintf fmt "%a < %a" (print_term ~annot) t1 (print_term ~annot) t2 | TApred (t, negated) -> - if negated then fprintf fmt "(not (%a))" print_term t - else print_term fmt t + if negated then fprintf fmt "(not (%a))" (print_term ~annot) t + else (print_term ~annot) fmt t | TTisConstr (t1, s) -> - fprintf fmt "%a ? %s" print_term t1 (Hstring.view s) + fprintf fmt "%a ? %s" (print_term ~annot) t1 (Hstring.view s) | TAdistinct l -> - fprintf fmt "distinct(%a)" print_term_list l + fprintf fmt "distinct(%a)" (print_term_list ~annot) l | _ -> assert false -and print_triggers fmt l = - List.iter (fun (tr, _) -> fprintf fmt "%a | " print_term_list tr) l +and print_triggers ?(annot=no_print) fmt l = + List.iter (fun (tr, _) -> fprintf fmt "%a | " (print_term_list ~annot) tr) l -and print_formula fmt f = +and print_formula ?(annot=no_print) fmt f = match f.c with | TFatom a -> print_atom fmt a | TFop(OPnot, [f]) -> - fprintf fmt "not %a" print_formula f + fprintf fmt "not %a" (print_formula ~annot) f | TFop(OPif, [cond; f1;f2]) -> fprintf fmt "if %a then %a else %a" - print_formula cond print_formula f1 print_formula f2 + (print_formula ~annot) cond (print_formula ~annot) f1 (print_formula ~annot) f2 | TFop(op, [f1; f2]) -> - fprintf fmt "%a %s %a" print_formula f1 (string_of_op op) print_formula 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 t print_formula f + print_binders l (print_triggers ~annot) t (print_formula ~annot) f | TFlet (_, binders, f) -> List.iter (fun (sy, let_e) -> fprintf fmt " let %a = " Symbols.print sy; match let_e with - | TletTerm t -> fprintf fmt "%a in@." print_term t - | TletForm f -> fprintf fmt "%a in@." print_formula f + | TletTerm t -> fprintf fmt "%a in@." (print_term ~annot) t + | TletForm f -> fprintf fmt "%a in@." (print_formula ~annot) f )binders; - fprintf fmt "%a" print_formula f + fprintf fmt "%a" (print_formula ~annot) f | _ -> fprintf fmt "(formula pprint not implemented)" (* let rec print_tdecl fmt = function + | TTheory (_, name, _, l) -> Format.fprintf fmt "th %s: @[%a@]" name (Util.print_list_pp ~sep:Format.pp_print_space ~pp:print_atdecl) l - | TAxiom (_, name, kind, f) -> - Format.fprintf fmt "ax %s: @[%a@]" name print_formula f + | TAxiom (_, name, _kind, f) -> + Format.fprintf fmt "ax %s: @[%a@]" name (print_formula ~annot) f | TRewriting (_, name, l) -> Format.fprintf fmt "rwt %s: @[%a@]" name (Util.print_list_pp ~sep:Format.pp_print_space @@ -365,7 +622,8 @@ let rec print_tdecl fmt = function | TPop (_loc,n) -> Format.fprintf fmt "pop %d" n -and print_atdecl fmt a = print_tdecl fmt a.c +and print_atdecl ?(annot=no_print) fmt a = + print_annot annot (fun fmt a -> print_tdecl ~annot fmt a.c) fmt a *) let fresh_hypothesis_name = diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli index ea03e419e..e21aaa0bd 100644 --- a/src/lib/structures/typed.mli +++ b/src/lib/structures/typed.mli @@ -306,24 +306,85 @@ and 'a tdecl = (* TODO: wrap this in a record to factorize away the location and name of the declaration ? *) +(** {5. Toplevel constants} *) +val true_atatom : int atatom +val false_atatom : int atatom -(** {5 Printing} *) +val true_tform : int tform +val false_tform : int tform -val print_term : Format.formatter -> _ atterm -> unit -(** Print annoted typed terms. Ignore the annotations. *) +val true_atform : int atform +val false_atform : int atform -val print_formula : Format.formatter -> _ atform -> unit -(**Print annoted typed formulas; Ignores the annotations. *) +val true_term : int tterm +val false_term : int tterm + +val true_atterm : int atterm +val false_atterm : int atterm + +(** {6. Structural equality} *) + +val eq_tterm : 'a tterm -> 'a tterm -> bool + +val eq_tt_desc : 'a tt_desc -> 'a tt_desc -> bool + +val eq_tatom : 'a tatom -> 'a tatom -> bool + +val eq_quant_form : 'a quant_form -> 'a quant_form -> bool + +val eq_tform : 'a tform -> 'a tform -> bool + +val eq_tlet_kind : 'a tlet_kind -> 'a tlet_kind -> bool + +(** {7 Printing} *) + +val string_of_op : oplogic -> string + +type 'annot annot_printer = Format.formatter -> 'annot -> unit +type ('a,'annot) annoted_printer = + Format.formatter -> ('a,'annot) annoted -> unit + +val no_print : _ annot_printer +val int_print : int annot_printer + +val print_atom : + ?annot: 'annot annot_printer -> Format.formatter -> 'annot atatom -> unit + +(** Print annoted typed terms. If no annot function is given, ignores + the annotations. *) +val print_term : + ?annot: 'annot annot_printer -> Format.formatter -> 'annot atterm -> unit + +(** Print annoted typed formulas. If no annot function is given, ignores + the annotations. *) +val print_formula : + ?annot: 'annot annot_printer -> Format.formatter -> 'annot atform -> unit -val print_binders : Format.formatter -> (Symbols.t * Ty.t) list -> unit (** Print a list of bound typed variables. *) +val print_binders : Format.formatter -> (Symbols.t * Ty.t) list -> unit -val print_triggers : Format.formatter -> ('a atterm list * bool) list -> unit +val print_triggers : + ?annot: 'annot annot_printer -> + Format.formatter -> ('annot atterm list * bool) list -> unit (** Print a list of triggers. *) val print_goal_sort : Format.formatter -> goal_sort -> unit (** Print a goal sort *) +(* +val print_tdecl : + ?annot: 'annot annot_printer -> + Format.formatter -> 'annot tdecl -> unit + +val print_atdecl : + ?annot: 'annot annot_printer -> Format.formatter -> 'annot atdecl -> unit +*) + +val print_annot : + 'annot annot_printer -> + ('a,'annot) annoted_printer -> + Format.formatter -> ('a,'annot) annoted -> unit + val print_rwt : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a rwt_rule -> unit diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 4504acec3..dc72e7afd 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -488,6 +488,9 @@ let status = ref Status_Unknown let session_file = ref "" let used_context_file = ref "" let js_mode = ref false +let simplify = ref Util.SNo +let simplify_th = ref true +let simplify_verbose = ref true let set_timers b = timers := b let set_status s = status := match_known_status s @@ -495,6 +498,9 @@ let set_file f = file := f let set_session_file f = session_file := f let set_used_context_file f = used_context_file := f let set_js_mode b = js_mode := b +let set_simplify s = simplify := s +let set_simplify_th b = simplify_th := b +let set_simplify_verbose b = simplify_verbose := b let get_timers () = !timers || !profiling let get_file () = !file @@ -502,6 +508,9 @@ let get_status () = !status let get_session_file () = !session_file let get_used_context_file () = !used_context_file let get_js_mode () = !js_mode +let get_simplify () = !simplify +let get_simplify_th () = !simplify_th +let get_simplify_verbose () = !simplify_verbose (** particular getters : functions that are immediately executed **************) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 308dbaae6..b166ca53f 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -274,6 +274,15 @@ val set_file : string -> unit (** Updates the filename to be parsed and sets a js_mode flag *) val set_file_for_js : string -> unit +(** Set [simplify] accessible with {!val:get_simplify} *) +val set_simplify : Util.simplify -> unit + +(** Set [simplify_th] accessible with {!val:get_simplify_th} *) +val set_simplify_th : bool -> unit + +(** Set [simplify_verbose] accessible with {!val:get_simplify_verbose} *) +val set_simplify_verbose : bool -> unit + (** Setters used by parse_command *) (** Set [case_split_policy] accessible with {!val:get_case_split_policy} *) @@ -962,6 +971,18 @@ val get_status : unit -> known_status val get_js_mode : unit -> bool (** Default to [false] *) +(** [true] if simplification is activated *) +val get_simplify : unit -> Util.simplify +(** Default to [true] *) + +(** Gets the simplify mode: [false] => no theory used *) +val get_simplify_th : unit -> bool +(** Default to [true] *) + +(** Gets the simplify verbose mode: [false] => no verbose *) +val get_simplify_verbose : unit -> bool +(** Default to [false] *) + (** Value specifying the file given to Alt-Ergo *) val get_file : unit -> string (** Default to [""] *) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index 672173403..1815cda8a 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -54,6 +54,11 @@ type theories_extensions = | NIA | FPA +type simplify = + | SNo + | SPreprocess + | SAll + type axiom_kind = Default | Propagator let th_ext_of_string ext = diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 65699b9b3..3c95df223 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -49,6 +49,11 @@ type theories_extensions = | NIA | FPA +type simplify = + | SNo + | SPreprocess + | SAll + type axiom_kind = Default | Propagator val th_ext_of_string : string -> theories_extensions option From be706bbceecb6de7397964103fabea769f8e8760 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 2 Mar 2021 08:35:28 +0100 Subject: [PATCH 02/18] First version of AI preprocessing --- src/bin/common/parse_command.ml | 3 +- src/lib/dune | 2 +- src/lib/frontend/cnf.ml | 23 +- src/lib/frontend/simple_reasoner_expr.ml | 537 ++++++++++------------ src/lib/frontend/simple_reasoner_expr.mli | 41 +- src/lib/reasoners/intervals.ml | 31 ++ src/lib/reasoners/intervals.mli | 2 + src/lib/reasoners/polynome.ml | 31 ++ src/lib/reasoners/polynome.mli | 17 + src/lib/reasoners/simplifiers.ml | 446 ++++++++++++++++++ src/lib/structures/expr.ml | 58 +-- src/lib/structures/expr.mli | 9 +- 12 files changed, 792 insertions(+), 408 deletions(-) create mode 100644 src/lib/reasoners/simplifiers.ml diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index fdb9b091e..223dbb170 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -436,7 +436,7 @@ let halt_opt version_info where = with Failure f -> `Error (false, f) | Error (b, m) -> `Error (b, m) -let mk_opts file () () () () () () halt_opt (gc) () () () () () () () () +let mk_opts file () () () () () () halt_opt (gc) () () () () () () () () () = if halt_opt then `Ok false @@ -482,6 +482,7 @@ let s_sat = "SAT OPTIONS" let s_term = "TERM OPTIONS" let s_theory = "THEORY OPTIONS" let s_fmt = "FORMATTER OPTIONS" +let s_simp = "SIMPLIFIER" (* Parsers *) diff --git a/src/lib/dune b/src/lib/dune index 5980a6b5e..f21a95085 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -29,7 +29,7 @@ ; modules that make up the lib (modules ; frontend - Simple_reasoner_expr + Simple_reasoner_expr Simplifiers Cnf Input Frontend Parsed_interface Typechecker ; reasoners Ac Arith Arrays Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 54d74e145..573daeff9 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -35,29 +35,14 @@ module E = Expr module Sy = Symbols module SE = E.Set module SRE = Simple_reasoner_expr - -(** Simplifyer not using the theory *) -module DummySimp = - Expr.SimpExpr - (struct - type expr = Expr.t - type v = unit - let top = () - let bottom = () - let compare _ _ = Some 0 - let join _ _ = () - let add_constraint _ _ = () - let vrai = () - let faux = () - end - ) +module Smp = Simplifiers let choose_preproc () : - (module Simple_reasoner_expr.S with type expr = Expr.t and type v = unit) = + (module Simple_reasoner_expr.S) = if not (Options.get_simplify_th ()) then - (module DummySimp) + (module Smp.DummySimp) else - (module DummySimp) + (module Smp.IntervalsSimp) module SimpExprPreproc () = (val (choose_preproc ())) diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index 4d94104a2..55e44d770 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -9,6 +9,9 @@ (* *) (******************************************************************************) +module E = Expr +module Sy = Symbols + let verb = Options.get_simplify_verbose let silent (msg : ('a, Format.formatter, unit) format) = @@ -116,6 +119,11 @@ let get_expr e = e.exp let get_abs_val e = e.v let has_changed e = e.diff +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 *) (** As the simplifyer interacts with different components of alt-ergo, @@ -127,7 +135,6 @@ let has_changed e = e.diff module type Dom = sig type v - type expr (** Top/Bottom value *) val top : v @@ -140,232 +147,131 @@ sig val join : v -> v -> v (** Add constraint *) - val add_constraint : expr -> v -> v + val add_constraint : Expr.t -> Expr.t -> Symbols.lit -> v -> v add_constraint_res - (** Constants *) - val vrai : v - val faux : v -end - -module type Expr = sig - type t - val equal : t -> t -> bool - val mk_term : Symbols.t -> t list -> Ty.t -> t - val get_comp : t -> Symbols.t - val get_sub_expr : t -> t list - val get_type : t -> Ty.t - val neg : t -> t - val vrai : t - val faux : t - val int : string -> t - val real : string -> t - val print : Format.formatter -> t -> unit + val pp : Format.formatter -> v -> unit end (** This is the signature of the simplifyer. *) module type S = sig type v - type expr (** Simplifies an expression. *) - val simp_expr : expr -> (expr, v) simp + val simp_expr : Expr.t -> (Expr.t, v) simp end - module SimpleReasoner - (E : Expr) - (D : Dom with type expr = E.t) - : S with type v = D.v and type expr = E.t = struct - type expr = E.t + (D : Dom) + : S with type v = D.v = struct type v = D.v let identity v exp = {exp; diff = false; v} (* - - let diff_list (l : ('a, 'expl) simp list) : (('a list), 'expl) simp = - let rev = - List.fold_left - (fun acc s -> - {exp = s.exp :: acc.exp; - diff = acc.diff || s.diff; - v = D.join acc.v s.v - } - ) - (identity []) - l - in - {rev with exp = List.rev rev.exp} - (* Check is an expression has an arithmetic type (Some true), - a boolean type (Some false) or else (None). *) - let is_arith (e : expr) : bool option = - match E.get_type e with - Ty.Tbool -> Some false - | Ty.Tint | Ty.Treal - | Ty.Tvar {value = Some Ty.Tint;_} - | Ty.Tvar {value = Some Ty.Treal;_} -> Some true - | _ -> None - - let value_from_query (e : expr) : (value * expl) option = - match is_arith e with - Some true -> ( - match T.q_query e !env with - Some (res_query, expl) -> - Some ((Num res_query), expl) - | None -> None - ) - | Some false -> ( - match T.bool_query e !env with - Some (res_query, expl) -> - Some ((Bool res_query), expl) - | None -> None - ) - | None -> None - - let expr_to_value (e : expr) : (value * expl) option = - match E.get_comp e with - True -> Some ((Bool true), no_reason) - | False -> Some ((Bool false), no_reason) - | Int s -> Some ((Num (Q.of_string (Hstring.view s))), no_reason) - | Real s -> Some ((Num (Q.of_string (Hstring.view s))), no_reason) - | _ -> value_from_query e - - let value_to_expr (ty : Ty.t) (v : value) : expr = - debug "Type = %a@." Ty.print ty; - match v with - Bool true -> E._true - | Bool false -> E._false - | Num i -> - let i' = Q.to_string i in - if ty == Ty.Treal - then E.real i' - else E.int i' - - let arith - (ty : Ty.t) - (op : value -> value -> value) - (e_list : expr list): (expr list, expl) simp = - (* Wrapper for op. Checks that it has been called. - If it has never been called, then there have been no - simplification. *) - let op_has_been_called = ref 0 in - let op v1 v2 = - op_has_been_called := !op_has_been_called + 1 ; - debug "Calling operator@."; - op v1 v2 - in - - let vals,expl,exprs = - fold_left - (fun (acc_solved,acc_expl,acc_remain) v -> - match expr_to_value v with - None -> (acc_solved, acc_expl, v :: acc_remain) - | Some (v, expl) -> - let new_expl = Expl.union expl acc_expl in - match acc_solved with - None -> - (Some v, new_expl, acc_remain) - | Some old_v -> (Some (op old_v v), new_expl, acc_remain) - ) - (None, Expl.empty, []) - e_list - in - if !op_has_been_called = 0 - then - begin - debug "Operator has not been called.@."; - identity e_list - end - else - match vals with - None -> identity e_list - | Some v -> - let cst_expr = value_to_expr ty v in - debug "Result of simplifyable operations : %a@." E.pretty cst_expr; - {v = List.rev exprs @ [value_to_expr ty v]; diff = true; expl} - - let oper (op : value -> value -> bool) (l : expr list) : bool * bool * expl = - (* all_true is a boolean stating that every call of 'op' returned 'true'. - set to true at the beginning, it is set to false if one of the - list term. - last_val is the last value that has been accepted by the test - acc_expl is the accumulated explanations of each value tested - *) - let rec _oper - (all_true : bool) - (last_val : value option) - (acc_expl : expl) - (l : expr list) : bool * bool * expl = - match l with - [] -> (* No more elements, and none failed the test. *) - false, all_true, acc_expl - | hd :: tl -> - let hd_val = expr_to_value hd in - match hd_val, last_val with - | None, None -> - _oper false None acc_expl tl - - | Some (v, expl), None -> - _oper - all_true - (Some v) - (Expl.union expl acc_expl) - tl - - | None, Some v -> - _oper false (Some v) acc_expl tl - - | Some (v, expl), Some v' -> - let res = op v v' in - debug "Result : %a (op) %a = %b@." - pp_val v' pp_val v res; - if op v' v - then ( - _oper all_true (Some v') (Expl.union expl acc_expl) tl - ) - else (* The operation is not respected *) ( - true, false, (Expl.union expl acc_expl) - ) - in - _oper true None no_reason l - - let apply_op - (op : value -> value -> bool) - (l : expr list) : (expr list, expl) simp = - let falsify,all_true,expl = oper op l in - if falsify - then {v = [E._false]; diff = true; expl} - else if all_true - then {v = [E._true]; diff = true; expl} - else {v = l; diff = false; expl} - - let is_unary (o : Symbols.operator) : bool = - let open Symbols in - match o with - | Plus | Minus | Mult | Div | Modulo - | Concat | Extract | Get | Set | Fixed | Float - | Reach | Record | Min_real | Min_int | Max_real | Max_int - | Integer_log2 | Pow | Tite -> false - - | Access _ - | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil - | Sqrt_real_default | Sqrt_real_excess | Integer_round - | Constr _ - | Destruct (_,_) -> true *) - let (|=) v1 v2 = match D.compare v1 v2 with | Some i -> i = 0 - | None -> false + | None -> false*) + + let simp_true = {exp = E.vrai; diff = true; v = D.top} + let simp_false = {exp = E.faux; diff = true; v = D.top} + + let is_true e = E.equal e.exp E.vrai + let is_false e = E.equal e.exp E.faux + + let rec add_lit_constraint (v : v) (e : Expr.t) = + let exception Stop of v add_constraint_res in + match E.lit_view e with + | Eq (e1, e2) -> + debug "[add_lit_constraint] Eq@."; + D.add_constraint e1 e2 Sy.L_eq v + + | Eql [] -> assert false + | Eql (hd :: tl) -> begin try + debug "[add_lit_constraint] Eql@."; + NewConstraint ( + List.fold_left + (fun v e -> + match D.add_constraint hd e Sy.L_eq v with + | AlreadyTrue -> v + | AlreadyFalse -> raise (Stop AlreadyFalse) + | NewConstraint v' -> v' + ) v tl + ) + with Stop res -> res + end + | Distinct [] -> assert false + | Distinct (hd :: tl) -> begin try + debug "[add_lit_constraint] Distinct@."; + NewConstraint ( + List.fold_left + (fun v e -> + match D.add_constraint hd e Sy.L_neg_eq v with + | AlreadyTrue -> v + | AlreadyFalse -> raise (Stop AlreadyFalse) + | NewConstraint v' -> v') v tl) + with Stop res -> res + end + | Builtin (_, btin, [e1; e2]) -> begin + match D.add_constraint e1 e2 (Sy.L_built btin) v with + | AlreadyTrue -> + debug "[add_lit_constraint] Already true@."; + AlreadyTrue + | AlreadyFalse -> + debug "[add_lit_constraint] Already false@."; + AlreadyFalse + | NewConstraint v' -> + debug "[add_lit_constraint] New constraint: %a@." + D.pp v'; + NewConstraint v' + end + | Builtin (_, _, _) -> failwith "Unhandled builtin" + | Pred _ -> + debug "[add_lit_constraint] Pred@."; + NewConstraint v + | Not_a_lit _ -> + debug "[add_lit_constraint] Not a lit@."; + failwith "add_lit_constraint should be only called on litterals" + (* + and add_form_constraint (v : v) (e : Expr.t) = + match E.form_view e with + | E.Unit (f1, f2) -> begin + match add_lit_constaint v f1 with + | AlreadyFalse -> + + end + add_lit_constraint (add_lit_constraint v f1) f2 + + | Clause (f1, f2, _) -> + let v1 = add_lit_constraint v f1 in + let v2 = add_lit_constraint v f2 in + D.join v1 v2 + + | Iff (f1, f2) -> + let pos = add_lit_constraint (add_lit_constraint v f1) f2 in + let neg = add_lit_constraint (add_lit_constraint v (E.neg f1)) (E.neg f2) in + D.join pos neg - let (&&&) v e = D.add_constraint e v + | Xor (f1, f2) -> + let v1 = add_lit_constraint (add_lit_constraint v f1) (E.neg f2) in + let v2 = add_lit_constraint (add_lit_constraint v (E.neg f1)) f2 in + D.join v1 v2 + | Literal e -> add_lit_constraint v e + + | Lemma _ | Skolem _ | Not_a_form -> v + + | Let _ -> failwith "todo" + *) + + and (&&&) v e = + add_lit_constraint v e +(* let is_true v = v |= D.vrai let is_false v = v |= D.faux +*) - let simp_true = {exp = E.vrai; diff = true; v = D.vrai} - let simp_false = {exp = E.faux; diff = true; v = D.faux} (* let is_constr (constr : Hstring.t) (e : expr) : bool option = @@ -373,116 +279,148 @@ module SimpleReasoner | Op (Constr s') -> Some (Hstring.equal constr s') | _ -> None*) - let rec simp_ite + and simp_ite (state : v) - (cond : expr) - (th : expr) - (el : expr) : - (expr, v) simp list = - let scond : (expr, v) simp = simp_expr state cond in - if is_true scond.v then - let th : (expr, v) simp = simp_expr state th in + (cond : E.t) + (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; + 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 + debug "[simp_ite] It is true, ending@."; + let th : (E.t, v) simp = simp_expr state th in [{th with diff = true}] - else if is_false scond.v then - let el : (expr, v) simp = simp_expr state el in + 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}] - else - let neg_cond = E.neg scond.exp in - let sth : (expr, v) simp = simp_expr (state &&& scond.exp) th in - let sel : (expr, v) simp = simp_expr (state &&& neg_cond) el in - if scond.diff || sth.diff || sel.diff then - [scond; sth; sel] - else [ - identity scond.v cond; - identity sth.v th; - identity sel.v el] + end else let cth = scond.v in begin + let neg_cond = E.neg scond.exp in + match state &&& neg_cond with + | AlreadyTrue -> + debug "[simp_ite] Negation is true, ending@."; + let el : (E.t, v) simp = simp_expr state el in + [{el with diff = true}] + | AlreadyFalse -> + debug "[simp_ite] Negation is fakse, ending@."; + let th : (E.t, v) simp = simp_expr state th in + [{th with diff = true}] + | 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 + if scond.diff || sth.diff || sel.diff then + [scond; sth; sel] + else [ + identity scond.v cond; + identity sth.v th; + identity sel.v el] + end and simp_form (state : v) (f : Symbols.form) - (elist : expr list) - : v * (expr, v) simp list = - match f with - | Symbols.F_Unit _ -> begin (* <=> AND *) - let () = debug "F_Unit@." in - let state,rev_res = - fold_left_stop - (fun (state, simp_exps) e -> - let esimp : (expr, v) simp = simp_expr state e in - if is_true esimp.v then ( - debug "%a = true@." E.print e; - (state, simp_exps), false - ) - else if is_false esimp.v then ( - debug "%a = false@." E.print e; - (D.faux, [simp_false]), true - ) else ( - debug "Keeping %a@." E.print e; - (state &&& esimp.exp, esimp :: simp_exps), false - ) - ) - (state, []) - elist - in - match rev_res with - | [] -> D.vrai, [simp_true] - | _ -> state, List.rev rev_res - end - - | F_Clause _ -> begin (* <=> OR *) - let () = debug "F_Clause@." in - let state, rev_res = - fold_left_stop - (fun (state, simp_exps) e -> - let (esimp : (expr, v) simp) = simp_expr state e in - if is_false esimp.v then ( - debug "%a = false@." E.print e; - (state, simp_exps), false - ) - else if is_true esimp.v then ( - debug "%a = true@." E.print e; - (D.vrai, [simp_true]), true - ) - else ( - debug "Keeping %a@." E.print e; - (D.join state esimp.v, (esimp :: simp_exps))) - , false) - (state, []) - elist - in - match rev_res with - | [] -> D.faux, [simp_false] - | _ -> state, List.rev rev_res - end - | _ -> - let () = debug "No additional simplification@." in - D.top, List.map (identity D.top) elist - - and simp_expr state (e : expr) : (expr, v) simp = - let ty = E.get_type e in + (elist : E.t list) + : v * (E.t, v) simp list = + match f with + | Symbols.F_Unit _ -> begin (* <=> AND *) + let () = debug "F_Unit@." in + let state,rev_res = + fold_left_stop + (fun (state, simp_exps) e -> + let esimp : (E.t, v) simp = simp_expr state e in + match state &&& esimp.exp with + | AlreadyTrue -> ( + debug "%a = true@." E.print e; + (state, simp_exps), false + ) + | AlreadyFalse -> ( + debug "%a = false@." E.print e; + (state, [simp_false]), true + ) + | NewConstraint c -> ( + debug "Keeping %a@." E.print e; + (c, esimp :: simp_exps), false + ) + ) + (state, []) + elist + in + match rev_res with + | [] -> state, [simp_true] + | _ -> state, List.rev rev_res + end + + | F_Clause _ -> begin (* <=> OR *) + let () = debug "F_Clause@." in + let state, rev_res = + fold_left_stop + (fun (state, simp_exps) e -> + let (esimp : (E.t, v) simp) = simp_expr state e in + if is_false esimp then ( + debug "%a = false@." E.print e; + (state, simp_exps), false + ) + else if is_true esimp then ( + debug "%a = true@." E.print e; + (state, [simp_true]), true + ) + else ( + debug "Keeping %a@." E.print e; + (D.join state esimp.v, (esimp :: simp_exps))) + , false) + (state, []) + elist + in + match rev_res with + | [] -> state, [simp_false] + | _ -> state, List.rev rev_res + end + | _ -> + let () = debug "No additional simplification@." in + D.top, List.map (identity D.top) elist + + and simp_expr state (e : E.t) : (E.t, v) simp = + debug "[simp_expr] Simplifying expression %a with %a@." E.print e D.pp state; + let ty = E.type_info e in let elist = E.get_sub_expr e in - let symb = E.get_comp e in + let symb = E.get_symb e in match symb, elist with | Op Tite, [cond; th; el] -> begin - debug "Ite"; + debug "[simp_expr] Ite@."; let simp = simp_ite state cond th el in + debug "[simp_expr] Ite treated@."; match simp with - | [branch] -> branch + | [branch] -> + 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 { (* A simplification has been made *) - exp = E.mk_term (Op Tite) [cond.exp; th.exp; el.exp] ty; - diff = true; - v = D.join th.v el.v - } else { (* No simplification has been done *) + 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} + end else begin + (* A simplification has been made *) + debug "[simp_expr] Simplification worked on a branch@."; { + exp = E.mk_term (Op Tite) [cond.exp; th.exp; el.exp] ty; + diff = true; + v = D.join th.v el.v + } + end else begin + debug "[simp_expr] Simplification worked on a branch@."; + { (* Simplification failed *) exp = e; diff = false; v = D.join th.v el.v - } + } end | _ -> assert false end | Op Tite, _ -> assert false | Symbols.Form f, _ -> - debug "Formula: %a@." Symbols.print symb; + debug "[simp_expr] Formula: %a@." Symbols.print symb; let v, l = simp_form state f elist in if List.exists (fun e -> e.diff) l then { exp = E.mk_term symb (List.map (fun e -> e.exp) l) ty; @@ -490,11 +428,20 @@ module SimpleReasoner v } else {exp = e; diff = false; v = D.top} + | Symbols.Lit _, _ -> begin + debug + "[simp_expr] Litteral : %a@." + Symbols.print symb; + match add_lit_constraint state e with + | AlreadyTrue -> simp_true + | AlreadyFalse -> simp_false + | NewConstraint v -> {exp = e; diff = false; v} + end | _ -> debug - "Other: %a@." + "[simp_expr] Other: %a@." Symbols.print symb; - let (l : (expr, v) simp list) = List.map (simp_expr state) elist in ( + 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; @@ -506,7 +453,7 @@ module SimpleReasoner (** Wrapper of simp_expr for verbose *) let simp_expr e = try - debug "Simplifying %a@." E.print e; + debug "START Simplifying %a@." E.print e; let res = simp_expr D.top e in if res.diff then diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli index e0a86ea99..bc0ddbf5d 100644 --- a/src/lib/frontend/simple_reasoner_expr.mli +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -24,10 +24,13 @@ val has_changed : _ simp -> bool defined below. *) -module type Dom = -sig +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 *) + +module type Dom = sig type v - type expr (** Top/Bottom value *) val top : v @@ -40,42 +43,20 @@ sig val join : v -> v -> v (** Add constraint *) - val add_constraint : expr -> v -> v - - (** Constants *) - val vrai : v - val faux : v -end + val add_constraint : Expr.t -> Expr.t -> Symbols.lit -> v -> v add_constraint_res -(** Expr is the signature of the module dedicated to - the representation of expressions that are to be - simplified. *) -module type Expr = sig - type t - val equal : t -> t -> bool - val mk_term : Symbols.t -> t list -> Ty.t -> t - val get_comp : t -> Symbols.t - val get_sub_expr : t -> t list - val get_type : t -> Ty.t - val neg : t -> t - val vrai : t - val faux : t - val int : string -> t - val real : string -> t - val print : Format.formatter -> t -> unit + val pp : Format.formatter -> v -> unit end (** This is the signature of the simplifyer. *) module type S = sig type v - type expr (** Simplifies an expression and returns its associated abstract value. *) - val simp_expr : expr -> (expr, v) simp + val simp_expr : Expr.t -> (Expr.t, v) simp end module SimpleReasoner - (E : Expr) - (D : Dom with type expr = E.t) - : S with type expr = E.t and type v = D.v + (D : Dom) + : S with type v = D.v diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml index 1764e02f5..8225c206e 100644 --- a/src/lib/reasoners/intervals.ml +++ b/src/lib/reasoners/intervals.ml @@ -1169,6 +1169,37 @@ let match_interval lb ub i accu = try Some (match_interval_upper ub i (match_interval_lower lb i accu)) with Exit -> None +(* todo: iterate on both lists at the same time for linear cplxty *) +let contained_in (lb, ub) i = + List.exists + (fun (lb', ub') -> + ( + match lb, lb' with + | _, Minfty -> true + | Pinfty, _ + | _, Pinfty -> assert false + | Minfty, _ -> false + | Large (q, _), (Large (q', _) | Strict (q', _)) + | Strict (q, _), Strict (q', _) -> + Q.compare q q' >= 0 + | Strict (q, _), Large (q', _) -> + Q.compare q q' > 0 + ) && + ( + match ub, ub' with + | _, Pinfty -> true + | Minfty, _ + | _, Minfty -> assert false + | Pinfty, _ -> false + | Large (q, _), (Large (q', _) | Strict (q', _)) + | Strict (q, _), Strict (q', _) -> + Q.compare q q' <= 0 + | Strict (q, _), Large (q', _) -> + Q.compare q q' < 0 + )) i.ints + +let contained_in i1 i2 = + List.for_all (fun i -> contained_in i i2) i1.ints (*****************) diff --git a/src/lib/reasoners/intervals.mli b/src/lib/reasoners/intervals.mli index 5d4b9ef61..8313a548f 100644 --- a/src/lib/reasoners/intervals.mli +++ b/src/lib/reasoners/intervals.mli @@ -150,3 +150,5 @@ type interval_matching = val match_interval: Symbols.bound -> Symbols.bound -> t -> interval_matching -> interval_matching option + +val contained_in : t -> t -> bool diff --git a/src/lib/reasoners/polynome.ml b/src/lib/reasoners/polynome.ml index a02ad662b..50c17649b 100644 --- a/src/lib/reasoners/polynome.ml +++ b/src/lib/reasoners/polynome.ml @@ -40,6 +40,13 @@ module type S = sig val mult : r -> r -> r end +module type Calc = sig + type t + val one : t + val add : t -> t -> t + val mul : Q.t -> t -> t +end + module type T = sig type r @@ -77,6 +84,15 @@ module type T = sig val abstract_selectors : t -> (r * r) list -> t * (r * r) list val separate_constant : t -> t * Numbers.Q.t + + val fold_on_vars : (r -> Numbers.Q.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc + + module M : Map.S with type key = r + + module Eval (C : Calc) : sig + exception MissingVar + val eval : C.t M.t -> t -> C.t + end end module type EXTENDED_Polynome = sig @@ -354,4 +370,19 @@ module Make (X : S) = struct let separate_constant t = { t with c = Q.zero}, t.c + let fold_on_vars f p = M.fold f p.m + + module Eval (C : Calc) = struct + + exception MissingVar + + let eval_monom(map : C.t M.t) (r : r) (q : Q.t) (acc : C.t) = + match M.find_opt r map with + | None -> raise MissingVar + | Some v -> + C.add acc (C.mul q v) + + let eval map p = + M.fold (eval_monom map) p.m (C.mul p.c C.one) + end end diff --git a/src/lib/reasoners/polynome.mli b/src/lib/reasoners/polynome.mli index 025e08146..8dfd07618 100644 --- a/src/lib/reasoners/polynome.mli +++ b/src/lib/reasoners/polynome.mli @@ -34,6 +34,13 @@ module type S = sig val mult : r -> r -> r end +module type Calc = sig + type t + val one : t + val add : t -> t -> t + val mul : Numbers.Q.t -> t -> t +end + module type T = sig type r @@ -79,6 +86,16 @@ module type T = sig val abstract_selectors : t -> (r * r) list -> t * (r * r) list val separate_constant : t -> t * Numbers.Q.t + + val fold_on_vars : (r -> Numbers.Q.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc + + module M : Map.S with type key = r + + module Eval (C : Calc) : sig + exception MissingVar + val eval : C.t M.t -> t -> C.t + end + end module type EXTENDED_Polynome = sig diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml new file mode 100644 index 000000000..5c86d02f3 --- /dev/null +++ b/src/lib/reasoners/simplifiers.ml @@ -0,0 +1,446 @@ +(******************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2021 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of the Apache Software *) +(* License version 2.0 *) +(* *) +(******************************************************************************) + +module SRE = Simple_reasoner_expr +module E = Expr +module Q = Numbers.Q +module R = Shostak.Combine +module A = Shostak.Arith +module P = Shostak.Polynome +module M = P.M + +let verb = Options.get_simplify_verbose + +let silent (msg : ('a, Format.formatter, unit) format) = + Format.ifprintf Format.std_formatter msg + +let talk (msg : ('a, Format.formatter, unit) format) = + Format.printf "[Simplifiers] "; + Format.printf msg + +let debug (msg : ('a, Format.formatter, unit) format) = + if verb () + then talk msg + else silent msg + +module DummySimp = + SRE.SimpleReasoner + (struct + type v = unit + let top = () + let bottom = () + let compare _ _ = Some 0 + let join _ _ = () + let add_constraint _ _ _ _ = SRE.NewConstraint () + let pp fmt _ = Format.fprintf fmt "()" + end + ) + +type 'a abstract_value = + | Bottom + | Top + | Value of 'a + +let pp_abs_val pp fmt = function + | Bottom -> Format.fprintf fmt "⊥" + | Top -> Format.fprintf fmt "T" + | Value v -> pp fmt v + +let compare_abs_val cmp v1 v2 = + match v1, v2 with + | Bottom, Bottom + | Top, Top -> Some 0 + | Bottom, _ + | _, Top -> Some (-1) + | Top, _ + | _, Bottom -> Some 1 + | Value v1, Value v2 -> cmp v1 v2 + +module IntervalsDomain : + SRE.Dom with type v = Intervals.t abstract_value M.t abstract_value = struct + type v = Intervals.t abstract_value M.t abstract_value + + let top = Top + let bottom : v = Bottom + + let pp fmt v = + pp_abs_val + (fun fmt -> M.iter + (fun r i -> Format.fprintf fmt "%a = %a" + R.print r + (pp_abs_val Intervals.print) i)) + fmt + v + + 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 + fun m1 m2 -> + (* Compares two maps. + Maps are compared itetatively ; the result is saved on a reference + checked through the main loop. *) + let res : int option option ref = ref None in + (* !res = None => comparison not started *) + (* !res = Some None => Non comparable *) + (* !res = Some (-1) => m1 < m2 *) + (* !res = Some 1 => m1 > m2 *) + (* !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 *) + match !res with + | None -> (* First time comparing *) + res := Some (Some r) + | Some None -> (* Comparison should have beed ended before *) + assert false + | Some (Some 0) -> (* Up to this point, comparison has shown both + maps are equal *) + if r <> 0 then res := Some (Some r) + | Some (Some r') -> + if r <> r' then begin res := Some None; raise Stop end in + let get_res () = + match !res with + | None -> Some 0 (* Comparison did not even started ; + maps are both empty *) + | Some v -> v in + try + let () = ignore @@ + M.merge (* The result of this merge is ignored : it is only here to compare *) + (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 + | Some v1, Some v2 -> + match compare_intervals v1 v2 with + | None -> res := Some None; raise Stop + | Some v -> set_res v; None + ) + m1 + m2 in get_res () with + | Stop -> get_res () + + let compare = compare_abs_val compare + + let join = + M.merge + (fun _k v1 v2 -> + match v1, v2 with + | None, ((Some _) as v) + | ((Some _) as v), None -> v + + | None, None -> assert false + + | Some Top, Some _ + | Some _, Some Top -> Some Top + + | ((Some _) as v), Some Bottom + | Some Bottom, ((Some _) as v) -> v + + | Some (Value v1), Some (Value v2) -> Some (Value (Intervals.merge v1 v2))) + + let join v1 v2 = + match v1, v2 with + | Top, _ + | _, Top -> Top + | Bottom, v + | v, Bottom -> v + | Value i1, Value i2 -> Value (join i1 i2) + + let eval_constraint (ty : Ty.t) (v : v) (p : P.t) : Intervals.t abstract_value = + match v with + | Top -> begin + match P.to_list p with + | [], q -> Value (Intervals.point q ty Explanation.empty) + | _ -> Top + end + | Bottom -> Bottom + | Value v -> + let ty = P.type_info p in + let module E = P.Eval (struct + type t = Intervals.t abstract_value + let one = Value (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) + let mul coef i = + match i with + | Top -> + if Q.equal coef Q.zero then + Value (Intervals.point Q.zero ty Explanation.empty) + else Top + | Bottom -> Bottom + | Value i -> + Value (Intervals.affine_scale ~const:Q.zero ~coef i) + end) in (* todo: apply functor statically for each type *) + E.eval v p + + let rfind ty k (v : v) = match v with + | Bottom -> failwith "Value is bottom: Should have been checked beforehand" + | Top -> Intervals.undefined ty + | 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 (Value i) -> i + + let radd k b v = match v with + | Top -> Value (M.add k b M.empty) + | Value m -> Value (M.add k b m) + | Bottom -> v + + let fix_point + (narrow : rinter:Intervals.t -> prev_inter:Intervals.t -> Intervals.t * bool) + (ty : Ty.t) + (constraints : (Q.t * R.r * P.t) list) + (v : v) = + let rec aux v = + let new_vars, keep_iterating = + List.fold_left + (fun ((v : v), 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; + match eval_constraint ty v p with + | Top + | Bottom -> v, false + | Value i -> + (* Deducing the value of `r` *) + debug "[fix_point] %a = %a@." P.print p Intervals.print i; + + if Intervals.is_undefined i then begin + debug "[fix_point] No information, continuing@."; + v, keep_iterating + end else begin + debug "[fix_point] Narrowing@."; + let rinter = Intervals.scale (Q.div Q.one q) i in + let prev_inter = rfind ty r v in + let ri, change = narrow ~rinter ~prev_inter in + debug "[fix_point] %a ~~> %a@." Intervals.print rinter Intervals.print prev_inter; + if change then + radd r (Value ri) v, change + else + v, keep_iterating + end + ) + (v, false) + constraints in + if keep_iterating then aux new_vars else v in + aux v + + let narrow_eq ~rinter ~prev_inter = + debug "[fix_point] Narrow EQ@."; + if Intervals.contained_in rinter prev_inter + 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 *) + debug "[fix_point] Narrow NEQ@."; + match Intervals.is_point rinter with + | None -> prev_inter, false + | Some (q, _) -> + if Intervals.contains prev_inter q then + Intervals.exclude rinter prev_inter, true + else prev_inter, false + + let narrow_le ~rinter ~prev_inter = + debug "[fix_point] Narrow LE@."; + try + let bound , _, is_le = Intervals.borne_sup rinter in + let prev_sup = + try + let s, _, _ = Intervals.borne_sup prev_inter in s + with + Intervals.No_finite_bound -> (* A value satisfying the next condition *) + Q.sub bound Q.one in + if Q.compare bound prev_sup <= 0 then begin + debug "[fix_point] %a <= %a@." Q.print bound Q.print prev_sup; + prev_inter, false + end else + (* The new upper bound is lower than then previous one, + replacing it *) + Intervals.new_borne_sup + Explanation.empty + bound + ~is_le + prev_inter, true + with + | Intervals.No_finite_bound -> prev_inter, false + + let narrow_lt ~rinter ~prev_inter = + debug "[fix_point] Narrow LT@."; + try + let bound , _, _ = Intervals.borne_sup rinter in + let prev_sup = + try + let s, _, _ = Intervals.borne_sup prev_inter in s + with + Intervals.No_finite_bound -> (* A value satisfying the next condition *) + Q.sub bound Q.one in + if Q.compare bound prev_sup <= 0 then + (* The new upper bound is higher then the previous one, + keeping it *) + prev_inter, false + else + (* The new upper bound is lower than then previous one, + replacing it *) + Intervals.new_borne_sup + Explanation.empty + bound + ~is_le:false + prev_inter, true + with + | Intervals.No_finite_bound -> prev_inter, false + + let narrow_gt ~rinter ~prev_inter = + debug "[fix_point] Narrow GT@."; + try + let bound , _, _ = Intervals.borne_inf rinter in + let prev_inf = + try let s , _, _ = Intervals.borne_inf prev_inter in s with + | Intervals.No_finite_bound -> (* A value satisfying the next condition *) + Q.add bound Q.one + in + 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 + with + | Intervals.No_finite_bound -> prev_inter, false + + let narrow_ge ~rinter ~prev_inter = + debug "[fix_point] Narrow GE@."; + try + let bound , _, is_le = Intervals.borne_inf rinter in + let prev_inf = + try let s , _, _ = Intervals.borne_inf prev_inter in s with + | Intervals.No_finite_bound -> (* A value satisfying the next condition *) + Q.add bound Q.one + in + if Q.compare prev_inf bound > 0 then + prev_inter, false + else + Intervals.new_borne_inf Explanation.empty bound ~is_le prev_inter, true + with + | Intervals.No_finite_bound -> prev_inter, false + + let fix_point_eq = fix_point narrow_eq + let fix_point_neq = fix_point narrow_neq + let fix_point_le = fix_point narrow_le + let fix_point_lt = fix_point narrow_lt + let fix_point_gt = fix_point narrow_gt + let fix_point_ge = fix_point narrow_ge + + (* Adds the constraints in argument to the abstract value, then repeats of the + abstract value has been refined thanks to the constraints. *) + let fix_point (lit : Symbols.lit) = + match lit with + | Symbols.L_eq -> fix_point_eq + | L_neg_eq -> fix_point_neq + | L_built LE -> fix_point_le + | L_built LT -> fix_point_lt + | 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_pred -> + failwith "todo (even a better error message would be nice)" + + (* todo: take into account types, open bounds & le/lt *) + let check_constraint ty lit p c v = + let interval = eval_constraint ty v p in + match interval with + | Top | Bottom -> None + | Value i -> begin + let inf = + try let (inf, _, _) = Intervals.borne_inf i in inf with + | Intervals.No_finite_bound -> Q.sub c Q.one in + let sup = + try let (sup, _, _) = Intervals.borne_sup i in sup with + | Intervals.No_finite_bound -> Q.add c Q.one in + match lit with + | Symbols.L_eq -> + if Q.compare c inf < 0 || Q.compare sup c < 0 then + Some false + else + None + | L_neg_eq -> + if Q.compare c inf < 0 || Q.compare sup c < 0 then + Some true + else + None + | L_built (LE | LT) -> + if Q.compare sup c < 0 then + Some true + else if Q.compare c inf < 0 then + Some false + else None + + | L_neg_built (LE | LT) -> + if Q.compare sup c < 0 then + Some false + else if Q.compare c inf < 0 then + Some true + 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_pred -> + failwith "Check constraint : todo (even a better error message would be nice)" + end + + (* 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 p1 = A.embed @@ fst (R.make l1) in + let p2 = A.embed @@ fst (R.make l2) in + let ty = P.type_info p1 in + + (* l1 R l2 <=> p + c R 0 *) + let (p, c, _cst) = P.normal_form_pos (P.sub p1 p2) in + + debug "Constraint : %a + %a R 0@." P.print p Q.print c; + + let mc = Q.minus c in + + match check_constraint ty lit p mc v with + | Some true -> SRE.AlreadyTrue + | Some false -> AlreadyFalse + | None -> + (* p = \Sum (q_i * r_i) + p R c <=> \A i. q_i * r_i = p - (q_i * r_i) - c *) + let constraints = + P.fold_on_vars + (fun r q acc_cstr -> ((q, r, P.sub p (P.create [q,r] c ty)) :: acc_cstr)) + p + [] in + NewConstraint (fix_point lit ty constraints v) +end + +module IntervalsSimp = + SRE.SimpleReasoner(IntervalsDomain) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index c378849fc..7e553e1b3 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -2568,59 +2568,5 @@ type th_elt = let print_th_elt fmt t = Format.fprintf fmt "%s/%s: @[%a@]" t.th_name t.ax_name print t.ax_form -module SimpExpr = - Simple_reasoner_expr.SimpleReasoner ( - struct - type nonrec t = t - let equal = equal - - let mk_term sy l typ = - match sy,l with - Sy.Form (Sy.F_Unit is_impl), f1 :: f2 :: [] -> - mk_and f1 f2 is_impl 0 - | Sy.Form (Sy.F_Unit _), _ -> - failwith "F_Unit not supported by simplifyer"; - - | Sy.Form (Sy.F_Clause is_impl), f1 :: f2 :: [] -> - mk_or f1 f2 is_impl 0 - | Sy.Form (Sy.F_Clause _), _ -> - failwith "F_Clause not supported by simplifyer"; - - | Sy.Form (Sy.F_Iff), [f1;f2] -> mk_iff f1 f2 0 - | Sy.Form (Sy.F_Iff), _ -> mk_nary_eq l - - | Sy.Form (Sy.F_Xor), f1 :: f2 :: [] -> mk_xor f1 f2 0 - | Sy.Form (Sy.F_Xor), _ -> - Format.eprintf "F_Xor not supported by simplifyer"; - assert false - - | Sy.Form (Sy.F_Lemma),_ - | Sy.Form (Sy.F_Skolem),_ -> failwith "Formula undefined." - - | Sy.Lit (Sy.L_eq),_ -> - mk_positive_lit sy (Sy.Lit (Sy.L_neg_eq)) l - | Sy.Lit (Sy.L_built b),_ -> - mk_positive_lit sy (Sy.Lit (Sy.L_neg_built b)) l - | Sy.Lit (Sy.L_neg_eq), _ -> - mk_positive_lit (Sy.Lit Sy.L_eq) (Sy.Lit Sy.L_neg_eq) l |> neg - | Sy.Lit (Sy.L_neg_built n), _ -> - mk_builtin ~is_pos:false n l - | Sy.Lit (Sy.L_neg_pred), _ -> - failwith "Lit (L_neg_pred) not supported by simplifyer" - | _ -> mk_term sy l typ - - let get_comp e = e.f - let get_sub_expr e = e.xs - let get_type e = e.ty - - let vrai = vrai - let faux = faux - - let real = real - let int = int - - let print = print - - let neg = neg - end - ) +let get_symb e = e.f +let get_sub_expr e = e.xs diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index c9598c2a2..38406d32b 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -320,9 +320,6 @@ val is_pure : t -> bool val const_term : t -> bool (** return true iff the given argument is a term without arguments *) -(** SimpExpr defines a simplifyer functor for expressions of type t - (defined in this file). *) -module SimpExpr : - functor - (D : Simple_reasoner_expr.Dom with type expr = t) - -> Simple_reasoner_expr.S with type expr = t and type v = D.v +val get_symb : t -> Symbols.t + +val get_sub_expr : t -> t list From 6a7be9fb50583fe6010ec8024edbd069937d6880 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 17 Mar 2021 10:53:39 +0100 Subject: [PATCH 03/18] Bug fixes --- src/bin/common/parse_command.ml | 4 +- src/lib/frontend/cnf.ml | 6 +- src/lib/frontend/simple_reasoner_expr.ml | 640 +++++++++++++--------- src/lib/frontend/simple_reasoner_expr.mli | 28 +- src/lib/reasoners/polynome.ml | 12 +- src/lib/reasoners/polynome.mli | 3 +- src/lib/reasoners/simplifiers.ml | 277 +++++++--- src/lib/util/options.ml | 6 +- src/lib/util/options.mli | 4 +- 9 files changed, 619 insertions(+), 361 deletions(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 223dbb170..dceb514dd 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -171,7 +171,8 @@ let mk_dbg_opt_spl2 debug_explanations debug_fm debug_fpa debug_gc `Ok() let mk_dbg_opt_spl3 debug_split debug_sum debug_triggers debug_types - debug_typing debug_uf debug_unsat_core debug_use debug_warnings rule + debug_typing debug_uf debug_unsat_core debug_use debug_warnings + debug_simplify rule = let rule = value_of_rule rule in set_debug_split debug_split; @@ -183,6 +184,7 @@ let mk_dbg_opt_spl3 debug_split debug_sum debug_triggers debug_types set_debug_unsat_core debug_unsat_core; set_debug_use debug_use; set_debug_warnings debug_warnings; + set_debug_simplify debug_simplify; set_rule rule; `Ok() diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 573daeff9..a07023d43 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -293,16 +293,16 @@ let rec make_term up_qv quant_basename t = up_qv quant_basename e Loc.dummy ~decl_kind:E.Daxiom (* not correct, but not a problem *) ~toplevel:false - in + in mk_term t (* let term = mk_term t in match Options.get_simplify () with | Util.SNo -> term | 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 + else term *) and make_trigger ~in_theory name up_qv quant_basename hyp (e, from_user) = let content, guard = match e with diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index 55e44d770..02e0ad86a 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -12,7 +12,7 @@ module E = Expr module Sy = Symbols -let verb = Options.get_simplify_verbose +let verb = Options.get_debug_simplify let silent (msg : ('a, Format.formatter, unit) format) = Format.ifprintf Format.std_formatter msg @@ -28,70 +28,6 @@ let debug (msg : ('a, Format.formatter, unit) format) = (** 1. Utils *) -(** Values are representations of expressions - that have been "solved", in the sense that they can - be reduced to a boolean or a float/int. -type value = - | Bool of bool - | Num of Q.t - -let (++) v1 v2 = - match v1, v2 with - Bool b1, Bool b2 -> Bool (b1 || b2) - | Num n1, Num n2 -> Num (Q.add n1 n2) - | _,_ -> assert false - -let (--) v1 v2 = - match v1, v2 with - | Num n1, Num n2 -> Num (Q.sub n1 n2) - | _,_ -> assert false - -let ( ** ) v1 v2 = - match v1, v2 with - Bool b1, Bool b2 -> Bool (b1 && b2) - | Num n1, Num n2 -> Num (Q.mul n1 n2) - | _,_ -> assert false - -let (|=) v1 v2 = - match v1, v2 with - Bool b1, Bool b2 -> b1 == b2 - | Num n1, Num n2 -> (Stdlib.(=)) n1 n2 - | _,_ -> false - -let (|<>) v1 v2 = not (v1 |= v2) - -let (|<) v1 v2 = - match v1, v2 with - | Num n1, Num n2 -> n1 < n2 - | _,_ -> assert false - -let (|<=) v1 v2 = - match v1, v2 with - | Num n1, Num n2 -> n1 <= n2 - | _,_ -> assert false - -let (|>) v1 v2 = - match v1, v2 with - | Num n1, Num n2 -> n1 > n2 - | _,_ -> assert false - -let (|>=) v1 v2 = - match v1, v2 with - | Num n1, Num n2 -> n1 >= n2 - | _,_ -> assert false - - -let pp_val fmt v = - match v with - Bool b -> Format.fprintf fmt "Bool %b" b - | Num n -> Format.fprintf fmt "Num %a" Q.pp_print n*) - -(** A simplified formula/expr/... type. - The diff field is set to false if the operation did not change the - input. - As queries may provide explanations, the third field correspond to the - explanation behind the simplification. *) - (** Same as List.fold_left, but f returns a tuple (acc, stop) where stop is a boolean stating that the loop has to stop. *) @@ -115,6 +51,9 @@ type ('expr, 'abs_val) simp = { v : 'abs_val } +let pp_simp pp_abs_val fmt s = + 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 let has_changed e = e.diff @@ -132,24 +71,36 @@ type 'abs_val add_constraint_res = defined below. *) (** Dom is the signature of the abstact domain. *) -module type Dom = -sig - type v +module type Dom = sig + type v (* The raw abstract value. For the interval domain, an interval *) + type state (* The global state representation. Usually a map of 'v's *) (** Top/Bottom value *) - val top : v - val bottom : v + val top : state + val bottom : state + + val vrai : v + val faux : v + val unknown : v (** (Partial) Compare function *) - val compare : v -> v -> int option + val compare : state -> state -> int option (** Join operator *) - val join : v -> v -> v + val join : state -> state -> state + val v_join : v -> v -> v (** Add constraint *) - val add_constraint : Expr.t -> Expr.t -> Symbols.lit -> v -> v 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 - val pp : Format.formatter -> v -> unit + (** Evaluates an expression in the given state *) + val eval_expr : Expr.t -> state -> v + + val pp : Format.formatter -> state -> unit + val pp_v : Format.formatter -> v -> unit end (** This is the signature of the simplifyer. *) @@ -164,40 +115,62 @@ end module SimpleReasoner (D : Dom) : S with type v = D.v = struct + type state = D.state type v = D.v - let identity v exp = {exp; diff = false; v} + 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 + + let add_cache cache exp state smp = + let c = !cache in + cache := + E.Map.add + exp + (match E.Map.find_opt exp c with + | None -> [state, smp] + | Some l -> (state, smp) :: l) + c + + let find_cache cache exp state = + match E.Map.find_opt exp !cache with + | Some l -> List.find_opt ( + fun (s,_) -> + match D.compare s state with + | Some 0 -> true + | _ -> false) + l + | None -> None + + let pp_simp = pp_simp D.pp_v - (* - let (|=) v1 v2 = - match D.compare v1 v2 with - | Some i -> i = 0 - | None -> false*) + let identity v exp = {exp; diff = false; v = D.eval_expr exp v} - let simp_true = {exp = E.vrai; diff = true; v = D.top} - let simp_false = {exp = E.faux; diff = true; v = D.top} + let simp_true = {exp = E.vrai; diff = true; v = D.vrai} + let simp_false = {exp = E.faux; diff = true; v = D.faux} let is_true e = E.equal e.exp E.vrai let is_false e = E.equal e.exp E.faux - let rec add_lit_constraint (v : v) (e : Expr.t) = - let exception Stop of v add_constraint_res in + let rec add_lit_constraint_no_cache (state : state) (e : Expr.t) = + let exception Stop of state add_constraint_res in match E.lit_view e with | Eq (e1, e2) -> debug "[add_lit_constraint] Eq@."; - D.add_constraint e1 e2 Sy.L_eq v + D.add_constraint e1 e2 Sy.L_eq state | Eql [] -> assert false | Eql (hd :: tl) -> begin try debug "[add_lit_constraint] Eql@."; NewConstraint ( List.fold_left - (fun v e -> - match D.add_constraint hd e Sy.L_eq v with - | AlreadyTrue -> v + (fun s e -> + match D.add_constraint hd e Sy.L_eq s with + | AlreadyTrue -> s | AlreadyFalse -> raise (Stop AlreadyFalse) - | NewConstraint v' -> v' - ) v tl + | NewConstraint s' -> s' + ) state tl ) with Stop res -> res end @@ -206,81 +179,156 @@ module SimpleReasoner debug "[add_lit_constraint] Distinct@."; NewConstraint ( List.fold_left - (fun v e -> - match D.add_constraint hd e Sy.L_neg_eq v with - | AlreadyTrue -> v + (fun s e -> + match D.add_constraint hd e Sy.L_neg_eq s with + | AlreadyTrue -> s | AlreadyFalse -> raise (Stop AlreadyFalse) - | NewConstraint v' -> v') v tl) + | NewConstraint s' -> s') state tl) with Stop res -> res end | Builtin (_, btin, [e1; e2]) -> begin - match D.add_constraint e1 e2 (Sy.L_built btin) v with + debug "[add_lit_constraint] Builtin@."; + match D.add_constraint e1 e2 (Sy.L_built btin) state with | AlreadyTrue -> debug "[add_lit_constraint] Already true@."; AlreadyTrue | AlreadyFalse -> debug "[add_lit_constraint] Already false@."; AlreadyFalse - | NewConstraint v' -> + | NewConstraint s' -> debug "[add_lit_constraint] New constraint: %a@." - D.pp v'; - NewConstraint v' + D.pp s'; + NewConstraint s' end | Builtin (_, _, _) -> failwith "Unhandled builtin" | Pred _ -> debug "[add_lit_constraint] Pred@."; - NewConstraint v - | Not_a_lit _ -> + NewConstraint state + | Not_a_lit {is_form} -> debug "[add_lit_constraint] Not a lit@."; - failwith "add_lit_constraint should be only called on litterals" - (* - and add_form_constraint (v : v) (e : Expr.t) = - match E.form_view e with - | E.Unit (f1, f2) -> begin - match add_lit_constaint v f1 with - | AlreadyFalse -> - - end - add_lit_constraint (add_lit_constraint v f1) f2 - - | Clause (f1, f2, _) -> - let v1 = add_lit_constraint v f1 in - let v2 = add_lit_constraint v f2 in - D.join v1 v2 - - | Iff (f1, f2) -> - let pos = add_lit_constraint (add_lit_constraint v f1) f2 in - let neg = add_lit_constraint (add_lit_constraint v (E.neg f1)) (E.neg f2) in - D.join pos neg - - | Xor (f1, f2) -> - let v1 = add_lit_constraint (add_lit_constraint v f1) (E.neg f2) in - let v2 = add_lit_constraint (add_lit_constraint v (E.neg f1)) f2 in - D.join v1 v2 - - | Literal e -> add_lit_constraint v e - - | Lemma _ | Skolem _ | Not_a_form -> v + if is_form then + add_form_constraint state e + else + failwith "add_lit_constraint should be only called on litterals or formulas" - | Let _ -> failwith "todo" - *) + 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 + add_cache constraint_cache e state res; + res + | Some (_, res) -> res and (&&&) v e = - add_lit_constraint v e -(* - let is_true v = v |= D.vrai - let is_false v = v |= D.faux -*) - - - (* - let is_constr (constr : Hstring.t) (e : expr) : bool option = - match E.get_comp e with - | Op (Constr s') -> Some (Hstring.equal constr s') - | _ -> None*) + add_form_constraint v e + + and add_form_view_constraint state = function + | E.Unit (e1, e2) -> begin + debug "[add_form_constraint] Unit@."; + match state &&& e1 with + | AlreadyTrue -> state &&& e2 + | AlreadyFalse -> AlreadyFalse + | NewConstraint state -> state &&& e2 + end + | Clause (e1, e2, _) -> begin + debug "[add_form_constraint] Clause@."; + match state &&& e1 with + | AlreadyTrue -> AlreadyTrue + | AlreadyFalse -> state &&& e2 + | NewConstraint state1 -> begin + match state &&& e2 with + | AlreadyTrue -> AlreadyTrue + | AlreadyFalse -> AlreadyFalse + | NewConstraint state2 -> + NewConstraint (D.join state1 state2) + 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 *) + match nc1 with + | AlreadyTrue -> (* e1 is false *) + state &&& E.neg e2 + | AlreadyFalse -> (* e1 is true *) + state &&& e2 + | NewConstraint ns1 -> + 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) *) + match nc2 with + | AlreadyTrue -> (* (~e1 /\ ~e2) is true *) + AlreadyTrue + | AlreadyFalse -> (* (~e1 /\ ~e2) is false *) + c2 + | NewConstraint ns2 -> + NewConstraint (D.join s2 ns2) + end + end + | Xor (e1, e2) -> begin (* (e1 /\ ~e2) \/ (~e1 /\ e2) *) + debug "[add_form_constraint] Xor@."; + let c1 = state &&& e1 in (* Constraint on e1 *) + match c1 with + | AlreadyTrue -> (* e1 is true *) + state &&& E.neg e2 + | AlreadyFalse -> (* e1 is false *) + state &&& e2 + | (NewConstraint s1) as c1 -> + let c2 = state &&& e2 in (* Constraint on e2 *) + match c2 with + | AlreadyTrue -> (* e2 is true *) + state &&& E.neg e1 + | AlreadyFalse -> (* e2 is false *) + c1 + | NewConstraint s2 -> (* 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 -> + 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) + end + | Literal e -> + debug "[add_form_constraint] Litteral@."; + add_lit_constraint state e + | Let _ -> + debug "[add_form_constraint] Let binding: TODO@."; + NewConstraint state + + | Lemma _ + | Skolem _ -> + 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" + + 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 : v) + (state : state) (cond : E.t) (th : E.t) (el : E.t) : @@ -296,159 +344,241 @@ module SimpleReasoner debug "[simp_ite] It is false, ending@."; let el : (E.t, v) simp = simp_expr state el in [{el with diff = true}] - end else let cth = scond.v in begin - let neg_cond = E.neg scond.exp in - match state &&& neg_cond with - | AlreadyTrue -> - debug "[simp_ite] Negation is true, ending@."; - let el : (E.t, v) simp = simp_expr state el in - [{el with diff = true}] - | AlreadyFalse -> - debug "[simp_ite] Negation is fakse, ending@."; - let th : (E.t, v) simp = simp_expr state th in - [{th with diff = true}] - | 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 - if scond.diff || sth.diff || sel.diff then - [scond; sth; sel] - else [ - identity scond.v cond; - identity sth.v th; - identity sel.v el] + 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, _ + | _, 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] end and simp_form - (state : v) + (state : state) (f : Symbols.form) (elist : E.t list) - : v * (E.t, v) simp list = + : (E.t, v) simp list = match f with | Symbols.F_Unit _ -> begin (* <=> AND *) - let () = debug "F_Unit@." in - let state,rev_res = + let () = debug "[simp_form] F_Unit@." in + let _state,rev_res = fold_left_stop (fun (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 - match state &&& esimp.exp with - | AlreadyTrue -> ( - debug "%a = true@." E.print e; - (state, simp_exps), false - ) - | AlreadyFalse -> ( - debug "%a = false@." E.print e; - (state, [simp_false]), true - ) - | NewConstraint c -> ( - debug "Keeping %a@." E.print e; - (c, esimp :: simp_exps), false - ) + debug "[simp_form] Simplified %a into %a in F_Unit@." + E.print e pp_simp esimp; + if is_false esimp then ( + debug "[simp_form] %a = false@." E.print e; + (state, [simp_false]), true + ) + else if is_true esimp then ( + debug "[simp_form] %a = true@." E.print e; + (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))) + , false ) (state, []) elist in match rev_res with - | [] -> state, [simp_true] - | _ -> state, List.rev rev_res + | [] -> + debug "[simp_form] No more litteral in form: must be true@."; + [simp_true] + | _ -> List.rev rev_res end | F_Clause _ -> begin (* <=> OR *) - let () = debug "F_Clause@." in - let state, rev_res = + let () = debug "[simp_form] F_Clause@." in + let _state, rev_res = fold_left_stop (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 + debug "[simp_form] Simplified %a into %a in clause@." + E.print e pp_simp esimp; if is_false esimp then ( - debug "%a = false@." E.print e; + debug "[simp_form] %a = false@." E.print e; (state, simp_exps), false ) else if is_true esimp then ( - debug "%a = true@." E.print e; + debug "[simp_form] %a = true@." E.print e; (state, [simp_true]), true ) else ( - debug "Keeping %a@." E.print e; - (D.join state esimp.v, (esimp :: simp_exps))) + debug "[simp_form] Keeping %a@." E.print e; + (state, (esimp :: simp_exps))) , false) (state, []) elist in match rev_res with - | [] -> state, [simp_false] - | _ -> state, List.rev rev_res + | [] -> + debug "[simp_form] No more litteral in form: must be false@."; + [simp_false] + | _ -> List.rev rev_res end | _ -> - let () = debug "No additional simplification@." in - D.top, List.map (identity D.top) elist + let () = debug "[simp_form] No additional simplification@." in + List.map (identity state) elist - and simp_expr state (e : E.t) : (E.t, v) simp = + 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; - 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 - debug "[simp_expr] Ite treated@."; - match simp with - | [branch] -> - 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 - (* 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} - end else begin - (* A simplification has been made *) - debug "[simp_expr] Simplification worked on a branch@."; { - exp = E.mk_term (Op Tite) [cond.exp; th.exp; el.exp] ty; - diff = true; - v = D.join th.v el.v - } - end else begin - debug "[simp_expr] Simplification worked on a branch@."; - { (* Simplification failed *) + let 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 + debug "[simp_expr] Ite treated@."; + match simp with + | [branch] -> + 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 + (* 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} + end else begin + (* A simplification has been made *) + debug "[simp_expr] Simplification worked on a branch@."; { + 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@."; + { (* Simplification failed *) + exp = e; + diff = false; + v = D.v_join th.v el.v + } end + | _ -> assert false + end + | Op Tite, _ -> assert false + | Symbols.Form (F_Skolem | F_Lemma), _ -> + debug "[simp_expr] Skolem/Lemmas not simplified"; + { + exp = e; + diff = false; + v = D.unknown + } + | Symbols.Form f, _ -> begin + debug "[simp_expr] Formula: %a@." Symbols.print symb; + let l = simp_form state f elist in + match l with + | [] -> assert false + | hd :: tl -> + if hd.diff || List.exists (fun e -> e.diff) tl then + begin + let make = + (match f with + | F_Unit b -> (fun e e' -> E.mk_and e e' b) + | F_Clause b -> (fun e e' -> E.mk_or e e' b) + | F_Iff -> E.mk_iff + | F_Xor -> E.mk_xor + | F_Skolem | F_Lemma -> assert false) in + 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.join th.v el.v - } end - | _ -> assert false + v = D.unknown + } end - | Op Tite, _ -> assert false - | Symbols.Form f, _ -> - debug "[simp_expr] Formula: %a@." Symbols.print symb; - let v, l = simp_form state f 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 - } - else {exp = e; diff = false; v = D.top} - | Symbols.Lit _, _ -> begin - debug - "[simp_expr] Litteral : %a@." - Symbols.print symb; - match add_lit_constraint state e with - | AlreadyTrue -> simp_true - | AlreadyFalse -> simp_false - | NewConstraint v -> {exp = e; diff = false; v} - end - | _ -> - debug - "[simp_expr] Other: %a@." - Symbols.print symb; - let (l : (E.t, v) simp list) = List.map (simp_expr state) elist in ( + | Symbols.Lit _, _ -> begin + debug + "[simp_expr] Litteral : %a@." + Symbols.print symb; + match add_lit_constraint state e with + | AlreadyTrue -> + debug "[simp_expr] Litteral %a is true@." E.print e; + 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 + } + 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 { + exp = E.mk_let let_v simp_let.exp simp_in.exp (-43); + diff = simp_let.diff || simp_in.diff; + v = simp_in.v + } + | _ -> assert false + end + + | Symbols.Let, _ -> assert false + | _ -> + 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.top + v = D.eval_expr e state } - else {exp = e; diff = false; v = D.top} - ) + else {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 + + and simp_expr state (e : E.t) : (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 (** Wrapper of simp_expr for verbose *) let simp_expr e = @@ -470,10 +600,10 @@ module SimpleReasoner debug "No change on %a@." E.print e in - identity res.v e + identity D.top e with Failure s -> - talk + debug "Error while simplifying %a\n%s\n\ I will continue with the initial expression@." E.print e diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli index bc0ddbf5d..c320c068c 100644 --- a/src/lib/frontend/simple_reasoner_expr.mli +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -29,23 +29,37 @@ type 'abs_val add_constraint_res = | AlreadyFalse (* The constraint is already false*) | NewConstraint of 'abs_val (* The new abstract value *) +(** Dom is the signature of the abstact domain. *) module type Dom = sig - type v + type v (* The raw abstract value. For the interval domain, an interval *) + type state (* The global state representation. Usually a map of 'v's *) (** Top/Bottom value *) - val top : v - val bottom : v + val top : state + val bottom : state + + val vrai : v + val faux : v + val unknown : v (** (Partial) Compare function *) - val compare : v -> v -> int option + val compare : state -> state -> int option (** Join operator *) - val join : v -> v -> v + val join : state -> state -> state + val v_join : v -> v -> v (** Add constraint *) - val add_constraint : Expr.t -> Expr.t -> Symbols.lit -> v -> v 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 + + (** Evaluates an expression in the given state. *) + val eval_expr : Expr.t -> state -> v - val pp : Format.formatter -> v -> unit + val pp : Format.formatter -> state -> unit + val pp_v : Format.formatter -> v -> unit end (** This is the signature of the simplifyer. *) diff --git a/src/lib/reasoners/polynome.ml b/src/lib/reasoners/polynome.ml index 50c17649b..bb91ca36d 100644 --- a/src/lib/reasoners/polynome.ml +++ b/src/lib/reasoners/polynome.ml @@ -90,8 +90,7 @@ module type T = sig module M : Map.S with type key = r module Eval (C : Calc) : sig - exception MissingVar - val eval : C.t M.t -> t -> C.t + val eval : (r -> C.t) -> t -> C.t end end @@ -374,13 +373,8 @@ module Make (X : S) = struct module Eval (C : Calc) = struct - exception MissingVar - - let eval_monom(map : C.t M.t) (r : r) (q : Q.t) (acc : C.t) = - match M.find_opt r map with - | None -> raise MissingVar - | Some v -> - C.add acc (C.mul q v) + let eval_monom (map : r -> C.t) (r : r) (q : Q.t) (acc : C.t) = + C.add acc (C.mul q (map r)) let eval map p = M.fold (eval_monom map) p.m (C.mul p.c C.one) diff --git a/src/lib/reasoners/polynome.mli b/src/lib/reasoners/polynome.mli index 8dfd07618..c100ae911 100644 --- a/src/lib/reasoners/polynome.mli +++ b/src/lib/reasoners/polynome.mli @@ -92,8 +92,7 @@ module type T = sig module M : Map.S with type key = r module Eval (C : Calc) : sig - exception MissingVar - val eval : C.t M.t -> t -> C.t + val eval : (r -> C.t) -> t -> C.t end end diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index 5c86d02f3..ab35047a5 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -16,7 +16,9 @@ module A = Shostak.Arith module P = Shostak.Polynome module M = P.M -let verb = Options.get_simplify_verbose +exception EmptyInterval + +let verb = Options.get_debug_simplify let silent (msg : ('a, Format.formatter, unit) format) = Format.ifprintf Format.std_formatter msg @@ -34,12 +36,20 @@ module DummySimp = SRE.SimpleReasoner (struct type v = unit + type state = unit let top = () let bottom = () let compare _ _ = Some 0 let join _ _ = () let add_constraint _ _ _ _ = SRE.NewConstraint () let pp fmt _ = Format.fprintf fmt "()" + let unknown = () + let faux = () + let vrai = () + let pp_v fmt _ = Format.fprintf fmt "()" + let eval_expr _ _ = () + let v_join _ _ = () + let add_raw_value _ _ _ = () end ) @@ -64,18 +74,27 @@ let compare_abs_val cmp v1 v2 = | Value v1, Value v2 -> cmp v1 v2 module IntervalsDomain : - SRE.Dom with type v = Intervals.t abstract_value M.t abstract_value = struct - type v = Intervals.t abstract_value M.t abstract_value + 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 + type state = v M.t abstract_value let top = Top - let bottom : v = Bottom + let bottom = Bottom + + let faux = Value (Intervals.point Q.zero Ty.Tbool Explanation.empty) + let vrai = Value (Intervals.point Q.one Ty.Tbool Explanation.empty) + let unknown = Top + let pp_v = pp_abs_val Intervals.print let pp fmt v = pp_abs_val (fun fmt -> M.iter - (fun r i -> Format.fprintf fmt "%a = %a" + (fun r i -> Format.fprintf fmt "\n%a = %a" R.print r - (pp_abs_val Intervals.print) i)) + pp_v i + )) fmt v @@ -138,6 +157,14 @@ module IntervalsDomain : let compare = compare_abs_val compare + let v_join v1 v2 = + match v1, v2 with + | Top, _ + | _, Top -> Top + | v, Bottom + | Bottom, v -> v + | Value v1, Value v2 -> Value (Intervals.merge v1 v2) + let join = M.merge (fun _k v1 v2 -> @@ -146,14 +173,7 @@ module IntervalsDomain : | ((Some _) as v), None -> v | None, None -> assert false - - | Some Top, Some _ - | Some _, Some Top -> Some Top - - | ((Some _) as v), Some Bottom - | Some Bottom, ((Some _) as v) -> v - - | Some (Value v1), Some (Value v2) -> Some (Value (Intervals.merge v1 v2))) + | Some i1, Some i2 -> Some (v_join i1 i2)) let join v1 v2 = match v1, v2 with @@ -163,8 +183,8 @@ module IntervalsDomain : | v, Bottom -> v | Value i1, Value i2 -> Value (join i1 i2) - let eval_constraint (ty : Ty.t) (v : v) (p : P.t) : Intervals.t abstract_value = - match v with + 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 | [], q -> Value (Intervals.point q ty Explanation.empty) @@ -173,7 +193,7 @@ module IntervalsDomain : | Bottom -> Bottom | Value v -> let ty = P.type_info p in - let module E = P.Eval (struct + let module Ev = P.Eval (struct type t = Intervals.t abstract_value let one = Value (Intervals.point Q.one ty Explanation.empty) let add i1 i2 = @@ -191,11 +211,15 @@ module IntervalsDomain : else Top | Bottom -> Bottom | Value i -> - Value (Intervals.affine_scale ~const:Q.zero ~coef i) + Value (Intervals.scale coef i) end) in (* todo: apply functor statically for each type *) - E.eval v p + let map r = + match M.find_opt r v with + | None -> Top + | Some v -> v in + Ev.eval map p - let rfind ty k (v : v) = match v with + let rfind ty k (v : state) = match v with | Bottom -> failwith "Value is bottom: Should have been checked beforehand" | Top -> Intervals.undefined ty | Value m -> match M.find_opt k m with @@ -203,52 +227,61 @@ module IntervalsDomain : | Some Bottom -> failwith "Internal value is bottom: Should have been checked beforehand" | Some (Value i) -> i - let radd k b v = match v with - | Top -> Value (M.add k b M.empty) - | Value m -> Value (M.add k b m) - | Bottom -> v + let radd k b v = + match b with + | Top -> v + | _ -> match v with + | Top -> Value (M.add k b M.empty) + | Value m -> Value (M.add k b m) + | Bottom -> v let fix_point (narrow : rinter:Intervals.t -> prev_inter:Intervals.t -> Intervals.t * bool) (ty : Ty.t) (constraints : (Q.t * R.r * P.t) list) - (v : v) = - let rec aux v = + (s : state) = + let rec aux s = let new_vars, keep_iterating = List.fold_left - (fun ((v : v), keep_iterating) (q,r,p) -> + (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; - match eval_constraint ty v p with + debug "[fix_point] Evaluating with state %a@." pp s; + match eval_constraint ty s p with | Top - | Bottom -> v, false + | Bottom -> s, false | Value i -> (* Deducing the value of `r` *) debug "[fix_point] %a = %a@." P.print p Intervals.print i; if Intervals.is_undefined i then begin debug "[fix_point] No information, continuing@."; - v, keep_iterating + s, keep_iterating end else begin debug "[fix_point] Narrowing@."; let rinter = Intervals.scale (Q.div Q.one q) i in - let prev_inter = rfind ty r v in + debug "[fix_point] Inteval of %a by the constraint : %a@." R.print r Intervals.print rinter; + let prev_inter = rfind ty r s in let ri, change = narrow ~rinter ~prev_inter in - debug "[fix_point] %a ~~> %a@." Intervals.print rinter Intervals.print prev_inter; + debug "[fix_point] Old interval of %a : %a@." + R.print r Intervals.print prev_inter; + debug "[fix_point] New interval of %a : %a@." + R.print r Intervals.print ri; + if change then - radd r (Value ri) v, change + radd r (Value ri) s, change else - v, keep_iterating + s, keep_iterating end ) - (v, false) + (s, false) constraints in - if keep_iterating then aux new_vars else v in - aux v + if keep_iterating then aux new_vars else s in + aux s let narrow_eq ~rinter ~prev_inter = debug "[fix_point] Narrow EQ@."; - if Intervals.contained_in rinter prev_inter + if Intervals.contained_in rinter prev_inter && not (Intervals.equal rinter prev_inter) then rinter, true else prev_inter, false @@ -264,28 +297,45 @@ module IntervalsDomain : else prev_inter, false let narrow_le ~rinter ~prev_inter = - debug "[fix_point] Narrow LE@."; + debug "[fix_point] Narrow LE ; r_inter = %a -- previous_inter = %a @." + Intervals.print rinter Intervals.print prev_inter + ; try let bound , _, is_le = Intervals.borne_sup rinter in let prev_sup = try - let s, _, _ = Intervals.borne_sup prev_inter in s + let s, _, _ = Intervals.borne_sup prev_inter in Some s with - Intervals.No_finite_bound -> (* A value satisfying the next condition *) - Q.sub bound Q.one in - if Q.compare bound prev_sup <= 0 then begin - debug "[fix_point] %a <= %a@." Q.print bound Q.print prev_sup; - prev_inter, false - end else - (* The new upper bound is lower than then previous one, - replacing it *) + Intervals.No_finite_bound -> None in + match prev_sup with + | None -> + debug "[fix_point] New constraint upper bound: %a" Q.print bound; Intervals.new_borne_sup Explanation.empty bound ~is_le 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@." + 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@." + Q.print bound Q.print prev_sup; + debug "[fix_point] Narrowing@."; + Intervals.new_borne_sup + Explanation.empty + bound + ~is_le + prev_inter, true + end with | Intervals.No_finite_bound -> prev_inter, false + | Intervals.NotConsistent _ -> raise EmptyInterval let narrow_lt ~rinter ~prev_inter = debug "[fix_point] Narrow LT@."; @@ -293,22 +343,37 @@ module IntervalsDomain : let bound , _, _ = Intervals.borne_sup rinter in let prev_sup = try - let s, _, _ = Intervals.borne_sup prev_inter in s + let s, _, _ = Intervals.borne_sup prev_inter in Some s with - Intervals.No_finite_bound -> (* A value satisfying the next condition *) - Q.sub bound Q.one in - if Q.compare bound prev_sup <= 0 then - (* The new upper bound is higher then the previous one, - keeping it *) - prev_inter, false - else - (* The new upper bound is lower than then previous one, - replacing it *) + Intervals.No_finite_bound -> None in + match prev_sup with + | None -> + debug "[fix_point] New constraint upper bound: %a" Q.print bound; Intervals.new_borne_sup Explanation.empty bound ~is_le:false prev_inter, true + | Some prev_sup -> + 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" + 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" + Q.print bound Q.print prev_sup; + debug "[fix_point] Narrowing"; + Intervals.new_borne_sup + Explanation.empty + bound + ~is_le:false + prev_inter, true + end with | Intervals.No_finite_bound -> prev_inter, false @@ -317,32 +382,43 @@ module IntervalsDomain : try let bound , _, _ = Intervals.borne_inf rinter in let prev_inf = - try let s , _, _ = Intervals.borne_inf prev_inter in s with - | Intervals.No_finite_bound -> (* A value satisfying the next condition *) - Q.add bound Q.one + try + let s , _, _ = Intervals.borne_inf prev_inter in Some s + with + | Intervals.No_finite_bound -> + None in - if Q.compare prev_inf bound > 0 then - prev_inter, false - else + match prev_inf with + | None -> 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 with | Intervals.No_finite_bound -> prev_inter, false + | Intervals.NotConsistent _ -> raise EmptyInterval let narrow_ge ~rinter ~prev_inter = debug "[fix_point] Narrow GE@."; try let bound , _, is_le = Intervals.borne_inf rinter in let prev_inf = - try let s , _, _ = Intervals.borne_inf prev_inter in s with - | Intervals.No_finite_bound -> (* A value satisfying the next condition *) - Q.add bound Q.one + try let s , _, _ = Intervals.borne_inf prev_inter in Some s with + | Intervals.No_finite_bound -> None in - if Q.compare prev_inf bound > 0 then - prev_inter, false - else + match prev_inf with + | None -> 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 with | Intervals.No_finite_bound -> prev_inter, false + | Intervals.NotConsistent _ -> raise EmptyInterval let fix_point_eq = fix_point narrow_eq let fix_point_neq = fix_point narrow_neq @@ -411,20 +487,44 @@ module IntervalsDomain : failwith "Check constraint : todo (even a better error message would be nice)" end + let to_arith e = A.embed @@ fst @@ R.make e + (* 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 p1 = A.embed @@ fst (R.make l1) in - let p2 = A.embed @@ fst (R.make l2) in + 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; + let p1 = to_arith l1 in + let p2 = to_arith l2 in + let p = P.sub p1 p2 in + debug "[add_constraint] Constraint : %a %a 0@." P.print p Symbols.print l; let ty = P.type_info p1 in (* l1 R l2 <=> p + c R 0 *) - let (p, c, _cst) = P.normal_form_pos (P.sub p1 p2) in - - debug "Constraint : %a + %a R 0@." P.print p Q.print c; + let (p, c, cst) = P.normal_form_pos p 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 + + let p, c, _cst = + let den = Q.from_z @@ Q.den c in + P.mult_const den p, Q.from_z @@ Q.num c, Q.mult den cst in + + debug "[add_constraint] Normalized constraint : %a + %a %a 0@." + P.print p Q.print c Symbols.print l; + debug "[add_constraint] Known information: %a@." pp v; let mc = Q.minus c in @@ -433,13 +533,32 @@ module IntervalsDomain : | Some false -> AlreadyFalse | None -> (* p = \Sum (q_i * r_i) - p R c <=> \A i. q_i * r_i = p - (q_i * r_i) - c *) + p R c <=> \A i. q_i * r_i R (q_i * r_i) - p + c *) let constraints = P.fold_on_vars - (fun r q acc_cstr -> ((q, r, P.sub p (P.create [q,r] c ty)) :: acc_cstr)) + (fun r q acc_cstr -> ((q, r, P.sub (P.create [q,r] c ty) p) :: acc_cstr)) p [] in - NewConstraint (fix_point lit ty constraints v) + try + let new_constraint = fix_point lit ty constraints v in + debug "[add_constraint] New constraint: %a@." pp new_constraint; + NewConstraint new_constraint + with + | EmptyInterval -> + (* fix_point calculation reduced a variable to the empty interval *) + debug "[add_constraint] Inconsistent interval, returning `false`@."; + AlreadyFalse + + let eval_expr e s = + match E.term_view e with + | Not_a_term _ -> unknown + | Term _ -> + eval_constraint (E.type_info e) s (A.embed @@ fst @@ R.make e) + + let add_raw_value e v (s : state) = + let r = fst @@ R.make e in + debug "[add_raw_value] Adding %a = %a in %a@." R.print r pp_v v pp s ; + radd r v s end module IntervalsSimp = diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index dc72e7afd..0d789640b 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -490,7 +490,7 @@ let used_context_file = ref "" let js_mode = ref false let simplify = ref Util.SNo let simplify_th = ref true -let simplify_verbose = ref true +let debug_simplify = ref false let set_timers b = timers := b let set_status s = status := match_known_status s @@ -500,7 +500,7 @@ let set_used_context_file f = used_context_file := f let set_js_mode b = js_mode := b let set_simplify s = simplify := s let set_simplify_th b = simplify_th := b -let set_simplify_verbose b = simplify_verbose := b +let set_debug_simplify b = debug_simplify := b let get_timers () = !timers || !profiling let get_file () = !file @@ -510,7 +510,7 @@ let get_used_context_file () = !used_context_file let get_js_mode () = !js_mode let get_simplify () = !simplify let get_simplify_th () = !simplify_th -let get_simplify_verbose () = !simplify_verbose +let get_debug_simplify () = !debug_simplify (** particular getters : functions that are immediately executed **************) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index b166ca53f..f31b1c9ee 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -281,7 +281,7 @@ val set_simplify : Util.simplify -> unit val set_simplify_th : bool -> unit (** Set [simplify_verbose] accessible with {!val:get_simplify_verbose} *) -val set_simplify_verbose : bool -> unit +val set_debug_simplify : bool -> unit (** Setters used by parse_command *) @@ -980,7 +980,7 @@ val get_simplify_th : unit -> bool (** Default to [true] *) (** Gets the simplify verbose mode: [false] => no verbose *) -val get_simplify_verbose : unit -> bool +val get_debug_simplify : unit -> bool (** Default to [false] *) (** Value specifying the file given to Alt-Ergo *) From ba41bbaf8b14c8982ec330e2bf0d8d5cb4ee15ec Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 17 Mar 2021 14:02:57 +0100 Subject: [PATCH 04/18] Replacing 'Intervals.scale' by Intervals arithmetic operators --- src/lib/reasoners/simplifiers.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index ab35047a5..26848e7c7 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -211,7 +211,7 @@ module IntervalsDomain : else Top | Bottom -> Bottom | Value i -> - Value (Intervals.scale coef 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 @@ -259,15 +259,18 @@ module IntervalsDomain : s, keep_iterating end else begin debug "[fix_point] Narrowing@."; - let rinter = Intervals.scale (Q.div Q.one q) i in - debug "[fix_point] Inteval of %a by the constraint : %a@." R.print r Intervals.print rinter; + 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 + debug "[fix_point] Inteval of %a by the constraint : %a@." + R.print r + Intervals.print rinter; let prev_inter = rfind ty r s in let ri, change = narrow ~rinter ~prev_inter in debug "[fix_point] Old interval of %a : %a@." R.print r Intervals.print prev_inter; debug "[fix_point] New interval of %a : %a@." R.print r Intervals.print ri; - if change then radd r (Value ri) s, change else @@ -279,6 +282,7 @@ 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 Intervals.contained_in rinter prev_inter && not (Intervals.equal rinter prev_inter) @@ -358,16 +362,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"; + debug "[fix_point] Narrowing@."; Intervals.new_borne_sup Explanation.empty bound From 158ea206774fc8affc5d7de7db93d1f7e4b824a9 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 18 Mar 2021 09:15:55 +0100 Subject: [PATCH 05/18] Sign bugfix --- src/lib/reasoners/simplifiers.ml | 37 +++++++++++++++++++++++--------- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index 26848e7c7..ad86e11d1 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -509,7 +509,24 @@ module IntervalsDomain : (* l1 R l2 <=> p + c R 0 *) let (p, c, cst) = P.normal_form_pos p in - let is_neg = Q.compare cst Q.zero < 0 in + + let p, c = + let den = Q.from_z @@ Q.den c in + P.mult_const den p, Q.from_z @@ Q.num c in + + let lit = + if Q.compare cst Q.zero < 0 then + 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 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, @@ -520,27 +537,27 @@ module IntervalsDomain : | L_neg_built LE -> L_built LT | L_neg_built LT -> L_built LE | l -> l - else p, c, lit in - - let p, c, _cst = - let den = Q.from_z @@ Q.den c in - P.mult_const den p, Q.from_z @@ Q.num c, Q.mult den cst in + else p, c, lit in *) debug "[add_constraint] Normalized constraint : %a + %a %a 0@." - P.print p Q.print c Symbols.print l; + P.print p Q.print c Symbols.print (Lit lit); debug "[add_constraint] Known information: %a@." pp v; + (* Checking if p R -c *) let mc = Q.minus c in - match check_constraint ty lit p mc v with | Some true -> SRE.AlreadyTrue | Some false -> AlreadyFalse | None -> + (* p R -c cannot be deduced from state : adding constraint *) (* p = \Sum (q_i * r_i) - p R c <=> \A i. q_i * r_i R (q_i * r_i) - p + c *) + p R -c <=> \A i. q_i * r_i R (q_i * r_i) - p - c *) let constraints = P.fold_on_vars - (fun r q acc_cstr -> ((q, r, P.sub (P.create [q,r] c ty) p) :: acc_cstr)) + (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'; + ((q, r, p') :: acc_cstr)) p [] in try From 7ef2a6b12427af25cafa3eb13ae081b2cf280d0d Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Fri, 19 Mar 2021 15:23:32 +0100 Subject: [PATCH 06/18] Not calling mk_let if a simplification has not been performed --- src/lib/frontend/simple_reasoner_expr.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index 02e0ad86a..f7f7ad093 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -541,11 +541,12 @@ module SimpleReasoner 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 { - exp = E.mk_let let_v simp_let.exp simp_in.exp (-43); - diff = simp_let.diff || simp_in.diff; - v = simp_in.v - } + 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} | _ -> assert false end From c5eb81aa2507576de4815bb352899cd31d29ad65 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 22 Mar 2021 15:58:21 +0100 Subject: [PATCH 07/18] Adding a reinitialization function to hconsing --- src/lib/util/hconsing.ml | 6 ++++++ src/lib/util/hconsing.mli | 3 +++ 2 files changed, 9 insertions(+) diff --git a/src/lib/util/hconsing.ml b/src/lib/util/hconsing.ml index 4e4b89301..71ed1ba29 100644 --- a/src/lib/util/hconsing.ml +++ b/src/lib/util/hconsing.ml @@ -42,6 +42,7 @@ end module type S = sig type t + val empty : unit -> unit val make : t -> t val elements : unit -> t list end @@ -62,6 +63,11 @@ struct let next_id = ref 0 + let empty () = + next_id := 0; + retain_list := []; + HWeak.clear storage + let make d = let d = Hashed.set_id !next_id d in let o = HWeak.merge storage d in diff --git a/src/lib/util/hconsing.mli b/src/lib/util/hconsing.mli index f9cd136b6..937e3518e 100644 --- a/src/lib/util/hconsing.mli +++ b/src/lib/util/hconsing.mli @@ -76,6 +76,9 @@ module type S = sig type t (** The type of value used. *) + val empty : unit -> unit + (** Resets the hashconsing storage *) + val make : t -> t (** Hashcons a value [t], either returning [t], or a value equal to [t] that was hashconsed previously. *) From 69db321582c64d62f38b7b3629b9dee1d0a645c6 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 22 Mar 2021 15:59:28 +0100 Subject: [PATCH 08/18] Adding a reinitialization function for the cache of Shostak.Combine.make --- src/lib/frontend/cnf.ml | 15 +++++++++++---- src/lib/reasoners/shostak.ml | 12 +++++++++--- src/lib/reasoners/sig.mli | 2 ++ 3 files changed, 22 insertions(+), 7 deletions(-) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index a07023d43..1c7d7290c 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -520,15 +520,22 @@ let make_form name f loc ~decl_kind = | Util.SPreprocess | Util.SAll -> let module S = SimpExprPreproc () in let smp_form = S.simp_expr form in - if SRE.has_changed smp_form then SRE.get_expr smp_form - else form + if SRE.has_changed smp_form then + let exp = SRE.get_expr smp_form in + exp + else begin + form + end in + Shostak.Combine.empty_cache (); assert (Sy.Map.is_empty (E.free_vars ff Sy.Map.empty)); let ff = E.purify_form ff in - if Ty.Svty.is_empty (E.free_type_vars ff) then ff - else + if Ty.Svty.is_empty (E.free_type_vars ff) then begin + ff + end else begin let id = E.id ff in E.mk_forall name loc Symbols.Map.empty [] ff id ~toplevel:true ~decl_kind + end let mk_assume acc f name loc = let ff = make_form name f loc ~decl_kind:E.Daxiom in diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index c51033843..89f6fe10e 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -118,6 +118,8 @@ struct module HC = Hconsing.Make(View) + let empty_cache () = HC.empty () + let hcons v = HC.make v (* end: Hconsing modules and functions *) @@ -738,12 +740,16 @@ and AC : Ac.S module Combine = struct include CX - let make = + let make, empty_cache = let cache = H.create 1024 in - fun t -> + let make t = match H.find_opt cache t with | None -> let res = make t in H.add cache t res; res - | Some res -> res + | Some res -> res in + let empty () = + empty_cache (); + H.clear cache in + make, empty end module Arith = X1 diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index 59a755529..2484cb42a 100644 --- a/src/lib/reasoners/sig.mli +++ b/src/lib/reasoners/sig.mli @@ -94,6 +94,8 @@ end module type X = sig type r + val empty_cache : unit -> unit + val make : Expr.t -> r * Expr.t list val type_info : r -> Ty.t From 2bf23ee7fa3fc8d5ce5c375389a5d1bda8e82364 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Wed, 24 Mar 2021 10:21:15 +0100 Subject: [PATCH 09/18] Also emptying simplifier's cache --- src/lib/frontend/cnf.ml | 6 ++++- src/lib/frontend/simple_reasoner_expr.ml | 8 ++++++ src/lib/frontend/simple_reasoner_expr.mli | 3 +++ src/lib/reasoners/simplifiers.ml | 30 +++++++++++++---------- 4 files changed, 33 insertions(+), 14 deletions(-) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 1c7d7290c..a45e26eea 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -520,6 +520,11 @@ let make_form name f loc ~decl_kind = | Util.SPreprocess | Util.SAll -> let module S = SimpExprPreproc () in let smp_form = S.simp_expr form in + let () = + (* Emptying the caches modified by the simplifier. + St : This is necessary for having consistent results. *) + Shostak.Combine.empty_cache (); + S.empty_caches () in if SRE.has_changed smp_form then let exp = SRE.get_expr smp_form in exp @@ -527,7 +532,6 @@ let make_form name f loc ~decl_kind = form end in - Shostak.Combine.empty_cache (); assert (Sy.Map.is_empty (E.free_vars ff Sy.Map.empty)); let ff = E.purify_form ff in if Ty.Svty.is_empty (E.free_type_vars ff) then begin diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index f7f7ad093..395036d5c 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -108,6 +108,9 @@ module type S = sig type v + (** Empties the simplifier caches *) + val empty_caches : unit -> unit + (** Simplifies an expression. *) val simp_expr : Expr.t -> (Expr.t, v) simp end @@ -123,6 +126,11 @@ module SimpleReasoner 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 := diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli index c320c068c..30e6423f1 100644 --- a/src/lib/frontend/simple_reasoner_expr.mli +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -67,6 +67,9 @@ module type S = sig type v + (** Empties the simplifier caches *) + val empty_caches : unit -> unit + (** Simplifies an expression and returns its associated abstract value. *) val simp_expr : Expr.t -> (Expr.t, v) simp end diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index ad86e11d1..e754117cd 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -219,21 +219,23 @@ module IntervalsDomain : | Some v -> v in Ev.eval map p - let rfind ty k (v : state) = match v with + let rfind ty k (s : state) = match s with | Bottom -> failwith "Value is bottom: Should have been checked beforehand" | Top -> Intervals.undefined ty - | Value m -> match M.find_opt k m with + | 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 (Value i) -> i + | Some ((Value i) as v) -> + debug "[rfind] Found %a in state %a, associated to %a@." R.print k pp s pp_v v; i - let radd k b v = + let radd k b s = match b with - | Top -> v - | _ -> match v with + | Top -> s + | _ -> match s with | Top -> Value (M.add k b M.empty) | Value m -> Value (M.add k b m) - | Bottom -> v + | Bottom -> s let fix_point (narrow : rinter:Intervals.t -> prev_inter:Intervals.t -> Intervals.t * bool) @@ -252,7 +254,7 @@ module IntervalsDomain : | Bottom -> s, false | Value i -> (* Deducing the value of `r` *) - debug "[fix_point] %a = %a@." P.print p Intervals.print i; + debug "[fix_point] %a R %a@." P.print p Intervals.print i; if Intervals.is_undefined i then begin debug "[fix_point] No information, continuing@."; @@ -262,10 +264,11 @@ module IntervalsDomain : 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 - debug "[fix_point] Inteval of %a by the constraint : %a@." + 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; let ri, change = narrow ~rinter ~prev_inter in debug "[fix_point] Old interval of %a : %a@." R.print r Intervals.print prev_inter; @@ -296,12 +299,13 @@ module IntervalsDomain : match Intervals.is_point rinter with | None -> prev_inter, false | Some (q, _) -> - if Intervals.contains prev_inter q then + 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 - else prev_inter, false + end else prev_inter, false let narrow_le ~rinter ~prev_inter = - debug "[fix_point] Narrow LE ; r_inter = %a -- previous_inter = %a @." + debug "[fix_point] Narrow LE ; r_inter = %a -- previous_inter = %a@." Intervals.print rinter Intervals.print prev_inter ; try @@ -313,7 +317,7 @@ module IntervalsDomain : Intervals.No_finite_bound -> None in match prev_sup with | None -> - debug "[fix_point] New constraint upper bound: %a" Q.print bound; + debug "[fix_point] New constraint upper bound: %a@." Q.print bound; Intervals.new_borne_sup Explanation.empty bound From f5b4d22c8e221c5857d023c9fba75656a27cafcf Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 29 Mar 2021 09:43:18 +0200 Subject: [PATCH 10/18] Correct indent --- src/lib/frontend/simple_reasoner_expr.ml | 60 ++++++++++++------------ src/lib/reasoners/simplifiers.ml | 58 +++++++++++------------ 2 files changed, 59 insertions(+), 59 deletions(-) diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index 395036d5c..78e2ca1b4 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -46,10 +46,10 @@ let fold_left_stop in __fold acc l type ('expr, 'abs_val) simp = { - exp : 'expr; - diff : bool; - v : 'abs_val - } + exp : 'expr; + diff : bool; + v : 'abs_val +} let pp_simp pp_abs_val fmt s = Format.fprintf fmt "%a:%a" E.print s.exp pp_abs_val s.v @@ -375,7 +375,7 @@ module SimpleReasoner 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] - end + end and simp_form (state : state) @@ -500,31 +500,31 @@ module SimpleReasoner v = D.unknown } | Symbols.Form f, _ -> begin - debug "[simp_expr] Formula: %a@." Symbols.print symb; - let l = simp_form state f elist in - match l with - | [] -> assert false - | hd :: tl -> - if hd.diff || List.exists (fun e -> e.diff) tl then - begin - let make = - (match f with - | F_Unit b -> (fun e e' -> E.mk_and e e' b) - | F_Clause b -> (fun e e' -> E.mk_or e e' b) - | F_Iff -> E.mk_iff - | F_Xor -> E.mk_xor - | F_Skolem | F_Lemma -> assert false) in - 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 - } - end + debug "[simp_expr] Formula: %a@." Symbols.print symb; + let l = simp_form state f elist in + match l with + | [] -> assert false + | hd :: tl -> + if hd.diff || List.exists (fun e -> e.diff) tl then + begin + let make = + (match f with + | F_Unit b -> (fun e e' -> E.mk_and e e' b) + | F_Clause b -> (fun e e' -> E.mk_or e e' b) + | F_Iff -> E.mk_iff + | F_Xor -> E.mk_xor + | F_Skolem | F_Lemma -> assert false) in + 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 + } + end | Symbols.Lit _, _ -> begin debug "[simp_expr] Litteral : %a@." diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index e754117cd..8859fb5b7 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -186,10 +186,10 @@ module IntervalsDomain : 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 + match P.to_list p with | [], q -> Value (Intervals.point q ty Explanation.empty) | _ -> Top - end + end | Bottom -> Bottom | Value v -> let ty = P.type_info p in @@ -340,7 +340,7 @@ module IntervalsDomain : bound ~is_le prev_inter, true - end + end with | Intervals.No_finite_bound -> prev_inter, false | Intervals.NotConsistent _ -> raise EmptyInterval @@ -493,7 +493,7 @@ module IntervalsDomain : failwith "Check constraint: do not handle IsConstr" | L_neg_pred -> failwith "Check constraint : todo (even a better error message would be nice)" - end + end let to_arith e = A.embed @@ fst @@ R.make e @@ -521,11 +521,11 @@ module IntervalsDomain : let lit = if Q.compare cst Q.zero < 0 then 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 + | 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 lit in @@ -553,26 +553,26 @@ module IntervalsDomain : | Some true -> SRE.AlreadyTrue | Some false -> AlreadyFalse | None -> - (* p R -c cannot be deduced from state : adding constraint *) - (* p = \Sum (q_i * r_i) - p R -c <=> \A i. q_i * r_i R (q_i * r_i) - p - c *) - let constraints = - 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'; - ((q, r, p') :: acc_cstr)) - p - [] in - try - let new_constraint = fix_point lit ty constraints v in - debug "[add_constraint] New constraint: %a@." pp new_constraint; - NewConstraint new_constraint - with - | EmptyInterval -> - (* fix_point calculation reduced a variable to the empty interval *) - debug "[add_constraint] Inconsistent interval, returning `false`@."; - AlreadyFalse + (* p R -c cannot be deduced from state : adding constraint *) + (* p = \Sum (q_i * r_i) + p R -c <=> \A i. q_i * r_i R (q_i * r_i) - p - c *) + let constraints = + 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'; + ((q, r, p') :: acc_cstr)) + p + [] in + try + let new_constraint = fix_point lit ty constraints v in + debug "[add_constraint] New constraint: %a@." pp new_constraint; + NewConstraint new_constraint + with + | EmptyInterval -> + (* fix_point calculation reduced a variable to the empty interval *) + debug "[add_constraint] Inconsistent interval, returning `false`@."; + AlreadyFalse let eval_expr e s = match E.term_view e with From 6f09152d1b56aa470d01a667ba5699189c676304 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 29 Mar 2021 09:50:49 +0200 Subject: [PATCH 11/18] Moving eq_list to util.ml --- src/lib/structures/typed.ml | 39 +++++++++++++------------------------ src/lib/util/util.ml | 10 ++++++++++ src/lib/util/util.mli | 2 ++ 3 files changed, 26 insertions(+), 25 deletions(-) diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 3bf2726b5..851d4134a 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -205,17 +205,6 @@ and 'a tdecl = | TPush of Loc.t * int | TPop of Loc.t * int -let eq_list eq l1 l2 = - let rec loop l1 l2 = - match l1, l2 with - [],[] -> true - | hd1 :: tl1, hd2 :: tl2 -> - if eq hd1 hd2 - then loop tl1 tl2 - else false - | _,_ -> false - in loop l1 l2 - let eq_tconstant (c1 : tconstant) (c2 : tconstant) : bool = match c1, c2 with Tint s1, Tint s2 @@ -230,7 +219,7 @@ let eq_pattern (p1 : pattern) (p2 : pattern) : bool = Constr {name = name2; args = args2} -> Hstring.equal name1 name2 && - eq_list + Util.eq_list (fun (x1,s1,t1) (x2,s2,t2) -> Var.equal x1 x2 && Hstring.equal s1 s2 && @@ -259,7 +248,7 @@ and eq_tt_desc (e1 : 'a tt_desc) (e2 : 'a tt_desc) : bool = | TTapp (s1, l1), TTapp (s2, l2) -> Symbols.equal s1 s2 && - eq_list + Util.eq_list (fun t1 t2 -> eq_tterm t1.c t2.c) l1 l2 @@ -284,13 +273,13 @@ and eq_tt_desc (e1 : 'a tt_desc) (e2 : 'a tt_desc) : bool = eq_tterm t1.c t2.c | TTrecord l1, TTrecord l2 -> - eq_list + Util.eq_list (fun (s1,t1) (s2,t2) -> Hstring.equal s1 s2 && eq_tterm t1.c t2.c) l1 l2 | TTlet (l1, t1), TTlet (l2, t2) -> eq_tterm t1.c t2.c && - eq_list + Util.eq_list (fun (s1, t1) (s2, t2) -> Symbols.equal s1 s2 && eq_tterm t1.c t2.c) l1 @@ -305,7 +294,7 @@ and eq_tt_desc (e1 : 'a tt_desc) (e2 : 'a tt_desc) : bool = | TTmatch (t1, l1), TTmatch (t2, l2) -> eq_tterm t1.c t2.c && - eq_list + Util.eq_list (fun (p1,t1) (p2,t2) -> eq_pattern p1 p2 && eq_tterm t1.c t2.c ) @@ -324,7 +313,7 @@ and eq_tatom (a1 : 'a tatom) (a2 : 'a tatom) : bool = | TAneq l1, TAneq l2 | TAle l1, TAle l2 | TAlt l1, TAlt l2 -> - eq_list + Util.eq_list (fun t1 t2 -> eq_tterm t1.c t2.c) l1 l2 @@ -337,17 +326,17 @@ and eq_tatom (a1 : 'a tatom) (a2 : 'a tatom) : bool = and eq_quant_form (q1 : 'a quant_form) (q2 : 'a quant_form) : bool = let stylist = - eq_list + Util.eq_list (fun (s1,t1) (s2, t2) -> Symbols.equal s1 s2 && Ty.equal t1 t2) in stylist q1.qf_bvars q2.qf_bvars && stylist q1.qf_upvars q2.qf_upvars && - eq_list (fun f1 f2 -> eq_tform f1.c f2.c) q1.qf_hyp q2.qf_hyp && + Util.eq_list (fun f1 f2 -> eq_tform f1.c f2.c) q1.qf_hyp q2.qf_hyp && eq_tform q1.qf_form.c q2.qf_form.c && - eq_list + Util.eq_list (fun (tlist1,b1) (tlist2,b2) -> (b1 && (not b2) || (not b1) && b2) && - eq_list + Util.eq_list (fun t1 t2 -> eq_tterm t1.c t2.c) tlist1 tlist2) @@ -360,7 +349,7 @@ and eq_tform (f1 : 'a tform) (f2 : 'a tform) : bool = | TFop (op1, l1), TFop (op2, l2) -> (Stdlib.(=)) op1 op2 && - eq_list + Util.eq_list (fun f1 f2 -> eq_tform f1.c f2.c) l1 l2 @@ -371,11 +360,11 @@ and eq_tform (f1 : 'a tform) (f2 : 'a tform) : bool = | TFlet (stlist1, slklist1,f1), TFlet (stlist2, slklist2,f2) -> let stylist = - eq_list + Util.eq_list (fun (s1,t1) (s2, t2) -> Symbols.equal s1 s2 && Ty.equal t1 t2) in stylist stlist1 stlist2 && - eq_list + Util.eq_list (fun (s1,lf1) (s2, lf2) -> Symbols.equal s1 s2 && eq_tlet_kind lf1 lf2) slklist1 slklist2 && @@ -386,7 +375,7 @@ and eq_tform (f1 : 'a tform) (f2 : 'a tform) : bool = | TFmatch (t1, pfl1), TFmatch (t2, pfl2) -> eq_tterm t1.c t2.c && - eq_list + Util.eq_list (fun (p1, f1) (p2, f2) -> eq_pattern p1 p2 && eq_tform f1.c f2.c) pfl1 pfl2 diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index 1815cda8a..5a8bbac4a 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -149,3 +149,13 @@ let rec print_list_pp ~sep ~pp fmt = function Format.fprintf fmt "%a %a" pp x sep (); print_list_pp ~sep ~pp fmt l +let eq_list eq l1 l2 = + let rec loop l1 l2 = + match l1, l2 with + [],[] -> true + | hd1 :: tl1, hd2 :: tl2 -> + if eq hd1 hd2 + then loop tl1 tl2 + else false + | _,_ -> false + in loop l1 l2 diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 3c95df223..56efc0065 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -99,3 +99,5 @@ val print_list_pp: sep:(Format.formatter -> unit -> unit) -> pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit + +val eq_list : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool From 04e53e3d8c3f2a708b6722ee9652cda08c5d41f1 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 29 Mar 2021 09:56:34 +0200 Subject: [PATCH 12/18] Replacing vrai/faux by english equivalents --- src/lib/frontend/simple_reasoner_expr.ml | 8 ++++---- src/lib/frontend/simple_reasoner_expr.mli | 4 ++-- src/lib/reasoners/simplifiers.ml | 8 ++++---- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index 78e2ca1b4..93d2929a4 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -79,8 +79,8 @@ module type Dom = sig val top : state val bottom : state - val vrai : v - val faux : v + val _true : v + val _false : v val unknown : v (** (Partial) Compare function *) @@ -155,8 +155,8 @@ module SimpleReasoner let identity v exp = {exp; diff = false; v = D.eval_expr exp v} - let simp_true = {exp = E.vrai; diff = true; v = D.vrai} - let simp_false = {exp = E.faux; diff = true; v = D.faux} + 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 diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli index 30e6423f1..c589a3b3d 100644 --- a/src/lib/frontend/simple_reasoner_expr.mli +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -38,8 +38,8 @@ module type Dom = sig val top : state val bottom : state - val vrai : v - val faux : v + val _true : v + val _false : v val unknown : v (** (Partial) Compare function *) diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index 8859fb5b7..4b05b43d5 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -44,8 +44,8 @@ module DummySimp = let add_constraint _ _ _ _ = SRE.NewConstraint () let pp fmt _ = Format.fprintf fmt "()" let unknown = () - let faux = () - let vrai = () + let _false = () + let _true = () let pp_v fmt _ = Format.fprintf fmt "()" let eval_expr _ _ = () let v_join _ _ = () @@ -83,8 +83,8 @@ module IntervalsDomain : let top = Top let bottom = Bottom - let faux = Value (Intervals.point Q.zero Ty.Tbool Explanation.empty) - let vrai = Value (Intervals.point Q.one Ty.Tbool Explanation.empty) + let _false = Value (Intervals.point Q.zero Ty.Tbool Explanation.empty) + let _true = Value (Intervals.point Q.one Ty.Tbool Explanation.empty) let unknown = Top let pp_v = pp_abs_val Intervals.print From 1c792e267e2feebba1a3c830447f7d65a876dbe6 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 29 Mar 2021 10:13:11 +0200 Subject: [PATCH 13/18] Poetry --- src/lib/reasoners/th_util.ml | 3 ++- src/lib/structures/expr.ml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/lib/reasoners/th_util.ml b/src/lib/reasoners/th_util.ml index f1a13b5f2..d49865c16 100644 --- a/src/lib/reasoners/th_util.ml +++ b/src/lib/reasoners/th_util.ml @@ -26,7 +26,8 @@ (* *) (******************************************************************************) -(** An answer type. If it is Some (thing), then the answer is yes, +(** An answer type. + If it is Some (thing) then the answer is 'true' (for a boolean query), otherwise it is unknown. *) type answer = (Explanation.t * Expr.Set.t list) option diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7e553e1b3..8e9b3aacc 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -45,7 +45,7 @@ and view = { xs: t list; ty: Ty.t; (* expression type *) bind : bind_kind; - tag: int; (* always = -42 *) + tag: int; (* S : always = -42 ? *) vars : (Ty.t * int) SMap.t; (* vars to types and nb of occurences *) vty : Ty.Svty.t; depth: int; From 9501cb2222eb7889088c9cf64843b1c749814de7 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 29 Mar 2021 13:16:40 +0200 Subject: [PATCH 14/18] Fixing style --- src/lib/frontend/cnf.ml | 2 +- src/lib/frontend/simple_reasoner_expr.ml | 36 +++++-- src/lib/frontend/simple_reasoner_expr.mli | 7 +- src/lib/reasoners/simplifiers.ml | 120 +++++++++++++--------- src/lib/structures/typed.ml | 12 ++- 5 files changed, 113 insertions(+), 64 deletions(-) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index a45e26eea..24305fef0 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 93d2929a4..8d559ed55 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 c589a3b3d..a6a36dee5 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 4b05b43d5..9f8d3368c 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 851d4134a..6111b8145 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 From 7320c6194f9a98701fad05f1cd3a1565ca4dc279 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 19 Apr 2021 10:23:34 +0200 Subject: [PATCH 15/18] 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 24305fef0..d6b56e822 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -519,16 +519,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 8d559ed55..c83ed389a 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 a6a36dee5..88cae9461 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 9f8d3368c..c634f88be 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 From 384795c48424d1b54a34bf058fb51e668e7a87a6 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 28 Jul 2022 10:51:06 +0200 Subject: [PATCH 16/18] Rebase fix --- src/bin/common/parse_command.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index dceb514dd..7b556e7c6 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -438,7 +438,7 @@ let halt_opt version_info where = with Failure f -> `Error (false, f) | Error (b, m) -> `Error (b, m) -let mk_opts file () () () () () () halt_opt (gc) () () () () () () () () () +let mk_opts file () () () () () () halt_opt (gc) () () () () () () () () = if halt_opt then `Ok false @@ -632,6 +632,10 @@ let parse_dbg_opt_spl3 = let doc = "Set the debugging flag of warnings." in Arg.(value & flag & info ["dwarnings"] ~docs ~doc) in + let debug_simplify = + let doc = "Set the debugging flag of the simplifier." in + Arg.(value & flag & info ["dsimplify"] ~docs ~doc) in + let rule = let doc = "$(docv) = parsing|typing|sat|cc|arith, output rule used on stderr." in @@ -649,6 +653,7 @@ let parse_dbg_opt_spl3 = debug_unsat_core $ debug_use $ debug_warnings $ + debug_simplify $ rule )) @@ -1281,6 +1286,7 @@ let main = `S s_halt; `S s_fmt; `S s_debug; + `S s_simp; `P "These options are used to output debug info for the concerned \ part of the solver.\ They are $(b,not) used to check internal consistency."; From c3055eb9eb0d599fb4d6ee73fd3a339241c99812 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 28 Jul 2022 14:36:54 +0200 Subject: [PATCH 17/18] Adding option for activatiing simplifier --- src/bin/common/parse_command.ml | 23 +++++++++++++++++++++-- src/lib/frontend/cnf.ml | 8 ++++---- src/lib/util/util.ml | 1 - src/lib/util/util.mli | 1 - 4 files changed, 25 insertions(+), 8 deletions(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 7b556e7c6..77620ee20 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -438,7 +438,7 @@ let halt_opt version_info where = with Failure f -> `Error (false, f) | Error (b, m) -> `Error (b, m) -let mk_opts file () () () () () () halt_opt (gc) () () () () () () () () +let mk_opts file () () () () () () halt_opt (gc) () () () () () () () () () = if halt_opt then `Ok false @@ -468,6 +468,12 @@ let mk_fmt_opt std_fmt err_fmt set_err_fmt (value_of_fmt err_fmt); `Ok() +let mk_simplify simp_opt use_th = + set_simplify + (if simp_opt then SPreprocess else SNo); + set_simplify_th use_th; + `Ok () + (* Custom sections *) let s_debug = "DEBUG OPTIONS" @@ -1250,6 +1256,19 @@ let parse_fmt_opt = std_formatter $ err_formatter )) +let simplifier = + let docs = s_simp in + + let simplify = + let doc = "Activates the formula preprocessing" in + Arg.(value & flag & info ["simplify"] ~docs ~doc) + in + let simplify_th = + let doc = "Activates the use of theories during formula preprocessing" in + Arg.(value & flag & info ["simplify-th"] ~docs ~doc) + in + Term.(ret (const mk_simplify $ simplify $ simplify_th)) + let main = let file = @@ -1318,7 +1337,7 @@ let main = parse_execution_opt $ parse_halt_opt $ parse_internal_opt $ parse_limit_opt $ parse_output_opt $ parse_profiling_opt $ parse_quantifiers_opt $ parse_sat_opt $ parse_term_opt $ - parse_theory_opt $ parse_fmt_opt + parse_theory_opt $ parse_fmt_opt $ simplifier )) in let info = diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index d6b56e822..997696f35 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -293,16 +293,16 @@ let rec make_term up_qv quant_basename t = up_qv quant_basename e Loc.dummy ~decl_kind:E.Daxiom (* not correct, but not a problem *) ~toplevel:false - in mk_term t (* + in (*mk_term t*) let term = mk_term t in match Options.get_simplify () with | Util.SNo -> term - | Util.SPreprocess | Util.SAll -> + | Util.SPreprocess -> let module S = SimpExprPreproc () in let smp_term = S.simp_expr term in if SRE.has_changed smp_term then SRE.get_expr smp_term - else term *) + else term and make_trigger ~in_theory name up_qv quant_basename hyp (e, from_user) = let content, guard = match e with @@ -517,7 +517,7 @@ let make_form name f loc ~decl_kind = let form = make_form Sy.Map.empty name f loc ~decl_kind ~toplevel:true in match Options.get_simplify () with Util.SNo -> form - | Util.SPreprocess | Util.SAll -> + | Util.SPreprocess -> let module S = SimpExprPreproc () in (*Format.printf "Simplifying@.";*) let smp_form = S.simp_expr form in diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index 5a8bbac4a..721ae9e61 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -57,7 +57,6 @@ type theories_extensions = type simplify = | SNo | SPreprocess - | SAll type axiom_kind = Default | Propagator diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 56efc0065..eefcd6228 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -52,7 +52,6 @@ type theories_extensions = type simplify = | SNo | SPreprocess - | SAll type axiom_kind = Default | Propagator From 8369dfcd20c395a02701e6940ebf39c2af1963dd Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 16 Aug 2022 11:16:06 +0200 Subject: [PATCH 18/18] Replacing variables values when constant --- src/lib/frontend/cnf.ml | 14 ++++------- src/lib/frontend/simple_reasoner_expr.ml | 30 +++++++++++++++++------ src/lib/frontend/simple_reasoner_expr.mli | 2 ++ src/lib/reasoners/simplifiers.ml | 12 +++++++++ 4 files changed, 41 insertions(+), 17 deletions(-) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 997696f35..87a952107 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -525,15 +525,11 @@ let make_form name f loc ~decl_kind = (* Emptying the caches modified by the simplifier. St : This is necessary for having consistent results. *) Shostak.Combine.empty_cache (); - 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 + S.empty_caches (); () + in *) + if SRE.has_changed smp_form + then SRE.get_expr smp_form + else form in assert (Sy.Map.is_empty (E.free_vars ff Sy.Map.empty)); let ff = E.purify_form ff in diff --git a/src/lib/frontend/simple_reasoner_expr.ml b/src/lib/frontend/simple_reasoner_expr.ml index c83ed389a..94ee95879 100644 --- a/src/lib/frontend/simple_reasoner_expr.ml +++ b/src/lib/frontend/simple_reasoner_expr.ml @@ -88,8 +88,10 @@ module type Dom = sig val _true : v val _false : v val unknown : v + val const_int : Numbers.Q.t -> v val to_bool : v -> bool option + val to_int : v -> Numbers.Q.t option (** (Partial) Compare function *) val compare : state -> state -> int option @@ -165,11 +167,29 @@ module SimpleReasoner let simp_true = {exp = E.vrai; diff = true; v = D._true} let simp_false = {exp = E.faux; diff = true; v = D._false} + let simp_int i = {exp = E.int (Numbers.Q.to_string i); diff = true; v = D.const_int i} 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 to_const state e = + let ty = E.type_info e in + let eval_e = D.eval_expr e state in + match ty with + | Tbool -> begin + match D.to_bool eval_e with + | Some true -> simp_true + | Some false -> simp_false + | None -> identity state e + end + | Tint -> begin + match D.to_int eval_e with + | Some i -> simp_int i + | None -> identity state e + end + | _ -> + identity state e let rec add_lit_constraint (state : state) (e : Expr.t) : state * (Expr.t, v) simp = @@ -676,14 +696,8 @@ module SimpleReasoner | 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] Name@."; + state, to_const state e | _ -> debug "[simp_expr] Other: %a@." diff --git a/src/lib/frontend/simple_reasoner_expr.mli b/src/lib/frontend/simple_reasoner_expr.mli index 88cae9461..1b50590d2 100644 --- a/src/lib/frontend/simple_reasoner_expr.mli +++ b/src/lib/frontend/simple_reasoner_expr.mli @@ -41,8 +41,10 @@ module type Dom = sig val _true : v val _false : v val unknown : v + val const_int : Numbers.Q.t -> v val to_bool : v -> bool option + val to_int : v -> Numbers.Q.t option (** (Partial) Compare function *) val compare : state -> state -> int option diff --git a/src/lib/reasoners/simplifiers.ml b/src/lib/reasoners/simplifiers.ml index c634f88be..776ebe517 100644 --- a/src/lib/reasoners/simplifiers.ml +++ b/src/lib/reasoners/simplifiers.ml @@ -46,7 +46,9 @@ module DummySimp = let unknown = () let _false = () let _true = () + let const_int _ = () let to_bool _ = None + let to_int _ = None let pp_v fmt _ = Format.fprintf fmt "()" let eval_expr _ _ = () let v_join _ _ = () @@ -105,6 +107,7 @@ module IntervalsDomain : let _false = Value (Bool false) let _true = Value (Bool true) + let const_int i = Value (Interval (Intervals.point i Ty.Tint Explanation.empty)) let unknown = Top let to_bool = @@ -114,6 +117,15 @@ module IntervalsDomain : | Value (Interval _) -> None | Value (Bool b) -> Some b + let to_int = function + | Value (Interval i) -> begin + match Intervals.is_point i with + | Some (i, _) -> Some i + | None -> None + end + | Top + | Bottom + | Value (Bool _) -> None let pp_v = pp_abs_val pp_interval