Home Docs Download Mail Status FM Tools
Yices

C API

The current C API provides access to the basic Yices functionalities.

Typedefs

typedef void * yices_context
 Yices context.
typedef void * yices_type
 Yices types (abstract syntax tree).
typedef void * yices_expr
 Yices expressions (abstract syntax tree).
typedef void * yices_var_decl
 Variable declaration.
typedef int assertion_id
 Assertion index, to identify weighted and retractable assertions.
typedef void * yices_model
 Model.
typedef void * yices_var_decl_iterator
 Iterator for scanning the boolean variables.

Enumerations

enum  lbool { l_false = -1, l_undef, l_true }
 Extended booleans: to represent the value of literals in the context. More...

Structures

struct srec_s
 String allocation structure used by yices_get_arith_value_as_string and yices_free_string. More...

Functions

const  char * yices_version ()
 Return the yices version number.
void yices_set_verbosity (int l)
 Set the verbosity level.
void yices_enable_type_checker (int flag)
 Force Yices to type check expressions when they are asserted (default = false).
int yices_enable_log_file (const char *file_name)
 Enable a log file that will store the assertions, checks, declartationss, etc.
void yices_set_arith_only (int flag)
 Inform Yices that only the arithmetic theory is going to be used.
void yices_set_max_num_conflicts_in_maxsat_iteration (unsigned n)
 Set the maximum number of conflicts that are allowed in a maxsat iteration.
void yices_set_max_num_iterations_in_maxsat (unsigned n)
 Set the maximum number of iterations in the MaxSAT algorithm.
void yices_set_maxsat_initial_cost (long long c)
 Set the initial cost for a maxsat problem.
yices_context yices_mk_context ()
 Create the logical context.
void yices_del_context (yices_context ctx)
 Delete the logical context.
void yices_reset (yices_context ctx)
 Reset the logical context.
void yices_dump_context (yices_context ctx)
 Display the internal representation of the logical context on stderr.
void yices_push (yices_context ctx)
 Create a backtracking point.
void yices_pop (yices_context ctx)
 Backtrack.
void yices_assert (yices_context ctx, yices_expr expr)
 Assert a constraint in the logical context.
assertion_id yices_assert_weighted (yices_context ctx, yices_expr expr, long long w)
 Assert a constraint in the logical context with weight w.
assertion_id yices_assert_retractable (yices_context ctx, yices_expr expr)
 Assert a constraint that can be later retracted.
void yices_retract (yices_context ctx, assertion_id id)
 Retract a retractable or weighted constraint.
int yices_inconsistent (yices_context ctx)
 Check whether the logical context is known to be inconsistent.
lbool yices_check (yices_context ctx)
 Check if the logical context is satisfiable.
lbool yices_max_sat (yices_context ctx)
 Compute the maximal satisfying assignment for the asserted weighted constraints.
lbool yices_max_sat_cost_leq (yices_context c, long long max_cost)
 Similar to yices_max_sat, but start looking for models with cost less than of equal to max_cost.
lbool yices_find_weighted_model (yices_context ctx, int random)
 Search for a model of the constraints asserted in ctx and compute its cost.
unsigned yices_get_unsat_core_size (yices_context  ctx)
 Return the size of the unsatisfiable core.
unsigned yices_get_unsat_core (yices_context  ctx, assertion_id  a[])
 Return the unsatisfiable core.
yices_model yices_get_model (yices_context ctx)
 Return a model for a satisfiable context.
lbool yices_get_value (yices_model m, yices_var_decl v)
 Return the value of variable v in model m.
int yices_get_int_value (yices_model m, yices_var_decl d, long *value)
 Get the integer value assigned to variable v in model m.
int yices_get_arith_value (yices_model m, yices_var_decl d, long *num, long *den)
 Get the rational value assigned to variable v in model m.
int yices_get_double_value (yices_model m, yices_var_decl d, double *value)
 Convert the value assigned to variable v in model m to a floating poin number.
int yices_get_mpq_value (yices_model m, yices_var_decl d, mpq_t value)
 Convert the value assigned to variable v in model m to a GMP rational (mpq_t).
int yices_get_mpz_value (yices_model m, yices_var_decl d, mpz_t value)
 Convert the value assigned to variable v in model m to a GMP integer (mpz_t).
int  yices_get_arith_value_as_string (yices_model m, yices_var_decl d, srec_t *r)
 Get the value assigned to variable v in model m as a string.
int  yices_free_string (srec_t *r)
 Free a string allocated by Yices
int yices_get_bitvector_value (yices_model m, yices_var_decl d, unsigned n, int bv[])
 Get the bitvector constant assigned to a variable v in model m.
int yices_get_scalar_value (yices_model m, yices_var_decl d)
 Get the value assigned to a scalar variable v in model m.
const char *  yices_get_scalar_value_name (yices_model m, yices_var_decl d)
 Get the value assigned to a scalar variable v in model m.
int yices_get_assertion_value (yices_model m, assertion_id id)
 Return 1 (0) if the assertion of the given id is satisfied (not satisfied) in the model m.
lbool yices_evaluate_in_model (yices_model m, yices_expr e)
 Evaluate a formula in a model.
void yices_display_model (yices_model m)
 Display the given model in the standard output.
long long yices_get_cost (yices_model m)
 Return the cost of model m.
