[FEATURE] Grammatical Case Distinction for SMT Formulas

[rindPHI]

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 #83 (comment):

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.