Merge branch 'master' into fix-iss-414

Author: ahmed-irfan

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/ff mcsat/bv \
+    mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/na mcsat/ff mcsat/bv \
     mcsat/bv/explain mcsat/utils
 
 testdir = tests/unit

doc/sphinx/source/_static/example1.c

@@ -86,7 +86,7 @@ static void simple_test(void) {
   }
 
   switch (yices_check_context(ctx, NULL)) { // call check_context, NULL means 'use default heuristics'
-  case STATUS_SAT:
+  case YICES_STATUS_SAT:
     printf("The formula is satisfiable\n");
     model_t* model = yices_get_model(ctx, true);  // get the model
     if (model == NULL) {
@@ -117,18 +117,18 @@ static void simple_test(void) {
     }
     break;
 
-  case STATUS_UNSAT:
+  case YICES_STATUS_UNSAT:
     printf("The formula is not satisfiable\n");
     break;
 
-  case STATUS_UNKNOWN:
+  case YICES_STATUS_UNKNOWN:
     printf("The status is unknown\n");
     break;
 
-  case STATUS_IDLE:
-  case STATUS_SEARCHING:
+  case YICES_STATUS_IDLE:
+  case YICES_STATUS_SEARCHING:
   case YICES_STATUS_INTERRUPTED:
-  case STATUS_ERROR:
+  case YICES_STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);
     break;

doc/sphinx/source/_static/example1b.c

@@ -93,7 +93,7 @@ static void simple_test(void) {
   }
 
   switch (yices_check_context(ctx, NULL)) { // call check_context, NULL means 'use default heuristics'
-  case STATUS_SAT:
+  case YICES_STATUS_SAT:
     printf("The formula is satisfiable\n");
     model = yices_get_model(ctx, 1);  // get the model
     if (model == NULL) {
@@ -125,18 +125,18 @@ static void simple_test(void) {
     }
     break;
 
-  case STATUS_UNSAT:
+  case YICES_STATUS_UNSAT:
     printf("The formula is not satisfiable\n");
     break;
 
-  case STATUS_UNKNOWN:
+  case YICES_STATUS_UNKNOWN:
     printf("The status is unknown\n");
     break;
 
-  case STATUS_IDLE:
-  case STATUS_SEARCHING:
+  case YICES_STATUS_IDLE:
+  case YICES_STATUS_SEARCHING:
   case YICES_STATUS_INTERRUPTED:
-  case STATUS_ERROR:
+  case YICES_STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);
     break;

doc/sphinx/source/api-types.rst

@@ -421,48 +421,48 @@ Contexts
    Context state::
 
      typedef enum smt_status {
-       STATUS_IDLE,
-       STATUS_SEARCHING,
-       STATUS_UNKNOWN,
-       STATUS_SAT,
-       STATUS_UNSAT,
+       YICES_STATUS_IDLE,
+       YICES_STATUS_SEARCHING,
+       YICES_STATUS_UNKNOWN,
+       YICES_STATUS_SAT,
+       YICES_STATUS_UNSAT,
        YICES_STATUS_INTERRUPTED,
-       STATUS_ERROR
+       YICES_STATUS_ERROR
      } smt_status_t;
 
    The type :c:type:`smt_status_t` enumerates the possible states of a
    context. It is also the type returned by the function that checks
    whether a context is satisfiable. The following codes are defined:
 
-   .. c:enum:: STATUS_IDLE
+   .. c:enum:: YICES_STATUS_IDLE
 
       Initial context state.
 
       In this state, it is possible to assert formulas in the context.
-      After assertions, the state may change to :c:enum:`STATUS_UNSAT` if
+      After assertions, the state may change to :c:enum:`YICES_STATUS_UNSAT` if
       the assertions are trivially unsatisfiable. Otherwise, the state
-      remains :c:enum:`STATUS_IDLE`.
+      remains :c:enum:`YICES_STATUS_IDLE`.
 
-   .. c:enum:: STATUS_SEARCHING
+   .. c:enum:: YICES_STATUS_SEARCHING
 
       State during search.
 
       A context enters this state after a call function
       :c:func:`yices_check_context`.  It remains in this state until
       either the solver completes or the search is interrupted.
 
-   .. c:enum:: STATUS_UNKNOWN
+   .. c:enum:: YICES_STATUS_UNKNOWN
 
       State entered when the search terminates but is inconclusive.
 
       This may happen if the context's solver is not complete for the specific
       logic used. For example, the logic may have quantifiers.
 
-   .. c:enum:: STATUS_SAT
+   .. c:enum:: YICES_STATUS_SAT
 
       State entered when the search terminates and the assertions are satisfiable.
 
-   .. c:enum:: STATUS_UNSAT
+   .. c:enum:: YICES_STATUS_UNSAT
 
       State entered when the assertions are known to be unsatisfiable.
 
@@ -474,11 +474,11 @@ Contexts
 
       State entered when the search is interrupted.
 
-      When a context is in the state :c:enum:`STATUS_SEARCHING` then the search
+      When a context is in the state :c:enum:`YICES_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:`YICES_STATUS_INTERRUPTED`.
 
-   .. c:enum:: STATUS_ERROR
+   .. c:enum:: YICES_STATUS_ERROR
 
       This is an error code. It is returned by functions that operate on a
       context when the operation cannot be performed.
@@ -674,7 +674,7 @@ Error Reports
 
    The following error codes are defined:
 
-   .. c:enum:: NO_ERROR
+   .. c:enum:: YICES_NO_ERROR
 
       Everything is fine.
 

doc/sphinx/source/basic-usage.rst

@@ -139,23 +139,23 @@ context, assert ``f`` in this context, then call function :c:func:`yices_check_c
   }
 
   switch (yices_check_context(ctx, NULL)) {
-  case STATUS_SAT:
+  case YICES_STATUS_SAT:
     printf("The formula is satisfiable\n");
     ...
     break;
 
-  case STATUS_UNSAT:
+  case YICES_STATUS_UNSAT:
     printf("The formula is not satisfiable\n");
     break;
 
-  case STATUS_UNKNOWN:
+  case YICES_STATUS_UNKNOWN:
     printf("The status is unknown\n");
     break;
 
-  case STATUS_IDLE:
-  case STATUS_SEARCHING:
+  case YICES_STATUS_IDLE:
+  case YICES_STATUS_SEARCHING:
   case YICES_STATUS_INTERRUPTED:
-  case STATUS_ERROR:
+  case YICES_STATUS_ERROR:
     fprintf(stderr, "Error in check_context\n");
     yices_print_error(stderr);
     break;
@@ -167,11 +167,11 @@ function :c:func:`yices_assert_formula` asserts a formula in the
 context. Function :c:func:`yices_check_context` returns a code of type
 :c:type:`smt_status_t`:
 
-   - :c:enum:`STATUS_SAT` means that the context is satisfiable.
+   - :c:enum:`YICES_STATUS_SAT` means that the context is satisfiable.
 
-   - :c:enum:`STATUS_UNSAT` means that the context is not satisfiable.
+   - :c:enum:`YICES_STATUS_UNSAT` means that the context is not satisfiable.
 
-   - :c:enum:`STATUS_UNKNOWN` means that the context's status could
+   - :c:enum:`YICES_STATUS_UNKNOWN` means that the context's status could
      not be determined.
 
 Other codes are error conditions.
@@ -183,8 +183,8 @@ Once the context ``ctx`` is no longer needed, we delete it using :c:func:`yices_
 Building and Querying a Model
 -----------------------------
 
-If :c:func:`yices_check_context` returns :c:data:`STATUS_SAT` (or
-:c:data:`STATUS_UNKNOWN`), we can construct a model of the asserted
+If :c:func:`yices_check_context` returns :c:data:`YICES_STATUS_SAT` (or
+:c:data:`YICES_STATUS_UNKNOWN`), we can construct a model of the asserted
 formulas by calling :c:func:`yices_get_model`. We then display the
 model using :c:func:`yices_pp_model`::