double yices_get_cost_as_double (yices_model m)
 Return the cost of the model m, converted to a double-precision floating point number.
yices_var_decl_iterator yices_create_var_decl_iterator (yices_context c)
 Create an iterator that can be used to traverse the boolean variables (var_decl objects) in the logical context.
int yices_iterator_has_next (yices_var_decl_iterator it)
 Return 1 if the iterator it still has elements to be iterated. Return 0 otherwise.
yices_var_decl yices_iterator_next (yices_var_decl_iterator it)
 Return the next variable, and move the iterator.
void yices_iterator_reset (yices_var_decl_iterator it)
 Reset the given iterator, that is, move it back to the first element.
void yices_del_iterator (yices_var_decl_iterator it)
 Delete an iterator created with yices_create_var_decl_iterator.
yices_expr yices_parse_expression (yices_context ctx, const char* s)
 Parse string s as an expression in the Yices syntax.
yices_type yices_parse_type (yices_context ctx, const char* s)
 Parse string s as a type in the Yices syntax.
int yices_parse_command (yices_context ctx, const char* s)
 Parse string s as a command in the Yices syntax and execute the command.
const char * yices_get_last_error_message (void)
 Return the last error message.
yices_type yices_mk_type (yices_context ctx, const char *name)
 Return the type associated with the given name. If the type does not exist, a new uninterpreted type is created.
yices_type yices_mk_bitvector_type (yices_context ctx, unsigned size)
 Returns the bitvector type (bv[size]).
yices_type yices_mk_function_type (yices_context ctx, yices_type domain[], unsigned domain_size, yices_type range)
 Return a function type (-> d1 ... dn r).
yices_type yices_mk_tuple_type (yices_context ctx, yices_type args[], unsigned size)
 Constructs the tuple type (arg[0], ..., arg[size-1]).
yices_var_decl yices_mk_bool_var_decl (yices_context ctx, const char *name)
 Return a new boolean variable declaration.
yices_var_decl yices_mk_var_decl (yices_context ctx, const char *name, yices_type ty)
 Return a new (global) variable declaration. It is an error to create two variables with the same name.
yices_var_decl yices_get_var_decl_from_name (yices_context ctx, const char *name)
 Return a variable declaration associated with the given name.
yices_var_decl yices_get_var_decl (yices_expr e)
 Return the variable declaration object associated with the given name expression.
const  char * yices_get_var_decl_name (yices_var_decl d)
 Return the name of a variable declaration.
yices_expr yices_mk_var_from_decl (yices_context ctx, yices_var_decl d)
 Return a name expression (instance) using the given variable declaration.
yices_expr yices_mk_bool_var_from_decl (yices_context ctx, yices_var_decl d)
 Return a name expression (instance) using the given variable declaration.
yices_expr yices_mk_bool_var (yices_context ctx, const char *name)
 Return a name expression for the given variable name.
yices_expr yices_mk_fresh_bool_var (yices_context ctx)
 Return a fresh boolean variable.
yices_expr yices_mk_true (yices_context ctx)
 Return an expression representing true.
yices_expr yices_mk_false (yices_context ctx)
 Return an expression representing false.
