YICES_SMT_SOLVER_IN_ROSE

Hi,
   I have now hooked up the Yices Satisfiability Modulo Theories (SMT)
solver to ROSE.  It is now a configuration option to use it.  This permits
a lot of interesting things to be done, and I look forward to playing with
it more.  Here is an example from their web page which I have
running in a ROSE translator.

It test if for "n1 = 1" and "n2 = 2" and the assertion that
"x + n1 <= y - n2" if "y <= x + 2" is satisfied when "x = 2"
so that the code this might come from is:
int n1 = 1;
int n2 = 2;
int x;
assert(x + n1 <= y - n2);
x += 2;
if (y <= x + 2)  {/* test if this is reachable */}

I think that I have the example correct :-).
Yices can handle much more complex expressions
and has been winning a number of competitions for
SMT solvers over the years.  It is available at:
     http://yices.csl.sri.com/index.shtml

   This opens the door to a whole new set of checkers in compass with
much deeper analysis capabilities to prove things about code.
And of course it should be some fun.  Importantly,
this work should also scale well to large scale applications.

   At the moment I have not written any checker that uses this work,
but we will likely be doing that soon as we play with it more. this
work is not in the version of ROSE that I just released, but I could
get it to any of you if your interested (but I suggest you wait and
let us figure it out more before that).


Example of code required to verify the previous code example:
void
test_yices_linear_arithmetic_API()
   {
  // Example from the Yices web page (small example illustrates linear arithmetic related functions in the API)
     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) == true)
          printf("unsat\n");
     yices_del_context(ctx);
   }