Moved most modules into lib

1 files changed, 0 insertions, 226 deletions

diff --git a/omegalib/omega/src/pres_logic.cc b/omegalib/omega/src/pres_logic.cc
deleted file mode 100644
index 8ee90f1..0000000
--- a/omegalib/omega/src/pres_logic.cc
+++ /dev/null
@@ -1,226 +0,0 @@
-#include <omega/pres_logic.h>
-#include <omega/pres_conj.h>
-#include <omega/pres_quant.h>
-#include <omega/omega_i.h>
-
-namespace omega {
-
-GEQ_Handle F_And::add_GEQ(int preserves_level) {
-  assert_not_finalized();
-  if (pos_conj == NULL || pos_conj->problem->nGEQs >= maxGEQs) {
-    pos_conj = NULL;
-    for(List_Iterator<Formula*> c(children()); c; c++) {
-      if ((*c)->node_type()==Op_Conjunct &&
-          ((*c)->really_conjunct())->problem->nGEQs < maxGEQs) {
-        pos_conj = (*c)->really_conjunct();
-        break;
-      }
-    }
-    if(!pos_conj) pos_conj = add_conjunct();// FERD -- set level if preserved?
-  }
-  return pos_conj->add_GEQ(preserves_level);
-}
-
-
-EQ_Handle F_And::add_EQ(int preserves_level) {
-  assert_not_finalized();
-  if (pos_conj == NULL || pos_conj->problem->nEQs >= maxEQs) {
-    pos_conj = NULL;
-    for(List_Iterator<Formula*> c(children()); c; c++) {
-      if ((*c)->node_type()==Op_Conjunct &&
-          ((*c)->really_conjunct())->problem->nEQs < maxEQs) {
-        pos_conj = (*c)->really_conjunct();
-        break;
-      }
-    }
-    if(!pos_conj) pos_conj = add_conjunct();//FERD-set level info if preserved?
-  }
-  return pos_conj->add_EQ(preserves_level);
-}
-
-Stride_Handle F_And::add_stride(int step, int preserves_level) {
-  assert_not_finalized();
-  if (pos_conj == NULL || pos_conj->problem->nEQs >= maxEQs) {
-    pos_conj = NULL;
-    for(List_Iterator<Formula*> c(children()); c; c++) {
-      if ((*c)->node_type()==Op_Conjunct &&
-          ((*c)->really_conjunct())->problem->nEQs < maxEQs) {
-        pos_conj = (*c)->really_conjunct();
-        break;
-      }
-    }
-    if(!pos_conj) pos_conj = add_conjunct();  // FERD -set level if preserved?
-  }
-  return pos_conj->add_stride(step, preserves_level);
-}
-
-GEQ_Handle F_And::add_GEQ(const Constraint_Handle &constraint, int preserves_level) {
-  assert_not_finalized();
-  if (pos_conj == NULL || pos_conj->problem->nGEQs >= maxGEQs) {
-    pos_conj = NULL;
-    for(List_Iterator<Formula*> c(children()); c; c++) {
-      if ((*c)->node_type()==Op_Conjunct &&
-          ((*c)->really_conjunct())->problem->nGEQs < maxGEQs) {
-        pos_conj = (*c)->really_conjunct();
-        break;
-      }
-    }
-    if(!pos_conj) pos_conj = add_conjunct();// FERD -- set level if preserved?
-  }
-  return pos_conj->add_GEQ(constraint, preserves_level);
-}
-
-
-EQ_Handle F_And::add_EQ(const Constraint_Handle &constraint, int preserves_level) {
-  assert_not_finalized();
-  if (pos_conj == NULL || pos_conj->problem->nEQs >= maxEQs) {
-    pos_conj = NULL;
-    for(List_Iterator<Formula*> c(children()); c; c++) {
-      if ((*c)->node_type()==Op_Conjunct &&
-          ((*c)->really_conjunct())->problem->nEQs < maxEQs) {
-        pos_conj = (*c)->really_conjunct();
-        break;
-      }
-    }
-    if(!pos_conj) pos_conj = add_conjunct();//FERD-set level info if preserved?
-  }
-  return pos_conj->add_EQ(constraint,preserves_level);
-}
-
-
-void F_And::add_unknown() {
-  assert_not_finalized();
-  if (pos_conj == NULL) {
-    for (List_Iterator<Formula*> c(children()); c; c++) {
-      if ((*c)->node_type()==Op_Conjunct) {
-        pos_conj = (*c)->really_conjunct();
-        break;
-      }
-    }
-    if(!pos_conj) pos_conj = add_conjunct(); // FERD - set level if preseved?
-  }
-  pos_conj->make_inexact();
-}     
-
-Conjunct *F_Or::find_available_conjunct() {
-  return 0;
-}
-
-Conjunct *F_Not::find_available_conjunct() {
-  return 0;
-}
-
-Conjunct *F_And::find_available_conjunct() {
-  for(List_Iterator<Formula*> child(children()); child; child++) {
-    Conjunct *c = (*child)->find_available_conjunct();
-    if (c) return c;
-  }
-  return 0;
-}
-
-
-void F_Not::finalize() {
-  assert(n_children() == 1);
-  Formula::finalize();
-}
-
-bool F_Not::can_add_child() {
-  return n_children() < 1;
-}
-
-F_And *F_And::and_with() {
-  assert_not_finalized();
-  assert(can_add_child());
-  return this;
-}
-
-F_And::F_And(Formula *p, Rel_Body *r): Formula(p,r), pos_conj(NULL) {
-}
-
-F_Or::F_Or(Formula *p, Rel_Body *r): Formula(p,r){
-}
-
-F_Not::F_Not(Formula *p, Rel_Body *r): Formula(p,r){
-}
-
-Formula *F_And::copy(Formula *parent, Rel_Body *reln) {
-  F_And *f = new F_And(parent, reln);
-  for(List_Iterator<Formula*> c(children()); c; c++)
-    f->children().append((*c)->copy(f,reln));
-  return f;
-}
-
-Formula *F_Or::copy(Formula *parent, Rel_Body *reln) {
-  F_Or *f = new F_Or(parent, reln);
-  for(List_Iterator<Formula*> c(children()); c; c++)
-    f->children().append((*c)->copy(f,reln));
-  return f;
-}
-
-Formula *F_Not::copy(Formula *parent, Rel_Body *reln) {
-  F_Not *f = new F_Not(parent, reln);
-  for(List_Iterator<Formula*> c(children()); c; c++)
-    f->children().append((*c)->copy(f,reln));
-  return f;
-}
-
-//
-// Create F_Exists nodes below this F_Or.
-// Copy list S to each of the created nodes.
-// Push_exists takes responsibility for reusing or deleting Var_ID's;
-//  here we delete them.  Must also empty out the Tuple when finished.
-void F_Or::push_exists(Variable_ID_Tuple &S) {
-  List<Formula*> mc;
-  mc.join(children());
-
-  while(!mc.empty()) {
-    Formula *f = mc.remove_front();
-    F_Exists *e = add_exists();
-
-    copy_var_decls(e->myLocals, S);
-    f->remap();
-    reset_remap_field(S);
-
-    e->add_child(f);
-  }
-  // Since these are not reused, they have to be deleted
-  for(Tuple_Iterator<Variable_ID> VI(S); VI; VI++) {
-    assert((*VI)->kind() == Exists_Var);
-    delete *VI;
-  }
-  S.clear();
-}
-
-void F_Exists::push_exists(Variable_ID_Tuple &S) {
-  myLocals.join(S);
-}
-
-F_Not *Formula::add_not() {
-  assert_not_finalized();
-  assert(can_add_child());
-  F_Not *f = new F_Not(this, myRelation);
-  myChildren.append(f);
-  return f;
-}
-
-F_And *Formula::add_and() {
-  assert_not_finalized();
-  assert(can_add_child());
-  F_And *f = new F_And(this, myRelation);
-  myChildren.append(f);
-  return f;
-}
-
-F_And *Formula::and_with() {
-  return add_and();
-}
-
-F_Or *Formula::add_or() {
-  assert_not_finalized();
-  assert(can_add_child());
-  F_Or *f = new F_Or(this, myRelation);
-  myChildren.append(f);
-  return f;
-}
-
-} // namespace