From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 85D2C7FCE9 for ; Fri, 27 Jan 2017 11:01:37 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=me+caml-list@gbury.eu; spf=Pass smtp.mailfrom=me+caml-list@gbury.eu; spf=None smtp.helo=postmaster@mail2.gbury.eu Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of me+caml-list@gbury.eu) identity=pra; client-ip=5.9.79.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="me+caml-list@gbury.eu"; x-sender="me+caml-list@gbury.eu"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of me+caml-list@gbury.eu designates 5.9.79.155 as permitted sender) identity=mailfrom; client-ip=5.9.79.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="me+caml-list@gbury.eu"; x-sender="me+caml-list@gbury.eu"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail2.gbury.eu) identity=helo; client-ip=5.9.79.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="me+caml-list@gbury.eu"; x-sender="postmaster@mail2.gbury.eu"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AF7BPix+IWrggAf9uRHKM819IXTAuvvDOBiVQ1KB4?= =?us-ascii?q?2+IcTK2v8tzYMVDF4r011RmSDNmdtq0P07eempujcFRI2YyGvnEGfc4EfD4+ou?= =?us-ascii?q?JSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgpp?= =?us-ascii?q?POT1HZPZg9iq2+yo9ZDeZwpFiCC9bL5wIxm6sQXcvdQKjIV/Lao81gHHqWZSde?= =?us-ascii?q?RMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZ?= =?us-ascii?q?TQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhz?= =?us-ascii?q?odNzMh8G/Zl9J+gqFVrh2vqBNw34HabZqJNPd8ZK7RYc8WSGRDU8tXSidPApm8?= =?us-ascii?q?b4wKD+cZPOhYsoj9p18KrRSkGAmsAf3gwSJVi3/rx6070/kqHAbD3AM+GN4BrG?= =?us-ascii?q?7brNDxNKsLVeC1zbLIzSnYYvNZwjj99ZLIcxA7rf6SQLJ9aMzcwlQhGQPCi1Wf?= =?us-ascii?q?s43lPzWN2+QCsmib8+pgVf+0hGI9qgFxpSCjxsgtionVhoIV10vL+T9lz4YyIN?= =?us-ascii?q?20UEp7YcSlEJdKuSGaLY17Sd4hTWFwoCs3yqcKtJqhcCUIzJkr3QPTZvyHfoSQ?= =?us-ascii?q?4R/vSvydLSl4iX9rYr6zmgi+/Em6xuHiWMS4zVBHpTdfnNbWrHACzRnT59CHSv?= =?us-ascii?q?Rj+keh3i6C1wXJ5eFFJUA4i7DXK5E6zb4tjJoSsV7PETHrmEnuja+WcFsr+vSw?= =?us-ascii?q?5unneLnrooWQOo1whw3kL6gjmsyyDfw9MgcUXmib/eq81Kfk/U38WLhKi+M5nq?= =?us-ascii?q?7Fv5/AIMQbore1AwtU0oY49xayFDim388FnXkdLFNJYgyIj5XxN1HUPP/4Feu/?= =?us-ascii?q?g0irkDpz2//JJLjhApHUInjHkbfhZqp95lVHyAszyNBf/4hbBqsAIPL1QE/xtc?= =?us-ascii?q?bXAgU3MwyukK7bD4B234YaHGaOGbOxMaXIsFbO6Ph8DfOLYdo6pTf5L/E44vOm?= =?us-ascii?q?p2IjiBdJeKTq1pISbDW8H+96C0qTfGD9xNocRzRZ9jEiRfDn3QXRGQVYYGy/Cv?= =?us-ascii?q?ox?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DZBAAJGotY/5tPCQVdSAYMgwsBAQEBA?= =?us-ascii?q?YEAAyeENIp7qEkmhgaCbhUBAQEBAQEBAQEBAWEogjMZgkeBCwImAmwIAQGJYQq?= =?us-ascii?q?dRZABgiWLI4ELhE+Cdod/gjqCXwWJCZJIhmeLEoJMgQeGYoY9ApJ+NSKBDQ4PB?= =?us-ascii?q?CCEOoJNiXQBAQE?= X-IPAS-Result: =?us-ascii?q?A0DZBAAJGotY/5tPCQVdSAYMgwsBAQEBAYEAAyeENIp7qEk?= =?us-ascii?q?mhgaCbhUBAQEBAQEBAQEBAWEogjMZgkeBCwImAmwIAQGJYQqdRZABgiWLI4ELh?= =?us-ascii?q?E+Cdod/gjqCXwWJCZJIhmeLEoJMgQeGYoY9ApJ+NSKBDQ4PBCCEOoJNiXQBAQE?= X-IronPort-AV: E=Sophos;i="5.33,294,1477954800"; d="scan'208";a="211123776" Received: from gbury.eu (HELO mail2.gbury.eu) ([5.9.79.155]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 27 Jan 2017 11:01:36 +0100 Received: from [10.0.0.4] (lns-bzn-38-82-253-126-231.adsl.proxad.net [82.253.126.231]) by mail2.gbury.eu (Postfix) with ESMTPSA id CA361204DB6 for ; Fri, 27 Jan 2017 11:01:36 +0100 (CET) From: Guillaume Bury To: caml-list@inria.fr Message-ID: <03f55f63-3d0c-d5a0-bc9a-9ce5893c050c@gbury.eu> Date: Fri, 27 Jan 2017 11:01:38 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.6.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit Subject: [Caml-list] [ANN] mSAT 0.6 Hello, I have the pleasure to announce the release of mSAT 0.6 [0], a modular SAT-solver library in pure OCaml. SAT solvers are useful for NP-complete constraint solving, and are commonly used directly in many tools (including the package manager of eclipse), or indirectly as part of SMT solvers (Satisfiability Modulo Theory). mSAT is a modernized fork of alt-ergo-zero[1] that can be used both as a pure SAT solver, and as a building block for writing SMT solvers. To write a SMT solver based on mSAT, there is a functor that can be instantiated with a custom term structure and a custom theory responsible for propagation, following the Lazy SMT framework. The functor also provides an interface for MCSat-style solvers. mSAT is also proof-producing (it can output boolean resolution proofs), model-producing, and can output unsat-cores. Its flexibility and availability as an OCaml library make it useful for writing SMT solvers that feature experimental theories or theory implementations. The documentation can be found online [2]. Performance-wise, mSAT should be in the fast end of what OCaml makes possibles. Obviously, state of the art C solvers (minisat, picosat, etc.) are still much better. mSAT is developed by Guillaume Bury and Simon Cruanes, and available on opam as "msat", under the permissive Apache license. [0] https://github.com/Gbury/mSAT [1] http://cubicle.lri.fr/alt-ergo-zero/ [2] https://gbury.github.io/mSAT/ -- Guillaume Bury