cmake build

1 files changed, 450 insertions, 0 deletions

diff --git a/omegalib/omega_lib/src/pres_cnstr.cc b/omegalib/omega_lib/src/pres_cnstr.cc
new file mode 100644
index 0000000..a8ebd15
--- /dev/null
+++ b/omegalib/omega_lib/src/pres_cnstr.cc
@@ -0,0 +1,450 @@
+#include <omega/pres_cnstr.h>
+#include <omega/pres_conj.h>
+#include <omega/Relation.h>
+#include <omega/omega_i.h>
+
+namespace omega {
+
+Constraint_Handle::Constraint_Handle(Conjunct *_c, eqn **_eqns, int _e):
+  c(_c), eqns(_eqns), e(_e) {
+}
+
+GEQ_Handle::GEQ_Handle(Conjunct *_c, int _e):
+  Constraint_Handle(_c,&(_c->problem->GEQs),_e) {
+}
+
+bool Constraint_Handle::is_const(Variable_ID v) {
+  bool is_const=true;
+  for(Constr_Vars_Iter cvi(*this, false); cvi && is_const; cvi++)
+    is_const = ((*cvi).coef == 0 || ((*cvi).var == v && (*cvi).coef !=0));
+  return is_const;
+}
+
+bool Constraint_Handle::is_const_except_for_global(Variable_ID v){
+  bool is_const=true;
+  for(Constr_Vars_Iter cvi(*this, false); cvi && is_const; cvi++)
+	if((*cvi).var->kind() != Global_Var)
+      is_const = ((*cvi).coef == 0 || ((*cvi).var == v && (*cvi).coef !=0));
+  return is_const;
+}
+
+bool EQ_Handle::operator==(const Constraint_Handle &that) {
+  Constraint_Handle &e1=*this;
+  const Constraint_Handle &e2=that;
+  int sign = 0;
+  for(Constr_Vars_Iter cvi(e1, false); cvi; cvi++) {
+    coef_t c1 = (*cvi).coef;
+    coef_t c2 = e2.get_coef((*cvi).var);
+    if (sign == 0) sign = (c1*c2>=0?1:-1);
+    if (sign*c1 != c2) return false;
+  }
+  assert(sign != 0);
+  {
+    for(Constr_Vars_Iter cvi(e2, false); cvi; cvi++) {
+      coef_t c1 = e1.get_coef((*cvi).var);
+      coef_t c2 = (*cvi).coef;
+      if (sign*c1 != c2) return false;
+    }
+  }
+  return sign * e1.get_const() == e2.get_const();
+}
+
+bool GEQ_Handle::operator==(const Constraint_Handle &that) {
+  Constraint_Handle &e1=*this;
+  const Constraint_Handle &e2=that;
+  for(Constr_Vars_Iter cvi(e1, false); cvi; cvi++) {
+    coef_t c1 = (*cvi).coef;
+    coef_t c2 = e2.get_coef((*cvi).var);
+    if (c1 != c2) return false;
+  }
+  {
+    for(Constr_Vars_Iter cvi(e2, false); cvi; cvi++) {
+      coef_t c1 = e1.get_coef((*cvi).var);
+      coef_t c2 = (*cvi).coef;
+      if (c1 != c2) return false;
+    }
+  }
+  return e1.get_const() == e2.get_const();
+}
+
+
+
+
+void GEQ_Handle::negate() {
+  assert(! this->relation()->is_simplified());
+  int i;
+  for(i=1; i<=c->problem->nVars; i++) {
+    (*eqns)[e].coef[i] = -(*eqns)[e].coef[i];
+  }
+  (*eqns)[e].coef[0] = -(*eqns)[e].coef[0]-1;
+}
+
+bool Constraint_Handle::has_wildcards() const {
+  Constr_Vars_Iter C(*this, true);
+  if (C.live()) {
+    assert(C.curr_var()->kind() == Wildcard_Var);
+    assert(C.curr_coef() != 0);
+    return 1;
+  }
+  return 0;
+}
+
+int Constraint_Handle::max_tuple_pos() const {
+  int m = 0;
+  for( Constr_Vars_Iter C(*this, false); C.live() ; C.next()) {
+    switch (C.curr_var()->kind()) {
+    case Input_Var: 
+    case Output_Var: {
+      int pos = C.curr_var()->get_position();
+      if (m < pos) m = pos;
+      break;
+    }
+    default: 
+      ;
+    }
+  }
+  return m;
+}
+
+int Constraint_Handle::min_tuple_pos() const {
+  int m = 0;
+  for( Constr_Vars_Iter C(*this, false); C.live() ; C.next()) {
+    switch (C.curr_var()->kind()) {
+    case Input_Var: 
+    case Output_Var: {
+      int pos = C.curr_var()->get_position();
+      if (m == 0 || m > pos) m = pos;
+      break;
+    }
+    default: 
+      ;
+    }
+  }
+  return m;
+}
+
+
+EQ_Handle::EQ_Handle(Conjunct *_c, int _e): Constraint_Handle(_c,&(_c->problem->EQs),_e) {
+}
+
+//
+// Update functions.
+//
+void Constraint_Handle::update_coef(Variable_ID D, coef_t I) {
+  assert(! this->relation()->is_simplified());
+  assert(D != 0);
+  // The next two assertions are somewhat high-cost.
+#if !defined(NDEBUG)
+  // skip_set_checks++;
+  assert((D->kind() != Input_Var || D->get_position() <= this->relation()->n_inp()));
+  assert((D->kind() != Output_Var || D->get_position() <= this->relation()->n_out()));
+  // skip_set_checks--;
+#endif
+  int col = c->get_column(D);
+  (*eqns)[e].coef[col] += I;
+}
+
+void Constraint_Handle::update_const(coef_t I) {
+  assert(! this->relation()->is_simplified());
+  (*eqns)[e].coef[0] += I;
+}
+
+
+// update a coefficient of a variable that already exists in mappedvars
+
+void Constraint_Handle::update_coef_during_simplify(Variable_ID D, coef_t I) {
+  assert(D != 0);
+  int col = c->get_column(D);
+  (*eqns)[e].coef[col] += I;
+}
+
+void Constraint_Handle::update_const_during_simplify(coef_t I) {
+  (*eqns)[e].coef[0] += I;
+}
+
+//
+// Get functions.
+//
+
+coef_t Constraint_Handle::get_coef(Variable_ID v) const {
+  assert(this->relation()->is_simplified());
+  assert(v != 0);
+  int col = c->find_column(v);
+  if(col == 0) {
+    return 0;
+  }
+  else {
+    return (*eqns)[e].coef[col];
+  }
+} 
+
+coef_t Constraint_Handle::get_coef_during_simplify(Variable_ID v) const {
+  assert(v != 0);
+  int col = c->find_column(v);
+  if(col == 0) {
+    return 0;
+  }
+  else {
+    return (*eqns)[e].coef[col];
+  }
+} 
+
+coef_t Constraint_Handle::get_const() const {
+  assert(this->relation()->is_simplified());
+  return((*eqns)[e].coef[0]);
+}
+
+coef_t Constraint_Handle::get_const_during_simplify() const {
+  return((*eqns)[e].coef[0]);
+}
+
+Variable_ID Constraint_Handle::get_local(const Global_Var_ID G) {
+  return relation()->get_local(G);
+}
+
+Variable_ID Constraint_Handle::get_local(const Global_Var_ID G, Argument_Tuple of) {
+  return relation()->get_local(G, of);
+}
+
+void Constraint_Handle::finalize() {
+  c->n_open_constraints--;
+}
+
+void Constraint_Handle::multiply(int multiplier) {
+  int i;
+  assert(! this->relation()->is_simplified());
+  for(i=1; i<=c->problem->nVars; i++) {
+    (*eqns)[e].coef[i] = (*eqns)[e].coef[i] * multiplier;
+  }
+  (*eqns)[e].coef[0] = (*eqns)[e].coef[0] * multiplier;
+}
+
+Rel_Body *Constraint_Handle::relation() const {
+  return c->relation();
+}
+
+
+//
+// Variables of constraint iterator.
+//
+Constr_Vars_Iter::Constr_Vars_Iter(const Constraint_Handle &ch, bool _wild_only): eqns(ch.eqns), e(ch.e), prob(ch.c->problem), vars(ch.c->mappedVars), wild_only(_wild_only) {
+  assert(vars.size() == prob->nVars);
+  for(current=1; current<=prob->nVars; current++) {
+    if((*eqns)[e].coef[current]!=0 && 
+       (!wild_only || vars[current]->kind()==Wildcard_Var)) 
+      return;
+  }
+}
+
+int Constr_Vars_Iter::live() const {
+  return (current<=prob->nVars);
+}
+
+
+void Constr_Vars_Iter::operator++() { this->operator++(0); }
+
+void Constr_Vars_Iter::operator++(int) {
+  for(current++ ; current <=prob->nVars; current++)
+    if((*eqns)[e].coef[current]!=0 && 
+       (!wild_only || vars[current]->kind()==Wildcard_Var))
+      return;
+}
+
+
+Variable_ID Constr_Vars_Iter::curr_var() const {
+  assert(current <= prob->nVars);
+  return vars[current];
+}
+
+coef_t Constr_Vars_Iter::curr_coef() const {
+  assert(current <= prob->nVars);
+  return (*eqns)[e].coef[current];
+}
+
+Variable_Info Constr_Vars_Iter::operator*() const {
+  assert(current <= prob->nVars);
+  return Variable_Info(vars[current],(*eqns)[e].coef[current]);
+}
+
+//
+// Constraint iterator.
+//
+Constraint_Iterator Conjunct::constraints() {
+  return Constraint_Iterator(this);
+}
+
+Constraint_Iterator::Constraint_Iterator(Conjunct *_c): c(_c), current(0),
+                                                        last(c->problem->nGEQs-1), eqns(&(c->problem->GEQs)) {
+  if(!this->live()) (*this)++; // switch to EQ's if no GEQs
+}
+
+int Constraint_Iterator::live() const {
+  return current <=last;
+}
+
+void Constraint_Iterator::operator++() {
+  this->operator++(0);
+}
+
+void Constraint_Iterator::operator++(int) {
+  if(++current > last)
+    if(eqns == &(c->problem->GEQs)) { // Switch to EQs
+      eqns = &(c->problem->EQs);
+      current = 0;
+      last = c->problem->nEQs-1;
+    }
+}
+
+Constraint_Handle Constraint_Iterator::operator*() {
+  assert((c && eqns && current <= last) && "Constraint_Iterator::operator*: bad call");
+  return Constraint_Handle(c,eqns,current);
+} 
+
+Constraint_Handle Constraint_Iterator::operator*() const {
+  assert((c && eqns && current <= last) && "Constraint_Iterator::operator*: bad call");
+  return Constraint_Handle(c,eqns,current);
+} 
+
+
+//
+// EQ iterator.
+//
+EQ_Iterator Conjunct::EQs() {
+  return EQ_Iterator(this);
+}
+
+EQ_Iterator::EQ_Iterator(Conjunct *_c) : c(_c) {
+  last = c->problem->nEQs-1;
+  current = 0;
+}
+
+int EQ_Iterator::live() const {
+  return current <= last;
+}
+
+void EQ_Iterator::operator++() {
+  this->operator++(0);
+}
+
+void EQ_Iterator::operator++(int) {
+  current++;
+}
+
+EQ_Handle EQ_Iterator::operator*() {
+  assert((c && current <= last) && "EQ_Iterator::operator*: bad call");
+  return EQ_Handle(c,current);
+} 
+
+EQ_Handle EQ_Iterator::operator*() const {
+  assert((c && current <= last) && "EQ_Iterator::operator*: bad call");
+  return EQ_Handle(c,current);
+} 
+
+
+//
+// GEQ iterator.
+//
+GEQ_Iterator Conjunct::GEQs() {
+  return GEQ_Iterator(this);
+}
+
+GEQ_Iterator::GEQ_Iterator(Conjunct *_c) : c(_c) {
+  last = c->problem->nGEQs-1;
+  current = 0;
+}
+
+int GEQ_Iterator::live() const {
+  return current <= last;
+}
+
+void GEQ_Iterator::operator++() {
+  this->operator++(0);
+}
+
+void GEQ_Iterator::operator++(int) {
+  current++;
+}
+
+
+GEQ_Handle GEQ_Iterator::operator*() {
+  assert((c && current <= last) && "GEQ_Iterator::operator*: bad call");
+  return GEQ_Handle(c,current);
+} 
+
+GEQ_Handle GEQ_Iterator::operator*() const {
+  assert((c && current <= last) && "GEQ_Iterator::operator*: bad call");
+  return GEQ_Handle(c,current);
+} 
+
+
+void copy_constraint(Constraint_Handle H, const Constraint_Handle initial) {
+  // skip_set_checks++;
+//  assert(H.relation()->n_inp() == initial.relation()->n_inp());
+//  assert(H.relation()->n_out() == initial.relation()->n_out());
+    
+  H.update_const_during_simplify(initial.get_const_during_simplify());
+  if (H.relation() == initial.relation())  {
+    for( Constr_Vars_Iter C(initial, false); C.live() ; C.next()) {
+      assert(C.curr_var()->kind()!= Forall_Var &&
+             C.curr_var()->kind()!= Exists_Var);
+      if (C.curr_var()->kind()!= Wildcard_Var)
+        H.update_coef_during_simplify(C.curr_var(), C.curr_coef());
+      else
+        // Must add a new wildcard,
+        // since they can't be used outside local Conjunct
+        H.update_coef_during_simplify(H.c->declare(), C.curr_coef());
+    }
+  }
+  else {
+    Rel_Body *this_rel = H.relation();
+    for( Constr_Vars_Iter C(initial, false); C.live() ; C.next()) {
+      switch (C.curr_var()->kind()) {
+      case Forall_Var:
+      case Exists_Var:
+        assert(0 && "Can't copy quantified constraints across relations");
+        break;
+      case Wildcard_Var:
+        // for each wildcard var we see, create a new wildcard
+        // will lead to lots of wildcards, but Wayne likes it
+        // that way
+      {
+        H.update_coef_during_simplify(H.c->declare(), C.curr_coef());
+        break;
+      }
+      case Input_Var: //use variable_ID of corresponding position
+      {
+        int pos = C.curr_var()->get_position();
+        assert(this_rel->n_inp() >= pos);
+        Variable_ID V = this_rel->input_var(pos);
+        H.update_coef_during_simplify(V, C.curr_coef());
+        break;
+      }
+      case Output_Var:  //use variable_ID of corresponding position
+      {
+        int pos = C.curr_var()->get_position();
+        assert(this_rel->n_out() >= pos);
+        Variable_ID V = this_rel->output_var(pos);
+        H.update_coef_during_simplify(V, C.curr_coef());
+        break;
+      }
+
+      case Global_Var:  // get this Global's Var_ID in this relation
+      {
+        Variable_ID V;
+        Global_Var_ID G = C.curr_var()->get_global_var();
+        if (G->arity() == 0)
+          V = this_rel->get_local(G);
+        else 
+          V = this_rel->get_local(G,C.curr_var()->function_of());
+        H.update_coef_during_simplify(V, C.curr_coef());
+        break;
+      }
+      default:
+        assert(0 && "copy_constraint: variable of impossible type");
+      }
+    }
+  }
+  // skip_set_checks--;
+}
+
+} // namespace