Omega/omega/omega_lib/src/pres_rear.c

   1 /* $Id: pres_rear.c,v 1.2 2006/05/04 08:59:31 boulet Exp $ */
   2
   3 #include <omega/pres_tree.h>
   4 #include <omega/pres_conj.h>
   5 #include <omega/Relation.h>
   6 #include <omega/omega_i.h>
   7
   8 /////////////////////////
   9 //                     //
  10 // Rearrange functions //
  11 //                     //
  12 /////////////////////////
  13
  14 //
  15 // Rules:
  16 // ~ (f1 | f2 | ... | fn) = ~f1 & ~f2 & ... & fn
  17 // ~ ~ f = f
  18 // Forall v: f = ~ (Exists v: ~ f)
  19 // Exists v: (f1 | ... | fn) = (Exists v: f1) | ... | (Exists v: fn)
  20 //
  21
  22 void Rel_Body::rearrange() {
  23   assert(children().length()==1);
  24
  25   skip_finalization_check++;
  26   formula()->rearrange();
  27   skip_finalization_check--;
  28
  29   if(pres_debug) {
  30     fprintf(DebugFile, "\n=== Rearranged TREE ===\n");
  31     prefix_print(DebugFile);
  32   }
  33 }
  34
  35 void Formula::rearrange()
  36     {
  37     // copy list of children, as they may be removed as we work
  38     List<Formula*> kiddies = myChildren;
  39
  40     for(List_Iterator<Formula*> c(kiddies); c; c++)
  41         (*c)->rearrange();
  42     }
  43
  44 //
  45 // Push nots down the tree until quantifier or conjunct, rearrange kids
  46 //
  47 void F_Not::rearrange() {
  48   Formula *child = children().front();
  49   Formula *new_child, *f;
  50
  51   switch(child->node_type()) {
  52   case Op_Or:
  53     parent().remove_child(this);
  54     new_child = parent().add_and();
  55     while(!child->children().empty()) {
  56       f = child->children().remove_front();
  57       F_Not *new_not = new_child->add_not();
  58       new_not->add_child(f);
  59     }
  60     delete this;
  61     break;
  62 //case Op_And:
  63 //  parent().remove_child(this);
  64 //  new_child = parent().add_or();
  65 //  while(!child->myChildren.empty()) {
  66 //    f = child->myChildren.remove_front();
  67 //    F_Not *new_not = new_child->add_not();
  68 //    new_not->add_child(f);
  69 //  }
  70 //  delete this;
  71 //  break;
  72   case Op_Not:
  73     parent().remove_child(this);
  74     f = child->children().remove_front();
  75     parent().add_child(f);
  76     delete this;
  77     f->rearrange();
  78     return;
  79   default:
  80     new_child = child;
  81     break;
  82   }
  83
  84   new_child->rearrange();
  85 }
  86
  87 //
  88 // Convert a universal quantifier to "not exists not".
  89 // Forall v: f = ~ (Exists v: ~ f)
  90 //
  91 void F_Forall::rearrange() {
  92   Formula &p = parent();
  93   p.remove_child(this);
  94
  95   F_Not *topnot = p.add_not();
  96   F_Exists *exist = topnot->add_exists();
  97   for (Variable_ID_Iterator VI(myLocals); VI; VI++)
  98         (*VI)->set_kind(Exists_Var);
  99   exist->myLocals.join(myLocals);
 100
 101   F_Not *botnot = exist->add_not();
 102   Formula *f = children().remove_front();
 103   botnot->add_child(f);
 104
 105   delete this;
 106
 107   botnot->rearrange();
 108 }
 109
 110 //
 111 // Exists v: (f1 | ... | fn) = (Exists v: f1) | ... | (Exists v: fn)
 112 //
 113 void F_Exists::rearrange() {
 114   Formula* child = children().front();
 115   switch(child->node_type()) {
 116   case Op_Or:
 117   case Op_Conjunct:
 118   case Op_Exists:
 119     child->push_exists(myLocals);
 120     parent().remove_child(this);
 121     parent().add_child(child);
 122     children().remove_front();
 123     delete this;
 124     break;
 125   default:
 126     break;
 127   }
 128
 129   child->rearrange();
 130 }