Contexts
Contexts are one of the most important data structures in Yices. A context contains one or more solvers and supports operations for manipulating assertions and for checking whether these assertions are satisfiable. If they are, a model can be constructed from the context.
Yices allows several contexts to be created and manipulated independently. The API provides functions for
creating and configuring a context
asserting formulas in a context
checking whether a context is satisfiable
building a model from a satisfiable context
deleting a context
A context can be configured to support a push/pop mechanism, which organizes the assertions in a stack to support incremental solving and backtracking.
Creation and Configuration
The simplest way to create a context is as follows:
context_t *ctx = yices_new_context(NULL);
This creates a new context in the default configuration. This context includes theory solvers for linear arithmetic, bitvectors, uninterpreted functions, and arrays. The context supports the push/pop mechanism and the arithmetic solver can handle mixed integer and real linear arithmetic.
To use a more specialized set of solvers, one can configure the context for a specific logic. Here is an example:
ctx_config_t *config = yices_new_config();
yices_default_config_for_logic(config, "QF_LRA");
context_t *ctx = yices_new_context(config);
yices_free_config(config);
In this case, we pass a nonNULL configuration descriptor to function
yices_new_context
to specify the logic. Logics are
identified by their SMTLIB name. In this example, QF_LRA means
quantifierfree linear real arithmetic. This configuration creates a
context with a single theory solver, namely, the Simplexbased solver
for linear arithmetic. As previously, the context supports the
push/pop mechanism.
If push and pop are not needed, we can change the configuration as follows:
ctx_config_t *config = yices_new_config();
yices_default_config_for_logic(config, "QF_LRA");
yices_set_config(config, "mode", "oneshot");
context_t *ctx = yices_new_context(config);
yices_free_config(config);
The call to yices_set_config
changes the context’s mode of
operation from the default (i.e., support for push and pop) to a more
restricted mode where push and pop are not supported. In this mode,
the context can use more aggressive simplification and preprocessing
procedures, which can improve solver performance.
The general process to configure a context is as follows:
Allocate a configuration descriptor by a call to
yices_new_config
.Set configuration parameters by repeated calls to
yices_set_config
or by callingyices_default_config_for_logic
.Create one or more contexts with this configuration by passing the descriptor to function
yices_new_context
.Delete the configuration descriptor when it is no longer needed using
yices_free_config
.
Configuration Parameters
Configuration parameters specify the theory solvers to use, the arithmetic fragment, and the context’s operating mode.
Solver Types
Yices includes two main types of solvers. One is based on the DPLL(T) approach to SMT solving [NOT2006]. The other relies on the ModelConstructing Satisfiability Calculus (MCSat) [dMJ2013].
Currently, DPLL(T) is the default, except for logics that include
nonlinear arithmetic. MCSat is required for nonlinear arithmetic and
for combination of nonlinear arithmetic and uninterpreted functions.
If you configure a context for a logic such as "QF_NRA"
or "QF_UFNIA"
then MCSat will be automatically selected.
The MCSat solver does not currently support as many features as the DPLL(T) implementation. In particular, MCSat does not yet support push and pop.
Theory Solvers
A context that uses DPLL(T) can be further configured to select one or more theory solvers. Currently the following theory solvers are available:
Solver name
Theory
egraph
uninterpreted functions
array solver
arrays + extensionality
simplex
linear arithmetic
integer FloydWarshall (IFW)
integer difference logic
real FloydWarshall (RFW)
real difference logic
bitvector
bitvector theory
A configuration selects a subset of these solvers. Not all combinations make sense. For example, there can be only one arithmetic solver so it’s not possible to have both a FloydWarshall solver and the Simplex solver in the same context. The following table lists the combinations of theory solvers currently supported by Yices.
Combination
no solvers at all
egraph alone
bitvector alone
simplex alone
IFW alone
RFW alone
egraph + bitvector
egraph + array solver
egraph + simplex solver
egraph + bitvector + array solver
egraph + simplex + array solver
egraph + bitvector + simplex + array solver
If no solvers are used, the context can deal only with Boolean formulas. By default, a DPLL(T) context uses egraph, bitvector, simplex, and the array solver (last row in the table).
Arithmetic Fragment
When the Simplex solver is used, it is possible to specify an arithmetic fragment:
Fragment
Meaning
IDL
Integer Difference Logic
RDL
Real Difference Logic
LRA
Real Linear Arithmetic
LIA
Integer Linear Arithmetic
LIRA
Mixed Linear Arithmetic (Integer/Real)
The arithmetic fragment is ignored if there is no arithmetic solver or if the arithmetic solver is one of the FloydWarshall solvers. The default fragment is LIRA.
Operating Mode
In addition to the solver combination, a context can be configured for different usages.
In mode oneshot, assertions are not allowed after a call to function
yices_check_context
. This mode is useful to check satisfiability of a single block of assertions and possibly construct a model if the assertions are satisfiable.In mode multicheck, the context can be used to check incremental blocks of assertions. It is possible to add assertions after a call to
yices_check_context
but it is not possible to retract assertions.In mode pushpop, the context maintains assertions in a stack and it is possible to add and later retract assertions.
The mode interactive provides the same functionalities as pushpop. In addition, the context can recover gracefully if a search is interrupted.
In the first two modes, Yices employs more aggressive simplifications
when processing assertions, which can lead to better performance. In
the interactive mode, the current state of the context is saved before
each call to yices_check_context
. This introduces overhead,
but the context can be restored to a clean state if the search is
interrupted.
Currently, MCSat supports only mode oneshot.
For DPLL(T), the four operating modes can be used, except if a FloydWarshal theory solver is used. The FloydWarshal solvers are specialized for difference logic and support only mode oneshot.
The default mode is pushpop for DPLL(T) and oneshot for MCSat.
Configuration Descriptor
A configuration descriptor is a record that stores solver type, operating mode, arithmetic fragment, and solver combination.
A first parameter specifies the solver type:
Name
Value
Meaning
solvertype
dpllt
use DPLL(T) approach
mcsat
use MCSat
Four configuration parameters describe the theory solvers:
Name
Value
Meaning
ufsolver
none
no UF solver
default
use the egraph
bvsolver
none
no bitvector solver
default
use the bitvector solver
arraysolver
none
no array solver
default
use the array solver
arithsolver
none
no arithmetic solver
ifw
integer FloydWarshall
rfw
real FloydWarshall
simplex
simplex solver
default
same as simplex
auto
same as simplex unless mode=oneshot and logic is QF_IDL or QF_RDL
Two more parameters in the configuration descriptor specify the arithmetic fragment and the operating mode:
Name
Possible values
arithfragment
IDL, RDL, LRA, LIA, or LIRA
mode
oneshot, multichecks, pushpop, or interactive
A configuration descriptor also stores a logic flag, which can either be unknown (i.e., no logic specified), or the name of an SMTLIB logic, or the special name NONE. If this logic flag is set (i.e., not unknown), it takes precedence over solver type and the four solverselection parameters listed in the previous table. If the logic involves nonlinear arithmetic, then MCSat is automatically selected. Otherwise, DPLL(T) is selected and the solver combination is determined by the logic.
The special logic name NONE means no theory solvers. If this logic is chosen, the context is configured to deal with purely Boolean problems, using DPLL.
If the logic is QF_IDL or QF_RDL and the mode is oneshot, then one
can set the arithsolver to auto. In this setting, the actual
arithmetic solver is selected when yices_check_context
is
called, based on the assertions. Depending on the number of
constraints and variables, Yices will either pick the FloydWarshall
solver for IDL or RDL, or the generic Simplexbased solver.
The following functions allocate configuration records and set parameters and logic.

