updated README

README

@@ -1,37 +0,0 @@
-Alt-Ergo Zero is an OCaml library for an SMT solver. This SMT solver
-is derived from Alt-Ergo. It uses an efficient SAT solver and supports
-the following quantifier free theories:
-    - Equality and uninterpreted functions
-    - Arithmetic (linear, non-linear, integer, real)
-    - Enumerated data-types
-
-This API makes heavy use of hash consing, in particular hash-consed strings.
-
-COPYRIGHT
-=========
-
-This program is distributed under the Apache Software License version
-2.0. See the enclosed file COPYING.
-
-
-INSTALLATION
-============
-To compile Alt-Ergo Zero you will need OCaml version 3.11 (or newer).
-
-Uncompress the archive and do:
-     cd aez-0.3
-     ./configure
-     make
-
-then with superuser rigths:
-     make install
-
-
-USAGE
-=====
-
-The documentation generated by ocamldoc is available in the repertory doc/.
-
-To use Alt-Ergo Zero in the toplevel you must give ocaml (or ocamlc)
-the options -I +alt-ergo-zero unix.cma nums.cma aez.cma. To compile
-natively you must use -I +alt-ergo-zero unix.cmxa nums.cmxa aez.cmxa.

README.md

@@ -0,0 +1,26 @@
+# MSAT
+
+MSAT is an OCaml library that features a modular SAT-solver and some
+extensions (including SMT). This is *work in progress*.
+
+
+It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
+
+The following theories should be supported:
+
+- Equality and uninterpreted functions
+- Arithmetic (linear, non-linear, integer, real)
+- Enumerated data-types
+
+## COPYRIGHT
+
+This program is distributed under the Apache Software License version
+2.0. See the enclosed file COPYING.
+
+
+## INSTALLATION
+============
+
+You will need ocamlfind.
+
+