blob: 7fec0bccdf6f4da721837ea2285dbecfd3659a67 (
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
|
#if ! defined _pres_decl_h
#define _pres_decl_h 1
#include <omega/pres_var.h>
#include <omega/pres_form.h>
#include <basic/Section.h>
namespace omega {
//
// Base class for presburger formula nodes with variables
//
class F_Declaration : public Formula {
public:
virtual Variable_ID declare(Const_String s)=0;
virtual Variable_ID declare()=0;
virtual Variable_ID declare(Variable_ID)=0;
virtual Section<Variable_ID> declare_tuple(int size);
void finalize();
inline Variable_ID_Tuple &locals() {return myLocals;}
protected:
F_Declaration(Formula *, Rel_Body *);
F_Declaration(Formula *, Rel_Body *, Variable_ID_Tuple &);
~F_Declaration();
Variable_ID do_declare(Const_String s, Var_Kind var_kind);
void prefix_print(FILE *output_file, int debug = 1);
void print(FILE *output_file);
void setup_names();
void setup_anonymous_wildcard_names();
Variable_ID_Tuple myLocals;
friend class F_Forall; // rearrange needs to access myLocals
friend class F_Or; // push_exists
private:
virtual bool can_add_child();
int priority();
friend void align(Rel_Body *originalr, Rel_Body *newr, F_Exists *fe,
Formula *f, const Mapping &mapping, bool &newrIsSet,
List<int> &seen_exists,
Variable_ID_Tuple &seen_exists_ids);
};
} // namespace
#endif
|
