C API


Functions

void yices_set_verbosity (int l)
 Set the verbosity level.
char * yices_version ()
 Return the yices version number.
yices_context yices_mk_context ()
 Create a logical context.
void yices_del_context (yices_context ctx)
 Delete the given logical context.
void yices_reset (yices_context ctx)
 Reset the given logical context.
void yices_dump_context (yices_context ctx)
 Display the internal representation of the given logical context in the standard error output. This function is used for debugging purposes.
void yices_push (yices_context ctx)
 Create a backtracking point in the given logical context.
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)
 Similar to yices_assert_weighted, but the weight is considered to be infinite.
void yices_retract (yices_context ctx, assertion_id id)
 Retract a retractable or weighted constraint.
int yices_inconsistent (yices_context ctx)
 Return 1 if the logical context is known to be inconsistent.
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, and 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.
lbool yices_max_sat (yices_context ctx)
 Compute the maximal satisfying assingment 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), and 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.
yices_model yices_get_model (yices_context ctx)
 Return a model for a satisfiable logical context.
lbool yices_get_value (yices_model m, yices_var_decl v)
 Return the assignment for the variable v. The result is l_undef if the value of v is a "don't care".
int yices_get_assertion_value (yices_model m, assertion_id id)
 Return 1 (0) if the given assertion id was satisfied (not satisfied) in the given module. 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.
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 the given model. The cost is the sum of the weights of unsatisfied constraints.
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_bool_var (yices_context ctx, 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_var_decl yices_get_var_decl (yices_expr e)
 Return the variable declaration object associated with the given name expression.
yices_var_decl yices_mk_bool_var_decl (yices_context ctx, char *name)
 Return a new boolean variable declaration. It is an error to create two variables with the same name.
char * yices_get_var_decl_name (yices_var_decl d)
 Return a name of a 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_or (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing the or of the given arguments. n is the number of elements in the array args.
yices_expr yices_mk_and (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing the and of the given arguments. n is the number of elements in the array args.
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_not (yices_context ctx, yices_expr a)
 Return an expression representing (not a).
yices_var_decl_iterator yices_create_var_decl_iterator (yices_context c)
 Create an iterator that can be used to traverse the 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.
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_type yices_mk_type (yices_context ctx, 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_function_type (yices_context ctx, yices_type domain[], unsigned domain_size, yices_type range)
 Return a function type (-> d1 ... dn r).
yices_var_decl yices_mk_var_decl (yices_context ctx, 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, char *name)
 Return a variable declaration associated with the given name. Return 0 if there is no variable declaration associated with the given name.
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_app (yices_context ctx, yices_expr f, yices_expr args[], unsigned n)
 Return a function application term (f t1 ... tn). The type of f must be a function-type, and its arity should be equal to the number of arguments.
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, char *n)
 Return an expression representing the number provided in ASCII format.
yices_expr yices_mk_sum (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing args[0] + ... + args[n-1]. n is the number of elements in the array args.
yices_expr yices_mk_sub (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing args[0] - ... - args[n-1]. n is the number of elements in the array args.
yices_expr yices_mk_mul (yices_context ctx, yices_expr args[], unsigned n)
 Return an expression representing args[0] * ... * args[n-1]. n is the number of elements in the array args.
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.
void yices_pp_expr (yices_expr e)
 Pretty print the given expression in the standard output.

Function Documentation

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. The method yices_inconsistent may be used to check that.

assertion_id yices_assert_retractable (  yices_context  ctx,
yices_expr  expr
) 
 

Similar to yices_assert_weighted, but the weight is considered to be infinite.

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 id that can be used to retract the constraint.

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

yices_var_decl_iterator yices_create_var_decl_iterator (  yices_context  c  ) 
 

Create an iterator that can be used to traverse the 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

void yices_del_context (  yices_context  ctx  ) 
 

Delete the given logical context.

See also:
yices_mk_context

void yices_del_iterator (  yices_var_decl_iterator  it  ) 
 

Delete an iterator created with yices_create_var_decl_iterator.

void yices_display_model (  yices_model  m  ) 
 

Display the given model in the standard output.

void yices_dump_context (  yices_context  ctx  ) 
 

Display the internal representation of the given logical context in the standard error output. This function is used for debugging purposes.

int yices_get_assertion_value (  yices_model  m,
assertion_id  id
) 
 

Return 1 (0) if the given assertion id was satisfied (not satisfied) in the given module. 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.

long long yices_get_cost (  yices_model  m  ) 
 

Return the cost of the given model. The cost is the sum of the weights of unsatisfied constraints.

Warning:
This method should be only called for models built using yices_max_sat.

yices_model yices_get_model (  yices_context  ctx  ) 
 

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. Return 0 if a model is not available. Calls to functions which modify the context invalidate the model.

lbool yices_get_value (  yices_model  m,
yices_var_decl  v
) 
 

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

yices_var_decl yices_get_var_decl (  yices_expr  e  ) 
 

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.

yices_var_decl yices_get_var_decl_from_name (  yices_context  ctx,
char *  name
) 
 

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

char* yices_get_var_decl_name (  yices_var_decl  d  ) 
 

Return a name of a variable declaration.

int yices_inconsistent (  yices_context  ctx  ) 
 

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

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.

lbool yices_max_sat (  yices_context  ctx  ) 
 

Compute the maximal satisfying assingment 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), and 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

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

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.

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

Return a function application term (f t1 ... tn). The type of f must be a function-type, and its arity should be equal to the number of arguments.

yices_expr yices_mk_bool_var (  yices_context  ctx,
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_var_decl yices_mk_bool_var_decl (  yices_context  ctx,
char *  name
) 
 

Return a new boolean variable declaration. It is an error to create two variables with the same name.

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_context yices_mk_context (   ) 
 

Create a logical context.

Definition at line 40 of file yices_c_wrapper.cpp.

References yices_context::m_context, and yices_context::m_next_id.

yices_expr yices_mk_diseq (  yices_context  ctx,
yices_expr  a1,
yices_expr  a2
) 
 

Return an expression representing a1 /= a2.

yices_expr yices_mk_eq (  yices_context  ctx,
yices_expr  a1,
yices_expr  a2
) 
 

Return an expression representing a1 = a2.

yices_expr yices_mk_false (  yices_context  ctx  ) 
 

Return an expression representing false.

yices_expr yices_mk_fresh_bool_var (  yices_context  ctx  ) 
 

Return a fresh boolean variable.

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_expr yices_mk_ge (  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_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_le (  yices_context  ctx,
yices_expr  a1,
yices_expr  a2
) 
 

Return an expression representing a1 <= a2.

yices_expr yices_mk_lt (  yices_context  ctx,
yices_expr  a1,
yices_expr  a2
) 
 

Return an expression representing a1 < a2.

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

Return an expression representing args[0] * ... * args[n-1]. n is the number of elements in the 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_num (  yices_context  ctx,
int  n
) 
 

Return an expression representing the given integer.

yices_expr yices_mk_num_from_string (  yices_context  ctx,
char *  n
) 
 

Return an expression representing the number provided in ASCII format.

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

Return an expression representing the or of the given arguments. n is 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 is the number of elements in the array args.

Warning:
n must be greater than zero.

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

Return an expression representing args[0] + ... + args[n-1]. n is the number of elements in the array args.

Warning:
n must be greater than zero.

yices_expr yices_mk_true (  yices_context  ctx  ) 
 

Return an expression representing true.

yices_type yices_mk_type (  yices_context  ctx,
char *  name
) 
 

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

Remarks:
number, real, int, nat, bool, any are builtin types.

yices_var_decl yices_mk_var_decl (  yices_context  ctx,
char *  name,
yices_type  ty
) 
 

Return a new (global) variable declaration. It is an error to create two variables with the same name.

yices_expr yices_mk_var_from_decl (  yices_context  ctx,
yices_var_decl  d
) 
 

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

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_pp_expr (  yices_expr  e  ) 
 

Pretty print the given expression in the standard output.

void yices_push (  yices_context  ctx  ) 
 

Create a backtracking point in the given logical context.

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_reset (  yices_context  ctx  ) 
 

Reset the given logical context.

void yices_retract (  yices_context  ctx,
assertion_id  id
) 
 

Retract a retractable or weighted constraint.

See also:
yices_assert_weighted

yices_assert_retractable

void yices_set_verbosity (  int  l  ) 
 

Set the verbosity level.

Definition at line 19 of file yices_c_wrapper.cpp.

References yices::set_verbosity_level().

char* yices_version (   ) 
 

Return the yices version number.

Definition at line 23 of file yices_c_wrapper.cpp.

References g_yices_version.

Generated on Thu Jul 13 11:47:56 2006 for Yices by  doxygen 1.4.5