C API

Typedefs

Enumerations

Functions

Assertion index, to identify retractable assertions.

Yices context.

A context stores a collection of declarations and assertions.

Yices expressions (abstract syntax tree).

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.

Yices types (abstract syntax tree).

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.

Iterator for scanning the boolean variables.

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

Enumerator:

l_false
l_undef
l_true

Assert a constraint in the logical context.

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

Assert a constraint that can be later retracted.

Returns:

An id that can be used to retract the constraint.

See also:

yices_retract

Assert a constraint in the logical context with weight w.

Returns:

An id that can be used to retract the constraint.

See also:

yices_retract

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.

Create an iterator that can be used to traverse the boolean variables (var_decl objects) in the given 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

Delete the given logical context.

See also:

yices_mk_context

Delete an iterator created with yices_create_var_decl_iterator.

Display the given model in the standard output.

Display the internal representation of the given logical context on stderr.

This function is mostly for debugging.

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

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

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

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 references (f 3)

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.

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

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

This function is only useful for assertion ids obtained using yices_assert_weighted, and yices_max_sat was used to build the model. That is the only scenario where an assertion may not be satisfied in a model produced by yices.

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

The value 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. Otherwise, if
• n is smaller than v's size, 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

Return the cost of model m.

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

Warning:

The model cost is computed automatically by yices_max_sat but not by yices_check. If yices_check returns l_true (or l_undef), you can call yices_compute_model_cost to compute the cost explicitly.

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

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

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

Return a model for a satisfiable logical context.

Warning:

The should be only called if yices_check or yices_max_sat returned l_true or l_undef.

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.

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.

Return the assignment for the variable v.

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

Return the variable declaration object associated with the given name expression.

Warning:

e must be a name expression created using methods such as: yices_mk_bool_var, yices_mk_fresh_bool_var, or yices_mk_bool_var_from_decl.

Return a variable declaration associated with the given name.

Return 0 if there is no variable declaration associated with the given name.

Return a name of a variable declaration.

Return 1 if the logical context is known to be inconsistent.

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

Return the next variable, and move the iterator.

See also:

yices_iterator_has_next

yices_create_var_decl_iterator

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

Compute the maximal satisfying assignment for the asserted weighted constraints.

• l_true means the maximal satisfying assignment was found
• l_false means it is unsatisfiable (this may happen if the context has unweighted constraints)
• l_undef means it was not possible to decide due to an incompleteness. If the result is l_true, then yices_get_model can be used to obtain a model.

See also:

yices_assert_weighted

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

Returns:

l_false if such a model doesn't exist.

Return an expression representing the and of the given arguments.

n is the number of elements in the array args.

Warning:

n must be greater than zero.

Return a function application term (f t1 ... tn).

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

Returns the bitvector type (bv[size]).

Size must be positive.

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

Return a new boolean variable declaration.

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

Return a name expression (instance) using the given variable declaration.

Bitvector addition.

a1 and a2 must be bitvector expression of same size.

Bitwise and.

a1 and a2 must be bitvector expression of same size.

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.

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

size must be positive

Create a bit vector constant from an array.

size must be positive 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

Bitvector extraction.

a must a bitvector expression of size n with begin < end < n. The result is the subvector a[begin .. end]

Unsigned comparison: (a1 >= a2).

a1 and a2 must be bitvector expression of same size.

Unsigned comparison: (a1 > a2).

a1 and a2 must be bitvector expression of same size.

Unsigned comparison: (a1 <= a2).

a1 and a2 must be bitvector expression of same size.