id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
82	add record types and tuple types to symbolic package	Stephen Siegel	ywei	"CVC3 supports tuple types.  Now we need to add these to the symbolic package.  There should be a method to create such a type like

{{{
SymType newTupleType(String name, SymType[] fieldTypes);
SymExpression tupleRead(SymExpression tuple, int index);
SymExpression tupleWrite(SymExpression tuple, int index, SymExpression element);
SymExpression tupleExpression(SymType tupleType, SymExpression[] elements)
}}}



The following is an example of using the CVC3 interactive to create a record type:

{{{
Reference : TYPE = [# pid         : INT,
                      stackIndex  : INT,
                      id          : INT,
                      numLinks    : INT,
                      links       : ARRAY INT OF INT #];

a,a1 : ARRAY INT OF INT;
ASSERT a1 = a WITH [0] := 3, [1]:=5;
r1 : Reference = (# pid:=2, stackIndex:=-1, id:=3, numLinks:=2, links:=a1 #);
TRANSFORM r1;
}}}

The CVC3 manual has a detailed description of record types.   Here is a simple example from the manual:

{{{
% Record updates

Item: TYPE = [# key: INT, weight: REAL #];

x:  Item = (# key := 23, weight := 43/10 #);

x1: Item = x WITH .weight := 48;
}}}

Similar methods work for tuple types.
"	enhancement	closed	major		symbolic	1.0	fixed	record, tuple, struct, field, type