add record types and tuple types to symbolic package

[Stephen Siegel]

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.

[Stephen Siegel]

For now, tuple types are all I need.

[ywei]

Operations for tuple type added in the SymUniverseIF. Implementation code will be added soon.

[ywei]

Add corresponding tuple type and tuple expression to the symbolic package. Also implemented the corresponding create/read/write methods in symbolic universe.

[ywei]

We decided that record type is not required at this time.