+ if (exprNode_isError (child1) && !exprNode_isError(child2) )
+ {
+ constraintList_free(parent->requiresConstraints);
+
+ parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
+ constraintList_free(parent->ensuresConstraints);
+
+ parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
+ DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
+ constraintList_print( child2->requiresConstraints),
+ constraintList_print (child2->ensuresConstraints)
+ )
+ ));
+ return;
+ }
+ else
+ {
+ llassert(exprNode_isError(child2) );
+ //parent->requiresConstraints = constraintList_makeNew();
+ //parent->ensuresConstraints = constraintList_makeNew();
+ return;
+ }
+ }
+
+ llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) );
+
+ DPRINTF( (message ("Child constraints are %s %s and %s %s",
+ constraintList_print (child1->requiresConstraints),
+ constraintList_print (child1->ensuresConstraints),
+ constraintList_print (child2->requiresConstraints),
+ constraintList_print (child2->ensuresConstraints)
+ ) ) );
+
+
+ constraintList_free(parent->requiresConstraints);
+
+ parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
+
+ if ( context_getFlag (FLG_ORCONSTRAINT) )
+ temp = reflectChangesOr (child2->requiresConstraints, child1->ensuresConstraints);
+ else
+ temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
+
+ temp2 = constraintList_mergeRequires (parent->requiresConstraints, temp);
+ constraintList_free(parent->requiresConstraints);
+ constraintList_free(temp);
+
+ parent->requiresConstraints = temp2;
+
+ DPRINTF( (message ("Parent requires constraints are %s ",
+ constraintList_print (parent->requiresConstraints)
+ ) ) );
+
+ constraintList_free(parent->ensuresConstraints);
+
+ parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
+ child2->ensuresConstraints);
+
+
+ DPRINTF( (message ("Parent constraints are %s and %s ",
+ constraintList_print (parent->requiresConstraints),
+ constraintList_print (parent->ensuresConstraints)
+ ) ) );
+
+}
+
+
+
+
+/*@only@*/ constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
+{
+ constraintList ret;
+ ret = constraintList_makeNew();
+ constraintList_elements (list1, el)
+ {
+
+ DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
+ if (!resolve (el, list2) )
+ {
+ constraint temp;
+ temp = constraint_copy(el);
+ ret = constraintList_add (ret, temp);
+ }
+ else
+ {
+ DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
+ }
+ } end_constraintList_elements;
+
+ return ret;
+}
+
+
+
+/* tries to resolve constraints in list pre2 using post1 */
+/*@only@*/ constraintList reflectChangesFreePre (/*@only@*/ constraintList pre2, /*@observer@*/ constraintList post1)
+{
+ constraintList ret;
+
+ ret = reflectChanges (pre2, post1);
+
+ constraintList_free (pre2);
+
+ return ret;
+}
+
+
+/* tries to resolve constraints in list pre2 using post1 */
+/*@only@*/ constraintList reflectChanges (/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
+{
+
+ constraintList ret;
+ constraint temp;
+ constraint temp2;
+
+ ret = constraintList_makeNew();
+ DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
+
+ constraintList_elements (pre2, el)
+ {
+ if (!resolve (el, post1) )
+ {
+ temp = substitute (el, post1);
+ if (!resolve (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 (temp);
+ // if (context_getFlag (FLG_ORCONSTRAINT) )
+ temp2 = inequalitySubstitute (temp2, post1);
+ if (!resolve (temp2, post1) )
+ {
+ temp2 = inequalitySubstituteUnsound (temp2, post1);
+ if (!resolve (temp2, post1) )
+ ret = constraintList_add (ret, temp2);
+ }
+ }
+ constraint_free(temp);
+ }
+ } end_constraintList_elements;
+
+ DPRINTF((message ("reflectChanges: returning %s", constraintList_print(ret) ) ) );
+ return ret;
+}
+
+
+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;