Yices: 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;
}