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 variable-sized 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 variable-sized 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¶: If-then-else

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¶: N-ary OR

enum YICES_XOR_TERM¶: N-ary 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 i-th bit of a bitvector (as a Boolean)

Arithmetic and bitvector polynomials use the following constructors:

enum YICES_BV_SUM¶

Sum of the form a₀ t₀ + … + a_n t_n where

all the coefficients a_i are bitvector constants

all the terms t_i (except possibly t₀) are bitvector terms

All terms and coefficients have the same size (i.e., same number of bits).

As a special case, t₀ may be equal to NULL_TERM to encode a constant term. In this case, the sum can be interpreted as a₀ + a₁ t₁ + … + a_n t_n.

enum YICES_ARITH_SUM¶

Sum of the form a₀ t₀ + … + a_n t_n where

the coefficients are rational constants

all the terms t_i (except possibly t₀) are arithmetic terms

As in YICES_BV_SUM, the term t₀ may be NULL_TERM to encode a constant term.

enum YICES_POWER_PRODUCT¶

Products of the form t₀^d₀ × … × 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.

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¶

Context-configuration 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 Simplex-based 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 remains STATUS_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 to yices_stop_search. This moves the context’s state to STATUS_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.

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 model-construction 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 and YVAL_SCALAR are attached to leaf nodes in the DAG. The non-leaf nodes have tags YVAL_TUPLE, YVAL_FUNCTION, and YVAL_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.

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 non-negative 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 non-leaf 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 and term_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 Fourier-Motzkin elimination and a model-based 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 type error_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 non-negative 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 type-exploration function.

enum INVALID_TERM_OP¶: Error in a term-exploration 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 scalar-type 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 non-constant arithmetic term.

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

enum INVALID_BVCONSTANT¶: Error while parsing (mk-bv 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 non-linear 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 and yices_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_EF_ASSERTIONS_CONTAIN_UF¶: Uninterpreted functions not supported by the exists/forall solver.

enum CTX_EF_NOT_EXISTS_FORALL¶: Assertions are not in the exists/forall fragment.

enum CTX_EF_HIGH_ORDER_VARS¶: High-order and tuple variables are not supported.

enum CTX_EF_INTERNAL_ERROR¶: The exists/forall solver failed.

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 and yices_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 non-linear 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 pretty-printing 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¶

Catch-all code for any other error.

If you ever see this error code, please report a bug at https://github.com/SRI-CSL/yices2

A few more error codes are defined in yices_types.h. They are related to type macros that Yices uses to support the SMT-LIB 2 sort constructors. Type macros are not exposed in the API.

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 and yices_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

Table of contents

Previous topic

Next topic