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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
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
|
