diff options
Diffstat (limited to 'omegalib/omega/src/Relations.cc')
| -rw-r--r-- | omegalib/omega/src/Relations.cc | 2882 |
1 files changed, 0 insertions, 2882 deletions
diff --git a/omegalib/omega/src/Relations.cc b/omegalib/omega/src/Relations.cc deleted file mode 100644 index d7dbe86..0000000 --- a/omegalib/omega/src/Relations.cc +++ /dev/null @@ -1,2882 +0,0 @@ -/***************************************************************************** - Copyright (C) 1994-2000 the Omega Project Team - Copyright (C) 2005-2011 Chun Chen - All Rights Reserved. - - Purpose: - Integer set and relation operations. - - Notes: - - History: - 04/22/09 merge_rels, Chun Chen -*****************************************************************************/ - -#include <omega/Relation.h> -#include <omega/Rel_map.h> -#include <omega/pres_tree.h> -#include <omega/pres_dnf.h> -#include <omega/pres_conj.h> -#include <omega/hull.h> -#include <basic/Tuple.h> -#include <basic/Map.h> -#include <basic/util.h> -#include <omega/omega_i.h> -#if defined STUDY_EVACUATIONS -#include <omega/evac.h> -#endif -#include <assert.h> - -namespace omega { - -#define CHECK_MAYBE_SUBSET 1 - -int relation_debug=0; - -namespace { - int leave_pufs_untouched = 0; - Variable_ID_Tuple exists_ids; - List<int> exists_numbers; - F_And * and_below_exists; -} - -/* The following allows us to avoid warnings about passing - temporaries as non-const references. This is useful but - has suddenly become illegal. */ - -Relation consume_and_regurgitate(NOT_CONST Relation &R) { - if(!R.is_null()) - ((Relation &) R).finalize(); - Relation S = (Relation &) R; - (Relation &) R = Relation::Null(); - return S; -} - - -// -// r1 Union r2. -// align the input tuples (if any) for F and G -// align the output tuples (if any) for F and G -// match named variables in F and G -// formula is f | g -// -Relation Union(NOT_CONST Relation &input_r1, - NOT_CONST Relation &input_r2) { - Relation r1 = consume_and_regurgitate(input_r1); - Relation r2 = consume_and_regurgitate(input_r2); - if (r1.is_null()) - return r2; - else if (r2.is_null()) - return r1; - if (r1.n_inp() != r2.n_inp() || r1.n_out() != r2.n_out()) - throw std::invalid_argument("relation arity does not match"); - - // skip_set_checks++; - // assert(r1.n_inp() == r2.n_inp()); - // assert(r1.n_out() == r2.n_out()); - // assert(!r1.is_null() && !r2.is_null()); - int in = r1.n_inp(), out = r1.n_out(); - // skip_set_checks--; - - return MapAndCombineRel2(r1, r2, Mapping::Identity(in, out), - Mapping::Identity(in,out), Comb_Or); -} - - -// -// F intersection G -// align the input tuples (if any) for F and G -// align the output tuples (if any) for F and G -// match named variables in F and G -// formula is f & g -// -Relation Intersection(NOT_CONST Relation &input_r1, - NOT_CONST Relation &input_r2) { - Relation r1 = consume_and_regurgitate(input_r1); - Relation r2 = consume_and_regurgitate(input_r2); - if (r1.is_null()) - return r2; - else if (r2.is_null()) - return r1; - if (r1.n_inp() != r2.n_inp() || r1.n_out() != r2.n_out()) - throw std::invalid_argument("relation arity does not match"); - - // skip_set_checks++; - // assert(r1.n_inp() == r2.n_inp()); - // assert(r1.n_out() == r2.n_out()); - // assert(!r1.is_null() && !r2.is_null()); - int in = r1.n_inp(), out = r1.n_out(); - // skip_set_checks--; - - return MapAndCombineRel2(r1, r2, Mapping::Identity(in,out), - Mapping::Identity(in,out), Comb_And); -} - - -// -// F \ G (the relation F restricted to domain G) -// align the input tuples for F and G -// match named variables in F and G -// formula is f & g -// -Relation Restrict_Domain(NOT_CONST Relation &input_r1, - NOT_CONST Relation &input_r2) { - Relation r1 = consume_and_regurgitate(input_r1); - Relation r2 = consume_and_regurgitate(input_r2); - if (r1.is_null()) - return r1; - else if (r2.is_null()) - return r1; - if (r1.n_inp() != r2.n_set()) - throw std::invalid_argument("relation arity does not match"); - - // assert(!r1.is_null() && !r2.is_null()); - // skip_set_checks++; - // assert(r1.n_inp() == r2.n_set()); - // assert(r2.is_set()); - int in = r1.n_inp(), out = r1.n_out(); - // skip_set_checks--; - - int i; - Mapping m2(r2.n_set()); - for(i=1; i<=r2.n_set(); i++) m2.set_map_set(i, Input_Var,i); - - // skip_set_checks++; - assert(r2.query_guaranteed_leading_0s() == -1 && - r2.query_possible_leading_0s() == -1); - // skip_set_checks--; - - Relation result = MapAndCombineRel2(r1, r2, Mapping::Identity(in,out), - m2, Comb_And); - // FERD -- update leading 0's - the may close up? - //result.invalidate_leading_info(); // could do better - return result; -} - -// -// -// F / G (the relation F restricted to range G) -// align the output tuples for F and G -// match named variables in F and G -// formula is f & g -// -Relation Restrict_Range(NOT_CONST Relation &input_r1, - NOT_CONST Relation &input_r2) { - Relation r1 = consume_and_regurgitate(input_r1); - Relation r2 = consume_and_regurgitate(input_r2); - if (r1.is_null()) - return r1; - else if (r2.is_null()) - return r1; - if (r1.n_out() != r2.n_set()) - throw std::invalid_argument("relation arity does not match"); - - // skip_set_checks++; - // assert(r1.n_out() == r2.n_set()); - // assert(r2.is_set()); - // assert(!r1.is_null() && !r2.is_null()); - int in = r1.n_inp(), out = r1.n_out(); - // skip_set_checks--; - - int i; - Mapping m2(r2.n_set()); - for(i=1; i<=r2.n_set(); i++) m2.set_map_set(i, Output_Var,i); - - // skip_set_checks++; - assert(r2.query_guaranteed_leading_0s() == -1 && - r2.query_possible_leading_0s() == -1); - // skip_set_checks--; - - Relation result = MapAndCombineRel2(r1, r2, Mapping::Identity(in, out), - m2, Comb_And); - // FERD -- update leading 0's - the may close up? - // result.invalidate_leading_info(); // could do better - return result; -} - - -// -// Add input variable to relation. -// -Relation Extend_Domain(NOT_CONST Relation &S) { - Relation R = consume_and_regurgitate(S); - if (R.is_null()) - throw std::invalid_argument("cannot extend domain on null relation"); - - // assert(!R.is_null() && (skip_set_checks || !R.is_set())); - // assert(!R.is_null()); - Rel_Body *r = R.split(); - r->In_Names.append(Const_String()); - r->number_input++; - assert(!r->is_null()); - - if (r->number_input <= r->number_output) - R.invalidate_leading_info(r->number_input); - - return R; -} - -// -// Add more input variables to relation. -// -Relation Extend_Domain(NOT_CONST Relation &S, int more) { - Relation R = consume_and_regurgitate(S); - if (R.is_null()) - throw std::invalid_argument("cannot extend domain on null relation"); - - // assert(!R.is_null()); - R.split(); - for (int i=1; i<=more; i++) R = Extend_Domain(R); - return R; -} - - -// -// Add output variable to relation. -// -Relation Extend_Range(NOT_CONST Relation &S) { - Relation R = consume_and_regurgitate(S); - if (R.is_null()) - throw std::invalid_argument("cannot extend range on null relation"); - - // assert(!R.is_null() && !R.is_set()); - // assert(!R.is_null()); - Rel_Body *r = R.split(); - r->Out_Names.append(Const_String()); - r->number_output++; - assert(!r->is_null()); - - if (r->number_output <= r->number_input) - R.invalidate_leading_info(r->number_output); - - return R; -} - -// -// Add more output variables to relation. -// -Relation Extend_Range(NOT_CONST Relation &S, int more) { - Relation R = consume_and_regurgitate(S); - - // assert(!R.is_null()); - R.split(); - for (int i=1; i<=more; i++) R = Extend_Range(R); - return R; -} - - -// -// Add set variable to set. -// -Relation Extend_Set(NOT_CONST Relation &S) { - Relation R = consume_and_regurgitate(S); - if (R.is_null()) - throw std::invalid_argument("cannot extend set on null relation"); - if (R.n_out() > 0) - throw std::invalid_argument("relation must be a set"); - - // assert(!R.is_null() && R.is_set()); - Rel_Body *r = R.split(); - r->In_Names.append(Const_String()); - r->number_input++; - assert(!r->is_null()); - return R; -} - -// -// Add more variables to set -// -Relation Extend_Set(NOT_CONST Relation &S, int more) { - Relation R = consume_and_regurgitate(S); - R.split(); - for (int i=1; i<=more; i++) R = Extend_Set(R); - return R; -} - - - -// -// Domain and Range. -// Make output (input) variables wildcards and simplify. -// Move all UFS's to have have the remaining tuple as an argument, -// and maprel will move them to the set tuple -// RESET all leading 0's -// -Relation Domain(NOT_CONST Relation &S) { - Relation r = consume_and_regurgitate(S); - if (r.is_null()) - return r; - - // assert(!S.is_null()); - // assert(!r.is_set()); - // skip_set_checks++; - int i; - Mapping m1(r.n_inp(), r.n_out()); - for(i=1; i<=r.n_inp(); i++) m1.set_map_in (i, Set_Var,i); - for(i=1; i<=r.n_out(); i++) m1.set_map_out(i, Exists_Var,i); - // skip_set_checks--; - - int a = r.max_ufs_arity_of_out(); - if (a > 0) { - // UFS's must evacuate from the output tuple - Variable_ID_Tuple remapped; - - r.simplify(); - DNF *d = r.split()->DNFize(); - d->count_leading_0s(); - // Any conjucts with leading_0s == -1 must have >= "a" leading 0s - // What a gross way to do this. Ferd - - for (DNF_Iterator conj(d); conj; conj++) { -#if defined STUDY_EVACUATIONS - study_evacuation(*conj, out_to_in, a); -#endif - - int cL0 = (*conj)->guaranteed_leading_0s; - - for (Variable_ID_Iterator func((*conj)->mappedVars); func; func++) - if ((*func)->kind() == Global_Var) { - Global_Var_ID f = (*func)->get_global_var(); - if (f->arity() > 0 && (*func)->function_of()==Output_Tuple) { - if (cL0 >= f->arity()) { - (*func)->remap = r.get_local(f, Input_Tuple); - } - else { - (*func)->remap = (*conj)->declare(); - (*conj)->make_inexact(); - } - remapped.append(*func); - } - } - (*conj)->remap(); - reset_remap_field(remapped); - remapped.clear(); - - (*conj)->guaranteed_leading_0s = (*conj)->possible_leading_0s = -1; - (*conj)->leading_dir = 0; - } - } - - MapRel1(r, m1, Comb_Id); // this invalidates leading0s - assert(r.is_set() || m1.n_in() == 0); // MapRel can't tell to make a set - r.markAsSet(); // if there were no inputs. - - // skip_set_checks++; - assert(r.query_guaranteed_leading_0s() == -1 && r.query_possible_leading_0s() == -1); - // skip_set_checks--; - - return r; -} - - -Relation Range(NOT_CONST Relation &S) { - Relation r = consume_and_regurgitate(S); - if (r.is_null()) - return r; - - //assert(!r.is_null()); - // skip_set_checks++; - - int i; - Mapping m1(r.n_inp(), r.n_out()); - for(i=1; i<=r.n_inp(); i++) m1.set_map_in (i, Exists_Var,i); - for(i=1; i<=r.n_out(); i++) m1.set_map_out(i, Set_Var,i); - // skip_set_checks--; - - int a = r.max_ufs_arity_of_in(); - if (a > 0) { - // UFS's must evacuate from the input tuple - Variable_ID_Tuple remapped; - - r.simplify(); - DNF *d = r.split()->DNFize(); - d->count_leading_0s(); - // Any conjucts with leading_0s == -1 must have >= "a" leading 0s - // What a gross way to do this. Ferd - - for (DNF_Iterator conj(d); conj; conj++) { -#if defined STUDY_EVACUATIONS - study_evacuation(*conj, in_to_out, a); -#endif - - int cL0 = (*conj)->guaranteed_leading_0s; - for (Variable_ID_Iterator func((*conj)->mappedVars); func; func++) - if ((*func)->kind() == Global_Var) { - Global_Var_ID f = (*func)->get_global_var(); - if (f->arity() > 0 && (*func)->function_of()==Input_Tuple) { - if (cL0 >= f->arity()) { - (*func)->remap = r.get_local(f, Output_Tuple); - } - else { - (*func)->remap = (*conj)->declare(); - (*conj)->make_inexact(); - } - remapped.append(*func); - } - } - (*conj)->remap(); - reset_remap_field(remapped); - remapped.clear(); - - (*conj)->guaranteed_leading_0s = (*conj)->possible_leading_0s = -1; - (*conj)->leading_dir = 0; - } - } - - MapRel1(r, m1, Comb_Id); // this invalidates leading0s - assert(r.is_set() || m1.n_out() == 0); // MapRel can't tell to make a set - r.markAsSet(); // if there were no outputs. - - // skip_set_checks++; - assert(r.query_guaranteed_leading_0s() == -1 && r.query_possible_leading_0s() == -1); - // skip_set_checks--; - - return r; -} - - -// -// Cross Product. Give two sets, A and B, create a relation whose -// domain is A and whose range is B. -// -Relation Cross_Product(NOT_CONST Relation &input_A, - NOT_CONST Relation &input_B) { - Relation A = consume_and_regurgitate(input_A); - Relation B = consume_and_regurgitate(input_B); - if (A.is_null() || B.is_null()) - throw std::invalid_argument("null relation"); - if (!A.is_set() || !B.is_set()) - throw std::invalid_argument("cross product must be on two set"); - - // assert(A.is_set()); - // assert(B.is_set()); - - // skip_set_checks++; - assert(A.query_guaranteed_leading_0s() == -1 && - A.query_possible_leading_0s() == -1); - assert(B.query_guaranteed_leading_0s() == -1 && - B.query_possible_leading_0s() == -1); - // skip_set_checks--; - - Mapping mA(A.n_set()); - Mapping mB(B.n_set()); - int i; - for(i = 1; i <= B.n_set(); i++) mB.set_map_set(i, Output_Var,i); - for(i = 1; i <= A.n_set(); i++) mA.set_map_set(i, Input_Var,i); - return MapAndCombineRel2(A, B, mA, mB, Comb_And); -} - - -// -// inverse F -// reverse the input and output tuples -// -Relation Inverse(NOT_CONST Relation &S) { - Relation r = consume_and_regurgitate(S); - if (r.is_null()) - return r; - - // assert(!r.is_null()); - // assert(!r.is_set()); - int i; - - Mapping m1(r.n_inp(), r.n_out()); - for(i=1; i<=r.n_inp(); i++) m1.set_map_in (i, Output_Var,i); - for(i=1; i<=r.n_out(); i++) m1.set_map_out(i, Input_Var,i); - - MapRel1(r, m1, Comb_Id, -1, -1, false); - - r.reverse_leading_dir_info(); - - return r; -} - -Relation After(NOT_CONST Relation &input_S, - int carried_by, int new_output,int dir) { - Relation S = consume_and_regurgitate(input_S); - assert(!S.is_null()); - assert(!S.is_set()); - int i; - Relation r(*S.split(),42); - - int a = r.max_ufs_arity_of_out(); - int preserved_positions = min(carried_by-1,new_output); - if (a >= preserved_positions) { - // UFS's must evacuate from the output tuple - Variable_ID_Tuple remapped; - - r.simplify(); - DNF *d = r.split()->DNFize(); - d->count_leading_0s(); - // Any conjucts with leading_0s == -1 must have >= "a" leading 0s - // What a gross way to do this. Ferd - - for (DNF_Iterator conj(d); conj; conj++) { - int cL0 = (*conj)->guaranteed_leading_0s; - - for (Variable_ID_Iterator func((*conj)->mappedVars); func; func++) - if ((*func)->kind() == Global_Var) { - Global_Var_ID f = (*func)->get_global_var(); - if (f->arity() > preserved_positions - && (*func)->function_of()==Output_Tuple) { - if (cL0 >= f->arity()) { - (*func)->remap = r.get_local(f, Input_Tuple); - } - else { - (*func)->remap = (*conj)->declare(); - (*conj)->make_inexact(); - } - remapped.append(*func); - } - } - (*conj)->remap(); - reset_remap_field(remapped); - remapped.clear(); - - (*conj)->guaranteed_leading_0s = - (*conj)->possible_leading_0s = -1; - (*conj)->leading_dir = 0; - } - } - - Mapping m1(r.n_inp(), r.n_out()); - for(i=1; i<=r.n_inp(); i++) m1.set_map_in (i, Input_Var,i); - if (carried_by > new_output) { - int preserve = min(new_output,r.n_out()); - for(i=1; i<=preserve; i++) m1.set_map_out(i, Output_Var,i); - for(i=preserve+1; i<=r.n_out(); i++) m1.set_map_out(i, Exists_Var,-1); - MapRel1(r, m1, Comb_Id, -1, -1, true); - if (new_output > preserve) - r = Extend_Range(r,new_output-r.n_out()); - return r; - } - - for(i=1; i<carried_by; i++) m1.set_map_out(i, Output_Var,i); - m1.set_map_out(carried_by, Exists_Var,1); - for(i=carried_by+1; i<=r.n_out(); i++) m1.set_map_out(i, Exists_Var,-1); - - MapRel1(r, m1, Comb_Id, -1, -1, true,false); - - Rel_Body *body = r.split(); - body->Out_Names.append(Const_String()); - body->number_output++; - assert(body->n_out() <= input_vars.size()); - - - GEQ_Handle h = and_below_exists->add_GEQ(0); - assert(carried_by < 128); - h.update_coef(exists_ids[1],-dir); - h.update_coef(r.output_var(carried_by),dir); - h.update_const(-1); - h.finalize(); - r.finalize(); - if (new_output > r.n_out()) - r = Extend_Range(r,new_output-r.n_out()); - return r; -} - -// -// Identity. -// -Relation Identity(int n_inp) { - Relation rr(n_inp, n_inp); - F_And *f = rr.add_and(); - for(int i=1; i<=n_inp; i++) { - EQ_Handle e = f->add_EQ(); - e.update_coef(rr.input_var(i), -1); - e.update_coef(rr.output_var(i), 1); - e.finalize(); - } - rr.finalize(); - assert(!rr.is_null()); - return rr; -} - -Relation Identity(NOT_CONST Relation &input_r) { - Relation r = consume_and_regurgitate(input_r); - return Restrict_Domain(Identity(r.n_set()),r); -} - -// -// Deltas(F) -// Return a set such that the ith variable is old Out_i - In_i -// Delta variables are created as input variables. -// Then input and output variables are projected out. -// -Relation Deltas(NOT_CONST Relation &S) { - Relation R = consume_and_regurgitate(S); - assert(!R.is_null()); - // skip_set_checks++; - assert(R.n_inp()==R.n_out()); - int in = R.n_inp(); - // skip_set_checks--; - return Deltas(R,in); -} - -Relation Deltas(NOT_CONST Relation &S, int eq_no) { - Relation R = consume_and_regurgitate(S); - // skip_set_checks++; - assert(!R.is_null()); - assert(eq_no<=R.n_inp()); - assert(eq_no<=R.n_out()); - // R.split(); - - int no_inp = R.n_inp(); - int no_out = R.n_out(); - - if(relation_debug) { - fprintf(DebugFile,"Computing Deltas:\n"); - R.prefix_print(DebugFile); - } - int a = R.max_ufs_arity(); - if (a > 0) { - Variable_ID_Tuple remapped; - - // UFS's must evacuate from all tuples - we need to go to DNF - // to enumerate the variables, I think... - R.simplify(); - if(relation_debug) { - fprintf(DebugFile,"Relation simplified:\n"); - R.prefix_print(DebugFile); - } - DNF *d = R.split()->DNFize(); - - for (DNF_Iterator conj(d); conj; conj++) { - for (Variable_ID_Iterator func((*conj)->mappedVars); func; func++) - if ((*func)->kind() == Global_Var) { - Global_Var_ID f = (*func)->get_global_var(); - if (f->arity() > 0) { - (*func)->remap = (*conj)->declare(); - (*conj)->make_inexact(); - remapped.append(*func); - } - } - (*conj)->remap(); - reset_remap_field(remapped); - remapped.clear(); - } - } - - R = Extend_Domain(R, eq_no); // add eq_no Delta vars - Mapping M(no_inp+eq_no, no_out); - int i; - for(i=1; i<=eq_no; i++) { // Set up Deltas equalities - EQ_Handle E = R.and_with_EQ(); - /* delta_i - w_i + r_i = 0 */ - E.update_coef(R.input_var(i), 1); - E.update_coef(R.output_var(i), -1); - E.update_coef(R.input_var(no_inp+i), 1); - E.finalize(); - M.set_map(Input_Var, no_inp+i, Set_Var, i); // Result will be a set - } - for(i=1; i<=no_inp; i++) { // project out input variables - M.set_map(Input_Var, i, Exists_Var, i); - } - for(i=1; i<=no_out; i++) { // project out output variables - M.set_map(Output_Var, i, Exists_Var, no_inp+i); - } - MapRel1(R, M, Comb_Id, eq_no, 0); - - if(relation_debug) { - fprintf(DebugFile,"Computing deltas:\n"); - R.prefix_print(DebugFile); - }; - R.finalize(); - assert(R.is_set()); // Should be since we map things to Set_Var - assert(R.n_set() == eq_no); - // skip_set_checks--; - return R; -} - - - - -Relation DeltasToRelation(NOT_CONST Relation &D, int n_inputs, int n_outputs) { - Relation R = consume_and_regurgitate(D); - - // skip_set_checks++; - assert(!R.is_null()); - R.markAsRelation(); - int common = R.n_inp(); - assert(common <= n_inputs); - assert(common <= n_outputs); - R.split(); - - if (R.max_ufs_arity() > 0) { - assert(R.max_ufs_arity() == 0 && - "'Deltas' not ready for UFS yet"); // FERD - fprintf(stderr, "'Deltas' not ready for UFS yet"); - exit(1); - } - - R = Extend_Domain(R, n_inputs); - R = Extend_Range(R, n_outputs); - Mapping M(common+n_inputs, n_outputs); - int i; - for(i=1; i<=common; i++) { // Set up Deltas equalities - EQ_Handle E = R.and_with_EQ(); - /* delta_i - w_i + r_i = 0 */ - E.update_coef(R.input_var(i), 1); - E.update_coef(R.output_var(i), -1); - E.update_coef(R.input_var(common+i), 1); - E.finalize(); - M.set_map(Input_Var, i, Exists_Var, i); // Result will be a set - } - for(i=1; i<=n_inputs; i++) { // project out input variables - M.set_map(Input_Var, common+i, Input_Var, i); - } - for(i=1; i<=n_outputs; i++) { // project out output variables - M.set_map(Output_Var, i, Output_Var, i); - } - MapRel1(R, M, Comb_Id, n_inputs, n_outputs); - - if(relation_debug) { - fprintf(DebugFile,"Computed DeltasToRelation:\n"); - R.prefix_print(DebugFile); - } - R.finalize(); - assert(!R.is_set()); - // skip_set_checks--; - return R; -} - - - -Relation Join(NOT_CONST Relation &G, NOT_CONST Relation &F) { - return Composition(F, G); -} - -bool prepare_relations_for_composition(Relation &r1,Relation &r2) { - assert(!r2.is_null() && !r1.is_null()); - - if(r2.is_set()) { - int a1 = r1.max_ufs_arity_of_in(), a2 = r2.max_ufs_arity_of_set(); - - if (a1 == 0 && a2 == 0) - return true; - else { - assert(0 && "Can't compose relation and set with function symbols"); - fprintf(stderr, "Can't compose relation and set with function symbols"); - exit(1); - return false; // make compiler shut up - } - } - - assert(r2.n_out() == r1.n_inp()); - - int zeros = max(r1.query_guaranteed_leading_0s(), - r2.query_guaranteed_leading_0s()); - return (zeros >= r1.max_ufs_arity_of_in() - && zeros >= r2.max_ufs_arity_of_out()); -} - -// -// Composition(F, G) = F o G, where F o G (x) = F(G(x)) -// That is, if F = { [i] -> [j] : ... } -// and G = { [x] -> [y] : ... } -// then Composition(F, G) = { [x] -> [j] : ... } -// -// align the output tuple for G and the input tuple for F, -// these become existensially quantified variables -// use the output tuple from F and the input tuple from G for the result -// match named variables in G and F -// formula is g & f -// -// If there are function symbols of arity > 0, we call special case -// code to handle them. This is not set up for the r2.is_set case yet. -// - -Relation Composition(NOT_CONST Relation &input_r1, NOT_CONST Relation &input_r2) { - Relation r1 = consume_and_regurgitate(input_r1); - Relation r2 = consume_and_regurgitate(input_r2); - assert(!r2.is_null() && !r1.is_null()); - - if(r2.is_set()) { - int a1 = r1.max_ufs_arity_of_in(), a2 = r2.max_ufs_arity_of_set(); - if (r2.n_set() != r1.n_inp()) { - fprintf(stderr,"Illegal composition/application, arities don't match\n"); - fprintf(stderr,"Trying to compute r1(r2)\n"); - fprintf(stderr,"arity of r2 must match input arity of r1\n"); - fprintf(stderr,"r1: "); - r1.print_with_subs(stderr); - fprintf(stderr,"r2: "); - r2.print_with_subs(stderr); - fprintf(stderr,"\n"); - assert(r2.n_set() == r1.n_inp()); - exit(1); - } - // skip_set_checks++; - int i; - if (a1 == 0 && a2 == 0) { - int x = r1.n_out(); - Mapping m1(r1.n_inp(), r1.n_out()); - for(i=1; i<=r1.n_out(); i++) m1.set_map_out(i, Set_Var,i); - for(i=1; i<=r1.n_inp(); i++) m1.set_map_in (i, Exists_Var,i); - Mapping m2(r2.n_set()); - for(i=1; i<=r2.n_set(); i++) m2.set_map_set(i, Exists_Var,i); - Relation R3 = MapAndCombineRel2(r2, r1, m2, m1, Comb_And); - // skip_set_checks--; - if (x == 0) - R3.markAsSet(); - return R3; - } - else { - assert(0 && - "Can't compose relation and set with function symbols"); - fprintf(stderr, - "Can't compose relation and set with function symbols"); - exit(1); - return Identity(0); // make compiler shut up - } - } - - if (r2.n_out() != r1.n_inp()) { - fprintf(stderr,"Illegal composition, arities don't match\n"); - fprintf(stderr,"Trying to compute r1 compose r2\n"); - fprintf(stderr,"Output arity of r2 must match input arity of r1\n"); - fprintf(stderr,"r1: "); - r1.print_with_subs(stderr); - fprintf(stderr,"r2: "); - r2.print_with_subs(stderr); - fprintf(stderr,"\n"); - assert(r2.n_out() == r1.n_inp()); - exit(1); - } - - int a1 = r1.max_ufs_arity_of_in(), a2 = r2.max_ufs_arity_of_out(); - - if (a1 == 0 && a2 == 0 && 0 /* FERD - leading 0's go wrong here */ ) { - // If no real UFS's, we can just use the general code: - int i; - Mapping m1(r1.n_inp(), r1.n_out()); - for(i=1; i<=r1.n_inp(); i++) m1.set_map_in (i, Exists_Var,i); - for(i=1; i<=r1.n_out(); i++) m1.set_map_out(i, Output_Var,i); - Mapping m2(r2.n_inp(), r2.n_out()); - for(i=1; i<=r2.n_inp(); i++) m2.set_map_in (i, Input_Var,i); - for(i=1; i<=r2.n_out(); i++) m2.set_map_out(i, Exists_Var,i); - - return MapAndCombineRel2(r2, r1, m2, m1, Comb_And); - } - else { - Relation result(r2.n_inp(), r1.n_out()); - int mid_size = r2.n_out(); - int i; - for(i =1; i<=r2.n_inp(); i++) - result.name_input_var(i,r2.input_var(i)->base_name); - for(i =1; i<=r1.n_out(); i++) - result.name_output_var(i,r1.output_var(i)->base_name); - - r1.simplify(); - r2.simplify(); - - Rel_Body *b1 = r1.split(), *b2 = r2.split(); - - if (b1 == b2) { - assert(0 && "Compose: not ready to handle b1 == b2 yet."); - fprintf(stderr, "Compose: not ready to handle b1 == b2 yet.\n"); - exit(1); - } - - DNF *d1 = b1->DNFize(); - DNF *d2 = b2->DNFize(); - - d1->count_leading_0s(); - d2->count_leading_0s(); - // Any conjucts with leading_0s == -1 must have >= max_arity leading 0s - // What a gross way to do this. Ferd - - F_Exists *exists = result.add_exists(); - Section<Variable_ID> middle_tuple = exists->declare_tuple(mid_size); - Map<Global_Var_ID, Variable_ID> lost_functions((Variable_ID)0); - - F_Or *result_conjs = exists->add_or(); - - for (DNF_Iterator conj1(d1); conj1; conj1++) - for (DNF_Iterator conj2(d2); conj2; conj2++) { - // combine conj1 and conj2: - // conj2's in becomes result's in; conj1's out becomes out - // conj2's out and conj1's in get merged and exist. quant. - // conj2's f(in) and conj1's f(out) become f(in) and f(out) - // conj2's f(out) and conj1's f(in) get merged, evacuate: - // if conj1 has f.arity leading 0s, they become f(out), - // if conj2 has f.arity leading 0s, they become f(in) - // if neither has enough 0s, they become a wildcard - // and the result is inexact - // old wildcards stay wildcards - -#if defined STUDY_EVACUATIONS - study_evacuation(*conj1, *conj2, max(a1, a2)); -#endif - - Conjunct *copy1, *copy2; - copy2 = (*conj2)->copy_conj_same_relation(); - copy1 = (*conj1)->copy_conj_same_relation(); - - Variable_ID_Tuple remapped; - - int c1L0 = copy1->guaranteed_leading_0s; - int c2L0 = copy2->guaranteed_leading_0s; - - int inexact = 0; - - // get rid of conj2's f(out) - { - for (Variable_ID_Iterator func(copy2->mappedVars); func; func++) - if ((*func)->kind() == Global_Var) { - Global_Var_ID f = (*func)->get_global_var(); - if (f->arity() > 0 && (*func)->function_of()==Output_Tuple) { - if (c2L0 >= f->arity()) { - (*func)->remap = r2.get_local(f, Input_Tuple); - remapped.append(*func); - } - else if (c1L0 >= f->arity()) { - // f->remap = copy1->get_local(f, Output_Tuple); - // this should work with the current impl. - // SHOULD BE A NO-OP? - assert((*func)==r1.get_local(f,Output_Tuple)); - } - else { - Variable_ID f_quantified = lost_functions[f]; - if (!f_quantified) { - f_quantified = exists->declare(); - lost_functions[f] = f_quantified; - } - inexact = 1; - (*func)->remap = f_quantified; - remapped.append(*func); - } - } - } - } - - // remap copy2's out - for (i=1; i<=mid_size; i++) { - r2.output_var(i)->remap = middle_tuple[i]; - } - - // do remapping for conj2, then reset everything so - // we can go on with conj1 - - copy2->remap(); - reset_remap_field(remapped); - reset_remap_field(output_vars,mid_size); - - - remapped.clear(); - - // get rid of conj1's f(in) - { - for (Variable_ID_Iterator func(copy1->mappedVars); func; func++) - if ((*func)->kind() == Global_Var) { - Global_Var_ID f = (*func)->get_global_var(); - if (f->arity() > 0 && (*func)->function_of()==Input_Tuple) { - if (c1L0 >= f->arity()) { - (*func)->remap = r1.get_local(f,Output_Tuple); - remapped.append(*func); - } - else if (c2L0 >= f->arity()) { - // f->remap = copy2->get_local(f, Input_Tuple); - // this should work with the current impl. - // SHOULD BE A NO-OP? - assert((*func)==r2.get_local(f,Input_Tuple)); - } - else { - Variable_ID f_quantified = lost_functions[f]; - if (!f_quantified) { - f_quantified = exists->declare(); - lost_functions[f] = f_quantified; - } - inexact = 1; - (*func)->remap = f_quantified; - remapped.append(*func); - } - } - } - } - - // merge copy1's in with the already remapped copy2's out - for (i=1; i<=mid_size; i++) { - r1.input_var(i)->remap = middle_tuple[i]; - } - - copy1->remap(); - reset_remap_field(remapped); - reset_remap_field(input_vars,mid_size); - - Conjunct *conj3 = merge_conjs(copy1, copy2, MERGE_COMPOSE, exists->relation()); - result_conjs->add_child(conj3); - delete copy1; - delete copy2; - - // make sure all variables used in the conjunct - // are listed in the "result" relation - - for (Variable_ID_Iterator func(conj3->mappedVars); func; func++) - if ((*func)->kind() == Global_Var) { - Global_Var_ID f = (*func)->get_global_var(); - if (f->arity() > 0) - result.get_local(f, (*func)->function_of()); - else - result.get_local(f); - } - - if (inexact) - conj3->make_inexact(); - } - - // result.simplify(2, 4); // can't really do that now, will cause failure in chill - result.finalize(); - r1 = r2 = Relation(); - return result; - } -} - - - -bool Is_Obvious_Subset(NOT_CONST Relation &input_r1, NOT_CONST Relation &input_r2) { - Relation r1 = consume_and_regurgitate(input_r1); - Relation r2 = consume_and_regurgitate(input_r2); - - assert(!r1.is_null() && !r2.is_null()); - Rel_Body *rr1 = r1.split(); - Rel_Body *rr2 = r2.split(); - rr1->simplify(); - rr2->simplify(); - use_ugly_names++; - - remap_DNF_vars(rr2, rr1); - - for(DNF_Iterator pd1(rr1->query_DNF()); pd1.live(); pd1.next()) { - Conjunct *conj1 = pd1.curr(); - int found = false; - for(DNF_Iterator pd2(rr2->query_DNF()); pd2.live(); pd2.next()) { - Conjunct *conj2 = pd2.curr(); - if (!conj2->is_exact()) continue; - - Conjunct *cgist = merge_conjs(conj1, conj2, MERGE_GIST, conj2->relation()); -#ifndef NDEBUG - cgist->setup_names(); -#endif - if (cgist->redSimplifyProblem(2, 0) == noRed) { - delete cgist; - found = true; - break; - } - delete cgist; - } - if (! found) { - use_ugly_names--; - r1 = r2 = Relation(); - return false; - } - } - use_ugly_names--; - r1 = r2 = Relation(); - return true; -} /* Is_Obvious_Subset */ - - -bool do_subset_check(NOT_CONST Relation &input_r1, - NOT_CONST Relation &input_r2); - -// do_subset_check really implements Must_Be_Subset anyway (due to -// correct handling of inexactness in the negation code), but -// still take upper and lower bounds here -bool Must_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2) { - Relation s1 = Upper_Bound(consume_and_regurgitate(r1)); - Relation s2 = Lower_Bound(consume_and_regurgitate(r2)); - return do_subset_check(s1,s2); -} - -bool Might_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2) { - Relation s1 = Lower_Bound(consume_and_regurgitate(r1)); - Relation s2 = Upper_Bound(consume_and_regurgitate(r2)); - return do_subset_check(s1,s2); -} - -bool May_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2){ - return Might_Be_Subset(r1,r2); -} - - - - -// -// F Must_Be_Subset G -// Test that (f => g) === (~f | g) is a Tautology -// or that (f & ~g) is unsatisfiable: -// align the input tuples (if any) for F and G -// align the output tuples (if any) for F and G -// Special case: if r2 has a single conjunct then use HasRedQeuations. -// - -bool do_subset_check(NOT_CONST Relation &input_r1, - NOT_CONST Relation &input_r2) { - Relation r1 = consume_and_regurgitate(input_r1); - Relation r2 = consume_and_regurgitate(input_r2); - if (r1.is_null() || r2.is_null()) - throw std::invalid_argument("null relation"); - if (r1.n_inp() != r2.n_inp() || r1.n_out() != r2.n_out()) - throw std::invalid_argument("relation arity does not match"); - - // assert(!r1.is_null() && !r2.is_null()); - // skip_set_checks++; - // assert(r1.n_inp() == r2.n_inp()); - // assert(r1.n_out() == r2.n_out()); - // skip_set_checks--; - r1.simplify(1,0); - r2.simplify(2,2); - Rel_Body *rr1 = r1.split(); - - if(relation_debug) { - fprintf(DebugFile, "\n$$$ Must_Be_Subset IN $$$\n"); - } - - bool c = true; - - // Check each conjunct separately - for(DNF_Iterator pd(rr1->query_DNF()); c && pd.live(); ) { - Relation tmp(r1,pd.curr()); - pd.next(); -#ifndef CHECK_MAYBE_SUBSET - if (pd.live()) - c = !Difference(tmp,copy(r2)).is_upper_bound_satisfiable(); - else - c = !Difference(tmp,r2).is_upper_bound_satisfiable(); -#else - Relation d=Difference(copy(tmp), copy(r2)); - c=!d.is_upper_bound_satisfiable(); - if (!c && !d.is_exact()) { // negation-induced inexactness - static int OMEGA_WHINGE = -1; - if (OMEGA_WHINGE < 0) { - OMEGA_WHINGE = getenv("OMEGA_WHINGE") ? atoi(getenv("OMEGA_WHINGE")) : 0; - } - if (OMEGA_WHINGE) { - fprintf(DebugFile,"\n===== r1 is maybe a Must_Be_Subset of r2 ========\n"); - fprintf(DebugFile,"-------> r1:\n"); - tmp.print_with_subs(DebugFile); - fprintf(DebugFile,"-------> r2:\n"); - r2.print_with_subs(DebugFile); - fprintf(DebugFile,"-------> r1-r2:\n"); - d.print_with_subs(DebugFile); - } - } -#endif - } - - if(relation_debug) { - fprintf(DebugFile, "$$$ Must_Be_Subset OUT $$$\n"); - } - r1 = r2 = Relation(); - return c; -} - - -// -// F minus G -// -Relation Difference(NOT_CONST Relation &input_r1, - NOT_CONST Relation &input_r2) { - Relation r1 = consume_and_regurgitate(input_r1); - Relation r2 = consume_and_regurgitate(input_r2); - if (r1.is_null() || r2.is_null()) - return r1; - if (r1.n_inp() != r2.n_inp() || r1.n_out() != r2.n_out()) - throw std::invalid_argument("relation arity does not match"); - - //assert(!r1.is_null() && !r2.is_null()); - // skip_set_checks++; - // assert(r1.n_inp() == r2.n_inp()); - // assert(r1.n_out() == r2.n_out()); - - int i; - Mapping m1(r1.n_inp(), r1.n_out()); - for(i=1; i<=r1.n_inp(); i++) m1.set_map_in (i, Input_Var,i); - for(i=1; i<=r1.n_out(); i++) m1.set_map_out(i, Output_Var,i); - Mapping m2(r2.n_inp(), r2.n_out()); - for(i=1; i<=r2.n_inp(); i++) m2.set_map_in (i, Input_Var,i); - for(i=1; i<=r2.n_out(); i++) m2.set_map_out(i, Output_Var,i); - // skip_set_checks--; - - return MapAndCombineRel2(r1, r2, m1, m2, Comb_AndNot); -} - -// -// complement F -// not F -// -Relation Complement(NOT_CONST Relation &S) { - Relation r = consume_and_regurgitate(S); - if (r.is_null()) - return r; - - // assert(!r.is_null()); - // skip_set_checks++; - int i; - Mapping m(r.n_inp(), r.n_out()); - for(i=1; i<=r.n_inp(); i++) m.set_map_in (i, Input_Var,i); - for(i=1; i<=r.n_out(); i++) m.set_map_out(i, Output_Var,i); - // skip_set_checks--; - - MapRel1(r, m, Comb_AndNot, -1, -1, false); - return r; -} - - -// -// Compute (gist r1 given r2). -// Currently we assume that r2 has only one conjunct. -// r2 may have zero input and output OR may have # in/out vars equal to r1. -// -Relation GistSingleConjunct(NOT_CONST Relation &input_R1, - NOT_CONST Relation &input_R2, int effort) { - Relation R1 = consume_and_regurgitate(input_R1); - Relation R2 = consume_and_regurgitate(input_R2); - - // skip_set_checks++; - assert(!R1.is_null() && !R2.is_null()); - assert((R1.n_inp() == R2.n_inp() && R1.n_out() == R2.n_out()) || - (R2.n_inp() == 0 && R2.n_out() == 0)); - R1.simplify(); - R2.simplify(); - Rel_Body *r1 = R1.split(); - Rel_Body *r2 = R2.split(); - - if(relation_debug) { - fprintf(DebugFile, "\n### GIST computation start ### [\n"); - R1.prefix_print(DebugFile); - R2.prefix_print(DebugFile); - fprintf(DebugFile, "### ###\n"); - } - - -// The merged conjunct has to have the variables of either r1 or r2, but -// not both. Use r1's, since it'll be cheaper to remap r2's single conj. - remap_DNF_vars(r2, r1); - assert(r2->is_upper_bound_satisfiable() && "Gist: second operand is FALSE"); - // skip_set_checks--; - - Conjunct *known = r2->single_conjunct(); - assert(known != NULL && "Gist: second operand has more than 1 conjunct"); - - DNF *new_dnf = new DNF(); - for(DNF_Iterator pd(r1->simplified_DNF); pd.live(); pd.next()) { - Conjunct *conj = pd.curr(); - Conjunct *cgist = merge_conjs(known, conj, MERGE_GIST, conj->relation()); // Uses r1's vars - cgist->set_relation(r1); // Thinks it's part of r1 now, for var. purposes - if(simplify_conj(cgist, true, effort+1, EQ_RED)) { - /* Throw out black constraints, turn red constraints into black */ - cgist->rm_color_constrs(); - if(cgist->is_true()) { - delete new_dnf; - delete cgist; - // skip_set_checks++; - Relation retval = Relation::True(r1->n_inp(), r2->n_out()); - // retval.finalize(); - retval.simplify(); - if(R1.is_set() && R2.is_set()) retval.markAsSet(); - // skip_set_checks--; - return retval; - } - else { - // since modular equations might be changed, simplify again! - simplify_conj(cgist, true, effort+1, EQ_BLACK); - - new_dnf->add_conjunct(cgist); - } - } - } - delete r1->simplified_DNF; - r1->simplified_DNF = new_dnf; - assert(!r1->is_null()); - R1.finalize(); - if(relation_debug) { - fprintf(DebugFile, "] ### GIST computation end ###\n"); - R1.prefix_print(DebugFile); - fprintf(DebugFile, "### ###\n"); - } - return(R1); -} - - -// -// Compute gist r1 given r2. r2 can have multiple conjuncts, -// return result is always simplified. -// -Relation Gist(NOT_CONST Relation &input_R1, - NOT_CONST Relation &input_R2, int effort) { - Relation R1 = consume_and_regurgitate(input_R1); - Relation R2 = consume_and_regurgitate(input_R2); - if (R1.is_null()) - return R1; - // change the Gist semantics to allow r2 be null -- by chun 07/30/2007 - if (R2.is_null()) { - R1.simplify(); - return R1; - } - if (!(R1.n_inp() == 0 && R2.n_out() == 0) && - (R1.n_inp() != R2.n_inp() || R1.n_out() != R2.n_out())) - throw std::invalid_argument("relation arity does not match"); - - // skip_set_checks++; - // assert(!R1.is_null()); - // assert(R2.is_null() || - // (R1.n_inp() == R2.n_inp() && R1.n_out() == R2.n_out()) || - // (R2.n_inp() == 0 && R2.n_out() == 0)); - // skip_set_checks--; - R2.simplify(); - - if(relation_debug) { - fprintf(DebugFile, "\n### multi-GIST computation start ### [\n"); - R1.prefix_print(DebugFile); - R2.prefix_print(DebugFile); - fprintf(DebugFile, "### ###\n"); - } - - if (!R2.is_upper_bound_satisfiable()) - return Relation::True(R1); - if (R2.is_obvious_tautology()) { - R1.simplify(); - return R1; - } - R1.simplify(); - - if (!Intersection(copy(R1), copy(R2)).is_upper_bound_satisfiable()) - return Relation::False(R1); - - int nconj1=0; - for (DNF_Iterator di(R1.simplified_DNF()); di.live(); di.next()) - nconj1++; - int nconj2=0; - for (DNF_Iterator di2(R2.simplified_DNF()); di2.live(); di2.next()) - nconj2++; - - { - static int OMEGA_WHINGE = -1; - if (OMEGA_WHINGE < 0) { - OMEGA_WHINGE = getenv("OMEGA_WHINGE") ? atoi(getenv("OMEGA_WHINGE")) : 0; - } - if (OMEGA_WHINGE && (nconj1 + nconj2 > 50)) { - fprintf(DebugFile,"WOW!!!! - Gist (%d conjuncts, %d conjuncts)!!!\n", - nconj1,nconj2); - fprintf(DebugFile,"Base:\n"); - R1.prefix_print(DebugFile); - fprintf(DebugFile,"Context:\n"); - R2.prefix_print(DebugFile); - } - } - - if (nconj2==1) - return GistSingleConjunct(R1,R2, effort); - else { - R1.simplify(0,1); - R2.simplify(0,1); - Relation G = Relation::True(R1); - for (DNF_Iterator di2(R2.simplified_DNF()); di2.live(); di2.next()) { - Conjunct * c2 = di2.curr(); - Relation G2 = Relation::False(R1); - for (DNF_Iterator di1(R1.simplified_DNF()); di1.live(); di1.next()) { - Conjunct * c1 = di1.curr(); - Relation G1=GistSingleConjunct(Relation(R1,c1), Relation(R2,c2),effort); - - if (G1.is_obvious_tautology()) { - G2 = G1; - break; - } - else if (!G1.is_upper_bound_satisfiable() || !G1.is_exact()) { - if(relation_debug) { - fprintf(DebugFile, "gist A given B is unsatisfiable\n"); - fprintf(DebugFile, "A:\n"); - Relation(R1,c1).prefix_print(DebugFile); - fprintf(DebugFile, "B:\n"); - Relation(R2,c2).prefix_print(DebugFile); - fprintf(DebugFile, "\n"); - } - //G1 = Relation(R1,c1); - return R1; - } - else if(0 && G1.is_exact() && !Must_Be_Subset(Relation(R1,c1),copy(G1))) { - fprintf(DebugFile,"Unexpected non-Must_Be_Subset gist result!\n"); - fprintf(DebugFile,"base: \n"); - Relation(R1,c1).prefix_print(DebugFile); - fprintf(DebugFile,"context: \n"); - Relation(R2,c2).prefix_print(DebugFile); - fprintf(DebugFile,"result: \n"); - G1.prefix_print(DebugFile); - fprintf(DebugFile,"base not subseteq result: \n"); - assert(!G1.is_exact() || Must_Be_Subset(Relation(R1,c1),copy(G1))); - } - G2=Union(G2,G1); - } - G2.simplify(0,1); - G = Intersection(G,G2); - G.simplify(0,1); - if(relation_debug) { - fprintf(DebugFile, "result so far is:\n"); - G.prefix_print(DebugFile); - } - } - - if(relation_debug) { - fprintf(DebugFile, "\n### end multi-GIST computation ### ]\n"); - fprintf(DebugFile, "G is:\n"); - G.prefix_print(DebugFile); - fprintf(DebugFile, "### ###\n"); - } -#if ! defined NDEBUG - Relation S1 = Intersection(copy(R1), copy(R2)); - Relation S2 = Intersection(copy(G), copy(R2)); - - - if(relation_debug) { - fprintf(DebugFile, "\n---->[Checking validity of the GIST result\n"); - fprintf(DebugFile, "for G=gist R1 given R2:\n"); - fprintf(DebugFile, "R1 intersect R2 is:\n"); - S1.print_with_subs(DebugFile); - fprintf(DebugFile, "\nG intersect R2 is:\n"); - S2.print_with_subs(DebugFile); - fprintf(DebugFile, "---->]\n"); - } - assert (!S1.is_exact() || !S2.is_exact() || (Must_Be_Subset(copy(S1),copy(S2)) && Must_Be_Subset(copy(S2),copy(S1)))); -#endif - return G; - } -} - - -// Project away all input and output variables. -Relation Project_On_Sym(NOT_CONST Relation &S, - NOT_CONST Relation &input_context) { - Relation R = consume_and_regurgitate(S); - Relation context = consume_and_regurgitate(input_context); - int i; - - // skip_set_checks++; - leave_pufs_untouched++; - int in_arity = R.max_ufs_arity_of_in(); - int out_arity = R.max_ufs_arity_of_out(); - assert(!R.is_null()); - R.split(); - - int no_inp = R.n_inp(); - int no_out = R.n_out(); - Mapping M(no_inp, no_out); - - for(i=1; i<=no_inp; i++) { // project out input variables - M.set_map(Input_Var, i, Exists_Var, i); - } - for(i=1; i<=no_out; i++) { // project out output variables - M.set_map(Output_Var, i, Exists_Var, no_inp+i); - } - MapRel1(R, M, Comb_Id, 0, 0); - - R.finalize(); - if (in_arity) R = Extend_Domain(R,in_arity); - if (out_arity) R = Extend_Range(R,out_arity); - - int d = min(in_arity,out_arity); - if (d && !context.is_null()) { - int g = min(d,context.query_guaranteed_leading_0s()); - int p = min(d,context.query_possible_leading_0s()); - int dir = context.query_leading_dir(); - R.enforce_leading_info(g,p,dir); - } - - leave_pufs_untouched--; - // skip_set_checks--; - if(relation_debug) { - fprintf(DebugFile,"\nProjecting onto symbolic (%d,%d):\n",in_arity,out_arity); - R.prefix_print(DebugFile); - } - return R; -} - - -// -// Project out global variable g from relation r -// -Relation Project(NOT_CONST Relation &S, Global_Var_ID g) { - Relation R = consume_and_regurgitate(S); - assert(!R.is_null()); - - skip_finalization_check++; - - Rel_Body *r = R.split(); - r->DNF_to_formula(); - Formula *f = r->rm_formula(); - F_Exists *ex = r->add_exists(); - ex->add_child(f); - - if (g->arity() == 0) { - assert(R.has_local(g) && "Project: Relation doesn't contain variable to be projected"); - Variable_ID v = R.get_local(g); - - bool rmd = rm_variable(r->Symbolic,v); - assert(rmd && "Project: Variable to be projected doesn't exist"); - - v->remap = ex->declare(v->base_name); - f->remap(); - v->remap = v; - } - else { - assert((R.has_local(g, Input_Tuple) || R.has_local(g, Output_Tuple)) && "Project: Relation doesn't contain variable to be projected"); - - if (R.has_local(g, Input_Tuple)) { - Variable_ID v = R.get_local(g, Input_Tuple); - - bool rmd = rm_variable(r->Symbolic,v); - assert(rmd && "Project: Variable to be projected doesn't exist"); - - v->remap = ex->declare(v->base_name); - f->remap(); - v->remap = v; - } - if (R.has_local(g, Output_Tuple)) { - Variable_ID v = R.get_local(g, Output_Tuple); - - bool rmd = rm_variable(r->Symbolic,v); - assert(rmd && "Project: Variable to be projected doesn't exist"); - - v->remap = ex->declare(v->base_name); - f->remap(); - v->remap = v; - } - } - - skip_finalization_check--; - - R.finalize(); - return R; -} - - -// -// Project all symbolic variables from relation r -// -Relation Project_Sym(NOT_CONST Relation &S) { - Relation R = consume_and_regurgitate(S); - assert(!R.is_null()); - - Rel_Body *r = R.split(); - r->DNF_to_formula(); - - Formula *f = r->rm_formula(); - - skip_finalization_check++; - F_Exists *ex = r->add_exists(); - for(Variable_ID_Iterator R_Sym(r->Symbolic); R_Sym; R_Sym++) { - Variable_ID v = *R_Sym; - v->remap = ex->declare(v->base_name); - } - ex->add_child(f); - skip_finalization_check--; - - f->remap(); - - reset_remap_field(r->Symbolic); - r->Symbolic.clear(); - - R.finalize(); - return R; -} - -// -// Project specified variables, leaving those variables with no constraints. -// -Relation Project(NOT_CONST Relation &S, Sequence<Variable_ID> &s) { - // This is difficult to do with mappings. This cheats, since it is - // much easier and more straightforward. - - Relation R = consume_and_regurgitate(S); - assert(!R.is_null()); - - Rel_Body *r = R.split(); - r->DNF_to_formula(); - Formula *f = r->rm_formula(); - bool need_symbolic_clear = false; - - skip_finalization_check++; - F_Exists *ex = r->add_exists(); - for(int i = 1; i <= s.size(); i++) { - if (s[i]->kind() == Global_Var) - need_symbolic_clear = true; - s[i]->remap = ex->declare(s[i]->base_name); - } - ex->add_child(f); - skip_finalization_check--; - - f->remap(); - - reset_remap_field(s); - if (need_symbolic_clear) - r->Symbolic.clear(); - - R.finalize(); - return R; -} - -Relation Project(NOT_CONST Relation &S, int pos, Var_Kind vkind) { - Variable_ID v = 0; // shut the compiler up - switch (vkind) { - case Input_Var: - v = input_vars[pos]; - break; - case Output_Var: - v = output_vars[pos]; - break; - // case Set_Var: - // v = set_vars[pos]; - // break; - default: - assert(0); - } - - return Project(S, v); -} - -Relation Project(NOT_CONST Relation &S, Variable_ID v) { - Tuple<Variable_ID> s; - s.append(v); - return Project(S, s); -} - -// -// Variables in DNF of map_rel reference declarations of map_rel (or not). -// remap_DNF_vars makes them to reference declarations of ref_rel. -// Ref_rel can get new global variable declarations in the process. -// -void remap_DNF_vars(Rel_Body *map_rel, Rel_Body *ref_rel) { - // skip_set_checks++; - assert (map_rel->simplified_DNF); - assert (ref_rel->simplified_DNF); - - // skip_set_checks++; - - for(DNF_Iterator pd(map_rel->simplified_DNF); pd.live(); pd.next()) { - Conjunct *cc = pd.curr(); - Variable_ID_Tuple &mvars = cc->mappedVars; - for(Variable_Iterator mvarsIter=mvars; mvarsIter; mvarsIter++) { - Variable_ID v = *mvarsIter; - switch(v->kind()) { - case Input_Var: - assert(ref_rel->n_inp() >= v->get_position()); - break; - case Output_Var: - assert(ref_rel->n_out() >= v->get_position()); - break; - case Global_Var: - // The assignment is a noop, but tells ref_rel that the global may be - // used inside it, which is required. - *mvarsIter = ref_rel->get_local(v->get_global_var(),v->function_of()); - break; - case Wildcard_Var: - break; - default: - assert(0 && "bad variable kind"); - } - } - } - // skip_set_checks--; -} - - -Relation projectOntoJust(Relation R, Variable_ID v) { - // skip_set_checks++; - - int ivars = R.n_inp(), ovars = R.n_out(); - int ex_ivars= 0, ex_ovars = 0; - - assert(v->kind() == Input_Var || v->kind() == Output_Var); - if (v->kind() == Input_Var) { - ex_ivars = 1; - R = Extend_Domain(R,1); - } - else { - ex_ovars = 1; - R = Extend_Range(R,1); - } - - // Project everything except v - Mapping m(ivars+ex_ivars,ovars+ex_ovars); - int j; - for(j = 1; j <=ivars+ex_ivars; j++) m.set_map_in(j, Exists_Var, j); - for(j = 1; j <=ovars+ex_ovars; j++) m.set_map_out(j, Exists_Var, j+ivars+ex_ivars); - m.set_map(v->kind(), v->get_position(), v->kind(), v->get_position()); - - MapRel1(R, m, Comb_Id,-1,-1); - R.finalize(); - // skip_set_checks--; - return R; -} - -//static -//void copyEQtoGEQ(GEQ_Handle &g, const EQ_Handle &e, bool negate) { -//extern void copy_constraint(Constraint_Handle H, Constraint_Handle initial); -// copy_constraint(g, e); -//} - - -Relation EQs_to_GEQs(NOT_CONST Relation &S, bool excludeStrides) { - Relation R = consume_and_regurgitate(S); - assert(R.is_simplified()); - use_ugly_names++; - for (DNF_Iterator s(R.query_DNF()); s.live(); s.next()) - s.curr()->convertEQstoGEQs(excludeStrides); - use_ugly_names--; - return R; -} - - -// Tuple to find values for is input+output -Relation Symbolic_Solution(NOT_CONST Relation &R) { - Relation S = consume_and_regurgitate(R); - Tuple<Variable_ID> vee; - // skip_set_checks++; - int i; - for(i = 1; i <= S.n_inp(); i++) vee.append(input_var(i)); - for(i = 1; i <= S.n_out(); i++) vee.append(output_var(i)); - // skip_set_checks--; - - return Solution(S, vee); -} - - -// Tuple to find values for is given as arg, plus input and output -Relation Symbolic_Solution(NOT_CONST Relation &R, Sequence<Variable_ID> &for_these){ - Relation S = consume_and_regurgitate(R); - Tuple<Variable_ID> vee; - // skip_set_checks++; - int i; - for(Any_Iterator<Variable_ID> it(for_these); it; it++) - vee.append(*it); - for(i = 1; i <= S.n_inp(); i++) vee.append(input_var(i)); - for(i = 1; i <= S.n_out(); i++) vee.append(output_var(i)); - // skip_set_checks--; - - return Solution(S, vee); -} - - -// Tuple to find values for is input+output+global_decls -Relation Sample_Solution(NOT_CONST Relation &R) { - Relation S = consume_and_regurgitate(R); - - Tuple<Variable_ID> vee; - - // skip_set_checks++; - int i; - for(i = 1; i <= S.global_decls()->size(); i++) - vee.append((*S.global_decls())[i]); - for(i = 1; i <= S.n_inp(); i++) vee.append(input_var(i)); - for(i = 1; i <= S.n_out(); i++) vee.append(output_var(i)); - // skip_set_checks--; - - return Solution(S,vee); -} - - -// Tuple to find values is given as arg -Relation Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &for_these ) { - Relation R = consume_and_regurgitate(S); - if (R.is_null()) - return R; - - //assert(!R.is_null()); - - if(!R.is_upper_bound_satisfiable()) { - return Relation::False(R); - } - - bool inexactAnswer=false; - if(R.is_inexact()) { - if(R.is_lower_bound_satisfiable()) - R = Lower_Bound(R); // a solution to LB is a solution to the relation - else { - // A solution to the UB may not be a solution to the relation: - // There may be a solution which satisfies all known constraints, but - // we have no way of knowing if it satisifies the unknown constraints. - inexactAnswer = true; - R = Upper_Bound(R); - } - } - - Sequence<Variable_ID> &vee = for_these; - for (DNF_Iterator di(R.query_DNF()); di; di++) { - Relation current(R, *di); - int i; - for(i = vee.size()-1; i >= 0; i--) { - bool some_constraints = false, one_stride = false; - - int current_var = vee.size()-i; - Section<Variable_ID> s(&vee,current_var+1,i); - - // Query variable in vee[current_var] - Relation projected = Project(copy(current), s); - - retry_solution: - assert(projected.has_single_conjunct()); - DNF_Iterator one = projected.query_DNF(); - - // Look for candidate EQ's - EQ_Handle stride; - EQ_Iterator ei(*one); - for(; ei; ei++) { - if((*ei).get_coef(vee[current_var]) != 0) { - if(!Constr_Vars_Iter(*ei,true).live()) { // no wildcards - some_constraints = true; - // Add this constraint to the current as an EQ - current.and_with_EQ(*ei); - break; - } - else { - one_stride = !one_stride && !some_constraints; - stride = *ei; - } - } - } - if(ei) - continue; // Found an EQ, skip to next variable - else if (one_stride && !some_constraints) { - // if unconstrained except for a stride, pick stride as value - Constr_Vars_Iter cvi(stride,true); - assert(cvi.live()); - cvi++; - if(!cvi) { // Just one existentially quantified variable - Relation current_copy = current; - EQ_Handle eh = current_copy.and_with_EQ(); - for(Constr_Vars_Iter si = stride; si; si++) - if((*si).var->kind() != Wildcard_Var){ - // pick "0" for wildcard, don't set its coef - eh.update_coef((*si).var, (*si).coef); - } - eh.update_const(stride.get_const()); - if(current_copy.is_upper_bound_satisfiable()){ - current = current_copy; - continue; // skip to next var - } - } - some_constraints = true; // count the stride as a constraint - } - - // Can we convert a GEQ? - GEQ_Iterator gi(*one); - for(; gi; gi++) { - if((*gi).get_coef(vee[current_var]) != 0) { - some_constraints = true; - if(!Constr_Vars_Iter(*gi,true).live()) { // no wildcards - Relation current_copy = current; - // Add this constraint to the current as an EQ & test - current_copy.and_with_EQ(*gi); - if (current_copy.is_upper_bound_satisfiable()) { - current = current_copy; - break; - } - } - } - } - if (gi) continue; // Turned a GEQ into EQ, skip to next - - // Remove wildcards, try try again - Relation approx = Approximate(copy(projected)); - assert(approx.has_single_conjunct()); - DNF_Iterator d2 = approx.query_DNF(); - - EQ_Iterator ei2(*d2); - for(; ei2; ei2++) { - if((*ei2).get_coef(vee[current_var]) != 0) { - some_constraints = true; - assert(!Constr_Vars_Iter(*ei2,true).live()); // no wildcards - Relation current_copy = current; - // Add this constraint to the current as an EQ & test - current_copy.and_with_EQ(*ei2); - if (current_copy.is_upper_bound_satisfiable()) { - current = current_copy; - break; - } - } - } - if(ei2) continue; // Found an EQ, skip to next variable - - GEQ_Iterator gi2(*d2); - for(; gi2; gi2++) { - if((*gi2).get_coef(vee[current_var]) != 0) { - some_constraints = true; - assert(!Constr_Vars_Iter(*gi2,true).live()); // no wildcards - Relation current_copy = current; - // Add this constraint to the current as an EQ & test - current_copy.and_with_EQ(*gi2); - if (current_copy.is_upper_bound_satisfiable()) { - current = current_copy; - break; - } - } - } - if(gi2) continue; - - if(!some_constraints) { // No constraints on this variable were found - EQ_Handle e = current.and_with_EQ(); - e.update_const(-42); // Be creative - e.update_coef(vee[current_var], 1); - continue; - } - else { // What to do? Find a wildcard to discard - Variable_ID wild = NULL; - - for (GEQ_Iterator gi(*one); gi; gi++) - if ((*gi).get_coef(vee[current_var]) != 0 && (*gi).has_wildcards()) { - Constr_Vars_Iter cvi(*gi, true); - wild = (*cvi).var; - break; - } - if (wild == NULL) - for (EQ_Iterator ei(*one); ei; ei++) - if ((*ei).get_coef(vee[current_var]) != 0 && (*ei).has_wildcards()) { - Constr_Vars_Iter cvi(*ei, true); - wild = (*cvi).var; - break; - } - - if (wild != NULL) { - // skip_set_checks++; - - Relation R2; - { - Tuple<Relation> r(1); - r[1] = projected; - Tuple<std::map<Variable_ID, std::pair<Var_Kind, int> > > mapping(1); - mapping[1][wild] = std::make_pair(vee[current_var]->kind(), vee[current_var]->get_position()); - mapping[1][vee[current_var]] = std::make_pair(Exists_Var, 1); - Tuple<bool> inverse(1); - inverse[1] = false; - R2 = merge_rels(r, mapping, inverse, Comb_And); - } - - Variable_ID R2_v; - switch (vee[current_var]->kind()) { - // case Set_Var: - case Input_Var: { - int pos = vee[current_var]->get_position(); - R2_v = R2.input_var(pos); - break; - } - case Output_Var: { - int pos = vee[current_var]->get_position(); - R2_v = R2.output_var(pos); - break; - } - case Global_Var: { - Global_Var_ID g = vee[current_var]->get_global_var(); - if (g->arity() == 0) - R2_v = R2.get_local(g); - else - R2_v = R2.get_local(g, vee[current_var]->function_of()); - } - default: - assert(0); - } - - Relation S2; - { - Tuple<Variable_ID> vee; - vee.append(R2_v); - S2 = Solution(R2, vee); - } - - Variable_ID S2_v; - switch (vee[current_var]->kind()) { - // case Set_Var: - case Input_Var: { - int pos = vee[current_var]->get_position(); - S2_v = S2.input_var(pos); - break; - } - case Output_Var: { - int pos = vee[current_var]->get_position(); - S2_v = S2.output_var(pos); - break; - } - case Global_Var: { - Global_Var_ID g = vee[current_var]->get_global_var(); - if (g->arity() == 0) - S2_v = S2.get_local(g); - else - S2_v = S2.get_local(g, vee[current_var]->function_of()); - } - default: - assert(0); - } - - Relation R3; - { - Tuple<Relation> r(2); - r[1] = projected; - r[2] = S2; - Tuple<std::map<Variable_ID, std::pair<Var_Kind, int> > > mapping(2); - mapping[1][wild] = std::make_pair(Exists_Var, 1); - mapping[2][S2_v] = std::make_pair(Exists_Var, 1); - Tuple<bool> inverse(2); - inverse[1] = inverse[2] = false; - R3 = merge_rels(r, mapping, inverse, Comb_And); - } - - // skip_set_checks--; - - if (R3.is_upper_bound_satisfiable()) { - projected = R3; - goto retry_solution; - } - } - } - - // If we get here, we failed to find a suitable constraint for - // this variable at this conjunct, look for another conjunct. - break; - } - - if (i < 0) { // solution found - if(inexactAnswer) - current.and_with_and()->add_unknown(); - current.finalize(); - return current; - } - } - - // No solution found for any conjunct, we bail out. - fprintf(stderr,"Couldn't find suitable constraint for variable\n"); - return Relation::Unknown(R); -} - - -Relation Approximate(NOT_CONST Relation &input_R, bool strides_allowed) { - Relation R = consume_and_regurgitate(input_R); - if (R.is_null()) - return R; - - // assert(!R.is_null()); - Rel_Body *r = R.split(); - - // approximate can be used to remove lambda variables from farkas, - // so be careful not to invoke simplification process for integers. - r->simplify(-1,-1); - - if (pres_debug) { - fprintf(DebugFile,"Computing approximation "); - if (strides_allowed) fprintf(DebugFile,"with strides allowed "); - fprintf(DebugFile,"[ \n"); - r->prefix_print(DebugFile); - } - - use_ugly_names++; - for (DNF_Iterator pd(r->simplified_DNF); pd.live(); ) { - Conjunct *C = pd.curr(); - pd.next(); - - for(int i = 0; i < C->problem->nGEQs; i++) - C->problem->GEQs[i].touched = 1; - - C->reorder(); - if(C->problem->simplifyApproximate(strides_allowed)==0) { - r->simplified_DNF->rm_conjunct(C); - delete C; - } - else { - C->simplifyProblem(1,0,1); - - free_var_decls(C->myLocals); C->myLocals.clear(); - - Problem *p = C->problem; - Variable_ID_Tuple new_mapped(0); // This is expanded by "append" - for (int i = 1; i <= p->safeVars; i++) { - // what is now in column i used to be in column p->var[i] - Variable_ID v = C->mappedVars[p->var[i]]; - assert (v->kind() != Wildcard_Var); - new_mapped.append(v); - } - assert(strides_allowed || C->problem->nVars == C->problem->safeVars); - C->mappedVars = new_mapped; - for (int i = p->safeVars+1; i <= p->nVars; i++) { - Variable_ID v = C->declare(); - C->mappedVars.append(v); - } - - - // reset var and forwarding address if desired. - p->variablesInitialized = 0; - for(int i = 1; i < C->problem->nVars; i++) - C->problem->var[i] = C->problem->forwardingAddress[i] = i; - } - } - - if (pres_debug) - fprintf(DebugFile,"] done Computing approximation\n"); - use_ugly_names--; - return R; -} - - -Relation Lower_Bound(NOT_CONST Relation &r) { - Relation s = consume_and_regurgitate(r); - s.interpret_unknown_as_false(); - return s; -} - - -Relation Upper_Bound(NOT_CONST Relation &r) { - Relation s = consume_and_regurgitate(r); - s.interpret_unknown_as_true(); - return s; -} - - -bool operator==(const Relation &, const Relation &) { - assert(0 && "You rilly, rilly don't want to do this.\n"); - abort(); - return false; -} - - -namespace { // supporting stuff for MapRel1 and MapAndCombine2 - // Determine if a mapping requires an f_exists node - bool has_existentials(const Mapping &m) { - for(int i=1;i<=m.n_in(); i++) - if (m.get_map_in_kind(i) == Exists_Var) return true; - for(int j=1;j<=m.n_out(); j++) - if (m.get_map_out_kind(j) == Exists_Var) return true; - return false; - } - - void get_relation_arity_from_one_mapping(const Mapping &m1, - int &in_req, int &out_req) { - int j, i; - in_req = 0; out_req = 0; - for(i = 1; i <= m1.n_in(); i++) { - j = m1.get_map_in_pos(i); - switch(m1.get_map_in_kind(i)) { - case Input_Var: in_req = max(in_req, j); break; - // case Set_Var: in_req = max(in_req, j); break; - case Output_Var: out_req = max(out_req, j); break; - default: break; - } - } - for(i = 1; i <= m1.n_out(); i++) { - j = m1.get_map_out_pos(i); - switch(m1.get_map_out_kind(i)) { - case Input_Var: in_req = max(in_req, j); break; - // case Set_Var: in_req = max(in_req, j); break; - case Output_Var: out_req = max(out_req, j); break; - default: break; - } - } - } - - // Scan mappings to see how many input and output variables they require. - void get_relation_arity_from_mappings(const Mapping &m1, - const Mapping &m2, - int &in_req, int &out_req) { - int inreq1, inreq2, outreq1, outreq2; - get_relation_arity_from_one_mapping(m1, inreq1, outreq1); - get_relation_arity_from_one_mapping(m2, inreq2, outreq2); - in_req = max(inreq1, inreq2); - out_req = max(outreq1, outreq2); - } -} - - -// -// Build lists of variables that need to be replaced in the given -// Formula. Declare globals in new relation. Then call -// map_vars to do the replacements. -// -// Obnoxiously many arguments here: -// Relation arguments contain declarations of symbolic and in/out vars. -// F_Exists argument is where needed existentially quant. vars can be decl. -// -// Mapping specifies how in/out vars are mapped -// Two lists are required to be able to map in/out variables from the first -// and second relations to the same existentially quantified variable. -// -void align(Rel_Body *originalr, Rel_Body *newr, F_Exists *fe, - Formula *f, const Mapping &mapping, bool &newrIsSet, - List<int> &seen_exists, Variable_ID_Tuple &seen_exists_ids) { - int i, cur_ex = 0; // initialize cur_ex to shut up the compiler - - f->set_relation(newr); // Might not need to do this anymore, if bugs were fixed - int input_remapped = 0; - int output_remapped = 0; - int sym_remapped = 0; - // skip_set_checks++; - - Variable_ID new_var; - Const_String new_name; - int new_pos; - - // MAP old input variables by setting their remap fields - for(i = 1; i <= originalr->n_inp(); i++) { - Variable_ID this_var = originalr->input_var(i), New_E; - Const_String this_name = originalr->In_Names[i]; - - switch (mapping.get_map_in_kind(i)) { - case Input_Var: - // case Set_Var: - // if (mapping.get_map_in_kind(i) == Set_Var) - // newrIsSet = true; // Don't mark it just yet; we still need to - // // refer to its "input" vars internally - - // assert((newrIsSet && mapping.get_map_in_kind(i) == Set_Var) - // || ((!newrIsSet &&mapping.get_map_in_kind(i) == Input_Var))); - - new_pos = mapping.get_map_in_pos(i); - new_var = newr->input_var(new_pos); - if (this_var != new_var) { - input_remapped = 1; - this_var->remap = new_var; - } - new_name = newr->In_Names[new_pos]; - if (!this_name.null()) { // should we name this? - if (!new_name.null()) { // already named, anonymize - if (new_name != this_name) - newr->name_input_var(new_pos, Const_String()); - } - else - newr->name_input_var(new_pos, this_name); - } - break; - case Output_Var: - assert(!newr->is_set()); - input_remapped = 1; - new_pos = mapping.get_map_in_pos(i); - this_var->remap = new_var = newr->output_var(new_pos); - new_name = newr->Out_Names[new_pos]; - if (!this_name.null()) { - if (!new_name.null()) { // already named, anonymize - if (new_name != this_name) - newr->name_output_var(new_pos, Const_String()); - } - else - newr->name_output_var(new_pos, this_name); - } - break; - case Exists_Var: - input_remapped = 1; - // check if we have declared it, use that if so. - // create it if not. - if (mapping.get_map_in_pos(i) <= 0 || - (cur_ex = seen_exists.index(mapping.get_map_in_pos(i))) == 0){ - if (!this_name.null()) - New_E = fe->declare(this_name); - else - New_E = fe->declare(); - this_var->remap = New_E; - if (mapping.get_map_in_pos(i) > 0) { - seen_exists.append(mapping.get_map_in_pos(i)); - seen_exists_ids.append(New_E); - } - } - else { - this_var->remap = new_var = seen_exists_ids[cur_ex]; - if (!this_name.null()) { // Have we already assigned a name? - if (!new_var->base_name.null()) { - if (new_var->base_name != this_name) - new_var->base_name = Const_String(); - } - else { - new_var->base_name = this_name; - assert(!this_name.null()); - } - } - } - break; - default: - assert(0 && "Unsupported var type in MapRel2"); - break; - } - } - - // MAP old output variables. - for(i = 1; i <= originalr->n_out(); i++) { - Variable_ID this_var = originalr->output_var(i), New_E; - Const_String this_name = originalr->Out_Names[i]; - - switch (mapping.get_map_out_kind(i)) { - case Input_Var: - // case Set_Var: - // if (mapping.get_map_out_kind(i) == Set_Var) - // newrIsSet = true; // Don't mark it just yet; we still need to refer to its "input" vars internally - - // assert((newrIsSet && mapping.get_map_out_kind(i) == Set_Var) - // ||((!newrIsSet &&mapping.get_map_out_kind(i) == Input_Var))); - - output_remapped = 1; - new_pos = mapping.get_map_out_pos(i); - this_var->remap = new_var = newr->input_var(new_pos); - new_name = newr->In_Names[new_pos]; - if (!this_name.null()) { - if (!new_name.null()) { // already named, anonymize - if (new_name != this_name) - newr->name_input_var(new_pos, Const_String()); - } - else - newr->name_input_var(new_pos, this_name); - } - break; - case Output_Var: - assert(!newr->is_set()); - new_pos = mapping.get_map_out_pos(i); - new_var = newr->output_var(new_pos); - if (new_var != this_var) { - output_remapped = 1; - this_var->remap = new_var; - } - new_name = newr->Out_Names[new_pos]; - if (!this_name.null()) { - if (!new_name.null()) { // already named, anonymize - if (new_name != this_name) - newr->name_output_var(new_pos, Const_String()); - } - else - newr->name_output_var(new_pos, this_name); - } - break; - case Exists_Var: - // check if we have declared it, create it if not. - output_remapped = 1; - if (mapping.get_map_out_pos(i) <= 0 || - (cur_ex = seen_exists.index(mapping.get_map_out_pos(i))) == 0) { // Declare it. - New_E = fe->declare(this_name); - this_var->remap = New_E; - if (mapping.get_map_out_pos(i) > 0) { - seen_exists.append(mapping.get_map_out_pos(i)); - seen_exists_ids.append(New_E); - } - } - else { - this_var->remap = new_var = seen_exists_ids[cur_ex]; - if (!this_name.null()) { - if (!new_var->base_name.null()) { - if (new_var->base_name != this_name) - new_var->base_name = Const_String(); - } - else { - new_var->base_name = this_name; - } - } - } - break; - default: - assert(0 &&"Unsupported var type in MapRel2"); - break; - } - } - - Variable_ID_Tuple *oldSym = originalr->global_decls(); - for(i=1; i<=(*oldSym).size(); i++) { - Variable_ID v = (*oldSym)[i]; - assert(v->kind()==Global_Var); - if (v->get_global_var()->arity() > 0) { - Argument_Tuple new_of = v->function_of(); - if (!leave_pufs_untouched) - new_of = mapping.get_tuple_fate(new_of, v->get_global_var()->arity()); - if (new_of == Unknown_Tuple) { - // hopefully v is not really used - // if we get here, f should have been in DNF, - // now an OR node with conjuncts below - // we just need to check that no conjunct uses v -#if ! defined NDEBUG - if (f->node_type() == Op_Conjunct) { - assert(f->really_conjunct()->mappedVars.index(v)==0 - && "v unused"); - } -#if 0 - else { - // assert(f->node_type() == Op_Or); - for (List_Iterator<Formula *> conj(f->children()); conj; conj++) { - assert((*conj)->really_conjunct()->mappedVars.index(v)==0 - && "v unused"); - } - } -#endif -#endif - // since its not really used, don't bother adding it to - // the the global_vars list of the new relation - continue; - } - if (v->function_of() != new_of) { - Variable_ID new_v=newr->get_local(v->get_global_var(),new_of); - assert(v != new_v); - v->remap = new_v; - sym_remapped = 1; - } - else { - // add symbolic to symbolic list -#if ! defined NDEBUG - Variable_ID new_v = -#endif - newr->get_local(v->get_global_var(), v->function_of()); -#if ! defined NDEBUG - assert(v == new_v); -#endif - } - } - else { - // add symbolic to symbolic list -#if ! defined NDEBUG - Variable_ID new_v = -#endif - newr->get_local(v->get_global_var()); -#if ! defined NDEBUG - assert(v == new_v); -#endif - } - } - - if (sym_remapped || input_remapped || output_remapped) { - f->remap(); - - // If 2 vars mapped to same variable, combine them - //There's a column to combine only when there are two equal remap fields. - Tuple<Variable_ID> vt(0); - bool combine = false; - Tuple_Iterator<Variable_ID> t(input_vars); - for(i=1; !combine && i<=originalr->n_inp(); t++, i++) - if (vt.index((*t)->remap)) - combine = true; - else - vt.append((*t)->remap); - Tuple_Iterator<Variable_ID> t2(output_vars); - for(i=1; !combine && i <= originalr->n_out(); t2++, i++) - if (vt.index((*t2)->remap)) - combine = true; - else - vt.append((*t2)->remap); - if (combine) f->combine_columns(); - - if (sym_remapped) - reset_remap_field(originalr->Symbolic); - if (input_remapped) - reset_remap_field(input_vars,originalr->n_inp()); - if (output_remapped) - reset_remap_field(output_vars,originalr->n_out()); - } - - // skip_set_checks--; - -#ifndef NDEBUG - if (fe) - foreach(v,Variable_ID,fe->myLocals,assert(v == v->remap)); -#endif -} - - -// MapRel1, MapAndCombineRel2 can be replaced by merge_rels -void MapRel1(Relation &R, const Mapping &map, Combine_Type ctype, - int number_input, int number_output, - bool invalidate_resulting_leading_info, - bool finalize) { -#if defined(INCLUDE_COMPRESSION) - assert(!R.is_compressed()); -#endif - assert(!R.is_null()); - - Relation inputRel = R; - R = Relation(); - Rel_Body *inputRelBody = inputRel.split(); - - int in_req=0, out_req=0; - get_relation_arity_from_one_mapping(map, in_req, out_req); - - R = Relation(number_input == -1 ? in_req : number_input, - number_output == -1 ? out_req : number_output); - - Rel_Body *outputRelBody = R.split(); - - inputRelBody->DNF_to_formula(); - Formula *f1 = inputRelBody->rm_formula(); - - F_Exists *fe; - Formula *f; - if (has_existentials(map)) { - f = fe = outputRelBody->add_exists(); - } - else { - fe = NULL; - f = outputRelBody; - } - and_below_exists = NULL; - if (finalize) and_below_exists = NULL; - else f = and_below_exists = f->add_and(); - if(ctype == Comb_AndNot) { - f = f->add_not(); - } - f->add_child(f1); - - exists_ids.clear(); - exists_numbers.clear(); - - bool returnAsSet=false; - align(inputRelBody, outputRelBody, fe, f1, map, returnAsSet, - exists_numbers, exists_ids); - - if (returnAsSet || - (inputRelBody->is_set() && outputRelBody->n_out() == 0)) { - R.markAsSet(); - R.invalidate_leading_info(); // nonsensical for a set - } - - if (finalize) R.finalize(); - inputRel = Relation(); - if (invalidate_resulting_leading_info) - R.invalidate_leading_info(); -} - - -Relation MapAndCombineRel2(Relation &R1, Relation &R2, const Mapping &mapping1, - const Mapping &mapping2, Combine_Type ctype, - int number_input, int number_output) { -#if defined(INCLUDE_COMPRESSION) - assert(!R1.is_compressed()); - assert(!R2.is_compressed()); -#endif - assert(!R1.is_null() && !R2.is_null()); - Rel_Body *r1 = R1.split(); - Rel_Body *r2 = R2.split(); - - int in_req, out_req; // Create the new relation - get_relation_arity_from_mappings(mapping1, mapping2, in_req, out_req); - Relation R3(number_input == -1 ? in_req : number_input, - number_output == -1 ? out_req : number_output); - Rel_Body *r3 = R3.split(); // This is just to get the pointer, it's cheap - - /* permit the add_{exists,and} below, reset after they are done.*/ - skip_finalization_check++; - - F_Exists *fe = NULL; - Formula *f; - if (has_existentials(mapping1) || has_existentials(mapping2)) { - fe = r3->add_exists(); - f = fe; - } - else { - f = r3; - } - - r1->DNF_to_formula(); - Formula *f1 = r1->rm_formula(); - r2->DNF_to_formula(); - Formula *f2 = r2->rm_formula(); - - // align: change r1 vars to r3 vars in formula f1 via map mapping1, - // declaring needed exists vars in F_Exists *fe - // Also maps symbolic variables appropriately, sets relation ptrs in f1. - // In order to map variables of both relations to the same variables, - // we keep a list of new existentially quantified vars between calls. - // returnAsSet means mark r3 as set before return. Don't mark it yet, - // because internally we need to refer to "input_vars" of a set, and that - // would blow assertions. - - bool returnAsSet=false; - exists_ids.clear(); - exists_numbers.clear(); - align(r1, r3, fe, f1, mapping1, returnAsSet, exists_numbers, exists_ids); - // align: change r2 vars to r3 vars in formula f2 via map mapping2 - align(r2, r3, fe, f2, mapping2, returnAsSet, exists_numbers, exists_ids); - - switch (ctype) { - case Comb_Or: - if(f1->node_type() == Op_Or) { - f->add_child(f1); - f = f1; - } - else { - f = f->add_or(); - f->add_child(f1); - } - break; - case Comb_And: - case Comb_AndNot: - if(f1->node_type() == Op_And) { - f->add_child(f1); - f = f1; - } - else { - f = f->add_and(); - f->add_child(f1); - } - break; - default: - assert(0 && "Invalid combine type in MapAndCombineRel2"); - } - - Formula *c2; - if (ctype==Comb_AndNot) { - c2 = f->add_not(); - } - else { - c2 = f; - } - c2->add_child(f2); - - skip_finalization_check--; /* Set this back for return */ - R3.finalize(); - - if (returnAsSet || - (R1.is_set() && R2.is_set() && R3.n_inp() >= 0 && R3.n_out() == 0)){ - R3.markAsSet(); - R3.invalidate_leading_info(); - } - R1 = Relation(); - R2 = Relation(); - return R3; -} - - -// -// Scramble each relation's variables and merge these relations -// together. Support variable mapping to and from existentials. -// Unspecified variables in mapping are mapped to themselves by -// default. It intends to replace MapRel1 and MapAndCombineRel2 -// functions (the time saved by grafting formula tree might be -// neglegible when compared to the simplification cost). -// -Relation merge_rels(Tuple<Relation> &R, const Tuple<std::map<Variable_ID, std::pair<Var_Kind, int> > > &mapping, const Tuple<bool> &inverse, Combine_Type ctype, int number_input, int number_output) { - const int m = R.size(); - assert(mapping.size() == m && inverse.size() == m); - // skip_set_checks++; - - // if new relation's arity is not given, calculate it on demand - if (number_input == -1) { - number_input = 0; - for (int i = 1; i <= m; i++) { - for (int j = R[i].n_inp(); j >= 1; j--) { - Variable_ID v = R[i].input_var(j); - std::map<Variable_ID, std::pair<Var_Kind, int> >::const_iterator p = mapping[i].find(v); - if (p == mapping[i].end()) { - number_input = j; - break; - } - } - - for (std::map<Variable_ID, std::pair<Var_Kind, int> >::const_iterator j = mapping[i].begin(); j != mapping[i].end(); j++) { - if ((*j).second.first == Input_Var || (*j).second.first == Set_Var) - number_input = max(number_input, (*j).second.second); - } - } - } - - if (number_output == -1) { - number_output = 0; - for (int i = 1; i <= m; i++) { - for (int j = R[i].n_out(); j >= 1; j--) { - Variable_ID v = R[i].output_var(j); - std::map<Variable_ID, std::pair<Var_Kind, int> >::const_iterator p = mapping[i].find(v); - if (p == mapping[i].end()) { - number_output = j; - break; - } - } - for (std::map<Variable_ID, std::pair<Var_Kind, int> >::const_iterator j = mapping[i].begin(); j != mapping[i].end(); j++) { - if ((*j).second.first == Output_Var) - number_output = max(number_output, (*j).second.second); - } - } - } - - Relation R2(number_input, number_output); - F_Exists *fe = R2.add_exists(); - Formula *f_root; - switch (ctype) { - case Comb_And: - f_root = fe->add_and(); - break; - case Comb_Or: - f_root = fe->add_or(); - break; - default: - assert(0); // unsupported merge type - } - - std::map<int, Variable_ID> seen_exists_by_num; - std::map<Variable_ID, Variable_ID> seen_exists_by_id; - - for (int i = 1; i <= m; i++) { - F_Or *fo; - if (inverse[i]) - fo = f_root->add_not()->add_or(); - else - fo = f_root->add_or(); - - for (DNF_Iterator di(R[i].query_DNF()); di; di++) { - F_And *f = fo->add_and(); - - for (GEQ_Iterator gi(*di); gi; gi++) { - GEQ_Handle h = f->add_GEQ(); - for (Constr_Vars_Iter cvi(*gi); cvi; cvi++) { - Variable_ID v = cvi.curr_var(); - std::map<Variable_ID, std::pair<Var_Kind, int> >::const_iterator p = mapping[i].find(v); - if (p == mapping[i].end()) { - switch (v->kind()) { - // case Set_Var: - case Input_Var: { - int pos = v->get_position(); - h.update_coef(R2.input_var(pos), cvi.curr_coef()); - break; - } - case Output_Var: { - int pos = v->get_position(); - h.update_coef(R2.output_var(pos), cvi.curr_coef()); - break; - } - case Exists_Var: - case Wildcard_Var: { - std::map<Variable_ID, Variable_ID>::iterator p2 = seen_exists_by_id.find(cvi.curr_var()); - Variable_ID e; - if (p2 == seen_exists_by_id.end()) { - e = fe->declare(); - seen_exists_by_id[cvi.curr_var()] = e; - } - else - e = (*p2).second; - h.update_coef(e, cvi.curr_coef()); - break; - } - case Global_Var: { - Global_Var_ID g = v->get_global_var(); - Variable_ID v2; - if (g->arity() == 0) - v2 = R2.get_local(g); - else - v2 = R2.get_local(g, v->function_of()); - h.update_coef(v2, cvi.curr_coef()); - break; - } - default: - assert(0); // shouldn't happen if input relations are simplified - } - } - else { - switch ((*p).second.first) { - // case Set_Var: - case Input_Var: { - int pos = (*p).second.second; - h.update_coef(R2.input_var(pos), cvi.curr_coef()); - break; - } - case Output_Var: { - int pos = (*p).second.second; - h.update_coef(R2.output_var(pos), cvi.curr_coef()); - break; - } - case Exists_Var: - case Wildcard_Var: { - int pos = (*p).second.second; - std::map<int, Variable_ID>::iterator p2 = seen_exists_by_num.find(pos); - Variable_ID e; - if (p2 == seen_exists_by_num.end()) { - e = fe->declare(); - seen_exists_by_num[pos] = e; - } - else - e = (*p2).second; - h.update_coef(e, cvi.curr_coef()); - break; - } - default: - assert(0); // mapped to unsupported variable type - } - } - } - h.update_const((*gi).get_const()); - } - - for (EQ_Iterator ei(*di); ei; ei++) { - EQ_Handle h = f->add_EQ(); - for (Constr_Vars_Iter cvi(*ei); cvi; cvi++) { - Variable_ID v = cvi.curr_var(); - std::map<Variable_ID, std::pair<Var_Kind, int> >::const_iterator p = mapping[i].find(v); - if (p == mapping[i].end()) { - switch (v->kind()) { - // case Set_Var: - case Input_Var: { - int pos = v->get_position(); - h.update_coef(R2.input_var(pos), cvi.curr_coef()); - break; - } - case Output_Var: { - int pos = v->get_position(); - h.update_coef(R2.output_var(pos), cvi.curr_coef()); - break; - } - case Exists_Var: - case Wildcard_Var: { - std::map<Variable_ID, Variable_ID>::iterator p2 = seen_exists_by_id.find(v); - Variable_ID e; - if (p2 == seen_exists_by_id.end()) { - e = fe->declare(); - seen_exists_by_id[v] = e; - } - else - e = (*p2).second; - h.update_coef(e, cvi.curr_coef()); - break; - } - case Global_Var: { - Global_Var_ID g = v->get_global_var(); - Variable_ID v2; - if (g->arity() == 0) - v2 = R2.get_local(g); - else - v2 = R2.get_local(g, v->function_of()); - h.update_coef(v2, cvi.curr_coef()); - break; - } - default: - assert(0); // shouldn't happen if input relations are simplified - } - } - else { - switch ((*p).second.first) { - // case Set_Var: - case Input_Var: { - int pos = (*p).second.second; - h.update_coef(R2.input_var(pos), cvi.curr_coef()); - break; - } - case Output_Var: { - int pos = (*p).second.second; - h.update_coef(R2.output_var(pos), cvi.curr_coef()); - break; - } - case Exists_Var: - case Wildcard_Var: { - int pos = (*p).second.second; - std::map<int, Variable_ID>::iterator p2 = seen_exists_by_num.find(pos); - Variable_ID e; - if (p2 == seen_exists_by_num.end()) { - e = fe->declare(); - seen_exists_by_num[pos] = e; - } - else - e = (*p2).second; - h.update_coef(e, cvi.curr_coef()); - break; - } - default: - assert(0); // mapped to unsupported variable type - } - } - } - h.update_const((*ei).get_const()); - } - } - } - - // skip_set_checks--; - - if (number_output == 0) { - R2.markAsSet(); - // R2.invalidate_leading_info(); - } - - return R2; -} - -} // namespace |