diff options
Diffstat (limited to 'omegalib/omega_lib/include/omega/Rel_map.h')
| -rw-r--r-- | omegalib/omega_lib/include/omega/Rel_map.h | 161 |
1 files changed, 0 insertions, 161 deletions
diff --git a/omegalib/omega_lib/include/omega/Rel_map.h b/omegalib/omega_lib/include/omega/Rel_map.h deleted file mode 100644 index 5641cb3..0000000 --- a/omegalib/omega_lib/include/omega/Rel_map.h +++ /dev/null @@ -1,161 +0,0 @@ -#if ! defined _Rel_map_h -#define _Rel_map_h 1 - -#include <omega/pres_gen.h> -#include <omega/pres_var.h> - -namespace omega { - -// -// Mapping for relations -// When a relation operation needs to re-arrange the variables, -// it describes the re-arragement with a mapping, and then calls -// align to re-arrange them. -// -// In a mapping, map_in (map_out/map_set) gives the new type and -// position of each of the old input (output/set) variables. -// For variables being mapped to Input, Output, or Set variables, -// the position is the new position in the tuple. -// For variables being mapped to Exists_Var, Forall_Var, or -// Wildcard_Var, the positions can be used to map multiple -// variables to the same quantified variable, by providing -// the same position. Each variable with a negative position -// is given a unique quantified variable that is NOT listed -// in the seen_exists_ids list. -// I'm not sure what the positions mean for Global_Vars - perhaps -// they are ignored? -// -// Currently, align seems to support only mapping to Set, Input, -// Output, and Exists vars. -// - -class Mapping { -public: - inline Mapping(int no_in, int no_out): n_input(no_in), n_output(no_out) {} - inline Mapping(int no_set): n_input(no_set), n_output(0){} - inline Mapping(const Mapping &m): n_input(m.n_input), n_output(m.n_output) { - int i; - for(i=1; i<=n_input; i++) map_in_kind[i] = m.map_in_kind[i]; - for(i=1; i<=n_input; i++) map_in_pos[i] = m.map_in_pos[i]; - for(i=1; i<=n_output;i++) map_out_kind[i] = m.map_out_kind[i]; - for(i=1; i<=n_output;i++) map_out_pos[i] = m.map_out_pos[i]; - } - - inline void set_map (Var_Kind in_kind, int pos, Var_Kind type, int map) { - if(in_kind==Input_Var) - set_map_in(pos,type,map); - else if(in_kind==Set_Var) - set_map_in(pos,type,map); - else if(in_kind==Output_Var) - set_map_out(pos,type,map); - else - assert(0); - } - - inline void set_map_in (int pos, Var_Kind type, int map) { - assert(pos>=1 && pos<=n_input); - map_in_kind[pos] = type; - map_in_pos[pos] = map; - } - inline void set_map_set (int pos, Var_Kind type, int map) { - assert(pos>=1 && pos<=n_input); - map_in_kind[pos] = type; - map_in_pos[pos] = map; - } - - inline void set_map_out(int pos, Var_Kind type, int map) { - assert(pos>=1 && pos<=n_output); - map_out_kind[pos] = type; - map_out_pos[pos] = map; - } - - inline Var_Kind get_map_in_kind(int pos) const { - assert(pos>=1 && pos<=n_input); - return map_in_kind[pos]; - } - - inline int get_map_in_pos(int pos) const { - assert(pos>=1 && pos<=n_input); - return map_in_pos[pos]; - } - - inline Var_Kind get_map_out_kind(int pos) const { - assert(pos>=1 && pos<=n_output); - return map_out_kind[pos]; - } - - inline int get_map_out_pos(int pos) const { - assert(pos>=1 && pos<=n_output); - return map_out_pos[pos]; - } - - inline int n_in() const { return n_input; } - inline int n_out() const { return n_output; } - - // If a tuple as a whole becomes the new Input or Output tuple, - // return the Tuple of they will become (Input, Output) - // Return Unknown_Tuple otherwise - - inline Argument_Tuple get_tuple_fate(Argument_Tuple t, int prefix = -1) const { - return t== Input_Tuple ? get_input_fate(prefix) : - (t==Output_Tuple ? get_output_fate(prefix) : Unknown_Tuple); } - - inline Argument_Tuple get_set_fate(int prefix = -1) const { - return get_input_fate(prefix); } - - inline Argument_Tuple get_input_fate(int prefix = -1) const { - if (prefix < 0) prefix = n_input; - assert(n_input >= prefix); - if (n_input < prefix) - return Unknown_Tuple; - Var_Kind vf = map_in_kind[1]; - for (int i = 1; i<=prefix; i++) - if (map_in_pos[i]!=i || map_in_kind[i]!=vf) - return Unknown_Tuple; - - return vf == Input_Var ? Input_Tuple - : vf == Set_Var ? Set_Tuple - : vf == Output_Var ? Output_Tuple - : Unknown_Tuple; - } - - inline Argument_Tuple get_output_fate(int prefix = -1) const { - if (prefix < 0) prefix = n_output; - assert(n_output >= prefix); - if (n_output < 1) - return Unknown_Tuple; - Var_Kind vf = map_out_kind[1]; - for (int i = 1; i<=prefix; i++) - if (map_out_pos[i]!=i || map_out_kind[i]!=vf) - return Unknown_Tuple; - return vf == Input_Var ? Input_Tuple - : vf == Set_Var ? Set_Tuple - : vf == Output_Var ? Output_Tuple - : Unknown_Tuple; - } - - inline static Mapping Identity(int inp, int outp) { - Mapping m(inp, outp); int i; - for(i=1; i<=m.n_input; i++) m.set_map(Input_Var, i, Input_Var, i); - for(i=1; i<=m.n_output;i++) m.set_map(Output_Var, i, Output_Var, i); - return m; - } - - inline static Mapping Identity(int setvars) { - Mapping m(setvars); int i; - for(i=1; i<=setvars; i++) m.set_map(Set_Var, i, Set_Var, i); - return m; - } - -private: - int n_input; - int n_output; - Var_Kind map_in_kind[maxVars]; - int map_in_pos[maxVars]; - Var_Kind map_out_kind[maxVars]; - int map_out_pos[maxVars]; -}; - -} // namespace - -#endif |