Merge branch 'master' into inc-aufbvnia-iss

SRI-CSL · Dec 21, 2024 · d262617 · d262617
2 parents 9aef38e + 1cb3967
commit d262617
Show file tree

Hide file tree

Showing 194 changed files with 13,266 additions and 2,635 deletions.
diff --git a/.github/actions/test/action.yml b/.github/actions/test/action.yml
@@ -13,4 +13,12 @@ runs:
         # This is needed for yices2 to find libpoly.so.0. /usr/local/lib not searched by default?
         export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH}
         make MODE=${{ inputs.mode }} check
+        make MODE=${{ inputs.mode }} test
+
+    - name: Test Yices API
+      shell: bash
+      if: inputs.mode != 'gcov'
+      run: |
+        # This is needed for yices2 to find libpoly.so.0. /usr/local/lib not searched by default?
+        export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH}
         make MODE=${{ inputs.mode }} check-api
diff --git a/.github/workflows/windows_ci.yml b/.github/workflows/windows_ci.yml
@@ -65,4 +65,5 @@ jobs:
         CYGWIN: winsymlinks:native
       run: >-
         export PATH=/tools/dynamic_gmp/bin:/tools/static_gmp/bin:$PATH &&
-        make OPTION=mingw64 MODE=${{ matrix.mode }} check-api
+        make OPTION=mingw64 MODE=${{ matrix.mode }} check-api &&
+        make OPTION=mingw64 MODE=${{ matrix.mode }} test
diff --git a/Makefile b/Makefile
@@ -56,7 +56,7 @@ YICES_TOP_DIR=$(shell pwd)
 #
 MAJOR = 2
 MINOR = 6
-PATCH_LEVEL = 4
+PATCH_LEVEL = 5
 
 YICES_VERSION = $(MAJOR).$(MINOR).$(PATCH_LEVEL)
 

diff --git a/Makefile.build b/Makefile.build
@@ -89,7 +89,7 @@ srcsubdirs = mt io terms utils solvers solvers/floyd_warshall \
     solvers/funs solvers/bv solvers/egraph solvers/cdcl solvers/simplex solvers/quant \
     parser_utils model api frontend frontend/common \
     frontend/smt1 frontend/yices frontend/smt2 context exists_forall \
-    mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/bv \
+    mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/ff mcsat/bv \
     mcsat/bv/explain mcsat/utils
 
 testdir = tests/unit

diff --git a/doc/manual/manual.tex b/doc/manual/manual.tex
@@ -49,7 +49,7 @@
 \date{\today}
 \author{Bruno Dutertre}
 \title{\textbf{Yices Manual\\[0.6em]
-Version 2.6.4}}
+Version 2.6.5}}
 \end{titlepage}
 
 \maketitle
@@ -811,10 +811,6 @@ \section{Thread-Safe API}
 models across several threads is not supported (unless you implement
 your own locking mechanism).
 
-\medskip\noindent
-In the current version (Yices~2.6.4), threat-safety and MCSAT are not compatible.
-It is not possible to build Yices to support MCSAT and be re-entrant.
-
 
 \section{Building for Windows}
 
@@ -4554,7 +4550,7 @@ \subsection*{Building a Context and Checking Satisfiability}
 
  case STATUS_IDLE:
  case STATUS_SEARCHING:
- case STATUS_INTERRUPTED:
+ case YICES_STATUS_INTERRUPTED:
  case STATUS_ERROR:
    fprintf(stderr, "Error in check_context\n");
    yices_print_error(stderr);

diff --git a/doc/sphinx/source/_static/example1.c b/doc/sphinx/source/_static/example1.c
@@ -127,7 +127,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

diff --git a/doc/sphinx/source/_static/example1b.c b/doc/sphinx/source/_static/example1b.c
@@ -135,7 +135,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

diff --git a/doc/sphinx/source/api-types.rst b/doc/sphinx/source/api-types.rst
@@ -426,7 +426,7 @@ Contexts
        STATUS_UNKNOWN,
        STATUS_SAT,
        STATUS_UNSAT,
-       STATUS_INTERRUPTED,
+       YICES_STATUS_INTERRUPTED,
        STATUS_ERROR
      } smt_status_t;
 
@@ -470,13 +470,13 @@ Contexts
       asserted (if the inconsistency is detected by formula
       simplification), or when the search terminates.
 
-   .. c:enum:: STATUS_INTERRUPTED
+   .. c:enum:: YICES_STATUS_INTERRUPTED
 
       State entered when the search is interrupted.
 
       When a context is in the state :c:enum:`STATUS_SEARCHING` then the search
       can be interrupted through a call to :c:func:`yices_stop_search`. This
-      moves the context's state to :c:enum:`STATUS_INTERRUPTED`.
+      moves the context's state to :c:enum:`YICES_STATUS_INTERRUPTED`.
 
    .. c:enum:: STATUS_ERROR
 

