From d7caa719f7f8a0836268bd371a15abda6272452d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 29 Oct 2014 13:45:19 +0100 Subject: [PATCH] updated README --- README | 37 ------------------------------------- README.md | 26 ++++++++++++++++++++++++++ 2 files changed, 26 insertions(+), 37 deletions(-) delete mode 100644 README create mode 100644 README.md diff --git a/README b/README deleted file mode 100644 index 4f4c7902..00000000 --- a/README +++ /dev/null @@ -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. diff --git a/README.md b/README.md new file mode 100644 index 00000000..0dcd0fac --- /dev/null +++ b/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. + +