diff --git a/doc/sphinx/source/api-types.rst b/doc/sphinx/source/api-types.rst index e0194090a..e1bfa855f 100644 --- a/doc/sphinx/source/api-types.rst +++ b/doc/sphinx/source/api-types.rst @@ -421,29 +421,29 @@ 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. @@ -451,18 +451,18 @@ Contexts :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. @@ -470,15 +470,15 @@ Contexts 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. diff --git a/doc/sphinx/source/basic-usage.rst b/doc/sphinx/source/basic-usage.rst index 6ca952cbd..50d93248c 100644 --- a/doc/sphinx/source/basic-usage.rst +++ b/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`:: diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst index c1eb7f583..a12a71ca0 100644 --- a/doc/sphinx/source/context-operations.rst +++ b/doc/sphinx/source/context-operations.rst @@ -533,24 +533,24 @@ assert formulas, check satisfiability, and query the context's status. The returned value is one of the following codes: - - :c:enum:`STATUS_IDLE`. This is the initial state. + - :c:enum:`SMT_STATUS_IDLE`. This is the initial state. In this state, it is possible to assert formulas. The state may - then change to :c:enum:`STATUS_UNSAT` if the assertions are + then change to :c:enum:`SMT_STATUS_UNSAT` if the assertions are trivially unsatisfiable Otherwise, the state remains - :c:enum:`STATUS_IDLE`. + :c:enum:`SMT_STATUS_IDLE`. - - :c:enum:`STATUS_SEARCHING`. This is the context state during search. + - :c:enum:`SMT_STATUS_SEARCHING`. This is the context state during search. The context enters this state on a call to :c:func:`yices_check_context` and remains in this state until the solver completes or the search is interrupted. - - :c:enum:`STATUS_SAT`, :c:enum:`STATUS_UNSAT`, :c:enum:`STATUS_UNKNOWN`. + - :c:enum:`SMT_STATUS_SAT`, :c:enum:`SMT_STATUS_UNSAT`, :c:enum:`SMT_STATUS_UNKNOWN`. - These are the states after a search completes. :c:enum:`STATUS_UNKNOWN` means + These are the states after a search completes. :c:enum:`SMT_STATUS_UNKNOWN` means that the search was inconclusive, which may happen if the solver is not complete. - - :c:enum:`STATUS_INTERRUPTED`. + - :c:enum:`SMT_STATUS_INTERRUPTED`. This state is entered if a search is interrupted. @@ -566,17 +566,17 @@ assert formulas, check satisfiability, and query the context's status. The term *t* must be Boolean. The context *ctx* must be in one of the following states: - :c:enum:`STATUS_IDLE`, :c:enum:`STATUS_UNSAT`, - :c:enum:`STATUS_SAT`, or :c:enum:`STATUS_UNKNOWN`. + :c:enum:`SMT_STATUS_IDLE`, :c:enum:`SMT_STATUS_UNSAT`, + :c:enum:`SMT_STATUS_SAT`, or :c:enum:`SMT_STATUS_UNKNOWN`. - - if the current state is :c:enum:`STATUS_UNSAT`, this function does nothing. + - if the current state is :c:enum:`SMT_STATUS_UNSAT`, this function does nothing. - otherwise, the formula *t* is simplified and asserted in the context. The context's state - is then changed to :c:enum:`STATUS_UNSAT` if the assertion simplifies to false, or to - :c:enum:`STATUS_IDLE` otherwise. + is then changed to :c:enum:`SMT_STATUS_UNSAT` if the assertion simplifies to false, or to + :c:enum:`SMT_STATUS_IDLE` otherwise. If the context is in mode *one-shot*, this function fails if the state is either - :c:enum:`STATUS_SAT` or :c:enum:`STATUS_UNKNOWN`. + :c:enum:`SMT_STATUS_SAT` or :c:enum:`SMT_STATUS_UNKNOWN`. The function returns 0 if there's no error, or -1 otherwise. @@ -596,11 +596,11 @@ 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:`SMT_STATUS_INTERRUPTED` -- error code: :c:enum:`CTX_INVALID_OPERATION` - - if *ctx*'s mode is *one-shot* and *ctx*'s state is neither :c:enum:`STATUS_IDLE` nor :c:enum:`STATUS_UNSAT` + - if *ctx*'s mode is *one-shot* and *ctx*'s state is neither :c:enum:`SMT_STATUS_IDLE` nor :c:enum:`SMT_STATUS_UNSAT` -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` @@ -620,9 +620,9 @@ assert formulas, check satisfiability, and query the context's status. - *t* must be an array of *n* Boolean terms. - The context must be in state :c:enum:`STATUS_IDLE`, - :c:enum:`STATUS_UNSAT`, :c:enum:`STATUS_SAT`, or - :c:enum:`STATUS_UNKNOWN`. + The context must be in state :c:enum:`SMT_STATUS_IDLE`, + :c:enum:`SMT_STATUS_UNSAT`, :c:enum:`SMT_STATUS_SAT`, or + :c:enum:`SMT_STATUS_UNKNOWN`. This function is equivalent to calling :c:func:`yices_assert_formula` with input *(and t[0] ... t[n-1])*. @@ -649,10 +649,10 @@ assert formulas, check satisfiability, and query the context's status. This function's behavior and returned value depend on *ctx*'s current state. - - If the state is :c:enum:`STATUS_SAT`, :c:enum:`STATUS_UNSAT`, or :c:enum:`STATUS_UNKNOWN`, + - If the state is :c:enum:`SMT_STATUS_SAT`, :c:enum:`SMT_STATUS_UNSAT`, or :c:enum:`SMT_STATUS_UNKNOWN`, the function just returns this status. - - If the state is :c:enum:`STATUS_IDLE`, then the context's solver + - If the state is :c:enum:`SMT_STATUS_IDLE`, then the context's solver (as defined by the context's configuration) searches for a satisfying assignment to all the assertions stored in *ctx*. If *params* is not :c:macro:`NULL`, the solver uses the @@ -660,25 +660,25 @@ assert formulas, check satisfiability, and query the context's status. Then the function returns one of the following codes: - - :c:enum:`STATUS_UNSAT`: the context is not satisfiable. + - :c:enum:`SMT_STATUS_UNSAT`: the context is not satisfiable. - - :c:enum:`STATUS_SAT`: the context is satisfiable. + - :c:enum:`SMT_STATUS_SAT`: the context is satisfiable. - - :c:enum:`STATUS_UNKNOWN`: the solver can't prove whether the context is + - :c:enum:`SMT_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:`SMT_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:`SMT_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`. + internal status flag is reset to :c:enum:`SMT_STATUS_IDLE`. - If *ctx* is in another state, the function - returns :c:enum:`STATUS_ERROR`. + returns :c:enum:`SMT_STATUS_ERROR`. **Error report** @@ -693,12 +693,12 @@ assert formulas, check satisfiability, and query the context's status. This function can be called from a signal handler to stop the search after at call to :c:func:`yices_check_context`. If the - context's state is :c:enum:`STATUS_SEARCHING` then the search is + context's state is :c:enum:`SMT_STATUS_SEARCHING` then the search is interrupted, otherwise the function does nothing. .. 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:`SMT_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). @@ -708,7 +708,7 @@ assert formulas, check satisfiability, and query the context's status. Resets a context. This function removes all the assertions stored in *ctx* and resets - the context's state to :c:enum:`STATUS_IDLE`. + the context's state to :c:enum:`SMT_STATUS_IDLE`. .. c:function:: int32_t yices_assert_blocking_clause(context_t* ctx) @@ -718,19 +718,19 @@ assert formulas, check satisfiability, and query the context's status. This function is intended to enumerate different models for a set of assertions. - - If *ctx*'s status is either :c:enum:`STATUS_SAT` or - :c:enum:`STATUS_UNKNOWN`, then a new clause is asserted in *ctx* + - If *ctx*'s status is either :c:enum:`SMT_STATUS_SAT` or + :c:enum:`SMT_STATUS_UNKNOWN`, then a new clause is asserted in *ctx* to remove the current truth assignment. After this clause is added, the next call to :c:func:`yices_check_context` will either produce a different truth assignment (hence a different model) or - return :c:enum:`STATUS_UNSAT`. + return :c:enum:`SMT_STATUS_UNSAT`. After adding the clause, the context's state is updated to either - :c:enum:`STATUS_IDLE` (if the clause is not empty) or to - :c:enum:`STATUS_UNSAT` if the blocking clause is empty. + :c:enum:`SMT_STATUS_IDLE` (if the clause is not empty) or to + :c:enum:`SMT_STATUS_UNSAT` if the blocking clause is empty. - - If *ctx*'s status is not :c:enum:`STATUS_SAT` or :c:enum:`STATUS_UNKNOWN`, + - If *ctx*'s status is not :c:enum:`SMT_STATUS_SAT` or :c:enum:`SMT_STATUS_UNKNOWN`, the function reports an error. This function is not supported if the context's mode is *one-shot*. @@ -739,7 +739,7 @@ assert formulas, check satisfiability, and query the context's status. **Error report** - - if *ctx*'s status is different from :c:enum:`STATUS_SAT` and :c:enum:`STATUS_UNKNOWN` + - if *ctx*'s status is different from :c:enum:`SMT_STATUS_SAT` and :c:enum:`SMT_STATUS_UNKNOWN` -- error code: :c:enum:`CTX_INVALID_OPERATION` @@ -770,8 +770,8 @@ be removed by :c:func:`yices_pop`. This function starts a new assertion level. The *ctx* must be configured to support push and pop, and its state must be either - :c:enum:`STATUS_IDLE`, or :c:enum:`STATUS_SAT`, or - :c:enum:`STATUS_UNKNOWN`. + :c:enum:`SMT_STATUS_IDLE`, or :c:enum:`SMT_STATUS_SAT`, or + :c:enum:`SMT_STATUS_UNKNOWN`. The function returns 0 if the operation succeeds or -1 otherwise. @@ -781,8 +781,8 @@ 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`: + - if *ctx* supports push and pop but its status is :c:enum:`SMT_STATUS_UNSAT`, + :c:enum:`SMT_STATUS_SEARCHING`, or :c:enum:`SMT_STATUS_INTERRUPTED`: -- error code: :c:enum:`CTX_INVALID_OPERATION` @@ -803,7 +803,7 @@ be removed by :c:func:`yices_pop`. -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` - - if *ctx*'s status is :c:enum:`STATUS_SEARCHING` or if the assertion level is zero: + - if *ctx*'s status is :c:enum:`SMT_STATUS_SEARCHING` or if the assertion level is zero: -- error code: :c:enum:`CTX_INVALID_OPERATION` @@ -862,26 +862,26 @@ distribution. The function checks whether all assertions currently asserted in *ctx* together with the *n* assumptions *t[0]* |...| *t[n-1]* are satisfiable, and returns the result as a status code. If the - function returns :c:enum:`STATUS_UNSAT` then one can compute an + function returns :c:enum:`SMT_STATUS_UNSAT` then one can compute an unsat core (i.e., a subset of the assumptions that is unsatisfiable) by calling :c:func:`yices_get_unsat_core`. 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 current status is :c:enum:`SMT_STATUS_UNSAT` then the function does nothing + and returns :c:enum:`SMT_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 + - If *ctx*'s status is :c:enum:`SMT_STATUS_IDLE`, :c:enum:`SMT_STATUS_SAT`, + or :c:enum:`SMT_STATUS_UNKNOWN` then the function checks whether *ctx* conjoined 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*'s status is anything else, the function returns :c:enum:`STATUS_ERROR`. + - If *ctx*'s status is anything else, the function returns :c:enum:`SMT_STATUS_ERROR`. - This operation fails and returns :c:enum:`STATUS_ERROR` if *ctx* is + This operation fails and returns :c:enum:`SMT_STATUS_ERROR` if *ctx* is configured for one-shot solving and *ctx*'s status is anything - other than :c:enum:`STATUS_IDLE`. + other than :c:enum:`SMT_STATUS_IDLE`. **Error report** @@ -906,7 +906,7 @@ distribution. - *v* must be an initialized term vector (see :c:func:`yices_init_term_vector`). The function checks whether *ctx*'s status is - :c:enum:`STATUS_UNSAT`. If so, it computes and unsat core and store + :c:enum:`SMT_STATUS_UNSAT`. If so, it computes and unsat core and store it in vector *v*. The unsat core is an subset of the assumptions passed to the most recent call to :c:func:`yices_check_context_with_assumptions`. @@ -923,12 +923,12 @@ distribution. There are no duplicates in the *v->data* array. - If *ctx*'s status is anything other than :c:enum:`STATUS_UNSAT`, + If *ctx*'s status is anything other than :c:enum:`SMT_STATUS_UNSAT`, the function leaves *v* unchanged and returns -1. **Error report** - - If *ctx*'s status is not :c:enum:`STATUS_UNSAT` + - If *ctx*'s status is not :c:enum:`SMT_STATUS_UNSAT` -- error code: :c:enum:`CTX_INVALID_OPERATION` @@ -1001,21 +1001,21 @@ yices_set_config). This model interpolant is constructed by calling 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 current status is :c:enum:`SMT_STATUS_UNSAT` then the function does nothing + and returns :c:enum:`SMT_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 + - If *ctx*'s status is :c:enum:`SMT_STATUS_IDLE`, :c:enum:`SMT_STATUS_SAT`, + or :c:enum:`SMT_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*'s status is anything else, the function returns :c:enum:`STATUS_ERROR`. + - If *ctx*'s status is anything else, the function returns :c:enum:`SMT_STATUS_ERROR`. - This operation fails and returns :c:enum:`STATUS_ERROR` if *ctx* is + This operation fails and returns :c:enum:`SMT_STATUS_ERROR` if *ctx* is configured for one-shot solving and *ctx*'s status is anything - other than :c:enum:`STATUS_IDLE`. + other than :c:enum:`SMT_STATUS_IDLE`. **Error report** @@ -1027,7 +1027,7 @@ yices_set_config). This model interpolant is constructed by calling -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` - - If the resulting status is :c:enum:`STATUS_SAT` and context does not support multichecks: + - If the resulting status is :c:enum:`SMT_STATUS_SAT` and context does not support multichecks: -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` @@ -1046,7 +1046,7 @@ yices_set_config). This model interpolant is constructed by calling 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 + :c:enum:`SMT_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`. @@ -1057,7 +1057,7 @@ yices_set_config). This model interpolant is constructed by calling -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED` - - If the context's status is not :c:enum:`STATUS_UNSAT`: + - If the context's status is not :c:enum:`SMT_STATUS_UNSAT`: -- error code: :c:enum:`CTX_INVALID_OPERATION` @@ -1100,10 +1100,10 @@ as follows:: - *ctx->ctx_B* can be another context (not necessarily with MCSAT support). - If this function returns :c:enum:`STATUS_UNSAT`, then an + If this function returns :c:enum:`SMT_STATUS_UNSAT`, then an interpolant is returned in *ctx->interpolant*. - If this function returns :c:enum:`STATUS_SAT` and *build_model* is + If this function returns :c:enum:`SMT_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`. diff --git a/doc/sphinx/source/formula-operations.rst b/doc/sphinx/source/formula-operations.rst index 3022eec0f..7cdbe1dd9 100644 --- a/doc/sphinx/source/formula-operations.rst +++ b/doc/sphinx/source/formula-operations.rst @@ -31,9 +31,9 @@ third-party Boolean satisfiability solvers for bit-vector problems. Check satisfiability of formula *f* - This returns :c:enum:`STATUS_SAT` if *f* is satisfiable, - :c:enum:`STATUS_UNSAT` if *f* is not satisfiable, - or :c:enum:`STATUS_ERROR` if there is an error. + This returns :c:enum:`SMT_STATUS_SAT` if *f* is satisfiable, + :c:enum:`SMT_STATUS_UNSAT` if *f* is not satisfiable, + or :c:enum:`SMT_STATUS_ERROR` if there is an error. **Parameters** @@ -92,7 +92,7 @@ third-party Boolean satisfiability solvers for bit-vector problems. model_t *result; smt_status_t status = yices_check_formula(f, "QF_LRA", &result, NULL); - if (status == STATUS_SAT) { + if (status == SMT_STATUS_SAT) { // a model is returned in result yices_pp_model(stdout, result, 100, 100, 0); ... @@ -198,7 +198,7 @@ to DIMACS cannot be performed as no CNF is constructed. The following two functions process formulas in the QF_BV logic. They first perform preprocessing and simplification. If the formulas are solved by this preprocessing, the functions return the status (either -:c:enum:`STATUS_SAT` or :c:enum:`STATUS_UNSAT`). Otherwise, the +:c:enum:`SMT_STATUS_SAT` or :c:enum:`SMT_STATUS_UNSAT`). Otherwise, the functions construct a CNF formula and write it to a file. Optionally, the functions can perform an extra round of simplification to the CNF formula before exporting it. diff --git a/doc/sphinx/source/model-operations.rst b/doc/sphinx/source/model-operations.rst index ec723d792..8b73e5136 100644 --- a/doc/sphinx/source/model-operations.rst +++ b/doc/sphinx/source/model-operations.rst @@ -37,7 +37,7 @@ Model Construction - *keep_subst*: flag to indicates whether the model should include eliminated variables - The context's status must be either :c:enum:`STATUS_SAT` or :c:enum:`STATUS_UNKNOWN`. + The context's status must be either :c:enum:`SMT_STATUS_SAT` or :c:enum:`SMT_STATUS_UNKNOWN`. When assertions are added to a context, the simplification procedures may eliminate variables by substitution (see @@ -54,7 +54,7 @@ Model Construction **Error report** - - if *ctx*'s status is not :c:enum:`STATUS_SAT` or :c:enum:`STATUS_UNKNOWN` + - if *ctx*'s status is not :c:enum:`SMT_STATUS_SAT` or :c:enum:`SMT_STATUS_UNKNOWN` -- error code: :c:enum:`CTX_INVALID_OPERATION` @@ -147,7 +147,7 @@ Model Construction Here is an example use of this function:: yices_assert_formula(ctx, f); - if (yices_check(ctx, ...) == STATUS_SAT) { + if (yices_check(ctx, ...) == SMT_STATUS_SAT) { term_vector_t v; model_t *m = yices_get_model(ctx, true); yices_init_term_vector(&v);