+ case CTT_SREF:
+ / * evans 2001-07-24: constants should use the original term * /
+ if (!constraintTerm_canGetValue (t))
+ {
+ sRef snew;
+ DPRINTF ((message("Doing sRef_fixInvarConstraint for %q ",
+ constraintTerm_unparse (t) ) ));
+
+ snew = fixSref (ct, s, constraintTerm_getSRef(t));
+
+ ret = constraintExpr_makeTermsRef(snew);
+
+ constraintExpr_free (e);
+
+ DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
+ constraintExpr_print (ret) ) ));
+ / *@-branchstate@* /
+ } / *@=branchstate@* /
+
+ break;
+ default:
+ BADEXIT;
+ }
+
+ return ret;
+
+}
+#endif
+
+/*drl moved from constriantTerm.c 5/20/001*/
+/*@only@*/ static constraintExpr
+doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
+{
+ constraintTerm t;
+
+ constraintExprData data;
+
+ constraintExprKind kind;
+
+ constraintExpr ret;
+
+
+ llassert(constraintExpr_isDefined (e) );
+
+ data = e->data;
+
+ kind = e->kind;
+
+
+
+ llassert(kind == term);
+
+ t = constraintExprData_termGetTerm (data);
+ llassert (constraintTerm_isDefined(t) );
+
+ ret = e;
+
+ DPRINTF (("Fixing: %s", constraintExpr_print (e)));
+
+ switch (constraintTerm_getKind(t))
+ {
+ case CTT_EXPR:
+ DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
+ fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
+ break;
+ case CTT_INTLITERAL:
+ DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
+ break;
+ case CTT_SREF:
+ /* evans 2001-07-24: constants should use the original term */
+ if (!constraintTerm_canGetValue (t))
+ {
+ DPRINTF ((message("Doing sRef_fixConstraintParam for %q ",
+ constraintTerm_unparse (t) ) ));
+ ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
+
+ constraintExpr_free (e);
+
+ DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
+ constraintExpr_print (ret) ) ));
+ /*@-branchstate@*/
+ } /*@=branchstate@*/
+
+ break;
+ default:
+ BADEXIT;
+ }
+
+ return ret;
+
+}
+
+
+#if 0
+bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
+{
+ if (constraintTerm_hasTerm (expr->term, term) )
+ return TRUE;
+
+ if ((expr->expr) != NULL)
+ {
+ return ( constraintExpr_includesTerm (expr->expr, term) );
+ }
+ return FALSE;
+
+}
+#endif
+
+/*drl added 6/11/01 */
+bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
+{
+
+ llassert(constraintExpr_isDefined (c) );
+
+ if ( ! (constraintExpr_isDefined (c) ) )
+ return FALSE;
+
+ if (c->kind == binaryexpr)
+ return TRUE;
+
+ else
+ return FALSE;
+}
+
+/*drl added 8/08/001 */
+bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
+{
+ llassert(constraintExpr_isDefined (c) );
+
+ if (c->kind == term)
+ return TRUE;
+
+ else
+ return FALSE;
+}
+
+/*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr c) /*@*/
+{
+ constraintTerm term;
+
+ llassert(constraintExpr_isDefined (c) );
+
+ llassert(constraintExpr_isTerm(c) );
+
+ term = constraintExprData_termGetTerm(c->data);
+
+ return term;
+}
+
+static void binaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
+{
+ constraintExpr expr1;
+ constraintExprBinaryOpKind binaryOp;
+ constraintExpr expr2;
+
+
+ binaryOp = constraintExprData_binaryExprGetOp (data);
+
+ fprintf(f, "%d\n", (int) binaryOp);
+
+ expr1 = constraintExprData_binaryExprGetExpr1 (data);
+ expr2 = constraintExprData_binaryExprGetExpr2 (data);
+
+ fprintf(f, "e1\n");
+
+ constraintExpr_dump(expr1, f);
+
+ fprintf(f, "e2\n");
+ constraintExpr_dump(expr2, f);
+}
+
+
+static constraintExpr binaryExpr_undump (FILE *f)
+{
+ constraintExpr expr1;
+ constraintExprBinaryOpKind binaryOp;
+ constraintExpr expr2;
+
+ constraintExpr ret;
+
+
+
+ char * str;
+ char * os;
+
+ os = mstring_create (MAX_DUMP_LINE_LENGTH);
+
+ str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ if (! mstring_isDefined(str) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
+ binaryOp = (constraintExprBinaryOpKind) reader_getInt(&str);
+
+ str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ if (! mstring_isDefined(str) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
+ reader_checkChar (&str, 'e');
+ reader_checkChar (&str, '1');
+
+ expr1 = constraintExpr_undump (f);
+
+ str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ reader_checkChar (&str, 'e');
+ reader_checkChar (&str, '2');
+
+ expr2 = constraintExpr_undump (f);
+
+ ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
+ ret->data = constraintExprData_binaryExprSetOp(ret->data, binaryOp);
+
+ free(os);
+ return ret;
+}
+
+
+
+static void unaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
+{
+
+ constraintExpr expr;
+ constraintExprUnaryOpKind unaryOp;
+
+ unaryOp = constraintExprData_unaryExprGetOp (data);
+
+ fprintf(f, "%d\n", (int) unaryOp);
+
+ expr = constraintExprData_unaryExprGetExpr (data);
+
+ constraintExpr_dump(expr, f);
+}
+
+static constraintExpr unaryExpr_undump ( FILE *f)
+{
+
+ constraintExpr expr;
+ constraintExprUnaryOpKind unaryOp;
+ constraintExpr ret;
+
+ char * str;
+ char * os;
+
+ str = mstring_create (MAX_DUMP_LINE_LENGTH);
+ os = str;
+ str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ if (! mstring_isDefined(str) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
+ unaryOp = (constraintExprUnaryOpKind) reader_getInt(&str);
+
+ expr = constraintExpr_undump (f);
+
+ ret = constraintExpr_makeUnaryOp (expr, unaryOp);
+
+ free(os);
+
+ return ret;
+}
+
+void constraintExpr_dump (/*@observer@*/ constraintExpr expr, FILE *f)
+{
+ constraintExprKind kind;
+ constraintTerm t;
+
+
+ llassert(constraintExpr_isDefined(expr) );
+
+ DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
+ constraintExpr_unparse(expr)
+ ) ));
+
+ kind = expr->kind;
+
+ fprintf(f,"%d\n", (int) kind);
+
+ switch (kind)
+ {
+ case term:
+ t = constraintExprData_termGetTerm (expr->data);
+ constraintTerm_dump (t, f);
+ break;
+ case unaryExpr:
+ unaryExpr_dump (expr->data, f);
+ break;
+ case binaryexpr:
+ binaryExpr_dump (expr->data, f);
+ break;
+ }
+}
+
+/*@only@*/ constraintExpr constraintExpr_undump (FILE *f)
+{
+ constraintExprKind kind;
+ constraintTerm t;
+ constraintExpr ret;
+
+ char * s;
+ char * os;
+
+ s = mstring_create (MAX_DUMP_LINE_LENGTH);
+
+ os = s;
+
+ s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+ if (! mstring_isDefined(s) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
+ kind = (constraintExprKind) reader_getInt(&s);
+
+ free (os);
+
+ switch (kind)
+ {
+ case term:
+ t = constraintTerm_undump (f);
+ ret = constraintExpr_makeTerm(t);
+ break;
+ case unaryExpr:
+ ret = unaryExpr_undump (f);
+ break;
+ case binaryexpr:
+ ret = binaryExpr_undump (f);
+ break;
+ }
+
+ return ret;
+
+}
+
+int constraintExpr_getDepth (constraintExpr ex)
+{
+ int ret;
+
+ constraintExprKind kind;
+
+ llassert (ex != NULL);
+
+ kind = ex->kind;
+
+ switch (kind)
+ {
+ case term:
+ ret = 1;
+ break;
+ case unaryExpr:
+ ret = constraintExpr_getDepth (constraintExprData_unaryExprGetExpr (ex->data) );
+ ret++;