You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
New optimization in SMT formula solving: Variables exclusively occurring in str.to.int contexts are passed to Z3 as integers and later converted to strings,
which reduces the solver's load.
Cleaned up / improved code corresponding to SMT formula solving optimizations.
[1.11.0] - 2023-03-22
Changed
The default for the ISLaSolver parameter enforce_unique_trees_in_queue changed
from True to False. The old setting could improve performance if the same
derivation tree can be generated by expansion and tree insertion (and similar cases),
but can have very unpleasant side effects, e.g., in the presence of disjunctions (see
GitHub Issue 53). If you encounter negative performance effects in your existing
use cases, consider setting this flag to True when creating the ISLaSolver.
[1.10.4] - 2023-03-15
Changed
Solved parser problem: Arithmetic differences (a = b - c) not parsed correctly
before.
Eliminated bug in solver: If an explicit start symbol was given, the given grammar
was mutated. Solver invocations (including the constructor) should, however, not
have such side effects. In fact, that problem rendered the test suite flaky.
delete_unreachable (which deletes unreachable nonterminal keys in a grammar) no
longer mutates grammars, but instead returns a new grammar.