Commit 113b783b authored by David Hauzar's avatar David Hauzar

Parsing also arrays with non integer indices.

parent 8c6d96ee
......@@ -33,7 +33,7 @@ type model_value =
| Bitvector of int
| Unparsed of string
and arr_index = {
arr_index_key : int;
arr_index_key : model_value;
arr_index_value : model_value;
}
and model_array = {
......@@ -51,11 +51,8 @@ let array_add_element ~array ~index ~value =
(*
Adds the element value to the array on specified index.
*)
let int_index = match index with
| Integer s -> int_of_string s
| _ -> raise Not_found in
let arr_index = {
arr_index_key = int_index;
arr_index_key = index;
arr_index_value = value
} in
{
......@@ -67,7 +64,7 @@ let rec print_indices sanit_print fmt indices =
match indices with
| [] -> ()
| index::tail ->
fprintf fmt "; %d -> " index.arr_index_key;
fprintf fmt "; %a -> " (print_model_value_sanit sanit_print) index.arr_index_key;
print_model_value_sanit sanit_print fmt index.arr_index_value;
print_indices sanit_print fmt tail
and
......
......@@ -20,7 +20,7 @@ type model_value =
| Bitvector of int
| Unparsed of string
and arr_index = {
arr_index_key : int;
arr_index_key : model_value;
arr_index_value : model_value;
}
and model_array = {
......
......@@ -85,9 +85,16 @@ other_than_const_array:
| INT_STR { $1 }
| CONST { "const" }
(* Example:
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4)
(store (store ((as const (Array Int Int)) false) 1 true) 3 true) *)
(* Examples:
(1) Map from int to int:
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4)
(2) Map from int to bool:
(store (store ((as const (Array Int Int)) false) 1 true) 3 true)
(3) Map from int to map from int to int (all elemets are 0):
((as const (Array Int (Array Int Int))) ((as const (Array Int Int)) 0))
(4) Map from int to map from int to int (element [1][1] is 3, all others are 0)
(store (store ((as const (Array Int (Array Int Int))) ((as const (Array Int Int)) 0)) 0 (store ((as const (Array Int Int)) 0) 0 3)) 1 (store ((as const (Array Int Int)) 0) 1 3))
*)
array:
| LPAREN possible_space
LPAREN possible_space
......@@ -97,16 +104,16 @@ array:
RPAREN
{ Model_parser.array_create_constant ~value:$13 }
| LPAREN possible_space
STORE possible_space array possible_space value SPACE integer
STORE possible_space array possible_space value SPACE value
possible_space
RPAREN
{ Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
array_skipped_part:
| LPAREN term_list RPAREN {}
(* Example:
(_ bv2048 16) *)
bitvector:
| BITVECTOR_VALUE
{ $1 }
array_skipped_part:
| LPAREN term_list RPAREN {}
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