ctx_config_t *yices_new_config(void)
Allocates a contextconfiguration record.
This functions returns a new configuration record, initialized for the default configuration.

void yices_free_config(ctx_config_t *config)
Deletes a configuration record.

int32_t yices_set_config(ctx_config_t *config, const char *name, const char *value)
Sets a contextconfiguration parameter.
Parameters
config must be a pointer to a configuration record returned by
yices_new_config
name must be the name of a configuration parameter
value is the value for the parameter
The name and value must be spelled as shown in the previous two tables. For example, to set the arithmetic solver to the FloydWarshall solver for QF_IDL, call:
yices_set_config(config, "arithsolver", "ifw");
The function returns 1 if there’s an error or 0 otherwise.
Error report
if name is not a known parameter name
– error code:
CTX_UNKNOWN_PARAMETER
if value is not valid for the parameter name
– error code:
CTX_INVALID_PARAMETER_VALUE

int32_t yices_default_config_for_logic(ctx_config_t *config, const char *logic)
Prepares a context configuration for a specified logic.
Parameters
config must be a pointer to a configuration record returned by
yices_new_config
logic must be either the name of a logic or the string
"NONE"
If logic is
"NONE"
then no theory solvers are included, and the context can only process purely Boolean assertions. Otherwise logic must be the name of an SMTLIB logic. The logics recognized and supported by Yices are listed in SMT Logics.If the logic is unrecognized or unsupported, the function leaves the configuration record unchanged and returns 1. It returns 0 otherwise.
Error code
if the logic is not recognized
– error code:
CTX_UNKNOWN_LOGIC
if the logic is known but not supported
– error code:
CTX_LOGIC_NOT_SUPPORTED
Context Creation and Deletion

