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_decl.h | 55 ++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 omegalib/omega_lib/include/omega/pres_decl.h (limited to 'omegalib/omega_lib/include/omega/pres_decl.h') diff --git a/omegalib/omega_lib/include/omega/pres_decl.h b/omegalib/omega_lib/include/omega/pres_decl.h new file mode 100644 index 0000000..7fec0bc --- /dev/null +++ b/omegalib/omega_lib/include/omega/pres_decl.h @@ -0,0 +1,55 @@ +#if ! defined _pres_decl_h +#define _pres_decl_h 1 + +#include +#include +#include + +namespace omega { + +// +// Base class for presburger formula nodes with variables +// + +class F_Declaration : public Formula { +public: + virtual Variable_ID declare(Const_String s)=0; + virtual Variable_ID declare()=0; + virtual Variable_ID declare(Variable_ID)=0; + virtual Section declare_tuple(int size); + + void finalize(); + + inline Variable_ID_Tuple &locals() {return myLocals;} + +protected: + F_Declaration(Formula *, Rel_Body *); + F_Declaration(Formula *, Rel_Body *, Variable_ID_Tuple &); + ~F_Declaration(); + + Variable_ID do_declare(Const_String s, Var_Kind var_kind); + + void prefix_print(FILE *output_file, int debug = 1); + void print(FILE *output_file); + + void setup_names(); + void setup_anonymous_wildcard_names(); + + Variable_ID_Tuple myLocals; + friend class F_Forall; // rearrange needs to access myLocals + friend class F_Or; // push_exists + +private: + virtual bool can_add_child(); + + int priority(); + + friend void align(Rel_Body *originalr, Rel_Body *newr, F_Exists *fe, + Formula *f, const Mapping &mapping, bool &newrIsSet, + List &seen_exists, + Variable_ID_Tuple &seen_exists_ids); +}; + +} // namespace + +#endif -- cgit v1.2.3-70-g09d2