Implement solving SMT formulas by grammatical case distinction: A predicate holds iff it holds for all direct children of an involved variable. Several issues need to be resolved for this, see #83.
In this particular example, one idea would be to transform:
(= (str.indexof <entry> "x") (- 1))
into
(= (str.indexof <entry>.<A> "x") (- 1)) and
(= (str.indexof <entry>.<X> "x") (- 1)) and
(= (str.indexof <entry>.<A> "x") (- 1))
and solve each subexpression separately.
My intuition is that Z3 would return unsat for(= (str.indexof <entry>.<X> "x") (- 1)), which implies unsat for the full expression. Unfortunately I can‘t test this currently as I am replying from my phone.
Implement solving SMT formulas by grammatical case distinction: A predicate holds iff it holds for all direct children of an involved variable. Several issues need to be resolved for this, see #83.
Originally posted by @leonbett in https://github.com/rindPHI/isla/issues/83#issuecomment-1667448425:
In this particular example, one idea would be to transform:
(= (str.indexof <entry> "x") (- 1))into
and solve each subexpression separately.
My intuition is that Z3 would return unsat for
(= (str.indexof <entry>.<X> "x") (- 1)), which implies unsat for the full expression. Unfortunately I can‘t test this currently as I am replying from my phone.