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

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_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

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)

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.

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:
YICES_BOOL_CONSTANT
Boolean constants

YICES_ARITH_CONSTANT
Rational constants

YICES_BV_CONSTANT
Bitvector constants

YICES_SCALAR_CONSTANT
Constants of uninterpreted or scalar type

YICES_VARIABLE
Variables in quantifiers and lambda expressions

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:

YICES_ITE_TERM
Ifthenelse

YICES_APP_TERM
Application of an uninterpreted function

YICES_UPDATE_TERM
Function update

YICES_TUPLE_TERM
Tuple

YICES_EQ_TERM
Binary equality

YICES_DISTINCT_TERM
Distinct

YICES_FORALL_TERM
Universal quantifier

YICES_LAMBDA_TERM
Lambda term

YICES_NOT_TERM
Boolean negation

YICES_OR_TERM
Nary OR

YICES_XOR_TERM
Nary XOR

YICES_BV_ARRAY
Bitvector represented as an array of Booleans terms

YICES_BV_DIV
Unsigned bitvector division

YICES_BV_REM
Remainder in the unsigned bitvector division

YICES_BV_SDIV
Signed bitvector division, with rounding to zero

YICES_BV_SREM
Remainder in the signed bitvector division

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

YICES_BV_SHL
Bitvector shift left

YICES_BV_LSHR
Bivector logical shift right

YICES_BV_ASHR
Bitvector arithmetic shift right

YICES_BV_GE_ATOM
Unsigned bitvector inequality (greater than or equal to)

YICES_BV_SGE_ATOM
Signed bitvector inequality

YICES_ARITH_GE_ATOM
Arithmetic inequality (greater than or equal to)

YICES_ARITH_ROOT_ATOM
Nonlinear arithmetic atom.

YICES_ABS
Absolute value

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

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

YICES_RDIV
Division

YICES_IDIV
Integer division

YICES_IMOD
Modulo

YICES_IS_INT_ATOM
Integrality test

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

YICES_SELECT_TERM
Projection of a tuple term on one component

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

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

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.

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:

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.

Contexts

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.

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.

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.

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

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.

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.

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

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.

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
.

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

Models

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.

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_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:

YVAL_UNKNOWN
Special tag for the unknown value

YVAL_BOOL
Boolean constants

YVAL_RATIONAL
Rational constants

YVAL_ALGEBRAIC
Algebraic numbers

YVAL_BV
Bitvector constants

YVAL_SCALAR
Constants of scalar or uninterpreted type

YVAL_TUPLE
Tuples of constants

YVAL_FUNCTION
Functions

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 have f(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.


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.

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.

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;

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.

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

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

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:

NO_ERROR
Everything is fine.

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

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

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.

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

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

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

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

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

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

INVALID_BVEXTRACT
Invalid indices given to function
yices_bvextract
.

INVALID_BITEXTRACT
Invalid index given to function
yices_bitextract
.

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

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

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

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

DIVISION_BY_ZERO
Zero divider in a rational constant.

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

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

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

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

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

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.

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

BITVECTOR_REQUIRED
Bad term argument: a bitvector term is expected.

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

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

TYPE_MISMATCH
Type error in various term constructor.

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

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

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

ARITHCONSTANT_REQUIRED
Invalid term: an arithmetic constant is expected.

BVTYPE_REQUIRED
Bad type parameter: a bitvector type is expected.

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

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

INVALID_TYPE_OP
Error in a typeexploration function.

INVALID_TERM_OP
Error in a termexploration function.

INVALID_TOKEN
Error in the lexer.

SYNTAX_ERROR
Syntax error.

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

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

REDEFINED_TYPE_NAME
Attempt to redefine an existing type name.

REDEFINED_TERM_NAME
Attempt to redefine an existing term name.

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

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

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

INTEGER_REQUIRED
Rational constant provided when an integer is expected.

RATIONAL_REQUIRED
Invalid argument: a rational constant is expected.

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

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

NON_CONSTANT_DIVISOR
Attempt to divide by a nonconstant arithmetic term.

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

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

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

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

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

CTX_FREE_VAR_IN_FORMULA
An assertion contains free variables.

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

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

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

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

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

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

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

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

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

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

CTX_TOO_MANY_ARITH_VARS
An internal limit of the arithmetic solver is exceeded.

CTX_TOO_MANY_ARITH_ATOMS
An internal limit of the arithmetic solver is exceeded.

CTX_TOO_MANY_BV_VARS
An internal limit of the bitvector solver is exceeded.

CTX_TOO_MANY_BV_ATOMS
An internal limit of the bitvector solver is exceeded.

CTX_ARITH_SOLVER_EXCEPTION
General error reported by the arithmetic solver.

CTX_BV_SOLVER_EXCEPTION
General error reported by the bitvector solver.

CTX_ARRAY_SOLVER_EXCEPTION
General error reported by the array/function solver.

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

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

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

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

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

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.

CTX_UNKNOWN_PARAMETER
Invalid parameter name.

CTX_INVALID_PARAMETER_VALUE
Invalid value for a parameter.

CTX_UNKNOWN_LOGIC
A logic name is not recognized.

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

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

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

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

EVAL_FAILED
A term value cannot be computed for another reason.

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.

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
.

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

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

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

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

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

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

MDL_CONSTRUCTION_FAILED
Function
yices_model_from_map
failed for some other reason.

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

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

MDL_GEN_FAILED
Model generalization failed for some other reason.

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

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

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

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

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.

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.

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
 the parsing functions