1

Closed

array rewrite suggestion

description

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 at 8:08 PM by leodemoura
The simplification is not sound.

comments

leodemoura wrote Jan 9 at 4: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.

Sign in to add a comment