context_t *yices_new_context(const ctx_config_t *config)
Creates a new context.
This function allocates and initializes a new context and returns (a pointer to) it.
Parameter
config: configuration record or
NULL
If config is
NULL
, the returned context is configured to use the default solver combination, arithmetic fragment, and operating mode.Otherwise, the function checks whether the specified configuration is valid and supported. If it is, the context is configured as specified. If the configuration is not valid, the function returns
NULL
and sets the error report.A configuration may be invalid if it requests a solver combination that is not supported (for example, the array solver but no egraph), or if the operating mode is not supported by the solvers (e.g., mode is pushpop and arithsolver is ifw).
Error report
if config is not valid
– error code:
CTX_INVALID_CONFIG

void yices_free_context(context_t *ctx)
Deletes a context.
This function should be called when ctx is no longer used to free the memory allocated to this context.
Note
If this function is not called, Yices will automatically free the context on a call to
yices_exit
oryices_reset
.
Preprocessing Options
Several options determine the simplifications performed when formulas are asserted. It is best to leave these unchanged, but in case you need fine control, the following functions selectively enable or disable a preprocessing option.
The current options include:
Option
Meaning
varelim
Eliminate variables by substitution
arithelim
Gaussian elimination
bvarithelim
Variable elimination for bitvector arithmetic
eagerarithlemmas
Eager lemma generation for the Simplex solver
flatten
Flattening of nested (or …)
learneq
Heuristic to learn equalities in QF_UF problems
keepite
Keep ifthenelse terms in the egraph
breaksymmetries
Heuristic to detect and break symmetries in QF_UF problems
assertitebounds
Attempt to learn and assert upper/lower bounds on ifthenelse terms
If eagerarithlemmas is enabled, the Simplex solver will eagerly generate lemmas such as (x ≥ 1) ⟹ (x ≥ 0), that is, lemmas that involve two atoms that contain the same variable. See [DdM2006] for more details.
The flatten option converts a term such as (or (or a b) (or b c d)) to (or a b c d).
The breaksymmetries option enables symmetry breaking as described in [DFMW2011].
If assertitebounds is enabled, Yices tries to compute upper and lower bounds on arithmetic ifthenelse terms, and asserts these bounds. For example, if t is defined as (ite c 10 (ite d 3 20)) then the context will include the bounds: 3 ≤ t ≤ 20.

int32_t yices_context_enable_option(context_t *ctx, const char *option)
Enables a preprocessing option.
Parameters
ctx context
option: option name
The option name must be given as a string, as listed in the previous table.
For example to enable symmetry breaking:
yices_context_enable_option(ctx, "breaksymmetries");
This function returns 1 if the option is not recognized, or 0 otherwise.
Error report
if the option is not recognized:
– error code:
CTX_UNKNOWN_PARAMETER

int32_t yices_context_disable_option(context_t *ctx, const char *option)
Disables a preprocessing option.
The parameters and error conditions are the same as for
yices_context_enable_option
.
Assertions and Satisfiability Checks
Once a context is initialized, the following functions can be used to assert formulas, check satisfiability, and query the context’s status.

