diff options
author | Tuowen Zhao <ztuowen@gmail.com> | 2016-09-18 15:45:13 +0000 |
---|---|---|
committer | Tuowen Zhao <ztuowen@gmail.com> | 2016-09-18 15:45:13 +0000 |
commit | 2fce43d484e4148ae858f410d51dcd9951d34374 (patch) | |
tree | 80c204799cd38349b3bb209d4d37962b11aa6222 /omegalib/omega_lib/include/omega/Relation.h | |
parent | f433eae7a1408cca20f3b72fb4c136d9b62de3b8 (diff) | |
download | chill-2fce43d484e4148ae858f410d51dcd9951d34374.tar.gz chill-2fce43d484e4148ae858f410d51dcd9951d34374.tar.bz2 chill-2fce43d484e4148ae858f410d51dcd9951d34374.zip |
remove include & rename
Diffstat (limited to 'omegalib/omega_lib/include/omega/Relation.h')
-rw-r--r-- | omegalib/omega_lib/include/omega/Relation.h | 299 |
1 files changed, 0 insertions, 299 deletions
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 |