smbc

Experimental model finder/SMT solver for functional programming

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