package mc2

  1. Overview
  2. Docs
A mcsat-based SMT solver in pure OCaml

Install

Dune Dependency

Authors

Maintainers

Sources

v0.1.tar.gz
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 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