package msat

  1. Overview
  2. Docs
Library containing a SAT solver that can be parametrized by a theory

Install

Dune Dependency

Authors

Maintainers

Sources

v0.9.1.tar.gz
md5=ba623630b0b8e0edc016079dd214c80b
sha512=51c133cefe8550125e7b1db18549e893bac15663fdd7a9fac87235c07de755f39eab9fc3cfdf6571612fd79b3d5b22f49f459581b480c7349bacddf2618c8a99

CHANGELOG.md.html

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