collect_data_model.ml 24 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  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
open Wstdlib
13 14 15 16
open Smt2_model_defs

exception Not_value

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 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 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
let debug_cntex = Debug.register_flag "cntex_collection"
    ~desc:"Intermediate representation debugging for counterexamples"

(** Intermediate data structure for propagations of tree projections inside
    counterexamples.
*)

(* Similar to definition except that we have a tree like structure for
    variables *)
type initial_definition = definition

type projection_name = string

module Mpr: Extmap.S with type key = projection_name = Mstr

type tree_variable =
  | Tree of tree
  | Var of string

and tarray =
  | TArray_var of variable
  | TConst of tterm
  | TStore of tarray * tterm * tterm

and tterm =
  | TSval of simple_value
  | TApply of (string * tterm list)
  | TArray of tarray
  | TCvc4_Variable of tree_variable
  | TFunction_Local_Variable of variable
  | TVariable of variable
  | TIte of tterm * tterm * tterm * tterm
  | TRecord of string * ((string * tterm) list)
  | TTo_array of tterm

and tree_definition =
  | TFunction of (variable * string option) list * tterm
  | TTerm of tterm
  | TNoelement

and tree =
  | Node of tree Mpr.t
  | Leaf of tree_definition

(* correpondence_table = map from var_name to tree representing its definition:
   Initially all var name begins with its original definition which is then
   refined using projections (that are saved in the tree) *)
type correspondence_table = tree Mstr.t


(** Printing functions *)
let print_float fmt f =
  match f with
  | Model_parser.Plus_infinity -> Format.fprintf fmt "Plus_infinity"
  | Model_parser.Minus_infinity -> Format.fprintf fmt "Minus_infinity"
  | Model_parser.Plus_zero -> Format.fprintf fmt "Plus_zero"
  | Model_parser.Minus_zero -> Format.fprintf fmt "Minus_zero"
  | Model_parser.Not_a_number -> Format.fprintf fmt "NaN"
  | Model_parser.Float_value (b, eb, sb) -> Format.fprintf fmt "(%s, %s, %s)" b eb sb
  | Model_parser.Float_hexa(s,f) -> Format.fprintf fmt "%s (%g)" s f

let print_value fmt v =
  match v with
  | Integer s -> Format.fprintf fmt "Integer: %s" s
  | Decimal (s1, s2) -> Format.fprintf fmt "Decimal: %s . %s" s1 s2
  | Fraction (s1, s2) -> Format.fprintf fmt "Fraction: %s / %s" s1 s2
  | Float f -> Format.fprintf fmt "Float: %a" print_float f
  | Other s -> Format.fprintf fmt "Other: %s" s
  | Bitvector bv -> Format.fprintf fmt "Bv: %s" bv
  | Boolean b -> Format.fprintf fmt "Boolean: %b " b

