CHANGES

0.6.1

add simple functor for DOT backend
various bugfixes

0.6

Feature

An already instantiated sat solver in the Sat module
A full_slice function for running possibly expensive satisfiability tests (in SMT) when a propositional model has been found
Forgetful propagations: propagations whose reason (i.e clause) is not watched

0.5.1

Bug

Removed some needless allocations

Breaking

Better interface for mcsat propagations

Feature

Allow level 0 semantic propagations

0.5

Bug

Grow heap when adding local hyps
Avoid forgetting some one atom clauses
Fixed a bug for propagations at level 0
Late propagations need to be re-propagated
Fixed conflict at level 0
Avoid forgetting some theory conflict clauses

Breaking

Changed if_sat interface

0.4.1

Bug

fix bug in add_clause

0.4

performance improvements
many bugfixes
more tests

Breaking

remove push/pop (source of many bugs)
replaced by solve : assumptions:lit list -> unit -> result

Features

Accept late conflict clauses
cleaner API, moving some types outside the client-required interface

0.3

Features

Proofs for atoms at level 0
Compatibility with ocaml >= 4.00
Released some restrictions on dummy sat theories

0.2

Breaking

Log argument has been removed from functors
All the functors now take a dummy last argument to ensure the solver modules are unique

Features

push/pop operations
access to decision level when evaluating literals