smt_status_t yices_context_status(context_t *ctx)
Returns a context’s status.
An internal flag stores the context’s current state. This function reads this flag and returns it.
The returned value is one of the following codes:
STATUS_IDLE
. This is the initial state.In this state, it is possible to assert formulas. The state may then change to
STATUS_UNSAT
if the assertions are trivially unsatisfiable Otherwise, the state remainsSTATUS_IDLE
.STATUS_SEARCHING
. This is the context state during search.The context enters this state on a call to
yices_check_context
and remains in this state until the solver completes or the search is interrupted.STATUS_SAT
,STATUS_UNSAT
,STATUS_UNKNOWN
.These are the states after a search completes.
STATUS_UNKNOWN
means that the search was inconclusive, which may happen if the solver is not complete.STATUS_INTERRUPTED
.This state is entered if a search is interrupted.
These codes are defined in
yices_types.h
(seesmt_status_t
).

int32_t yices_assert_formula(context_t *ctx, term_t t)
Asserts a formula.
This function asserts formula t in context ctx.
The term t must be Boolean.
The context ctx must be in one of the following states:
STATUS_IDLE
,STATUS_UNSAT
,STATUS_SAT
, orSTATUS_UNKNOWN
.if the current state is
STATUS_UNSAT
, this function does nothing.otherwise, the formula t is simplified and asserted in the context. The context’s state is then changed to
STATUS_UNSAT
if the assertion simplifies to false, or toSTATUS_IDLE
otherwise.
If the context is in mode oneshot, this function fails if the state is either
STATUS_SAT
orSTATUS_UNKNOWN
.The function returns 0 if there’s no error, or 1 otherwise.
Error report
if t is invalid
– error code:
INVALID_TERM
– term1 := t
if t is not Boolean
– error code:
TYPE_MISMATCH
– term1 := t
– type1 := bool
if ctx’s state is
STATUS_INTERRUPTED
– error code:
CTX_INVALID_OPERATION
if ctx’s mode is oneshot and ctx’s state is neither
STATUS_IDLE
norSTATUS_UNSAT
– error code:
CTX_OPERATION_NOT_SUPPORTED
Other error codes are possible if t is outside the logic supported by the context. See Error Reports.

int32_t yices_assert_formulas(context_t *ctx, uint32_t n, const term_t t[])
Asserts an array of formula.
This function adds assertions t[0] … t[n1] to ctx.
Parameters
n is the number of formulas to assert
t must be an array of n Boolean terms.
The context must be in state
STATUS_IDLE
,STATUS_UNSAT
,STATUS_SAT
, orSTATUS_UNKNOWN
.This function is equivalent to calling
yices_assert_formula
with input (and t[0] … t[n1]). In particular, if n is 0, this function is equivalent to asserting true in ctx.The returned value and error conditions are as in
yices_assert_formulas
.

smt_status_t yices_check_context(context_t *ctx, const param_t *params)
Checks whether a context is satisfiable.
Parameters
ctx is a context
params is an optional pointer to a searchparameter structure
The params data structure can be used to control the heuristics used by the solvers. See Search Parameters. If params is
NULL
, default settings are used.This function’s behavior and returned value depend on ctx’s current state.
If the state is
STATUS_SAT
,STATUS_UNSAT
, orSTATUS_UNKNOWN
, the function just returns this status.If the state is
STATUS_IDLE
, then the context’s solver (as defined by the context’s configuration) searches for a satisfying assignment to all the assertions stored in ctx. If params is notNULL
, the solver uses the heuristic parameters specified by params.Then the function returns one of the following codes:
STATUS_UNSAT
: the context is not satisfiable.STATUS_SAT
: the context is satisfiable.STATUS_UNKNOWN
: the solver can’t prove whether the context is satisfiable or not.STATUS_INTERRUPTED
: the search was interrupted by a call toyices_stop_search
.
This returned value is also stored as the context’s status flag, with the following exception:
If the context is configured for mode interactive and the search is interrupted, then the function returns
STATUS_INTERRUPTED
but the context’s state is restored to what it was before the call toyices_check_context
, and the internal status flag is reset toSTATUS_IDLE
.
If ctx is in another state, the function returns
STATUS_ERROR
.
Error report
if ctx’s states is wrong:
– error code:
CTX_INVALID_OPERATION

void yices_stop_search(context_t *ctx)
Interrupts the search.
This function can be called from a signal handler to stop the search after at call to
yices_check_context
. If the context’s state isSTATUS_SEARCHING
then the search is interrupted, otherwise the function does nothing.Note
If the search is interrupted and the context’s mode is not interactive then the context’s enters state
STATUS_INTERRUPTED
. The only way to recover is then to callyices_reset_context
oryices_pop
(assuming the context supports push and pop).