diff --git a/doc/sphinx/source/basic-usage.rst b/doc/sphinx/source/basic-usage.rst
@@ -154,7 +154,7 @@ context, assert ``f`` in this context, then call function :c:func:`yices_check_c
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

diff --git a/doc/sphinx/source/conf.py b/doc/sphinx/source/conf.py
@@ -59,7 +59,7 @@
 # The short X.Y version.
 version = '2.6'
 # The full version, including alpha/beta/rc tags.
-release = '2.6.2'
+release = '2.6.5'
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.

diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst
@@ -550,7 +550,7 @@ assert formulas, check satisfiability, and query the context's status.
      These are the states after a search completes. :c:enum:`STATUS_UNKNOWN` means
      that the search was inconclusive, which may happen if the solver is not complete.
 
-   - :c:enum:`STATUS_INTERRUPTED`.
+   - :c:enum:`YICES_STATUS_INTERRUPTED`.
 
      This state is entered if a search is interrupted.
 
@@ -596,7 +596,7 @@ assert formulas, check satisfiability, and query the context's status.
 
      -- type1 := bool
 
-   - if *ctx*'s state is :c:enum:`STATUS_INTERRUPTED`
+   - if *ctx*'s state is :c:enum:`YICES_STATUS_INTERRUPTED`
 
      -- error code: :c:enum:`CTX_INVALID_OPERATION`
 
@@ -667,13 +667,13 @@ assert formulas, check satisfiability, and query the context's status.
      - :c:enum:`STATUS_UNKNOWN`: the solver can't prove whether the context is
        satisfiable or not.
 
-     - :c:enum:`STATUS_INTERRUPTED`: the search was interrupted by a
+     - :c:enum:`YICES_STATUS_INTERRUPTED`: the search was interrupted by a
        call to :c:func:`yices_stop_search`.
 
      This returned value is also stored as the context's status flag, with the following exception:
 
      - If the context is configured for mode *interactive* and the search is interrupted,
-       then the function returns :c:enum:`STATUS_INTERRUPTED` but the context's state is
+       then the function returns :c:enum:`YICES_STATUS_INTERRUPTED` but the context's state is
        restored to what it was before the call to :c:func:`yices_check_context`, and the
        internal status flag is reset to  :c:enum:`STATUS_IDLE`.
 
@@ -698,7 +698,7 @@ assert formulas, check satisfiability, and query the context's status.
 
    .. note:: If the search is interrupted and the context's mode is
              not *interactive* then the context's enters state
-             :c:enum:`STATUS_INTERRUPTED`. The only way to recover is
+             :c:enum:`YICES_STATUS_INTERRUPTED`. The only way to recover is
              then to call :c:func:`yices_reset_context` or
              :c:func:`yices_pop` (assuming the context supports push and pop).
 
@@ -782,7 +782,7 @@ be removed by :c:func:`yices_pop`.
      -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED`
 
    - if *ctx* supports push and pop but its status is :c:enum:`STATUS_UNSAT`,
-     :c:enum:`STATUS_SEARCHING`, or :c:enum:`STATUS_INTERRUPTED`:
+     :c:enum:`STATUS_SEARCHING`, or :c:enum:`YCIES_STATUS_INTERRUPTED`:
 
      -- error code: :c:enum:`CTX_INVALID_OPERATION`
 

diff --git a/doc/sphinx/source/smt-logics.rst b/doc/sphinx/source/smt-logics.rst
@@ -125,15 +125,24 @@ officially part of SMT-LIB.
    | QF_AUF     | Arrays and Uninterpreted Functions           |
    |            |                                              |
    +------------+----------------------------------------------+
+   | QF_AUFBVLIA| Arrays, Uninterpreted Functions, Bitvectors  |
+   |            | and Linear Integer Arithmetic                |
+   +------------+----------------------------------------------+
    | QF_AUFLRA  | Arrays, Uninterpreted Functions,             |
    |            | Linear Real Arithmetic                       |
    +------------+----------------------------------------------+
    | QF_AUFLIRA | Arrays, Uninterpreted Functions,             |
    |            | Mixed Linear Arithmetic                      |
    +------------+----------------------------------------------+
+   | QF_BVLRA   | Bitvectors, Linear Real Arithmetic           |
+   |            |                                              |
+   +------------+----------------------------------------------+
    | QF_LIRA    | Mixed Linear Arithmetic                      |
    |            |                                              |
    +------------+----------------------------------------------+
+   | QF_UFBVLIA | Uninterpreted Functions, Bitvectors          |
+   |            | Linear Integer Arithmetic                    |
+   +------------+----------------------------------------------+
    | QF_UFLIRA  | Uninterpreted Functions and                  |
    |            | Mixed Linear Arithmetic                      |
    +------------+----------------------------------------------+

