From 210f77d2c32f14d2e99577fd3c9842bb19d47e50 Mon Sep 17 00:00:00 2001
From: Tuowen Zhao <ztuowen@gmail.com>
Date: Mon, 19 Sep 2016 21:14:58 +0000
Subject: Moved most modules into lib
---
lib/omega/src/pres_quant.cc | 95 +++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 95 insertions(+)
create mode 100644 lib/omega/src/pres_quant.cc
(limited to 'lib/omega/src/pres_quant.cc')
diff --git a/lib/omega/src/pres_quant.cc b/lib/omega/src/pres_quant.cc
new file mode 100644
index 0000000..5483bad
--- /dev/null
+++ b/lib/omega/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
--
cgit v1.2.3-70-g09d2