From 2fce43d484e4148ae858f410d51dcd9951d34374 Mon Sep 17 00:00:00 2001 From: Tuowen Zhao Date: Sun, 18 Sep 2016 15:45:13 +0000 Subject: remove include & rename --- omegalib/omega_lib/include/omega/pres_quant.h | 63 --------------------------- 1 file changed, 63 deletions(-) delete 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 deleted file mode 100644 index 98c30df..0000000 --- a/omegalib/omega_lib/include/omega/pres_quant.h +++ /dev/null @@ -1,63 +0,0 @@ -#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