Yices 1 C API

Typedefs

Enumerations

Structures

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

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

Return the yices version number.

Set the verbosity level.

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

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

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

This flag usually improves performance (default = false).

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.

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.

Set the initial cost for a maxsat problem.

Create the logical context.

Delete the logical context.

See also:

yices_mk_context

Reset the logical context.

Display the internal representation of the logical context on stderr.

This function is mostly for debugging.

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.

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

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.

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

Assert a constraint that can be retracted later.

Returns:

An id that can be used to retract the constraint.

See also:

yices_retract

Retract a retractable or weighted constraint.

See also:

yices_assert_weighted

yices_assert_retractable

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.

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.

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

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.

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.

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

See also

• yices_get_unsat_core

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.

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.

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

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

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

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

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

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.

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.

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

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

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

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

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.

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)

Display the given model on standard output.

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.

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

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

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.

Delete an iterator created with yices_create_var_decl_iterator.

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

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

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

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

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.

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

size must be positive.

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

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

size must be positive

Return a new boolean variable declaration.

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

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

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

Return the variable declaration associated with the given name.

Return 0 if there is no such variable declaration.

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.

Return the name of variable declaration d.

Return an instance of the variable declaration d.

Return an instance of variable declaration d.

d must be a Boolean variable declaration.

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 fresh boolean variable.

Return an expression representing true.

Return an expression representing false.

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.

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.

Return an expression representing (not a).

Return an expression representing a1 = a2.

Return an expression representing a1 /= a2.

Return an expression representing (if c t e).

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.

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.

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

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

Return an expression representing the given integer.

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>

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

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

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.

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.

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.

Return an expression representing a1 < a2.

Return an expression representing a1 <= a2.

Return an expression representing a1 > a2.

Return an expression representing a1 >= a2.

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

Bitvector addition.

a1 and a2 must be bitvector expression of same size.

Bitvector subtraction.

a1 and a2 must be bitvector expression of same size.

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.

Bitvector opposite (2s complement).

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

Bitwise and.

a1 and a2 must be bitvector expression of same size.

Bitwise or.

a1 and a2 must be bitvector expression of same size.

Bitwise exclusive or.

a1 and a2 must be bitvector expression of same size.

Bitwise negation.

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.

Bitvector extraction.

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

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

Sign extension.

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

Left shift by n bits, padding with zeros.

Left shift by n bits, padding with ones.

Right shift by n bits, padding with zeros.

Right shift by n bits, padding with ones.

Unsigned comparison: (a1 < a2).

a1 and a2 must be bitvector expressions of same size.

Unsigned comparison: (a1 <= a2).

a1 and a2 must be bitvector expressions of same size.

Unsigned comparison: (a1 > a2).

a1 and a2 must be bitvector expressions of same size.

Unsigned comparison: (a1 >= a2).

a1 and a2 must be bitvector expressions of same size.

Signed comparison: (a1 < a2).

a1 and a2 must be bitvector expression of same size.

Signed comparison: (a1 <= a2).

a1 and a2 must be bitvector expression of same size.

Signed comparison: (a1 > a2).

a1 and a2 must be bitvector expressions of same size.

Signed comparison: (a1 >= a2).

a1 and a2 must be bitvector expressions of same size.

Pretty print the given expression on standard output.