eliminate_literal.ml 8.87 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Clément Fumex's avatar
Clément Fumex committed
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

open Ident
open Ty
open Term
open Decl
open Theory

let meta_keep_lit = register_meta "literal:keep" [MTtysymbol]
  ~desc:"Preserve@ literals@ of@ a@ given@ type."

let add_literal (known_lit, decl as acc) t c ls_proj fin =
  try acc, Mterm.find t known_lit with Not_found ->
    (* TODO: pretty-print the constant to have a readable name *)
    let litname =
      match fin with None -> "rliteral" | _ -> "fliteral" in
    let ls = create_lsymbol (id_fresh litname) [] t.t_ty in
    let ls_decl = create_param_decl ls in
    let pr = create_prsymbol (id_fresh (litname^"_axiom")) in
    let ls_t = t_app ls [] t.t_ty in
    let f = t_app ls_proj [ls_t] ls_proj.ls_value in
    let f = t_equ f (t_const c (Opt.get f.t_ty)) in
    let f = match fin with
      | None -> f
      | Some isF -> t_and (t_app isF [ls_t] None) f in
    let ax_decl = create_prop_decl Paxiom pr f in
    let decl = ax_decl::ls_decl::decl in
    (Mterm.add t ls_t known_lit, decl), ls_t

(* TODO: remove int and real literals if not supported.
   NOTE: in this case, [add_literal] above is incorrect. *)
let rec abstract_terms kn range_metas float_metas type_kept acc t =
  match t.t_node, t.t_ty with
  | Tconst (Number.ConstInt _ as c), Some {ty_node = Tyapp (ts,[])}
    when not (ts_equal ts ts_int || Sts.mem ts type_kept) ->
      let to_int = Mts.find ts range_metas in
      add_literal acc t c to_int None
  | Tconst (Number.ConstReal _ as c), Some {ty_node = Tyapp (ts,[])}
    when not (ts_equal ts ts_real || Sts.mem ts type_kept) ->
      let to_real,isF = Mts.find ts float_metas in
      add_literal acc t c to_real (Some isF)
  | _ ->
      t_map_fold (abstract_terms kn range_metas float_metas type_kept) acc t

54
let elim le_int le_real neg_real type_kept kn
Clément Fumex's avatar
Clément Fumex committed
55 56 57 58 59 60
    range_metas float_metas d (known_lit,task) =
  match d.d_node with
  | Dtype ts when Mts.exists (fun ts' _ -> ts_equal ts ts') range_metas
               && not (Sts.mem ts type_kept) ->
      let to_int = Mts.find ts range_metas in
      let ir = match ts.ts_def with Range ir -> ir | _ -> assert false in
61 62
      let lo = ir.Number.ir_lower in
      let hi = ir.Number.ir_upper in
Clément Fumex's avatar
Clément Fumex committed
63 64 65 66 67
      let ty_decl = create_ty_decl ts in
      let ls_decl = create_param_decl to_int in
      let pr = create_prsymbol (id_fresh (ts.ts_name.id_string ^ "'axiom")) in
      let v = create_vsymbol (id_fresh "i") (ty_app ts []) in
      let v_term = t_app to_int [t_var v] (Some ty_int) in
68 69
      let a_term = t_bigint_const lo in
      let b_term = t_bigint_const hi in
Clément Fumex's avatar
Clément Fumex committed
70 71 72 73 74
      let f = t_and (t_app le_int [a_term; v_term] None)
          (t_app le_int [v_term; b_term] None)
      in
      let f = t_forall_close [v] [] f in
      let ax_decl = create_prop_decl Paxiom pr f in
75 76
      let add_decl t d = try Task.add_decl t d
                         with UnknownIdent _ -> t in (*FIXME*)
77
      (known_lit, List.fold_left add_decl task [ty_decl; ls_decl; ax_decl])
Clément Fumex's avatar
Clément Fumex committed
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
  | Dtype ts when Mts.exists (fun ts' _ -> ts_equal ts ts') float_metas
               && not (Sts.mem ts type_kept) ->
      let to_real,is_finite = Mts.find ts float_metas in
      let fp = match ts.ts_def with Float fp -> fp | _ -> assert false in
      let eb = BigInt.of_int fp.Number.fp_exponent_digits in
      let sb = BigInt.of_int fp.Number.fp_significand_digits in
      (* declare abstract type [t] *)
      let ty_decl = create_ty_decl ts in
      (* declare projection to_real *)
      let proj_decl = create_param_decl to_real in
      (* declare predicate is_finite *)
      let isFinite_decl = create_param_decl is_finite in
      (* create defining axiom *)
      (* [forall v:t. is_finite v -> | to_real v | <= max] *)
      let pr = create_prsymbol (id_fresh (ts.ts_name.id_string ^ "'axiom")) in
      let v = create_vsymbol (id_fresh "x") (ty_app ts []) in
      let v_term = t_app to_real [t_var v] (Some ty_real) in
      (* compute max *)
      let emax = BigInt.pow_int_pos_bigint 2 (BigInt.pred eb) in
      let m = BigInt.pred (BigInt.pow_int_pos_bigint 2 sb) in
      let e = BigInt.sub emax sb in
