2.6.0 Release

What's Changed

• Parametric Sort by @Shoooooon in #111
• ArraysEx and Parametric Sorts in Function Ranks by @kjcjohnson in #112
• Support "intrinsic" declarations by @kjcjohnson in #114
• Add option to disable legacy symbols in CHC JSON events by @kjcjohnson in #115
• Add the (experimental cvc5) theory of sequences by @kjcjohnson in #116
• Add option for term annotations in s-expression format by @kjcjohnson in #118

New Contributors

• @Shoooooon made their first contribution in #111

Full Changelog: v2.5.0...v2.6.0

2.6.0 Preview 3

What's Changed

• Parametric Sort by @Shoooooon in #111
• ArraysEx and Parametric Sorts in Function Ranks by @kjcjohnson in #112
• Support "intrinsic" declarations by @kjcjohnson in #114
• Add option to disable legacy symbols in CHC JSON events by @kjcjohnson in #115
• Add the (experimental cvc5) theory of sequences by @kjcjohnson in #116
• Add option for term annotations in s-expression format by @kjcjohnson in #118

New Contributors

• @Shoooooon made their first contribution in #111

Full Changelog: v2.5.0...v2.6.0-preview3

2.6.0 Preview 2

What's Changed

• Parametric Sort by @Shoooooon in #111
• ArraysEx and Parametric Sorts in Function Ranks by @kjcjohnson in #112
• Support "intrinsic" declarations by @kjcjohnson in #114
• Add option to disable legacy symbols in CHC JSON events by @kjcjohnson in #115
• Add the (experimental cvc5) theory of sequences by @kjcjohnson in #116

New Contributors

• @Shoooooon made their first contribution in #111

Full Changelog: v2.5.0...v2.6.0-preview2

2.6.0 Preview 1

What's Changed

• Parametric Sort by @Shoooooon in #111
• ArraysEx and Parametric Sorts in Function Ranks by @kjcjohnson in #112
• Support "intrinsic" declarations by @kjcjohnson in #114

New Contributors

• @Shoooooon made their first contribution in #111

Full Changelog: v2.5.0...v2.6.0-preview1

2.5.0 Release

Highlights

• CHCs now have IDs!
• More extended bitvector functions!

What's Changed

• Add IDs to CHCs by @kjcjohnson in #104
• Move BV extensions by @kjcjohnson in #106

Full Changelog: v2.4.1...v2.5.0

2.5.0 Preview 1

What's Changed

• More BV extensions by @rahulk64 in #106

Note

CHC ids from v2.4.2 Preview 1 are included in this preview, as it was decided it was a breaking change worthy of a minor version increment.

Full Changelog: v2.4.2-preview1...v2.5.0-preview1

2.4.2 Preview 1

CHC IDs

This release adds unique IDs to each CHC, so that they can be processed and matched back to the original CHCs in other tooling.

What's Changed

• Add IDs to CHCs by @kjcjohnson in #104

Full Changelog: v2.4.1...v2.4.2-preview1

2.4.1 Release

set-info fix for S-expression format

Previously, the S-expression output format would not include the value of attributes from set-info commands. These values are now included.

What's Changed

• Fix sexpr set-info handling (and add tests) by @kjcjohnson in #102

Full Changelog: v2.4.0...v2.4.1

2.4.0 Release

New CHC Symbol Table

Previously, the chc events output a list of input variables, output variables, and just "variables". This had some problems, for example:

• The term variable wasn't present anywhere other than the CHC head signature (#93)
• Auxiliary variables weren't tracked separately, so it wasn't possible to distinguish cases where auxiliary variables shadowed input or outputs
• Variables were not typed, so gymnastics were required to re-generate SMT expressions from the parser output
  and more.

With v2.4.0, we're now generating a symbol table data structure that discretely tracks all the variable information.

What's Changed

• CHC symbol tables by @kjcjohnson in #96
• Add unclassified symbols to symbol table by @kjcjohnson in #97
• Update action versions by @kjcjohnson in #98

Full Changelog: v2.3.0...v2.4.0

2.4.0 Preview 1

New CHC Symbol Table

Previously, the chc events output a list of input variables, output variables, and just "variables". This had some problems, for example:

• The term variable wasn't present anywhere other than the CHC head signature (#93)
• Auxiliary variables weren't tracked separately, so it wasn't possible to distinguish cases where auxiliary variables shadowed input or outputs
• Variables were not typed, so gymnastics were required to re-generate SMT expressions from the parser output
  and more.

With v2.4.0, we're now generating a symbol table data structure that discretely tracks all the variable information.

What's Changed

• CHC symbol tables by @kjcjohnson in #96

Full Changelog: v2.3.0...v2.4.0-preview1