1 files changed, 88 insertions, 0 deletions
diff --git a/omegalib/omega_lib/include/omega/pres_subs.h b/omegalib/omega_lib/include/omega/pres_subs.h
new file mode 100644
index 0000000..8a9ee92
--- /dev/null
+++ b/omegalib/omega_lib/include/omega/pres_subs.h
@@ -0,0 +1,88 @@
+#if !defined(pres_subs_h)
+#define pres_subs_h
+
+/* Interface to omega core's substitutions.
+
+   Creating an object of class Substitutions causes ordered elimination, 
+   i.e. variables in the input and output tuples are substituted for by
+   functions of earlier variables.  Could conceivablely create a more 
+   flexible interface to orderedElimination if we developed a way to 
+   specify the desired variable order.  
+
+   This is not an entirely consistent interface, since Sub_Handles
+   shouldn't really permit update_coef on SUBs.  It is not a real
+   problem since subs are now no longer part of a conjunct, but it is
+   a slightly odd situation.
+
+   Don't try to simplify r after performing orderedElimination.
+*/
+
+   
+#include <omega/pres_gen.h>
+#include <omega/Relation.h>
+#include <omega/pres_conj.h>
+#include <omega/pres_cnstr.h>
+
+namespace omega {
+
+class Sub_Handle;
+class Sub_Iterator;
+
+class Substitutions  {
+public: 
+    Substitutions(Relation &input_R, Conjunct *input_c);
+    ~Substitutions();
+    Sub_Handle get_sub(Variable_ID v);
+    bool substituted(Variable_ID v);
+    bool sub_involves(Variable_ID v, Var_Kind kind);
+private:
+    friend class Sub_Iterator;
+    friend class Sub_Handle;
+    Relation *r;
+    Conjunct *c;
+    eqn *subs;
+    Variable_ID_Tuple subbed_vars;
+};
+
+
+//::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
+
+
+class Sub_Handle: public Constraint_Handle {
+public:
+    inline Sub_Handle() {}
+
+    virtual std::string print_to_string() const;
+    virtual std::string print_term_to_string() const;
+    Variable_ID variable() {return v;}
+
+private:
+    friend class Substitutions;
+    friend class Sub_Iterator;
+    Sub_Handle(Substitutions *, int, Variable_ID);
+//    Sub_Handle(Substitutions *, int);
+
+    Variable_ID v;
+};
+
+//::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
+
+
+class Sub_Iterator : public Generator<Sub_Handle> {
+public:
+    Sub_Iterator(Substitutions *input_s): s(input_s), current(0),
+                                          last(s->c->problem->nSUBs-1) {}
+    int  live() const;
+    void operator++(int);
+    void operator++();
+    Sub_Handle operator* ();
+    Sub_Handle operator* () const;
+
+private:
+    Substitutions *s;
+    int current, last;
+};
+
+} // namespace
+
+#endif