[BUG] Runtime differences between equivalent constraints

[ju-klein]

Describe the bug: The solver can solve not (a or b) within five minutes. The solver cannot solve not a and not b within five minutes. I have not tested if it terminates.

To reproduce: Create a constraint

exists a:
exists b:
((not inside(a, b)) and (not inside(b,a))) 

does not terminate at all or takes long.

Use the equivalence

exists <something> a in <somewhere>:
exists <something> b in <somewhere>:
(not (inside(a,b) or inside(b,a)))

and it terminates rather quickly.

Expected behavior: Not sure if this is intended behavior, but I would think that both versions should take the same time.

System/Installation Specs:

• ISLa Version: ISLa-solver 1.14.1
• Python Version: 3.12
• OS: Linux 6.7.0-arch3-1 #1 SMP PREEMPT_DYNAMIC Sat, 13 Jan 2024 14:37:14 +0000 x86_64 GNU/Linux

[rindPHI]

Thanks for the report.

Could you please provide a small but complete example, including a grammar and parseable ISLa constraints with concrete nonterminal symbols? This will help me tremendously in addressing the issue.

[ju-klein]

Probably, but I have to wait until next Monday. This is from an exercise that is due on Sunday.