Moved most modules into lib

1 files changed, 906 insertions, 0 deletions

diff --git a/lib/omega/src/RelBody.cc b/lib/omega/src/RelBody.cc
new file mode 100644
index 0000000..825b153
--- /dev/null
+++ b/lib/omega/src/RelBody.cc
@@ -0,0 +1,906 @@
+/*****************************************************************************
+ Copyright (C) 1994-2000 the Omega Project Team
+ Copyright (C) 2005-2011 Chun Chen
+ All Rights Reserved.
+
+ Purpose:
+   class Rel_Body, internal Relation representation
+
+ Notes:
+
+ History:
+   11/26/09  Remove unecessary mandatary checking for set or relation,
+             treat them uniformly for easy coding, by Chun Chen
+*****************************************************************************/
+
+#include <basic/util.h>
+#include <omega/RelBody.h>
+#include <omega/Relation.h>
+#include <omega/pres_tree.h>
+#include <omega/pres_conj.h>
+#include <omega/omega_i.h>
+#include <assert.h>
+
+namespace omega {
+
+Rel_Body null_rel;
+bool Rel_Body::is_null() const {
+  return(this == &null_rel);
+}
+
+
+int Rel_Body::max_ufs_arity() {
+  int ma = 0, a;
+  for (Variable_ID_Iterator v(*global_decls()); v; v++) {
+    a = (*v)->get_global_var()->arity();
+    if (a > ma)
+      ma = a;
+  }
+  return ma;
+}
+
+int Rel_Body::max_ufs_arity_of_set() {
+  int ma = 0, a;
+  for (Variable_ID_Iterator v(*global_decls()); v; v++)
+    if ((*v)->function_of() == Set_Tuple) {
+      a = (*v)->get_global_var()->arity();
+      if (a > ma)
+        ma = a;
+    }
+  return ma;
+}
+
+int Rel_Body::max_ufs_arity_of_in() {
+  int ma = 0, a;
+  for (Variable_ID_Iterator v(*global_decls()); v; v++)
+    if ((*v)->function_of() == Input_Tuple) {
+      a = (*v)->get_global_var()->arity();
+      if (a > ma)
+        ma = a;
+    }
+  return ma;
+}
+
+int Rel_Body::max_ufs_arity_of_out() {
+  int ma = 0, a;
+  for (Variable_ID_Iterator v(*global_decls()); v; v++)
+    if ((*v)->function_of() == Output_Tuple) {
+      a = (*v)->get_global_var()->arity();
+      if (a > ma)
+        ma = a;
+    }
+  return ma;
+}
+
+int Rel_Body::max_shared_ufs_arity() {
+  int ma = 0, a;
+  for (Variable_ID_Iterator v(*global_decls()); v; v++)
+    for (Variable_ID_Iterator v2(*global_decls()); v2; v2++)
+      if (*v != *v2 
+          && (*v)->get_global_var() == (*v2)->get_global_var()
+          && (*v)->function_of() != (*v2)->function_of()) {
+        a = (*v)->get_global_var()->arity();
+        if (a > ma)
+          ma = a;
+      }
+  return ma;
+}
+
+//
+// Input and output variables.
+//
+void Rel_Body::name_input_var(int nth, Const_String S) {
+  // assert(1 <= nth && nth <= number_input && (!is_set() || skip_set_checks > 0));
+  if (is_null())
+    throw std::invalid_argument("empty relation");
+  if (nth < 1 || nth > number_input)
+    throw std::invalid_argument("invalid input var number");
+  In_Names[nth] = S;
+}
+
+void Rel_Body::name_output_var(int nth, Const_String S) {
+  // assert(1<= nth && nth <= number_output && (!is_set() || skip_set_checks > 0));
+  if (is_null())
+    throw std::invalid_argument("empty relation");
+  if (nth < 1 || nth > number_output)
+    throw std::invalid_argument("invalid output var number");
+  Out_Names[nth] = S;
+}
+
+void Rel_Body::name_set_var(int nth, Const_String S) {
+  if (number_output != 0)
+    throw std::runtime_error("relation is not a set");
+  name_input_var(nth, S);
+}
+
+int Rel_Body::n_inp() const {
+  // assert(!is_null() && (!is_set()||skip_set_checks>0));
+  if (is_null())
+    return 0;
+  else
+    return number_input;
+}
+
+int Rel_Body::n_out() const {
+  // assert(!is_null() && (!is_set()||skip_set_checks>0));
+  if (is_null())
+    return 0;
+  else
+    return number_output;
+}
+
+int Rel_Body::n_set() const {
+  if (number_output != 0)
+    throw std::runtime_error("relation is not a set");
+  return n_inp();
+}
+
+Variable_ID Rel_Body::input_var(int nth) {
+  // assert(!is_null());
+  // assert(!is_set() || skip_set_checks>0);
+  // assert(1 <= nth && nth <= number_input);
+  if (is_null())
+    throw std::invalid_argument("empty relation");
+  if (nth < 1 || nth > number_input)
+    throw std::invalid_argument("invalid input var number");
+  input_vars[nth]->base_name = In_Names[nth];
+  return input_vars[nth];
+}
+
+Variable_ID Rel_Body::output_var(int nth) {
+  // assert(!is_null());
+  // assert(!is_set() || skip_set_checks>0);
+  // assert(1<= nth && nth <= number_output);
+  if (is_null())
+    throw std::invalid_argument("empty relation");
+  if (nth < 1 || nth > number_output)
+    throw std::invalid_argument("invalid output var number");
+  output_vars[nth]->base_name = Out_Names[nth];
+  return output_vars[nth];
+}
+
+Variable_ID Rel_Body::set_var(int nth) {
+  if (number_output != 0)
+    throw std::runtime_error("relation is not a set");
+  return input_var(nth);
+}
+
+//
+// Add the AND node to the relation.
+// Useful for adding restraints.
+//
+F_And *Rel_Body::and_with_and() {
+  assert(!is_null());
+  if (is_simplified())
+    DNF_to_formula();
+  relation()->finalized = false;
+  Formula *f = rm_formula();
+  F_And *a = add_and();
+  a->add_child(f);
+  return a;
+}
+
+//
+// Add constraint to relation at the upper level.
+//
+EQ_Handle Rel_Body::and_with_EQ() {
+  assert(!is_null());
+  if (is_simplified())
+    DNF_to_formula();
+  assert(! is_shared());  // The relation has been split.
+  relation()->finalized = false;
+  return find_available_conjunct()->add_EQ();
+}
+
+EQ_Handle Rel_Body::and_with_EQ(const Constraint_Handle &initial) {
+  assert(!is_null());
+  assert(initial.relation()->is_simplified());
+  EQ_Handle H = and_with_EQ();
+  copy_constraint(H, initial);
+  return H;
+}
+
+GEQ_Handle Rel_Body::and_with_GEQ() {
+  assert(!is_null());
+  if (is_simplified())
+    DNF_to_formula();
+  assert(! is_shared());  // The relation has been split.
+  relation()->finalized = false;  // We are giving out a handle.
+  // We should evantually implement finalization
+  // of subtrees, so the existing formula cannot
+  // be modified.
+  return find_available_conjunct()->add_GEQ();
+}
+
+GEQ_Handle Rel_Body::and_with_GEQ(const Constraint_Handle &initial) {
+  assert(!is_null());
+  assert(initial.relation()->is_simplified());
+  GEQ_Handle H = and_with_GEQ();
+  copy_constraint(H, initial);
+  return H;
+}
+
+
+
+Conjunct *Rel_Body::find_available_conjunct() {
+  Conjunct *c;
+  assert(!is_null());
+
+  if (children().empty()) {
+    c = add_conjunct();
+  }
+  else {
+    assert(children().length() == 1);
+    Formula *kid = children().front();  // RelBodies have only one child
+    c = kid->find_available_conjunct();
+    if (c==NULL) {
+      remove_child(kid);
+      F_And *a = add_and();
+      a->add_child(kid);
+      c = a->add_conjunct();
+    }
+  } 
+  return c;
+}
+
+void Rel_Body::finalize() {
+  assert(!is_null());
+  if (!is_finalized())
+    assert(! is_shared());  // no other pointers into here
+  finalized = true;
+  if (! children().empty())
+    children().front()->finalize();  // Can have at most one child
+}
+
+// Null Rel_Body
+// This is the only rel_body constructor that has ref_count initialized to 1;
+// That's because it's used to construct the global Rel_Body "null_rel". 
+// Unfortunately because we don't know in what order global constructors will
+// be called, we could create a global relation with the default relation
+// constructor (which would set the null_rel ref count to 1), and *then* 
+// call Rel_Body::Rel_Body(), which would set it back to 0, leaving a relation
+// that points to a rel_body with it's ref_count set to 0!  So this is done as
+// a special case, in which the ref_count is always 1.
+Rel_Body::Rel_Body():
+  Formula(0, this), 
+  ref_count(1),
+  status(under_construction),
+  number_input(0), number_output(0),
+  In_Names(0), Out_Names(0),
+  simplified_DNF(NULL),
+  r_conjs(0), 
+  finalized(true),
+  _is_set(false) {
+}
+
+
+Rel_Body::Rel_Body(int n_input, int n_output):
+  Formula(0, this),
+  ref_count(0),
+  status(under_construction),
+  number_input(n_input), number_output(n_output), 
+  In_Names(n_input), Out_Names(n_output),
+  simplified_DNF(NULL),
+  r_conjs(0), 
+  finalized(false) {
+  if (n_output == 0)
+    _is_set = true;
+  else
+    _is_set = false;
+  if(pres_debug) {
+    fprintf(DebugFile, "+++ Create Rel_Body::Rel_Body(%d, %d) = 0x%p +++\n",
+            n_input, n_output, this);
+  }
+  int i; 
+  for(i=1; i<=number_input; i++) {
+    In_Names[i] = Const_String();
+  }
+  for(i=1; i<=number_output; i++) {
+    Out_Names[i] = Const_String();
+  }
+}
+
+// Rel_Body::Rel_Body(Rel_Body *r):
+//   Formula(0, this),
+//   ref_count(0),
+//   status(r->status),
+//   number_input(r->number_input), number_output(r->number_output),
+//   In_Names(r->number_input), Out_Names(r->number_output),
+//   simplified_DNF(NULL),
+//   r_conjs(r->r_conjs), 
+//   finalized(r->finalized),
+//   _is_set(r->_is_set) {
+//   if(pres_debug) {
+//     fprintf(DebugFile, "+++ Copy Rel_Body::Rel_Body(Rel_Body * 0x%p) = 0x%p +++\n", r, this);
+//     prefix_print(DebugFile);
+//   }
+
+//   int i;
+//   for(i=1;i<=r->number_input;i++) In_Names[i] = r->In_Names[i];
+//   for(i=1;i<=r->number_output;i++) Out_Names[i] = r->Out_Names[i];
+//   copy_var_decls(Symbolic,r->Symbolic);
+
+//   if(!r->children().empty() && r->simplified_DNF==NULL) {
+//     Formula *f = r->formula()->copy(this,this);
+//     f->remap();
+//     children().append(f);
+//   }
+//   else if(r->children().empty() && r->simplified_DNF!=NULL) {
+//     simplified_DNF = r->simplified_DNF->copy(this);
+//     simplified_DNF->remap();
+//   }
+//   else {   // copy NULL relation
+//   }
+
+//   reset_remap_field(r->Symbolic);
+// }
+
+Rel_Body *Rel_Body::clone() {
+  Rel_Body *b = new Rel_Body();
+
+  b->ref_count = 0;
+  b->status = status;
+  b->number_input = number_input;
+  b->number_output = number_output;
+  b->r_conjs = r_conjs;
+  b->finalized = finalized;
+  b->_is_set = _is_set;
+  
+  b->In_Names = Tuple<Const_String>(number_input);
+  b->Out_Names = Tuple<Const_String>(number_output);
+  for(int i = 1; i <= number_input; i++)
+    b->In_Names[i] = In_Names[i];
+  for(int i = 1; i <= number_output; i++)
+    b->Out_Names[i] = Out_Names[i];
+  
+  copy_var_decls(b->Symbolic, Symbolic);
+
+  if(!children().empty() && simplified_DNF==NULL) {
+    Formula *f = formula()->copy(b, b);
+    f->remap();
+    b->children().append(f);
+  }
+  else if(children().empty() && simplified_DNF!=NULL) {
+    b->simplified_DNF = simplified_DNF->copy(b);
+    b->simplified_DNF->remap();
+  }
+  else {   // copy NULL relation
+  }
+
+  reset_remap_field(Symbolic);
+  return b;
+}
+
+
+Rel_Body::Rel_Body(Rel_Body *r, Conjunct *c):
+  Formula(0, this),
+  ref_count(0),
+  status(uncompressed),
+  number_input(r->number_input), number_output(r->number_output),
+  In_Names(r->number_input), Out_Names(r->number_output),
+  r_conjs(0), 
+  finalized(r->finalized),
+  _is_set(r->_is_set) {
+  if(pres_debug) {
+    fprintf(DebugFile, "+++ Copy Rel_Body::Rel_Body(Rel_Body * 0x%p, Conjunct * 0x%p) = 0x%p +++\n",r,c,this);
+  }
+
+  int i;
+  for(i=1;i<=r->number_input;i++) In_Names[i] = r->In_Names[i];
+  for(i=1;i<=r->number_output;i++) Out_Names[i] = r->Out_Names[i];
+  copy_var_decls(Symbolic,r->Symbolic);
+
+  // assert that r has as many variables as c requires, or that c is from r
+  assert(r == c->relation());
+  assert(r->simplified_DNF != NULL);
+  simplified_DNF = new DNF;
+  simplified_DNF->add_conjunct(c->copy_conj_diff_relation(this,this));
+  single_conjunct()->remap();
+
+  reset_remap_field(r->Symbolic);
+}
+
+Rel_Body::~Rel_Body() {
+  if(pres_debug) {
+    fprintf(DebugFile, "+++ Destroy Rel_Body::~Rel_Body() 0x%p +++\n", this);
+  }
+  free_var_decls(Symbolic);
+  if(simplified_DNF != NULL) {
+    delete simplified_DNF;
+  }
+}
+
+//
+// Take a relation that has been simplified and convert it 
+// back to formula form.  
+//
+void Rel_Body::DNF_to_formula() {
+  assert(!is_null());
+  if (simplified_DNF != NULL) {
+    simplified_DNF->DNF_to_formula(this);
+    simplified_DNF = NULL;
+    status = under_construction;
+  }
+}
+
+bool Rel_Body::can_add_child() {
+  assert(this != &null_rel);
+  return n_children() < 1;
+}
+
+
+
+// ********************
+//  Simplify functions
+// ********************
+
+
+extern int s_rdt_constrs;
+
+
+//
+// Simplify a given relation.
+// Store the resulting DNF in the relation, clean out the formula.
+//
+void Rel_Body::simplify(int rdt_conjs, int rdt_constrs) {
+  if(simplified_DNF == NULL) {
+    finalized = true;
+    if(children().empty()) {
+      simplified_DNF = new DNF;
+    }
+    else {
+      if(pres_debug) {
+        if(DebugFile==NULL) {
+          DebugFile = fopen("test.out", "w");
+          if(DebugFile==NULL)
+            fprintf(stderr, "Can not open file test.out\n");
+        }
+      }
+
+      assert(children().length()==1);
+      if(pres_debug) {
+        fprintf(DebugFile, "=== %p Rel_Body::simplify(%d, %d) Input tree (%d) ===\n", this,rdt_conjs,rdt_constrs,r_conjs);
+        prefix_print(DebugFile);
+      }
+      verify_tree();
+
+      beautify();
+      verify_tree();
+
+      rearrange();
+      verify_tree();
+
+      beautify();
+      verify_tree();
+
+      s_rdt_constrs = rdt_constrs;
+      if(pres_debug) {
+        fprintf(DebugFile, "\n=== In simplify, before DNFize ===\n");
+        prefix_print(DebugFile);
+      }
+      DNFize();
+      if(pres_debug) {
+        fprintf(DebugFile, "\n=== In simplify, after DNFize ===\n");
+        prefix_print(DebugFile);
+      }
+      verify_tree();
+
+
+      simplified_DNF->rm_redundant_inexact_conjs();
+      verify_tree();
+
+      if (rdt_conjs > 0 && !simplified_DNF->is_definitely_false() && simplified_DNF->length() > 1) {
+        simplified_DNF->rm_redundant_conjs(rdt_conjs-1);
+        verify_tree();
+      }
+      
+      if(pres_debug) {
+        fprintf(DebugFile, "\n=== Resulting Relation ===\n");
+        prefix_print(DebugFile);
+      }
+    }
+  }
+  else {
+    /* Reprocess DNF to get rid of redundant stuff */
+
+    if (rdt_constrs < 0) return;
+    simplified_DNF->rm_redundant_inexact_conjs();
+
+    if (rdt_conjs > r_conjs) {
+      if(pres_debug) 
+        fprintf(DebugFile,"=== Rel_Body::simplify() redundant CONJUNCTS ===\n");
+      simplified_DNF->rm_redundant_conjs(rdt_conjs-1);
+    }
+    if (rdt_constrs > 0 ) {
+      if(pres_debug) 
+        fprintf(DebugFile,"=== Rel_Body::simplify() redundant CONSTR-S ===\n");
+      s_rdt_constrs = rdt_constrs;
+      simplified_DNF->simplify();
+    }
+  }
+
+  r_conjs = rdt_conjs;
+
+  for(DNF_Iterator D(simplified_DNF); D.live(); D.next()) {
+    D.curr()->set_relation(this);
+    D.curr()->set_parent(this);
+  }
+}
+
+
+// ******************
+//  Query functions
+// ******************
+
+
+//
+// Check if relation has a single conjunct formula and return this conjunct.
+//
+Conjunct *Rel_Body::single_conjunct() {
+  simplify();
+  return simplified_DNF->single_conjunct();
+}
+
+bool Rel_Body::has_single_conjunct() {
+  simplify();
+  return simplified_DNF->has_single_conjunct();
+}
+
+//
+// Remove and return first conjunct
+//
+Conjunct *Rel_Body::rm_first_conjunct() {
+  simplify();
+  return simplified_DNF->rm_first_conjunct();
+}
+
+
+void Rel_Body::query_difference(Variable_ID v1, Variable_ID v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed) {
+  simplify();
+
+  coef_t _lb, _ub;
+  int first = 1;
+  bool _g;
+  lowerBound = negInfinity;  // default values if no DNF's
+  upperBound = posInfinity;
+  guaranteed = 0;
+
+  for (DNF_Iterator D(simplified_DNF); D.live(); D.next()) {
+    (*D)->query_difference(v1, v2, _lb, _ub, _g);
+    if (first) {
+      lowerBound = _lb;
+      upperBound = _ub;
+      guaranteed = _g;
+      first = 0;
+    }
+    else {
+      guaranteed = guaranteed && _g;
+      lowerBound = min(lowerBound, _lb);
+      upperBound = max(upperBound, _ub);
+    }
+  }
+}
+
+
+void Rel_Body::query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound) {
+  simplify();
+
+  coef_t _lb, _ub;
+  int first = 1;
+  lowerBound = negInfinity;  // default values if no DNF's
+  upperBound = posInfinity;
+
+  for (DNF_Iterator D(simplified_DNF); D.live(); D.next()) {
+    (*D)->query_variable_bounds(v, _lb, _ub);
+    if (first) {
+      lowerBound = _lb;
+      upperBound = _ub;
+      first = 0;
+    }
+    else {
+      lowerBound = min(lowerBound, _lb);
+      upperBound = max(upperBound, _ub);
+    }
+  }
+}
+
+coef_t Rel_Body::query_variable_mod(Variable_ID v, coef_t factor) {
+  simplify();
+
+  bool first = true;
+  coef_t result;
+
+  for (DNF_Iterator D(simplified_DNF); D.live(); D.next()) {
+    coef_t t = (*D)->query_variable_mod(v, factor);
+    if (t == posInfinity)
+      return posInfinity;
+
+    if (first) {
+      result = t;
+      first = false;
+    }
+    else {
+      if (result != t)
+        return posInfinity;
+    }
+  }
+
+  return result;
+}
+
+
+
+//
+// Simplify formula if needed and return the resulting DNF.
+//
+DNF* Rel_Body::query_DNF() {
+  return(query_DNF(false,false));
+}
+
+DNF* Rel_Body::query_DNF(int rdt_conjs, int rdt_constrs) {
+  simplify(rdt_conjs, rdt_constrs);
+  return(simplified_DNF);
+}
+
+//
+// Other formula queries.
+//
+
+// Interpret UNKNOWN as true, then check satisfiability
+// i.e., check if the formula simplifies to FALSE, since the library
+// will never say that if the *known* constraints are unsatisfiable by 
+// themselves.
+bool Rel_Body::is_upper_bound_satisfiable() {
+  int tmp = s_rdt_constrs;
+  s_rdt_constrs = -1;
+  simplify();
+  s_rdt_constrs = tmp;
+  return(!simplified_DNF->is_definitely_false());
+}
+
+// Interpret UNKNOWN as false, then check satisfiability
+// i.e., check if there exist any exact conjuncts in the solution
+bool Rel_Body::is_lower_bound_satisfiable() {
+  int tmp = s_rdt_constrs;
+  s_rdt_constrs = -1;
+  simplify();
+  s_rdt_constrs = tmp;
+  for(DNF_Iterator d(simplified_DNF); d; d++)
+    if((*d)->is_exact()) return true;
+  return false;
+}
+
+bool Rel_Body::is_satisfiable() {
+  assert(is_lower_bound_satisfiable() == is_upper_bound_satisfiable());
+  return is_upper_bound_satisfiable();
+}
+
+// Check if we can easily determine if the formula evaluates to true.
+bool Rel_Body::is_obvious_tautology() {
+  int tmp = s_rdt_constrs;
+  s_rdt_constrs = 0;
+  simplify();
+  s_rdt_constrs = tmp;
+  return(simplified_DNF->is_definitely_true());
+}
+
+// Expensive check to determine if the formula evaluates to true.
+bool Rel_Body::is_definite_tautology() {
+  if(is_obvious_tautology()) return true;
+  Relation l =  Lower_Bound(Relation(*this,1));
+  return !(Complement(l).is_upper_bound_satisfiable());
+}
+
+bool Rel_Body::is_unknown() {
+  simplify();
+  return(has_single_conjunct() && single_conjunct()->is_unknown());
+}
+
+//
+// Get accuracy status of the relation
+//
+
+Rel_Unknown_Uses Rel_Body::unknown_uses() {
+  if (!is_simplified())
+    simplify();
+    
+  Rel_Unknown_Uses local_status=0; 
+  int n_conj=0;
+
+  for (DNF_Iterator c(simplified_DNF); c; c++) {
+    n_conj++;
+    if ((*c)->is_exact())
+      local_status |= no_u;
+    else if ((*c)->is_unknown())
+      local_status |= or_u;
+    else
+      local_status |= and_u;
+  }
+
+  if (n_conj == 0) {
+    assert(local_status == 0);
+    local_status = no_u;
+  }
+  assert(local_status);
+#if ! defined NDEBUG
+  Rel_Unknown_Uses impossible = (and_u | or_u);
+  assert( (local_status & impossible) != impossible);
+#endif
+
+  return local_status;
+}
+
+void Rel_Body::interpret_unknown_as_false() {
+  simplify();
+  simplified_DNF->remove_inexact_conj();  
+}
+       
+void Rel_Body::interpret_unknown_as_true() {
+  simplify();
+  for(DNF_Iterator d(simplified_DNF); d; d++)
+    (*d)->interpret_unknown_as_true();
+}
+       
+
+void Rel_Body::reverse_leading_dir_info() {
+  if (is_simplified()) {
+    for (DNF_Iterator c(simplified_DNF); c; c++)
+      (*c)->reverse_leading_dir_info();
+  }
+  else {
+    assert(!simplified_DNF);
+    assert(children().size() == 1);
+    children().front()->reverse_leading_dir_info();
+  }
+}
+
+//
+// Rel_Body::DNFize just DNF-izes its child node and calls verify
+//
+
+DNF* Rel_Body::DNFize() {
+#if defined(INCLUDE_COMPRESSION)
+  assert(!this->is_compressed());
+#endif
+  if (! simplified_DNF) {
+    simplified_DNF = children().remove_front()->DNFize();
+
+    int mua = max_shared_ufs_arity();
+    if (mua > 0) {
+      if (pres_debug) {
+        fprintf(DebugFile, "\n=== In DNFize, before LCDNF ===\n");
+        prefix_print(DebugFile);
+      }
+
+      simplified_DNF->make_level_carried_to(mua);
+    }
+
+    if(pres_debug) {
+      fprintf(DebugFile, "\n=== In DNFize, before verify ===\n");
+      prefix_print(DebugFile);
+    }
+
+    simplified_DNF->simplify();
+  }
+
+  assert(children().length() == 0);
+
+  return simplified_DNF;
+}
+
+void Rel_Body::make_level_carried_to(int level) {
+  if (!simplified_DNF) {
+    DNFize();
+  }
+
+  assert(simplified_DNF && children().empty());
+
+  simplified_DNF->make_level_carried_to(level);
+}
+
+//
+// if direction==0, move all conjuncts with >= level leading 0's to return
+//            else  move all conjuncts with level-1 0's followed by
+//      the appropriate signed difference to returned Relation
+//
+
+Relation Rel_Body::extract_dnf_by_carried_level(int level, int direction) {
+  if (!simplified_DNF) {
+    DNFize();
+  }
+
+  assert(simplified_DNF && children().empty());
+
+  simplified_DNF->make_level_carried_to(level);
+
+  Relation extracted(n_inp(), n_out());
+  extracted.copy_names(*this);
+  assert(extracted.rel_body->children().empty());
+  assert(extracted.rel_body->simplified_DNF == NULL);
+  extracted.rel_body->simplified_DNF = new DNF;
+  extracted.rel_body->Symbolic = Symbolic;
+
+  DNF *remaining = new DNF;
+  Conjunct *curr;
+
+  for (curr = simplified_DNF->rm_first_conjunct();
+       curr;
+       curr = simplified_DNF->rm_first_conjunct()) {
+    assert(curr->guaranteed_leading_0s >= level || curr->guaranteed_leading_0s == curr->possible_leading_0s);
+    assert(curr->possible_leading_0s >= 0);
+
+    curr->assert_leading_info();
+
+    if ((direction == 0 && curr->guaranteed_leading_0s >= level) ||
+        (curr->guaranteed_leading_0s == level-1 &&
+         curr->leading_dir_valid_and_known() &&
+         curr->leading_dir * direction > 0)) {
+      extracted.rel_body->simplified_DNF->add_conjunct(curr);
+    }
+    else {
+      remaining->add_conjunct(curr);
+    }
+  }
+  delete simplified_DNF;
+  simplified_DNF = remaining;
+
+#if ! defined NDEBUG
+  for (DNF_Iterator rc(simplified_DNF); rc; rc++)
+    (*rc)->assert_leading_info();
+
+  for (DNF_Iterator ec(extracted.rel_body->simplified_DNF); ec; ec++)
+    (*ec)->assert_leading_info();
+#endif
+
+  finalize();
+  extracted.finalize();
+  return extracted;
+}
+
+//Compress/uncompress functions
+
+bool Rel_Body::is_compressed() {
+#if defined(INCLUDE_COMPRESSION)
+  if(is_simplified()) {
+    for(DNF_Iterator p(simplified_DNF); p.live(); p.next()) {
+      if(p.curr()->is_compressed())
+        return true;
+    }
+  }
+  return false;
+#else
+  return true; // This allows is_compressed assertions to work
+#endif
+}
+
+void Rel_Body::compress() {
+#if !defined(INCLUDE_COMPRESSION)
+  return;
+#else
+  if (status == compressed)
+    return;
+  if (pres_debug)
+    fprintf(DebugFile,">>> Compressing relation %p\n",this);
+  simplify();
+  for(DNF_Iterator p(simplified_DNF); p.live(); p.next()) {
+    p.curr()->compress();
+    status = compressed;
+  }
+#endif
+}
+
+void Rel_Body::uncompress() {
+#if !defined(INCLUDE_COMPRESSION)
+  return;
+#else
+  if (pres_debug)
+    fprintf(DebugFile,"<<< Uncompressing relation %p\n",this);
+  assert(is_simplified());
+  for(DNF_Iterator p(simplified_DNF); p.live(); p.next()) {
+    p.curr()->uncompress();
+    status = uncompressed;
+  }
+#endif
+}
+
+}