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_quant.h | 63 +++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 omegalib/omega_lib/include/omega/pres_quant.h (limited to 'omegalib/omega_lib/include/omega/pres_quant.h') diff --git a/omegalib/omega_lib/include/omega/pres_quant.h b/omegalib/omega_lib/include/omega/pres_quant.h new file mode 100644 index 0000000..98c30df --- /dev/null +++ b/omegalib/omega_lib/include/omega/pres_quant.h @@ -0,0 +1,63 @@ +#if ! defined _pres_quant_h +#define _pres_quant_h 1 + +#include + +namespace omega { + +// +// Presburger formula nodes for quantifiers +// + +class F_Exists : public F_Declaration { +public: + inline Node_Type node_type() {return Op_Exists;} + Variable_ID declare(Const_String s); + Variable_ID declare(); + Variable_ID declare(Variable_ID v); + virtual void push_exists(Variable_ID_Tuple &S); + +protected: + friend class Formula; + + F_Exists(Formula *, Rel_Body *); + F_Exists(Formula *, Rel_Body *, Variable_ID_Tuple &); + +private: + Formula *copy(Formula *parent, Rel_Body *reln); + + virtual Conjunct *find_available_conjunct(); + void print(FILE *output_file); + void prefix_print(FILE *output_file, int debug = 1); + void beautify(); + void rearrange(); + DNF* DNFize(); +}; + + +class F_Forall : public F_Declaration { +public: + inline Node_Type node_type() {return Op_Forall;} + Variable_ID declare(Const_String s); + Variable_ID declare(); + Variable_ID declare(Variable_ID v); + +protected: + friend class Formula; + + F_Forall(Formula *, Rel_Body *); + +private: + Formula *copy(Formula *parent, Rel_Body *reln); + + virtual Conjunct *find_available_conjunct(); + void print(FILE *output_file); + void prefix_print(FILE *output_file, int debug = 1); + void beautify(); + void rearrange(); + DNF* DNFize(); +}; + +} // namespace + +#endif -- cgit v1.2.3-70-g09d2