Loading...
We prove an NP upper bound on a theory of integer-indexed integer-valued arrays that extends combi- natory array logic with an ordering relation on the index set and the ability to express sums of elements. We compare our fragment with seven other fragments in the literature in terms of their expressiveness and computational complexity.
Loading...
Name
array_sums_smt.pdf
Type
preprint
Access type
openaccess
License Condition
CC BY
Size
211.85 KB
Format
Adobe PDF
Checksum (MD5)
771f004795b2d90bf73ff340efede59c