+/* 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;
+
+ ret = doResolve (ret, post1, resolved);
+
+ if (*resolved)
+ {
+ if (next != NULL)
+ constraint_free(next);
+
+ /*we don't need to free ret when resolved is false because ret is null*/
+ llassert(ret == NULL);
+
+ return NULL;
+ }
+
+ while (next != NULL)
+ {
+ curr = next;
+ next = curr->or;
+ curr->or = NULL;
+
+ curr = doResolve (curr, post1, resolved);
+
+ if (*resolved)
+ {
+ /* curr is null so we don't try to free it*/
+ llassert(curr == NULL);
+
+ if (next != NULL)
+ constraint_free(next);
+
+ constraint_free(ret);
+ return NULL;
+ }
+ ret = constraint_addOr (ret, curr);
+ constraint_free(curr);
+ }
+ return ret;
+}
+
+/* tries to resolve constraints in list pr2 using post1 */
+/*@only@*/ constraintList constraintList_reflectChangesOr (constraintList pre2, constraintList post1)
+{
+ bool resolved;
+ constraintList ret;
+ constraint temp;
+ ret = constraintList_makeNew();
+ DPRINTF((message ("constraintList_reflectChangesOr: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
+
+ constraintList_elements (pre2, el)
+ {
+ temp = doResolveOr (el, post1, &resolved);
+
+ if (!resolved)
+ {
+ ret = constraintList_add(ret, temp);
+ }
+ else
+ {
+ /* we don't need to free temp when
+ resolved is false because temp is null */
+ llassert(temp == NULL);
+ }
+
+ } end_constraintList_elements;