void yices_reset_context(context_t *ctx)
Resets a context.
This function removes all the assertions stored in ctx and resets the context’s state to
STATUS_IDLE
.

int32_t yices_assert_blocking_clause(context_t *ctx)
Adds a blocking clause.
This function is intended to enumerate different models for a set of assertions.
If ctx’s status is either
STATUS_SAT
orSTATUS_UNKNOWN
, then a new clause is asserted in ctx to remove the current truth assignment. After this clause is added, the next call toyices_check_context
will either produce a different truth assignment (hence a different model) or returnSTATUS_UNSAT
.After adding the clause, the context’s state is updated to either
STATUS_IDLE
(if the clause is not empty) or toSTATUS_UNSAT
if the blocking clause is empty.If ctx’s status is not
STATUS_SAT
orSTATUS_UNKNOWN
, the function reports an error.
This function is not supported if the context’s mode is oneshot.
The returned value is 0 if the operation succeeds or 1 otherwise.
Error report
if ctx’s status is different from
STATUS_SAT
andSTATUS_UNKNOWN
– error code:
CTX_INVALID_OPERATION
if ctx’s mode is oneshot
– error code:
CTX_OPERATION_NOT_SUPPORTED
Push and Pop
If a context is configured to support push and pop (i.e., if the mode is either pushpop or interactive) then the context maintains a stack of assertions organized in levels.The push operation starts a new level and the pop operation removes all assertions added at the current level. Push can be thought of as setting a backtracking point and pop restores the context’s state to a previous backtracking point.
Initially, the assertion level is zero. Assertions at level zero
cannot be retracted. For example, any formula asserted before the
first call to yices_push
is part of the context and cannot
be removed by yices_pop
.

int32_t yices_push(context_t *ctx)
Marks a backtracking point.
This function starts a new assertion level. The ctx must be configured to support push and pop, and its state must be either
STATUS_IDLE
, orSTATUS_SAT
, orSTATUS_UNKNOWN
.The function returns 0 if the operation succeeds or 1 otherwise.
Error report
if ctx is not configured for push and pop:
– error code:
CTX_OPERATION_NOT_SUPPORTED
if ctx supports push and pop but its status is
STATUS_UNSAT
,STATUS_SEARCHING
, orSTATUS_INTERRUPTED
:– error code:
CTX_INVALID_OPERATION

int32_t yices_pop(context_t *ctx)
Backtracks.
This function removes all assertions at the current level (i.e., restores the context’s state to what it was at the matching call to
yices_push
), then decrements the assertion level. It fails if the current assertion level is zero.The function returns 0 if the operation succeeds or 1 otherwise.
Error report
if ctx is not configured for push and pop:
– error code:
CTX_OPERATION_NOT_SUPPORTED
if ctx’s status is
STATUS_SEARCHING
or if the assertion level is zero:– error code:
CTX_INVALID_OPERATION
Check with Assumptions and Unsat Cores
When checking satisfiability, it is possible to treat certain formulas as assumptions. Assumptions are similar to asserted formulas but they are local to a single call to check. Here is an example:
context_t *ctx = yices_new_context(NULL);
yices_assert_formula(ctx, f);
status = yices_check_context_with_assumptions(ctx, NULL, 5, a);
In this fragment, we first create a context ctx
then we assert a
formula f
. In the call to check, we give an array of five
assumptions a[0]
, …, a[4]
. This amounts to checking the
conjunction of f
and the five assumptions, but the assumptions are
local to the call to yices_check_context_with_assumptions
and are not added to the context. We could achieve the same effect by
using incremental solving:
context_t *ctx = yices_new_context(NULL);
yices_assert_formula(ctx, f);
yices_push(ctx);
yices_assert_formulas(ctx, 5, a);
status = yices_check_context(ctx, NULL);
yices_pop(ctx);
However, check with assumptions provides an additional functionality,
namely, the construction of an unsatisfiable core, that is, a subset
of the five assumptions that’s inconsistent. The unsatisfiable core is
constructed by calling function yices_get_unsat_core
, which
returns the core in a term vector. A full example is in file
examples/example_unsat_core.c
included in the Yices
distribution.

