symbolic expressions not being transformed into canonical form

[Stephen Siegel]

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).

[ywei]

Fixed. The symbolic universe will try to simplify each expression by querying CVC3.