Right-hand side of disjunction not always considered

[mojung]

Description

ISLa does not always consider the right-hand side of a disjunction. Setting ISLaSolver.__init__'s parameter activate_unsat_support to True resolves the issue in many cases, but not always.

This bug also affects implications.

Steps To Reproduce

Please execute the code snippet below. The expected output would always be [Any number between 10 and 19] 10, independent of the constraint being used. Please see the comment above each constraint for the actual output after passing that constraint to ISLa, as well as some additional information.

import traceback

from isla.helpers import crange
from isla.language import parse_isla
from isla.solver import ISLaSolver

activate_unsat_support = True

grammar = {
    '<start>': ['<x> <y>'],
    '<x>': ['<leaddigit><digit>'],
    '<y>': ['<leaddigit><digit>'],
    '<leaddigit>': ['1'],
    '<digit>': crange('0', '9')
}

# Actual output: The output should be `StopIteration` since the left-hand side is unsatisfiable, and the right-hand 
# side not considered in this case.
constraint_1 = parse_isla(
    """
    not (= <x>.<leaddigit> <y>.<leaddigit>)
    or
    (= <y>.<digit> "0")
    """,
    grammar
)

# Equivalent to `constraint_1`, but the order of the two operands has been inverted.
# Actual output: The output should be correct since the left-hand side of the disjunction is now satisfiable.
constraint_2 = parse_isla(
    """
    (= <y>.<digit> "0")
    or
    not (= <x>.<leaddigit> <y>.<leaddigit>)
    """,
    grammar
)

# Same as `constraint_1`, but with added quantifiers.
# Actual output: If `activate_unsat_support` is set to `True`, then the output should be correct, otherwise the output
# should again be `StopIteration`.
constraint_3 = parse_isla(
    """
    forall <x> x:
        forall <y> y:
            (not (= x.<leaddigit> y.<leaddigit>)
            or
            (= y.<digit> "0"))
    """,
    grammar
)

# Equivalent to `constraint_1`, but the disjunction has been transformed into an implication.
# Actual output: `StopIteration`
constraint_4 = parse_isla(
    """
    (= <x>.<leaddigit> <y>.<leaddigit>)
    implies
    (= <y>.<digit> "0")
    """,
    grammar
)

for i, constraint in enumerate([constraint_1, constraint_2, constraint_3, constraint_4], 1):
    print(f'*** constraint_{i} ***')
    try:
        solver = ISLaSolver(grammar, constraint, activate_unsat_support=activate_unsat_support)
        for _ in range(10):
            print(solver.solve().to_string())
    except StopIteration:
        traceback.print_exc()

Tested ISLa version

ISLa versions 1.10.0 (pip version) and 1.10.1 (GitHub commit #14f84ef)

[rindPHI]

Hi Moritz,

I will need more time too investigate all your examples, but in

not (= <x>.<leaddigit> <y>.<leaddigit>)
or
(= <y>.<digit> "0")
)

the unsatisfiability of the first constraint simply implies that the constraint is equivalent to

(= <y>.<digit> "0")

so you should get the input 10 10. What do you get?

If ISLa is asked to solve a disjunction A or B, it attempts to generate inputs from A and inputs from B separately (see also https://rindphi.github.io/isla/islaspec/#propositional-combinators). A implies B is equivalent to not A or B, i.e., you get inputs satisfying not A and inputs satisfying B.

Is it possible that instead of A or B you mean A or (not A and B) (or not A or (A and B))? This would basically be the "intuitionistic" interpretation of implication; ISLa is very "classical" in these cases. ors just split the states (constraint-tree pairs).

Best, Dominic

[mojung]

Hi Dominic,

Thank you for your reply!

I will need more time too investigate all your examples, but in

not (= <x>.<leaddigit> <y>.<leaddigit>)
or
(= <y>.<digit> "0")
)

the unsatisfiability of the first constraint simply implies that the constraint is equivalent to

(= <y>.<digit> "0")

so you should get the input 10 10. What do you get?

I was expecting to get [Any number between 10 and 19] 10, but instead got StopIteration.

If ISLa is asked to solve a disjunction A or B, it attempts to generate inputs from A and inputs from B separately (see also https://rindphi.github.io/isla/islaspec/#propositional-combinators). A implies B is equivalent to not A or B, i.e., you get inputs satisfying not A and inputs satisfying B.

In the given example, ISLa seems to only output solutions that satisfy the left-hand side of the disjunction (or raise a StopIteration exception if there are none). If you allow leading digits to also take on values other than 1 (e.g. by changing rule '<leaddigit>': ['1'] to'<leaddigit>': ['1', '2']), then you will see that ISLa generates inputs that contain two numbers whose leading digits do not match, i.e. inputs that satisfy the left-hand side of the disjunction, but no inputs that only satisfy the right-hand side of the disjunction. (For constraint_2 ISLa generates inputs within which the second digit of y is always 0, which again indicates that ISLa only considers the left-hand side of the disjunction in the given example.)

Is it possible that instead of A or B you mean A or (not A and B) (or not A or (A and B))? This would basically be the "intuitionistic" interpretation of implication; ISLa is very "classical" in these cases. ors just split the states (constraint-tree pairs).

I'm not sure if I'm missing something here, but A or B and A or (not A and B) (and also not A or B and not A or (A and B) for that matter) should be equivalent, and choosing one formula over the other should make no difference w.r.t. the generated inputs other than some inputs may becoming less likely to be generated due to the splitting of states and the additional constraint on the right-hand side of the disjunction.

Having said that, when using the constraint below, then ISLa actually does find a correct solution, but only with activate_unsat_support set to True.

# Equivalent to `constraint_1`, but the right-hand side of the disjunction is now more restrictive.
# Actual output: If `activate_unsat_support` is set to `True`, then the output should be correct, otherwise the output
# should again be `StopIteration`.
constraint_5 = parse_isla(
    """
    not (= <x>.<leaddigit> <y>.<leaddigit>)
    or
    ((= <x>.<leaddigit> <y>.<leaddigit>) and (= <y>.<digit> "0"))
    """,
    grammar
)

Best,
Moritz

[rindPHI]

Hi Moritz,

with ISLa 1.11.0 (will probably be published within the next hour; changes are independent from this issue), I get

*** constraint_1 ***
18 10
14 10
12 10
11 10
15 10
17 10
19 10
16 10
13 10
10 10
*** constraint_2 ***
17 10
13 10
16 10
14 10
12 10
15 10
11 10
10 10
18 10
19 10
*** constraint_3 ***
18 10
17 10
15 10
13 10
14 10
12 10
11 10
19 10
10 10
16 10
*** constraint_4 ***
19 10
10 10
13 10
18 10
12 10
16 10
15 10
17 10
14 10
11 10

when running your MWE. You said

The expected output would always be [Any number between 10 and 19] 10, independent of the constraint being used.

so I guess you're happy now? :smile:

Considering your comment

I'm not sure if I'm missing something here, but A or B and A or (not A and B) (and also not A or B and not A or (A and B) for that matter) should be equivalent, and choosing one formula over the other should make no difference w.r.t. the generated inputs other than some inputs may becoming less likely to be generated due to the splitting of states and the additional constraint on the right-hand side of the disjunction.

In classical logic, they're equivalent (in intuitionistic logic, the disjunction is strictly stronger). Otherwise, you're correct; the difference concerning outputs generated by ISLa will be one of their distribution. However, the formula A and not B or B and not A (i.e., exclusive or) is strictly stronger and will generate solutions where either A or B hold true, but not both. I think this might be what some ppl expect when they say "or" in ISLa, so I thought I should elaborate on disjunction a little.

Closing this since the output in the current version seems to match your expectations. Feel free to re-open if needed.

[rindPHI]

ISLa 1.11.0 is now on PyPI.

[mojung]

Hi Dominic,

Thanks for the fix! enforce_unique_trees_in_queue=False seems to do the trick. :relaxed: