blob: 508959dc6b7466b58f0f54167a65fde6edbc69f6 (
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
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
#include <omega/pres_tree.h>
#include <omega/pres_conj.h>
#include <omega/Relation.h>
#include <omega/omega_i.h>
namespace omega {
/////////////////////////
// //
// Rearrange functions //
// //
/////////////////////////
//
// Rules:
// ~ (f1 | f2 | ... | fn) = ~f1 & ~f2 & ... & fn
// ~ ~ f = f
// Forall v: f = ~ (Exists v: ~ f)
// Exists v: (f1 | ... | fn) = (Exists v: f1) | ... | (Exists v: fn)
//
void Rel_Body::rearrange() {
assert(children().length()==1);
skip_finalization_check++;
formula()->rearrange();
skip_finalization_check--;
if(pres_debug) {
fprintf(DebugFile, "\n=== Rearranged TREE ===\n");
prefix_print(DebugFile);
}
}
void Formula::rearrange() {
// copy list of children, as they may be removed as we work
List<Formula*> kiddies = myChildren;
for(List_Iterator<Formula*> c(kiddies); c; c++)
(*c)->rearrange();
}
//
// Push nots down the tree until quantifier or conjunct, rearrange kids
//
void F_Not::rearrange() {
Formula *child = children().front();
Formula *new_child, *f;
switch(child->node_type()) {
case Op_Or:
parent().remove_child(this);
new_child = parent().add_and();
while(!child->children().empty()) {
f = child->children().remove_front();
F_Not *new_not = new_child->add_not();
new_not->add_child(f);
}
delete this;
break;
//case Op_And:
// parent().remove_child(this);
// new_child = parent().add_or();
// while(!child->myChildren.empty()) {
// f = child->myChildren.remove_front();
// F_Not *new_not = new_child->add_not();
// new_not->add_child(f);
// }
// delete this;
// break;
case Op_Not:
parent().remove_child(this);
f = child->children().remove_front();
parent().add_child(f);
delete this;
f->rearrange();
return;
default:
new_child = child;
break;
}
new_child->rearrange();
}
//
// Convert a universal quantifier to "not exists not".
// Forall v: f = ~ (Exists v: ~ f)
//
void F_Forall::rearrange() {
Formula &p = parent();
p.remove_child(this);
F_Not *topnot = p.add_not();
F_Exists *exist = topnot->add_exists();
for (Variable_ID_Iterator VI(myLocals); VI; VI++)
(*VI)->set_kind(Exists_Var);
exist->myLocals.join(myLocals);
F_Not *botnot = exist->add_not();
Formula *f = children().remove_front();
botnot->add_child(f);
delete this;
botnot->rearrange();
}
//
// Exists v: (f1 | ... | fn) = (Exists v: f1) | ... | (Exists v: fn)
//
void F_Exists::rearrange() {
Formula* child = children().front();
switch(child->node_type()) {
case Op_Or:
case Op_Conjunct:
case Op_Exists:
child->push_exists(myLocals);
parent().remove_child(this);
parent().add_child(child);
children().remove_front();
delete this;
break;
default:
break;
}
child->rearrange();
}
} // namespace
|
