Merge branch 'master' into doe

1 files changed, 95 insertions, 0 deletions

diff --git a/omega/omega_lib/src/pres_quant.cc b/omega/omega_lib/src/pres_quant.cc
new file mode 100644
index 0000000..5483bad
--- /dev/null
+++ b/omega/omega_lib/src/pres_quant.cc
@@ -0,0 +1,95 @@
+#include <omega/pres_quant.h>
+#include <omega/omega_i.h>
+
+namespace omega {
+
+F_Forall::F_Forall(Formula *p, Rel_Body *r): F_Declaration(p,r) {
+}
+
+F_Exists::F_Exists(Formula *p, Rel_Body *r): F_Declaration(p,r) {
+}
+
+F_Exists::F_Exists(Formula *p, Rel_Body *r, Variable_ID_Tuple &S): F_Declaration(p,r,S) {
+}
+
+
+Formula *F_Forall::copy(Formula *parent, Rel_Body *reln) {
+  F_Forall *f = new F_Forall(parent, reln);
+  copy_var_decls(f->myLocals, myLocals);
+  for(List_Iterator<Formula*> c(children()); c; c++)
+    f->children().append((*c)->copy(f,reln));
+  reset_remap_field(myLocals);
+  return f;
+}
+
+Formula *F_Exists::copy(Formula *parent, Rel_Body *reln) {
+  F_Exists *f = new F_Exists(parent, reln);
+  copy_var_decls(f->myLocals, myLocals);
+  for(List_Iterator<Formula*> c(children()); c; c++)
+    f->children().append((*c)->copy(f,reln));
+  reset_remap_field(myLocals);
+  return f;
+}
+
+Variable_ID F_Forall::declare(Const_String s) {
+  return do_declare(s, Forall_Var);
+}
+
+Variable_ID F_Forall::declare() {
+  return do_declare(Const_String(), Forall_Var);
+}
+
+Variable_ID F_Forall::declare(Variable_ID v) {
+  return do_declare(v->base_name, Forall_Var);
+}
+
+
+Variable_ID F_Exists::declare(Const_String s) {
+  return do_declare(s, Exists_Var);
+}
+
+Variable_ID F_Exists::declare() {
+  return do_declare(Const_String(), Exists_Var);
+}
+
+Variable_ID F_Exists::declare(Variable_ID v) {
+  return do_declare(v->base_name, Exists_Var);
+}
+
+Conjunct *F_Forall::find_available_conjunct() {
+  return 0;
+}
+
+Conjunct *F_Exists::find_available_conjunct() {
+  assert(children().length() == 1 || children().length() == 0);
+  if (children().length() == 0)
+    return 0;
+  else 
+    return children().front()->find_available_conjunct();
+}
+
+F_Exists *Formula::add_exists() {
+  assert_not_finalized();
+  assert(can_add_child());
+  F_Exists *f = new F_Exists(this, myRelation);
+  myChildren.append(f);
+  return f;
+}
+
+F_Exists *Formula::add_exists(Variable_ID_Tuple &S) {
+  assert_not_finalized();
+  assert(can_add_child());
+  F_Exists *f = new F_Exists(this, myRelation, S);
+  myChildren.append(f);
+  return f;
+}
+
+F_Forall *Formula::add_forall() {
+  assert_not_finalized();
+  assert(can_add_child());
+  F_Forall *f = new F_Forall(this, myRelation);
+  myChildren.append(f);
+  return f;
+}
+
+} // namespace