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