cmake build

1 files changed, 190 insertions, 0 deletions

diff --git a/omegalib/examples/c_code/library_example.c b/omegalib/examples/c_code/library_example.c
new file mode 100644
index 0000000..06f6570
--- /dev/null
+++ b/omegalib/examples/c_code/library_example.c
@@ -0,0 +1,190 @@
+/*
+  IF THESE EXAMPLES CHANGE, CHANGE construction.tex CORRESPONDINGLY
+
+  S1 := { [t] : 1 <= t <= n }
+
+  S2 := { [x] : (0 <= x <= 100 and
+  exists y : (2n <= y <= x and y is odd))
+  or x = 17 }
+
+  R := { [i,j] -> [i',j'] : 1 <= i <= i' <= n and not (F(i) = F(i'))
+  and 1 <= j, j' <= m }
+*/
+
+//BEGIN PART 1
+#include <omega.h>
+using namespace omega;
+int main() {
+  Relation S1(1), S2(1), R(2,2);
+  S1.name_set_var(1, "t");
+  S2.name_set_var(1, "x");
+
+  assert(!R.is_set());
+  assert(S1.is_set());
+  assert(S2.is_set());
+
+  Free_Var_Decl n("n");
+  Free_Var_Decl m("m");
+  Free_Var_Decl f("F", 1);
+
+  Variable_ID S1s_n = S1.get_local(&n);
+  Variable_ID S2s_n = S2.get_local(&n);
+
+  Variable_ID Rs_n = R.get_local(&n);
+  Variable_ID Rs_m = R.get_local(&m);
+  Variable_ID Rs_f_in  = R.get_local(&f, Input_Tuple);
+  Variable_ID Rs_f_out = R.get_local(&f, Output_Tuple);
+    
+  R.name_input_var(1, "i");
+  R.name_input_var(2, "j");
+  R.name_output_var(1, "i'");
+  R.name_output_var(2, "j'");
+  Variable_ID i = R.input_var(1);
+  Variable_ID j = R.input_var(2);
+  Variable_ID i2 = R.output_var(1);
+  Variable_ID j2 = R.output_var(2);
+
+  Variable_ID t = S1.set_var(1);
+  Variable_ID x = S2.set_var(1);
+//END PART 1
+//BEGIN PART 2
+  F_And *S1_root = S1.add_and();
+
+  GEQ_Handle tmin = S1_root->add_GEQ();   // t-1 >= 0
+  tmin.update_coef(t, 10);
+  tmin.update_coef(t, -9);       // t now has coef. 1
+  tmin.update_const(-1);
+  GEQ_Handle tmax = S1_root->add_GEQ();   // n-t >= 0
+  tmax.update_coef(S1s_n,1);
+  tmax.update_coef(t, -1);
+
+
+  F_Or  *S2_root = S2.add_or();
+  F_And *part1 = S2_root->add_and();
+
+  GEQ_Handle xmin = part1->add_GEQ();
+  xmin.update_coef(x,1);
+  GEQ_Handle xmax = part1->add_GEQ();
+  xmax.update_coef(x,-1);
+  xmax.update_const(100);
+
+  F_Exists *exists_y = part1->add_exists();
+  Variable_ID y = exists_y->declare("y");
+
+  F_And *y_stuff = exists_y->add_and();
+  GEQ_Handle ymin = y_stuff->add_GEQ();
+  ymin.update_coef(y,1);
+  ymin.update_coef(S2s_n,-2);
+  GEQ_Handle ymax = y_stuff->add_GEQ();
+  ymax.update_coef(x,1);
+  ymax.update_coef(y,-1);
+  Stride_Handle y_even = y_stuff->add_stride(2);
+  y_even.update_coef(y,1);
+  y_even.update_const(1);
+
+  F_And *part2 = S2_root->add_and();
+
+  EQ_Handle xvalue = part2->add_EQ();
+  xvalue.update_coef(x,1);
+  xvalue.update_const(-17);
+//END PART 2
+//BEGIN PART 3
+  F_And *R_root = R.add_and();
+
+  GEQ_Handle imin = R_root->add_GEQ();
+  imin.update_coef(i,1);
+  imin.update_const(-1);
+  GEQ_Handle imax = R_root->add_GEQ();
+  imax.update_coef(i2,1);
+  imax.update_coef(i,-1);
+  GEQ_Handle i2max = R_root->add_GEQ();
+  i2max.update_coef(Rs_n,1);
+  i2max.update_coef(i2,-1);
+
+  EQ_Handle f_eq = R_root->add_not()->add_and()->add_EQ();
+  f_eq.update_coef(Rs_f_in,-1);
+  f_eq.update_coef(Rs_f_out,1);  // F(In) - F(Out) = 0
+
+  GEQ_Handle jmin = R_root->add_GEQ();
+  jmin.update_coef(j,1);
+  jmin.update_const(-1);
+  GEQ_Handle jmax = R_root->add_GEQ();
+  jmax.update_coef(Rs_m,1);
+  jmax.update_coef(j,-1);
+    
+  GEQ_Handle j2min = R_root->add_GEQ();
+  j2min.update_coef(j2,1);
+  j2min.update_const(-1);
+  GEQ_Handle j2max = R_root->add_GEQ();
+  j2max.update_coef(Rs_m,1);
+  j2max.update_coef(j2,-1);
+//END PART 3
+//BEGIN PART 4
+  S1.print_with_subs(stdout);
+  assert(S1.is_upper_bound_satisfiable());
+  assert(!S1.is_tautology());
+  S1.print_with_subs(stdout);  // same as above print
+  printf("\n");
+
+  S2.print();
+  assert(S2.is_upper_bound_satisfiable());
+  assert(!S2.is_tautology());
+  S2.print();                 // different from above
+  printf("\n");
+
+  assert(R.is_upper_bound_satisfiable());
+  assert(!R.is_tautology());
+  R.print_with_subs(stdout);
+
+  coef_t lb, ub;
+  bool coupled;
+  R.query_difference(i2, i, lb, ub, coupled);
+  assert(lb == 1);        // i < i2: i2 - i1 > 0
+  assert(ub == posInfinity);
+
+  for(DNF_Iterator di(R.query_DNF()); di; di++) {
+    printf("In next conjunct,\n");
+    for(EQ_Iterator ei = (*di)->EQs(); ei; ei++) {
+      printf("  In next equality constraint,\n");
+      for(Constr_Vars_Iter cvi(*ei); cvi; cvi++)
+        printf("    Variable %s has coefficient "coef_fmt"\n",
+               (*cvi).var->char_name(), 
+               (*cvi).coef);
+    }
+    for(GEQ_Iterator gi = (*di)->GEQs(); gi; gi++) {
+      printf("  In next inequality constraint,\n");
+      for(Constr_Vars_Iter cvi(*gi); cvi; cvi++)
+        printf("    Variable %s has coefficient "coef_fmt"\n",
+               (*cvi).var->char_name(), 
+               (*cvi).coef);
+      int c = (*gi).get_const();
+      if (c != 0)
+        printf("    Constant %d\n", c);
+    }
+        
+    printf("\n");
+  }
+//END PART 4
+//BEGIN PART 5
+  Relation S1_or_S2 = Union(copy(S1), copy(S2));
+
+  // NOTE! THE FOLLOWING KILLS S1 AND S2
+  Relation S1_and_S2 = Intersection(S1, S2);
+
+  S1_or_S2.is_upper_bound_satisfiable();
+  S1_and_S2.is_upper_bound_satisfiable();
+
+  S1_or_S2.print();
+  printf("\n");
+
+  S1_and_S2.print();    
+  printf("\n");
+
+  Relation R_R = Composition(copy(R), R);
+  R_R.query_difference(i2, i, lb, ub, coupled);
+  assert(lb == 2);
+  assert(ub == posInfinity);
+
+  return 0;
+}
+//END PART 5