cmake build

1 files changed, 90 insertions, 0 deletions

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 <omega/pres_form.h>
+
+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