diff options
Diffstat (limited to 'omegalib/omega_lib/include/omega')
25 files changed, 0 insertions, 2851 deletions
diff --git a/omegalib/omega_lib/include/omega/RelBody.h b/omegalib/omega_lib/include/omega/RelBody.h deleted file mode 100644 index 3c11702..0000000 --- a/omegalib/omega_lib/include/omega/RelBody.h +++ /dev/null @@ -1,165 +0,0 @@ -#if ! defined _RelBody_h -#define _RelBody_h 1 - -#include <omega/pres_form.h> -#include <omega/pres_dnf.h> - -namespace omega { - -typedef enum {under_construction, compressed, uncompressed} Rel_Body_Status; -typedef unsigned char Rel_Unknown_Uses; -const Rel_Unknown_Uses no_u = 1; -const Rel_Unknown_Uses and_u = 2; -const Rel_Unknown_Uses or_u = 4; - -// -// Relation body. -// Body and representative are separated to do reference counting. -// - -class Rel_Body : public Formula { -public: - bool is_null() const; - - inline Node_Type node_type() { return Op_Relation; } - - inline bool is_set() const { return number_output == 0; } - int n_inp() const; - int n_out() const; - int n_set() const; - - inline Variable_ID_Tuple *global_decls() { return &Symbolic; } - int max_ufs_arity(); - int max_shared_ufs_arity(); - int max_ufs_arity_of_set(); - int max_ufs_arity_of_in(); - int max_ufs_arity_of_out(); - - Variable_ID input_var(int nth); - Variable_ID output_var(int nth); - Variable_ID set_var(int nth); - Variable_ID get_local(const Variable_ID v); - Variable_ID get_local(const Global_Var_ID G); - Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of); - bool has_local(const Global_Var_ID G); - bool has_local(const Global_Var_ID G, Argument_Tuple of); - void name_input_var(int, Const_String); - void name_output_var(int, Const_String); - void name_set_var(int, Const_String); - - F_And *and_with_and(); - EQ_Handle and_with_EQ(); - EQ_Handle and_with_EQ(const Constraint_Handle &c); - GEQ_Handle and_with_GEQ(); - GEQ_Handle and_with_GEQ(const Constraint_Handle &c); - - void print(); - void print(FILE *output_file) { print(output_file, true); } - void print(FILE *output_file, bool printSym); - std::string print_variables_to_string(bool printSym); - void print_with_subs(FILE *output_file, bool printSym, bool newline); - void print_with_subs(); - std::string print_with_subs_to_string(bool printSym, bool newline); - std::string print_outputs_with_subs_to_string(); - std::string print_outputs_with_subs_to_string(int i); - std::string print_formula_to_string(); - void prefix_print(); - void prefix_print(FILE *output_file, int debug = 1); - - bool is_satisfiable(); - bool is_lower_bound_satisfiable(); - bool is_upper_bound_satisfiable(); - bool is_obvious_tautology(); - bool is_definite_tautology(); - bool is_unknown(); - DNF* query_DNF(); - DNF* query_DNF(int rdt_conjs, int rdt_constrs); - void simplify(int rdt_conjs = 0, int rdt_constrs = 0); - void finalize(); - inline bool is_finalized() { return finalized; } - inline bool is_shared() { return ref_count > 1; } - - void query_difference(Variable_ID v1, Variable_ID v2, - coef_t &lowerBound, coef_t &upperBound, - bool &quaranteed); - void query_variable_bounds(Variable_ID, coef_t &lowerBound, coef_t &upperBound); - coef_t query_variable_mod(Variable_ID v, coef_t factor); - - Relation extract_dnf_by_carried_level(int level, int direction); - void make_level_carried_to(int level); - - // these are only public to allow the creation of "null_rel" - Rel_Body(); - ~Rel_Body(); - void setup_names(); - -private: - - // These are manipulated primarily as parts of Relations - friend class Relation; - friend_rel_ops; - - friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel); - - Rel_Unknown_Uses unknown_uses(); - - inline bool is_simplified() const { return (simplified_DNF!=NULL && get_children().empty()); } - bool is_compressed(); - Conjunct *rm_first_conjunct(); - Conjunct *single_conjunct(); - bool has_single_conjunct(); - - void beautify(); - void rearrange(); - - friend class EQ_Handle; // these set up names for printing - friend class GEQ_Handle; // and check if simplified - friend class Constraint_Handle; // and update coefficients - - void compress(); - void uncompress(); - - void interpret_unknown_as_true(); - void interpret_unknown_as_false(); - - Rel_Body(int n_input, int n_output); - /* Rel_Body(Rel_Body *r); */ - Rel_Body(Rel_Body *r, Conjunct *c); - Rel_Body &operator=(Rel_Body &r); - Rel_Body *clone(); - - inline Formula *formula() { return children().front(); } - inline Formula *rm_formula() { return children().remove_front(); } - bool can_add_child(); - - void reverse_leading_dir_info(); - void invalidate_leading_info(int changed = -1) { Formula::invalidate_leading_info(changed); } - void enforce_leading_info(int guaranteed, int possible, int dir) { Formula::enforce_leading_info(guaranteed, possible, dir); } - // re-declare this so that Relation (a friend) can call it - - DNF* DNFize(); - void DNF_to_formula(); - - Conjunct *find_available_conjunct(); - F_And *find_available_And(); - - -/* === data === */ -private: - - int ref_count; - Rel_Body_Status status; - - int number_input, number_output; - Tuple<Const_String> In_Names, Out_Names; - Variable_ID_Tuple Symbolic; - - DNF* simplified_DNF; - short r_conjs; // are redundant conjuncts eliminated? - bool finalized; - bool _is_set; -}; - -} // namespace - -#endif 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 diff --git a/omegalib/omega_lib/include/omega/Relation.h b/omegalib/omega_lib/include/omega/Relation.h deleted file mode 100644 index b41bef5..0000000 --- a/omegalib/omega_lib/include/omega/Relation.h +++ /dev/null @@ -1,299 +0,0 @@ -#if ! defined _Relation_h -#define _Relation_h 1 - -#include <omega/RelBody.h> -#include <omega/pres_cnstr.h> -#include <iostream> -#include <limits.h> - -namespace omega { - -// -// Relation representative. -// Body and representative are separated to do reference counting. -// -class Relation { -public: - Relation(); - - Relation(int n_input, int n_output = 0); - Relation(const Relation &r); - Relation(const Relation &r, Conjunct *c); - Relation &operator=(const Relation &r); - Relation(Rel_Body &r, int foo); - - static Relation Null(); - static Relation Empty(const Relation &R); - static Relation True(const Relation &R); - static Relation True(int setvars); - static Relation True(int in, int out); - static Relation False(const Relation &R); - static Relation False(int setvars); - static Relation False(int in, int out); - static Relation Unknown(const Relation &R); - static Relation Unknown(int setvars); - static Relation Unknown(int in, int out); - - - bool is_null() const; - - ~Relation(); - - inline F_Forall *add_forall() - { return rel_body->add_forall(); } - inline F_Exists *add_exists() - { return rel_body->add_exists(); } - inline F_And *add_and() - { return rel_body->add_and(); } - inline F_And *and_with() - { return rel_body->and_with(); } - inline F_Or *add_or() - { return rel_body->add_or(); } - inline F_Not *add_not() - { return rel_body->add_not(); } - inline void finalize() - { rel_body->finalize(); } - inline bool is_finalized() const - { return rel_body->finalized; } - inline bool is_set() const - { return rel_body->is_set(); } - inline int n_inp() const - { return rel_body->n_inp(); } - inline int n_out() const - { return rel_body->n_out(); } - inline int n_set() const - { return rel_body->n_set(); } - - inline const Variable_ID_Tuple *global_decls() const - { return rel_body->global_decls(); } - inline int max_ufs_arity() const - { return rel_body->max_ufs_arity(); } - inline int max_ufs_arity_of_in() const - { return rel_body->max_ufs_arity_of_in(); } - inline int max_ufs_arity_of_set() const - { return rel_body->max_ufs_arity_of_set(); } - inline int max_ufs_arity_of_out() const - { return rel_body->max_ufs_arity_of_out(); } - inline int max_shared_ufs_arity() const - { return rel_body->max_shared_ufs_arity(); } - - inline Variable_ID input_var(int nth) - { return rel_body->input_var(nth); } - inline Variable_ID output_var(int nth) - { return rel_body->output_var(nth); } - inline Variable_ID set_var(int nth) - { return rel_body->set_var(nth); } - inline bool has_local(const Global_Var_ID G) - { return rel_body->has_local(G); } - inline bool has_local(const Global_Var_ID G, Argument_Tuple of) - { return rel_body->has_local(G, of); } - inline Variable_ID get_local(const Variable_ID v) - { return split()->get_local(v); } - inline Variable_ID get_local(const Global_Var_ID G) - { return split()->get_local(G); } - inline Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of) - { return split()->get_local(G, of); } - - inline void name_input_var(int nth, Const_String S) - { split()->name_input_var(nth, S); } - inline void name_output_var(int nth, Const_String S) - { split()->name_output_var(nth, S); } - inline void name_set_var(int nth, Const_String S) - { split()->name_set_var(nth, S); } - - - inline F_And *and_with_and() - { return split()->and_with_and(); } - inline EQ_Handle and_with_EQ() - { return split()->and_with_EQ(); } - inline EQ_Handle and_with_EQ(const Constraint_Handle &c) - { return split()->and_with_EQ(c); } - inline GEQ_Handle and_with_GEQ() - { return split()->and_with_GEQ(); } - inline GEQ_Handle and_with_GEQ(const Constraint_Handle &c) - { return split()->and_with_GEQ(c); } - - inline void print() - { rel_body->print(); } - inline void print(FILE *output_file) - { rel_body->print(output_file); } - inline void print_with_subs() - { rel_body->print_with_subs(); } - inline void print_with_subs(FILE *output_file, bool printSym=false, - bool newline=true) - { rel_body->print_with_subs(output_file, printSym, newline); } - inline std::string print_with_subs_to_string(bool printSym=false, - bool newline=true) - { return rel_body->print_with_subs_to_string(printSym, newline); } - inline std::string print_outputs_with_subs_to_string() - { return rel_body->print_outputs_with_subs_to_string(); } - inline std::string print_outputs_with_subs_to_string(int i) - { return rel_body->print_outputs_with_subs_to_string(i); } - inline void prefix_print() - { rel_body->prefix_print(); } - inline void prefix_print(FILE *output_file, int debug = 1) - { rel_body->prefix_print(output_file, debug); } - inline std::string print_formula_to_string() { - return rel_body->print_formula_to_string(); - } - void dimensions(int & ndim_all, int &ndim_domain); - - inline bool is_lower_bound_satisfiable() - { return rel_body->is_lower_bound_satisfiable(); } - inline bool is_upper_bound_satisfiable() - { return rel_body->is_upper_bound_satisfiable(); } - inline bool is_satisfiable() - { return rel_body->is_satisfiable(); } - - inline bool is_tautology() - { return rel_body->is_obvious_tautology(); } // for compatibility - inline bool is_obvious_tautology() - { return rel_body->is_obvious_tautology(); } - inline bool is_definite_tautology() - { return rel_body->is_definite_tautology(); } - - // return x s.t. forall conjuncts c, c has >= x leading 0s - // for set, return -1 (pass this in, in case there are no conjuncts - inline int number_of_conjuncts() - { return rel_body->query_DNF()->length(); } - - // return x s.t. forall conjuncts c, c has >= x leading 0s - // for set, return -1 (pass this in, in case there are no conjuncts - inline int query_guaranteed_leading_0s() - { return rel_body->query_DNF()->query_guaranteed_leading_0s(this->is_set() ? -1 : 0); } - - // return x s.t. forall conjuncts c, c has <= x leading 0s - // if no conjuncts return min of input and output tuple sizes, or -1 if relation is a set - inline int query_possible_leading_0s() - { return rel_body->query_DNF()->query_possible_leading_0s( - this->is_set()? -1 : min(n_inp(),n_out())); } - - // return +-1 according to sign of leading dir, or 0 if we don't know - inline int query_leading_dir() - { return rel_body->query_DNF()->query_leading_dir(); } - - inline DNF* query_DNF() - { return rel_body->query_DNF(); } - inline DNF* query_DNF(int rdt_conjs, int rdt_constrs) - { return rel_body->query_DNF(rdt_conjs, rdt_constrs); } - inline void simplify(int rdt_conjs = 0, int rdt_constrs = 0) - { rel_body->simplify(rdt_conjs, rdt_constrs); } - inline bool is_simplified() - { return rel_body->is_simplified(); } - inline bool is_compressed() const - { return rel_body->is_compressed(); } - inline Conjunct *rm_first_conjunct() - { return rel_body->rm_first_conjunct(); } - inline Conjunct *single_conjunct() - { return rel_body->single_conjunct(); } - inline bool has_single_conjunct() - { return rel_body->has_single_conjunct(); } - - - void query_difference(Variable_ID v1, Variable_ID v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed) { - rel_body->query_difference(v1, v2, lowerBound, upperBound, guaranteed); - } - void query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound) { - rel_body->query_variable_bounds(v,lowerBound,upperBound); - } - coef_t query_variable_mod(Variable_ID v, coef_t factor) { - assert(factor > 0); - return rel_body->query_variable_mod(v, factor); - } - int query_variable_mod(Variable_ID v, int factor) { - assert(sizeof(int) <= sizeof(coef_t)); - coef_t result = rel_body->query_variable_mod(v, static_cast<coef_t>(factor)); - if (result == posInfinity) - return INT_MAX; - else - return static_cast<int>(result); - } - - - inline void make_level_carried_to(int level) - { - split()->make_level_carried_to(level); - } - - inline Relation extract_dnf_by_carried_level(int level, int direction) - { - return split()->extract_dnf_by_carried_level(level, direction); - } - - inline void compress() - { -#if defined(INCLUDE_COMPRESSION) - split()->compress(); -#endif - } - void uncompress() - { rel_body->uncompress(); } - - inline bool is_exact() const - { return !(rel_body->unknown_uses() & (and_u | or_u)) ; } - inline bool is_inexact() const - { return !is_exact(); } - inline bool is_unknown() const - { return rel_body->is_unknown(); } - inline Rel_Unknown_Uses unknown_uses() const - { return rel_body->unknown_uses(); } - - void setup_names() {rel_body->setup_names();} - void copy_names(const Relation &r) { - copy_names(*r.rel_body); - }; - void copy_names(Rel_Body &r); - -private: - // Functions that have to create sets from relations: - friend class Rel_Body; - friend_rel_ops; - - - Rel_Body *split(); - - DNF* simplified_DNF() { - simplify(); - return rel_body->simplified_DNF; - }; - - inline void invalidate_leading_info(int changed = -1) - { split()->invalidate_leading_info(changed); } - inline void enforce_leading_info(int guaranteed, int possible, int dir) - { - split()->enforce_leading_info(guaranteed, possible, dir); - } - - - void makeSet(); - void markAsSet(); - void markAsRelation(); - - friend bool operator==(const Relation &, const Relation &); - - void reverse_leading_dir_info() - { split()->reverse_leading_dir_info(); } - void interpret_unknown_as_true() - { split()->interpret_unknown_as_true(); } - void interpret_unknown_as_false() - { split()->interpret_unknown_as_false(); } - - - Rel_Body *rel_body; - - - friend 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); -}; - -inline std::ostream & operator<<(std::ostream &o, Relation &R) -{ - return o << R.print_with_subs_to_string(); -} - -Relation copy(const Relation &r); - -} // namespace - -#include <omega/Relations.h> - -#endif diff --git a/omegalib/omega_lib/include/omega/Relations.h b/omegalib/omega_lib/include/omega/Relations.h deleted file mode 100644 index 4fd81e6..0000000 --- a/omegalib/omega_lib/include/omega/Relations.h +++ /dev/null @@ -1,88 +0,0 @@ -#if ! defined _Relations_h -#define _Relations_h 1 - -#include <map> -#include <omega/Relation.h> - -namespace omega { - -// UPDATE friend_rel_ops IN pres_gen.h WHEN ADDING TO THIS LIST -// REMEMBER TO TAKE OUT DEFAULT ARGUMENTS IN THAT FILE - -/* 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); - -// -// Operations over relations -// -Relation Union(NOT_CONST Relation &r1, NOT_CONST Relation &r2); -Relation Intersection(NOT_CONST Relation &r1, NOT_CONST Relation &r2); -Relation Extend_Domain(NOT_CONST Relation &R); -Relation Extend_Domain(NOT_CONST Relation &R, int more); -Relation Extend_Range(NOT_CONST Relation &R); -Relation Extend_Range(NOT_CONST Relation &R, int more); -Relation Extend_Set(NOT_CONST Relation &R); -Relation Extend_Set(NOT_CONST Relation &R, int more); -Relation Restrict_Domain(NOT_CONST Relation &r1, NOT_CONST Relation &r2); // Takes set as 2nd -Relation Restrict_Range(NOT_CONST Relation &r1, NOT_CONST Relation &r2); // Takes set as 2nd -Relation Domain(NOT_CONST Relation &r); // Returns set -Relation Range(NOT_CONST Relation &r); // Returns set -Relation Cross_Product(NOT_CONST Relation &A, NOT_CONST Relation &B); // Takes two sets -Relation Inverse(NOT_CONST Relation &r); -Relation After(NOT_CONST Relation &r, int carried_by, int new_output,int dir=1); -Relation Deltas(NOT_CONST Relation &R); // Returns set -Relation Deltas(NOT_CONST Relation &R, int eq_no); // Returns set -Relation DeltasToRelation(NOT_CONST Relation &R, int n_input, int n_output); -Relation Complement(NOT_CONST Relation &r); -Relation Project(NOT_CONST Relation &R, Global_Var_ID v); -Relation Project(NOT_CONST Relation &r, int pos, Var_Kind vkind); -Relation Project(NOT_CONST Relation &S, Variable_ID v); -Relation Project(NOT_CONST Relation &S, Sequence<Variable_ID> &s); -Relation Project_Sym(NOT_CONST Relation &R); -Relation Project_On_Sym(NOT_CONST Relation &R, - NOT_CONST Relation &context = Relation::Null()); -Relation GistSingleConjunct(NOT_CONST Relation &R, NOT_CONST Relation &R2, int effort=0); -Relation Gist(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort=0); -Relation Difference(NOT_CONST Relation &r1, NOT_CONST Relation &r2); -Relation Approximate(NOT_CONST Relation &R, bool strides_allowed = false); -Relation Identity(int n_inp); -Relation Identity(NOT_CONST Relation &r); -bool Must_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); -bool Might_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); -// May is the same as might, just another name -bool May_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); -bool Is_Obvious_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); -Relation Composition(NOT_CONST Relation &F, NOT_CONST Relation &G); -bool prepare_relations_for_composition(Relation &F, Relation &G); -Relation Join(NOT_CONST Relation &G, NOT_CONST Relation &F); -Relation EQs_to_GEQs(NOT_CONST Relation &, bool excludeStrides=false); -Relation Symbolic_Solution(NOT_CONST Relation &S); -Relation Symbolic_Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); -Relation Sample_Solution(NOT_CONST Relation &S); -Relation Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); -Relation Upper_Bound(NOT_CONST Relation &r); -Relation Lower_Bound(NOT_CONST Relation &r); - -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 = -1, int number_output = -1); - -// The followings might retire in the futrue!!! -void MapRel1(Relation &inputRel, - const Mapping &map, - Combine_Type ctype, - int number_input=-1, int number_output=-1, - bool invalidate_resulting_leading_info = true, - bool finalize = true); -Relation MapAndCombineRel2(Relation &R1, Relation &R2, - const Mapping &mapping1, const Mapping &mapping2, - Combine_Type ctype, - int number_input=-1, int number_output=-1); -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); - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/closure.h b/omegalib/omega_lib/include/omega/closure.h deleted file mode 100644 index 67088dd..0000000 --- a/omegalib/omega_lib/include/omega/closure.h +++ /dev/null @@ -1,31 +0,0 @@ -#if ! defined _closure_h -#define _closure_h - -#include <omega/Relation.h> - -namespace omega { - -Relation VennDiagramForm( - Tuple<Relation> &Rs, - NOT_CONST Relation &Context_In); -Relation VennDiagramForm( - NOT_CONST Relation &R_In, - NOT_CONST Relation &Context_In = Relation::Null()); - -// Given a Relation R, returns a relation deltas -// that correspond to the ConicHull of the detlas of R -Relation ConicClosure (NOT_CONST Relation &R); - -Relation TransitiveClosure (NOT_CONST Relation &r, - int maxExpansion = 1, - NOT_CONST Relation &IterationSpace=Relation::Null()); - -/* Tomasz Klimek */ -Relation calculateTransitiveClosure(NOT_CONST Relation &r); - -/* Tomasz Klimek */ -Relation ApproxClosure(NOT_CONST Relation &r); - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/evac.h b/omegalib/omega_lib/include/omega/evac.h deleted file mode 100644 index a561f8c..0000000 --- a/omegalib/omega_lib/include/omega/evac.h +++ /dev/null @@ -1,15 +0,0 @@ -#if defined STUDY_EVACUATIONS - -namespace omega { - -// study the evacuation from one side of C to the other for UFS's of -// arity up to max_arity -extern void study_evacuation(Conjunct *C, which_way dir, int max_arity); - -// study the evacuation from the joined C2's output and C1's input to -// either of the other possible tuples -extern void study_evacuation(Conjunct *C1, Conjunct *C2, int max_arity); - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/farkas.h b/omegalib/omega_lib/include/omega/farkas.h deleted file mode 100644 index e77ed66..0000000 --- a/omegalib/omega_lib/include/omega/farkas.h +++ /dev/null @@ -1,19 +0,0 @@ -#ifndef Already_Included_Affine_Closure -#define Already_Included_Affine_Closure - -#include <omega/Relation.h> - -namespace omega { - -enum Farkas_Type {Basic_Farkas, Decoupled_Farkas, - Linear_Combination_Farkas, Positive_Combination_Farkas, - Affine_Combination_Farkas, Convex_Combination_Farkas }; - -Relation Farkas(NOT_CONST Relation &R, Farkas_Type op, bool early_bailout = false); - -extern coef_t farkasDifficulty; -extern Global_Var_ID coefficient_of_constant_term; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/hull.h b/omegalib/omega_lib/include/omega/hull.h deleted file mode 100644 index 928d0c6..0000000 --- a/omegalib/omega_lib/include/omega/hull.h +++ /dev/null @@ -1,89 +0,0 @@ -#ifndef Already_Included_Hull -#define Already_Included_Hull - -#include <omega/farkas.h> - -namespace omega { - -Relation SimpleHull(const Relation &R, bool allow_stride_constraint = false, bool allow_irregular_constraint = false); -Relation SimpleHull(const std::vector<Relation> &Rs, bool allow_stride_constraint = false, bool allow_irregular_constraint = false); - - -// All of the following first call approximate on R to -// eliminate any wildcards and strides. - -// x in Convex Hull of R -// iff -// exist a_i, y_i s.t. -// x = Sum_i a_i y_i s.t. -// forall i, y_i in R -// forall i, a_i >=0 -// sum_i a_i = 1 -Relation ConvexHull(NOT_CONST Relation &R); - -// DecoupledConvexHull is the same as ConvexHull, -// except that it only finds constraints that involve -// both variables x&y if there is a constraint -// that involves both x&y in one of the conjuncts -// of R. -Relation DecoupledConvexHull(NOT_CONST Relation &R); - -// The affine hull just consists of equality constraints -// but is otherwise the tightest hull on R. -// x in Affine Hull of R -// iff -// exist a_i, y_i s.t. -// x = Sum_i a_i y_i s.t. -// forall i, y_i in R -// sum_i a_i = 1 -Relation AffineHull(NOT_CONST Relation &R); - -// x in Linear Hull of R -// iff -// exist a_i, y_i s.t. -// x = Sum_i a_i y_i s.t. -// forall i, y_i in R -Relation LinearHull(NOT_CONST Relation &R); - -// The conic hull is the tighest cone that contains R -// x in Conic Hull of R. -// iff -// exist a_i, y_i s.t. -// x = Sum_i a_i y_i s.t. -// forall i, y_i in R -// forall i, a_i >=0 -Relation ConicHull(NOT_CONST Relation &R); - -// RectHull includes readily-available constraints from relation -// that can be part of hull, plus rectangular bounds calculated -// from input/output/set variables' range. -Relation RectHull(NOT_CONST Relation &Rel); - -// A constraint is in the result of QuickHull only if it appears in one of -// the relations and is directly implied by a single constraint in each of -// the other relations. -Relation QuickHull(Relation &R); // deprecated -Relation QuickHull(Tuple<Relation> &Rs); // deprecated - -Relation FastTightHull(NOT_CONST Relation &input_R, - NOT_CONST Relation &input_H); -Relation Hull(NOT_CONST Relation &R, - bool stridesAllowed = false, - int effort=1, - NOT_CONST Relation &knownHull = Relation::Null() - ); -Relation Hull(Tuple<Relation> &Rs, - const std::vector<bool> &validMask, - int effort = 1, - bool stridesAllowed = false, - NOT_CONST Relation &knownHull = Relation::Null()); - -// If a union of several conjuncts is a convex, their union -// representaition can be simplified by their convex hull. -Relation ConvexRepresentation(NOT_CONST Relation &R); -Relation CheckForConvexPairs(NOT_CONST Relation &S); // deprecated -Relation CheckForConvexRepresentation(NOT_CONST Relation &R_In); // deprecated - -} - -#endif diff --git a/omegalib/omega_lib/include/omega/omega_core/debugging.h b/omegalib/omega_lib/include/omega/omega_core/debugging.h deleted file mode 100644 index e217ae9..0000000 --- a/omegalib/omega_lib/include/omega/omega_core/debugging.h +++ /dev/null @@ -1,30 +0,0 @@ -#if !defined(Already_included_debugging) -#define Already_included_debugging - -// Debugging flags. Can set any of these. - -#include <stdio.h> -#include <ctype.h> - -namespace omega { - - - -extern int omega_core_debug; -extern int pres_debug; -extern int relation_debug; -extern int closure_presburger_debug; -extern int hull_debug; -extern int farkas_debug; -extern int code_gen_debug; - -enum negation_control { any_negation, one_geq_or_eq, one_geq_or_stride }; -extern negation_control pres_legal_negations; - -#if defined STUDY_EVACUATIONS -extern int evac_debug; -#endif - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/omega_core/oc.h b/omegalib/omega_lib/include/omega/omega_core/oc.h deleted file mode 100644 index e4f5444..0000000 --- a/omegalib/omega_lib/include/omega/omega_core/oc.h +++ /dev/null @@ -1,350 +0,0 @@ -#ifndef Already_Included_OC -#define Already_Included_OC 1 - -#include <stdio.h> -#include <string> -#include <basic/util.h> -#include <omega/omega_core/debugging.h> -#include <basic/Tuple.h> - -namespace omega { - -// Manu:: commented the line below -- fortran bug workaround -//#define maxVars 256 /* original 56, increased by chun */ -#define maxVars 100 - -extern int maxGEQs; -extern int maxEQs; - -// Manu:: commented the lines below -- fortran bug workaround -//const int maxmaxGEQs = 2048; // original 512, increaded by chun -//const int maxmaxEQs = 512; // original 256, increased by chun -const int maxmaxGEQs = 512; -const int maxmaxEQs = 256; - -/* #if ! defined maxmaxGEQs */ -/* #define maxmaxGEQs 2048 /\* original 512, increaded by chun *\/ */ -/* #endif */ -/* #if ! defined maxmaxEQs */ -/* #define maxmaxEQs 512 /\* original 256, increased by chun *\/ */ -/* #endif */ - - -#if 0 -#if ! defined Already_Included_Portable -typedef unsigned char bool; /* what a gross thing to do */ -#endif -#endif - -typedef int EqnKey; - -enum {EQ_BLACK = 0, EQ_RED = 1}; -enum {OC_SOLVE_UNKNOWN = 2, OC_SOLVE_SIMPLIFY = 3}; - -struct eqn { - EqnKey key; - coef_t touched; // see oc_simple.c - int color; - int essential; - int varCount; - coef_t coef[maxVars + 1]; -}; - -// typedef eqn * Eqn; -enum redType {notRed=0, redEQ, redGEQ, redLEQ, redStride}; -enum redCheck {noRed=0, redFalse, redConstraints}; -enum normalizeReturnType {normalize_false, normalize_uncoupled, - normalize_coupled}; - -extern char wildName[200][20]; - -extern FILE *outputFile; /* printProblem writes its output to this file */ -#define doTrace (trace && TRACE) -#define isRed(e) (desiredResult == OC_SOLVE_SIMPLIFY && (e)->color) -// #define eqnncpy(e1,e2,s) {int *p00,*q00,*r00; p00 = (int *)(e1); q00 = (int *)(e2); r00 = &p00[headerWords+1+s]; while(p00 < r00) *p00++ = *q00++; } -// #define eqncpy(e1,e2) eqnncpy(e1,e2,nVars) -// #define eqnnzero(e,s) {int *p00,*r00; p00 = (int *)(e); r00 = &p00[headerWords+1+(s)]; while(p00 < r00) *p00++ = 0;} -// #define eqnzero(e) eqnnzero(e,nVars) - -//void eqnncpy(eqn *dest, eqn *src, int); -//void eqnnzero(eqn *e, int); - -inline void eqnncpy(eqn *dest, eqn *src, int nVars) { - dest->key = src->key; - dest->touched = src->touched; - dest->color = src->color; - dest->essential = src->essential; - dest->varCount = src->varCount; - for (int i = 0; i <= nVars; i++) - dest->coef[i] = src->coef[i]; -} - - -inline void eqnnzero(eqn *e, int nVars) { - e->key = 0; - e->touched = 0; - e->color = EQ_BLACK; - e->essential = 0; - e->varCount = 0; - for (int i = 0; i <= nVars; i++) - e->coef[i] = 0; -} - -extern int mayBeRed; - -#ifdef SPEED -#define TRACE 0 -#define DBUG 0 -#define DEBUG 0 -#else -#define TRACE (omega_core_debug) -#define DBUG (omega_core_debug > 1) -#define DEBUG (omega_core_debug > 2) -#endif - - -class Memory { -public: - int length; - coef_t stride; - redType kind; - coef_t constantTerm; - coef_t coef[maxVars + 1]; - int var[maxVars + 1]; -}; - -/* #define headerWords ((4*sizeof(int) + sizeof(coef_t))/sizeof(int)) */ - -void check_number_EQs(int); -void check_number_GEQs(int); -extern eqn SUBs[]; -extern Memory redMemory[]; - -class Problem { -public: - short nVars, safeVars; - short nEQs, nGEQs,nSUBs,nMemories,allocEQs,allocGEQs; - short varsOfInterest; - bool variablesInitialized; - bool variablesFreed; - short var[maxVars+2]; - short forwardingAddress[maxVars+2]; - // int variableColor[maxVars+2]; - int hashVersion; - const char *(*get_var_name)(unsigned int var, void *args); - void *getVarNameArgs; - eqn *GEQs; - eqn *EQs; - bool isTemporary; - - Problem(int in_eqs=0, int in_geqs=0); - Problem(const Problem &); - ~Problem(); - Problem & operator=(const Problem &); - -/* Allocation parameters and functions */ - - static const int min_alloc,first_alloc_pad; - int padEQs(int oldalloc, int newreq) { - check_number_EQs(newreq); - return min((newreq < 2*oldalloc ? 2*oldalloc : 2*newreq),maxmaxEQs); - } - int padGEQs(int oldalloc, int newreq) { - check_number_GEQs(newreq); - return min((newreq < 2*oldalloc ? 2*oldalloc : 2*newreq),maxmaxGEQs); - } - int padEQs(int newreq) { - check_number_EQs(newreq); - return min(max(newreq+first_alloc_pad,min_alloc), maxmaxEQs); - } - int padGEQs(int newreq) { - check_number_GEQs(newreq); - return min(max(newreq+first_alloc_pad,min_alloc), maxmaxGEQs); - } - - - void zeroVariable(int i); - - void putVariablesInStandardOrder(); - void noteEssential(int onlyWildcards); - int findDifference(int e, int &v1, int &v2); - int chainKill(int color,int onlyWildcards); - - int newGEQ(); - int newEQ(); - int newSUB(){ - return nSUBs++; - } - - - void initializeProblem(); - void initializeVariables() const; - void printProblem(int debug = 1) const; - void printSub(int v) const; - std::string print_sub_to_string(int v) const; - void clearSubs(); - void printRedEquations() const; - int countRedEquations() const; - int countRedGEQs() const; - int countRedEQs() const; - int countRedSUBs() const; - void difficulty(int &numberNZs, coef_t &maxMinAbsCoef, coef_t &sumMinAbsCoef) const; - int prettyPrintProblem() const; - std::string prettyPrintProblemToString() const; - int prettyPrintRedEquations() const; - int simplifyProblem(int verify, int subs, int redundantElimination); - int simplifyProblem(); - int simplifyAndVerifyProblem(); - int simplifyApproximate(bool strides_allowed); - void coalesce(); - void partialElimination(); - void unprotectVariable(int var); - void negateGEQ(int); - void convertEQstoGEQs(bool excludeStrides); - void convertEQtoGEQs(int eq); - void nameWildcard(int i); - void useWildNames(); - void ordered_elimination(int symbolic); - int eliminateRedundant (bool expensive); - void eliminateRed(bool expensive); - void constrainVariableSign(int color, int var, int sign); - void constrainVariableValue(int color, int var, int value); - void query_difference(int v1, int v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed); - int solve(int desiredResult); - std::string print_term_to_string(const eqn *e, int c) const; - void printTerm(const eqn * e, int c) const; - std::string printEqnToString(const eqn * e, int test, int extra) const; - void sprintEqn(char *str, const eqn * e, int is_geq,int extra) const; - void printEqn(const eqn * e, int is_geq, int extra) const; - void printEQ(const eqn *e) const {printEqn(e,0,0); } - std::string print_EQ_to_string(const eqn *e) const {return printEqnToString(e,0,0);} - std::string print_GEQ_to_string(const eqn *e) const {return printEqnToString(e,1,0);} - void printGEQ(const eqn *e) const {printEqn(e,1,0); } - void printGEQextra(const eqn *e) const {printEqn(e,1,1); } - void printSubstitution(int s) const; - void printVars(int debug = 1) const; - void swapVars(int i, int j); - void reverseProtectedVariables(); - redCheck redSimplifyProblem(int effort, int computeGist); - - // calculate value of variable mod integer from set of equations -- by chun 12/14/2006 - coef_t query_variable_mod(int v, coef_t factor, int color=EQ_BLACK, int nModularEQs=0, int nModularVars=0) const; - coef_t query_variable_mod(int v, coef_t factor, int color, int nModularEQs, int nModularVars, Tuple<bool> &working_on) const; // helper function - - int queryVariable(int i, coef_t *lowerBound, coef_t *upperBound); - int query_variable_bounds(int i, coef_t *l, coef_t *u); - void queryCoupledVariable(int i, coef_t *l, coef_t *u, int *couldBeZero, coef_t lowerBound, coef_t upperBound); - int queryVariableSigns(int i, int dd_lt, int dd_eq, int dd_gt, coef_t lowerBound, coef_t upperBound, bool *distKnown, coef_t *dist); - void addingEqualityConstraint(int e); - normalizeReturnType normalize(); - void normalize_ext(); - void cleanoutWildcards(); - void substitute(eqn *sub, int i, coef_t c); - void deleteVariable( int i); - void deleteBlack(); - int addNewProtectedWildcard(); - int addNewUnprotectedWildcard(); - int protectWildcard( int i); - void doMod( coef_t factor, int e, int j); - void freeEliminations( int fv); - int verifyProblem(); - void resurrectSubs(); - int solveEQ(); - int combineToTighten() ; - int quickKill(int onlyWildcards, bool desperate = false); - int expensiveEqualityCheck(); - int expensiveRedKill(); - int expensiveKill(); - int smoothWeirdEquations(); - void quickRedKill(int computeGist); - void chainUnprotect(); - void freeRedEliminations(); - void doElimination( int e, int i); - void analyzeElimination( - int &v, - int &darkConstraints, - int &darkShadowFeasible, - int &unit, - coef_t ¶llelSplinters, - coef_t &disjointSplinters, - coef_t &lbSplinters, - coef_t &ubSplinters, - int ¶llelLB); - int parallelSplinter(int e, int diff, int desiredResult); - int solveGEQ( int desiredResult); - void setInternals(); - void setExternals(); - int reduceProblem(); - void problem_merge(Problem &); - void deleteRed(); - void turnRedBlack(); - void checkGistInvariant() const; - void check() const; - coef_t checkSum() const; - void rememberRedConstraint(eqn *e, redType type, coef_t stride); - void recallRedMemories(); - void simplifyStrideConstraints(); - const char * orgVariable(int i) const { - return ((i == 0) ? // cfront likes this form better - "1" : - ((i < 0) ? - wildName[-i] : - (*get_var_name)(i,getVarNameArgs))); - }; - const char * variable(int i) const { - return orgVariable(var[i]) ; - }; - - void deleteGEQ(int e) { - if (DEBUG) { - fprintf(outputFile,"Deleting %d (last:%d): ",e,nGEQs-1); - printGEQ(&GEQs[e]); - fprintf(outputFile,"\n"); - }; - if (e < nGEQs-1) - eqnncpy (&GEQs[e], &GEQs[nGEQs - 1],(nVars)); - nGEQs--; - }; - void deleteEQ(int e) { - if (DEBUG) { - fprintf(outputFile,"Deleting %d (last:%d): ",e,nEQs-1); - printGEQ(&EQs[e]); - fprintf(outputFile,"\n"); - }; - if (e < nEQs-1) - eqnncpy (&EQs[e], &EQs[nEQs - 1],(nVars)); - nEQs--; - }; - -}; - - - -/* #define UNKNOWN 2 */ -/* #define SIMPLIFY 3 */ -/* #define _red 1 */ -/* #define black 0 */ - - -extern int print_in_code_gen_style; - - -void initializeOmega(void); - - -/* set extra to 0 for normal use */ -int singleVarGEQ(eqn *e); - -void setPrintLevel(int level); - -void printHeader(); - -void setOutputFile(FILE *file); - -extern void check_number_EQs(int nEQs); -extern void check_number_GEQs(int nGEQs); -extern void checkVars(int nVars); - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/omega_core/oc_i.h b/omegalib/omega_lib/include/omega/omega_core/oc_i.h deleted file mode 100644 index 9533a40..0000000 --- a/omegalib/omega_lib/include/omega/omega_core/oc_i.h +++ /dev/null @@ -1,79 +0,0 @@ -#if !defined(Already_included_oc_i) -#define Already_included_oc_i - -#include <basic/util.h> -#include <omega/omega_core/oc.h> -#include <stdlib.h> -#include <assert.h> -#include <string> -#include <vector> - -namespace omega { - -#define maxWildcards 18 - -extern int findingImplicitEqualities; -extern int firstCheckForRedundantEquations; -extern int use_ugly_names; -extern int doItAgain; -extern int newVar; -extern int conservative; -extern FILE *outputFile; /* printProblem writes its output to this file */ -extern int nextWildcard; -extern int trace; -extern int depth; -extern int packing[maxVars]; -extern int headerLevel; -extern int inApproximateMode; -extern int inStridesAllowedMode; -extern int addingOuterEqualities; -extern int outerColor; - -const int keyMult = 31; -const int hashTableSize =5*maxmaxGEQs; -const int maxKeys = 8*maxmaxGEQs; -extern int hashVersion; -extern eqn hashMaster[hashTableSize]; -extern int fastLookup[maxKeys*2]; -extern int nextKey; - -extern int reduceWithSubs; -extern int pleaseNoEqualitiesInSimplifiedProblems; - -#define noProblem ((Problem *) 0) - -extern Problem *originalProblem; -int checkIfSingleVar(eqn *e, int i); -/* Solve e = factor alpha for x_j and substitute */ - -void negateCoefficients(eqn * eqn, int nV); - -extern int omegaInitialized; -extern Problem full_answer, context,redProblem; - -#if defined BRAIN_DAMAGED_FREE -static inline void free(const Problem *p) -{ - free((char *)p); -} -#endif - -#if defined NDEBUG -#define CHECK_FOR_DUPLICATE_VARIABLE_NAMES -#else -#define CHECK_FOR_DUPLICATE_VARIABLE_NAMES \ - { \ - std::vector<std::string> name(nVars); \ - for(int i=1; i<=nVars; i++) { \ - name[i-1] = variable(i); \ - assert(!name[i-1].empty()); \ - for(int j=1; j<i; j++) \ - assert(!(name[i-1] == name[j-1])); \ - } \ - } -#endif - - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/omega_i.h b/omegalib/omega_lib/include/omega/omega_i.h deleted file mode 100644 index e5d9230..0000000 --- a/omegalib/omega_lib/include/omega/omega_i.h +++ /dev/null @@ -1,30 +0,0 @@ -#if ! defined _omega_i_h -#define _omega_i_h 1 - -#include <omega/pres_var.h> - -namespace omega { - -/* #define Assert(c,t) if(!(c)) PresErrAssert(t) */ -/* void PresErrAssert(const char *t); */ - -extern Rel_Body null_rel; - -extern int skip_finalization_check; -// extern int skip_set_checks; - -// Global input and output variable tuples. - -extern Global_Input_Output_Tuple input_vars; -extern Global_Input_Output_Tuple output_vars; -extern Global_Input_Output_Tuple &set_vars; - -} // namespace - -#if ! defined DONT_INCLUDE_TEMPLATE_CODE -// with g++258, everything will need to make Tuple<Relation>, as a -// function taking it as an argument is a friend of lots of classes -#include <omega/Relation.h> -#endif - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_cmpr.h b/omegalib/omega_lib/include/omega/pres_cmpr.h deleted file mode 100644 index fb3e6f0..0000000 --- a/omegalib/omega_lib/include/omega/pres_cmpr.h +++ /dev/null @@ -1,49 +0,0 @@ -#if ! defined _pres_cmpr_h -#define _pres_cmpr_h 1 - -#include <omega/omega_core/oc.h> - -namespace omega { - -// -// Compressed problem: rectangular non-0 cut from the big problem. -// -class Comp_Constraints { -public: - Comp_Constraints(eqn *constrs, int no_constrs, int no_vars); - void UncompressConstr(eqn *constrs, short &pn_constrs); - ~Comp_Constraints(); - bool no_constraints() const - { return n_constrs == 0; } - int n_constraints() const - { return n_constrs; } - -protected: - inline int coef_index(int e, int v) - {return e*(n_vars+1) + v;} - -private: - int n_constrs; - int n_vars; - coef_t *coefs; -}; - -class Comp_Problem { -public: - Comp_Problem(Problem *problem); - Problem *UncompressProblem(); - bool no_constraints() const - { return eqs.no_constraints() && geqs.no_constraints(); } - -private: -/* === data === */ - int _nVars, _safeVars; - const char *(*_get_var_name)(unsigned int var, void *args); - void *_getVarNameArgs; - Comp_Constraints eqs; - Comp_Constraints geqs; -}; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_cnstr.h b/omegalib/omega_lib/include/omega/pres_cnstr.h deleted file mode 100644 index 7b2d98d..0000000 --- a/omegalib/omega_lib/include/omega/pres_cnstr.h +++ /dev/null @@ -1,192 +0,0 @@ -#if ! defined _pres_cnstr_h -#define _pres_cnstr_h 1 - -#include <omega/pres_var.h> -#include <vector> - -namespace omega { - -// -// Constraint handles -// - - - -void copy_constraint(Constraint_Handle H, const Constraint_Handle initial); - -class Constraint_Handle { -public: - Constraint_Handle() {} - virtual ~Constraint_Handle() {} - - void update_coef(Variable_ID, coef_t delta); - void update_const(coef_t delta); - coef_t get_coef(Variable_ID v) const; - coef_t get_const() const; - bool has_wildcards() const; - int max_tuple_pos() const; - int min_tuple_pos() const; - bool is_const(Variable_ID v); - bool is_const_except_for_global(Variable_ID v); - - virtual std::string print_to_string() const; - virtual std::string print_term_to_string() const; - - Variable_ID get_local(const Global_Var_ID G); - Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of); - // not sure that the second one can be used in a meaningful - // way if the conjunct is in multiple relations - - void finalize(); - void multiply(int multiplier); - Rel_Body *relation() const; - - -protected: - Conjunct *c; - eqn **eqns; - int e; - - friend class Constr_Vars_Iter; - friend class Constraint_Iterator; - - Constraint_Handle(Conjunct *, eqn **, int); - -#if defined PROTECTED_DOESNT_WORK - friend class EQ_Handle; - friend class GEQ_Handle; -#endif - - void update_coef_during_simplify(Variable_ID, coef_t delta); - void update_const_during_simplify(coef_t delta); - coef_t get_const_during_simplify() const; - coef_t get_coef_during_simplify(Variable_ID v) const; - - -public: - friend class Conjunct; // assert_leading_info updates coef's - // as does move_UFS_to_input - friend class DNF; // and DNF::make_level_carried_to - - friend void copy_constraint(Constraint_Handle H, - const Constraint_Handle initial); - // copy_constraint does updates and gets at c and e - -}; - -class GEQ_Handle : public Constraint_Handle { -public: - inline GEQ_Handle() {} - - virtual std::string print_to_string() const; - virtual std::string print_term_to_string() const; - bool operator==(const Constraint_Handle &that); - - void negate(); - -private: - friend class Conjunct; - friend class GEQ_Iterator; - - GEQ_Handle(Conjunct *, int); -}; - - -class EQ_Handle : public Constraint_Handle { -public: - inline EQ_Handle() {} - - virtual std::string print_to_string() const; - virtual std::string print_term_to_string() const; - bool operator==(const Constraint_Handle &that); - -private: - friend class Conjunct; - friend class EQ_Iterator; - - EQ_Handle(Conjunct *, int); -}; - - -// -// Conjuct iterators -- for querying resulting DNF. -// -class Constraint_Iterator : public Generator<Constraint_Handle> { -public: - Constraint_Iterator(Conjunct *); - int live() const; - void operator++(int); - void operator++(); - Constraint_Handle operator* (); - Constraint_Handle operator* () const; - -private: - Conjunct *c; - int current,last; - eqn **eqns; -}; - - -class EQ_Iterator : public Generator<EQ_Handle> { -public: - EQ_Iterator(Conjunct *); - int live() const; - void operator++(int); - void operator++(); - EQ_Handle operator* (); - EQ_Handle operator* () const; - -private: - Conjunct *c; - int current, last; -}; - - -class GEQ_Iterator : public Generator<GEQ_Handle> { -public: - GEQ_Iterator(Conjunct *); - int live() const; - void operator++(int); - void operator++(); - GEQ_Handle operator* (); - GEQ_Handle operator* () const; - -private: - Conjunct *c; - int current, last; -}; - - -// -// Variables of constraint iterator. -// -struct Variable_Info { - Variable_ID var; - coef_t coef; - Variable_Info(Variable_ID _var, coef_t _coef) - { var = _var; coef = _coef; } -}; - -class Constr_Vars_Iter : public Generator<Variable_Info> { -public: - Constr_Vars_Iter(const Constraint_Handle &ch, bool _wild_only = false); - int live() const; - void operator++(int); - void operator++(); - Variable_Info operator*() const; - - Variable_ID curr_var() const; - coef_t curr_coef() const; - -private: - eqn **eqns; - int e; - Problem *prob; - Variable_ID_Tuple &vars; - bool wild_only; - int current; -}; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_conj.h b/omegalib/omega_lib/include/omega/pres_conj.h deleted file mode 100644 index ea10a2c..0000000 --- a/omegalib/omega_lib/include/omega/pres_conj.h +++ /dev/null @@ -1,299 +0,0 @@ -#if ! defined _pres_conj_h -#define _pres_conj_h 1 - -#include <limits.h> -#include <omega/pres_decl.h> -#include <omega/pres_logic.h> -#include <omega/pres_cnstr.h> - -namespace omega { - -// -// Conjunct -// -// About variables in Conjunct: -// All varaibles appear in exactly one declaration. -// All variables used in Conjunct are referenced in mappedVars. -// Wildcard variables are referenced both in mappedVars and in myLocals, -// since they are declared in the conjunct. -// All other variables are declared at the levels above. -// Column number is: -// in forwardingAddress in Problem if variablesInitialized is set, -// equal to position of Variable_ID in mappedVars list otherwise. -// - -class Conjunct : public F_Declaration { -public: - Constraint_Iterator constraints(); - Variable_ID_Tuple *variables(); - EQ_Iterator EQs(); - GEQ_Iterator GEQs(); - inline int n_EQs() { return problem->nEQs; } - inline int n_GEQs() { return problem->nGEQs; } - - void promise_that_ub_solutions_exist(Relation &R); - - inline Node_Type node_type() {return Op_Conjunct;} - - inline int is_true() {return problem->nEQs==0 && problem->nGEQs==0 - && exact;} - - void query_difference(Variable_ID v1, Variable_ID v2, - coef_t &lowerBound, coef_t &upperBound, bool &guaranteed); - void query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound); - coef_t query_variable_mod(Variable_ID v, coef_t factor); - bool query_variable_used(Variable_ID v); - - int countNonzeros() const { - int numberNZs; - coef_t maxCoef, SumAbsCoef; - problem->difficulty(numberNZs,maxCoef,SumAbsCoef); - return numberNZs; - } - - void difficulty(int &numberNZs, coef_t &maxCoef, coef_t &SumAbsCoef) const { - problem->difficulty(numberNZs,maxCoef,SumAbsCoef); - } - - int query_guaranteed_leading_0s() { - count_leading_0s(); - return guaranteed_leading_0s; - } - - int query_possible_leading_0s() { - count_leading_0s(); - return possible_leading_0s; - } - - int query_leading_dir() { - count_leading_0s(); - return leading_dir; - } - - void calculate_dimensions(Relation &R, int &ndim_all, int &ndim_domain); - int max_ufs_arity_of_set(); - int max_ufs_arity_of_in(); - int max_ufs_arity_of_out(); - - int rank(); - - ~Conjunct(); - - bool is_unknown() const; - inline bool is_exact() const { return exact;} - inline bool is_inexact() const { return !exact;} - inline void make_inexact() { exact=false;} - - -#if ! defined NDEBUG - void assert_leading_info(); -#else - void assert_leading_info() {} -#endif - - - // PRINTING FUNCTIONS - void print(FILE *output_file); - void prefix_print(FILE *output_file, int debug = 1); - std::string print_to_string(int true_printed); - std::string print_EQ_to_string(eqn *e) { return problem->print_EQ_to_string(e); } - std::string print_GEQ_to_string(eqn *e) { return problem->print_GEQ_to_string(e); } - std::string print_EQ_to_string(int e) - { return problem->print_EQ_to_string(&(problem->EQs[e])); } - std::string print_GEQ_to_string(int e) - { return problem->print_GEQ_to_string(&(problem->GEQs[e])); } - std::string print_term_to_string(eqn *e) { return problem->print_term_to_string(e,1); } - std::string print_EQ_term_to_string(int e) - { return problem->print_term_to_string(&(problem->EQs[e]),1); } - std::string print_GEQ_term_to_string(int e) - { return problem->print_term_to_string(&(problem->GEQs[e]),1); } - std::string print_sub_to_string(int col) { return problem->print_sub_to_string(col); } - -private: - - inline void interpret_unknown_as_true() { exact=true;} - - friend Relation approx_closure(NOT_CONST Relation &r, int n); - - virtual Conjunct *really_conjunct(); - - - // create new constraints with all co-efficients 0 - // These are public in F_And, use them from there. - EQ_Handle add_stride(int step, int preserves_level = 0); - EQ_Handle add_EQ(int preserves_level = 0); - GEQ_Handle add_GEQ(int preserves_level = 0); - EQ_Handle add_EQ(const Constraint_Handle &c, int preserves_level = 0); - GEQ_Handle add_GEQ(const Constraint_Handle &c, int preserves_level = 0); - - friend class GEQ_Handle; - friend class EQ_Handle; - friend class Sub_Handle; - friend class Constraint_Handle; - friend class Constraint_Iterator; - friend class GEQ_Iterator; - friend class EQ_Iterator; - friend class Sub_Iterator; - friend class Constr_Vars_Iter; - - - // FUNCTIONS HAVING TO DO WITH BUILDING FORMULAS/DNFs - bool can_add_child(); - void remap(); - void beautify(); - DNF* DNFize(); - int priority(); - virtual Conjunct *find_available_conjunct(); - void finalize(); - - friend class DNF; - - - - // CREATING CONJUNCTS - Conjunct(); - Conjunct(Conjunct &); - Conjunct(Formula *, Rel_Body *); - - friend class Formula; // add_conjunct (a private function) creates Conjuncts - friend class F_Not; - friend class F_Or; - // class F_And; is a friend below - - - // VARIOUS FUNCTIONS TO CREATE / WORK WITH VARIABLES - Variable_ID declare(Const_String s); - Variable_ID declare(); - Variable_ID declare(Variable_ID v); - - friend const char *get_var_name(unsigned int, void *); - void push_exists(Variable_ID_Tuple &S); - int get_column(Variable_ID); - int find_column(Variable_ID); - int map_to_column(Variable_ID); - void combine_columns(); - void reorder(); - void reorder_for_print(bool reverseOrder=false, - int first_pass_input=0, - int first_pass_output=0, - bool sort=false); - - friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel); - - void localize_var(Variable_ID D); - - - // this creates variables in conjuncts for us: - friend int new_WC(Conjunct *nc, Problem *np); - - - // UFS/LEADING ZEROS STUFF - - void move_UFS_to_input(); - - void count_leading_0s(); - void invalidate_leading_info(int changed = -1); - void enforce_leading_info(int guaranteed, int possible, int dir); - - void reverse_leading_dir_info(); - - - - // CONJUNCT SPECIFIC STUFF - - void rm_color_constrs(); - inline int N_protected() { return problem->safeVars; } - - - void ordered_elimination(int symLen) { problem->ordered_elimination(symLen);} - void convertEQstoGEQs(bool excludeStrides); - - int cost(); - - inline Formula* copy(Formula *parent, Rel_Body *reln) - { return copy_conj_diff_relation(parent,reln); } - Conjunct* copy_conj_diff_relation(Formula *parent, Rel_Body *reln); - inline Conjunct* copy_conj_same_relation() - { return copy_conj_diff_relation(&(parent()), relation()); } - friend void internal_copy_conjunct(Conjunct* to, Conjunct* fr); - friend void copy_constraint(Constraint_Handle H, - const Constraint_Handle initial); - -#if defined STUDY_EVACUATIONS - // The core function of "evac.c" does lots of work with conjuncts: - friend bool check_subseq_n(Conjunct *c, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity, int n, bool allow_offset); - friend void assert_subbed_syms(Conjunct *c); - friend bool check_affine(Conjunct *d, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity); - friend evac study(Conjunct *C, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity); -#endif - - // The relational ops tend to do lots of demented things to Conjuncts: - friend class Rel_Body; - friend_rel_ops; - - // F_And sometimes absorbs conjuncts - friend class F_And; - - // Various DNFize functions also get a the problem: - - friend DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak); - friend class F_Exists; - - // Substitutions are a wrapper around a low-level Problem operation - friend class Substitutions; - - // private functions to call problem functions - int simplifyProblem(); - int simplifyProblem(int verify, int subs, int redundantElimination); - int redSimplifyProblem(int effort, int computeGist); - - friend int simplify_conj(Conjunct* conj, int ver_sim, int elim_red, int color); - friend DNF* negate_conj(Conjunct* conj); - friend Conjunct* merge_conjs(Conjunct* conj1, Conjunct* conj2, - Merge_Action action, Rel_Body *body = 0); - friend void copy_conj_header(Conjunct* to, Conjunct* fr); - - - // === at last, the data === - - Variable_ID_Tuple mappedVars; - - int n_open_constraints; - bool cols_ordered; - bool simplified; - bool verified; - - int guaranteed_leading_0s; // -1 if unknown - int possible_leading_0s; // -1 if unknown - int leading_dir; // 0 if unknown, else +/- 1 - int leading_dir_valid_and_known(); - - bool exact; - - short r_constrs; // are redundant constraints eliminated? - Problem *problem; - - bool is_compressed(); - void compress(); - void uncompress(); - - friend class Comp_Problem; - Comp_Problem *comp_problem; -}; - - -/* === Misc. problem manipulation utilities === */ - -const int CantBeNegated = INT_MAX-10; -const int AvoidNegating = INT_MAX-11; - -void copy_column(Problem *tp, int to_col, - Problem *fp, int fr_col, - int start_EQ, int start_GEQ); -void zero_column(Problem *tp, int to_col, - int start_EQ, int start_GEQ, - int no_EQs, int no_GEQs); - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_decl.h b/omegalib/omega_lib/include/omega/pres_decl.h deleted file mode 100644 index 7fec0bc..0000000 --- a/omegalib/omega_lib/include/omega/pres_decl.h +++ /dev/null @@ -1,55 +0,0 @@ -#if ! defined _pres_decl_h -#define _pres_decl_h 1 - -#include <omega/pres_var.h> -#include <omega/pres_form.h> -#include <basic/Section.h> - -namespace omega { - -// -// Base class for presburger formula nodes with variables -// - -class F_Declaration : public Formula { -public: - virtual Variable_ID declare(Const_String s)=0; - virtual Variable_ID declare()=0; - virtual Variable_ID declare(Variable_ID)=0; - virtual Section<Variable_ID> declare_tuple(int size); - - void finalize(); - - inline Variable_ID_Tuple &locals() {return myLocals;} - -protected: - F_Declaration(Formula *, Rel_Body *); - F_Declaration(Formula *, Rel_Body *, Variable_ID_Tuple &); - ~F_Declaration(); - - Variable_ID do_declare(Const_String s, Var_Kind var_kind); - - void prefix_print(FILE *output_file, int debug = 1); - void print(FILE *output_file); - - void setup_names(); - void setup_anonymous_wildcard_names(); - - Variable_ID_Tuple myLocals; - friend class F_Forall; // rearrange needs to access myLocals - friend class F_Or; // push_exists - -private: - virtual bool can_add_child(); - - int priority(); - - friend 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); -}; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_dnf.h b/omegalib/omega_lib/include/omega/pres_dnf.h deleted file mode 100644 index 93d5942..0000000 --- a/omegalib/omega_lib/include/omega/pres_dnf.h +++ /dev/null @@ -1,87 +0,0 @@ -#if ! defined _pres_dnf_h -#define _pres_dnf_h 1 - -#include <omega/pres_gen.h> - -namespace omega { - -// -// Disjunctive Normal Form -- list of Conjuncts -// -class DNF { -public: - void print(FILE *out_file); - void prefix_print(FILE *out_file, int debug = 1, bool parent_names_setup=false); - - bool is_definitely_false() const; - bool is_definitely_true() const; - int length() const; - - Conjunct *single_conjunct() const; - bool has_single_conjunct() const; - Conjunct *rm_first_conjunct(); - void clear(); - int query_guaranteed_leading_0s(int what_to_return_for_empty_dnf); - int query_possible_leading_0s(int what_to_return_for_empty_dnf); - int query_leading_dir(); - -private: - // all DNFize functions need to access the dnf builders: - friend class F_And; - friend class F_Or; - friend class Conjunct; - friend DNF * negate_conj(Conjunct *); - - friend class Rel_Body; - friend_rel_ops; - - DNF(); - ~DNF(); - - DNF* copy(Rel_Body *); - - void simplify(); - void make_level_carried_to(int level); - void count_leading_0s(); - - void add_conjunct(Conjunct*); - void join_DNF(DNF*); - void rm_conjunct(Conjunct *c); - - void rm_redundant_conjs(int effort); - void rm_redundant_inexact_conjs(); - void DNF_to_formula(Formula* root); - - - friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel); - void remap(); - - void setup_names(); - - void remove_inexact_conj(); - - // These may need to get at the conjList itself: - friend DNF* DNF_and_DNF(DNF*, DNF*); - friend DNF* DNF_and_conj(DNF*, Conjunct*); - friend DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak); - - friend class DNF_Iterator; - - List<Conjunct*> conjList; -}; - -DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak=false); - -// -// DNF iterator -// -class DNF_Iterator : public List_Iterator<Conjunct*> { -public: - DNF_Iterator(DNF*dnf) : List_Iterator<Conjunct*>(dnf->conjList) {} - DNF_Iterator() {} - void curr_set(Conjunct *c) { *(*this) = c; } -}; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_form.h b/omegalib/omega_lib/include/omega/pres_form.h deleted file mode 100644 index ed3258e..0000000 --- a/omegalib/omega_lib/include/omega/pres_form.h +++ /dev/null @@ -1,112 +0,0 @@ -#if ! defined _pres_form_h -#define _pres_form_h 1 - -#include <omega/pres_gen.h> - -namespace omega { - -typedef enum {Op_Relation, Op_Not, Op_And, Op_Or, - Op_Conjunct, Op_Forall, Op_Exists} Node_Type; - - -// -// Presburger Formula base class -// - -class Formula { -public: - virtual Node_Type node_type()=0; - - F_Forall *add_forall(); - F_Exists *add_exists(); - virtual F_And *and_with(); - F_And *add_and(); - F_Or *add_or(); - F_Not *add_not(); - void add_unknown(); - - virtual void finalize(); - virtual void print(FILE *output_file); - - Rel_Body *relation() { return myRelation; } - -protected: - virtual ~Formula(); -private: - Formula(Formula *, Rel_Body *); - - // The relational operations need to work with formula trees - friend class Relation; - friend_rel_ops; - // as do the functions that build DNF's - friend class DNF; - // or other parts of the tree - friend class Conjunct; - friend class F_Declaration; - friend class F_Exists; - friend class F_Forall; - friend class F_Or; - friend class F_And; - friend class F_Not; - friend class Rel_Body; - - - // Operations needed for manipulation of formula trees: - - void remove_child(Formula *); - void replace_child(Formula *child, Formula *new_child); - virtual bool can_add_child(); - void add_child(Formula *); - - Conjunct *add_conjunct(); - virtual Conjunct *find_available_conjunct() = 0; - - virtual Formula *copy(Formula *parent, Rel_Body *reln); - F_Exists *add_exists(Variable_ID_Tuple &S); - virtual void push_exists(Variable_ID_Tuple &S); - - // Accessor functions for tree building - - List<Formula*> &children() {return myChildren;} - int n_children() const {return myChildren.length();} - const List<Formula*> &get_children() const {return myChildren;} - Formula &parent() {return *myParent;} - void set_parent(Formula *p) {myParent = p;} - - - virtual int priority(); - - void verify_tree(); // should be const, but iterators are used - - virtual void reverse_leading_dir_info(); - virtual void invalidate_leading_info(int changed = -1); - virtual void enforce_leading_info(int guaranteed, int possible, int dir); - - virtual void remap(); - virtual DNF* DNFize() = 0; - virtual void beautify(); - virtual void rearrange(); - virtual void setup_names(); - - virtual void print_separator(FILE *output_file); - virtual void combine_columns(); - virtual void prefix_print(FILE *output_file, int debug = 1); - void print_head(FILE *output_file); - - void set_relation(Rel_Body *r); - void set_parent(Formula *parent, Rel_Body *reln); - - void assert_not_finalized(); - - virtual Conjunct *really_conjunct(); // until we get RTTI - -private: - List<Formula*> myChildren; - Formula *myParent; - Rel_Body *myRelation; - -}; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_gen.h b/omegalib/omega_lib/include/omega/pres_gen.h deleted file mode 100644 index ba6a793..0000000 --- a/omegalib/omega_lib/include/omega/pres_gen.h +++ /dev/null @@ -1,192 +0,0 @@ -#if ! defined _pres_gen_h -#define _pres_gen_h 1 - -#include <omega/omega_core/oc.h> -#include <basic/ConstString.h> -#include <basic/Iterator.h> -#include <basic/List.h> -#include <basic/Tuple.h> -#include <assert.h> -#include <stdlib.h> - -namespace omega { - -// -// general presburger stuff thats needed everywhere -// - -/* The following allows us to avoid warnings about passing - temporaries as non-const references. This is useful but - has suddenly become illegal. */ - -#if !defined(LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY) -#if defined(__GNUC__) && (__GNUC__ > 2 || (__GNUC__ == 2 && __GNUC_MINOR__ >= 7)) -#define LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY 1 -#else -#define LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY 0 -#endif -#endif - -#if LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY -#define NOT_CONST const -#else -#define NOT_CONST -#endif - -// -// I/O and error processing and control flags (also in omega_core/debugging.h) -// - -extern FILE *DebugFile; -extern int pres_debug; - -extern int mega_total; -extern int use_ugly_names; - -extern negation_control pres_legal_negations; - - -// -// Lots of things refer to each other, -// so we forward declare these classes: -// - -class Var_Decl; -typedef enum {Input_Var, Set_Var = Input_Var, Output_Var, - Global_Var, Forall_Var, Exists_Var, Wildcard_Var} Var_Kind; -class Global_Var_Decl; -typedef enum {Unknown_Tuple = 0, Input_Tuple = 1, Output_Tuple = 2, - Set_Tuple = Input_Tuple } Argument_Tuple; - -class Constraint_Handle; -class EQ_Handle; -class GEQ_Handle; -typedef EQ_Handle Stride_Handle; - -class Formula; -class F_Declaration; -class F_Forall; -class F_Exists; -class F_And; -class F_Or; -class F_Not; -class Conjunct; -class Relation; -class Rel_Body; -class DNF; -class Mapping; -class Omega_Var; -class Coef_Var_Decl; - -typedef Var_Decl *Variable_ID; -typedef Global_Var_Decl *Global_Var_ID; - -typedef Tuple<Variable_ID> Variable_ID_Tuple; -typedef Sequence<Variable_ID> Variable_ID_Sequence; // use only for rvalues -typedef Tuple_Iterator<Variable_ID> Variable_ID_Tuple_Iterator; -typedef Tuple_Iterator<Variable_ID> Variable_ID_Iterator; - -typedef Variable_ID_Iterator Variable_Iterator; - -typedef enum {Comb_Id, Comb_And, Comb_Or, Comb_AndNot} Combine_Type; - - -// things that are (hopefully) used only privately -class Comp_Problem; -class Comp_Constraints; - -// this has to be here rather than in pres_conj.h because -// MergeConj has to be a friend of Constraint_Handle -typedef enum {MERGE_REGULAR, MERGE_COMPOSE, MERGE_GIST} Merge_Action; - - -// Conjunct can be exact or lower or upper bound. -// For lower bound conjunct, the upper bound is assumed to be true; -// For upper bound conjunct, the lower bound is assumed to be false - -typedef enum {EXACT_BOUND, UPPER_BOUND, LOWER_BOUND, UNSET_BOUND} Bound_Type; - - -#if defined STUDY_EVACUATIONS -typedef enum { in_to_out = 0, out_to_in = 1} which_way; - -enum evac { evac_trivial = 0, - evac_offset = 1, - evac_subseq = 2, - evac_offset_subseq = 3, -// evac_permutation = , - evac_affine = 4, - evac_nasty = 5 }; - -extern char *evac_names[]; - -#endif - -// the following list should be updated in sync with Relations.h - -#define friend_rel_ops \ -friend Relation Union(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend Relation Intersection(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend Relation After(NOT_CONST Relation &R, int carried_by, int new_output, int dir);\ -friend Relation Extend_Domain(NOT_CONST Relation &R); \ -friend Relation Extend_Domain(NOT_CONST Relation &R, int more); \ -friend Relation Extend_Range(NOT_CONST Relation &R); \ -friend Relation Extend_Range(NOT_CONST Relation &R, int more); \ -friend Relation Extend_Set(NOT_CONST Relation &R); \ -friend Relation Extend_Set(NOT_CONST Relation &R, int more); \ -friend Relation Restrict_Domain(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend Relation Restrict_Range(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend Relation Domain(NOT_CONST Relation &r); \ -friend Relation Range(NOT_CONST Relation &r); \ -friend Relation Cross_Product(NOT_CONST Relation &A, NOT_CONST Relation &B); \ -friend Relation Inverse(NOT_CONST Relation &r); \ -friend Relation Deltas(NOT_CONST Relation &R); \ -friend Relation Deltas(NOT_CONST Relation &R, int eq_no); \ -friend Relation DeltasToRelation(NOT_CONST Relation &R, int n_input, int n_output); \ -friend Relation Complement(NOT_CONST Relation &r); \ -friend Relation Project(NOT_CONST Relation &R, Global_Var_ID v); \ -friend Relation Project(NOT_CONST Relation &r, int pos, Var_Kind vkind); \ -friend Relation Project(NOT_CONST Relation &S, Sequence<Variable_ID> &s); \ -friend Relation Project_Sym(NOT_CONST Relation &R); \ -friend Relation Project_On_Sym(NOT_CONST Relation &R, NOT_CONST Relation &context); \ -friend Relation GistSingleConjunct(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort); \ -friend Relation Gist(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort); \ -friend Relation Difference(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend Relation Approximate(NOT_CONST Relation &R, bool strides_allowed); \ -friend Relation Identity(int n_inp); \ -friend Relation Identity(NOT_CONST Relation &r); \ -friend bool do_subset_check(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend bool Must_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend bool Might_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend bool May_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend bool Is_Obvious_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ -friend Relation Join(NOT_CONST Relation &G, NOT_CONST Relation &F); \ -friend Relation Composition(NOT_CONST Relation &F, NOT_CONST Relation &G); \ -friend bool can_do_exact_composition(NOT_CONST Relation &F, NOT_CONST Relation &G); \ -friend Relation EQs_to_GEQs(NOT_CONST Relation &, bool excludeStrides); \ -friend Relation Symbolic_Solution(NOT_CONST Relation &S); \ -friend Relation Symbolic_Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); \ -friend Relation Sample_Solution(NOT_CONST Relation &S); \ -friend Relation Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); \ -friend void MapRel1(Relation &inputRel, const Mapping &map, \ - Combine_Type ctype, int number_input, \ - int number_output, bool, bool); \ -friend Relation MapAndCombineRel2(Relation &R1, Relation &R2, \ - const Mapping &mapping1, \ - const Mapping &mapping2, \ - Combine_Type ctype, \ - int number_input, \ - int number_output); \ -friend void align(Rel_Body *, Rel_Body *, F_Exists *, \ - Formula *, const Mapping &, bool &, \ - List<int> &, Variable_ID_Tuple &); \ -friend Relation Lower_Bound(NOT_CONST Relation &r); \ -friend Relation Upper_Bound(NOT_CONST Relation &r) - - -// REMEMBER - THE LAST LINE OF THE MACRO SHOULD NOT HAVE A ; -/* TransitiveClosure doesn't need to be in friend_rel_ops */ - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_logic.h b/omegalib/omega_lib/include/omega/pres_logic.h deleted file mode 100644 index 27c4553..0000000 --- a/omegalib/omega_lib/include/omega/pres_logic.h +++ /dev/null @@ -1,90 +0,0 @@ -#if ! defined _pres_logic_h -#define _pres_logic_h 1 - -#include <omega/pres_form.h> - -namespace omega { -// -// Presburger formula classes for logical operations: and, or not -// - -class F_And : public Formula { -public: - inline Node_Type node_type() {return Op_And;} - - // "preserves level" should be 0 unless we know this will not - // change the "level" of the constraints - ie the number of - // leading corresponding in,out variables known to be equal - GEQ_Handle add_GEQ(int preserves_level = 0); - EQ_Handle add_EQ(int preserves_level = 0); - Stride_Handle add_stride(int step, int preserves_level = 0); - EQ_Handle add_EQ(const Constraint_Handle &c, int preserves_level = 0); - GEQ_Handle add_GEQ(const Constraint_Handle &c, int preserves_level = 0); - - F_And *and_with(); - void add_unknown(); - -private: - friend class Formula; // add_and() - F_And(Formula *p, Rel_Body *r); - -private: - Formula *copy(Formula *parent, Rel_Body *reln); - virtual Conjunct *find_available_conjunct(); - int priority(); - void print_separator(FILE *output_file); - void prefix_print(FILE *output_file, int debug = 1); - void beautify(); - DNF* DNFize(); - - Conjunct *pos_conj; -}; - - -class F_Or : public Formula { -public: - inline Node_Type node_type() {return Op_Or;} - -private: - friend class Formula; // add_or - F_Or(Formula *, Rel_Body *); - -private: - Formula *copy(Formula *parent, Rel_Body *reln); - - virtual Conjunct *find_available_conjunct(); - void print_separator(FILE *output_file); - void prefix_print(FILE *output_file, int debug = 1); - void beautify(); - int priority(); - DNF* DNFize(); - void push_exists(Variable_ID_Tuple &S); -}; - - -class F_Not : public Formula { -public: - inline Node_Type node_type() {return Op_Not;} - void finalize(); - -private: - friend class Formula; - F_Not(Formula *, Rel_Body *); - -private: - Formula *copy(Formula *parent, Rel_Body *reln); - - virtual Conjunct *find_available_conjunct(); - friend class F_Forall; - bool can_add_child(); - void beautify(); - void rearrange(); - int priority(); - DNF* DNFize(); - void print(FILE *output_file); - void prefix_print(FILE *output_file, int debug = 1); -}; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_quant.h b/omegalib/omega_lib/include/omega/pres_quant.h deleted file mode 100644 index 98c30df..0000000 --- a/omegalib/omega_lib/include/omega/pres_quant.h +++ /dev/null @@ -1,63 +0,0 @@ -#if ! defined _pres_quant_h -#define _pres_quant_h 1 - -#include <omega/pres_decl.h> - -namespace omega { - -// -// Presburger formula nodes for quantifiers -// - -class F_Exists : public F_Declaration { -public: - inline Node_Type node_type() {return Op_Exists;} - Variable_ID declare(Const_String s); - Variable_ID declare(); - Variable_ID declare(Variable_ID v); - virtual void push_exists(Variable_ID_Tuple &S); - -protected: - friend class Formula; - - F_Exists(Formula *, Rel_Body *); - F_Exists(Formula *, Rel_Body *, Variable_ID_Tuple &); - -private: - Formula *copy(Formula *parent, Rel_Body *reln); - - virtual Conjunct *find_available_conjunct(); - void print(FILE *output_file); - void prefix_print(FILE *output_file, int debug = 1); - void beautify(); - void rearrange(); - DNF* DNFize(); -}; - - -class F_Forall : public F_Declaration { -public: - inline Node_Type node_type() {return Op_Forall;} - Variable_ID declare(Const_String s); - Variable_ID declare(); - Variable_ID declare(Variable_ID v); - -protected: - friend class Formula; - - F_Forall(Formula *, Rel_Body *); - -private: - Formula *copy(Formula *parent, Rel_Body *reln); - - virtual Conjunct *find_available_conjunct(); - void print(FILE *output_file); - void prefix_print(FILE *output_file, int debug = 1); - void beautify(); - void rearrange(); - DNF* DNFize(); -}; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_subs.h b/omegalib/omega_lib/include/omega/pres_subs.h deleted file mode 100644 index 8a9ee92..0000000 --- a/omegalib/omega_lib/include/omega/pres_subs.h +++ /dev/null @@ -1,88 +0,0 @@ -#if !defined(pres_subs_h) -#define pres_subs_h - -/* Interface to omega core's substitutions. - - Creating an object of class Substitutions causes ordered elimination, - i.e. variables in the input and output tuples are substituted for by - functions of earlier variables. Could conceivablely create a more - flexible interface to orderedElimination if we developed a way to - specify the desired variable order. - - This is not an entirely consistent interface, since Sub_Handles - shouldn't really permit update_coef on SUBs. It is not a real - problem since subs are now no longer part of a conjunct, but it is - a slightly odd situation. - - Don't try to simplify r after performing orderedElimination. -*/ - - -#include <omega/pres_gen.h> -#include <omega/Relation.h> -#include <omega/pres_conj.h> -#include <omega/pres_cnstr.h> - -namespace omega { - -class Sub_Handle; -class Sub_Iterator; - -class Substitutions { -public: - Substitutions(Relation &input_R, Conjunct *input_c); - ~Substitutions(); - Sub_Handle get_sub(Variable_ID v); - bool substituted(Variable_ID v); - bool sub_involves(Variable_ID v, Var_Kind kind); -private: - friend class Sub_Iterator; - friend class Sub_Handle; - Relation *r; - Conjunct *c; - eqn *subs; - Variable_ID_Tuple subbed_vars; -}; - - -//:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: - - -class Sub_Handle: public Constraint_Handle { -public: - inline Sub_Handle() {} - - virtual std::string print_to_string() const; - virtual std::string print_term_to_string() const; - Variable_ID variable() {return v;} - -private: - friend class Substitutions; - friend class Sub_Iterator; - Sub_Handle(Substitutions *, int, Variable_ID); -// Sub_Handle(Substitutions *, int); - - Variable_ID v; -}; - -//:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: - - -class Sub_Iterator : public Generator<Sub_Handle> { -public: - Sub_Iterator(Substitutions *input_s): s(input_s), current(0), - last(s->c->problem->nSUBs-1) {} - int live() const; - void operator++(int); - void operator++(); - Sub_Handle operator* (); - Sub_Handle operator* () const; - -private: - Substitutions *s; - int current, last; -}; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_tree.h b/omegalib/omega_lib/include/omega/pres_tree.h deleted file mode 100644 index ad78ad0..0000000 --- a/omegalib/omega_lib/include/omega/pres_tree.h +++ /dev/null @@ -1,15 +0,0 @@ -#if ! defined _pres_tree_h -#define _pres_tree_h 1 - -// -// Header to include if you need all the classes to build -// a Presburger formula: -// variables, constraints, nodes for logical operations & quantifiers -// - -#include <omega/pres_var.h> -#include <omega/pres_cnstr.h> -#include <omega/pres_logic.h> -#include <omega/pres_quant.h> - -#endif diff --git a/omegalib/omega_lib/include/omega/pres_var.h b/omegalib/omega_lib/include/omega/pres_var.h deleted file mode 100644 index bf60dcb..0000000 --- a/omegalib/omega_lib/include/omega/pres_var.h +++ /dev/null @@ -1,230 +0,0 @@ -#if ! defined _pres_var_h -#define _pres_var_h 1 - -#include <omega/pres_gen.h> -#include <map> - -namespace omega { - -// -// Variable declaration. -// Variables are free or quantified. -// Free variables are classified as input, output and global. -// Quantified variables are classified as forall, exists and wildcard. -// All global variables are functions symbols of (possibly 0) arguments -// Local variables that correspond to >0-ary functions are identified -// as functions of a prefix of the input, output, or both tuples -// -// -// typedef enum {Input_Var, Output_Var, Set_Var, -// Global_Var, Forall_Var, Exists_Var, Wildcard_Var} Var_Kind; - -typedef enum {Free_Var, Coef_Var, Bomega_Var} Global_Kind; - -// NOW IN PRES_GEN.H, as its used as an argument and can't -// be forward declared: -// typedef enum {Unknown_Tuple = 0, Input_Tuple = 1, Output_Tuple = 2, -// Set_Tuple = Input_Tuple } Argument_Tuple; -// Only Input, Output, and Set can be passed to get_local, -// but the values 0 and 3 are also used internally. - - -class Var_Decl { -public: - inline Var_Kind kind() { return var_kind; } - int get_position(); - Global_Var_ID get_global_var(); - Argument_Tuple function_of(); // valid iff kind() == Global_var - - Const_String base_name; - void name_variable(char *newname); - - // The following should be used with care, as they are only valid - // after setup_names has been used on the relation containing this - // variable. - std::string name(); - const char* char_name(); - void set_kind(Var_Kind v) { var_kind = v; } - - // Operation to allow the remap field to be used for - // union-find operations on variables. - // Be sure to reset the remap fields afterward - void UF_union(Variable_ID v); - Variable_ID UF_owner(); - -private: - Var_Decl(Const_String name, Var_Kind vkind, int pos); - Var_Decl(Var_Kind vkind, int pos); - Var_Decl(Variable_ID v); - Var_Decl(Const_String name, Global_Var_ID v); - Var_Decl(Const_String name, Global_Var_ID v, Argument_Tuple function_of); - - friend class F_Declaration; // creates local variables - friend class Global_Var_Decl; // its constructors create Var_Decls. - - friend class Global_Input_Output_Tuple; - friend void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl); - -private: - int instance; - void setup_name(); - - // these set up the names - friend class Rel_Body; -// friend class F_Declaration; already a friend - -private: - Variable_ID remap; // pointer to new copy of this node - - // lots of things need to get at "remap" - lots of relation ops, - // and functions that move UFS's around: - // dnf::make_level_carried_to and Conjunct::move_UFS_to_input() - // Also of course Conjunct::remap and push_exists - friend_rel_ops; - friend class DNF; - friend class Conjunct; - - // this prints remap to the debugging output - friend void print_var_addrs(std::string &s, Variable_ID v); - - friend void reset_remap_field(Variable_ID v); - friend void reset_remap_field(Sequence<Variable_ID> &S); - friend void reset_remap_field(Sequence<Variable_ID> &S, int var_no); - friend void reset_remap_field(Variable_ID_Tuple &S); - friend void reset_remap_field(Variable_ID_Tuple &S, int var_no); - -private: - - Var_Kind var_kind; - int position; // only for Input_Var, Output_Var - Global_Var_ID global_var; // only for Global_Var - Argument_Tuple of; // only for Global_Var -}; - -bool rm_variable(Variable_ID_Tuple &vl, Variable_ID v); -void reset_remap_field(Sequence<Variable_ID> &S); -void reset_remap_field(Sequence<Variable_ID> &S, int var_no); -void reset_remap_field(Variable_ID v); -void reset_remap_field(Variable_ID_Tuple &S); -void reset_remap_field(Variable_ID_Tuple &S, int var_no); - -class Global_Input_Output_Tuple: public Tuple<Variable_ID> { -public: - Global_Input_Output_Tuple(Var_Kind in_my_kind, int init=-1); - ~Global_Input_Output_Tuple(); - virtual Variable_ID &operator[](int index); - virtual const Variable_ID &operator[](int index) const; -private: - Var_Kind my_kind; - static const int initial_allocation; -}; - -extern Global_Input_Output_Tuple input_vars; -extern Global_Input_Output_Tuple output_vars; -// This allows the user to refer to set_vars to query sets, w/o knowing -// they are really inputs. -extern Global_Input_Output_Tuple &set_vars; - -Variable_ID input_var(int nth); -Variable_ID output_var(int nth); -Variable_ID set_var(int nth); - - - -// -// Global_Var_ID uniquely identifies global var-s through the whole program. -// Global_Var_Decl is an ADT with the following operations: -// - create global variable, -// - find the arity of the variable, (default = 0, for symbolic consts) -// - get the name of global variable, -// - tell if two variables are the same (if they are the same object) -// - -class Global_Var_Decl { -public: - Global_Var_Decl(Const_String baseName); - - virtual Const_String base_name() const - { - return loc_rep1.base_name; - } - - virtual void set_base_name(Const_String newName) - { - loc_rep1.base_name = newName; - loc_rep2.base_name = newName; - } - - virtual int arity() const - { - return 0; // default compatible with old symbolic constant stuff - } - - virtual Omega_Var *really_omega_var(); // until we get RTTI in C++ - virtual Coef_Var_Decl *really_coef_var(); // until we get RTTI in C++ - virtual Global_Kind kind() const; - -private: - - friend class Rel_Body; // Rel_Body::get_local calls this get_local - - Variable_ID get_local() - { - assert(arity() == 0); - return &loc_rep1; - } - Variable_ID get_local(Argument_Tuple of) - { - assert(arity() == 0 || of == Input_Tuple || of == Output_Tuple); - return ((arity() == 0 || of == Input_Tuple) ? &loc_rep1 : &loc_rep2); - } - - // local representative, there is just 1 for every 0-ary global variable - Var_Decl loc_rep1; // arity == 0, or arity > 0 and of == In - Var_Decl loc_rep2; // arity > 0 and of == Out - -public: -// friend class Rel_Body; // Rel_Body::setup_names sets instance - friend class Var_Decl; - int instance; -}; - - -class Coef_Var_Decl : public Global_Var_Decl { -public: - Coef_Var_Decl(int id, int var); - int stmt() const; - int var() const; - virtual Global_Kind kind() const; - virtual Coef_Var_Decl *really_coef_var(); // until we get RTTI in C++ - -private: - int i, v; -}; - - - -// -// Test subclass for Global_Var: named global variable -// -class Free_Var_Decl : public Global_Var_Decl { -public: - Free_Var_Decl(Const_String name); - Free_Var_Decl(Const_String name, int arity); - int arity() const; - virtual Global_Kind kind() const; - -private: - int _arity; -}; - - -/* === implementation functions === */ -void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl); -void free_var_decls(Variable_ID_Tuple &vl); - -extern int wildCardInstanceNumber; - -} // namespace - -#endif diff --git a/omegalib/omega_lib/include/omega/reach.h b/omegalib/omega_lib/include/omega/reach.h deleted file mode 100644 index ff4bf79..0000000 --- a/omegalib/omega_lib/include/omega/reach.h +++ /dev/null @@ -1,23 +0,0 @@ -#if ! defined _reach_h -#define _reach_h 1 - -namespace omega { - -class reachable_information { -public: - Tuple<std::string> node_names; - Tuple<int> node_arity; - Dynamic_Array1<Relation> start_nodes; - Dynamic_Array2<Relation> transitions; -}; - - -Dynamic_Array1<Relation> * -Reachable_Nodes(reachable_information * reachable_info); - -Dynamic_Array1<Relation> * -I_Reachable_Nodes(reachable_information * reachable_info); - -} // namespace - -#endif |