+/* 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;
+
+ llassert(constraint_isDefined(orig) );
+
+ 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;
+
+ llassert(constraint_isDefined(c) );
+
+ 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_isDefined (c ) );
+
+ DPRINTF((message("doResolve:: call on constraint c = : %q and constraintList %q",
+ constraint_printOr(c), constraintList_print(post1)
+ )
+ ));
+
+ if (!resolveOr (c, post1) )
+ {
+
+ temp = constraint_substitute (c, post1);
+
+ DPRINTF((message("doResolve:: after substitute temp is %q",
+ constraint_printOr(temp)
+ )
+ ));
+
+ 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);
+ 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) )
+ {
+ /* drl added 8/28/2002*/
+ /*make sure that the information from
+ a post condition like i = i + 1 is transfered
+ */
+ constraint tempSub;
+ tempSub = constraint_substitute (temp2, post1);
+
+ DPRINTF((
+ message("doResolve: adding %s ",
+ constraint_printOr(tempSub)
+ )
+ ));
+
+ DPRINTF((
+ message("doResolve: not adding %s ",
+ constraint_printOr(temp2)
+ )
+ ));
+
+ temp = constraint_addOr (temp, tempSub);
+ constraint_free(tempSub);
+
+ }
+ if (!constraint_same (temp, temp3) && !constraint_same (temp3, temp2) )
+ {
+ /* drl added 8/28/2002*/
+ /*make sure that the information from
+ a post condition like i = i + 1 is transfered
+ */
+ constraint tempSub;
+
+ tempSub = constraint_substitute (temp3, post1);
+
+ DPRINTF((
+ message("doResolve: adding %s ",
+ constraint_printOr(tempSub)
+ )
+ ));
+
+
+ DPRINTF((
+ message("doResolve: not adding %s ",
+ constraint_printOr(temp3)
+ )
+ ));
+
+ temp = constraint_addOr (temp, tempSub);
+
+ constraint_free(tempSub);
+ }
+ *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;
+
+ llassert(constraint_isDefined(c) );
+
+ ret = constraint_copy(c);
+
+ llassert(constraint_isDefined(ret) );
+
+ 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;