package mc2
Install
Dune Dependency
Authors
Maintainers
Sources
md5=92de696251ec76fbf3eba6ee917fd80f
sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0
CHANGELOG.md.html
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 foundForgetful 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