[FEATURE] Interval analysis to improve a..b #446
Labels
help wanted
product-owner-triage
This should be triaged by the product owner
usability
UX improvements
Milestone
Apalache translates the range operator
a..b
to SMT only ifa
andb
areconstant expressions. This annoys the users: #425, #150.
The standard workaround is to find two constants
c
andd
such thatc <= a /\ b <= d
in all states. Then the user can rewrite the range operatora..b
as{i \in c..d: a <= i /\ i <= b}
. This works in Apalache, as therange
c..d
is constant.We could do it better. By running interval analysis, we could automatically
compute
c
andd
, if such constants exist. Moreover, the staticanalyzer could give the user better feedback, as it does not have to be as
local as the SMT rewriter.
The text was updated successfully, but these errors were encountered: