omega_lib/doc/example.c

   1 #include <presburger.h>
   2
   3 THIS NEEDS TO BE A LOT SIMPLER - I'M CUTTING IT DOWN
   4
   5 // R := { [i,j] -> [i', j'] :
   6 //        1 <= i, i' <= n && 1 <= j <= L(i) && 1 <= j' <= m &&
   7 //        j = j' && i < i' }
   8 //
   9 // S := { [x,y] : 1 <= x <= n && y <= x + 5 && x is divisible by 17 &&
  10 //        there exists z such that y <= z <= x &&
  11 //        ( z is divisible by 8 || z+5x is divisible by 12 ) }
  12
  13 main()
  14     {
  15     Relation R(2,2), S(2);
  16     S.name_set_var(1, "x");
  17     S.name_set_var(2, "y");
  18
  19     assert(!R.is_set());
  20     assert( S.is_set());
  21
  22     Free_Var_Decl n("n");
  23     Free_Var_Decl m("m");
  24     Free_Var_Decl l("L", 1);
  25
  26     Variable_ID local_n = R.get_local(&n);
  27     Variable_ID local_m = R.get_local(&m);
  28     Variable_ID l_in    = R.get_local(&l, Input_Tuple);
  29     Variable_ID l_out   = R.get_local(&l, Output_Tuple);
  30
  31     Variable_ID in1 = R.input_var(1);
  32     Variable_ID in2 = R.input_var(2);
  33     Variable_ID out1 = R.output_var(1);
  34     Variable_ID out2 = R.output_var(2);
  35
  36     Variable_ID x = S.set_var(1);
  37     Variable_ID y = S.set_var(2);
  38
  39     F_And *S_root = S.add_and();
  40
  41     GEQ_Handle xmin = S_root->add_GEQ();  // x-1 >= 0
  42     xmin.update_coef(x, 1);
  43     xmin.update_const(-1);
  44     GEQ_Handle xmax = S_root->add_GEQ();  // n-x >= 0
  45     xmax.update_coef(x, -1);
  46     xmax.update_coef(S.get_local(&n), 1);
  47     GEQ_Handle ymax = S_root->add_GEQ();  // x+5-y >= 0
  48     ymax.update_coef(x, 1);
  49     ymax.update_coef(y, -1);
  50     ymax.update_const(5);
  51
  52     // x is divisible by 17
  53     S_root->add_stride(17).update_coef(x,1);
  54
  55     F_Exists *e = S_root->add_exists();
  56
  57     Variable_ID z = e->declare("z");      // exists z
  58     F_And *z_stuff = e->add_and();
  59
  60     GEQ_Handle zmin = z_stuff->add_GEQ(); // z-y >= 0
  61     zmin.update_coef(z,1);
  62     zmin.update_coef(y,-1);
  63     GEQ_Handle zmax = z_stuff->add_GEQ(); // x-z >= 0
  64     zmax.update_coef(x,1);
  65     zmax.update_coef(z,-1);
  66
  67     F_Or *o = z_stuff->add_or();
  68     Stride_Handle z8  = o->add_and()->add_stride(8);
  69     z8.update_coef(z,1);         // z divisible by 8
  70
  71     Stride_Handle z12 = o->add_and()->add_stride(12);
  72     z12.update_coef(z,1);
  73     z12.update_coef(x,5);    // z+5x divisible by 12
  74
  75     S.finalize();
  76     S.prefix_print();
  77     S.is_upper_bound_satisfiable();
  78     S.prefix_print();
  79     }
  80