+/*@access exprNode @*/
+
+
+static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c);
+
+
+static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
+ /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
+
+/* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
+
+/* { */
+/* char *t; */
+/* int c; */
+/* constraint ret; */
+/* ret = constraint_makeNew(); */
+/* llassert (sRef_isValid(x) ); */
+/* if (!sRef_isValid(x)) */
+/* return ret; */
+
+
+/* ret->lexpr = constraintExpr_makeTermsRef (x); */
+/* #warning fix abstraction */
+
+/* if (relOp.tok == GE_OP) */
+/* ret->ar = GTE; */
+/* else if (relOp.tok == LE_OP) */
+/* ret->ar = LTE; */
+/* else if (relOp.tok == EQ_OP) */
+/* ret->ar = EQ; */
+/* else */
+/* llfatalbug(message ("Unsupported relational operator") ); */
+
+
+/* t = cstring_toCharsSafe (exprNode_unparse(cconstant)); */
+/* c = atoi( t ); */
+/* ret->expr = constraintExpr_makeIntLiteral (c); */
+
+/* ret->post = TRUE; */
+/* // ret->orig = ret; */
+/* DPRINTF(("GENERATED CONSTRAINT:")); */
+/* DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
+/* return ret; */
+/* } */
+
+
+static void
+advanceField (char **s)
+{
+ checkChar (s, '@');
+}
+
+
+
+constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
+{
+ char *t;
+ int c;
+ constraint ret;
+ ret = constraint_makeNew();
+ llassert (l!=NULL);
+
+ ret->lexpr = constraintExpr_copy (l);
+
+
+ if (relOp.tok == GE_OP)
+ ret->ar = GTE;
+ else if (relOp.tok == LE_OP)
+ ret->ar = LTE;
+ else if (relOp.tok == EQ_OP)
+ ret->ar = EQ;
+ else
+ llfatalbug(message("Unsupported relational operator") );
+
+
+ t = cstring_toCharsSafe (exprNode_unparse(cconstant));
+ c = atoi( t );
+ ret->expr = constraintExpr_makeIntLiteral (c);
+
+ ret->post = TRUE;
+ // ret->orig = ret;
+ DPRINTF(("GENERATED CONSTRAINT:"));
+ DPRINTF( (message ("%s", constraint_print(ret) ) ) );
+ return ret;
+}
+
+bool constraint_same (constraint c1, constraint c2)
+{
+
+ if (c1->ar != c2->ar)
+ return FALSE;
+
+ if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
+ return FALSE;
+
+ if (!constraintExpr_similar (c1->expr, c2->expr) )
+ return FALSE;
+
+ return TRUE;
+}
+
+constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
+{
+ constraint ret;
+ ret = constraint_makeNew();
+ llassert (l !=NULL);
+
+ ret->lexpr = constraintExpr_copy (l);
+
+ if (relOp.tok == GE_OP)
+ ret->ar = GTE;
+ else if (relOp.tok == LE_OP)
+ ret->ar = LTE;
+ else if (relOp.tok == EQ_OP)
+ ret->ar = EQ;
+ else
+ llfatalbug( message("Unsupported relational operator") );
+
+ ret->expr = constraintExpr_copy (r);
+
+ ret->post = TRUE;
+
+ ret->orig = constraint_copy(ret);
+
+ ret = constraint_simplify (ret);
+
+ // ret->orig = ret;
+ DPRINTF(("GENERATED CONSTRAINT:"));
+ DPRINTF( (message ("%s", constraint_print(ret) ) ) );
+ return ret;
+}