diff options
Diffstat (limited to 'omegalib/omega_lib/src/pres_beaut.cc')
| -rw-r--r-- | omegalib/omega_lib/src/pres_beaut.cc | 235 |
1 files changed, 235 insertions, 0 deletions
diff --git a/omegalib/omega_lib/src/pres_beaut.cc b/omegalib/omega_lib/src/pres_beaut.cc new file mode 100644 index 0000000..c23962a --- /dev/null +++ b/omegalib/omega_lib/src/pres_beaut.cc @@ -0,0 +1,235 @@ +#include <omega/pres_tree.h> +#include <omega/pres_conj.h> +#include <omega/Relation.h> +#include <omega/omega_i.h> + +///////////////////////// +// // +// Beautify functions // +// // +///////////////////////// + + +namespace omega { + +// +// f & true = f +// f | false = f +// f1 & f2 & ... & fn = Conjunct(f1,f2,...,fn) +// + +void Rel_Body::beautify() { + assert(children().length()==1); + set_parent(NULL,this); + + skip_finalization_check++; + formula()->beautify(); + Formula *child = formula(); + if(child->node_type()==Op_And && child->children().empty()) { + remove_child(child); + delete child; + add_conjunct(); + } + skip_finalization_check--; + + if(pres_debug) { + fprintf(DebugFile, "\n=== Beautified TREE ===\n"); + prefix_print(DebugFile); + } + assert(children().length()==1); +} + +void Formula::beautify() { + // 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)->beautify(); +} + +void F_Exists::beautify() { + Formula::beautify(); + assert(children().length()==1); + + if(myLocals.empty()) { + // exists( : ***) + parent().remove_child(this); + parent().add_child(children().remove_front()); + delete this; + } + else if (children()[1]->node_type() == Op_And && children()[1]->children().empty()) { + // exists(*** : TRUE) --chun 6/4/2008 + parent().remove_child(this); + parent().add_child(children().remove_front()); + delete this; + } + else { + Formula *child = children().front(); + if(child->node_type() == Op_Conjunct || child->node_type() == Op_Exists) { + child->push_exists(myLocals); + parent().remove_child(this); + parent().add_child(child); + children().remove_front(); + delete this; + } + } +} + +void F_Forall::beautify() { + Formula::beautify(); + assert(children().length()==1); + + if(myLocals.empty()) { + parent().remove_child(this); + parent().add_child(children().remove_front()); + delete this; + } +} + + +// +// The Pix-free versions of beautify for And and Or are a bit +// less efficient than the previous code, as we keep moving +// things from one list to another, but they do not depend on +// knowing that a Pix is valid after the list is updated, and +// they can always be optimized later if necessary. +// + +void F_Or::beautify() { + Formula::beautify(); + + List<Formula*> uglies, beauties; + uglies.join(children()); assert(children().empty()); +#if ! defined NDEBUG + foreach(c,Formula*,uglies,c->set_parent(0)); +#endif + + while(!uglies.empty()) { + Formula *f = uglies.remove_front(); + if(f->node_type()==Op_And && f->children().empty() ) { + // smth | true = true + foreach(c,Formula*,uglies,delete c); + foreach(c,Formula*,beauties,delete c); + parent().remove_child(this); + parent().add_and(); + delete f; + delete this; + return; + } + else if(f->node_type()==Op_Or) { + // OR(f[1-m], OR(c[1-n])) = OR(f[1-m], c[1-n]) +#if ! defined NDEBUG + foreach(c,Formula*,f->children(),c->set_parent(0)); +#endif + uglies.join(f->children()); + delete f; + } + else + beauties.prepend(f); + } + + if(beauties.length()==1) { + beauties.front()->set_parent(&parent()); + parent().remove_child(this); + parent().add_child(beauties.remove_front()); + delete this; + } + else { + foreach(c,Formula*,beauties,(c->set_parent(this), + c->set_relation(relation()))); + assert(children().empty()); + children().join(beauties); + } +} + +void F_And::beautify() { + Formula::beautify(); + + Conjunct *conj = NULL; + + List<Formula*> uglies, beauties; + uglies.join(children()); assert(children().empty()); +#if ! defined NDEBUG + foreach(c,Formula*,uglies,c->set_parent(0)); +#endif + + while(!uglies.empty()) { + Formula *f = uglies.remove_front(); + if (f->node_type() == Op_Conjunct) { + if(conj==NULL) + conj = f->really_conjunct(); + else { + Conjunct *conj1 = merge_conjs(conj, f->really_conjunct(), MERGE_REGULAR); + delete f; + delete conj; + conj = conj1; + } + } + else if(f->node_type()==Op_Or && f->children().empty()) { + // smth & false = false + foreach(c,Formula*,uglies,delete c); + foreach(c,Formula*,beauties,delete c); + parent().remove_child(this); + parent().add_or(); + delete f; + delete conj; + delete this; + return; + } + else if(f->node_type()==Op_And) { + // AND(f[1-m], AND(c[1-n])) = AND(f[1-m], c[1-n]) +#if ! defined NDEBUG + foreach(c,Formula*,f->children(),c->set_parent(0)); +#endif + uglies.join(f->children()); + delete f; + } + else + beauties.prepend(f); + } + + if(conj!=NULL) + beauties.prepend(conj); + + if(beauties.length()==1) { + beauties.front()->set_parent(&parent()); + parent().remove_child(this); + parent().add_child(beauties.remove_front()); + delete this; + } + else { + foreach(c,Formula*,beauties,(c->set_parent(this), + c->set_relation(relation()))); + assert(children().empty()); + children().join(beauties); + } +} + +void F_Not::beautify() { + Formula::beautify(); + assert(children().length()==1); + Formula *child = children().front(); + + if(child->node_type()==Op_And && child->children().empty()) { + // Not TRUE = FALSE + parent().remove_child(this); + parent().add_or(); + delete this; + } + else if (child->node_type()==Op_Or && child->children().empty()) { + // Not FALSE = TRUE + parent().remove_child(this); + parent().add_and(); + delete this; + } +} + +void Conjunct::beautify() { + if(is_true()) { + parent().remove_child(this); + parent().add_and(); + delete this; + } +} + +} // namespace |