yices_expr yices_mk_or (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing the or of the given arguments.
yices_expr yices_mk_and (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing the and of the given arguments.
yices_expr yices_mk_not (yices_context ctx, yices_expr a)
 Return an expression representing (not a).
yices_expr yices_mk_eq (yices_context ctx, yices_expr a1, yices_expr a2)
 Return an expression representing a1 = a2.
yices_expr yices_mk_diseq (yices_context ctx, yices_expr a1, yices_expr a2)
 Return an expression representing a1 /= a2.
yices_expr yices_mk_ite (yices_context ctx, yices_expr c, yices_expr t, yices_expr e)
 Return an expression representing (if c t e).
yices_expr yices_mk_app (yices_context ctx, yices_expr f, yices_expr args[], unsigned n)
 Return a function application term (f t1 ... tn).
yices_expr yices_mk_function_update (yices_context ctx, yices_expr f, yices_expr args[], unsigned n, yices_expr v)
 Build a function update term (update f (t1 ... tn) v).
yices_expr yices_mk_tuple_literal (yices_context ctx, yices_expr args[], unsigned n)
 Build a tuple term (tuple t1 ... tn).
yices_expr yices_mk_num (yices_context ctx, int n)
 Return an expression representing the given integer.
yices_expr yices_mk_num_from_string (yices_context ctx, const char *n)
 Return an expression representing the number provided in ASCII format.
yices_expr yices_mk_num_from_mpz (yices_context ctx, const mpz_t z)
 Construct a numerical expression form a GMP integer.
yices_expr yices_mk_num_from_mpq (yices_context ctx, const mpq_t q)
 Construct a numerical expression form a GMP rational.
yices_expr yices_mk_sum (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing args[0] + ... + args[n-1].
yices_expr yices_mk_sub (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing args[0] - ... - args[n-1].
yices_expr yices_mk_mul (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing args[0] * ... * args[n-1].
yices_expr yices_mk_lt (yices_context ctx, yices_expr a1, yices_expr a2)
 Return an expression representing a1 < a2.
yices_expr yices_mk_le (yices_context ctx, yices_expr a1, yices_expr a2)
 Return an expression representing a1 <= a2.
yices_expr yices_mk_gt (yices_context ctx, yices_expr a1, yices_expr a2)
 Return an expression representing a1 > a2.
yices_expr yices_mk_ge (yices_context ctx, yices_expr a1, yices_expr a2)
 Return an expression representing a1 >= a2.
yices_expr yices_mk_bv_constant (yices_context ctx, unsigned size, unsigned long value)
 Create a bit vector constant of size bits and of the given value.
yices_expr yices_mk_bv_constant_from_array (yices_context ctx, unsigned size, int bv[])
 Create a bit vector constant from an array.
yices_expr yices_mk_bv_add (yices_context ctx, yices_expr a1, yices_expr a2)
 Bitvector addition.
yices_expr yices_mk_bv_sub (yices_context ctx, yices_expr a1, yices_expr a2)
 Bitvector subtraction.
yices_expr yices_mk_bv_mul (yices_context ctx, yices_expr a1, yices_expr a2)
 Bitvector multiplication.
yices_expr yices_mk_bv_minus (yices_context ctx, yices_expr a1)
 Bitvector opposite.
yices_expr yices_mk_bv_and (yices_context ctx, yices_expr a1, yices_expr a2)
 Bitwise and.
yices_expr yices_mk_bv_or (yices_context ctx, yices_expr a1, yices_expr a2)
 Bitwise or.
yices_expr yices_mk_bv_xor (yices_context ctx, yices_expr a1, yices_expr a2)
 Bitwise exclusive or.
yices_expr yices_mk_bv_not (yices_context ctx, yices_expr a1)
 Bitwise negation.
yices_expr yices_mk_bv_concat (yices_context ctx, yices_expr a1, yices_expr a2)
 Bitvector concatenation.
yices_expr yices_mk_bv_extract (yices_context ctx, unsigned end, unsigned begin, yices_expr a)
 Bitvector extraction.
yices_expr yices_mk_bv_sign_extend (yices_context ctx, yices_expr a, unsigned n)
 Sign extension.
yices_expr yices_mk_bv_shift_left0 (yices_context ctx, yices_expr a, unsigned n)
 Left shift by n bits, padding with zeros.
yices_expr yices_mk_bv_shift_left1 (yices_context ctx, yices_expr a, unsigned n)
 Left shift by n bits, padding with ones.
yices_expr yices_mk_bv_shift_right0 (yices_context ctx, yices_expr a, unsigned n)
 Right shift by n bits, padding with zeros.
yices_expr yices_mk_bv_shift_right1 (yices_context ctx, yices_expr a, unsigned n)
 Right shift by n bits, padding with ones.
yices_expr yices_mk_bv_lt (yices_context ctx, yices_expr a1, yices_expr a2)
 Unsigned comparison: (a1 < a2).
yices_expr yices_mk_bv_le (yices_context ctx, yices_expr a1, yices_expr a2)
 Unsigned comparison: (a1 <= a2).
yices_expr yices_mk_bv_gt (yices_context ctx, yices_expr a1, yices_expr a2)
 Unsigned comparison: (a1 > a2).
yices_expr yices_mk_bv_ge (yices_context ctx, yices_expr a1, yices_expr a2)
 Unsigned comparison: (a1 >= a2).
yices_expr yices_mk_bv_slt (yices_context ctx, yices_expr a1, yices_expr a2)
 Signed comparison: (a1 < a2).
yices_expr yices_mk_bv_sle (yices_context ctx, yices_expr a1, yices_expr a2)
 Signed comparison: (a1 <= a2).
yices_expr yices_mk_bv_sgt (yices_context ctx, yices_expr a1, yices_expr a2)
 Signed comparison: (a1 > a2).
yices_expr yices_mk_bv_sge (yices_context ctx, yices_expr a1, yices_expr a2)
 Signed comparison: (a1 >= a2).
void yices_pp_expr (yices_expr e)
 Pretty print the given expression in the standard output.

Typedef Documentation

typedef int assertion_id
 

Assertion index, to identify retractable assertions.

typedef void* yices_context
 

Yices context.

A context stores a collection of declarations and assertions.

typedef void* yices_expr
 

Yices expressions (abstract syntax tree).

typedef void* yices_model
 

Model.

A model assigns constant values to variables defined in a context. The context must be known to be consistent for a model to be available. The model is constructed by calling yices_check (or its relatives) then yices_get_model.

typedef void* yices_type
 

Yices types (abstract syntax tree).

typedef void* yices_var_decl
 

Variable declaration.

A declaration consists of a name and a type (such as x::bool). An instance of the declaration represents the term x.

Instances are also called name expressions. Instances can be created using yices_mk_bool_var_from_decl or yices_mk_var_from_decl.

typedef void* yices_var_decl_iterator
 

Iterator for scanning the boolean variables.


Enumeration Type Documentation

enum lbool
 

Extended booleans to represent the value of literals in the context.

Enumerator:
l_false 
l_undef 
l_true 

Structure Documentation

typedef struct srec_s {
     int flag;
     char * str;
} srec_t;
 

This structure consists of an integer flag and a pointer str.

If the flag is 0 then the pointer is NULL

If the flag is 1 then the pointer is a valid '\0'-terminated C string.

See also:
yices_get_arith_value_as_string
yices_free_string


Function Documentation

const char* yices_version  ) 
 

Return the yices version number.

void yices_set_verbosity int  l  ) 
 

Set the verbosity level.

void yices_enable_type_checker int  flag  ) 
 

Force Yices to type check expressions when they are asserted (default = false).

int yices_enable_log_file const char *  file_name  ) 
 

Enable a log file that will store the assertions, checks, decls, etc.

If the log file is already open, then nothing happens.

Return code:

  • 1 if the operation succeeds
  • 0 if there's already a log file
  • -1 if there's an error when trying to open the file

void yices_set_arith_only int  flag  ) 
 

