Merge pull request #607 from SRI-CSL/context_delegates

QF_BV context delegates (#453): config/param selection, incremental state, assumptions, and delegate regressions

Author: disteph

Makefile.build

@@ -305,13 +305,21 @@ static-check-api: static_build_subdirs version
 check: regress
 mcsat-check: mcsat-regress
 static-check: static-regress
+delegate-check: delegate-regress
+static-delegate-check: static-delegate-regress
 
 regress: build_subdirs version
 	@ echo "=== Building binaries ==="
 	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin
 	@ echo "=== Running regressions ==="
 	+@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin
 
+delegate-regress: build_subdirs version
+	@ echo "=== Building binaries ==="
+	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin
+	@ echo "=== Running delegate-only regressions ==="
+	+@ REGRESS_DELEGATE_MODE=only $(regressdir)/check.sh $(regressdir) $(build_dir)/bin
+
 
 mcsat-regress: build_subdirs version
 	@ echo "=== Building binaries ==="
@@ -326,6 +334,12 @@ static-regress: static_build_subdirs version
 	@ echo "=== Running regressions ==="
 	+@ $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin
 
+static-delegate-regress: static_build_subdirs version
+	@ echo "=== Building binaries ==="
+	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin
+	@ echo "=== Running delegate-only regressions ==="
+	+@ REGRESS_DELEGATE_MODE=only $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin
+
 
 static-mcsat-regress: static_build_subdirs version
 	@ echo "=== Building binaries ==="
@@ -335,7 +349,9 @@ static-mcsat-regress: static_build_subdirs version
 
 
 .PHONY: all obj static-obj lib static-lib bin static-bin test static-test \
-    regress static-regress check static-check check-api static-check-api
+    regress delegate-regress static-regress static-delegate-regress \
+    check delegate-check static-check static-delegate-check \
+    check-api static-check-api
 
 
 #

doc/manual/manual.tex

@@ -1455,16 +1455,71 @@ \section{MCSAT}
 non-linear arithmetic are presented in a preprint~\cite{jovanovic2021interpolation}.
 
 \section{Third-Party SAT Solvers}
+\label{delegates}
+
+Yices supports using third-party Boolean satisfiability solvers as the
+back-end CNF engine for QF\_BV problems. Such solvers, called
+\emph{delegates}, are optional but can provide significant performance
+improvements. When a delegate is selected, Yices performs ``bit
+blasting'' as usual --- converting the problem to an equisatisfiable
+SAT problem in conjunctive normal form (CNF) --- and then hands the
+resulting CNF to the selected delegate instead of the internal Yices
+CDCL SAT solver. Bit-blasting itself is unchanged.
+
+Yices recognizes four delegate names. \texttt{y2sat} is an internal
+SAT solver always available in any Yices build. CaDiCaL,
+CryptoMiniSat, and Kissat are external solvers; support for each must
+be enabled at compilation time as explained in
+Chapter~\ref{compilation}. The capability matrix is summarized below.
+\begin{center}
+\begin{tabular}{|l|c|c|c|c|}
+\hline
+Delegate            & Always available & Incremental push/pop &
+                      \texttt{check-sat-assuming} & Unsat core from assumptions \\
+\hline
+\texttt{y2sat}        & yes & rebuild on each check & rebuild on each check & no \\
+\texttt{cadical}      & no  & yes (selector frames) & yes & yes \\
+\texttt{cryptominisat}& no  & yes (selector frames) & yes & yes \\
+\texttt{kissat}       & no  & rebuild on each check & rebuild on each check & no \\
+\hline
+\end{tabular}
+\end{center}
+
+A delegate can be selected in three ways:
+\begin{itemize}
+\item from the SMT-LIB~2 frontend, by passing
+  \texttt{--delegate=<solver>} to \texttt{yices-smt2}
+  (Section~\ref{smt2-tool});
+\item from the API, by setting the \texttt{sat-delegate} parameter on
+  the context configuration with \texttt{yices\_set\_config} before
+  the context is created;
+\item from the API on a per-check basis, by setting the
+  \texttt{delegate} field of a search-parameter record with
+  \texttt{yices\_set\_param}, and passing that record to
+  \texttt{yices\_check\_context} (or one of its variants).
+\end{itemize}
+The one-shot helpers \texttt{yices\_check\_formula} and
+\texttt{yices\_check\_formulas} also accept a delegate name as their
+last argument; they bit-blast the input formulas into a fresh CNF and
+hand it to the chosen delegate.
+
+For incremental QF\_BV contexts (\texttt{push-pop} or
+\texttt{multi-checks} mode), CaDiCaL and CryptoMiniSat support a
+\emph{selector-frames} strategy that keeps the delegate live across
+\texttt{check-sat} calls and uses fresh selector literals to retract
+clauses on \texttt{pop}. This strategy preserves learned clauses
+between checks and is selected by setting the
+\texttt{sat-delegate-selector-frames} configuration parameter to
+\texttt{"true"} on the context. The default is \texttt{"false"}, in
+which case the delegate is rebuilt from the current bit-blasted
+problem at every mutation. The non-incremental delegates
+\texttt{y2sat} and Kissat are always rebuilt on each check; the
+\texttt{sat-delegate-selector-frames} option has no effect for them.
 
-In Yices 2.6.2, we have added support for using third-party Boolean
-satisfiability solvers. Such solvers are optional but can provide
-significant performance improvements on bit-vector problems. Use of
-these SAT solvers is enabled by a command-line option and is currently
-restricted to non-incremental QF\_BV problems. If an external solver
-is selected, Yices will perform ``bit blasting,'' that is, convert the
-problem to an equisatisfiable SAT problem in conjunctive normal form
-(CNF) and use the third-party solver to check satisfiability of this
-CNF formula.
+The full list of API names recognized by these mechanisms, together
+with their possible values and error codes, is documented in the
+\texttt{yices.h} header and on the Yices website (see
+Section~\ref{full-api}).
 
 
 
@@ -3652,6 +3707,7 @@ \section{SMT-LIB 2.x}
 
 
 \subsection{Tool Invocation}
+\label{smt2-tool}
 
 To run \texttt{yices-smt2} on an input file, type
 \begin{small}
@@ -3772,7 +3828,13 @@ \subsubsection*{Selecting a Back-end SAT Solver}
 problems by preprocessing and simplification, without producing a CNF
 formula. In such cases, the \texttt{delegate} option is irrelevant.
 
-\paragraph{Limitation:} Currently, use of the delegates is restricted to non-incremental problems.
+\paragraph{Incremental use:} Delegates can be used with
+\texttt{--incremental} on QF\_BV problems. CaDiCaL and CryptoMiniSat
+support incremental delegate checks. Non-incremental delegates such as
+\texttt{y2sat} and Kissat are rebuilt from the current bit-blasted
+problem on each \texttt{check-sat}. The selector-frame configuration
+used by the API for incremental delegates has no effect for
+non-incremental delegates.
 
 \subsubsection*{Exporting to Dimacs}
 
@@ -3864,7 +3926,10 @@ \subsubsection*{All Command-line Options}
 
 \item[--delegate=<solver>] Select an external SAT solver for bit-vector problems,
 
-   The \texttt{<solver>} can be either \texttt{cadical}, or \texttt{cryptominisat}, or \texttt{y2sat}.
+   The \texttt{<solver>} can be either \texttt{cadical},
+   \texttt{cryptominisat}, \texttt{kissat}, or \texttt{y2sat}. In
+   incremental mode, \texttt{y2sat} and Kissat are rebuilt from the
+   current bit-blasted problem on each \texttt{check-sat}.
 
 \item[--dimacs=<filename>] Bitblast then export the CNF to a file (in DIMACS format).
 
@@ -4641,6 +4706,7 @@ \subsection*{Building and Querying a Model}
 
 
 \section{Full API}
+\label{full-api}
 
 The main header file \texttt{yices.h} includes documentation about all
 API functions. We provide more documentation on the Yices website:

doc/sphinx/source/context-operations.rst

@@ -226,6 +226,53 @@ specialized for difference logic and support only mode one-shot.
 The default mode is push-pop.
 
 
+.. _sat_delegate_config:
+
+**SAT Delegate (QF_BV only)**
+
+For QF_BV contexts, Yices can be configured to use a third-party
+Boolean SAT solver --- called a *delegate* --- as the back-end CNF
+engine. When a delegate is selected, Yices bit-blasts the assertions
+to CNF as usual and hands the resulting clause set to the chosen
+delegate instead of the internal Yices CDCL SAT solver.
+
+Yices recognizes four delegate names. ``y2sat`` is an internal SAT
+solver always available in any Yices build. ``cadical``,
+``cryptominisat``, and ``kissat`` are external solvers; their
+inclusion in a particular Yices build is optional and can be checked
+at runtime with :c:func:`yices_has_delegate`. The capabilities of each
+delegate are summarized in the following table.
+
+   +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+
+   | Delegate          | Always available  | Incremental push/pop    | ``check_with_assumptions``| Unsat core from assumptions      |
+   +===================+===================+=========================+===========================+==================================+
+   | ``y2sat``         | yes               | rebuild on each check   | rebuild on each check     | no                               |
+   +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+
+   | ``cadical``       | optional          | yes (selector frames)   | yes                       | yes                              |
+   +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+
+   | ``cryptominisat`` | optional          | yes (selector frames)   | yes                       | yes                              |
+   +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+
+   | ``kissat``        | optional          | rebuild on each check   | rebuild on each check     | no                               |
+   +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+
+
+For incremental QF_BV contexts (``push-pop`` or ``multi-checks``
+mode), CaDiCaL and CryptoMiniSat support a *selector-frames* strategy
+that keeps the delegate live across :c:func:`yices_check_context`
+calls and uses fresh selector literals to retract clauses on
+``yices_pop``. This strategy preserves the delegate's learned clauses
+between checks. It is opt-in via the
+``sat-delegate-selector-frames`` configuration parameter described
+below. When the option is ``"false"`` (the default) or the delegate
+is non-incremental, Yices rebuilds the delegate from the current
+bit-blasted problem at every mutation.
+
+The delegate can also be selected, or one-shot overridden, on a
+per-check basis through the ``delegate`` field of a search-parameter
+record (see :ref:`heuristic_parameters`).
+
+The SAT delegate options are ignored for any logic other than QF_BV.
+
+
 
 Configuration Descriptor
 ........................
@@ -288,6 +335,31 @@ arithmetic fragment and the operating mode:
    +--------------------+-----------------------------------------------------+
 
 
+Two more parameters control the SAT back-end for QF_BV contexts.
+They are ignored for any other logic. See
+:ref:`sat_delegate_config` above for the meaning of each value.
+
+   +--------------------------------+---------------------+----------------------------------------------+
+   | Name                           |  Value              |  Meaning                                     |
+   +================================+=====================+==============================================+
+   | sat-delegate                   | ``"none"``          |  use the internal Yices SAT solver (default) |
+   |                                +---------------------+----------------------------------------------+
+   |                                | ``"y2sat"``         |  use y2sat as the SAT back-end               |
+   |                                +---------------------+----------------------------------------------+
+   |                                | ``"cadical"``       |  use CaDiCaL as the SAT back-end             |
+   |                                +---------------------+----------------------------------------------+
+   |                                | ``"cryptominisat"`` |  use CryptoMiniSat as the SAT back-end       |
+   |                                +---------------------+----------------------------------------------+
+   |                                | ``"kissat"``        |  use Kissat as the SAT back-end              |
+   +--------------------------------+---------------------+----------------------------------------------+
+   | sat-delegate-selector-frames   | ``"false"``         |  rebuild the delegate on each context        |
+   |                                |                     |  mutation (default)                          |
+   |                                +---------------------+----------------------------------------------+
+   |                                | ``"true"``          |  keep an incremental delegate live across    |
+   |                                |                     |  checks using selector-guarded frames        |
+   +--------------------------------+---------------------+----------------------------------------------+
+
+
 
 A configuration descriptor also stores a logic flag, which can either
 be *unknown* (i.e., no logic specified), or the name of an SMT-LIB

doc/sphinx/source/formula-operations.rst

@@ -69,21 +69,28 @@ third-party Boolean satisfiability solvers for bit-vector problems.
 
   A delegate is a SAT solver to use as backend when checking satisfiability of a bit-vector
   formula. The *delegate* parameter is ignored and has no effect unless the *logic* is "QF_BV".
-  In the latter case, three different delegates can be used:
+  In the latter case, four different delegates can be used:
 
    - "cadical": the CaDiCaL solver (https://github.com/arminbiere/cadical)
 
-   - "cryptominisat: the CryptoMiniSat solver (https://github.com/msoos/cryptominisat)
+   - "cryptominisat": the CryptoMiniSat solver (https://github.com/msoos/cryptominisat)
+
+   - "kissat": the Kissat solver (https://github.com/arminbiere/kissat)
 
    - "y2sat": an experimental SAT solver included in Yices
 
-   These three delegates are known to Yices but support for CaDiCaL and CryptoMiniSat is optional.
+   These four delegates are known to Yices but support for CaDiCaL, CryptoMiniSat, and Kissat is optional.
    They may or may not be available depending on how the Yices library was configured and compiled.
    The "y2sat" delegate is always available.
 
    If *delegate* is NULL, the default SAT solver internal to Yices is used (which can be much slower
    than state-of-the-art solvers such as CaDiCaL).
 
+   The same delegates can also be used through the regular context API
+   --- including with push/pop and ``check-sat-assuming`` --- by setting
+   the ``sat-delegate`` configuration parameter on a QF_BV context. See
+   :ref:`sat_delegate_config`.
+
 
   **Examples**
 

doc/sphinx/source/parameters.rst

@@ -472,3 +472,38 @@ Flattening *(<=> p q)* rewrites the term to *(and (=> p q) (=> q p))*
 
 Flattening *(ite c p q)* rewrites the term to *(and (=> c p) (=> (not c) q)*
 
+
+
+SAT Delegate Selection (QF_BV)
+------------------------------
+
+For QF_BV contexts, the back-end SAT solver --- called a *delegate*
+--- can be selected on a per-check basis through the following
+parameter.
+
+  +------------+-----------------+---------------------------------------------+
+  | Parameter  | Value           |  Meaning                                    |
+  | Name       |                 |                                             |
+  +============+=================+=============================================+
+  | delegate   | none            | use the SAT back-end configured on the      |
+  |            |                 | context (default)                           |
+  |            +-----------------+---------------------------------------------+
+  |            | y2sat           | use y2sat for this check                    |
+  |            +-----------------+---------------------------------------------+
+  |            | cadical         | use CaDiCaL for this check                  |
+  |            +-----------------+---------------------------------------------+
+  |            | cryptominisat   | use CryptoMiniSat for this check            |
+  |            +-----------------+---------------------------------------------+
+  |            | kissat          | use Kissat for this check                   |
+  +------------+-----------------+---------------------------------------------+
+
+If a delegate is set in the parameter record and it differs from the
+delegate configured on the context (see :ref:`sat_delegate_config`),
+the parameter takes effect for that single call only and the persistent
+delegate state of the context is left untouched. If the parameter is
+``"none"``, the context's configured delegate is used.
+
+A delegate name in this parameter has no effect for any logic other
+than QF_BV. Whether a particular delegate is available in the current
+Yices build can be checked with :c:func:`yices_has_delegate`.
+