[TG-2721] Use sparse arrays in string_refinementt::get#2009

Merged

romainbrenguier merged 25 commits intodiffblue:developfrom

romainbrenguier:solvers/sparse-arrays-in-get

Apr 10, 2018

Commits on Apr 10, 2018

Use map instead of vector for sparse array entries
romainbrenguier
committed
Initialize sparse array from array_exprt
romainbrenguier
committed
Clear string_dependencies in calls to dec_solve
romainbrenguier
committed
Reduce number of constraints in format
romainbrenguier
committed
Initialization of sparse array from array-list
romainbrenguier
committed
Add an interval_sparse_array::of_expr function
romainbrenguier
committed
Add an `at` function for access in sparse arrays
romainbrenguier
committed
Add a sum_overflows function
romainbrenguier
committed
Truncate string concatenations in case of overflow
romainbrenguier
committed
Get rid of calls to plus_exprt_with_overflow
romainbrenguier
committed
Remove plus_exprt_with_overflow_check
romainbrenguier
committed
Use sparse arrays in substitute_array_access
romainbrenguier
committed
Add concretize function for interval_sparse_array
romainbrenguier
committed
Refactor string_refinementt::get
romainbrenguier
committed
Use sparse arrays in string_refinement::get
romainbrenguier
committed
Use sparse arrays in get_array
romainbrenguier
committed
Avoid copy in ranged for loops over expressions
romainbrenguier
committed
Remove unused header
romainbrenguier
committed
Use get_array in get_char_array_and_concretize
romainbrenguier
committed
Use concretize instead of fill_in_array
romainbrenguier
committed
Stop using concretize_arrays_in_expression
romainbrenguier
committed
Tests where model involves long strings
romainbrenguier
committed
Stop using concretize_array_expr in unit tests
romainbrenguier
committed
Reserve size of array in concretize
romainbrenguier
committed
Refactor interval_sparse_array::concretize
romainbrenguier
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[TG-2721] Use sparse arrays in string_refinementt::get#2009

Commits on Apr 10, 2018

Use map instead of vector for sparse array entries

Initialize sparse array from array_exprt

Clear string_dependencies in calls to dec_solve

Reduce number of constraints in format

Initialization of sparse array from array-list

Add an interval_sparse_array::of_expr function

Add an `at` function for access in sparse arrays

Add a sum_overflows function

Truncate string concatenations in case of overflow

Get rid of calls to plus_exprt_with_overflow

Remove plus_exprt_with_overflow_check

Use sparse arrays in substitute_array_access

Add concretize function for interval_sparse_array

Refactor string_refinementt::get

Use sparse arrays in string_refinement::get

Use sparse arrays in get_array

Avoid copy in ranged for loops over expressions

Remove unused header

Use get_array in get_char_array_and_concretize

Use concretize instead of fill_in_array

Stop using concretize_arrays_in_expression

Tests where model involves long strings

Stop using concretize_array_expr in unit tests

Reserve size of array in concretize

Refactor interval_sparse_array::concretize