diff options
Diffstat (limited to 'omegalib/omega_lib/include/omega/Relation.h')
| -rw-r--r-- | omegalib/omega_lib/include/omega/Relation.h | 299 |
1 files changed, 299 insertions, 0 deletions
diff --git a/omegalib/omega_lib/include/omega/Relation.h b/omegalib/omega_lib/include/omega/Relation.h new file mode 100644 index 0000000..b41bef5 --- /dev/null +++ b/omegalib/omega_lib/include/omega/Relation.h @@ -0,0 +1,299 @@ +#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 |