rindPHI / isla

The ISLa (Input Specification Language) language & solver.
https://isla.readthedocs.org
GNU General Public License v3.0
62 stars 8 forks source link

[BUG] Correct result with infix AND, incorrect result with s-expr AND #72

Open leonbett opened 1 year ago

leonbett commented 1 year ago

Describe the bug Sometimes ISLa only produces a correct result for infix AND, but not for S-expr AND. It seems like the S-expr AND constraint is completely ignored.

To Reproduce Run the python program below. It should produce the same results for all three versions of the same constraint, but only the infix version produces the correct result.

from isla.solver import ISLaSolver

IBAN_GRAMMAR_BNF_SIMPLE = '''
<start> ::= <iban>
<iban> ::= <country> <checksum> <bban>
<country> ::= <D> <E>
<D> ::= "D"
<E> ::= "E"
<checksum> ::= <digit> <digit>
<bban> ::= <digit> | <digit> <bban>
<digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
'''

def isla_solve(g, c):
    solver = ISLaSolver(
        grammar=g,
        formula=c,
        timeout_seconds=100
    )
    return solver.solve()

def main():
    cond = '(= str.to_code(<iban>.<bban>.<digit>) str.to_code(<iban>.<bban>.<bban>.<digit>))'
    length_constraint = "(= 6 str.len(start))"

    isla_formula_1 = f'{length_constraint} and {cond}' # correct result
    print('Infix result: ', isla_solve(IBAN_GRAMMAR_BNF_SIMPLE, isla_formula_1))

    isla_formula_2 = f'(and {cond} {length_constraint})' # incorrect result (seems to ignore all constraints)
    print('Sexpr result 1: ', isla_solve(IBAN_GRAMMAR_BNF_SIMPLE, isla_formula_2))

    isla_formula_3 = f'(and {length_constraint} {cond})' # incorrect result (seems to ignore all constraints)
    print('Sexpr result 2: ', isla_solve(IBAN_GRAMMAR_BNF_SIMPLE, isla_formula_3))

if __name__ == "__main__":
    main()

Expected behavior Infix and S-expr AND should have the same result.

System/Installation Specs:

rindPHI commented 1 year ago

This is indeed a bug. I will put it on hold for a while. I don't consider mixing the S-expr and "mathematical" style a good "feature" and want to prevent this since it broke many things. I plan to offer different ISLa concrete syntax parsers with exclusive support for either S-expr or mathematical.