From dde54d2ea9a8ec9fae85da865780aff5d45f9539 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 24 Jan 2017 11:28:40 +0100 Subject: [PATCH] [changes] Added changelog --- CHANGELOG.md | 86 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 CHANGELOG.md diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 00000000..e2902eb6 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,86 @@ +# CHANGES + +## Unreleased + + + +## 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 +