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 record types and tuple types.  Now we need to add these to the symbolic package.  There should be a method to create such a type like

{{{
SymType newRecordType(String name, String[] fieldNames, SymType[] fieldTypes);
SymType newTypleType(String name, String[] fieldTypes);
}}}

A tuple type is just the special case of record type, where the fields are just named 0, 1, 2, ....

Then there must be methods to 

1. create a new SymExpression of a given record type, given the field values
2. read a field from a record
3. modify a field in a record.

Ditto for tuples.

This is similar in many ways to the way arrays are dealt with.

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;
}}}

"	enhancement	new	major		symbolic	1.0		record, tuple, struct, field, type