Project

General

Profile

Actions
Copy link

Task #5462

closed

[arrays] arrays initialization is inconvenient

Added by Sergey Smolov about 10 years ago. Updated almost 10 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Artem Kotsynyak
Category:
-
Target version:
0.3
Start date:
12/04/2014
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Published in build:
141226

Description

There is only one way for array to be initialized - by constructing SMT-LIB strings like "((key_1:value_1)...(key_n:value_n))".

It is inconvenient because an additional work is needed here to translate an array into such string format.

More suitable methods are needed here (for example, look at methods for LOGIC_INTEGER/LOGIC_BOOLEAN types an so on).

Actions
Copy link
 #1

Updated by Artem Kotsynyak about 10 years ago

  • Status changed from New to Feedback

r726 added ru.ispras.fortress.data.types.datamap.DataMap type implementing Map<Data, Data> to use as arrays backend. Data.newArray(DataMap map) converts given map to Data instance.

Actions
Copy link
 #2

Updated by Sergey Smolov about 10 years ago

  • Status changed from Feedback to Resolved

Ok, the methods you've implemented are suitable for array initialization with constants.

Actions
Copy link
 #3

Updated by Sergey Smolov about 10 years ago

  • Status changed from Resolved to Verified
Actions
Copy link
 #4

Updated by Andrei Tatarnikov almost 10 years ago

  • Status changed from Verified to Closed
  • % Done changed from 0 to 100
  • Published in build set to 141226
Actions
Copy link

Also available in: Atom PDF