Experimental model finder/SMT solver for functional programming


  • fixes: format error, compat with containers 2.7


  • upgrade to msat 0.8

  • upgrade to tip-parser 0.6

  • remove some dead code

  • make tests faster (timeout=10)

  • use release mode


  • 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


  • support containers 2.0

  • move to jbuilder

  • small optims

  • add option --eval-under-quant

  • more stats


  • bugfix related to De Bruijn indices and function extensionality


  • quantification on datatypes/bool

  • remove limited checking of models

  • some bugfixes and regression tests


  • compatibility with containers 1.0


  • 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