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