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

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

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

If-then-else

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

N-ary OR

YICES_XOR_TERM

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

Arithmetic and bitvector polynomials use the following constructors:

YICES_BV_SUM

Sum of the form a0 t0 + … + an tn where

  • all the coefficients ai are bitvector constants
  • all the terms ti (except possibly t0) are bitvector terms

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

As a special case, t0 may be equal to NULL_TERM to encode a constant term. In this case, the sum can be interpreted as a0 + a1 t1 + … + an tn.

YICES_ARITH_SUM

Sum of the form a0 t0 + … + an tn where

  • the coefficients are rational constants
  • all the terms ti (except possibly t0) are arithmetic terms

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

YICES_POWER_PRODUCT

Products of the form t0^d0 × … × tn^dn where

  • the exponents di are positive integers
  • the terms ti 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

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.

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.

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 remains STATUS_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 to yices_stop_search. This moves the context’s state to STATUS_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 model-construction 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_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_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, 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.

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.

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.

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

INVALID_TERM_OP

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

NEGATIVE_BVSIZE

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

INVALID_BVCONSTANT

Error while parsing (mk-bv 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 non-linear 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 and yices_term_array_value.

EVAL_NO_IMPLICANT

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

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 non-linear 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.

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.

INTERNAL_EXCEPTION

Catch-all code for any other error.

If you ever see this error code, please send a bug report at

yices-bugs@csl.sri.com.

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.

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