From e3fc66919d474f14320c9dbe6b9e0952d3343e3d Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 15 Apr 2016 13:39:09 +0200 Subject: [PATCH] Put info about Msat.Solver higher in the readme --- README.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 43eed5df..f70b8ef9 100644 --- a/README.md +++ b/README.md @@ -15,6 +15,15 @@ This program is distributed under the Apache Software License version ## USAGE +### Generic SAT/SMT Solver + +A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module, +as a functor which takes two modules : + + - 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. + ### Sat Solver A ready-to-use SAT solver is available in the Sat module. It can be used @@ -45,15 +54,6 @@ as shown in the following code : let _ = Sat.solve () (* Should return Sat.Unsat *) ``` -### Generic SAT/SMT Solver - -A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module, -as a functor which takes two modules : - - - 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. - ## INSTALLATION ### Via opam