From 75ff98e4d65862ff5b36b533b4f6e3ea71ede1d5 Mon Sep 17 00:00:00 2001 From: Tuowen Zhao Date: Sat, 17 Sep 2016 03:22:53 +0000 Subject: cmake build --- omegalib/omega_lib/include/omega/pres_logic.h | 90 +++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 omegalib/omega_lib/include/omega/pres_logic.h (limited to 'omegalib/omega_lib/include/omega/pres_logic.h') diff --git a/omegalib/omega_lib/include/omega/pres_logic.h b/omegalib/omega_lib/include/omega/pres_logic.h new file mode 100644 index 0000000..27c4553 --- /dev/null +++ b/omegalib/omega_lib/include/omega/pres_logic.h @@ -0,0 +1,90 @@ +#if ! defined _pres_logic_h +#define _pres_logic_h 1 + +#include + +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 -- cgit v1.2.3-70-g09d2