isla
isla copied to clipboard
rindPHI
The ISLa (Input Specification Language) language & solver.
An alternative way to solve ISLa constraints following a "fuzz'n'repair" approach.
**Describe the bug** Some seemingly innocuous ISLa formulas with XPath-style shortcuts don't parse. **To Reproduce** Consider the following code: ```python from isla import __version__ from isla.solver import ISLaSolver print(__version__) #...
**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...
Implement solving SMT formulas by grammatical case distinction: A predicate holds iff it holds for all direct children of an involved variable. Several issues need to be resolved for this,...
Many problems in ISLa's frontend parser (e.g., #3, #72) originate in the mixture of S-expressions and "mathematical" syntax in ISLa's concrete syntax. Supporting both correctly is difficult; the necessity of...
The queue-based approach with the highly problem-specific cost function is a central pain point in the ISLa solver. It might be the most significant performance barrier in ISLa. The old...
The ISLa 2.0 syntax should support higher-order functions such as `num( v; P(v))` and `sum( v; P(v); t(v))`, so that we can write ``` num( b; inside(b, )) < 40...
**Describe the bug** When solving a complex XPath expression of the form x..y..z, ISLa raises an AssertionError. **To Reproduce** Use `str.len(....) = 10` or similar as constraint. The result is...
In an error message, `ISLaSolver.check()` reports "" as start symbol, although a different start symbol was given as constructor. **To Reproduce** In the context ``` digit_solver = ISLaSolver(EXPR_GRAMMAR, start_symbol='') str(digit_solver.solve())...