Inform yices that only the arithmetic theory is going to be used.

This flag usually improves performance (default = false).

void yices_set_max_num_conflicts_in_maxsat_iteration unsigned  n  ) 
 

Set the maximum number of conflicts that are allowed in a maxsat iteration.

If the maximum is reached, then "unknown" (i.e., l_undef) is returned by maxsat.

void yices_set_max_num_iterations_in_maxsat unsigned  n  ) 
 

Set the maximum number of iterations in the MaxSAT algorithm.

If the maximum is reached, then "unknown" (i.e., l_undef) is returned by maxsat.

void yices_set_maxsat_initial_cost long long  c  ) 
 

Set the initial cost for a maxsat problem.

yices_context yices_mk_context  ) 
 

Create the logical context.

void yices_del_context yices_context  ctx  ) 
 

Delete the logical context.

See also:
yices_mk_context

void yices_reset yices_context  ctx  ) 
 

Reset the logical context.

void yices_dump_context yices_context  ctx  ) 
 

Display the internal representation of the logical context on stderr.

This function is mostly for debugging.

void yices_push yices_context  ctx  ) 
 

Create a backtracking point.

The logical context can be viewed as a stack of contexts. The scope level is the number of elements on this stack. The stack of contexts is simulated using trail (undo) stacks.

void yices_pop yices_context  ctx  ) 
 

Backtrack.

Restores the context from the top of the stack, and pops it off the stack. Any changes to the logical context (by yices_assert or other functions) between the matching yices_push and yices_pop operators are flushed, and the context is completely restored to what it was right before the yices_push.

See also:
yices_push

void yices_assert yices_context  ctx,
yices_expr  expr
 

Assert a constraint in the logical context.

After one assertion, the logical context may become inconsistent. Function yices_inconsistent may be used to check that.

assertion_id yices_assert_weighted yices_context  ctx,
yices_expr  expr,
long long  w
 

Assert a constraint in the logical context with weight w.

Returns:
An integer id that can be used to retract the constraint.
See also:
yices_retract

assertion_id yices_assert_retractable yices_context  ctx,
yices_expr  expr
 

Assert a constraint that can be retracted later.

Returns:
An id that can be used to retract the constraint.
This is similar to yices_assert_weighted, but the weight is considered to be infinite.

See also:
yices_retract

void yices_retract yices_context  ctx,
assertion_id  id
 

Retract a retractable or weighted constraint.

See also:
yices_assert_weighted

yices_assert_retractable

int yices_inconsistent yices_context  ctx  ) 
 

Check whether the logical context is known to be inconsistent.

If the function returns true (i.e., a non-zero value) then the context is inconsistent.

If the function returns false (i.e., zero) then the context's status is not known. To determine the status, function yices_check must be used.

lbool yices_check yices_context  ctx  ) 
 

Check if the logical context is satisfiable.

  • l_true means the context is satisfiable
  • l_false means it is unsatisfiable
  • l_undef means it was not possible to decide due to an incompleteness.

If the context is satisfiable, then yices_get_model can be used to obtain a model.

Warning:
This method ignore the weights associated with the constraints.

lbool yices_max_sat yices_context  ctx  ) 
 

Compute the maximal satisfying assignment for the asserted weighted constraints.

  • l_true means the maximal satisfying assignment was found
  • l_false means that the context is unsatisfiable (this may happen if the context has unweighted constraints)
  • l_undef means that it was not possible to decide because of an incompleteness.

If the result is l_true, then yices_get_model can be used to obtain a model.

See also:
yices_assert_weighted

lbool yices_max_sat_cost_leq yices_context  c,
long long  max_cost
 

Similar to yices_max_sat, but start looking for models with cost less than or equal to max_cost.

Returns:
l_false if such a model doesn't exist.

lbool yices_find_weighted_model yices_context  ctx,
int  random
 

Search for a model of the constraints asserted in ctx and compute its cost.

If random is non-zero, then random search is used, otherwise, the default decision heuristic is used.

If there are no weighted constaints in ctx, then this function is the same as yices_check.

Otherwise, it searches for a model that satisfies all the non-weighted constraints but not necessarily the weighted constraints. The function returns l_true if such a model is found, and the model can be obtained using yices_get_model. The cost of this model is the sum of the weights of the unsatisfied weighted constraints.

The function returns l_false if it cannot find such a model.

The function may also return l_undef if the context contains formulas for which yices is incomplete (e.g., quantifiers). Do not use the model in this case.

unsigned  yices_get_unsat_core_size yices_context  ctx  ) 
 

Return the size of the unsat core or 0 it there's no unsat core.

See also

unsigned  yices_get_unsat_core yices_context  ctx,
assertion_id  a[]
 

Copy the unsatisfiable core into array a. Each assertion in the core is identified by an assertion_id as returned by yices_assert_retractable.

The unsatisfiable core is a (small) subset of the retractable assertions that is inconsistent by itself.

