Conversation
| return false; | ||
| } | ||
|
|
||
| void arrayst::weg_path_condition( |
There was a problem hiding this comment.
should be documented
There was a problem hiding this comment.
using a verb in the function name is generally clearer
|
@tautschnig shout when you want a review from me. |
b179c53 to
7a8f99b
Compare
7a8f99b to
b0c69ff
Compare
|
@tautschnig This PR is still waiting on some changes to address reviewer comments (and now a rebase). Is there a plan to progress on this PR since it is mentioned in others? |
Yes, this is on my pile of TODOs. In terms of performance, it's probably one of the most urgent to work on. Just trying to address the soundness-related ones first. |
|
@tautschnig : Trevor and I have been having some issues with the current array code and may need to look at it in the next few months. Reviewing this / getting it merged might well help us with that. |
c820fbd to
211fb19
Compare
211fb19 to
837dbac
Compare
Uses the capabilities of binding_exprt instead of relying on the unrelated replace_exprt to do the right thing.
837dbac to
31ade23
Compare
All existing tests rely on indexed access to arrays, which is covered by the read-over-write axiom.
There is not really anything wrong in having empty bitvectors, which we otherwise already support (as of e021eef).
The test specification expects that the indices 0, 1, and one other are instantiated. The array theory is only required to do so when also reading from these elements.
This implements Christ and Hoenicke's Weakly Equivalent Arrays (https://arxiv.org/pdf/1405.6939.pdf) with in-place depth-first path enumeration. Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
31ade23 to
a02b480
Compare
Code has now largely been rewritten.
|
Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work. |
No description provided.