99 100
      let m_string = Format.asprintf "%a" (Number.print_in_base 16 None) m in
      let e_string = Format.asprintf "%a" (Number.print_in_base 10 None) e in
101
      let e_val = Number.real_const_hex m_string "" (Some e_string) in
102
      let max_term = t_const
103 104 105
          Number.(ConstReal { rc_negative = false ; rc_abs = e_val })
          ty_real
      in
Clément Fumex's avatar
Clément Fumex committed
106
      (* compose axiom *)
107 108 109
      let f = t_and (t_app le_real [t_app neg_real [max_term] (Some ty_real); v_term] None)
          (t_app le_real [v_term; max_term] None) in
        (* t_app le_real [t_app abs_real [v_term] (Some ty_real); term] None in *)
Clément Fumex's avatar
Clément Fumex committed
110 111 112 113 114 115 116 117 118 119 120 121 122
      let f = t_implies (t_app is_finite [t_var v] None) f in
      let f = t_forall_close [v] [] f in
      let ax_decl = create_prop_decl Paxiom pr f in
      (known_lit, List.fold_left Task.add_decl task
         [ty_decl; proj_decl; isFinite_decl; ax_decl])
  | _ ->
      let (known_lit, local_decl), d =
        decl_map_fold
          (abstract_terms kn range_metas float_metas type_kept)
          (known_lit,[]) d in
      let t = List.fold_left Task.add_decl task (List.rev local_decl) in
      (known_lit, Task.add_decl t d)

123
let eliminate le_int le_real neg_real type_kept
Clément Fumex's avatar
Clément Fumex committed
124 125 126
    range_metas float_metas t (known_lit, acc) =
  match t.Task.task_decl.td_node with
  | Decl d ->
127
      elim le_int le_real neg_real type_kept
Clément Fumex's avatar
Clément Fumex committed
128 129 130 131 132 133 134 135 136 137 138 139 140 141
        t.Task.task_known range_metas float_metas d (known_lit, acc)
  | Meta (m, [MAts ts]) when meta_equal m meta_keep_lit ->
      let td = create_meta Libencoding.meta_kept [MAty (ty_app ts [])] in
      let acc = Task.add_tdecl acc t.Task.task_decl in
      known_lit, Task.add_tdecl acc td
  | Use _ | Clone _ | Meta _ ->
      known_lit, Task.add_tdecl acc t.Task.task_decl

let eliminate_literal env =
  (* FIXME: int.Int.le_sym should be imported in the task *)
  let th = Env.read_theory env ["int"] "Int" in
  let le_int = ns_find_ls th.th_export ["infix <="] in
  let th = Env.read_theory env ["real"] "Real" in
  let le_real = ns_find_ls th.th_export ["infix <="] in
142
  let neg_real = ns_find_ls th.th_export ["prefix -"] in
Clément Fumex's avatar
Clément Fumex committed
143 144 145 146 147 148 149 150 151 152 153 154 155 156
  Trans.on_meta meta_range (fun range_metas ->
      Trans.on_meta meta_float (fun float_metas ->
          let range_metas = List.fold_left (fun acc meta_arg ->
              match meta_arg with
              | [MAts ts; MAls to_int] -> Mts.add ts to_int acc
              | _ -> assert false) Mts.empty range_metas in
          let float_metas = List.fold_left (fun acc meta_arg ->
              match meta_arg with
              | [MAts ts; MAls to_real; MAls is_finite] ->
                  Mts.add ts (to_real,is_finite) acc
              | _ -> assert false) Mts.empty float_metas in
          Trans.on_tagged_ts meta_keep_lit
            (fun type_kept ->
               Trans.fold_map
157
                 (eliminate le_int le_real neg_real type_kept
Clément Fumex's avatar
Clément Fumex committed
158 159 160 161 162 163
                    range_metas float_metas)
                 Mterm.empty None)))

let () =
  Trans.register_env_transform "eliminate_literal" eliminate_literal
    ~desc:"Eliminate@ unsupported@ literals."
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199



(* simple transformation that just replace negative constants by application
   of 'prefix -' to positive constant *)

open Number

let rec replace_negative_constants neg_int neg_real t =
  match t.t_ty, t.t_node with
  | (Some ty), (Tconst (ConstInt c)) ->
     if c.ic_negative && ty_equal ty ty_int then
       t_app neg_int
             [t_const (ConstInt { c with ic_negative = false }) ty_int]
             (Some ty_int)
     else t
  | (Some ty), (Tconst (ConstReal c)) ->
     if c.rc_negative && ty_equal ty ty_real then
       t_app neg_real
             [t_const (ConstReal { c with rc_negative = false }) ty_real]
             (Some ty_real)
     else t
  | _ -> t_map (replace_negative_constants neg_int neg_real) t

let eliminate_negative_constants env =
  (* FIXME: int.Int should be imported in the task *)
  let th = Env.read_theory env ["int"] "Int" in
  let neg_int = ns_find_ls th.th_export ["prefix -"] in
  let th = Env.read_theory env ["real"] "Real" in
  let neg_real = ns_find_ls th.th_export ["prefix -"] in
  Trans.rewrite (replace_negative_constants neg_int neg_real) None

let () =
  Trans.register_env_transform "eliminate_negative_constants"
                               eliminate_negative_constants
                               ~desc:"Eliminate@ negative@ constants"