This project is read-only.


array rewrite suggestion


I see many terms of the form:

(= (select (store k!82 f23 k!98) index!83) (select k!82 index!83))

Logically, this could be simplified to:

(= (select k!82 f23) k!98)

I have no idea if such a transformation would make a meaningful difference, but it might be something to consider.
Closed Jan 24, 2013 at 9:08 PM by leodemoura
The simplification is not sound.


leodemoura wrote Jan 9, 2013 at 5:52 PM

This transformation is not sound. That is, the formulas are not logically equivalent.
Here is a counterexample

f23 -> 2
k!98 -> 3
index!83 -> 1
k!82 -> { 2 -> 4, else -> 0 }

The first formula is true and the second is false in this model.