package msat
Install
Dune Dependency
Authors
Maintainers
Sources
md5=ba623630b0b8e0edc016079dd214c80b
sha512=51c133cefe8550125e7b1db18549e893bac15663fdd7a9fac87235c07de755f39eab9fc3cfdf6571612fd79b3d5b22f49f459581b480c7349bacddf2618c8a99
CHANGELOG.md.html
CHANGES
0.9.1
add
on_conflit
callbackfix 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 ofsequence
in dune and opam filesmore 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 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