package msat

CHANGES

0.9.1

• add on_conflit callback
• fix termination issue when using push_decision_lit from plugin

0.9

• feat: allow the theory to ask for some literals to be decided on
• feat: allow to set the default polarity of variables at creation time

0.8.3

• support containers 3.0

0.8.2

• fix opam file
• fix: allow conflicts below decision level in Make_cdcl_t

0.8.1

• fixes in Heap
• package for msat-bin
• use iter instead of sequence in dune and opam files
• more docs

0.8

big refactoring, change of API with fewer functions, etc. see git log for more details.

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