The returned value is the size of the unsat core, that is, the number of assertion ids copied into array a. The function returns 0 if there's no unsat core.

Warning:
  • a must be large enough to store the unsat core.
  • If you don't want to keep track of the number of retractable assertions, you can use yices_get_unsat_core_size to determine the size of the unsat core.

yices_model yices_get_model yices_context  ctx  ) 
 

Return a model for a satisfiable logical context.

Warning:
This should be only called if yices_check or yices_max_sat returned l_true or l_undef.

Return 0 if a model is not available. Calls to functions that modify the context invalidate the model.

lbool yices_get_value yices_model  m,
yices_var_decl  v
 

Return the value of variable v in model m

The result is l_undef if the value of v is a "don't care".

Warning:
v must be the declaration of a boolean variable

See also:
yices_get_int_value

yices_get_arith_value

yices_get_double_value

int yices_get_int_value yices_model  m,
yices_var_decl  d,
long *  value
 

Get the integer value assigned to variable v in model m.

The value is stored in * value. Returns 1 on success.

A return code of 0 indicates one of the following errors:

  • v is not a proper declaration or not the declaration of a numerical variable
  • v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)
  • v has a value that cannot be converted to long, because it is rational or too big

See also:
yices_get_value

yices_get_arith_value

yices_get_double_value

int yices_get_arith_value yices_model  m,
yices_var_decl  d,
long *  num,
long *  den
 

Get the rational value assigned to variable v in model m.

The numerator is stored in * num and the denominator in * den. Returns 1 on success.

A return code of 0 indicates one of the following errors:

  • v is not a proper declaration or not the declaration of a numerical variable
  • v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)
  • v has a value that cannot be converted to long/long because the numerator or the denominator is too big

See also:
yices_get_value

yices_get_int_value

yices_get_double_value

int yices_get_double_value yices_model  m,
yices_var_decl  d,
double *  value
 

Convert the value assigned to variable v in model m to a floating point number.

The value is stored in * value. Returns 1 on success.

A return code of 0 indicates one of the following errors:

  • v is not a proper declaration or not the declaration of a numerical variable
  • v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)

See also:
yices_get_value

yices_get_int_value

yices_get_arith_value

int yices_get_mpq_value yices_model  m,
yices_var_decl  d,
mpq_t  value
 

Convert the value assigned to variable v in model m to a GMP rational (mpq_t).

Return 1 on success.

A return code of 0 indicates one of the following errors:

  • v is not a proper declaration or not the declaration of a numerical variable
  • v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)

Warning:
  • For this function to be declared properly, put #include <gmp.h> before #include <yices_c.h> in your code.
    If you don't need GMP numbers, don't include <gmp.h>.
  • The mpq_t object value must be initialized first, by calling GMP's mpq_init function. (Check the GNU MP documentation).
See also:
yices_get_mpz_value.

int yices_get_mpz_value yices_model  m,
yices_var_decl  d,
mpz_t  value
 

Convert the value assigned to variable v in model m to a GMP integer (mpz_t).

Return 1 on success.

A return code of 0 indicates one of the following errors:

  • v is not a proper declaration or not the declaration of a numerical variable
  • v has no value assigned in model m (typically, this means that v does not occur in the asserted constraints)
  • the value assigned to v is not an integer.

Warning:
  • For this function to be declared properly, put #include <gmp.h> before #include <yices_c.h> in your code.
    If you don't need GMP numbers, don't include <gmp.h>.
  • The mpz_t object value must be initialized first, by calling GMP's mpz_init function or its variants. (Check the GNU MP documentation).
See also:
yices_get_mpq_value.

int yices_get_arith_value_as_string yices_model  m,
yices_var_decl  d,
srec_t r
 

Convert the value assigned to variable v in model m to a character string.

Yices internally allocates a string to store the value. The result is returned in record *r

If v's value is not known then

  • r->flag is set to 0
  • r->str is set to NULL

If v's value is found then

  • r->flag is set to 1
  • r->str contains v's value converted to a string (in decimal format)

The string r->str is allocated internally by Yices. It must be freed when it is no longer neededd by calling yices_free_string.

void yices_free_string srec_t r  ) 
 

Free the string returned in *r by a call to yices_get_arith_value_as_string

Also resets r->flag to 0 and r->str to NULL

int yices_get_bitvector_value yices_model  m,
yices_var_decl  d,
unsigned  n,
int  bv[]
 

Get the bitvector value assigned to a variable v in model m.

The value is stored in array bv: bv[0] is the low-order bit and bv[n - 1] is the high-order bit.

  • n should be the size of the bitvector variable v
  • if n is smaller than v's size, then the n lower-order bits of v are returned.
  • if n is larger than v's size, then the extra high-order bits are set to 0.

The return code is 0 if an error occurs, 1 otherwise.

Possible errors are:

  • d is not the declaration of a bitvector variable.
  • d is not assigned a value in model m

int yices_get_scalar_value yices_model  m,
yices_var_decl  d,
 

Get the value assigned to a scalar variable d in model m.

If d is a variable declaration of a scalar type tau, then the type must consists of n constants, for some positive integer n. For example, tau was defined via (define-type tau (scalar e_0 ... e_n-1)).

This function returns the value of variable d in m as an integer index between 0 and n-1.

The function returns -1 if an error occurs.

Possible errors are:

  • d is not the declaration of a scalar variable.
  • d is not assigned a value in model m

