Edits to the doc and README

Author: BrunoDutertre

README

@@ -63,16 +63,6 @@ You can change the installation location by giving option
 For more explanations, please check doc/COMPILING.
 
 
-WINDOWS BUILD
--------------
-
-We recommend compiling using Cygwin. If you want a version that works
-natively on Windows (i.e., does not depend on the Cygwin DLLs), you
-can compile from Cygwin using the MinGW cross-compilers. This is
-explained in doc/COMPILING.
-
-
-
 SUPPORT FOR NON-LINEAR ARITHMETIC
 ---------------------------------
 
@@ -96,6 +86,13 @@ follow these instructions:
    ./configure --help to see what's there.
 
 
+WINDOWS BUILDS
+--------------
+
+We recommend compiling using Cygwin. If you want a version that works
+natively on Windows (i.e., does not depend on the Cygwin DLLs), you
+can compile from Cygwin using the MinGW cross-compilers. This is
+explained in doc/COMPILING.
 
 
 DOCUMENTATION

doc/sphinx/source/overview.rst

@@ -39,12 +39,34 @@ For a detailed explanation of the build process and options, check the
 file :file:`doc/COMPILING` included in the distribution.
 
 
+MCSAT and Nonlinear Arithmetic
+..............................
+
+Yices now includes a new solver for nonlinear arithmetic based on the
+Model Constructing Satisfiability Calculus (MCSAT). This solver depends
+on an external library available at
+https://github.com/SRI-CSL/libpoly. It you need nonlinear arithmetic
+and want to compile Yices from the source, you must install this libpoly
+library first. Then, compile Yices with MCSAT support as follows:
+
+.. code-block:: sh
+
+   ./configure --enable-mcsat
+   make -j
+   sudo make install
+
+You may need to set CPPFLAGS and LDFLAGS if the libpoly library is not
+in a standard location.
+
+
+
 Binary Distribution
 ...................
 
 The binary distributions contain pre-compiled binaries and
 libraries. These distributions are self-contained. The binaries and
-libraries are linked statically against GMP.
+libraries are linked statically against GMP and libpoly. They include
+support for nonlinear arithmetic and MCSAT.
 
 The binary distributions for Linux and Mac OS X include a shell script
 to install the binaries, headers, and library in

doc/sphinx/source/smt-logics.rst

@@ -7,8 +7,9 @@ SMT Logics
 
 The following table lists the names of all the official SMT-LIB logics
 at http://smt-lib.org (as of January 2015) and indicates whether Yices
-supports  them.  Currently,  Yices supports  all  the  quantifier-free
-SMT-LIB logics that do not involve nonlinear arithmetic.
+supports them.  Currently, Yices supports most quantifier-free SMT-LIB
+logics. Nonlinear real arithmetic is supported by using the MCSAT
+solver of Yices.
 
 
    +------------+----------------------------------------------+------------+
@@ -68,7 +69,7 @@ SMT-LIB logics that do not involve nonlinear arithmetic.
    | QF_NIA     | Nonlinear Integer Arithmetic                 | No         |
    |            |                                              |            |
    +------------+----------------------------------------------+------------+
-   | QF_NRA     | Nonlinear Real Arithmetic                    | No         |
+   | QF_NRA     | Nonlinear Real Arithmetic                    | Yes        |
    |            |                                              |            |
    +------------+----------------------------------------------+------------+
    | QF_RDL     | Real Difference Logic                        | Yes        |

doc/sphinx/source/version-data.rst

@@ -22,11 +22,11 @@ used at compile time for checking the Yices version.
  
    Patch level
 
-For Yices 2.3.1, they are defined as follows::
+For Yices 2.4.0, they are defined as follows::
 
    #define __YICES_VERSION            2
-   #define __YICES_VERSION_MAJOR      3
-   #define __YICES_VERSION_PATCHLEVEL 1
+   #define __YICES_VERSION_MAJOR      4
+   #define __YICES_VERSION_PATCHLEVEL 0
 
 The same information is available in the following constant string.
 
@@ -35,7 +35,7 @@ The same information is available in the following constant string.
    Version as a string.
 
    The string includes the version number, followed by the revision
-   number and the patch level, as in ``"2.3.1"``.
+   number and the patch level, as in ``"2.4.0"``.
 
 More details are given by three constant strings: