Skip to content

0.10

Latest
Compare
Choose a tag to compare
@Gbury Gbury released this 17 Jun 12:51
· 4 commits to master since this release

CHANGES:

UI

  • Improved the printing of some data-structures (PR#190)

Std

  • Replace the Plain statement with the Other statement,
    which is a more general version (PR#190)

Parsing

  • Treat quoted symbols from the stdlib as symbols, regardless of
    their contents. Previously a |assert| would be understood as the
    reserved work assert, allowing e.g. (|assert| false). From now on
    these are understood as symbols, so one can (declare |assert| () Bool)
    (PR#198)
  • Add parsing extensions for the smtlib2 language (PR#190, PR#194)
  • Better split elements of clauses in cnf TPTP statements (PR#190)
  • Ensure illegal chars raise the correct error during lexing
    (Issue#191, PR#192)

Printing

  • Add printers for smtlib identifiers (PR#198)
  • Printing of typed expressions (i.e. the Std.Expr module)
    can now print the tags (PR#210)

Typing

  • Enforce some missing constraints on bitvectors
    indexes and sizes for the smtlib2 BV theory (PR#172, PR#175)
  • Slightly improve wording for errors and warnings concerning
    non linearity and other arithmetic restrictions (PR#184)
  • More information for reserved Id, resulting in more precise
    errors when smt2 scripts use reserved ids (PR#193)
  • Expose implicit declarations/definitions that happen during
    typechecking (PR#199)
  • Treat smtlib :named annotations as implicit definitions as
    required by the spec (PR#199)
  • Add a warning for unknown attributes in smtlib2. This replaces
    the unbound id error that some files could raise before when
    using non-standard attribtues (PR#207)
  • Only type annotations on quantified formulas and binders once.
    Previously, these were typed twice so that they can be attached to
    both the body of the bound formula and the quantified formula itself.
    (PR#207, PR#210)

Loop

  • Add the String theory to the ALL logic of smtlib2 (PR#182)