Yices 1 C API Example

• Create a new empty C file (e.g., tst.c).
• Include yices_c.h.
• Implement the following simple main function.

  #include"yices_c.h"
  
  int main() {
    yices_context ctx = yices_mk_context();
  
    yices_del_context(ctx);
    return 0;
  }
  

• Assuming that yices_c.h is located at ~/include, libyices.a is located at ~/lib, and GMP is available in your system. The program can be compiled using:

  gcc -o tst -I ~/include -L ~/lib tst.c -lyices -lgmp -lstdc++
  

• The following small example illustrates other functions in the API:

  #include<stdio.h>
  #include"yices_c.h"
  
  int main() {
    yices_context ctx = yices_mk_context();
    yices_expr e1 = yices_mk_fresh_bool_var(ctx);
    yices_expr e2 = yices_mk_fresh_bool_var(ctx);
    yices_expr eq1 = yices_mk_eq(ctx, e1, e2);
    yices_assert(ctx, eq1);
    yices_dump_context(ctx);
    switch(yices_check(ctx)) {
    case l_true:
      printf("satisfiable\n");
      yices_model m = yices_get_model(ctx);
      printf("e1 = %d\n", yices_get_value(m, yices_get_var_decl(e1)));
      printf("e2 = %d\n", yices_get_value(m, yices_get_var_decl(e2)));
      yices_display_model(m);
      break;  
    case l_false:
      printf("unsatisfiable\n");
      break;
    case l_undef:
      printf("unknown\n");
      break;
    }
    yices_del_context(ctx);
    return 0;
  } 
  

• The following small example illustrates the EUF (equality and uninterpreted functions) related functions in the API:

  #include<stdio.h>
  #include"yices_c.h"
  
  int main() {
    yices_context ctx = yices_mk_context();
    yices_type ty  = yices_mk_type(ctx, "any");
    yices_type domain[1];
    domain[0] = ty;
    yices_type fty = yices_mk_function_type(ctx, domain, 1, ty);
    yices_var_decl fdecl = yices_mk_var_decl(ctx, "f", fty);
    yices_var_decl xdecl = yices_mk_var_decl(ctx, "x", ty);
    yices_var_decl ydecl = yices_mk_var_decl(ctx, "y", ty);
    yices_expr     f     = yices_mk_var_from_decl(ctx, fdecl);
    yices_expr     x     = yices_mk_var_from_decl(ctx, xdecl);
    yices_expr     y     = yices_mk_var_from_decl(ctx, ydecl);
    yices_expr args[1];
    args[0] = x;
    yices_expr     fx    = yices_mk_app(ctx, f, args, 1);
    args[0] = y;
    yices_expr     fy    = yices_mk_app(ctx, f, args, 1);
    yices_expr     eq    = yices_mk_eq(ctx, x, y);
    yices_expr     diseq = yices_mk_diseq(ctx, fx, fy);
    yices_assert(ctx, eq);
    yices_assert(ctx, diseq);
    if (yices_inconsistent(ctx))
      printf("unsat\n");
    yices_del_context(ctx);
    return 0;
  }
  

• The following small example illustrates linear arithmetic related functions in the API:

  #include<stdio.h>
  #include"yices_c.h"
  
  int main() {
    yices_context ctx = yices_mk_context();
    yices_type ty  = yices_mk_type(ctx, "int");
    yices_var_decl xdecl = yices_mk_var_decl(ctx, "x", ty);
    yices_var_decl ydecl = yices_mk_var_decl(ctx, "y", ty);
    yices_expr     x     = yices_mk_var_from_decl(ctx, xdecl);
    yices_expr     y     = yices_mk_var_from_decl(ctx, ydecl);
    yices_expr     n1    = yices_mk_num(ctx, 1);
    yices_expr     n2    = yices_mk_num(ctx, 2);
    yices_expr args[2];
    args[0] = x;
    args[1] = n1;
    yices_expr     e1    = yices_mk_sum(ctx, args, 2);  x + 1 
    args[0] = y;
    args[1] = n2;
    yices_expr     e2    = yices_mk_sub(ctx, args, 2);  y - 2 
    yices_expr     c1    = yices_mk_le(ctx,e1, e2);     x + n1 <= y - n2 
    yices_assert(ctx, c1);
    args[0] = x;
    args[1] = n2;
    yices_expr     e3    = yices_mk_sum(ctx, args, 2);  x + 2 
    yices_expr     c2    = yices_mk_le(ctx, y, e3);     y <= x + 2 
    yices_assert(ctx, c2);
    if (yices_inconsistent(ctx))
      printf("unsat\n");
    yices_del_context(ctx);
    return 0;
  }