cmake build

1 files changed, 0 insertions, 906 deletions

diff --git a/omega/omega_lib/src/RelBody.cc b/omega/omega_lib/src/RelBody.cc
deleted file mode 100644
index 825b153..0000000
--- a/omega/omega_lib/src/RelBody.cc
+++ /dev/null
@@ -1,906 +0,0 @@
-/*****************************************************************************
- 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
-}
-
-}