diff --git a/doc/yices-sat.1 b/doc/yices-sat.1
@@ -1,4 +1,4 @@
-.TH YICES-SAT 1 "October 2021" "Yices 2.6.4" "User Commands"
+.TH YICES-SAT 1 "June 2024" "Yices 2.6.5" "User Commands"
 .SH NAME
 yices-sat \- the Yices Sat solver
 .SH SYNOPSIS

diff --git a/doc/yices-smt.1 b/doc/yices-smt.1
@@ -1,4 +1,4 @@
-.TH YICES-SMT 1 "October 2021" "Yices 2.6.4" "User Commands"
+.TH YICES-SMT 1 "June 2024" "Yices 2.6.5" "User Commands"
 .SH NAME
 yices-smt \- the Yices SMT solver for the SMT-LIB 1.2 language
 .SH SYNOPSIS

diff --git a/doc/yices-smt2.1 b/doc/yices-smt2.1
@@ -1,4 +1,4 @@
-.TH YICES-SMT2 1 "October 2021" "Yices 2.6.4" "User Commands"
+.TH YICES-SMT2 1 "June 2024" "Yices 2.6.5" "User Commands"
 .SH NAME
 yices-smt2 \- the Yices SMT solver for the SMT-LIB 2 language
 .SH SYNOPSIS

diff --git a/doc/yices.1 b/doc/yices.1
@@ -1,4 +1,4 @@
-.TH YICES 1 "October 2021" "Yices 2.6.4" "User Commands"
+.TH YICES 1 "June 2024" "Yices 2.6.5" "User Commands"
 .SH NAME
 yices \- the Yices SMT solver for the Yices language
 .SH SYNOPSIS

diff --git a/examples/example1.c b/examples/example1.c
@@ -145,7 +145,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

diff --git a/examples/example1b.c b/examples/example1b.c
@@ -157,7 +157,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);

diff --git a/examples/example1c.c b/examples/example1c.c
@@ -150,7 +150,7 @@ static void simple_test(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error_fd(2);

diff --git a/examples/example2.c b/examples/example2.c
@@ -104,7 +104,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

diff --git a/examples/example2b.c b/examples/example2b.c
@@ -124,7 +124,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

diff --git a/examples/example2c.c b/examples/example2c.c
@@ -124,7 +124,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

diff --git a/examples/example2d.c b/examples/example2d.c
@@ -117,7 +117,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

diff --git a/examples/example2e.c b/examples/example2e.c
@@ -117,7 +117,7 @@ int main(void) {
 
   case STATUS_IDLE:
   case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
   case STATUS_ERROR:
     // these codes should not be returned
     printf("Bug: unexpected status returned\n");

diff --git a/examples/example_unsat_core.c b/examples/example_unsat_core.c
@@ -109,7 +109,7 @@ static void check_and_get_core(context_t *ctx, uint32_t n, const term_t *a) {
     yices_delete_term_vector(&core);
     break;
 
-  case STATUS_INTERRUPTED:
+  case YICES_STATUS_INTERRUPTED:
     printf("the check was interrupted\n");
     break;
 

diff --git a/src/Makefile b/src/Makefile
@@ -349,12 +349,16 @@ mcsat_src_c := \
 	mcsat/model.c \
 	mcsat/trail.c \
 	mcsat/conflict.c \
+	mcsat/unit_info.c \
 	mcsat/gc.c \
 	mcsat/eq/equality_graph.c \
 	mcsat/eq/merge_queue.c \
 	mcsat/weq/weak_eq_graph.c \
 	mcsat/utils/int_mset.c \
 	mcsat/utils/int_lset.c \
+	mcsat/utils/lp_data.c \
+	mcsat/utils/lp_utils.c \
+	mcsat/utils/lp_constraint_db.c \
 	mcsat/utils/value_hash_map.c \
 	mcsat/utils/value_vector.c \
 	mcsat/utils/scope_holder.c \
@@ -368,9 +372,13 @@ mcsat_src_c := \
 	mcsat/nra/nra_plugin.c \
 	mcsat/nra/nra_plugin_internal.c \
 	mcsat/nra/nra_plugin_explain.c \
-	mcsat/nra/libpoly_utils.c \
-	mcsat/nra/poly_constraint.c \
+	mcsat/nra/nra_libpoly.c \
 	mcsat/nra/feasible_set_db.c \
+	mcsat/ff/ff_plugin.c \
+	mcsat/ff/ff_plugin_internal.c \
+	mcsat/ff/ff_plugin_explain.c \
+	mcsat/ff/ff_libpoly.c \
+	mcsat/ff/ff_feasible_set_db.c \
 	mcsat/ite/ite_plugin.c \
 	mcsat/bv/bv_plugin.c \
 	mcsat/bv/bv_bdd_manager.c \