smt_status_t yices_check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t t[])
Checks whether n assumptions are satisfiable in a context ctx.
Parameters
ctx is a context
params is an optional structure to a searchparameter structure.
n is the number of assumptions
t is an array of n Boolean terms
The params structure controls search heuristics. If params is NULL, default settings are used. See Search Parameters and
yices_check_context
.The function checks whether all assertions currently asserted in ctx together with the n assumptions t[0] … t[n1] are satisfiable, and returns the result as a status code. If the function returns
STATUS_UNSAT
then one can compute an unsat core (i.e., a subset of the assumptions that is unsatisfiable) by callingyices_get_unsat_core
.More precisely:
If ctx’s current status is
STATUS_UNSAT
then the function does nothing and returnsSTATUS_UNSAT
.If ctx’s status is
STATUS_IDLE
,STATUS_SAT
, orSTATUS_UNKNOWN
then the function checks whether ctx conjoined with the n assumptions is satisfiable. This is done even if n is zero. The function will then return a code as inyices_check_context
.If ctx’status is anything else, the function returns
STATUS_ERROR
.
This operation fails and returns
STATUS_ERROR
if ctx is configured for oneshot solving and ctx’s status is anything other thanSTATUS_IDLE
.Error report
If ctx’s status is wrong:
– error code:
CTX_INVALID_OPERATION
If the operation is not supported by this context:
– error code:
CTX_OPERATION_NOT_SUPPORTED

int32_t yices_get_unsat_core(context_t *ctx, term_vector_t *v)
Construct an unsat core (after a call to
yices_check_context_with_assumptions
) and store it in vector v.Parameters
ctx is a context
v must be an initialized term vector (see
yices_init_term_vector
).
The function checks whether ctx’s status is
STATUS_UNSAT
. If so, it computes and unsat core and store it in vector v. The unsat core is an subset of the assumptions passed to the most recent call toyices_check_context_with_assumptions
.It is also possible to use this function after a call to
yices_check_context
. In this case, the function returns an empty core.The unsat core is returned as follows:
v>size contains the number of elements in the core
v>data[0 … v>size  1] contains the elements. Each term in v>data[i] is a Boolean term, equal to one of the assumption that is part of the core.
There are no duplicates in the v>data array.
If ctx’s status is anything other than
STATUS_UNSAT
, the function leaves v unchanged and returns 1.Error report
If ctx’s status is not
STATUS_UNSAT
– error code:
CTX_INVALID_OPERATION
Search Parameters
A parameter record stores search parameters and options that control
the heuristics used by a solver. It is created by calling
yices_new_param_record
. Individual parameters can be set
using function yices_set_param
. The record can then be
passed as argument to function yices_check_context
. When the
record is no longer needed, it can be deleted by
yices_free_param_record
.

param_t *yices_new_param_record(void)
Allocates a parameter record.
This returns a (pointer to) a record initialized with default settings.
The record is allocated internally by Yices. It must be freed when nolonger used by calling
yices_free_param_record
.

int32_t yices_set_param(param_t *p, const char *name, const char *value)
Sets a search parameter.
Parameters
p must be a record returned by
yices_new_param_record
.name is a parameter name
value is the value for this parameter
Both name and value must be given as
'\0'
terminated strings. Here are a few examples:yices_set_param(p, "branching", "negative"); // branching heuristic yices_set_param(p, "randomness", "0.02"); // 2% of random decisions yices_set_param(p, "maxinterfaceeqs", "20");
The full list of search parameters and possible values for each is given in Section Heuristic Parameters.
This function returns 1 if there’s an error, or 0 otherwise.
Error report
if name is not a known parameter
– error code:
CTX_UNKNOWN_PARAMETER
if value is not valid for the parameter name
– error code:
CTX_INVALID_PARAMETER_VALUE

void yices_default_params_for_context(const context_t *ctx, param_t *p)
Set all the parameters in record p to values appropriate for context ctx. The parameter settings depend on the logic supported by ctx and are based on empirical evaluation on benchmarks in the same logic.

void yices_free_param_record(param_t *param)
Deletes a parameter record.
param must be a record returned by
yices_new_param_record
.This function frees the memory allocated to this record.