+ constraintList ret;
+
+ ret = reflectChangesEnsures (pre2, post1);
+
+ constraintList_free(pre2);
+
+ return ret;
+}
+
+
+static bool constraint_conflict (constraint c1, constraint c2)
+{
+
+ if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
+ {
+ if (c1->ar == EQ)
+ if (c1->ar == c2->ar)
+ {
+ DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+ return TRUE;
+ }
+ }
+
+ DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+
+ return FALSE;
+
+}
+
+static void constraint_fixConflict ( constraint good, /*@observer@*/ constraint conflicting) /*@modifies good@*/
+{
+ if (conflicting->ar ==EQ )
+ {
+ good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
+ good = constraint_simplify (good);
+ }
+
+
+}
+
+static bool conflict (constraint c, constraintList list)
+{
+
+ constraintList_elements (list, el)
+ {
+ if ( constraint_conflict(el, c) )
+ {
+ constraint_fixConflict (el, c);
+ return TRUE;
+ }
+ } end_constraintList_elements;
+
+ return FALSE;
+
+}
+
+//check if constraint in list1 conflicts with constraints in List2. If so we
+//remove form list1 and change list2.
+constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
+{
+ constraintList ret;
+ ret = constraintList_makeNew();
+ llassert(constraintList_isDefined(list1) );
+ constraintList_elements (list1, el)
+ {
+ if (! conflict (el, list2) )
+ {
+ constraint temp;
+ temp = constraint_copy(el);
+ ret = constraintList_add (ret, temp);
+ }
+ } end_constraintList_elements;
+
+ return ret;
+}
+
+/*returns true if constraint post satifies cosntriant pre */
+static bool satifies (constraint pre, constraint post)
+{
+ if (constraint_isAlwaysTrue (pre) )
+ return TRUE;
+
+ if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
+ {
+ return FALSE;
+ }
+ if (post->expr == NULL)
+ {
+ llassert(FALSE);
+ return FALSE;
+ }
+
+ return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
+}
+
+
+bool resolve (/*@observer@*/ constraint c, /*@observer@*/ constraintList p)
+{
+ constraintList_elements (p, el)
+ {
+ if ( satifies (c, el) )
+ {
+ DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
+ return TRUE;
+ }
+ DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
+ }
+ end_constraintList_elements;
+ DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
+ return FALSE;
+}
+
+static bool arithType_canResolve (arithType ar1, arithType ar2)
+{
+ switch (ar1)
+ {
+ case GTE:
+ case GT:
+ if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
+ {
+ return TRUE;
+ }
+ break;
+
+ case EQ:
+ if (ar2 == EQ)
+ return TRUE;
+ break;
+
+ case LT:
+ case LTE:
+ // llassert(FALSE);
+ if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
+ return TRUE;
+ break;
+ default:
+ return FALSE;
+ }
+ return FALSE;
+}
+
+/* We look for constraint which are tautologies */
+
+bool constraint_isAlwaysTrue (/*@observer@*/ constraint c)
+{
+ constraintExpr l, r;
+ bool /*@unused@*/ lHasConstant, rHasConstant;
+ int /*@unused@*/ lConstant, rConstant;
+
+ l = c->lexpr;
+ r = c->expr;
+
+ DPRINTF(( message("constraint_IsAlwaysTrue:examining %s", constraint_print(c) ) ));
+
+ if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) )
+ {
+ int cmp;
+ cmp = constraintExpr_compare (l, r);
+ switch (c->ar)
+ {
+ case EQ:
+ return (cmp == 0);
+ case GT:
+ return (cmp > 0);
+ case GTE:
+ return (cmp >= 0);
+ case LTE:
+ return (cmp <= 0);
+ case LT:
+ return (cmp < 0);
+
+ default:
+ BADEXIT;
+ /*@notreached@*/
+ break;
+ }
+ }
+
+ if (constraintExpr_similar (l,r) )
+ {
+ switch (c->ar)
+ {
+ case EQ:
+ case GTE:
+ case LTE:
+ return TRUE;
+
+ case GT:
+ case LT:
+ break;
+ default:
+ BADEXIT;
+ /*@notreached@*/
+ break;
+ }
+ }
+
+ l = constraintExpr_copy (c->lexpr);
+ r = constraintExpr_copy (c->expr);
+
+ // l = constraintExpr_propagateConstants (l, &lHasConstant, &lConstant);
+ r = constraintExpr_propagateConstants (r, &rHasConstant, &rConstant);
+
+ if (constraintExpr_similar (l,r) && (rHasConstant ) )
+ {
+ DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) ));
+ DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant ) ));
+
+ constraintExpr_free(l);
+ constraintExpr_free(r);
+
+ switch (c->ar)
+ {
+ case EQ:
+ return (rConstant == 0);
+ case LT:
+ return (rConstant > 0);
+ case LTE:
+ return (rConstant >= 0);
+ case GTE:
+ return (rConstant <= 0);
+ case GT:
+ return (rConstant < 0);
+
+ default:
+ BADEXIT;
+ /*@notreached@*/
+ break;
+ }
+ }
+ else
+ {
+ constraintExpr_free(l);
+ constraintExpr_free(r);
+ DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) ));
+ return FALSE;
+ }
+
+ BADEXIT;
+}
+
+static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arithType ar2, /*@observer@*/ constraintExpr expr2)
+
+{
+ DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
+
+ if (! arithType_canResolve (ar1, ar2) )
+ return FALSE;
+
+ switch (ar1)
+ {
+ case GTE:
+ if (constraintExpr_similar (expr1, expr2) )
+ return TRUE;
+ /*@fallthrough@*/
+ case GT:
+ if (! (constraintExpr_canGetValue (expr1) &&
+ constraintExpr_canGetValue (expr2) ) )