smt2_model_defs.ml 7.17 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

12
13
14
15
open Stdlib

type variable = string

16
17
18
19
20
21
22
23
type float_type =
  | Plus_infinity
  | Minus_infinity
  | Plus_zero
  | Minus_zero
  | Not_a_number
  | Float_value of string * string * string

24
25
26
27
28
29
30
type array =
  | Const of term
  | Store of array * term * term

and term =
  | Integer of string
  | Decimal of (string * string)
31
  | Float of float_type
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
  | Other of string
  | Array of array
  | Bitvector of string
  | Boolean of bool
  | Cvc4_Variable of variable
  | Function_Local_Variable of variable
  | Variable of variable
  | Ite of term * term * term * term
  | Record of int * (term list)
  | Discr of int * (term list)
  | To_array of term

type definition =
  | Function of variable list * term
  | Term of term
  | Noelement

(* Type returned by parsing of model.
Sylvain Dailler's avatar
Sylvain Dailler committed
50
   An hashtable that makes a correspondence between names (string) and
51
   associated definition (complex stuff) *)
Sylvain Dailler's avatar
Sylvain Dailler committed
52
type correspondence_table = (bool * definition) Mstr.t
53

54
55
56
57
58
59
60
61
62
let print_float fmt f =
  match f with
  | Plus_infinity -> Format.fprintf fmt "Plus_infinity"
  | Minus_infinity -> Format.fprintf fmt "Minus_infinity"
  | Plus_zero -> Format.fprintf fmt "Plus_zero"
  | Minus_zero -> Format.fprintf fmt "Minus_zero"
  | Not_a_number -> Format.fprintf fmt "NaN"
  | Float_value (b, eb, sb) -> Format.fprintf fmt "(%s, %s, %s)" b eb sb

63
64
65
66
67
68
69
70
71
72
73
74
let rec print_array fmt a =
  match a with
  | Const t -> Format.fprintf fmt "CONST : %a" print_term t
  | Store (a, t1, t2) ->
      Format.fprintf fmt "STORE : %a %a %a"
        print_array a print_term t1 print_term t2

(* Printing function for terms *)
and print_term fmt t =
  match t with
  | Integer s -> Format.fprintf fmt "Integer: %s" s
  | Decimal (s1, s2) -> Format.fprintf fmt "Decimal: %s . %s" s1 s2
75
  | Float f -> Format.fprintf fmt "Float: %a" print_float f
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
  | Other s -> Format.fprintf fmt "Other: %s" s
  | Array a -> Format.fprintf fmt "Array: %a" print_array a
  | Bitvector bv -> Format.fprintf fmt "Bv: %s" bv
  | Boolean _b -> Format.fprintf fmt "Boolean"
  | Cvc4_Variable cvc -> Format.fprintf fmt "CVC4VAR: %s" cvc
  | Function_Local_Variable v -> Format.fprintf fmt "LOCAL: %s" v
  | Variable v -> Format.fprintf fmt "VAR: %s" v
  | Ite _ -> Format.fprintf fmt "ITE"
  | Record (n, l) -> Format.fprintf fmt "record_type: %d; list_fields: %a" n
        (fun fmt -> Pp.print_list (fun fmt () -> Format.fprintf fmt " ") print_term fmt) l
  | Discr (n, l) -> Format.fprintf fmt "record_type: %d; list_fields: %a" n
        (fun fmt -> Pp.print_list (fun fmt () -> Format.fprintf fmt " ") print_term fmt) l
  | To_array t -> Format.fprintf fmt "TO_array: %a@." print_term t

let print_def fmt d =
  match d with
  | Function (_vars, t) -> Format.fprintf fmt "FUNCTION : %a" print_term t
  | Term t -> Format.fprintf fmt "TERM : %a" print_term t
  | Noelement -> Format.fprintf fmt "NOELEMENT"

Sylvain Dailler's avatar
Sylvain Dailler committed
96
let add_element x (t: correspondence_table) b =
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
  match x with
  | None -> t
  | Some (key, value) ->
      Mstr.add key (b, value) t

exception Bad_local_variable

