1 files changed, 112 insertions, 0 deletions
diff --git a/omegalib/omega_lib/include/omega/pres_form.h b/omegalib/omega_lib/include/omega/pres_form.h
new file mode 100644
index 0000000..ed3258e
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_form.h
@@ -0,0 +1,112 @@
+#if ! defined _pres_form_h
+#define _pres_form_h 1
+
+#include <omega/pres_gen.h>
+
+namespace omega {
+
+typedef enum {Op_Relation, Op_Not, Op_And, Op_Or,
+              Op_Conjunct, Op_Forall, Op_Exists}  Node_Type;
+
+
+//
+// Presburger Formula base class
+//
+
+class Formula {
+public:
+  virtual Node_Type node_type()=0;
+
+  F_Forall *add_forall();
+  F_Exists *add_exists();
+  virtual F_And  *and_with();
+  F_And  *add_and();
+  F_Or *add_or();
+  F_Not *add_not();
+  void add_unknown();
+
+  virtual void finalize();
+  virtual void print(FILE *output_file);
+
+  Rel_Body *relation() { return myRelation; }
+
+protected:
+  virtual ~Formula();
+private:
+  Formula(Formula *, Rel_Body *);
+
+  // The relational operations need to work with formula trees
+  friend class Relation;
+  friend_rel_ops;
+  // as do the functions that build DNF's
+  friend  class DNF;
+  // or other parts of the tree
+  friend class Conjunct;
+  friend class F_Declaration;
+  friend class F_Exists;
+  friend class F_Forall;
+  friend class F_Or;
+  friend class F_And;
+  friend class F_Not;
+  friend class Rel_Body;
+
+
+  // Operations needed for manipulation of formula trees:
+
+  void remove_child(Formula *);
+  void replace_child(Formula *child, Formula *new_child);
+  virtual bool can_add_child();
+  void add_child(Formula *);
+
+  Conjunct *add_conjunct();
+  virtual Conjunct *find_available_conjunct() = 0;
+
+  virtual Formula *copy(Formula *parent, Rel_Body *reln);
+  F_Exists *add_exists(Variable_ID_Tuple &S); 
+  virtual     void push_exists(Variable_ID_Tuple &S);
+
+  // Accessor functions for tree building
+
+  List<Formula*> &children() {return myChildren;}
+  int n_children() const {return myChildren.length();}
+  const List<Formula*> &get_children() const {return myChildren;}
+  Formula &parent() {return *myParent;}
+  void set_parent(Formula *p) {myParent = p;}
+
+
+  virtual int priority();
+
+  void verify_tree();  // should be const, but iterators are used
+
+  virtual void reverse_leading_dir_info();
+  virtual void invalidate_leading_info(int changed = -1);
+  virtual void enforce_leading_info(int guaranteed, int possible, int dir);
+
+  virtual void remap();   
+  virtual DNF* DNFize() = 0;
+  virtual void beautify();
+  virtual void rearrange();
+  virtual void setup_names();
+
+  virtual void print_separator(FILE *output_file);
+  virtual void combine_columns();
+  virtual void prefix_print(FILE *output_file, int debug = 1);
+  void print_head(FILE *output_file);
+
+  void set_relation(Rel_Body *r);
+  void set_parent(Formula *parent, Rel_Body *reln);
+
+  void assert_not_finalized();
+
+  virtual Conjunct *really_conjunct();  // until we get RTTI
+
+private:
+  List<Formula*>     myChildren;
+  Formula           *myParent;
+  Rel_Body          *myRelation;
+
+};
+
+} // namespace
+
+#endif