diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7b11f90ff4..18840b25fb 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -308,10 +308,177 @@ module F_Htbl : Hashtbl.S with type key = t = let equal = equal end) +let neg t = + match t with + | { ty = Ty.Tbool; neg = Some n; _ } -> n + | { f = _; _ } -> assert false + +let is_int t = t.ty == Ty.Tint +let is_real t = t.ty == Ty.Treal + +let merge_vars acc b = + SMap.merge (fun sy a b -> + match a, b with + | None, None -> assert false + | Some _, None -> a + | None, Some _ -> b + | Some (ty, x), Some (ty', y) -> + assert (Ty.equal ty ty' || Sy.equal sy Sy.underscore); + Some (ty, x + y) + ) acc b + +let free_vars t acc = merge_vars acc t.vars + +let free_type_vars t = t.vty + +let is_ground t = + SMap.is_empty (free_vars t SMap.empty) && + Ty.Svty.is_empty (free_type_vars t) + +let size t = t.nb_nodes + +let depth t = t.depth + +(** smart constructors for terms *) + +let free_vars_non_form s l ty = + match s, l with + | Sy.Var _, [] -> SMap.singleton s (ty, 1) + | Sy.Var _, _ -> assert false + | Sy.Form _, _ -> assert false (* not correct for quantified and Lets *) + | _, [] -> SMap.empty + | _, e::r -> List.fold_left (fun s t -> merge_vars s t.vars) e.vars r + +let free_type_vars_non_form l ty = + List.fold_left (fun acc t -> Ty.Svty.union acc t.vty) (Ty.vty_of ty) l + +let is_ite s = match s with + | Sy.Op Sy.Tite -> true + | _ -> false + +let mk_term s l ty = + assert (match s with Sy.Lit _ | Sy.Form _ -> false | _ -> true); + let d = match l with + | [] -> + 1 (*no args ? depth = 1 (ie. current app s, ie constant)*) + | _ -> + (* if args, d is 1 + max_depth of args (equals at least to 1 *) + 1 + List.fold_left (fun z t -> max z t.depth) 1 l + in + let nb_nodes = List.fold_left (fun z t -> z + t.nb_nodes) 1 l in + let vars = free_vars_non_form s l ty in + let vty = free_type_vars_non_form l ty in + let pure = List.for_all (fun e -> e.pure) l && not (is_ite s) in + let pos = + HC.make {f=s; xs=l; ty=ty; depth=d; tag= -42; vars; vty; + nb_nodes; neg = None; bind = B_none; pure} + in + if ty != Ty.Tbool then pos + else if pos.neg != None then pos + else + let neg_s = Sy.Lit Sy.L_neg_pred in + let neg = + HC.make {f=neg_s; xs=[pos]; ty=ty; depth=d; tag= -42; + vars; vty; nb_nodes; neg = None; bind = B_none; pure = false} + in + assert (neg.neg == None); + pos.neg <- Some neg; + neg.neg <- Some pos; + pos + +let vrai = + let res = + let nb_nodes = 0 in + let vars = SMap.empty in + let vty = Ty.Svty.empty in + let faux = + HC.make + {f = Sy.False; xs = []; ty = Ty.Tbool; depth = -2; (*smallest depth*) + tag = -42; vars; vty; nb_nodes; neg = None; bind = B_none; + pure = true} + in + let vrai = + HC.make + {f = Sy.True; xs = []; ty = Ty.Tbool; depth = -1; (*2nd smallest d*) + tag= -42; vars; vty; nb_nodes; neg = None; bind = B_none; + pure = true} + in + assert (vrai.neg == None); + assert (faux.neg == None); + vrai.neg <- Some faux; + faux.neg <- Some vrai; + vrai + in + res + +let faux = neg (vrai) +let void = mk_term (Sy.Void) [] Ty.Tunit + +let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty + +let is_internal_name t = + match t with + | { f; xs = []; _ } -> Sy.is_fresh_internal_name f + | _ -> false + +let is_internal_skolem t = Sy.is_fresh_skolem t.f + +let positive_int i = mk_term (Sy.int i) [] Ty.Tint + +let int i = + let len = String.length i in + assert (len >= 1); + match i.[0] with + | '-' -> + assert (len >= 2); + let pi = String.sub i 1 (len - 1) in + mk_term (Sy.Op Sy.Minus) [ positive_int "0"; positive_int pi ] Ty.Tint + | _ -> positive_int i + +let positive_real i = mk_term (Sy.real i) [] Ty.Treal + +let real r = + let len = String.length r in + assert (len >= 1); + match r.[0] with + | '-' -> + assert (len >= 2); + let pi = String.sub r 1 (len - 1) in + mk_term (Sy.Op Sy.Minus) [ positive_real "0"; positive_real pi ] Ty.Treal + | _ -> positive_real r + +let bitv bt ty = mk_term (Sy.bitv bt) [] ty + +let pred t = mk_term (Sy.Op Sy.Minus) [t;int "1"] Ty.Tint (** pretty printing *) module SmtPrinter = struct + (** Helper functions used by the postprocessing phase in the printers. *) + let zero ty = + match ty with + | Ty.Tint -> Sy.Int Z.zero + | Ty.Treal -> Sy.Real Q.zero + | _ -> assert false + + let is_zero sy = + match sy with + | Sy.Int i when Z.(equal i zero) -> true + | Sy.Real q when Q.(equal q zero) -> true + | _ -> false + + let is_one sy = + match sy with + | Sy.Int i when Z.(equal i one) -> true + | Sy.Real q when Q.(equal q one) -> true + | _ -> false + + let is_mone sy = + match sy with + | Sy.Int i when Z.(equal i (neg one)) -> true + | Sy.Real q when Q.(equal q (neg one)) -> true + | _ -> false + let pp_binder ppf (var, (ty, _)) = let var = match var with @@ -419,6 +586,33 @@ module SmtPrinter = struct | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op + | Sy.Op Plus, [e1; e2] when is_zero e1.f -> pp ppf e2 + + | Sy.Op Plus, [e1; e2] when is_zero e2.f -> pp ppf e1 + + | Sy.Op Minus, [e1; e2] when is_zero e1.f -> + Fmt.pf ppf "@[(-@ %a@])" pp e2 + + | Sy.Op Minus, [e1; e2] when is_zero e2.f -> pp ppf e1 + + | Sy.Op Mult, [e1; e2] when is_one e1.f -> pp ppf e2 + + | Sy.Op Mult, [e1; e2] when is_one e2.f -> pp ppf e1 + + | Sy.Op Mult, [e1; e2] when is_mone e2.f -> + let ty = e1.ty in + pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e2] ty) + + | Sy.Op Mult, [e1; e2] when is_mone e1.f -> + let ty = e2.ty in + pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e1] ty) + + | Sy.Op Div, [e1; e2] when is_one e2.f -> pp ppf e1 + + | Sy.Op Div, [e1; e2] when is_mone e2.f -> + let ty = e1.ty in + pp ppf (mk_term Sy.(Op Minus) [mk_term (zero ty) [] ty; e1] ty) + | Sy.Op op, _ :: _ -> Fmt.pf ppf "@[(%a@ %a@])" Symbols.pp_smtlib_operator op @@ -753,29 +947,6 @@ let mk_binders, reset_binders_cpt = mk_binders, reset_binders_cpt -let merge_vars acc b = - SMap.merge (fun sy a b -> - match a, b with - | None, None -> assert false - | Some _, None -> a - | None, Some _ -> b - | Some (ty, x), Some (ty', y) -> - assert (Ty.equal ty ty' || Sy.equal sy Sy.underscore); - Some (ty, x + y) - ) acc b - -let free_vars t acc = merge_vars acc t.vars - -let free_type_vars t = t.vty - -let is_ground t = - SMap.is_empty (free_vars t SMap.empty) && - Ty.Svty.is_empty (free_type_vars t) - -let size t = t.nb_nodes - -let depth t = t.depth - let rec is_positive e = let { f; bind; _ } = e in match f, bind with @@ -784,14 +955,6 @@ let rec is_positive e = | Sy.Let, B_let { in_e; is_bool = true; _ } -> is_positive in_e | _ -> true -let neg t = - match t with - | { ty = Ty.Tbool; neg = Some n; _ } -> n - | { f = _; _ } -> assert false - -let is_int t = t.ty == Ty.Tint -let is_real t = t.ty == Ty.Treal - let name_of_lemma f = match form_view f with | Lemma { name; _ } -> name @@ -802,7 +965,6 @@ let name_of_lemma_opt opt = | None -> "(Lemma=None)" | Some f -> name_of_lemma f - (** Labeling and models *) let labels = Labels.create 107 @@ -833,119 +995,6 @@ let print_tagged_classes = Format.fprintf fmt "\n{ %a }" (print_list_sep " , ") cl) l -(** smart constructors for terms *) - -let free_vars_non_form s l ty = - match s, l with - | Sy.Var _, [] -> SMap.singleton s (ty, 1) - | Sy.Var _, _ -> assert false - | Sy.Form _, _ -> assert false (* not correct for quantified and Lets *) - | _, [] -> SMap.empty - | _, e::r -> List.fold_left (fun s t -> merge_vars s t.vars) e.vars r - -let free_type_vars_non_form l ty = - List.fold_left (fun acc t -> Ty.Svty.union acc t.vty) (Ty.vty_of ty) l - -let is_ite s = match s with - | Sy.Op Sy.Tite -> true - | _ -> false - -let mk_term s l ty = - assert (match s with Sy.Lit _ | Sy.Form _ -> false | _ -> true); - let d = match l with - | [] -> - 1 (*no args ? depth = 1 (ie. current app s, ie constant)*) - | _ -> - (* if args, d is 1 + max_depth of args (equals at least to 1 *) - 1 + List.fold_left (fun z t -> max z t.depth) 1 l - in - let nb_nodes = List.fold_left (fun z t -> z + t.nb_nodes) 1 l in - let vars = free_vars_non_form s l ty in - let vty = free_type_vars_non_form l ty in - let pure = List.for_all (fun e -> e.pure) l && not (is_ite s) in - let pos = - HC.make {f=s; xs=l; ty=ty; depth=d; tag= -42; vars; vty; - nb_nodes; neg = None; bind = B_none; pure} - in - if ty != Ty.Tbool then pos - else if pos.neg != None then pos - else - let neg_s = Sy.Lit Sy.L_neg_pred in - let neg = - HC.make {f=neg_s; xs=[pos]; ty=ty; depth=d; tag= -42; - vars; vty; nb_nodes; neg = None; bind = B_none; pure = false} - in - assert (neg.neg == None); - pos.neg <- Some neg; - neg.neg <- Some pos; - pos - -let vrai = - let res = - let nb_nodes = 0 in - let vars = SMap.empty in - let vty = Ty.Svty.empty in - let faux = - HC.make - {f = Sy.False; xs = []; ty = Ty.Tbool; depth = -2; (*smallest depth*) - tag = -42; vars; vty; nb_nodes; neg = None; bind = B_none; - pure = true} - in - let vrai = - HC.make - {f = Sy.True; xs = []; ty = Ty.Tbool; depth = -1; (*2nd smallest d*) - tag= -42; vars; vty; nb_nodes; neg = None; bind = B_none; - pure = true} - in - assert (vrai.neg == None); - assert (faux.neg == None); - vrai.neg <- Some faux; - faux.neg <- Some vrai; - vrai - in - res - -let faux = neg (vrai) -let void = mk_term (Sy.Void) [] Ty.Tunit - -let fresh_name ty = mk_term (Sy.fresh_internal_name ()) [] ty - -let is_internal_name t = - match t with - | { f; xs = []; _ } -> Sy.is_fresh_internal_name f - | _ -> false - -let is_internal_skolem t = Sy.is_fresh_skolem t.f - -let positive_int i = mk_term (Sy.int i) [] Ty.Tint - -let int i = - let len = String.length i in - assert (len >= 1); - match i.[0] with - | '-' -> - assert (len >= 2); - let pi = String.sub i 1 (len - 1) in - mk_term (Sy.Op Sy.Minus) [ positive_int "0"; positive_int pi ] Ty.Tint - | _ -> positive_int i - -let positive_real i = mk_term (Sy.real i) [] Ty.Treal - -let real r = - let len = String.length r in - assert (len >= 1); - match r.[0] with - | '-' -> - assert (len >= 2); - let pi = String.sub r 1 (len - 1) in - mk_term (Sy.Op Sy.Minus) [ positive_real "0"; positive_real pi ] Ty.Treal - | _ -> positive_real r - -let bitv bt ty = mk_term (Sy.bitv bt) [] ty - -let pred t = mk_term (Sy.Op Sy.Minus) [t;int "1"] Ty.Tint - - (** simple smart constructors for formulas *) let mk_or f1 f2 is_impl =