API Types
The following types are defined in yices_types.h
and are used
by the API.
Yices Types

type type_t
The type constructors return objects of type
type_t
. This type is defined as follows:typedef int32_t type_t;
Internally, Yices maintains a global table of types and an element of type
type_t
is an index in this global table.

NULL_TYPE
This code is returned by type constructors when an error occurs. Its definition is:
#define NULL_TYPE (1)
This is not a valid index in the global type table.

type type_vector_t
Vector of types. This is a structure defined as follows:
typedef struct type_vector_s { uint32_t capacity; uint32_t size; type_t *data; } type_vector_t;
A type vector v stores a variablesized array of types:
v.capacity is the full size of array v.data
v.size is the number of elements stored in v.data
v.data is a dynamically allocated array that contains the elements
The API provides functions for initializing, emptying, and deleting type vectors. See Vectors.
Yices Terms

type term_t
All term constructors return objects of type
term_t
, which is defined as follows:typedef int32_t term_t;
Internally, Yices stores terms in a global term table and an object of type
term_t
is an index in this table.

NULL_TERM
This special code is returned by term constructors to report an error. It is defined as follows:
#define NULL_TERM (1)

type term_vector_t
Vectors of terms. This is a structure defined as follows:
typedef struct type_vector_s { uint32_t capacity; uint32_t size; type_t *data; } type_vector_t;
A term vector v stores a variablesized array of terms:
v.capacity is the full size of array v.data
v.size is the number of elements stored in v.data
v.data is a dynamically allocated array that contains the elements
See Vectors.

