isla
isla copied to clipboard
[BUG] Correct result with infix AND, incorrect result with s-expr AND
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:
- ISLa Version: 1.13.9
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.