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
|
#include <omega/pres_decl.h>
#include <omega/omega_i.h>
namespace omega {
//
// Declare functions.
//
Variable_ID F_Declaration::do_declare(Const_String s, Var_Kind var_type) {
Variable_ID v;
assert(var_type != Global_Var);
if(!s.null()) {
v = new Var_Decl(s, var_type, 0);
}
else {
v = new Var_Decl(var_type, 0);
}
myLocals.append(v);
return v;
}
Variable_ID F_Declaration::declare(Const_String) {
assert(0); // must be declared in forall, exists, or conjunct
return(NULL);
}
Section<Variable_ID> F_Declaration::declare_tuple(int n) {
int first = myLocals.size()+1;
for (int i=1 ; i<=n; i++)
declare();
return Section<Variable_ID>(&myLocals, first, n);
}
void F_Declaration::finalize() {
assert(n_children() == 1);
Formula::finalize();
}
bool F_Declaration::can_add_child() {
return n_children() < 1;
}
F_Declaration::F_Declaration(Formula *p, Rel_Body *r):
Formula(p,r), myLocals(0) {
}
F_Declaration::F_Declaration(Formula *p, Rel_Body *r, Variable_ID_Tuple &S):
Formula(p,r), myLocals(S) {
}
//
// Destruct declarative node.
// Delete variableID's themselves if they are not global.
//
F_Declaration::~F_Declaration() {
free_var_decls(myLocals);
}
//Setup names for printing
void F_Declaration::setup_anonymous_wildcard_names() {
for(Tuple_Iterator<Variable_ID> VI(myLocals); VI; VI++) {
Variable_ID v = *VI;
if (v->base_name.null()) v->instance = wildCardInstanceNumber++;
}
}
} // namespace
|
