package smbc

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