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