Merge pull request #57 from pysmt/clarifying_readme

Clarifying readme

README.rst

@@ -22,25 +22,10 @@ Among others, you can:
            :target: https://readthedocs.org/projects/pysmt/?badge=latest
            :alt: Documentation Status
 
-
-Getting Started
-===============
-You can install the latest stable release of pySMT from PyPI:
-
-  # pip install pysmt
-this will additionally install the *pysmt-install* command, that can be used to install the solvers: e.g.,
-
-  # pysmt-install --msat
-this will download and install Mathsat 5. You will need to set your PYTHONPATH as suggested by the installer to make the python bindings visible. To verify that a solver has been installed run
-
-  $ pysmt-install --check
-*Note* pysmt-install is provided to simplify the installation of solvers. However, each solver has its own dependencies, license and restrictions on use that you need to take into account.
-
-
 Supported Theories and Solvers
 ==============================
 pySMT provides methods to define a formula in Linear Real Arithmetic (LRA), Real Difference Logic (RDL), their combination (LIRA) and
-Equalities and Uninterpreted Functions (EUF). The following solvers are supported:
+Equalities and Uninterpreted Functions (EUF). The following solvers are supported through native APIs:
 
 * MathSAT (http://mathsat.fbk.eu/) >= 5
 * Z3 (http://z3.codeplex.com/releases) >= 4
@@ -49,13 +34,22 @@ Equalities and Uninterpreted Functions (EUF). The following solvers are supporte
 * pyCUDD (http://bears.ece.ucsb.edu/pycudd.html)
 * PicoSAT (http://fmv.jku.at/picosat/)
 
-The library assumes that the python binding for the SMT Solver are installed
-and accessible from your PYTHONPATH. For Yices 2 we rely on pyices (https://github.com/cheshire/pyices).
+Additionally, you can use any SMT-LIB 2 compliant solver.
+
+PySMT assumes that the python bindings for the SMT Solver are installed and accessible from your PYTHONPATH. For Yices 2 we rely on pyices (https://github.com/cheshire/pyices).
+
+pySMT works on both Python 2 and Python 3. Some solvers support both versions (e.g., MathSAT) but in general, many solvers still support only Python 2.
+
 
-pySMT works on both Python 2 and Python 3. Some solvers support both
-versions (e.g., MathSAT) but in general, many solvers still support
-only Python 2.
+Getting Started
+===============
+You can install the latest stable release of pySMT from PyPI:
+
+  # pip install pysmt
+this will additionally install the *pysmt-install* command, that can be used to install the solvers: e.g.,
 
+  $ pysmt-install --check
+will show you which solvers have been found in your PYTHONPATH. For instructions on how to install each solver refer to the section on *solvers installation*.
 
 Usage
 =====
@@ -111,3 +105,22 @@ The following is the pySMT code for solving this problem:
     print(model)
   else:
     print("No solution found")
+
+
+Solvers Installation
+====================
+
+PySMT does not depend directly on any solver. If you want to perform solving, you need to have at least one solver installed, and then call it via pySMT either through its native API, or passing through an SMT-LIB file.
+
+The script *pysmt-install* can be used to simplify the installation of the solvers:
+
+ $ pysmt-install --msat
+will install MathSAT 5. This script does not install required dependencies for building the solver (e.g., make or gcc) and has been tested mainly on Linux Debian/Ubuntu systems. We suggest that you refer to the documentation of each solver to understand how to install it with its python bindings. Nevertheless, we try to keep *pysmt/cmd/install.py* as readable and documented as possible..
+
+Finally, for CVC4, pycudd and picosat, we have patches that need to be applied. The patches are available in the repository 'pysmt/solvers_patches' and should be applied against the following versions of the solvers:
+
+- CVC4: Git revision 68f22235a62f5276b206e9a6692a85001beb8d42
+- pycudd: 2.0.2
+- picosat 960
+
+For instruction on how to use any SMT-LIB complaint solver with pySMT see examples/generic_wrapper.py

examples/README.rst

@@ -12,3 +12,4 @@ pySMT. Suggested order:
    (BMC+K-Induction) in ~150 lines
 6. allsat.py: How to access functionalities of solvers not currently
    wrapped by pySMT.
+7. generic_smtlib.py: Shows how to use any SMT-LIB complaint SMT solver

examples/generic_smtlib.py

@@ -0,0 +1,60 @@
+# This example shows how to define a generic SMT-LIB solver, and use
+# it within pySMT. The example looks for mathsat in /tmp, you can
+# create a symlink there.
+#
+# Using this process you can experiment with any SMT-LIB 2 compliant
+# solver even if it does not have python bindings, or has not been
+# integrated with pySMT.
+#
+# Note: When using the SMT-LIB wrapper, you can only use logics
+# supported by pySMT. If the version of pySMT in use does not support
+# Arrays, then you cannot represent arrays.
+#
+
+# To define a Generic Solver you need to provide:
+#
+# - A name to associate to the solver
+# - The path to the script + Optional arguments
+# - The list of logics supported by the solver
+#
+# It is usually convenient to wrap the solver in a simple shell script.
+# See examples for Z3, Mathsat and Yices in pysmt/test/smtlib/bin/*.template
+#
+from pysmt.logics import QF_UFLRA, QF_UFIDL, QF_LRA, QF_IDL, QF_LIA
+from pysmt.shortcuts import get_env, GT, Solver, Symbol
+from pysmt.typing import REAL, INT
+from pysmt.exceptions import NoSolverAvailableError
+
+name = "mathsat" # Note: The API version is called 'msat'
+path = ["/tmp/mathsat"] # Path to the solver
+logics = [QF_UFLRA, QF_UFIDL] # Some of the supported logics
+
+env = get_env()
+
+# Add the solver to the environment
+env.factory.add_generic_solver(name, path,logics)
+
+r, s = Symbol("r", REAL), Symbol("s", REAL)
+p, q = Symbol("p", INT), Symbol("q", INT)
+
+f_lra = GT(r, s)
+f_idl = GT(p, q)
+
+# PySMT takes care of recognizing that QF_LRA can be solved by a QF_UFLRA solver.
+with Solver(name=name, logic=QF_LRA) as s:
+    res = s.solve()
+    assert res, "Was expecting '%s' to be SAT" % f_lra
+
+
+with Solver(name=name, logic=QF_IDL) as s:
+    s.add_assertion(f_idl)
+    res = s.solve()
+    assert res, "Was expecting '%s' to be SAT" % f_idl
+
+try:
+    with Solver(name=name, logic=QF_LIA) as s:
+        pass
+except NoSolverAvailableError:
+    # If we ask for a logic that is not contained by any of the
+    # supported logics an exception is thrown
+    print("%s does not support QF_LIA" % name)