See also:
yices_get_scalar_value_name

const char* yices_get_scalar_value_name yices_model  m,
yices_var_decl  d,
 

Get the value assigned to a scalar variable d in model m as a string.

If d is a variable declaration of a scalar type tau, then the type must consists of n constants, for some positive integer n. For example, tau was defined via (define-type tau (scalar e_0 ... e_n-1)).

This function returns the value of variable d in m as one of the names e_0 to e_n-1.

The function returns NULL if an error occurs.

Possible errors are:

  • d is not the declaration of a scalar variable.
  • d is not assigned a value in model m

See also:
yices_get_scalar_value

int yices_get_assertion_value yices_model  m,
assertion_id  id
 

Return 1 (0) if the assertion of the given id is satisfied (not satisfied) in model m.

This function is only useful for assertion ids obtained using yices_assert_weighted, and if yices_max_sat was used to build the model.

This is the only scenario where an assertion may not be satisfied in a model produced by Yices.

lbool yices_evaluate_in_model yices_model  m,
yices_expr  e
 

Evaluate a formula in a model.

Model m can be obtained via yices_get_model, after a call to yices_check, yices_max_sat, or yices_find_weighted_model

  • l_true means the formula is true in the model
  • l_false means the formula is false in the model
  • l_undef means the model does not have enough information. Typically this is due to a function application, e.g., the model defines (f 1) and (f 2), but the formula e references (f 3)

void yices_display_model yices_model  m  ) 
 

Display the given model on standard output.

long long yices_get_cost yices_model  m  ) 
 

Return the cost of model m.

The cost is the sum of the weights of the unsatisfied constraints.

Warning:
The model cost is computed by yices_max_sat but not by yices_check.

double yices_get_cost_as_double yices_model  m  ) 
 

Return the cost of model m, converted to a double-precision floating point number.

yices_var_decl_iterator yices_create_var_decl_iterator yices_context  c  ) 
 

Create an iterator that can be used to traverse the boolean variables (var_decl objects) in the logical context.

An iterator is particulary useful when we want to extract the assignment (model) produced by the yices_check command.

Example:

	    yices_context ctx = yices_mk_context();
	    ...
	    if (yices_check(ctx) == l_true) {
 	       yices_var_decl_iterator it = yices_create_var_decl_iterator(ctx);
  	       yices_model m = yices_get_model(ctx);
	       while (yices_iterator_has_next(it)) {
                  yices_var_decl d = yices_iterator_next(it);
    	          char * val;
	          switch(yices_get_value(m, d)) {
	          case l_true: 
                     val = "true"; 
	             break;
	          case l_false: 
	             val = "false";
	             break;
	          case l_undef: 
	             val = "unknown"; 
	             break;
	          }
	          printf("%s = %s\n", yices_get_var_decl_name(d), val);
	       }
	     yices_del_iterator(it);
	    }
	  

See also:
yices_iterator_has_next

yices_iterator_next

yices_iterator_reset

int yices_iterator_has_next yices_var_decl_iterator  it  ) 
 

Return 1 if the iterator it still has elements to be iterated. Return 0 otherwise.

See also:
yices_iterator_next

yices_create_var_decl_iterator

yices_var_decl yices_iterator_next yices_var_decl_iterator  it  ) 
 

Return the next variable, and move the iterator.

See also:
yices_iterator_has_next

yices_create_var_decl_iterator

void yices_iterator_reset yices_var_decl_iterator  it  ) 
 

Reset the given iterator, that is, move it back to the first element.

void yices_del_iterator yices_var_decl_iterator  it  ) 
 

Delete an iterator created with yices_create_var_decl_iterator.

yices_expr yices_parse_expression yices_context  ctx,
const char *  s
 

Parse string s as a Yices expression and return the expression.

The string must be terminated by '\0' and use the Yices input syntax.

If there's an error during parsing, Yices will generate an error message that can be retrieved using function yices_get_last_error_message.

Returns:
NULL if parsing fails or the Yices expression otherwise

yices_type yices_parse_type yices_context  ctx,
const char *  s
 

Parse string s as a Yices type and return the type.

The string must be terminated by '\0' and use the Yices input syntax.

If there's an error during parsing, Yices will generate an error message that can be retrieved using function yices_get_last_error_message.

Returns:
NULL if parsing fails or the Yices type otherwise

int yices_parse_command yices_context  ctx,
const char *  s
 

Parse string s as a Yices command and execute the command.

The string must be terminated by '\0' and use the Yices input syntax.

If there's an error during parsing or if the command fails, Yices will generate an error message that can be retrieved using function yices_get_last_error_message.

Returns:
0 if there's a parsing error or if the command fails
1 if the command succeeds
const  char* yices_get_last_error_message  ) 
 

Return the last error message produced by the functions yices_parse_expression, yices_parse_type, or yices_parse_command.

yices_type yices_mk_type yices_context  ctx,
const char *  name
 

Return the type with the given name. If no type of this name does not exist, a new uninterpreted type is created.

Remark:
This function can be used to obtain one of the builtin types: number, real, int, nat, and bool.

yices_type yices_mk_bitvector_type yices_context  ctx,
unsigned  size
 

Return the type (bitvector size) (i.e., bitvector of size bits).

size must be positive.

yices_type yices_mk_function_type yices_context  ctx,
yices_type  domain[],
unsigned  domain_size,
yices_type  range
 