let rec make_local_array vars_lists a =
  match a with
  | Const t ->
    let t' = make_local vars_lists t in
    Const t'
  | Store (a, t1, t2) ->
    let a' = make_local_array vars_lists a in
    let t1' = make_local vars_lists t1 in
    let t2' = make_local vars_lists t2 in
    Store (a', t1', t2')

(* For a definition of function f, local variables being in vars_lists and the
   returned term being t, this function changes the term give an appropriate tag
   to variables that are actually local. *)
and make_local vars_lists t =
  match t with
  | Variable s ->
      begin
        if (List.exists (fun x -> s = x) vars_lists) then
          Function_Local_Variable s
        else
          try
          (* Check that s is a Cvc4 or z3 variable. Note that s is a variable
             name so it is of size > 0 *)
            (if (String.get s 0 = '@' || String.contains s '!') then
              Cvc4_Variable s
            else
              Variable s
            ) (* should not happen *)
          with
            _ -> raise Bad_local_variable (* Should not happen. s = "" *)
      end
  | Array a ->
    begin
      Array (make_local_array vars_lists a)
    end
  | Ite (t1, t2, t3, t4) ->
    let t1 = make_local vars_lists t1 in
    let t2 = make_local vars_lists t2 in
    let t3 = make_local vars_lists t3 in
    let t4 = make_local vars_lists t4 in
    Ite (t1, t2, t3, t4)
146
  | Integer _ | Decimal _ | Float _ | Other _ -> t
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
  | Bitvector _ -> t
  | Cvc4_Variable _ -> raise Bad_local_variable
  | Boolean _ -> t
  | Function_Local_Variable _ -> raise Bad_local_variable
  | Record (n, l) -> Record (n, List.map (fun x -> make_local vars_lists x) l)
  | Discr (n, l) -> Discr (n, List.map (fun x -> make_local vars_lists x) l)
  | To_array t -> To_array (make_local vars_lists t)


let build_record_discr lgen =

  let rec build_records_with_discrs acc (l: term list) =
    match l,acc with
    | Record (n, t) :: tl, None ->
        build_records_with_discrs (Some (Record (n, t))) tl
    | Record (_n, _t) :: _tl, Some (Record (_n', _t')) ->
        assert (false)
    | Record (n, t) :: _tl, Some (Discr (n', t')) ->
        Record (n, (Discr (n', t')) :: t)
    | Discr (n, t) :: tl, None ->
        build_records_with_discrs (Some (Discr (n, t))) tl
    | Discr (n, t) :: _tl, Some (Record (n', t')) ->
        Record (n', (Discr (n, t) :: t'))
    | Discr (_n, _t) :: _tl, Some (Discr (_n', _t')) ->
        assert (false)
    | _a :: tl, _ -> build_records_with_discrs acc tl
    | [], Some b -> b
    | [], None -> List.hd lgen
  in

  build_records_with_discrs None lgen

let rec subst var value t =
  match t with
181
  | Integer _ | Decimal _ | Float _ | Other _ | Bitvector _ | Boolean _ ->
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
      t
  | Array a -> Array (subst_array var value a)
  | Cvc4_Variable _ -> raise Bad_local_variable
  | Function_Local_Variable _ -> t
  | Variable v -> if v = var then value else Variable v
  | Ite (t1, t2, t3, t4) ->
    let t1 = subst var value t1 in
    let t2 = subst var value t2 in
    let t3 = subst var value t3 in
    let t4 = subst var value t4 in
    Ite (t1, t2, t3, t4)
 | Record (n, l) ->
     Record (n, List.map (fun t -> subst var value t) l)
 | Discr (n, l) ->
     Discr (n, List.map (fun t -> subst var value t) l)
 | To_array t -> To_array (subst var value t)


and subst_array var value a =
  match a with
  | Const t -> Const (subst var value t)
  | Store (a, t1, t2) ->
      let t1 = subst var value t1 in
      let t2 = subst var value t2 in
      let a = subst_array var value a in
      Store (a, t1, t2)

let substitute l t =
  List.fold_left (fun t (var, value) -> subst var value t) t l