id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
157	tuple support in symbolic universe incomplete	Stephen Siegel	ywei	"The following code in the {{{SymUniverse}}} assumes that an expression of tuple type will be an instance of {{{SymTupleExpression}}}.

{{{

	public SymExpression tupleRead(SymExpression assumption,
			SymExpression tupleExpr, int index) {
		if (!(tupleExpr instanceof SymTupleExpression)) {
			throw new RuntimeException(
					""The symbolic expression being read must be a symbolic tuple expression."");
		}
		return ((SymTupleExpression) tupleExpr).getElement(index);
	}

	public SymExpression tupleWrite(SymExpression assumption,
			SymExpression tupleExpr, int index, SymExpression expr) {
		if (!(tupleExpr instanceof SymTupleExpression)) {
			throw new RuntimeException(
					""The symbolic expression being read must be a symbolic tuple expression."");
		}
		return ((SymTupleExpression) tupleExpr).setElement(expr, index);
	}
}}}


It is possible to have a symbolic expression of tuple type even though the expression is not an instance of {{{SymTupleExpression}}}.  For example, suppose {{{a}}} is an array of tuples, and {{{X}}} is a symbolic constant of integer type.   Then {{{a[X]}}} has tuple type even though it is an instance of subscript expression, not tuple expression.

This code should instead call the corresponding methods in CVC3 (tupleRead, tupleWrite, or whatever they are called), which can handle all these situations correctly.

"	defect	closed	major	Release 1.0	symbolic	1.0	fixed	tuple symbolic