Return the type (-> d1 ... dn r) where

  • di is given by domain[i]
  • n is equal to domain_size
  • r is equal to range

domain_size must be positive

yices_type yices_mk_tuple_type yices_context  ctx,
yices_type   args[],
unsigned  size
 

Return the tuple type (tuple arg[0], ..., arg[size-1]),

size must be positive

yices_var_decl yices_mk_bool_var_decl yices_context  ctx,
const char *  name
 

Return a new boolean variable declaration.

It is an error to create two variables with the same name.

yices_var_decl yices_mk_var_decl yices_context  ctx,
const char *  name,
yices_type  ty
 

Return a new (global) variable declaration of type ty.

It is an error to create two variables with the same name.

yices_var_decl yices_get_var_decl_from_name yices_context  ctx,
const char *  name
 

Return the variable declaration associated with the given name.

Return 0 if there is no such variable declaration.

yices_var_decl yices_get_var_decl yices_expr  e  ) 
 

Return the variable declaration object associated with the given expression.

Return 0 if e is not a name expression.

This can be use to get the delcration of an expression e created using functions such as: yices_mk_bool_var, yices_mk_fresh_bool_var, or yices_mk_bool_var_from_decl, etc.

const char* yices_get_var_decl_name yices_var_decl  d  ) 
 

Return the name of variable declaration d.

yices_expr yices_mk_var_from_decl yices_context  ctx,
yices_var_decl  d
 

Return an instance of the variable declaration d.

yices_expr yices_mk_bool_var_from_decl yices_context  ctx,
yices_var_decl  d
 

Return an instance of variable declaration d.

d must be a Boolean variable declaration.

yices_expr yices_mk_bool_var yices_context  ctx,
const char *  name
 

Return a name expression for the given variable name.

yices_mk_bool_var(c, n1) == yices_mk_bool_var(c, n2) when strcmp(n1, n2) == 0.

See also:
yices_mk_bool_var_decl

yices_mk_fresh_bool_var

yices_mk_bool_var_from_decl

yices_expr yices_mk_fresh_bool_var yices_context  ctx  ) 
 

Return a fresh boolean variable.

yices_expr yices_mk_true yices_context  ctx  ) 
 

Return an expression representing true.

yices_expr yices_mk_false yices_context  ctx  ) 
 

Return an expression representing false.

yices_expr yices_mk_or yices_context  ctx,
yices_expr  args[],
unsigned  n
 

Return an expression representing the or of the given arguments.

n must be the number of elements in array args.

Warning:
n must be greater than zero.

yices_expr yices_mk_and yices_context  ctx,
yices_expr  args[],
unsigned  n
 

Return an expression representing the and of the given arguments.

n must be the number of elements in array args.

Warning:
n must be greater than zero.

yices_expr yices_mk_not yices_context  ctx,
yices_expr  a
 

Return an expression representing (not a).

yices_expr yices_mk_eq yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Return an expression representing a1 = a2.

yices_expr yices_mk_diseq yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Return an expression representing a1 /= a2.

yices_expr yices_mk_ite yices_context  ctx,
yices_expr  c,
yices_expr  t,
yices_expr  e
 

Return an expression representing (if c t e).

yices_expr yices_mk_app yices_context  ctx,
yices_expr  f,
yices_expr  args[],
unsigned  n
 

Return the term (f t1 ... tn)

The type of f must be a function-type, and its arity must be equal to the number of arguments.

yices_expr yices_mk_function_update yices_context  ctx,
yices_expr  f,
yices_expr  args[],
unsigned  n
yices_expr  v,
 

Return the term (update f (t1 ... tn) v)

The type of f must be a function type, and its arity must be equal to the number n of arguments.

v's type must be a subtype of f's range.

yices_expr yices_mk_tuple_literal yices_context  ctx,
yices_expr  args[],
unsigned  n
 

Return the term (mk-tuple t1 ... tn).

n must be positive and it must be the size of array args.

yices_expr yices_mk_num yices_context  ctx,
int  n
 

Return an expression representing the given integer.

yices_expr yices_mk_num_from_string yices_context  ctx,
const char *  n
 

Return an expression representing the number provided in ASCII format.

n must be a '\0'-terminated string in one of the following formats:

  • +/- <number>
  • +/- <number> . <fractional part>
  • +/- <numerator> / <denominator>
where <number>, <fractional part>, <numerator>, and <denominator> are strings of decimal digits.

The <denominator> must be non-zero and the + sign is optional.

yices_expr yices_mk_num_from_mpz yices_context  ctx,
const mpz_t  z
 

Construct a numerical expression form a GMP integer.

Warning:
  • You must include <gmp.h> before <yices_c.h> for this function to be available.
  • If you don't need GMP numbers, don't include <gmp.h>
See also:
yices_mk_num_from_mpq

yices_expr yices_mk_num_from_mpq yices_context  ctx,
const mpq_t  q
 

Construct a numerical expression form a GMP rational.

q must be canonicalized (see GMP documentation).

Warning:
  • You must include <gmp.h> before <yices_c.h> for this function to be available.
  • If you don't need GMP numbers, don't include <gmp.h>
See also:
yices_mk_num_from_mpz

yices_expr yices_mk_sum yices_context  ctx,
yices_expr  args[],
unsigned  n
 

