isla

isla copied to clipboard

[FEATURE] Discussion: Compatibility with "theory of fixed size bit-vectors"

1

In order to model constraints imposed by general purpose programs, the operations used in the program have to be translated to an ISLa constraint. Currently, ISLa supports some arithmetic operations...

leonbett

[BUG] Solving arithmetic constraints takes very long

6

**Describe the bug** ISLa takes a long time (~3-5 minutes) to solve a formula with many arithmetic constraints. **To Reproduce** 0. Two fixes probably need to be applied to ISLa...

leonbett

[BUG] Correct result with infix AND, incorrect result with s-expr AND

1

**Describe the bug** Sometimes ISLa only produces a correct result for infix AND, but not for S-expr AND. It seems like the S-expr AND constraint is completely ignored. **To Reproduce**...

leonbett

**Is your feature request related to a problem? Please describe.** [timeout_ms](https://github.com/rindPHI/isla/blob/main/src/isla/z3_helpers.py#L556) is set to 500 ms by default, and cannot be configured by a user, if I understand correctly. **Describe...

leonbett

[FEATURE] Language syntax wishlist

1

- Unary minus would be cool. Currently, instead of writing `-48`, I use `(0 - 48)`. - For Infix-notation, could we have `%` and `/` operators instead of `mod` and...

leonbett

**Description** When trying to parse the formula below (see code snippet), ISLa raises a SyntaxError. Using full paths instead of shortened ones resolves the issue, although ISLa displays a warning...

mojung

**Describe the bug** The solver does not output solutions for a particular class of constraints such as in the following example: ```python grammar = { "": ["$"], "": [""], "":...

rindPHI

The formula ``` forall ref in start: exists lpar in start: ref. = lpar.. and forall fref in start: exists lpar in start: fref. = lpar.. ``` cannot be parsed...

rindPHI

failure when trying to parse expressions containing nested `and`-`not` in prefix notation

1

Here is a file reproducing the problem: ```Python # isla_and_not.py from isla.language import parse_isla if __name__ == "__main__": parse_isla('(and (= "a") (= "b"))') # no not -> ok parse_isla('(not (=...

michaelmera

inconsistent result for evaluate()/solve() when changing order of variables and constants in (+) operands

1

Here is a file reproducing the problem. It does two times the same computation, just inverting the order of the operands of `(+)`: ```Python # isla_add_order.py from isla.type_defs import Grammar...

michaelmera