Skip to content

Latest commit

 

History

History
66 lines (47 loc) · 1.59 KB

CHANGELOG.md

File metadata and controls

66 lines (47 loc) · 1.59 KB
Raw

Change Log

0.6.1

  • fixes: format error, compat with containers 2.7

0.6

  • upgrade to msat 0.8
  • upgrade to tip-parser 0.6
  • remove some dead code
  • make tests faster (timeout=10)
  • use release mode

0.5

  • fix(model): add a constant to unin types with empty domains

  • adapt to tip-parser 0.5

  • handle new Stmt_prove from TIP

  • cleaner display of result in presence of progress bar

  • add default case in match (makes smaller terms)

  • display theorem/countersat if the goal is a prove goal

  • refactor a bit AST

  • add travis support

  • modernize metatada: opam2 and dune

0.4.2

  • support containers 2.0
  • move to jbuilder
  • small optims
  • add option --eval-under-quant
  • more stats

0.4.1

  • bugfix related to De Bruijn indices and function extensionality

0.4

  • quantification on datatypes/bool

  • remove limited checking of models

  • some bugfixes and regression tests

0.3.1

  • compatibility with containers 1.0

0.3

  • add flag --check-proof for checking SAT solver proofs
  • remove parser for custom format; only keep TIP; remove .lisp from tests
  • less accurate detection of incomplete expansions (without unsat-cores)
  • bugfixes in uninterpreted types
  • detect some evaluation loops with a term_being_evaled field
  • internal notion of undefined for asserting, loops, and selectors
  • simple prefix skolemization for assert axioms
  • add asserting construct
  • delay a bit combinatorial explosion for HO functions
  • support for HO unknowns
  • allow quantification over booleans, translated as conjunction/disjunction
  • better error message for HO metas
  • add support for selectors