Commit 44ad10b4 authored by Sylvain Dailler's avatar Sylvain Dailler

ce: model parsing now accepts let-binding with an array typed variable

parent 7be4c9dc
......@@ -50,6 +50,8 @@ let rec get_variables_term (table: correspondence_table) t =
and get_variables_array table a =
match a with
| Array_var _v ->
table
| Const t ->
let table = get_variables_term table t in
table
......@@ -146,6 +148,7 @@ let rec refine_definition table t =
and refine_array table a =
match a with
| Array_var _v -> a
| Const t ->
let t = refine_function table t in
Const t
......@@ -225,6 +228,7 @@ let rec convert_array_value (a: array) : Model_parser.model_array =
let rec create_array_value a =
match a with
| Array_var _v -> raise Not_value
| Const t -> { Model_parser.arr_indices = !array_indices;
Model_parser.arr_others = convert_to_model_value t}
| Store (a, t1, t2) ->
......@@ -288,6 +292,7 @@ let default_apply_to_record (list_records: (string list) Mstr.t) (t: term) =
let rec array_apply_to_record (a: array) =
match a with
| Array_var _v -> raise Not_value
| Const x ->
let x = apply_to_record x in
Const x
......
......@@ -147,6 +147,9 @@ array:
| LPAREN
STORE array smt_term smt_term
RPAREN { Smt2_model_defs.Store ($3, $4, $5) }
| LPAREN
STORE name smt_term smt_term
RPAREN { Smt2_model_defs.Store (Smt2_model_defs.Array_var $3, $4, $5) }
(* When array is of type int -> bool, Cvc4 returns something that looks like:
(ARRAY_LAMBDA (LAMBDA ((BOUND_VARIABLE_1162 Int)) false)) *)
| LPAREN
......
......@@ -14,6 +14,7 @@ open Stdlib
type variable = string
type array =
| Array_var of variable
| Const of term
| Store of array * term * term
......@@ -56,6 +57,7 @@ let print_float fmt f =
let rec print_array fmt a =
match a with
| Array_var v -> Format.fprintf fmt "ARRAY_VAR : %s" v
| Const t -> Format.fprintf fmt "CONST : %a" print_term t
| Store (a, t1, t2) ->
Format.fprintf fmt "STORE : %a %a %a"
......@@ -103,6 +105,8 @@ exception Bad_local_variable
let rec make_local_array vars_lists a =
match a with
| Array_var v ->
Array_var v
| Const t ->
let t' = make_local vars_lists t in
Const t'
......@@ -178,6 +182,13 @@ let rec subst var value t =
and subst_array var value a =
match a with
| Array_var v ->
if v = var then
match value with
| Array a -> a
| _ -> Array_var v
else
Array_var v
| Const t -> Const (subst var value t)
| Store (a, t1, t2) ->
let t1 = subst var value t1 in
......
......@@ -14,6 +14,8 @@ open Stdlib
type variable = string
type array =
(* Array_var is used by let-bindings only *)
| Array_var of variable
| Const of term
| Store of array * term * term
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment