RecursionError when using an implication in forall

[leonbett]

Describe the bug A RecursionError occurs when using an implication in a forall scope: RecursionError: maximum recursion depth exceeded in comparison

To Reproduce

from isla.solver import ISLaSolver

grammar = '''
<start> ::= <list> 
<list>  ::= <item> | <item> <list>
<item> ::= "(" <type> "," <digit> ")"
<type> ::= "A"
<digit> ::= "1" | "2"
'''

constraint = """
forall <item> item="({<type> type},{<digit> digit})" in start:
  (
    ((type = "A") implies (digit = "1"))
  )
"""

solver = ISLaSolver(
    grammar=grammar,
    formula=constraint)

for _ in range(100):
    print(solver.solve())

Expected behavior The constraint should be satisfiable and the output should be: [(A,1)]+

System/Installation Specs:

• ISLa Version: 1.10.0
• Python Version: 3.11.1
• OS: macOS

Additional context The expected behavior is observed for the following (equivalent) constraint:

constraint = """
forall <item> item="({<type> type},{<digit> digit})" in start:
  (
    (digit = "1")
  )
"""

[rindPHI]

Sorry for the late reply.

The issue can be circumvented by constructing the solver like this:

solver = ISLaSolver(
    grammar=grammar,
    formula=constraint,
    enforce_unique_trees_in_queue=False,
)

The problem is that an implication (i.e., a disjunction with negated first element) yields two states with the same derivation tree since ISLa splits disjunctions. Per default, however, ISLa drops states if another state with the same derivation tree already exists in the queue. In certain cases this leads to better performance. In other cases, however, this behavior must be disabled. I'm currently considering to change the default....

The nontermination issue, by the way, results from the first part of the disjunction (not type = "A") being unsatisfiable and the other one discarded.

Interestingly, the flag activate_unsat_support=True also fixes the issue (as an alternative to enforce_unique_trees_in_queue). This is always a nice one to try out when something doesn't terminate :smile:

[rindPHI]

I changed the default in ISLa 1.11.0 (https://github.com/rindPHI/isla/pull/58/commits/61c0f5057f8e80543e9bec5db74492859c51bc0f). If the current build succeeds, I will publish the change in 1.11.0 to PyPI.

Closing this :)

[rindPHI]

ISLa 1.11.0 is now on PyPI.