v1.3.0

Expects mata v1.6.9

What's Changed

• New length-based decision procedure for handling special equations with lengths (enabled by default, can be turned off with str.try_length_proc=false)
• New decision procedure for handling not-contains and disequations based on counting automata (disabled by default, can be enabled with str.ca_constr=true)
• Z3-Noodler can now produce models
• Minor bug fixes in axiomatizations for replace_re, prefix, suffix, and string-integer conversions

Full Changelog: v1.2.0...v1.3.0

v1.2.0

Expects mata v1.2.4

What's Changed

• Update base Z3 to v4.13.0 by @jurajsic in #133
• Regex construction: optimizations by @vhavlena in #134
• Nielsen optimizations by @vhavlena in #136
• Reenable rewriter rule (str.in A (str.to_re B)) -> (A = B) by @jurajsic in #137
• Multiple regex membership heuristic by @jurajsic in #139
• Fixing infinite looping by @vhavlena in #140
• Fix invalid link to SMTLIB theory of strings by @Adda0 in #141
• Add support for QF_SNIA by @jurajsic in #144
• Multiple membership heuristic improvement by @jurajsic in #145

Full Changelog: v1.1.0...v1.2.0

Z3-Noodler-v1.1.0

What's Changed

• Small refactoring of final_check by @vhavlena in #105
• Update README by @jurajsic in #108
• Add support for replace_re by @jurajsic in #102
• Optimizations for hard equations by @vhavlena in #103
• Support for str.< and str.<= by @vhavlena in #109
• Pyex: optimizations by @vhavlena in #104
• Bug fix after merge by @vhavlena in #110
• Turn on reduction for noodlification by @jurajsic in #107
• Tests fixing by @vhavlena in #111
• An optimisation of underapproximation by @vhavlena in #112
• Pyex Optimisations Iteration 2 by @vhavlena in #113
• Handling of from_int and to_int by @jurajsic in #114
• to_int/from_int optimization by @jurajsic in #116
• Underapproximating to_int/from_int by @jurajsic in #117
• Fixing errors by @vhavlena in #115
• Optimizations of full_str_int by @vhavlena in #118
• to_int: axioms for number equations by @vhavlena in #124
• Length based conversion encoding of int conversions by @jurajsic in #121
• Less underapproximating int conversions by @jurajsic in #125
• Reenable str.in_re rewrite rule by @jurajsic in #126
• Update instructions to install Mata to use 'sudo' by @Adda0 in #128
• Solver extension to handle underapproximation by @vhavlena in #129
• Warn about checking include paths by @Adda0 in #130
• Fix to_int computation so invalid cases are not used to generate numbers by @jurajsic in #132

Full Changelog: v1.0.0...v1.1.0

Z3-Noodler-v1.0.0

Initial main release of Z3-Noodler. Needs version 0.109.0 of Mata.