diff options
Diffstat (limited to 'omegalib/examples/c_code/library_example.c')
| -rw-r--r-- | omegalib/examples/c_code/library_example.c | 190 |
1 files changed, 0 insertions, 190 deletions
diff --git a/omegalib/examples/c_code/library_example.c b/omegalib/examples/c_code/library_example.c deleted file mode 100644 index 06f6570..0000000 --- a/omegalib/examples/c_code/library_example.c +++ /dev/null @@ -1,190 +0,0 @@ -/* - 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 |