tuple support in symbolic universe incomplete

[Stephen Siegel]

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.

[ywei]

In order to do this, I think I need to add tuple read/write expression classes to the symbolic package, similar to array read/write expression. Because the index of a tuple read/write expression could be a symbolic value. Is it correct?

[Stephen Siegel]

I think we can assume the index to a tuple expression will always be a concrete int. A C or MiniMP program always has to specify the name of the field of a record in order to access that field (e.g., x.next) so we will always know exactly what the field is.

However I still think you need a TupleRead and TupleWrite class because the other component(s) of the tuple reference may be symbolic. For example, a TupleRead object comprises two components: the original tuple expression and the (concrete) field index. The original tuple expression does not necessarily have a concrete representation. Similarly, a TupleWrite class comprises 3 components: original tuple expression, concrete int index, and new value. The first and third are not necessarily concrete.

It is very similar to the case of arrays. The only difference is that a tuple index is always concrete, whereas in an array it could be any symbolic expression.

And I believe CVC3 supports tuple-real and tuple-write expressions. At least, that's what it seems like from the command line interface. I believe we have some examples of that checked in to the notes directory.

[ywei]

Yes, CVC3 supports such kind of tuple operations. They are called tuple select and tuple update.

[ywei]

Since CVC3 is required to construct a tuple read/write expression, the configuration should turn on the simplify_prover flag to use the simplification mechanism in CVC3.

[ywei]

I mean if the users want to use CVC3 to simplify tuple read/write expression, they should set the simplify_prover option to true. Otherwise the tuple read/write expression will keep the way they are.

[Stephen Siegel]

Is that the way it works for arrays? It should be similar, I think.

[ywei]

tuple read and tuple write expression classes added to the symbolic package. Also modified the theorem prover class to handle these two expressions as well as the tuple expression class.