Completeness bug: Solver does not terminate for forall-exists formula with recursive bound variable types

[rindPHI]

Describe the bug

The solver does not output solutions for a particular class of constraints such as in the following example:

grammar = {
    "<start>": ["<E>$"],
    "<E>": ["<T><EE>"],
    "<EE>": ["+<T><EE>", ""],
    "<T>": ["<F><TT>"],
    "<TT>": ["*<F><TT>", ""],
    "<F>": ["(<E>)", "a", "b", "c", "d", "e", "f", "g"],
}

inside_test = """
forall <F> f2 in start:
exists <F> f1="({<E> e})" in start:
(not (= f2 "a") or not inside(f2, e))"""

solver = ISLaSolver(
    grammar, inside_test, structural_predicates={IN_TREE_PREDICATE}
)

# Here are some examples of passing and failing inputs
# print(solver.parse("(e)$").to_parse_tree())  # Passes
# print(solver.parse("(e)+(a)$").to_parse_tree())  # Passes
# print(solver.parse("(a)+(a)$").to_parse_tree())  # Passes
# print(solver.parse("(a)$").to_parse_tree())  # Fails

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

See (inactive) test case Xtest_negated_constraint in test_solver.py (should soon be on the master branch).

The problem probably is rooted in tree insertion.

Expected behavior

We want some outputs such as the ones in the comments above.

System/Installation Specs:

• ISLa Version: 1.10.0