This release of Ethos is associated with the 1.3.4 release of the SMT solver cvc5.
- The command
declare-parameterized-constnow forbids return types that contain parameters with non-ground type. - Updates to the external plugin interface.
- The identifier
Typeis no longer treated as a keyword in proofs and reference files. - The command
declare-sortis now allowed in proof files. - The builtin
eo::to_strno longer prints rationals, decimals, or bitvectors. It now only evaluates on strings and numeral code points. - Adds support for an attribute
:is_eqto test whether a defined term is equal to another. - Fixes a bug where the character code point
\u{30000}was incorrectly
treated as a valid code point. - Fixes issue in the parser which did not guard for overflow of 32 bit unsigned
values. - Fixes an issue where non-ground nil terminators would not be properly computed for list construction operators with types where the element type is different from the return type of the operator.
- Fixes for evaluation of
:left-assoc-niland:left-assoc-non-singleton-niloperators. - Variables
(eo::var s T)are now considered ordinary terms, which are hence allowed in patterns. - Fixes the implementation of
eo::list_minclude, which had considered the arguments in opposite order.