ISLa 1.14.1

[1.14.1] - 2023-07-10

Changed

• Supporting literal negative numbers in ISLa constraints (concrete syntax), such as in
  str.to.int(<int>) < -1. This raised a SyntaxError before.

ISLa 1.14.0

[1.14.0] - 2023-07-05

Changed

• Improved optimized handling of str.to.int (when enable_optimized_z3_queries is
  enabled). For variables exclusively appearing in str.to.int, we support a wider
  range of possible solutions, such as negative numbers or languages with an optional
  + or padding of zeroes in front. Furthermore, ISLa tries to infer the domains of
  these variables automatically, e.g., to exclude "0" or negative values.

ISLa 1.13.9

[1.13.9] - 2023-04-27

Changed

• Bug fix to HUGE unsoundness: Solver returned a solution for "false" constraint.

[1.13.8] - 2023-04-27

Changed

• Fixed a parser bug occurring when a conjunctive formula contains two independent sets
  of XPath expressions. Previously, the produced quantifiers were nested, which is
  incorrect. Now, they're "pushed in" as expected.
• Fixed a bug in isla.solver.subtree_solutions surfacing for the reST example when
  a subtree gets substituted by a smaller subtree produced by a semantic predicate
  (in that case, extend_crop).

[1.13.7] - 2023-04-26

Changed

• Bug fix: When solving SMT formulas with multiple independent clusters, an exponential
  number of solutions was pre-computed (many more than asked for), which resulted in
  a potentially huge performance problem.

[1.13.6] - 2023-04-26

Changed

• Bug fix for parsing a formula where two XPath expressions are appended to the same
  bound variable, and one of the possible expansions that can be chosen cannot be
  merged.

[1.13.5] - 2023-04-26

Changed

• Introducing a global configuration module global_config.py. Currently, this contains
  a flag for disabling assertions guarded by assertions_activated(), which are many
  of the more costly assertions. This flag is an opportunity to programmatically turn
  off at least some assertions if setting the global -O flag is not an option.
• Suppressing potentially meaningless error messages issued during the procedure
  implemented in 1.13.4.

[1.13.4] - 2023-04-26

Changed

• Fixed bug concerning numeric solutions to SMT formulas with "padded" variables:
  only "01," e.g., is a valid solution, not "1."

[1.13.3] - 2023-04-17

Changed

• Fix to partial last bug fix.

[1.13.2] - 2023-04-17

Changed

• Fixed unparsing of null byte unicode literal: Got "\u{}" before (which could not be
  parsed by Z3!), now obtain the correct "\u{0}".

[1.13.1] - 2023-04-06

Changed

• BugFix in ISLaSolver.eliminate_all_ready_semantic_predicate_formulas: Subtrees in
  computed substitutions are now considered (as they were already for SMT formulas).
• When defining a new semantic predicate, an order parameter can be set that
  specifies when a semantic predicate is evaluated relatively to the other semantic
  predicates.

[1.13.0] - 2023-04-06

Changed

• Refactoring & optimization in implementation of count semantic predicate. We now
  select candidates with larger numbers of <needle> occurrences first.
• Optimization in ISLaSolver.extract_regular_expression: Better re-use of already
  computed regexes for frequently re-used nonterminals (such like <byte>)

[1.12.0] - 2023-04-06

Changed

• Change in the implementation of the count predicate: We now only ask for one tree
  insertion solution. This increases efficiency in our examples (before, we asked for
  50 insertion solutions). Yet, it is not entirely certain if this step might cause
  prolems in more complex examples.

ISLa 1.11.2

[1.11.2] - 2023-04-04

Changed

• Worked on documentation; now available on https://isla.readthedocs.io/.

[1.11.1] - 2023-03-24

Changed

• 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.

ISLa 1.10.3

[1.10.3] - 2023-03-09

Changed

• Upgrade to ANTLR 4.12.0

[1.10.2] - 2023-03-09

Changed

• The BNF parser now handles XML-like terminals (e.g., "<a>") that are no longer
  treated as nonterminal symbols. We introduce a fresh nonterminal "<langle>"
  ("<langle_i>" for smallest possible i if the other alternative(s) are not free)
  expanding to "<" and replace "<" in terminals with that nonterminal in the
  resulting Python grammar.

ISLa 1.10.1

[1.10.1] - 2022-01-10

Changed

• Deterministic hashing of structural predicates.
• Fixed too aggressive simplification of existential quantifiers (see test
  test_subsitute_in_existential_formula in test_language.py).
• Fixed too aggressive simplification of universal quantifiers for recursive grammars:
  even if a quantifier already matched a tree node, we cannot simplify it away in the
  absence of other current matches if the quantified nonterminal can still be reached
  from the already mached tree.
• Deactivated custom solver for str.len in presence of "too concrete" tree
  substitutions, e.g., a str.len(<chars>) < 10 constraint with a <char><char> tree,
  where 2 is the only possible instantiation of str.len.

ISLa 1.10.0

[1.10.0] - 2022-01-05

Changed

• Resolves GitHub Issue #36, which in
  essence refers to solving multiple "conflicting" SMT formulas. These are formulas
  whose solutions change subtrees of substitutions in other SMT formulas. Before,
  we did not check that the chosen "priority" formulas are not themselves influenced
  by other formulas. See test case test_issue_36 in test_solver.py.
• Resolves GitHub Issue #39. The count
  predicate now better handles grammars with epsilon productions: If the number of
  "needles" is already reached, it can "finish off" the remaining nonterminals that
  might be instantiated with needle nonterminals if alternative instantiations are
  available.
• Adds the feature requested in GitHub Issue #38:
  one can now pass a start symbol (parameter start_symbol) to the ISLaSolver
  constructor as alternative to the (also optional) initial derivation tree.
• Resolves GitHub Issue #40. The default
  value for formula in ISLaSolver is now None and no longer "true", with the
  same semantics. This means that you can still pass Formula objects and strings,
  but additionally None for the trivially valid constraint.

[1.9.9] - 2022-12-22

Changed

• Improved DerivationTree.to_dot(): Now, nodes at same levels appear at the same
  levels, and the horizontal order of child nodes is retained.

ISLa 1.9.8

[1.9.8] - 2022-12-20

Changed

• Fixed "build" shield in README.md
• Changed computation of symbol costs in solver; now computed statically from grammar
  graph, not using fuzzer.

[1.9.7] - 2022-12-16

Changed

• Fix in performance evaluator; improves output, where an error (w/o consequences) was
  shown in case of an intentional timeout. Now, the solvers terminate silently after
  the set timeout.
• Small performance improvements in establishing normal form, computing potential
  matches, and performing substitutions in SMT formulas.

ISLa 1.9.6

[1.9.6] - 2022-12-15

Changed

• Fixed hashing in call to solver.is_valid_combination
• Performance improvements, mainly by avoiding replace_formula for top-level formulas
  (performing shallow replace instead) and re-using the same objects for atomic SMT
  formulas.

ISLa 1.9.5

[1.9.5] - 2022-11-21

Changed

• Bug fix in optimized solution of length constraints: (1) Preventing infinite loop for
  unsolvable constraints (e.g., zero length for non-nullable nonterminal), (2)
  preventing solver from trying to produce strings with negative lengths.

[1.9.4] - 2022-11-13

Changed

• Can use Unicode symbols like "\x01" in the nonprintable range in BNF grammars (parsing
  and unparsing now works for these symbols).