summaryrefslogtreecommitdiff
path: root/omegalib/omega_lib/src/pres_col.cc
diff options
context:
space:
mode:
Diffstat (limited to 'omegalib/omega_lib/src/pres_col.cc')
-rw-r--r--omegalib/omega_lib/src/pres_col.cc104
1 files changed, 104 insertions, 0 deletions
diff --git a/omegalib/omega_lib/src/pres_col.cc b/omegalib/omega_lib/src/pres_col.cc
new file mode 100644
index 0000000..1569116
--- /dev/null
+++ b/omegalib/omega_lib/src/pres_col.cc
@@ -0,0 +1,104 @@
+#include <omega/pres_conj.h>
+#include <omega/RelBody.h>
+#include <omega/omega_i.h>
+
+namespace omega {
+
+//
+// Copy column fr_col of problem fp
+// to column to_col of problem tp.
+// Displacement for constraints in tp are start_EQ and start_GEQ.
+//
+void copy_column(Problem *tp, int to_col,
+ Problem *fp, int fr_col,
+ int start_EQ, int start_GEQ) {
+ checkVars(to_col);
+ assert(start_EQ + fp->nEQs <= tp->allocEQs);
+ assert(start_GEQ + fp->nGEQs <= tp->allocGEQs);
+
+ int i;
+ for(i=0; i<fp->nEQs; i++) {
+ tp->EQs[i+start_EQ].coef[to_col] = fp->EQs[i].coef[fr_col];
+ }
+ for(i=0; i<fp->nGEQs; i++) {
+ tp->GEQs[i+start_GEQ].coef[to_col] = fp->GEQs[i].coef[fr_col];
+ }
+}
+
+//
+// Zero column to_col of problem tp.
+// Displacement for constraints in to_conj are start_EQ and start_GEQ.
+// Number of constraints to zero are no_EQ and no_GEQ.
+//
+void zero_column(Problem *tp, int to_col,
+ int start_EQ, int start_GEQ,
+ int no_EQs, int no_GEQs) {
+ assert(start_EQ + no_EQs <= tp->allocEQs);
+ assert(start_GEQ + no_GEQs <= tp->allocGEQs);
+
+ int i;
+ for(i=0; i<no_EQs; i++) {
+ tp->EQs[i+start_EQ].coef[to_col] = 0;
+ }
+ for(i=0; i<no_GEQs; i++) {
+ tp->GEQs[i+start_GEQ].coef[to_col] = 0;
+ }
+}
+
+//
+// return column for D in conjunct
+//
+int Conjunct::get_column(Variable_ID D) {
+ int col = find_column(D);
+ if (col == 0) // if it does not already have a column assigned
+ col = map_to_column(D);
+ assert(col > 0); // Not substituted
+ return col;
+}
+
+//
+// Find column in conjunct.
+//
+int Conjunct::find_column(Variable_ID D) {
+ assert(D != 0);
+ int column = mappedVars.index(D);
+
+ // If it has been through the omega core (variablesInitialized),
+ // and it exists in the problem, check to see if it has been forwarded.
+ // This will likely only be the case if substitutions have been done;
+ // that won't arise in user code, only in print_with_subs and the
+ // Substitutions class.
+ if (problem->variablesInitialized && column > 0) {
+ assert(problem->forwardingAddress[column] != 0);
+ column = problem->forwardingAddress[column];
+ }
+ assert (column <= problem->nVars);
+ return column;
+}
+
+//
+// Create new column in conjunct.
+//
+int Conjunct::map_to_column(Variable_ID D) {
+ assert(D != 0);
+ // This heavy-duty assertion says that if you are trying to use a global
+ // var's local representative in a relation, that you have first told the
+ // relation that you are using it here. PUFS requires that we know
+ // all the function symbols that might be used in a relation.
+ // If one wanted to be less strict, one could just tell the relation
+ // that the global variable was being used.
+ assert(D->kind() != Global_Var ||
+ (relation()->has_local(D->get_global_var(), D->function_of())
+ && "Attempt to update global var without a local variable ID"));
+
+ cols_ordered = false; // extremely important
+ checkVars(problem->nVars+2);
+ int col = ++problem->nVars;
+ mappedVars.append(D);
+ problem->forwardingAddress[col] = col;
+ problem->var[col] = col;
+ zero_column(problem, col, 0, 0, problem->nEQs, problem->nGEQs);
+ return col;
+}
+
+} // namespace