Commit c5d3d0f4 authored by David Hauzar's avatar David Hauzar

Enhancement of parsing of arrays in cvc4 counterexamples.

The indices and values of arrays can be now arbitrary values
(not just indices).
parent e4340f82
......@@ -85,17 +85,18 @@ other_than_const_array:
| CONST { "const" }
(* Example:
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4) *)
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4)
(store (store ((as const (Array Int Int)) false) 1 true) 3 true) *)
array:
| LPAREN possible_space
LPAREN possible_space
AS SPACE CONST possible_space array_skipped_part possible_space
RPAREN possible_space
integer possible_space
value possible_space
RPAREN
{ Model_parser.array_create_constant ~value:$13 }
| LPAREN possible_space
STORE possible_space array possible_space integer SPACE integer
STORE possible_space array possible_space value SPACE integer
possible_space
RPAREN
{ Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
......
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