+static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint or)
+{
+ constraint c;
+ c = orig;
+
+ DPRINTF((message("constraint_addor: oring %s onto %s", constraint_printOr(or), constraint_printOr(orig) ) ));
+
+ while (c->or != NULL)
+ {
+ c = c->or;
+ }
+ c->or = constraint_copy(or);
+
+ DPRINTF((message("constraint_addor: returning %s",constraint_printOr(orig) ) ));
+
+ return orig;
+}
+
+
+static bool resolveOr (/*@observer@*/ constraint c, /*@observer@*/ constraintList list)
+{
+ constraint temp;
+
+ DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(list) ) ));
+ temp = c;
+
+ do
+ {
+ if (resolve (temp, list) )
+ return TRUE;
+ temp = temp->or;
+ }
+ 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;
+
+ if (!resolveOr (c, post1) )
+ {
+
+ temp = 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 it anyway
+ temp2 = constraint_copy (c);
+ // if (context_getFlag (FLG_ORCONSTRAINT) )
+ temp2 = inequalitySubstitute (temp2, post1);
+ if (!resolveOr (temp2, post1) )
+ {
+ temp2 = inequalitySubstituteUnsound (temp2, post1);
+ if (!resolveOr (temp2, post1) )
+ {
+ if (!constraint_same (temp, temp2) )
+ temp = constraint_addOr (temp, temp2);
+ *resolved = FALSE;
+
+ constraint_free(temp2);
+ constraint_free(c);
+
+ return temp;
+ }
+ }
+
+ constraint_free(temp2);
+ }
+ constraint_free(temp);
+ }
+
+ constraint_free(c);
+
+ *resolved = TRUE;
+ return NULL;
+
+
+
+}
+
+static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * resolved)
+{
+ constraint ret;
+ constraint next;
+ constraint curr;
+
+ *resolved = FALSE;
+ ret = constraint_copy(c);
+ 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 reflectChangesOr (constraintList pre2, constraintList post1)
+{
+ bool resolved;
+ constraintList ret;
+ constraint temp;
+ ret = constraintList_makeNew();
+ DPRINTF((message ("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 ret when resolved is false because ret is null*/
+ llassert(temp == NULL);
+ }
+
+ } end_constraintList_elements;