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
|
#include <omega/pres_quant.h>
#include <omega/omega_i.h>
namespace omega {
F_Forall::F_Forall(Formula *p, Rel_Body *r): F_Declaration(p,r) {
}
F_Exists::F_Exists(Formula *p, Rel_Body *r): F_Declaration(p,r) {
}
F_Exists::F_Exists(Formula *p, Rel_Body *r, Variable_ID_Tuple &S): F_Declaration(p,r,S) {
}
Formula *F_Forall::copy(Formula *parent, Rel_Body *reln) {
F_Forall *f = new F_Forall(parent, reln);
copy_var_decls(f->myLocals, myLocals);
for(List_Iterator<Formula*> c(children()); c; c++)
f->children().append((*c)->copy(f,reln));
reset_remap_field(myLocals);
return f;
}
Formula *F_Exists::copy(Formula *parent, Rel_Body *reln) {
F_Exists *f = new F_Exists(parent, reln);
copy_var_decls(f->myLocals, myLocals);
for(List_Iterator<Formula*> c(children()); c; c++)
f->children().append((*c)->copy(f,reln));
reset_remap_field(myLocals);
return f;
}
Variable_ID F_Forall::declare(Const_String s) {
return do_declare(s, Forall_Var);
}
Variable_ID F_Forall::declare() {
return do_declare(Const_String(), Forall_Var);
}
Variable_ID F_Forall::declare(Variable_ID v) {
return do_declare(v->base_name, Forall_Var);
}
Variable_ID F_Exists::declare(Const_String s) {
return do_declare(s, Exists_Var);
}
Variable_ID F_Exists::declare() {
return do_declare(Const_String(), Exists_Var);
}
Variable_ID F_Exists::declare(Variable_ID v) {
return do_declare(v->base_name, Exists_Var);
}
Conjunct *F_Forall::find_available_conjunct() {
return 0;
}
Conjunct *F_Exists::find_available_conjunct() {
assert(children().length() == 1 || children().length() == 0);
if (children().length() == 0)
return 0;
else
return children().front()->find_available_conjunct();
}
F_Exists *Formula::add_exists() {
assert_not_finalized();
assert(can_add_child());
F_Exists *f = new F_Exists(this, myRelation);
myChildren.append(f);
return f;
}
F_Exists *Formula::add_exists(Variable_ID_Tuple &S) {
assert_not_finalized();
assert(can_add_child());
F_Exists *f = new F_Exists(this, myRelation, S);
myChildren.append(f);
return f;
}
F_Forall *Formula::add_forall() {
assert_not_finalized();
assert(can_add_child());
F_Forall *f = new F_Forall(this, myRelation);
myChildren.append(f);
return f;
}
} // namespace
|
