+/* tries to resolve constraints in list pre2 using post1 */
+/*@only@*/ constraintList constraintList_reflectChanges(/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
+{
+ constraintList temp;
+
+ if ( context_getFlag (FLG_ORCONSTRAINT) )
+
+ temp = constraintList_reflectChangesOr (pre2, post1);
+ else
+ temp = reflectChangesNoOr(pre2, post1);
+
+ return temp;
+}
+
+static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint orConstr)
+{
+ constraint c;
+ c = orig;
+
+ DPRINTF((message("constraint_addor: oring %s onto %s", constraint_printOr(orConstr), constraint_printOr(orig) ) ));
+
+ while (c->or != NULL)
+ {
+ c = c->or;
+ }
+
+ c->or = constraint_copy(orConstr);
+
+ DPRINTF((message("constraint_addor: returning %s",constraint_printOr(orig) ) ));
+
+ return orig;
+}
+
+
+static bool resolveOr ( /*@temp@*/ constraint c, /*@observer@*/ /*@temp@*/ constraintList list)
+{
+ constraint temp;
+
+ int numberOr;
+
+ numberOr = 0;
+ DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(list) ) ));
+ temp = c;
+
+ do
+ {
+ if (constraintList_resolve (temp, list) )
+ return TRUE;
+ temp = temp->or;
+ numberOr++;
+ llassert(numberOr <= 10);
+ }
+ while (constraint_isDefined(temp));
+
+ return FALSE;
+}
+
+/*This is a "helper" function for doResolveOr */
+
+static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList post1, bool * resolved)
+{
+ constraint temp;
+
+ llassert(constraint_isUndefined (c->or ) );
+
+ if (!resolveOr (c, post1) )
+ {
+
+ temp = constraint_substitute (c, post1);
+
+ if (!resolveOr (temp, post1) )
+ {
+ // try inequality substitution
+ constraint temp2;
+
+ // the inequality substitution may cause us to lose information
+ //so we don't want to store the result but we do anyway
+ temp2 = constraint_copy (c);
+ // if (context_getFlag (FLG_ORCONSTRAINT) )
+ temp2 = inequalitySubstitute (temp2, post1);
+ if (!resolveOr (temp2, post1) )
+ {
+ constraint temp3;
+ temp3 = constraint_copy(temp2);
+
+ temp3 = inequalitySubstituteStrong (temp3, post1);
+ if (!resolveOr (temp3, post1) )
+ {
+ temp2 = inequalitySubstituteUnsound (temp2, post1);
+ if (!resolveOr (temp2, post1) )
+ {
+ if (!constraint_same (temp, temp2) )
+ temp = constraint_addOr (temp, temp2);
+
+ if (!constraint_same (temp, temp3) && !constraint_same (temp3, temp2) )
+ temp = constraint_addOr (temp, temp3);
+
+ *resolved = FALSE;
+
+ constraint_free(temp2);
+ constraint_free(temp3);
+ constraint_free(c);
+
+ return temp;
+ }
+ constraint_free(temp2);
+ constraint_free(temp3);
+ }
+ else
+ {
+ constraint_free(temp2);
+ constraint_free(temp3);
+ }
+ }
+ else
+ {
+ constraint_free(temp2);
+ }
+
+ }
+ constraint_free(temp);
+ }
+ constraint_free(c);
+
+ *resolved = TRUE;
+ return NULL;
+
+}
+
+static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c, constraintList post1, /*@out@*/bool * resolved)
+{
+ constraint ret;
+ constraint next;
+ constraint curr;
+
+
+ DPRINTF(( message("doResolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(post1) ) ));
+
+
+
+ *resolved = FALSE;
+
+
+ ret = constraint_copy(c);
+
+ if (constraintList_isEmpty(post1) )
+ {
+ return ret;
+ }
+
+ next = ret->or;
+ ret->or = NULL;