[BUG] Unparseable XPath-style Formula

[rindPHI]

Describe the bug

Some seemingly innocuous ISLa formulas with XPath-style shortcuts don't parse.

To Reproduce

Consider the following code:

from isla import __version__
from isla.solver import ISLaSolver

print(__version__)  # 1.14.4

grammar = {
    "<start>": ["<eq>"],
    "<eq>": ["|<number>| = |<number>|"],
    "<number>": ["<digit>", "-<digit>"],
    "<digit>": ["0", "1", "2", "3", "4", "5", "6", "7", "8", "9"],
}

fml_orig = """
not (<eq>.<number>[1] = <eq>.<number>[2]) and 
<eq>.<number>[1].<digit> = <eq>.<number>[2].<digit>
"""

fml_working = r'''
forall <eq> eq = "|{<number> n1}| = |{<number> n2}|" in start: (
  not n1 = n2 and
  forall <digit> d1 in n1: (
    forall <digit> d2 in n2: (
      d1 = d2
    )
  )
)
'''

fml_different_error = r'''
forall <eq> eq = "|{<number> n1}| = |{<number> n2}|" in start: (
  not n1 = n2 and
  n1.<digit> = n2.<digit>
)
'''

s = ISLaSolver(grammar, fml_different_error)  # Replace with formula to try out
print(s.solve())

Parsing fml_orig yields an error because some match expressions cannot be merged. Merging them is indeed difficult/impossible based on the current procedures. fml_working is a working refactoring, but hard to come up with automatically (it only works if there is exactly on <digit> in each <number>). fml_different_error is an intermediate step of a different possible resolution scenario in which the numbers would be factored out first. However, this yields a different error:

SyntaxError: Unbound variables: digit_0, digit in formula
forall <eq> eq="|{<number> n1}| = |{<number> n2}|" in start:
  ((not (= n1 n2)) and
  (= digit digit_0))

This error should be fixed. Afterward, we can implement an XPath resolution scenario in which fml_different_error is an intermediate step. The final result must use an optional [-], otherwise it's impossible to merge the resulting match expressions.

Expected behavior

Everything should parse fine; a possible printout on the terminal would be

1.14.4
|0| = |-0|

System/Installation Specs:

• ISLa Version: 1.14.4
• Python Version: 3.11.7
• OS: macOS

Additional context

The issue came up during the master thesis of Stanimir.