isla
isla copied to clipboard
SyntaxError when trying to parse formula with shortened paths
Description
When trying to parse the formula below (see code snippet), ISLa raises a SyntaxError. Using full paths instead of shortened ones resolves the issue, although ISLa displays a warning message.
Steps To Reproduce
Execute the following code snippet:
from isla.helpers import crange
from isla.language import parse_isla
from isla.solver import ISLaSolver
grammar = {
'<start>': ['<x> <y>'],
'<x>': ['<xdigit>'],
'<xdigit>': ['<digit>'],
'<y>': ['<ydigit>'],
'<ydigit>': ['<digit>'],
'<digit>': crange('1', '9')
}
constraint = parse_isla(
"""
forall <x> x:
exists <y> y:
(= x..<digit> y..<digit>)
""",
grammar
)
print(constraint)
solver = ISLaSolver(
grammar,
constraint
)
print(solver.solve().to_string())
While the expected output would be the parsed formula, followed by a correct solution, i.e. two equal numbers between 1 and 9, the actual output should be as follows:
SyntaxError: Unbound variables: y in formula
forall <x> x in start:
exists <y> y in start:
(= digit digit_0)
Now replace the constraint in the code snippet above with the one below, and execute the entire code snippet once again. Note how the constraint below differs from the one above in that it only contains full paths.
constraint = parse_isla(
"""
forall <x> x:
exists <y> y:
(= x.<xdigit>.<digit> y.<ydigit>.<digit>)
""",
grammar
)
The output should now be similar to the following:
∀ "{<digit> digit}" = x ∈ start: (∃ '{<digit> digit_0}' = y ∈ start: (digit == digit_0))
Existential qfr elimination: Could not eliminate existential formula ∃ '{<digit> digit_0}' = y ∈ <digit> <y>: ((digit == digit_0, {'digit': '<digit>'})) by matching or tree insertion
Existential qfr elimination: Could not eliminate existential formula ∃ '{<digit> digit_0}' = y ∈ <digit> <ydigit>: ((digit == digit_0, {'digit': '<digit>'})) by matching or tree insertion
2 2
Tested ISLa version
ISLa versions 1.9.9 and 1.10.0