inconsistent result for evaluate()/solve() when changing order of variables and constants in (+) operands

[michaelmera]

Here is a file reproducing the problem. It does two times the same computation, just inverting the order of the operands of (+):

# isla_add_order.py
from isla.type_defs import Grammar
from isla.solver import ISLaSolver

GRAMMAR: Grammar = {
    "<start>": ["<isbn10>"],
    "<isbn10>": [
        "<digit><digit><digit><digit><digit><digit><digit><digit><digit><checkdigit>"
    ],
    "<digit>": ["0", "1", "2", "3", "4", "5", "6", "7", "8", "9"],
    "<checkdigit>": ["0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "X"],
}

valid="097522980X"

if __name__ == "__main__":
    solver = ISLaSolver(GRAMMAR, "(= (+ 254 10 (* 2 str.to.int(<isbn10>.<digit>[9]))) 264)")
    print(solver.evaluate(valid))
    solver = ISLaSolver(GRAMMAR, "(= (+ 254 (* 2 str.to.int(<isbn10>.<digit>[9])) 10) 264)")
    print(solver.evaluate(valid))

The output is:

$ python isla_add_order.py
TRUE
FALSE

[rindPHI]

Hi Michael,

ISLa can unfortunately only handle the binary version of "+" it seems. I added a test case and a TODO for the issue. In the meantime, you could just write

solver = ISLaSolver(GRAMMAR, "(= (+ 254 (+ 10 (* 2 str.to.int(<isbn10>.<digit>[9])))) 264)")

This version of + should be commutative.

Best, Dominic