Increased version number to 2.4.2 + updates to the doc.

Author: BrunoDutertre

Makefile

@@ -37,7 +37,7 @@ YICES_TOP_DIR=$(shell pwd)
 #
 MAJOR = 2
 MINOR = 4
-PATCH_LEVEL = 1
+PATCH_LEVEL = 2
 
 YICES_VERSION = $(MAJOR).$(MINOR).$(PATCH_LEVEL)
 

doc/manual/manual.tex

@@ -153,7 +153,7 @@ \subsection{Source Distribution}
    sudo apt-get install gperf
 \end{verbatim}
 \end{small}
-After this, compiling and installing Yices uses the following standard steps:
+After this, compiling and installing Yices use the following standard steps:
 \begin{small}
 \begin{verbatim}
    ./configure
@@ -172,6 +172,40 @@ \subsection{Source Distribution}
 source distribution gives more details.
 
 
+\subsection{Nonlinear Arithmetic and MCSAT}
+\label{mcsat-install}
+
+Yices includes a solver for nonlinear arithmetic based on the Model
+Constructing Satisfiability Calculus (MCSAT). This calculus and its
+application to nonlinear arithmetic are explained
+in~\cite{Jovanovic-etal:MCSATb:2013}
+and~\cite{deMouraJovanovic:nla:2012}.
+
+The precompiled, binary distributions of Yices include the MCSAT
+solver and can process nonlinear arithmetic problems. If you build
+Yices from source and want support for nonlinear arithmetic, you must
+install an external library first and enable MCSAT support when you
+compile Yices.
+
+This library is called ``libpoly''. It implements various operations
+on polynomials used by the MCSAT solver. It is open source and it is
+available on GitHub (\url{https://github.com/SRI-CSL/libpoly}). Make
+sure that you download the latest version of libpoly. Yices~2.4.2
+requires libpoly v0.1.2.
+
+Once you have installed libpoly, you can compile Yices with MCSAT
+support as follows:
+\begin{small}
+\begin{verbatim}
+   ./configure --enable-mcsat
+   make -j
+   sudo make install
+\end{verbatim}
+\end{small}
+The usual environment variables (e.g., \texttt{CPPFLAGS} and
+\texttt{LDFLAGS}) can be used if you install libpoly in a non-standad
+location.
+
 
 \section{Content of the Distributions}
 
@@ -213,19 +247,17 @@ \section{Library Dependencies}
 reproduced in Appendix~\ref{gmp-license}.
 
 Since release 2.4.0, Yices has optional support for nonlinear real
-arithmetic, using the Model Constructing Satisfiability Calculus
-(MCSAT)~\cite{deMouraJovanovic:nla:2012,deMouraJovanovic:MCSAT:2013,Jovanovic-etal:MCSATb:2013}. This
-depends on an external library for operations on polynomials which is
+arithmetic. As explained in Section~\ref{mcsat-install}, this depends
+on an external library for operations on polynomials which is
 available at~\url{https://github.com/SRI-CSL/libpoly}.
 
 
 \section{Supported Logics}
 
 The current Yices~2 release supports quantifier-free combinations of
 linear integer and real arithmetic, uninterpreted function, arrays,
-and bitvectors. Currently, Yices~2 supports all SMT-LIB logics that do
+and bitvectors. Currently, Yices~2 supports most SMT-LIB logics that do
 not involve quantifiers as summarized in Table~\ref{supported-logics}.
-Yices~2 includes a solver for non-linear real arithmeitce
 The meaning of the logics and theories in this table is explained at
 the SMT-LIB website (\url{http://www.smtlib.org}).  In addition,
 Yices~2 supports a more general set of array operations than required
@@ -781,17 +813,12 @@ \subsection{Bitvectors}
 \label{bitvectors}
 \end{table}
 
-\medskip\noindent
-The semantics of all the bitvector operators is defined in the
-SMT-LIB standard.  Yices~2 follows the standard except for the
-case of division by zero.  In SMT-LIB, the result of a division by
-zero is an unspecified value, but one must ensure that the division
-operators are functional. In other words, SMT-LIB does not specify the
-result of $(\mathtt{bvudiv}\ a\ b)$ if $b$ is the zero vector, but
-$(\mathtt{bvudiv}\ a\ b)$ and $(\mathtt{bvudiv}\ c\ b)$ must be equal
-whenever $a = c$, even if $b$ is the zero vector. Yices~2 uses a
-simpler semantics (inspired by the BTOR
-format~\cite{Brummayer-etal:2008}):
+\medskip\noindent The semantics of all the bitvector operators is
+defined in the SMT-LIB standard. Like other SMT solvers, Yices~2
+follows the BTOR conventions for bitvector division by
+zero~\cite{Brummayer-etal:2008}. Until recently, this was not the
+semantics defined by the SMT-LIB standard. The SMT-LIB semantics
+changed in October 2015. It is now the same as BTOR:
 \begin{description}
 \item[Unsigned Division:]  If $b$ is  the zero bitvector  of $n$
   bits then
@@ -1018,10 +1045,11 @@ \section{MCSAT}
 currently dedicated to quantifier-free nonlinear real arithmetic. The
 theory and implementation of MCSAT is discussed in several
 publications~\cite{Jovanovic-etal:MCSATb:2013,deMouraJovanovic:MCSAT:2013}.
-Currently, this solver can process input written the SMT-LIB~2.0
-notation. It does not support as many features as the CDCL-based
-solver described in the previous section. In particular, the MCSAT
-solver does not yet support incremental solving (i.e., push and pop).
+Currently, this solver can process input written in the SMT-LIB~2.0 or
+Yices notations. It does not support as many features as the
+CDCL-based solver described in the previous section. In particular,
+the MCSAT solver does not yet support incremental solving (i.e., push
+and pop).
 
 
 \chapter{Yices Tool}
@@ -1248,6 +1276,10 @@ \section{Tool Invocation}
   includes no  theory solvers  at all. All  assertions must  be purely
   propositional (i.e., involve only Boolean terms).
 
+  With option \texttt{--logic=QF\_NRA}, the \texttt{yices} binary uses
+  its MCSAT solver for nonlinear real arithmetic. When this solver is
+  selected, incremental solving is not supported.
+
 \item[--arith-solver=<solver>] Select one of the possible arithmetic solvers.\\[1mm]
   \texttt{<solver>}     must    be     one     of    \texttt{simplex},
   \texttt{floyd-warshall}, or \texttt{auto}.

doc/sphinx/source/basic-usage.rst

@@ -61,8 +61,10 @@ This has two effects:
      printing these two terms. Otherwise, it would construct names
      such as ``"t!3"`` and ``"t!4"``.
 
-  2. The symbol table maps the strings ``"x"`` and ``"y"`` to the
-     terms ``x`` and ``y``, respectively.
+  2. The strings ``"x"`` and ``"y"`` can now be used to retrieve the
+     terms ``x`` and ``y``. Yices maintains an internal symbol table
+     that maps strings to terms. Calling :c:func:`yices_set_term_name`
+     adds an entry in this table.
 
 We can now build a more complex term by using constructors such as
 :c:func:`yices_arith_geq0_atom` and :c:func:`yices_and3`::

doc/sphinx/source/conf.py

@@ -58,7 +58,7 @@
 # The short X.Y version.
 version = '2.4'
 # The full version, including alpha/beta/rc tags.
-release = '2.4.0'
+release = '2.4.2'
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.

doc/sphinx/source/error-reports.rst

@@ -47,3 +47,5 @@ The following functions give access to the error report.
 
    To avoid memory leaks, the returned string must be freed when it is
    no longer used by calling :c:func:`yices_free_string`.
+
+

doc/sphinx/source/index.rst

@@ -23,6 +23,7 @@ API Reference
 
    version-data
    global-initialization
+   out-of-memory
    hard-limits
    api-types
    error-reports

doc/sphinx/source/overview.rst

@@ -42,12 +42,17 @@ 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:
+Yices now includes a solver for nonlinear arithmetic based on the
+Model Constructing Satisfiability Calculus (MCSAT). This solver
+depends on an external library for manipulating polynomials. If you
+need nonlinear arithmetic and want to compile Yices from the source,
+you must install this library first. Get it from our `GitHub
+repository <https://github.com/SRI-CSL/libpoly>`_ and follow the build
+instructions there.  Make sure to get the latest libpoly release
+(v0.1.2).
+
+Once you have installed libpoly, you can compile Yices with MCSAT
+support as follows:
 
 .. code-block:: sh
 

doc/sphinx/source/version-data.rst

@@ -22,11 +22,11 @@ used at compile time for checking the Yices version.
  
    Patch level
 
-For Yices 2.4.0, they are defined as follows::
+For Yices 2.4.2, they are defined as follows::
 
    #define __YICES_VERSION            2
    #define __YICES_VERSION_MAJOR      4
-   #define __YICES_VERSION_PATCHLEVEL 0
+   #define __YICES_VERSION_PATCHLEVEL 2
 
 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.4.0"``.
+   number and the patch level, as in ``"2.4.2"``.
 
 More details are given by three constant strings:
 
@@ -58,4 +58,4 @@ More details are given by three constant strings:
 
    Build date.
 
-   This string uses the format ``"Year-Month-Day"``, as in ``"2014-12-20"``.
+   This string uses the format ``"Year-Month-Day"``, as in ``"2015-12-11"``.

src/include/yices.h

@@ -1,5 +1,5 @@
 /*
- * The Yices SMT Solver. Copyright 2014 SRI International.
+ * The Yices SMT Solver. Copyright 2015 SRI International.
  *
  * This program may only be used subject to the noncommercial end user
  * license agreement which is downloadable along with this program.
@@ -72,7 +72,7 @@ extern "C" {
 
 #define __YICES_VERSION            2
 #define __YICES_VERSION_MAJOR      4
-#define __YICES_VERSION_PATCHLEVEL 1
+#define __YICES_VERSION_PATCHLEVEL 2
 
 
 /*
@@ -136,6 +136,50 @@ __YICES_DLLSPEC__ extern void yices_free_string(char *s);
 
 
 
+/***************************
+ * OUT-OF-MEMORY CALLBACK  *
+ **************************/
+
+/*
+ * By default, when Yices runs out of memory, it
+ * first prints an error message on stderr; then it calls
+ * exit(YICES_EXIT_OUT_OF_MEMORY).  This kills the whole process.
+ *
+ * The following function allows you to register a callback to invoke
+ * if Yices runs out of memory.  The callback function takes no
+ * arguments and returns nothing.
+ *
+ * Installing an out-of-memory callback allows you to do something a
+ * bit less brutal than killing the process. If there's a callback,
+ * yices will call it first when it runs out of memory.  The callback
+ * function should not return. If it does, yices will call exit as
+ * previously.
+ *
+ * In other words, the code that handles out-of-memory is as follows:
+ *
+ *   if (callback != NULL) {
+ *     callback();
+ *   } else {
+ *     fprintf(stderr, ...);
+ *   }
+ *   exit(YICES_EXIT_OUT_OF_MEMORY);
+ *
+ *
+ * IMPORTANT
+ * ---------
+ * After Yices runs out of memory, its internal data structures may be
+ * left in an inconsistent/corrupted state. The API is effectively
+ * unusable at this point and nothing can be done to recover cleanly.
+ * Evan a call to yices_exit() may cause a seg fault. The callback
+ * should not try to cleanup anything, or call any function from the API.
+ * 
+ * A plausible use of this callback feature is to implement an
+ * exception mechanism using setjmp/longjmp.
+ */
+__YICES_DLLSPEC__ extern void yices_set_out_of_mem_callback(void (*callback)(void));
+
+
+
 /*********************
  *  ERROR REPORTING  *
  ********************/
@@ -193,45 +237,6 @@ __YICES_DLLSPEC__ extern char *yices_error_string(void);
 
 
 
-/*
- * Register a callback function to invoke if Yices runs out of memory.
- * The callback function takes no arguments and returns nothing.
- *
- * By default, there's no callback. When Yices runs out of memory, it
- * first prints an error message on stderr; then it calls
- * exit(YICES_EXIT_OUT_OF_MEMORY).  This kills the whole process.
- *
- * Installing an out-of-memory callback allows you to do
- * something a bit less brutal. If there's a callback,
- * yices will call it first when it runs out of memory.
- * The callback function should not return. If it does,
- * yices will call exit as previously.
- *
- * In other words, the code that handles out-of-memory is as follows:
- *
- *   if (callback != NULL) {
- *     callback();
- *   } else {
- *     fprintf(stderr, ...);
- *   }
- *   exit(YICES_EXIT_OUT_OF_MEMORY);
- *
- *
- * IMPORTANT
- * ---------
- * After Yices runs out of memory, its internal data structures may be
- * left in an inconsistent/corrupted state. The API is effectively
- * unusable at this point and nothing can be done to recover cleanly.
- * Evan a call to yices_exit() may cause a seg fault. The callback
- * should not try to cleanup anything, or call any function from the API.
- * 
- * A plausible use of this callback feature is to implement an
- * exception mechanism using setjmp/longjmp.
- */
-__YICES_DLLSPEC__ extern void yices_set_out_of_mem_callback(void (*callback)(void));
-
-
-
 /********************************
  *  VECTORS OF TERMS AND TYPES  *
  *******************************/