From cdf83713948c09fb76008f7231e0221b1fb354e7 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 3 Mar 2015 17:06:16 +0100
Subject: [PATCH] Added info about solver functor

---
 README.md | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 754f1b84..0991d8b9 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,14 @@ as shown in the following code :
 
 ### Generic SAT/SMT Solver
 
-A modular implementation of the SMT algorithm can be found in the `Msat.`
+A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module,
+as a functor which takes three modules :
+
+  - A log module for debug output
+
+  - 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