isla icon indicating copy to clipboard operation
isla copied to clipboard

SyntaxError when trying to parse formula with shortened paths

Open mojung opened this issue 2 years ago • 0 comments

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

mojung avatar Jan 06 '23 19:01 mojung