summaryrefslogtreecommitdiff
path: root/omegalib/omega_lib/include/omega/Relation.h
diff options
context:
space:
mode:
authorTuowen Zhao <ztuowen@gmail.com>2016-09-18 15:45:13 +0000
committerTuowen Zhao <ztuowen@gmail.com>2016-09-18 15:45:13 +0000
commit2fce43d484e4148ae858f410d51dcd9951d34374 (patch)
tree80c204799cd38349b3bb209d4d37962b11aa6222 /omegalib/omega_lib/include/omega/Relation.h
parentf433eae7a1408cca20f3b72fb4c136d9b62de3b8 (diff)
downloadchill-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.h299
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