Project

General

Profile

Actions

Task #5462

closed

[arrays] arrays initialization is inconvenient

Added by Sergey Smolov over 9 years ago. Updated over 9 years ago.

Status:
Closed
Priority:
Normal
Category:
-
Target version:
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 #1

Updated by Artem Kotsynyak over 9 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 #2

Updated by Sergey Smolov over 9 years ago

  • Status changed from Feedback to Resolved

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

Actions #3

Updated by Sergey Smolov over 9 years ago

  • Status changed from Resolved to Verified
Actions #4

Updated by Andrei Tatarnikov over 9 years ago

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

Also available in: Atom PDF