blob: 8a9ee926f12e7b8f4b41603f310e2dfc38389912 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
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
|
