BoiseState-AdaptLab / IEGenLib

Inspector/Executor Generation Library for manipulating sets and relations with uninterpreted function symbols.
BSD 2-Clause "Simplified" License
2 stars 4 forks source link

Dataspace Versions #102

Open Aaron3154518 opened 3 years ago

Aaron3154518 commented 3 years ago

Every time a data space is written to, a new version should be created. This new version replaces the old version on every line between the last write and the current line.

Aaron3154518 commented 3 years ago

@cathieO Do we need to add a statement for each new version which assigns the previous version's value to the new version?

cathieO commented 3 years ago

Nope. You need to replace the uses in the previous statements to the new version and the read in the current statement.

On Tue, Jul 6, 2021 at 12:12 PM Aaron3154518 @.***> wrote:

@cathieO Do we need to add a statement for each new version which assigns the previous version's value to the new version?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

--

Catherine Olschanowsky, Ph.D. Assistant Professor

rvishnkr commented 3 years ago

SSA is not applied if a dataspace is not surrounded by $ signs

rvishnkr commented 3 years ago

The dataspace get renamed to dataSpaceName_number when we encounter the first write. When we encounter any subsequent writes, the replaceDataSpaceName functions rechecks all the dataspaces names slowing it down significantly. We need to iterate backwards until we find the previous write based on the rename format varName__w__number

rvishnkr commented 3 years ago

@cathieO when we do renames how do we get the datatypes?