From 72790d658f9ef01169a13b903a509a4350cf5323 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Sat, 8 Jul 2023 03:40:36 -0700 Subject: [PATCH 1/6] install guide for kissat --- doc/sphinx/source/install-sources.rst | 44 ++++++++++++++++++++++----- 1 file changed, 36 insertions(+), 8 deletions(-) diff --git a/doc/sphinx/source/install-sources.rst b/doc/sphinx/source/install-sources.rst index b7f231092..a2121268c 100644 --- a/doc/sphinx/source/install-sources.rst +++ b/doc/sphinx/source/install-sources.rst @@ -177,14 +177,18 @@ Third-Party SAT Solvers ----------------------- Yices can use third-party SAT solvers as backends to the bit-vector -solvers. We call these *delegates*. Currently two third-party solvers -are supported +solvers. Currently one internal and three third-party solvers are +supported -1. Armin Biere's `CaDiCal `_ +1. Internal y2sat SAT solver (default solver) -2. Mate Soos' `CryptoMiniSAT `_ +2. Armin Biere's `CaDiCal `_ -You can compile Yices with one or both of these SAT solvers. +3. Mate Soos' `CryptoMiniSAT `_ + +4. Armin Biere's `Kissat (patched version) `_ + +You can also compile Yices with any of these SAT solvers. Install CaDiCaL ............... @@ -235,16 +239,34 @@ This will install CryptoMiniSAT in ``/usr/local/``. There are more detailed build instructions in the CryptoMiniSAT ``README``. +Install Kissat +.............. + +We provide a patched version of Kissat that fixes an issue. Download +this patched version at https://github.com/BrunoDutertre/kissat. The +original is at https://github.com/arminbiere/kissat. To compile the +code, follow these instructions: + +.. code-block:: sh + + git clone https://github.com/BrunoDutertre/kissat + cd kissat + ./configure -fPIC + make + sudo install build/libkissat.a /usr/local/lib + sudo install -m644 src/kissat.h /usr/local/include + + Configure and Build Yices with Third-Party Solvers .................................................. -To build Yices with support for both CaDiCaL and CryptoMiniSAT, use the following +To build Yices with support for all third-party solvers, use the following configure command in the top-level yices source directory: .. code-block:: sh - ./configure CPPFLAGS='-DHAVE_CADICAL -DHAVE_CRYPTOMINISAT' \ - LIBS=’-lcryptominisat5 -lcadical -lstdc++ -lm’ + ./configure CPPFLAGS='-DHAVE_CADICAL -DHAVE_CRYPTOMINISAT -DHAVE_KISSAT' \ + LIBS=’-lcryptominisat5 -lcadical -lkissat -lstdc++ -lm’ If you want only CaDiCaL: @@ -258,6 +280,12 @@ If you want only CryptoMiniSAT: ./configure CPPFLAGS=-DHAVE_CRYPTOMINISAT LIBS=’-lcryptominisat5 -lstdc++’ +If you want only Kissat, use this command: + +.. code-block:: sh + + ./configure CPPFLAGS=-DHAVE_KISSAT LIBS=’-lkissat -lm’ + After any of these ``configure`` commands, you can build Yices as usual: .. code-block:: sh From 9cc62e7fbd482ae457269ce4887f9f18f4dcd79b Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Sun, 9 Jul 2023 13:22:37 -0700 Subject: [PATCH 2/6] add missing EF errors --- doc/sphinx/source/api-types.rst | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/doc/sphinx/source/api-types.rst b/doc/sphinx/source/api-types.rst index c2e80456a..e0194090a 100644 --- a/doc/sphinx/source/api-types.rst +++ b/doc/sphinx/source/api-types.rst @@ -1014,6 +1014,22 @@ Error Reports Attempt to use a delegate that was not included in the Yices library at compilation time. + .. c:enum:: CTX_EF_ASSERTIONS_CONTAIN_UF + + Uninterpreted functions not supported by the exists/forall solver. + + .. c:enum:: CTX_EF_NOT_EXISTS_FORALL + + Assertions are not in the exists/forall fragment. + + .. c:enum:: CTX_EF_HIGH_ORDER_VARS + + High-order and tuple variables are not supported. + + .. c:enum:: CTX_EF_INTERNAL_ERROR + + The exists/forall solver failed. + .. c:enum:: CTX_INVALID_CONFIG Reported by :c:func:`yices_new_context` if the requested From 9b2129c2db29374bea00b625977193332b935699 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Tue, 11 Jul 2023 14:52:32 -0700 Subject: [PATCH 3/6] interpolats in the context doc --- doc/sphinx/source/context-operations.rst | 189 ++++++++++++++++++++++- 1 file changed, 183 insertions(+), 6 deletions(-) diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst index c918c7f1e..364e3b0fa 100644 --- a/doc/sphinx/source/context-operations.rst +++ b/doc/sphinx/source/context-operations.rst @@ -111,8 +111,8 @@ If you configure a context for a logic such as ``"QF_NRA"`` or ``"QF_UFNIA"`` then MCSat will be automatically selected. The MCSat solver does not currently support as many features as the -DPLL(T) implementation. In particular, MCSat does not yet support push -and pop. +DPLL(T) implementation. In particular, MCSat does not yet support +computing unsat cores. **Theory Solvers** @@ -222,14 +222,12 @@ each call to :c:func:`yices_check_context`. This introduces overhead, but the context can be restored to a clean state if the search is interrupted. -Currently, MCSat supports only mode one-shot. - For DPLL(T), the four operating modes can be used, except if a Floyd-Warshal theory solver is used. The Floyd-Warshal solvers are specialized for difference logic and support only mode one-shot. -The default mode is push-pop for DPLL(T) and one-shot for MCSat. +The default mode is push-pop. @@ -842,7 +840,6 @@ returns the core in a term vector. A full example is in file :file:`examples/example_unsat_core.c` included in the Yices distribution. - .. c:function:: smt_status_t yices_check_context_with_assumptions(context_t* ctx, const param_t* params, uint32_t n, const term_t t[]) Checks whether *n* assumptions are satisfiable in a context *ctx*. @@ -935,6 +932,186 @@ distribution. +Check Modulo a Model and Model Interpolant +------------------------------------------ + +When checking satisfiability, it is possible to provide a partial +model such that the satisfiability is checked for the assertions in +conjunction with the provided model. To use this functionality, the +context must be a context initialized with support for MCSAT (see +yices_new_context, yices_new_config, yices_set_config). +Here is an example:: + + ctx_config_t* config = yices_new_config(); + yices_set_config(config, "solver-type", "mcsat"); + context_t *ctx = yices_new_context(config); + yices_assert_formula(ctx, f); + status = yices_check_context_with_model(ctx, NULL, model, 5, a); + +In this fragment, we first create a yices configuration ``config`` +then we set its parameter ``solver-type`` to ``mcsat``. Then, we +create a context ``ctx`` using ``config``. After that we assert a +formula ``f``. In the call to check, we give an array of five +uninterpreted terms ``a[0]``, ..., ``a[4]``. This amounts to checking +the conjunction of ``f`` and the equalities between the unintpreted +terms and their value in the ``model``. + +The check modulo a model provides an additional functionality, namely, +the construction of a model interpolant, if the yices context is +unsatisfiable and supports model interpolation (see +yices_set_config). This model interpolant is constructed by calling +:c:func:`yices_get_model_interpolant`. + + +.. c:function:: smt_status_t yices_check_context_with_model(context_t* ctx, const param_t* params, model_t *mdl, uint32_t n, const term_t t[]) + + Checks whether *n* assumptions are satisfiable in a context *ctx*. + + **Parameters** + + - *ctx* is a context + + - *params* is an optional structure to a search-parameter structure. + + - *mdl* is a model + + - *n* is the number of assumptions + + - *t* is an array of *n* uninterpreted terms + + The *params* structure controls search heuristics. If *params* is NULL, default + settings are used. See :ref:`params` and :c:func:`yices_check_context`. + + This function checks statisfiability of the constraints in ctx + conjoined with a conjunction of equalities defined by *t[i]* and the + model, namely, + + *t[0] == v_0 /\ .... /\ t[n-1] = v_{n-1}*, + + where *v_i* is the value of *t[i]* in *mdl*. + + NOTE: if *t[i]* does not have a value in *mdl*, then a default value is + picked for *v_i*. + + If this function returns STATUS_UNSAT and the context supports + model interpolation, then one can construct a model interpolant by + calling function :c:func:`yices_get_model_interpolant`. + + More precisely: + + - If *ctx*'s current status is :c:enum:`STATUS_UNSAT` then the function does nothing + and returns :c:enum:`STATUS_UNSAT`. + + - If *ctx*'s status is :c:enum:`STATUS_IDLE`, :c:enum:`STATUS_SAT`, + or :c:enum:`STATUS_UNKNOWN` then the function checks whether + *ctx* conjoined with the *n* equalities given by *mdl* and *t* is + satisfiable. This is done even if *n* is zero. The function will + then return a code as in :c:func:`yices_check_context`. + + - If *ctx*'status is anything else, the function returns :c:enum:`STATUS_ERROR`. + + + This operation fails and returns :c:enum:`STATUS_ERROR` if *ctx* is + configured for one-shot solving and *ctx*'s status is anything + other than :c:enum:`STATUS_IDLE`. + + **Error report** + + - If one of the terms *t[i]* is not an uninterpreted: + + -- error code: :c:enum:`MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED` + + - If the context does not have the MCSAT solver enabled: + + -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` + + - If the resulting status is :c:enum:`STATUS_SAT` and context does not support multichecks: + + -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` + +.. c:function:: term_t yices_get_model_interpolant(context_t* ctx) + + Construct and return a model interpolant. + + **Parameters** + + - *ctx* is a context + + + If *ctx* status is unsat and the context was configured with model-interpolation, + this function returns a model interpolant. + Otherwise, it sets an error code and return NULL_TERM. + + This is intended to be used after a call to + :c:func:`yices_check_context_with_model` that returned + :c:enum:`STATUS_UNSAT`. In this case, the function builds an model + interpolant. The model interpolant is a clause implied by the + current context that is false in the model provides to + :c:func:`yices_check_context_with_model`. + + **Error report** + + - If the context is not configured with model interpolation: + + -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` + + - If the context's status is not :c:enum:`STATUS_UNSAT`: + + -- error code: :c:enum:`CTX_INVALID_OPERATION` + + +Check and Compute Interpolant +----------------------------- + +It is possible to check assertions and compute an interpolant if the +assertions are unsatisfiable. This functionality requires having two +contexts that are stored in a *interpolation_context*. The +*interpolation_context* is a struct with four components defined +as follows:: + + typedef struct interpolation_context_s { + context_t *ctx_A; + context_t *ctx_B; + term_t interpolant; + model_t *model; + } interpolation_context_t; + + +.. c:function:: smt_status_t yices_check_context_with_interpolation(interpolation_context_t *ctx, const param_t *params, int32_t build_model) + + Check satisfiability and compute interpolant. + + **Parameters** + + - *ctx* is a interpolation context + + - *params* is an optional structure to a search-parameter structure. + + - *build_model* is a Boolean flag + + The *params* structure controls search heuristics. If *params* is NULL, default + settings are used. See :ref:`params` and :c:func:`yices_check_context`. + + To call this function: + + - *ctx->ctx_A* must be a context initialized with support for MCSAT and interpolation. + + - *ctx->ctx_B* can be another context (not necessarily with MCSAT support). + + If this function returns :c:enum:`STATUS_UNSAT`, then an + interpolant is returned in *ctx->interpolant*. + + If this function returns :c:enum:`STATUS_SAT` and *build_model* is + true, then a model is returned in *ctx->model*. This model must be + freed when no-longer needed by calling :c:func:`yices_free_model`. + + **Error report** + + - If something is wrong: + + -- error code: :c:enum:`CTX_INVALID_OPERATION` + + .. _params: Search Parameters From 3608896a95864875983df28dc0aa561c6f90d93a Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Wed, 12 Jul 2023 18:04:21 -0700 Subject: [PATCH 4/6] rm push/pop comment about mcsat --- src/include/yices.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/include/yices.h b/src/include/yices.h index 8d42843b0..2ed8a1735 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -2654,8 +2654,7 @@ __YICES_DLLSPEC__ extern void yices_garbage_collect(const term_t t[], uint32_t n * - mcsat: solver based on the Model-Constructing Satisfiability Calculus * * The "mcsat" solver is required for formulas that use non-linear - * arithmetic. Currently the mcsat solver does not support push and - * pop. If you select "mcsat" as the solver type, no other + * arithmetic. If you select "mcsat" as the solver type, no other * configuration is necessary. * * If you select "dpllt" as the solver type, then you can define the From cfcd69072d0796e3e535f33355b2cd561fcc3ff9 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Mon, 17 Jul 2023 04:38:30 -0700 Subject: [PATCH 5/6] add comment about mcsat unsat cores --- doc/sphinx/source/context-operations.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst index 364e3b0fa..f1e2a6c02 100644 --- a/doc/sphinx/source/context-operations.rst +++ b/doc/sphinx/source/context-operations.rst @@ -112,7 +112,9 @@ then MCSat will be automatically selected. The MCSat solver does not currently support as many features as the DPLL(T) implementation. In particular, MCSat does not yet support -computing unsat cores. +computing unsat cores. However, unsat cores in MCSat can be computed +using :c:func:`yices_check_context_with_model` and +:c:func:`yices_get_model_interpolant`. **Theory Solvers** From 75bb08dc778bb4a024ed63ee57e8e506cae64758 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Mon, 17 Jul 2023 04:40:55 -0700 Subject: [PATCH 6/6] fix typo --- doc/sphinx/source/context-operations.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst index f1e2a6c02..d64598a09 100644 --- a/doc/sphinx/source/context-operations.rst +++ b/doc/sphinx/source/context-operations.rst @@ -876,7 +876,7 @@ distribution. with the *n* assumptions is satisfiable. This is done even if *n* is zero. The function will then return a code as in :c:func:`yices_check_context`. - - If *ctx*'status is anything else, the function returns :c:enum:`STATUS_ERROR`. + - If *ctx*'s status is anything else, the function returns :c:enum:`STATUS_ERROR`. This operation fails and returns :c:enum:`STATUS_ERROR` if *ctx* is