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
89
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
|
