From 9e3484d2b381b49c83ee9f78545a4811c1593268 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 22 Jan 2018 22:14:01 -0600
Subject: [PATCH] update readme

---
 README.md | 102 +++++++++---------------------------------------------
 1 file changed, 17 insertions(+), 85 deletions(-)

diff --git a/README.md b/README.md
index 8e1d42b7..3e7332de 100644
--- a/README.md
+++ b/README.md
@@ -1,107 +1,39 @@
-# MSAT  [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT)
+# CDCL [![Build Status](https://travis-ci.org/c-cube/cdcl.svg?branch=master)](https://travis-ci.org/c-cube/CDCL)
 
-MSAT is an OCaml library that features a modular SAT-solver and some
-extensions (including SMT).
+CDCL is an OCaml library with a functor to create SMT solvers following
+the CDCL(T) approach (so called "lazy SMT").
 
+It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero)
+and its fork [mSAT](https://github.com/gbury/msat).
 
-It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
-
-
-## COPYRIGHT
-
-This program is distributed under the Apache Software License version
-2.0. See the enclosed file `LICENSE`.
 
 ## Documentation
 
-See https://gbury.github.io/mSAT/
+See https://c-cube.github.io/cdcl/
 
-## INSTALLATION
+## Installation
 
 ### Via opam
 
-Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
+Once the package is on [opam](http://opam.ocaml.org), just `opam install cdcl`.
 For the development version, use:
 
-    opam pin add msat https://github.com/Gbury/mSAT.git
+    opam pin add msat https://github.com/c-cube/cdcl.git
 
 ### Manual installation
 
-You will need ocamlfind and ocamlbuild. The command is:
+You will need jbuilder. The command is:
 
     make install
 
-## USAGE
+## Usage
 
-### Generic SAT/SMT Solver
+The main module is `CDCL`.
 
-A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
-as a functor which takes two modules :
+A modular implementation of the SMT algorithm can be found in the `CDCL.Make` functor,
+as a functor which takes a `Theory_intf.S` module
 
-  - A representation of formulas (which implements the `Formula_intf.S` signature)
-
-  - A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions.
-
-  - A dummy empty module to ensure generativity of the solver (solver modules heavily relies on
-  side effects to their internal state)
-
-### Sat Solver
-
-A ready-to-use SAT solver is available in the Sat module. It can be used
-as shown in the following code :
-
-```ocaml
-(* Module initialization *)
-module Sat = Msat.Sat.Make()
-module E = Msat.Sat.Expr (* expressions *)
-
-(* We create here two distinct atoms *)
-let a = E.fresh ()    (* A 'new_atom' is always distinct from any other atom *)
-let b = E.make 1      (* Atoms can be created from integers *)
-
-(* We can try and check the satisfiability of some clauses --
-   here, the clause [a or b].
-   Sat.assume adds a list of clauses to the solver. *)
-let() = Sat.assume [[a; b]]
-let res = Sat.solve ()        (* Should return (Sat.Sat _) *)
-
-(* The Sat solver has an incremental mutable state, so we still have
-   the clause [a or b] in our assumptions.
-   We add [not a] and [not b] to the state. *)
-let () = Sat.assume [[E.neg a]; [E.neg b]]
-let res = Sat.solve ()        (* Should return (Sat.Unsat _) *)
-```
-
-
-#### Formulas API
-
-Writing clauses by hand can be tedious and error-prone.
-The functor `Msat.Tseitin.Make` proposes a formula AST (parametrized by
-atoms) and a function to convert these formulas into clauses:
-
-```ocaml
-(* Module initialization *)
-module Sat = Msat.Sat.Make()
-module E = Msat.Sat.Expr (* expressions *)
-module F = Msat.Tseitin.Make(E)
-
-(* We create here two distinct atoms *)
-let a = E.fresh ()    (* A fresh atom is always distinct from any other atom *)
-let b = E.make 1      (* Atoms can be created from integers *)
-
-(* Let's create some formulas *)
-let p = F.make_atom a
-let q = F.make_atom b
-let r = F.make_and [p; q]
-let s = F.make_or [F.make_not p; F.make_not q]
-
-(* We can try and check the satisfiability of the given formulas *)
-let () = Sat.assume (F.make_cnf r)
-let _ = Sat.solve ()        (* Should return (Sat.Sat _) *)
-
-(* The Sat solver has an incremental mutable state, so we still have
- * the formula 'r' in our assumptions *)
-let () = Sat.assume (F.make_cnf s)
-let _ = Sat.solve ()        (* Should return (Sat.Unsat _) *)
-```
+## Copyright
 
+This program is distributed under the Apache Software License version
+2.0. See the enclosed file `LICENSE`.