Return an expression representing args[0] + ... + args[n-1].

n must be the number of elements in the array args.

Warning:
n must be greater than zero.

yices_expr yices_mk_sub yices_context  ctx,
yices_expr  args[],
unsigned  n
 

Return an expression representing args[0] - ... - args[n-1].

n must be the number of elements in the array args.

Warning:
n must be greater than zero.

yices_expr yices_mk_mul yices_context  ctx,
yices_expr  args[],
unsigned  n
 

Return an expression representing args[0] * ... * args[n-1].

n must be the number of elements in the array args.

Warning:
n must be greater than zero.

yices_expr yices_mk_lt yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Return an expression representing a1 < a2.

yices_expr yices_mk_le yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Return an expression representing a1 <= a2.

yices_expr yices_mk_gt yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Return an expression representing a1 > a2.

yices_expr yices_mk_ge yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Return an expression representing a1 >= a2.

yices_expr yices_mk_bv_constant yices_context  ctx,
unsigned  size,
unsigned long  value
 

Create a bit vector constant of size bits and of the given value.

size must be positive

yices_expr yices_mk_bv_constant_from_array yices_context  ctx,
unsigned  size,
int  bv[]
 

Create a bit vector constant from an array.

size must be positive and bv must be an array of size elements

bit i of the bitvector is set to 0 if bv[i] = 0 and to 1 if bv[i] != 0

yices_expr yices_mk_bv_add yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Bitvector addition.

a1 and a2 must be bitvector expression of same size.

yices_expr yices_mk_bv_sub yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Bitvector subtraction.

a1 and a2 must be bitvector expression of same size.

yices_expr yices_mk_bv_mul yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Bitvector multiplication.

a1 and a2 must be bitvector expression of same size. The result is truncated to that size too. E.g., multiplication of two 8-bit vectors gives an 8-bit result.

yices_expr yices_mk_bv_minus yices_context  ctx,
yices_expr  a1
 

Bitvector opposite (2s complement).

a1 must be bitvector expression. The result is (- a1)/

yices_expr yices_mk_bv_and yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Bitwise and.

a1 and a2 must be bitvector expression of same size.

yices_expr yices_mk_bv_or yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Bitwise or.

a1 and a2 must be bitvector expression of same size.

yices_expr yices_mk_bv_xor yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Bitwise exclusive or.

a1 and a2 must be bitvector expression of same size.

yices_expr yices_mk_bv_not yices_context  ctx,
yices_expr  a1
 

Bitwise negation.

yices_expr yices_mk_bv_concat yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Bitvector concatenation.

a1 and a2 must be two bitvector expressions.

a1 is the left part of the result and a2 the right part.

Assuming a1 and a2 have n1 and n2 bits, respectively, then the result is a bitvector concat of size n1 + n2.

Bit 0 of concat is bit 0 of a2 and bit n2 of concat is bit 0 of a1.

yices_expr yices_mk_bv_extract yices_context  ctx,
unsigned  end,
unsigned  begin,
yices_expr  a
 

Bitvector extraction.

a must a bitvector expression of size n with begin < end < n.

The result is the subvector a[begin .. end]

yices_expr yices_mk_bv_sign_extend yices_context  ctx,
yices_expr  a,
unsigned  n
 

Sign extension.

Append n times the most-significant bit of to the left of a

yices_expr yices_mk_bv_shift_left0 yices_context  ctx,
yices_expr  a,
unsigned  n
 

Left shift by n bits, padding with zeros.

yices_expr yices_mk_bv_shift_left1 yices_context  ctx,
yices_expr  a,
unsigned  n
 

Left shift by n bits, padding with ones.

yices_expr yices_mk_bv_shift_right0 yices_context  ctx,
yices_expr  a,
unsigned  n
 

Right shift by n bits, padding with zeros.

yices_expr yices_mk_bv_shift_right1 yices_context  ctx,
yices_expr  a,
unsigned  n
 

Right shift by n bits, padding with ones.

yices_expr yices_mk_bv_lt yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Unsigned comparison: (a1 < a2).

a1 and a2 must be bitvector expressions of same size.

yices_expr yices_mk_bv_le yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Unsigned comparison: (a1 <= a2).

a1 and a2 must be bitvector expressions of same size.

yices_expr yices_mk_bv_gt yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Unsigned comparison: (a1 > a2).

a1 and a2 must be bitvector expressions of same size.

<

yices_expr yices_mk_bv_ge yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Unsigned comparison: (a1 >= a2).

a1 and a2 must be bitvector expressions of same size.

yices_expr yices_mk_bv_slt yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Signed comparison: (a1 < a2).

a1 and a2 must be bitvector expression of same size.

yices_expr yices_mk_bv_sle yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Signed comparison: (a1 <= a2).

a1 and a2 must be bitvector expression of same size.

yices_expr yices_mk_bv_sgt yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Signed comparison: (a1 > a2).

a1 and a2 must be bitvector expressions of same size.

yices_expr yices_mk_bv_sge yices_context  ctx,
yices_expr  a1,
yices_expr  a2
 

Signed comparison: (a1 >= a2).

a1 and a2 must be bitvector expressions of same size.

void yices_pp_expr yices_expr  e  ) 
 

Pretty print the given expression on standard output.

Home Docs Download Mail Status FM Tools

Last modified: Thu 10 Apr 2014 17:11 PDT