type term_constructor_t
This type gives access to the internal term representation used by Yices. It enumerates the term constructors used internally, and it is the return type of function
yices_term_constructor
.typedef enum term_constructor { YICES_CONSTRUCTOR_ERROR = 1, // atomic terms YICES_BOOL_CONSTANT, YICES_ARITH_CONSTANT, YICES_BV_CONSTANT, YICES_SCALAR_CONSTANT, YICES_VARIABLE, YICES_UNINTERPRETED_TERM, // composite terms YICES_ITE_TERM, YICES_APP_TERM, YICES_UPDATE_TERM, YICES_TUPLE_TERM, YICES_EQ_TERM, YICES_DISTINCT_TERM, YICES_FORALL_TERM, YICES_LAMBDA_TERM, YICES_NOT_TERM, YICES_OR_TERM, YICES_XOR_TERM, YICES_BV_ARRAY, YICES_BV_DIV, YICES_BV_REM, YICES_BV_SDIV, YICES_BV_SREM, YICES_BV_SMOD, YICES_BV_SHL, YICES_BV_LSHR, YICES_BV_ASHR, YICES_BV_GE_ATOM, YICES_BV_SGE_ATOM, YICES_ARITH_GE_ATOM, YICES_ARITH_ROOT_ATOM, YICES_ABS, YICES_CEIL, YICES_FLOOR, YICES_RDIV, YICES_IDIV, YICES_IMOD, YICES_IS_INT_ATOM, YICES_DIVIDES_ATOM, // projections YICES_SELECT_TERM, YICES_BIT_TERM, // sums YICES_BV_SUM, YICES_ARITH_SUM, // products YICES_POWER_PRODUCT } term_constructor_t;
Atomic terms include constants, variables, and uninterpreted terms (i.e., all terms that do not have subterms). For such terms, function
yices_term_constructor
returns one of the following codes:
enum YICES_BOOL_CONSTANT
Boolean constants

enum YICES_ARITH_CONSTANT
Rational constants

enum YICES_BV_CONSTANT
Bitvector constants

enum YICES_SCALAR_CONSTANT
Constants of uninterpreted or scalar type

enum YICES_VARIABLE
Variables in quantifiers and lambda expressions

enum YICES_UNINTERPRETED_TERM
Uninterpreted terms (i.e., global variables)
Composite terms are defined by a constructor and a list of children terms. They can have one of the following constructors:

enum YICES_ITE_TERM
Ifthenelse

enum YICES_APP_TERM
Application of an uninterpreted function

enum YICES_UPDATE_TERM
Function update

enum YICES_TUPLE_TERM
Tuple

enum YICES_EQ_TERM
Binary equality

enum YICES_DISTINCT_TERM
Distinct

enum YICES_FORALL_TERM
Universal quantifier

enum YICES_LAMBDA_TERM
Lambda term

enum YICES_NOT_TERM
Boolean negation

enum YICES_OR_TERM
Nary OR

enum YICES_XOR_TERM
Nary XOR

enum YICES_BV_ARRAY
Bitvector represented as an array of Booleans terms

enum YICES_BV_DIV
Unsigned bitvector division

enum YICES_BV_REM
Remainder in the unsigned bitvector division

enum YICES_BV_SDIV
Signed bitvector division, with rounding to zero

enum YICES_BV_SREM
Remainder in the signed bitvector division

enum YICES_BV_SMOD
Remainder in the signed bitvector division with rounding to minus infinity

enum YICES_BV_SHL
Bitvector shift left

enum YICES_BV_LSHR
Bivector logical shift right

enum YICES_BV_ASHR
Bitvector arithmetic shift right

enum YICES_BV_GE_ATOM
Unsigned bitvector inequality (greater than or equal to)

enum YICES_BV_SGE_ATOM
Signed bitvector inequality

enum YICES_ARITH_GE_ATOM
Arithmetic inequality (greater than or equal to)

enum YICES_ARITH_ROOT_ATOM
Nonlinear arithmetic atom.

enum YICES_ABS
Absolute value

enum YICES_CEIL
Ceiling (i.e., rounding up to the nearest integer)

enum YICES_FLOOR
Floor (i.e., rounding down to the nearest integer)

enum YICES_RDIV
Division

enum YICES_IDIV
Integer division

enum YICES_IMOD
Modulo

enum YICES_IS_INT_ATOM
Integrality test

enum YICES_DIVIDES_ATOM
Divisibility test
Two special constructors are used for projection and bit extraction:

enum YICES_SELECT_TERM
Projection of a tuple term on one component

enum YICES_BIT_TERM
Extraction of the ith bit of a bitvector (as a Boolean)
Arithmetic and bitvector polynomials use the following constructors:

enum YICES_BV_SUM
Sum of the form a_{0} t_{0} + … + a_{n} t_{n} where
all the coefficients a_{i} are bitvector constants
all the terms t_{i} (except possibly t_{0}) are bitvector terms
All terms and coefficients have the same size (i.e., same number of bits).
As a special case, t_{0} may be equal to
NULL_TERM
to encode a constant term. In this case, the sum can be interpreted as a_{0} + a_{1} t_{1} + … + a_{n} t_{n}.

enum YICES_ARITH_SUM
Sum of the form a_{0} t_{0} + … + a_{n} t_{n} where
the coefficients are rational constants
all the terms t_{i} (except possibly t_{0}) are arithmetic terms
As in
YICES_BV_SUM
, the term t_{0} may beNULL_TERM
to encode a constant term.

enum YICES_POWER_PRODUCT
Products of the form t_{0}^d_{0} × … × t_{n}^d_{n} where
the exponents d_{i} are positive integers
the terms t_{i} are either all arithmetic terms or all bitvector terms
The last code is used to report errors:

enum YICES_CONSTRUCTOR_ERROR
This special code is returned by
yices_term_constructor
if its argument is not a valid term.
See Access to Term Components for more details.

enum YICES_BOOL_CONSTANT
Contexts

type context_t
Opaque type of contexts:
typedef struct context_s context_t;
A context is a central data structure in Yices. A context stores a set of formulas to check for satisfiability. The API includes function to initialize and configure contexts, assert formulas in a context, check satisfiability, and construct models from a context.

type ctx_config_t
Contextconfiguration record:
typedef struct ctx_config_s ctx_config_t;
When a context is created, it can be configured to use a specific solver or combination of solvers. One can also specify whether or not the context supports features such as backtracking and removal of formulas (via a push/pop mechanism).
A
ctx_config_t
object describes a context configuration. It is an opaque data structure that lists the solvers to use and the features supported by the context.

type param_t
Parameter record:
typedef struct param_s param_t;
A parameter record stores various parameters that control the heuristics used by the solvers. For example, heuristic parameters can specify the restart strategy employed by the CDCL SAT solver. Other parameters control the branching heuristics, or the generation of theory lemmas by the Simplexbased arithmetic solver.

type smt_status_t
Context state:
typedef enum smt_status { STATUS_IDLE, STATUS_SEARCHING, STATUS_UNKNOWN, STATUS_SAT, STATUS_UNSAT, STATUS_INTERRUPTED, STATUS_ERROR } smt_status_t;
The 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:
enum STATUS_IDLE
Initial context state.
In this state, it is possible to assert formulas in the context. After assertions, the state may change to
STATUS_UNSAT
if the assertions are trivially unsatisfiable. Otherwise, the state remainsSTATUS_IDLE
.

enum STATUS_SEARCHING
State during search.
A context enters this state after a call function
yices_check_context
. It remains in this state until either the solver completes or the search is interrupted.

enum 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.

enum STATUS_SAT
State entered when the search terminates and the assertions are satisfiable.

enum 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.

enum STATUS_INTERRUPTED
State entered when the search is interrupted.
When a context is in the state
STATUS_SEARCHING
then the search can be interrupted through a call toyices_stop_search
. This moves the context’s state toSTATUS_INTERRUPTED
.

enum STATUS_ERROR
This is an error code. It is returned by functions that operate on a context when the operation cannot be performed.

enum STATUS_IDLE
Models

type model_t
Opaque type of models:
typedef struct model_s model_t;
A model is a mapping from uninterpreted terms to constant values. Models can be constructed from a context after checking that the context is satisfiable, or using an explicit modelconstruction function.

type yval_tag_t
The value of a term in a model can be an atomic value, a tuple, or a function. Internally, Yices represents tuple and function values as nodes in a DAG. The API provides functions to compute and examine these nodes, which gives access to the values of terms of function or tuple types. Every node in this DAG has a unique id and a tag of type
yval_tag_t
that defines the node type:typedef enum yval_tag { YVAL_UNKNOWN, YVAL_BOOL, YVAL_RATIONAL, YVAL_ALGEBRAIC, YVAL_BV, YVAL_SCALAR, YVAL_TUPLE, YVAL_FUNCTION, YVAL_MAPPING } yval_tag_t;
These codes are interpreted as follows:

enum YVAL_UNKNOWN
Special tag for the unknown value

enum YVAL_BOOL
Boolean constants

enum YVAL_RATIONAL
Rational constants

enum YVAL_ALGEBRAIC
Algebraic numbers

enum YVAL_BV
Bitvector constants

enum YVAL_SCALAR
Constants of scalar or uninterpreted type

enum YVAL_TUPLE
Tuples of constants

enum YVAL_FUNCTION
Functions

enum YVAL_MAPPING
Mappings of the form [tuple ↦ value] used to represent functions
The tags
YVAL_UNKNOWN
,YVAL_BOOL
,YVAL_RATIONAL
,YVAL_BV
,YVAL_ALGEBRAIC
andYVAL_SCALAR
are attached to leaf nodes in the DAG. The nonleaf nodes have tagsYVAL_TUPLE
,YVAL_FUNCTION
, andYVAL_MAPPING
.The nodes with tag
YVAL_MAPPING
are auxiliary nodes that occur in the definition of functions. In a model, all function values are defined by a finite set of mappings, and a default value. For example, if we havef(0, 0) = 0
f(0, 1) = 1
f(1, 0) = 1
f(x, y) = 2 for all other x and y
then f is represented as follows:
 set of mappings:
 [0, 0 ↦ 0][0, 1 ↦ 1][1, 0 ↦ 1]
default value: 2
The DAG contains a node for f, a node for the default value, and three nodes for each of the three mappings.

enum YVAL_UNKNOWN

type yval_t
This data structure describes a node in the DAG. It consists of a node_id and a node_tag:
typedef struct yval_s { int32_t node_id; yval_tag_t node_tag; } yval_t;
The node_id is a nonnegative integer; all the nodes have different node_ids. The API includes functions for extracting the value encoded in a leaf node and for collecting the children of a nonleaf nodes.

type yval_vector_t
Vector of node descriptors:
typedef struct yval_vector_s { uint32_t capacity; uint32_t size; yval_t *data; } yval_vector_t;
This record is similar to
type_vector_t
andterm_vector_t
:capacity is the full size of the data array
size is the number of nodes stored in data
data is a dynamically allocated array.
This type is used by function
yices_val_expand_function
, which expands a function node.Section Vectors explains how to initialize, reset, and delete these vectors.

type yices_gen_mode_t
Yices includes functions for generalizing a model. Given a model of a formula F(X,Y), generalization is a simplified form of quantifier elimination. It constructs a formula G(X) such that
G(X) is true in the model
G(X) implies (exists Y F(X, Y))
The type
yices_gen_mode_t
lists the different generalization methods implemented in Yices:typedef enum yices_gen_mode { YICES_GEN_DEFAULT, YICES_GEN_BY_SUBST, YICES_GEN_BY_PROJ } yices_gen_mode_t;

enum YICES_GEN_DEFAULT
The default generalization method. This is a either generalization by substitution or generalization by projection, depending on the type of variables to eliminate.

enum YICES_GEN_BY_SUBST
Generalization by substitution. This replaces the variables to eliminate by their value in the model.

enum YICES_GEN_BY_PROJ
Generalization by projection. This is a hybrid of FourierMotzkin elimination and a modelbased variant of virtual term substitution.
See
yices_generalize_model
for more details.
Error Reports

type error_code_t
When a function in the API fails for some reason, it returns a special value (typically a negative number or the
NULL
pointer) and stores an error code in a global record of typeerror_report_t
.The following error codes are defined:

enum NO_ERROR
Everything is fine.

enum INVALID_TYPE
Invalid type argument (not a valid index in the internal type table).

enum INVALID_TERM
Invalid term argument (not a valid index in the internal term table).

enum INVALID_CONSTANT_INDEX
Attempt to create a constant of uninterpreted type with a negative index, or a constant of scalar type with an index that’s larger than the type’s cardinality.

enum INVALID_TUPLE_INDEX
Components of a tuple are indexed from 1 to N. This error code signals that an operation to extract or update a tuple component was given an index outside the interval [1 .. N].

enum INVALID_RATIONAL_FORMAT
The input to
yices_parse_rational
does not have the right format.

enum INVALID_FLOAT_FORMAT
The input to
yices_parse_float
does not have the right format.

enum INVALID_BVBIN_FORMAT
The input to
yices_parse_bvbin
does not have the right format.

enum INVALID_BVHEX_FORMAT
The input to
yices_parse_bvhex
does not have the right format.

enum INVALID_BITSHIFT
Invalid shift amount for a bitvector shift or rotate operation.

enum INVALID_BVEXTRACT
Invalid indices given to function
yices_bvextract
.

enum INVALID_BITEXTRACT
Invalid index given to function
yices_bitextract
.

enum TOO_MANY_ARGUMENTS
Attempt to create a type or term of arity larger than
YICES_MAX_ARITY

enum TOO_MANY_VARS
Attempt to create a quantified term or a lambda term with more than
YICES_MAX_VARS
variables.

enum MAX_BVSIZE_EXCEEDED
Attempt to create a bitvector type or term with more than
YICES_MAX_BVSIZE
bits.

enum DEGREE_OVERFLOW
Attempt to create a polynomial of degree higher than
YICES_MAX_DEGREE
.

enum DIVISION_BY_ZERO
Zero divider in a rational constant.

enum POS_INT_REQUIRED
Bad integer argument: the function expects a positive argument.

enum NONNEG_INT_REQUIRED
Bad integer argument: the function expects a nonnegative argument.

enum SCALAR_OR_UTYPE_REQUIRED
Bad type argument: the function expects either an uninterpreted type or a scalar type.

enum FUNCTION_REQUIRED
Bad term argument: a term of function type is expected.

enum TUPLE_REQUIRED
Bad term argument: a term of tuple type is expected.

enum VARIABLE_REQUIRED
Bad term argument: a variable is expected. Some functions also report this error when they expect an argument that can be either a variable or an uninterpreted term.

enum ARITHTERM_REQUIRED
Bad term argument: an arithmetic term (of type Int or Real) is expected.

enum BITVECTOR_REQUIRED
Bad term argument: a bitvector term is expected.

enum SCALAR_TERM_REQUIRED
Bad term argument: a term of scalar type is expected.

enum WRONG_NUMBER_OF_ARGUMENTS
Wrong number of arguments in a function application or function update.

enum TYPE_MISMATCH
Type error in various term constructor.

enum INCOMPATIBLE_TYPES
Error in functions that require terms of compatible types. The Yices manual explains what this means.

enum DUPLICATE_VARIABLE
Error in quantifier or lambda term constructors: the same variable occurs twice or more.

enum EMPTY_BITVECTOR
Attempt to create a bitvector term of type (bitvector 0).

enum ARITHCONSTANT_REQUIRED
Invalid term: an arithmetic constant is expected.

enum BVTYPE_REQUIRED
Bad type parameter: a bitvector type is expected.

enum BAD_TERM_DECREF
Error in reference counting: attempt to decrement the reference counter of a term when the counter is already zero.

enum BAD_TYPE_DECREF
Error in reference counting: attempt to decrement the reference counter of a type when the counter is already zero.

enum INVALID_TYPE_OP
Error in a typeexploration function.

enum INVALID_TERM_OP
Error in a termexploration function.

enum INVALID_TOKEN
Error in the lexer.

enum SYNTAX_ERROR
Syntax error.

enum UNDEFINED_TYPE_NAME
A name is not defined in the symbol table for types.

enum UNDEFINED_TERM_NAME
A name is not defined in the symbol table for terms.

enum REDEFINED_TYPE_NAME
Attempt to redefine an existing type name.

enum REDEFINED_TERM_NAME
Attempt to redefine an existing term name.

enum DUPLICATE_NAME_IN_SCALAR
A scalartype definition contains the same element name twice (or more).

enum DUPLICATE_VAR_NAME
Error in quantifiers or lambda term definition: the same variable name occurs twice or more.

enum INTEGER_OVERFLOW
Integer constant can’t be converted to a signed 32bit integer.

enum INTEGER_REQUIRED
Rational constant provided when an integer is expected.

enum RATIONAL_REQUIRED
Invalid argument: a rational constant is expected.

enum SYMBOL_REQUIRED
Error in a definition or local declaration: a symbol is expected.

enum TYPE_REQUIRED
Error in a definition or declaration: a type is expected.

enum NON_CONSTANT_DIVISOR
Attempt to divide by a nonconstant arithmetic term.

enum NEGATIVE_BVSIZE
Error while parsing
(bitvector size)
: the size is negative.

enum INVALID_BVCONSTANT
Error while parsing
(mkbv size value)
: the value is negative.

enum TYPE_MISMATCH_IN_DEF
Error in a term definition: the term value does not have the declared type.

enum ARITH_ERROR
Error in an arithmetic operation: an argument is not an arithmetic term.

enum BVARITH_ERROR
Error in a bitvector operation: an argument is not a bitvector.

enum CTX_FREE_VAR_IN_FORMULA
An assertion contains free variables.

enum CTX_LOGIC_NOT_SUPPORTED
An assertion is not in a logic for which the context was configured.

enum CTX_UF_NOT_SUPPORTED
An assertion contains uninterpreted functions but the context does not support them.

enum CTX_ARITH_NOT_SUPPORTED
An assertion contains arithmetic terms but the context does not support arithmetic.

enum CTX_BV_NOT_SUPPORTED
An assertion contains bitvector terms but the context does not support bitvectors.

enum CTX_ARRAYS_NOT_SUPPORTED
An assertion contains array or function updates but the context does not support arrays.

enum CTX_QUANTIFIERS_NOT_SUPPORTED
An assertion contains quantifiers but the context does not support them.

enum CTX_LAMBDAS_NOT_SUPPORTED
An assertion contains lambda terms but the context does not support them.

enum CTX_NONLINEAR_ARITH_NOT_SUPPORTED
An assertion contains nonlinear polynomials but the context supports only linear arithmetic.

enum CTX_FORMULA_NOT_IDL
The context is configured for integer difference logic but an assertion is not in this fragment.

enum CTX_FORMULA_NOT_RDL
The context is configured for real difference logic but an assertion is not in this fragment.

enum CTX_TOO_MANY_ARITH_VARS
An internal limit of the arithmetic solver is exceeded.

enum CTX_TOO_MANY_ARITH_ATOMS
An internal limit of the arithmetic solver is exceeded.

enum CTX_TOO_MANY_BV_VARS
An internal limit of the bitvector solver is exceeded.

enum CTX_TOO_MANY_BV_ATOMS
An internal limit of the bitvector solver is exceeded.

enum CTX_ARITH_SOLVER_EXCEPTION
General error reported by the arithmetic solver.

enum CTX_BV_SOLVER_EXCEPTION
General error reported by the bitvector solver.

enum CTX_ARRAY_SOLVER_EXCEPTION
General error reported by the array/function solver.

enum CTX_SCALAR_NOT_SUPPORTED
An assertion contains terms of scalar type but the context does not support them.

enum CTX_TUPLE_NOT_SUPPORTED
An assertion contains terms of tuple type but the context does not support them.

enum CTX_UTYPE_NOT_SUPPORTED
An assertion contains terms of uninterpreted type but the context does not support them.

enum CTX_INVALID_OPERATION
Invalid operation on a context: the context is in a state that does not allow the operation to be performed.

enum CTX_OPERATION_NOT_SUPPORTED
Invalid operation on a context: the context is not configured to support this operation.

enum CTX_UNKNOWN_DELEGATE
A delegate name is not recognized. See
yices_check_formula
andyices_check_formulas
.

enum CTX_DELEGATE_NOT_AVAILABLE
Attempt to use a delegate that was not included in the Yices library at compilation time.

enum CTX_INVALID_CONFIG
Reported by
yices_new_context
if the requested configuration is not supported. This means that the combination of solvers does not implement the set of features requested.

enum CTX_UNKNOWN_PARAMETER
Invalid parameter name.

enum CTX_INVALID_PARAMETER_VALUE
Invalid value for a parameter.

enum CTX_UNKNOWN_LOGIC
A logic name is not recognized.

enum EVAL_UNKNOWN_TERM
The model does not assign a value to the specified term.

enum EVAL_FREEVAR_IN_TERM
A term value cannot be computed because the term contains free variables.

enum EVAL_QUANTIFIER
A term value cannot be computed because the term contains quantifiers.

enum EVAL_LAMBDA
A term value cannot be computed because the term contains lambdas.

enum EVAL_FAILED
A term value cannot be computed for another reason.

enum EVAL_OVERFLOW
The value of a term is known but it does not fit in the given variable. For example,
yices_get_int32_value
will report this error if the term value does not fit in a signed, 32bit integer.

enum EVAL_CONVERSION_FAILED
Failed to convert the value of a term in a model into a constant term. This error can be reported by
yices_get_value_as_term
andyices_term_array_value
.

enum EVAL_NO_IMPLICANT
Error reported by
yices_implicant_for_formula
and variants when the input formula is false in the model.

enum EVAL_NOT_SUPPORTED
Reported by function
yices_get_algebraic_number_value
when the library is compiled without MCSAT support.

enum MDL_UNINT_REQUIRED
Invalid map for
yices_model_from_map
: an element in the domain is not an uninterpreted term.

enum MDL_CONSTANT_REQUIRED
Invalid map for
yices_model_from_map
: an element in the range is not a constant term.

enum MDL_DUPLICATE_VAR
Invalid map for
yices_model_from_map
: the domain contains duplicate terms.

enum MDL_FTYPE_NOT_ALLOWED
Invalid map for
yices_model_from_map
: one element in the domain has a function type.

enum MDL_CONSTRUCTION_FAILED
Function
yices_model_from_map
failed for some other reason.

enum MDL_GEN_TYPE_NOT_SUPPORTED
Model generalization failed because variables to eliminate have a type that’s not supported.

enum MDL_GEN_NONLINEAR
Model generalization failed because the input formula(s) include nonlinear arithmetic.

enum MDL_GEN_FAILED
Model generalization failed for some other reason.

enum YVAL_INVALID_OP
Invalid operation on a value descriptor (node in the model DAG).

enum YVAL_OVERFLOW
The value of a leaf node does not fit in the given input variable.

enum YVAL_NOT_SUPPORTED
Reported by function
yices_val_get_algebraic_number
when the library is compiled without MCSAT support.

enum MCSAT_ERROR_UNSUPPORTED_THEORY
A formula asserted in the MCSAT solver is not in a theory that this solver can process.

enum OUTPUT_ERROR
Error when attempting to write to a stream. This error can be reported by the prettyprinting functions if they fail to write to the specified file.
If this error is reported, then system variables and functions (e.g.,
errno
,perror
,strerror
) can be used for diagnosis.

enum INTERNAL_EXCEPTION
Catchall code for any other error.
If you ever see this error code, please report a bug at https://github.com/SRICSL/yices2
A few more error codes are defined in
yices_types.h
. They are related to type macros that Yices uses to support the SMTLIB 2 sort constructors. Type macros are not exposed in the API.
enum NO_ERROR

type error_report_t
A global record stores information about the errors reported by the API. The data includes the error code as defined previously (cf.
error_code_t
) and additional information that can be used for diagnosis:typedef struct error_report_s { error_code_t code; uint32_t line; uint32_t column; term_t term1; type_t type1; term_t term2; type_t type2; int64_t badval; } error_report_t;
The code is always set. The other meaningful fields depend on the error code:
the parsing functions
yices_parse_type
andyices_parse_term
set the line and column fields to help locate the error in the input string.the field badval is set when an incorrect integer argument is provided
the other fields are set by terms and type constructors