let rec print_array fmt a =
  match a with
  | TArray_var v -> Format.fprintf fmt "ARRAY_VAR : %s" v
  | TConst t -> Format.fprintf fmt "CONST : %a" print_term t
  | TStore (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
  | TSval v -> print_value fmt v
  | TApply (s, lt) ->
      Format.fprintf fmt "Apply: (%s, %a)" s
        (Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.comma print_term)
        lt
  | TArray a -> Format.fprintf fmt "Array: %a" print_array a
  | TCvc4_Variable (Var cvc) -> Format.fprintf fmt "CVC4VAR: %s" cvc
  | TCvc4_Variable _ -> Format.fprintf fmt "CVC4VAR: TREE"
  | TFunction_Local_Variable v -> Format.fprintf fmt "LOCAL: %s" v
  | TVariable v -> Format.fprintf fmt "VAR: %s" v
  | TIte _ -> Format.fprintf fmt "ITE"
  | TRecord (n, l) ->
      Format.fprintf fmt "record_type: %s; list_fields: %a" n
        (Pp.print_list Pp.semi
           (fun fmt (x, a) -> Format.fprintf fmt "(%s, %a)" x print_term a))
        l
  | TTo_array t -> Format.fprintf fmt "TO_array: %a@." print_term t

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

let rec print_tree fmt t =
124
  match t with
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147
  | Node mpt -> Format.fprintf fmt "NODE : [%a]" print_mpt mpt
  | Leaf td -> Format.fprintf fmt "LEAF: %a" print_def td

and print_mpt fmt t =
  Mpr.iter (fun key e -> Format.fprintf fmt "P: %s; T: %a" key print_tree e) t


(* Printing function for debugging *)
let print_table (t: correspondence_table) =
  Debug.dprintf debug_cntex "Correspondence table key and value@.";
  Mstr.iter (fun key t ->
      Debug.dprintf debug_cntex "%s %a@." key print_tree t)
    t;
  Debug.dprintf debug_cntex "End table@."

(* Adds all referenced cvc4 variables found in the term t to table.
   In particular, this function helps us to collect all the target prover's
   generated constants so that they become part of constant-to-value
   correspondence.  *)
let rec get_variables_term (table: initial_definition Mstr.t) t =
  match t with
  | Sval _ -> table
  | Variable _ | Function_Local_Variable _ -> table
148 149 150 151 152 153 154 155 156 157 158 159
  | Array a ->
    get_variables_array table a
  | Ite (t1, t2, t3, t4) ->
    let table = get_variables_term table t1 in
    let table = get_variables_term table t2 in
    let table = get_variables_term table t3 in
    let table = get_variables_term table t4 in
    table
  | Cvc4_Variable cvc ->
    if Mstr.mem cvc table then
      table
    else
160
      Mstr.add cvc Noelement table
161
  | Record (_, l) ->
162
    List.fold_left (fun table (_f, t) -> get_variables_term table t) table l
163 164
  | To_array t ->
    get_variables_term table t
165 166
  | Apply (_s, lt) ->
      List.fold_left (fun table t -> get_variables_term table t) table lt
167 168
  (* TODO does not exist at this moment *)
  | Trees _ -> raise Not_found
169 170 171

and get_variables_array table a =
   match a with
172 173
   | Array_var _v ->
     table
174 175 176 177 178 179 180 181
   | Const t ->
    let table = get_variables_term table t in
    table
   | Store (a, t1, t2) ->
     let table = get_variables_array table a in
     let table = get_variables_term table t1 in
     get_variables_term table t2

182
let get_all_var (table: definition Mstr.t) : definition Mstr.t =
183 184
  Mstr.fold (fun _key element table ->
    match element with
185 186 187
    | Noelement -> table
    | Function (_, t) -> get_variables_term table t
    | Term t -> get_variables_term table t) table table
188 189 190 191 192 193

exception Bad_variable

(* Get the "radical" of a variable *)
let remove_end_num s =
  let n = ref (String.length s - 1) in
194 195 196 197 198 199 200 201 202 203
  if !n <= 0 then s else
  begin
    while String.get s !n <= '9' && String.get s !n >= '0' && !n >= 0 do
      n := !n - 1
    done;
    try
      String.sub s 0 (!n + 1)
    with
    | _ -> s
  end
204

205 206 207
(* Used to handle case of badly formed table *)
exception Incorrect_table

208
(* Add the variables that can be deduced from ITE to the table of variables *)
209 210
let add_vars_to_table (table: correspondence_table) key value : correspondence_table =

211
  let rec add_vars_to_table ~type_value (table: correspondence_table) value =
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229

    let add_var_ite cvc t1 table : correspondence_table =
      let t1 = Leaf (TTerm t1) in
      match Mstr.find cvc table with
      | Node tree ->
          if Mpr.mem key tree then
            raise Incorrect_table
          else
            let new_tree = Node (Mpr.add key t1 tree) in
            Mstr.add cvc new_tree table
      | Leaf TNoelement ->
          Mstr.add cvc (Node (Mpr.add key t1 Mpr.empty)) table
      | Leaf _ ->
          raise Incorrect_table
      | exception Not_found ->
          Mstr.add cvc (Node (Mpr.add key t1 Mpr.empty)) table
    in

230
    match value with
231 232 233 234 235 236 237 238 239 240 241 242 243
    | TIte (TCvc4_Variable (Var cvc), TFunction_Local_Variable _x, t1, t2) ->
        let table = add_var_ite cvc t1 table in
        add_vars_to_table ~type_value table t2
    | TIte (TFunction_Local_Variable _x, TCvc4_Variable (Var cvc), t1, t2) ->
        let table = add_var_ite cvc t1 table in
        add_vars_to_table ~type_value table t2
    | TIte (t, TFunction_Local_Variable _x, TCvc4_Variable (Var cvc), t2) ->
        let table = add_var_ite cvc t table in
        add_vars_to_table ~type_value table t2
    | TIte (TFunction_Local_Variable _x, t, TCvc4_Variable (Var cvc), t2) ->
        let table = add_var_ite cvc t table in
        add_vars_to_table ~type_value table t2
    | TIte (_, _, _, _) -> table
244 245 246 247 248
    | _ ->
      begin
        match type_value with
        | None -> table
        | Some type_value ->
249
            Mstr.fold (fun key_val l_elt acc ->
250 251 252
              let match_str_z3 = type_value ^ "!" in
              let match_str_cvc4 = "_" ^ type_value ^ "_" in
              let match_str = Str.regexp ("\\(" ^ match_str_z3 ^ "\\|" ^ match_str_cvc4 ^ "\\)") in
253
              match Str.search_forward match_str (remove_end_num key_val) 0 with
254 255
              | exception Not_found -> acc
              | _ ->
256 257
                  if l_elt = Leaf TNoelement then
                    Mstr.add key_val (Node (Mpr.add key (Leaf (TTerm value)) Mpr.empty)) acc
258
                  else
259
                    begin match l_elt with
260 261 262 263 264 265 266
                      | Node mpt ->
                          (* We always prefer explicit assignment to default
                             type assignment. *)
                          if Mpr.mem key mpt then
                            acc
                          else
                            Mstr.add key_val (Node (Mpr.add key (Leaf (TTerm value)) mpt)) acc
267 268 269
                      | _ -> acc
                    end
              )
270 271
              table table
      end
272
  in
273

274 275 276
  let type_value, t = match value with
  | TTerm t -> (None, t)
  | TFunction (cvc_var_list, t) ->
277 278 279 280 281
    begin
      match cvc_var_list with
      | [(_, type_value)] -> (type_value, t)
      | _ -> (None, t)
    end
282
  | TNoelement -> raise Bad_variable in
283

284 285 286 287
  try add_vars_to_table ~type_value table t
  with Incorrect_table ->
    Debug.dprintf debug_cntex "Badly formed table@.";
    table
288

289
let rec refine_definition ~enc (table: correspondence_table) t =
290
  match t with
291 292 293
  | TTerm t -> TTerm (refine_function ~enc table t)
  | TFunction (vars, t) -> TFunction (vars, refine_function ~enc table t)
  | TNoelement -> TNoelement
294

295
and refine_array ~enc table a =
296
  match a with
297 298 299 300 301 302 303 304 305
  | TArray_var _v -> a
  | TConst t ->
    let t = refine_function ~enc table t in
    TConst t
  | TStore (a, t1, t2) ->
    let a = refine_array ~enc table a in
    let t1 = refine_function ~enc table t1 in
    let t2 = refine_function ~enc table t2 in
    TStore (a, t1, t2)
306 307 308 309 310

(* This function takes the table of assigned variables and a term and replace
   the variables with the constant associated with them in the table. If their
   value is not a constant yet, recursively apply on these variables and update
   their value. *)
311
and refine_function ~enc (table: correspondence_table) (term: tterm) =
312
  match term with
313 314 315 316 317 318 319 320 321 322 323 324
  | TSval _ -> term
  | TCvc4_Variable (Var v) ->
      begin
        try (
          let tree = Mstr.find v table in
          (* Here, it is very *important* to have [enc] so that we don't go in
             circles: remember that we cannot make any assumptions on the result
             prover.
             There has been cases where projections were legitimately circularly
             defined
          *)
          if Hstr.mem enc v then
325
            TCvc4_Variable (Tree tree)
326
          else
327
            let () = Hstr.add enc v () in
328 329 330 331 332
            let table = refine_variable_value ~enc table v tree in
            let tree = Mstr.find v table in
            TCvc4_Variable (Tree tree)
        )
      with
333 334 335
      | Not_found -> term
      | Not_value -> term
    end
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372
  | TCvc4_Variable (Tree t) ->
      let t = refine_tree ~enc table t in
      TCvc4_Variable (Tree t)
  | TFunction_Local_Variable _ -> term
  | TVariable _ -> term
  | TIte (t1, t2, t3, t4) ->
    let t1 = refine_function ~enc table t1 in
    let t2 = refine_function ~enc table t2 in
    let t3 = refine_function ~enc table t3 in
    let t4 = refine_function ~enc table t4 in
    TIte (t1, t2, t3, t4)
  | TArray a ->
    TArray (refine_array ~enc table a)
  | TRecord (n, l) ->
    TRecord (n, List.map (fun (f, v) -> f, refine_function ~enc table v) l)
  | TTo_array t ->
    TTo_array (refine_function ~enc table t)
  | TApply (s1, lt) ->
    TApply (s1, List.map (refine_function ~enc table) lt)

and refine_tree ~enc table t =
  match t with
  | Leaf t -> Leaf (refine_definition ~enc table t)
  | Node mpr -> Node (Mpr.map (fun x -> refine_tree ~enc table x) mpr)

and refine_variable_value ~enc (table: correspondence_table) key (t: tree) : correspondence_table =
  let t = refine_tree ~enc table t in
  Mstr.add key t table

(* TODO in the future, we should keep the table that is built at each call of
   this to populate the acc where its called. Because what we do here is
   inefficient. ie we calculate the value of constants several time during
   propagation without saving it: this is currently ok as counterexamples
   parsing is *not* notably taking time/memory *)
let refine_variable_value table key t =
  let encountered_key = Hstr.create 16 in
  refine_variable_value ~enc:encountered_key table key t
373

374 375 376 377 378 379 380 381 382 383
let convert_simple_to_model_value (v: simple_value) =
  match v with
  | Integer i -> Model_parser.Integer i
  | Decimal (d1, d2) -> Model_parser.Decimal (d1, d2)
  | Fraction (s1, s2) -> Model_parser.Fraction (s1, s2)
  | Float f -> Model_parser.Float f
  | Bitvector bv -> Model_parser.Bitvector bv
  | Boolean b -> Model_parser.Boolean b
  | Other _s -> raise Not_value

DAILLER Sylvain's avatar
DAILLER Sylvain committed
384 385 386 387
(* In the following lf is the list of fields. It is used to differentiate
   projections from fields so that projections cannot be reconstructed into a
   record. *)
let rec convert_array_value lf (a: array) : Model_parser.model_array =
388 389 390 391
  let array_indices = ref [] in

  let rec create_array_value a =
    match a with
392
    | Array_var _v -> raise Not_value
393
    | Const t -> { Model_parser.arr_indices = !array_indices;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
394
                   Model_parser.arr_others = convert_to_model_value lf t}
395 396
    | Store (a, t1, t2) ->
        let new_index =
397
          { Model_parser.arr_index_key = convert_to_model_value lf t1;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
398
            Model_parser.arr_index_value = convert_to_model_value lf t2} in
399 400 401 402
        array_indices := new_index :: !array_indices;
        create_array_value a in
  create_array_value a

DAILLER Sylvain's avatar
DAILLER Sylvain committed
403
and convert_to_model_value lf (t: term): Model_parser.model_value =
404
  match t with
405
  | Sval v -> convert_simple_to_model_value v
DAILLER Sylvain's avatar
DAILLER Sylvain committed
406
  | Array a -> Model_parser.Array (convert_array_value lf a)
407
  | Record (_n, l) ->
DAILLER Sylvain's avatar
DAILLER Sylvain committed
408
      Model_parser.Record (convert_record lf l)
409 410 411
  | Trees tree ->
      begin match tree with
      | [] -> raise Not_value
412
      | [field, value] ->
DAILLER Sylvain's avatar
DAILLER Sylvain committed
413
          Model_parser.Proj (field, convert_to_model_value lf value)
414
      | l ->
DAILLER Sylvain's avatar
DAILLER Sylvain committed
415 416 417 418 419 420 421 422 423
          if List.for_all (fun x -> Mstr.mem (fst x) lf) l then
            Model_parser.Record
              (List.map (fun (field, value) ->
                   let model_value = convert_to_model_value lf value in
                   (field, model_value))
                  l)
          else
            let (proj_name, proj_value) = List.hd l in
            Model_parser.Proj (proj_name, convert_to_model_value lf proj_value)
424
      end
425
  | Cvc4_Variable _v -> raise Not_value (*Model_parser.Unparsed "!"*)
426
  (* TODO change the value returned for non populated Cvc4 variable '!' -> '?' ? *)
DAILLER Sylvain's avatar
DAILLER Sylvain committed
427 428
  | To_array t -> convert_to_model_value lf (Array (convert_z3_array t))
  | Apply (s, lt) -> Model_parser.Apply (s, List.map (convert_to_model_value lf) lt)
429
  | Function_Local_Variable _ | Variable _ | Ite _ -> raise Not_value
430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451

and convert_z3_array (t: term) : array =

  let rec convert_array t =
    match t with
    (* This works for multidim array because, we call convert_to_model_value on
       the new array generated (which will still contain a To_array).
       Example of value for multidim array:
       To_array (Ite (x, 1, (To_array t), To_array t')) -> call on complete term ->
       Store (1, To_array t, To_array t') -> call on subpart (To_array t) ->
       Store (1, Const t, To_array t') -> call on subpart (To_array t') ->
       Store (1, Const t, Const t')
     *)

    | Ite (Function_Local_Variable _x, if_t, t1, t2) ->
      Store (convert_array t2, if_t, t1)
    | Ite (if_t, Function_Local_Variable _x, t1, t2) ->
      Store (convert_array t2, if_t, t1)
    | t -> Const t
  in
  convert_array t

DAILLER Sylvain's avatar
DAILLER Sylvain committed
452 453
and convert_record lf l =
  List.map (fun (f, v) -> f, convert_to_model_value lf v) l
454

DAILLER Sylvain's avatar
DAILLER Sylvain committed
455 456
let convert_to_model_element ~set_str list_field name (t: term) =
  let value = convert_to_model_value list_field t in
457 458 459 460 461 462
  let attrs =
    match Mstr.find name set_str with
    | exception Not_found -> Ident.Sattr.empty
    | attrs -> attrs
  in
  Model_parser.create_model_element ~name ~value ~attrs ()
463

464 465
let default_apply_to_record (list_records: (string list) Mstr.t)
    (noarg_constructors: string list) (t: term) =
466 467 468

  let rec array_apply_to_record (a: array) =
    match a with
469
    | Array_var _v -> raise Not_value
470 471 472 473 474 475 476 477 478 479 480
    | Const x ->
        let x = apply_to_record x in
        Const x
    | Store (a, t1, t2) ->
        let a = array_apply_to_record a in
        let t1 = apply_to_record t1 in
        let t2 = apply_to_record t2 in
        Store (a, t1, t2)

  and apply_to_record (v: term) =
    match v with
481
    | Sval _ -> v
482 483 484 485
    (* Variable with no arguments can actually be constructors. We check this
       here and if it is the case we change the variable into a value. *)
    | Variable s when List.mem s noarg_constructors ->
        Apply (s, [])
486
    | Cvc4_Variable _ | Function_Local_Variable _ | Variable _ -> v
487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506
    | Array a ->
        Array (array_apply_to_record a)
    | Record (s, l) ->
        let l = List.map (fun (f,v) -> f, apply_to_record v) l in
        Record (s, l)
    | Apply (s, l) ->
        let l = List.map apply_to_record l in
        if Mstr.mem s list_records then
          Record (s, List.combine (Mstr.find s list_records) l)
        else
          Apply (s, l)
    | Ite (t1, t2, t3, t4) ->
        let t1 = apply_to_record t1 in
        let t2 = apply_to_record t2 in
        let t3 = apply_to_record t3 in
        let t4 = apply_to_record t4 in
        Ite (t1, t2, t3, t4)
    | To_array t1 ->
        let t1 = apply_to_record t1 in
        To_array t1
507 508
    (* TODO Does not exist yet *)
    | Trees _ -> raise Not_value
509 510 511
  in
  apply_to_record t

512 513 514 515 516
let apply_to_records_ref = ref None

let register_apply_to_records f =
  apply_to_records_ref := Some f

517
let apply_to_record list_records noarg_constructors t =
518
  match !apply_to_records_ref with
519 520
  | None -> default_apply_to_record list_records noarg_constructors t
  | Some f -> f list_records noarg_constructors t
521

522
let definition_apply_to_record list_records noarg_constructors d =
523 524
    match d with
    | Function (lt, t) ->
525 526
        Function (lt, apply_to_record list_records noarg_constructors t)
    | Term t -> Term (apply_to_record list_records noarg_constructors  t)
527 528
    | Noelement -> Noelement

529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597
let rec convert_to_tree_def (d: definition) : tree_definition =
  match d with
  | Function (l, t) ->
      TFunction (l, convert_to_tree_term t)
  | Term t -> TTerm (convert_to_tree_term t)
  | Noelement -> TNoelement

and convert_to_tree_term (t: term) : tterm =
  match t with
  | Sval v -> TSval v
  | Apply (s, tl) -> TApply(s, List.map convert_to_tree_term tl)
  | Array a -> TArray (convert_to_tree_array a)
  | Cvc4_Variable v -> TCvc4_Variable (Var v)
  | Function_Local_Variable v -> TFunction_Local_Variable v
  | Variable v -> TVariable v
  | Ite (t1, t2, t3, t4) ->
      TIte (convert_to_tree_term t1, convert_to_tree_term t2, convert_to_tree_term t3, convert_to_tree_term t4)
  | Record (s, tl) -> TRecord (s, List.map (fun (s, t) -> (s, convert_to_tree_term t)) tl)
  | To_array t -> TTo_array (convert_to_tree_term t)
  (* TODO should not appear here *)
  | Trees _ -> raise Not_value

and convert_to_tree_array a =
  match a with
  | Array_var v -> TArray_var v
  | Const t -> TConst (convert_to_tree_term t)
  | Store (a, t1, t2) ->
      TStore (convert_to_tree_array a, convert_to_tree_term t1, convert_to_tree_term t2)

let rec convert_tree_to_term (t: tree) : term =
  match t with
  | Node mpt ->
      let l = Mpr.bindings mpt in
      let l = List.map (fun (k,e) -> (k, convert_tree_to_term e)) l in
      Trees l
  | Leaf t ->
      convert_tdef_to_term t

and convert_tdef_to_term (t: tree_definition) =
  match t with
  | TFunction (_l, t) -> convert_tterm_to_term t
  | TTerm t -> convert_tterm_to_term t
  | TNoelement -> Sval (Other ("error")) (* TODO check which error can be raised here *)

and convert_tterm_to_term t =
  match t with
  | TSval v -> Sval v
  | TApply (s, tl) -> Apply (s, List.map convert_tterm_to_term tl)
  | TArray ta -> Array (convert_tarray_to_array ta)
  | TCvc4_Variable (Var v) -> Cvc4_Variable v
  | TCvc4_Variable (Tree v) -> convert_tree_to_term v
  | TFunction_Local_Variable v -> Function_Local_Variable v
  | TVariable v -> Variable v
  | TIte (t1, t2, t3, t4) ->
      let t1 = convert_tterm_to_term t1 in
      let t2 = convert_tterm_to_term t2 in
      let t3 = convert_tterm_to_term t3 in
      let t4 = convert_tterm_to_term t4 in
      Ite (t1, t2, t3, t4)
  | TRecord (s, ls) ->
      Record (s, List.map (fun (s, t) -> (s, convert_tterm_to_term t)) ls)
  | TTo_array t -> To_array (convert_tterm_to_term t)

and convert_tarray_to_array a =
  match a with
  | TArray_var v -> Array_var v
  | TConst t -> Const (convert_tterm_to_term t)
  | TStore (a, t1, t2) -> Store (convert_tarray_to_array a, convert_tterm_to_term t1, convert_tterm_to_term t2)

598
let create_list (projections_list: Ident.ident Mstr.t)
DAILLER Sylvain's avatar
DAILLER Sylvain committed
599
    (field_list: Ident.ident Mstr.t)
600 601 602
    (list_records: ((string * string) list) Mstr.t)
    (noarg_constructors: string list) (set_str: Ident.Sattr.t Mstr.t)
    (table: definition Mstr.t) =
603 604 605 606 607 608 609 610

  (* Convert list_records to take replace fields with model_trace when
     necessary. *)
  let list_records =
    Mstr.fold (fun key l acc ->
      Mstr.add key (List.map (fun (a, b) -> if b = "" then a else b) l) acc) list_records Mstr.empty
  in

611 612
  (* Convert Apply that were actually recorded as record to Record. Also replace
     Variable that are originally unary constructor  *)
613
  let table =
614
    Mstr.fold (fun key value acc ->
615 616 617
      let value =
        definition_apply_to_record list_records noarg_constructors value
      in
618
      Mstr.add key value acc) table Mstr.empty
619
  in
620 621 622 623

  (* First populate the table with all references to a cvc variable *)
  let table = get_all_var table in

624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
  Debug.dprintf debug_cntex "After parsing@.";
  Mstr.iter (fun k e ->
      let t = convert_to_tree_def e in
      Debug.dprintf debug_cntex "constant %s : %a@."
        k print_def t)
    table;

  let table: tree_definition Mstr.t =
    Mstr.fold (fun k elt acc ->
        let elt = convert_to_tree_def elt in
        Mstr.add k elt acc) table Mstr.empty
  in

  (* Convert the table to a table of tree *)
  (* TODO this could probably be optimized away *)
  let table1 = Mstr.fold (fun key value acc ->
      Mstr.add key (Leaf value) acc) table Mstr.empty
  in

643
  (* First recover values stored in projections that were registered *)
644 645
  let table =
    Mstr.fold (fun key value acc ->
DAILLER Sylvain's avatar
DAILLER Sylvain committed
646
      if Mstr.mem key projections_list || Mstr.mem key field_list then
647
        add_vars_to_table acc key value
648 649
      else
        acc)
650 651 652 653 654 655
      table table1
  in

  (* Only printed in debug *)
  Debug.dprintf debug_cntex "Value were queried from projections@.";
  print_table table;
656 657 658

  (* Then substitute all variables with their values *)
  let table =
659 660 661 662 663 664 665 666 667 668
    Mstr.fold (fun key v acc -> refine_variable_value acc key v) table table
  in

  Debug.dprintf debug_cntex "Variable values were propagated@.";
  print_table table;

  let table: term Mstr.t =
    Mstr.fold (fun k e acc ->
        Mstr.add k (convert_tree_to_term e) acc) table Mstr.empty
  in
669 670

  (* Then converts all variables to raw_model_element *)
671 672
  Mstr.fold
    (fun key value list_acc ->
DAILLER Sylvain's avatar
DAILLER Sylvain committed
673
      try (convert_to_model_element ~set_str field_list key value :: list_acc)
674 675
      with Not_value when not (Debug.test_flag Debug.stack_trace) ->
        Debug.dprintf debug_cntex "Element creation failed: %s@." key; list_acc
676
      | e -> raise e)
677 678
    table
    []