id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
8	symbolic expressions not being transformed into canonical form	Stephen Siegel	ywei	"It seems like the symbolic expressions are not being transformed into a canonical form.  Examples:

X0<4&&!X0<0&&2<X0&&1<X0&&0<X0&&X0<4&&!X0<0&&!X2==0&&!X2<0

is a path condition in the tile (compare) example.   If this is passed to CVC3's ""transform"" command, it will simplify it by (for example) removing one of the duplicate ""X0<4"" clauses.

Another example:

hi = X2+X2;

would be simplified to 2*X2.

The ""canonicalization"" should be happening after every symbolic operation is performed.  It can be achieved by calling CVC3's ""transform"" function, then reading the expression back into a symbolic expression.

I _think_ (but am not absolutely sure) this would be a good idea, mainly because it will improve state matching (you will be able to tell that two states are equal).
"	enhancement	closed	major		symbolic	1.0	fixed	canonicalization