From 35c99df753563000f78539a15bc9d1efd50d6817 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sun, 25 Dec 2016 20:52:18 +0100 Subject: [PATCH 1/2] Added some missing headers --- src/core/plugin_intf.ml | 5 +++++ src/core/solver_types.ml | 5 +++++ src/core/solver_types.mli | 5 +++++ src/core/solver_types_intf.ml | 5 +++++ src/core/theory_intf.ml | 5 +++++ 5 files changed, 25 insertions(+) diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml index bfba8585..2c2d703b 100644 --- a/src/core/plugin_intf.ml +++ b/src/core/plugin_intf.ml @@ -11,6 +11,11 @@ (* Apache Software License version 2.0 *) (* *) (**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) (** McSat Theory diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml index 7d4fe172..36fb949b 100644 --- a/src/core/solver_types.ml +++ b/src/core/solver_types.ml @@ -10,6 +10,11 @@ (* Apache Software License version 2.0 *) (* *) (**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) open Printf diff --git a/src/core/solver_types.mli b/src/core/solver_types.mli index 2670096e..b9e76a7a 100644 --- a/src/core/solver_types.mli +++ b/src/core/solver_types.mli @@ -10,6 +10,11 @@ (* Apache Software License version 2.0 *) (* *) (**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) (** Internal types (implementation) diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml index 18ad7fe2..94f23b67 100644 --- a/src/core/solver_types_intf.ml +++ b/src/core/solver_types_intf.ml @@ -10,6 +10,11 @@ (* Apache Software License version 2.0 *) (* *) (**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) (** Internal types (interface) diff --git a/src/core/theory_intf.ml b/src/core/theory_intf.ml index f6e9c263..8df11c20 100644 --- a/src/core/theory_intf.ml +++ b/src/core/theory_intf.ml @@ -11,6 +11,11 @@ (* Apache Software License version 2.0 *) (* *) (**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) (** SMT Theory From 109ddd7a73e375ecc6077fa2458ea36ea93c2ec3 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 26 Dec 2016 12:24:07 +0100 Subject: [PATCH 2/2] Readme update --- README.md | 34 ++++++++++++++++------------------ 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 025983e6..93ac820a 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ # MSAT [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT) MSAT is an OCaml library that features a modular SAT-solver and some -extensions (including SMT). This is **work in progress**. +extensions (including SMT). It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero). @@ -16,6 +16,21 @@ This program is distributed under the Apache Software License version See https://gbury.github.io/mSAT/ +## INSTALLATION + +### Via opam + +Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`. +For the development version, use: + + opam pin add msat https://github.com/Gbury/mSAT.git + +### Manual installation + +You will need ocamlfind and ocamlbuild. The command is: + + make install + ## USAGE ### Generic SAT/SMT Solver @@ -60,20 +75,3 @@ as shown in the following code : let _ = Sat.solve () (* Should return (Sat.Unsat _) *) ``` -## INSTALLATION - -### Via opam - -Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`. -For the development version, use: - - opam pin add msat https://github.com/Gbury/mSAT.git - -### Manual installation - -You will need ocamlfind. The command is: - - make install - - -