From e4b20015a4ee35f1279af4caa983478fa2ff0d4a Mon Sep 17 00:00:00 2001
From: dhuth <derickhuth@gmail.com>
Date: Mon, 6 Oct 2014 11:56:47 -0600
Subject: Added omega to source
---
omega/omega_lib/src/pres_logic.cc | 226 ++++++++++++++++++++++++++++++++++++++
1 file changed, 226 insertions(+)
create mode 100644 omega/omega_lib/src/pres_logic.cc
(limited to 'omega/omega_lib/src/pres_logic.cc')
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
--
cgit v1.2.3-70-g09d2