update html doc

doc/sphinx/source/api-types.rst

@@ -421,64 +421,64 @@ Contexts
    Context state::
 
      typedef enum smt_status {
-       STATUS_IDLE,
-       STATUS_SEARCHING,
-       STATUS_UNKNOWN,
-       STATUS_SAT,
-       STATUS_UNSAT,
-       STATUS_INTERRUPTED,
-       STATUS_ERROR
+       SMT_STATUS_IDLE,
+       SMT_STATUS_SEARCHING,
+       SMT_STATUS_UNKNOWN,
+       SMT_STATUS_SAT,
+       SMT_STATUS_UNSAT,
+       SMT_STATUS_INTERRUPTED,
+       SMT_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:: SMT_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:`SMT_STATUS_UNSAT` if
       the assertions are trivially unsatisfiable. Otherwise, the state
-      remains :c:enum:`STATUS_IDLE`.
+      remains :c:enum:`SMT_STATUS_IDLE`.
 
-   .. c:enum:: STATUS_SEARCHING
+   .. c:enum:: SMT_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:: SMT_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:: SMT_STATUS_SAT
 
       State entered when the search terminates and the assertions are satisfiable.
 
-   .. c:enum:: STATUS_UNSAT
+   .. c:enum:: SMT_STATUS_UNSAT
 
       State entered when the assertions are known to be unsatisfiable.
 
       An unsatisfiability can be detected either when a formula is
       asserted (if the inconsistency is detected by formula
       simplification), or when the search terminates.
 
-   .. c:enum:: STATUS_INTERRUPTED
+   .. c:enum:: SMT_STATUS_INTERRUPTED
 
       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:`SMT_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:`SMT_STATUS_INTERRUPTED`.
 
-   .. c:enum:: STATUS_ERROR
+   .. c:enum:: SMT_STATUS_ERROR
 
       This is an error code. It is returned by functions that operate on a
       context when the operation cannot be performed.

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 SMT_STATUS_SAT:
     printf("The formula is satisfiable\n");
     ...
     break;
 
-  case STATUS_UNSAT:
+  case SMT_STATUS_UNSAT:
     printf("The formula is not satisfiable\n");
     break;
 
-  case STATUS_UNKNOWN:
+  case SMT_STATUS_UNKNOWN:
     printf("The status is unknown\n");
     break;
 
-  case STATUS_IDLE:
-  case STATUS_SEARCHING:
-  case STATUS_INTERRUPTED:
-  case STATUS_ERROR:
+  case SMT_STATUS_IDLE:
+  case SMT_STATUS_SEARCHING:
+  case SMT_STATUS_INTERRUPTED:
+  case SMT_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:`SMT_STATUS_SAT` means that the context is satisfiable.
 
-   - :c:enum:`STATUS_UNSAT` means that the context is not satisfiable.
+   - :c:enum:`SMT_STATUS_UNSAT` means that the context is not satisfiable.
 
-   - :c:enum:`STATUS_UNKNOWN` means that the context's status could
+   - :c:enum:`SMT_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:`SMT_STATUS_SAT` (or
+:c:data:`SMT_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`::