diff options
Diffstat (limited to 'lib/omega/src/pres_logic.cc')
| -rw-r--r-- | lib/omega/src/pres_logic.cc | 226 |
1 files changed, 226 insertions, 0 deletions
diff --git a/lib/omega/src/pres_logic.cc b/lib/omega/src/pres_logic.cc new file mode 100644 index 0000000..8ee90f1 --- /dev/null +++ b/lib/omega/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 |