Skip to content

Latest commit

 

History

History
39 lines (26 loc) · 2.95 KB

NEWS.md

File metadata and controls

39 lines (26 loc) · 2.95 KB

This file contains a summary of important user-visible changes.

ethos 0.1.2 prerelease

  • Adds support for the SMT-LIB as annotations for ambiguous datatype constructors, i.e. those whose return type cannot be inferred from its argument types. Following SMT-LIB convention, ambiguous datatype constructors are expected to be annotated with their return type using as, which internally is treated as a type argument to the constructor.
  • The semantics for eo::dt_constructors is extended for instantiated parametric datatypes. For example calling eo::dt_constructors on (List Int) returns the list containing cons and (as nil (List Int)).
  • The semantics for eo::dt_selectors is extended for annotated constructors. For example calling eo::dt_selectors on (as nil (List Int)) returns the empty list.

ethos 0.1.1

This release of Ethos is associated with the 1.2.1 release of the SMT solver cvc5.

  • When parsing Eunoia signatures, decimals and hexidecimals are never normalized, variables in binders are always unique for their name and type, and let is never treated as a builtin way of specifying macros. The options --no-normalize-dec, --no-normalize-hex, --binder-fresh, and --no-parse-let now only apply when parsing proofs and reference files.
  • Adds a new option --normalize-num, which also only applies when reference parsing. This option treats numerals as rationals, which can be used when parsing SMT-LIB inputs in logics where numerals are shorthand for rationals.
  • Makes the set-option command available in proofs and Eunoia files.
  • Adds --include=X and --reference=X to the command line interface for including (reference) files.
  • Fixed the disambiguation of overloaded symbols that are not applied to arguments.
  • Fixed the interpretation of operators that combine opaque and ordinary arguments.
  • Fixed a bug in the evaluation of eo::cons for left associative operators, which would construct erroneous terms.
  • Adds support for eo::dt_constructors which returns the list of constructors associated with a datatype, and eo::dt_selectors which returns the list of selectors associated with a datatype constructor. These operators make use of a type eo::List, which is now part of the background signature assumed by Ethos.
  • Fixed parser for the singleton case of declare-datatype.

ethos 0.1.0

This is the initial release of the Ethos proof checker. Ethos implements the Eunoia logical framework which is a logical framework targeted at SMT solvers. It allows users to define proof formats and write proofs.

This release of Ethos is associated with the 1.2.0 release of the SMT solver cvc5. It can check the proofs generated by cvc5's native proof format cpc. Ethos and Eunoia have reached a certain level of stability, but they are still under active development.

Development Repository

https://github.com/cvc5/ethos

Documentation

https://github.com/cvc5/ethos/blob/main/user_manual.md