# CHANGES

## 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