Yices 1 C API Lite Example

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

  #include"yicesl_c.h"
  
  int main() {
    yicesl_context ctx = yicesl_mk_context();
  
    yicesl_del_context(ctx);
    return 0;
  }
  

• Assuming that yicesl_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<yicesl_c.h>
  
  void display(yicesl_context ctx) {
    if (yicesl_inconsistent(ctx)) 
      printf("unsatisfiable\n"); 
    else
      printf("satisfiable\n");
  }
  
  int main() {
    yicesl_context ctx = yicesl_mk_context();
    yicesl_set_output_file(".yices-output");
    yicesl_read(ctx, "(define x::int)");
    yicesl_read(ctx, "(define y::int)");
    yicesl_read(ctx, "(assert (= (+ x y) 0))");
    yicesl_read(ctx, "(assert (>= y 0))");
    display(ctx);
    yicesl_read(ctx, "(push)");
    yicesl_read(ctx, "(assert (>= x 1))");
    display(ctx);
    yicesl_read(ctx, "(pop)");
    yicesl_read(ctx, "(assert (>= x 0))");
    display(ctx);
    yicesl_read(ctx, "(set-evidence! true)");
    yicesl_read(ctx, "(check)");
    yicesl_del_context(ctx);
    return 0;
  }