Merge branch 'master' into doe

1 files changed, 226 insertions, 0 deletions

diff --git a/omega/omega_lib/src/pres_logic.cc b/omega/omega_lib/src/pres_logic.cc
new file mode 100644
index 0000000..8ee90f1
--- /dev/null
+++ b/omega/omega_lib/src/pres_logic.cc
@@ -0,0 +1,226 @@
+#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