#5 "=" should be allowed on booleans

[David Wagner]

STP doesn't allow one to use the "=" binary operator on booleans. Example input:

x : BOOLEAN;
ASSERT(x = TRUE);
QUERY(FALSE);

and the output from STP:

syntax error: line 2
syntax error, unexpected '='
Fatal Error:

The prohibition on use of "=" for booleans is confusing and unexpected. It might be a bit more user-friendly to accept "=" on booleans.

The simplest workaround appears to be to replace "=" with "<=>". However "<=>" appears to have other problems. Another workaround is to use "NOT(x XOR y)" instead of "x = y", but this is not so readable. (There is no "NXOR".)

("&", "|", and "^" don't work either, but this seems less important.)

[David Wagner]

By the way, a minor consequence of the fact that "=" is not valid on BOOLEANs is that the output from "stp -p" is not actually valid STP. Example input:

x : BOOLEAN;
ASSERT(x);
QUERY(FALSE);

If you run "stp -p" on this input, you get:

Invalid.
ASSERT( x = TRUE );

However the latter line of the output is not valid STP syntax. A consequence is that you can't just take the output from "stp -p" and add it to your constraint system (if you wanted to do that for some reason). This seems of very low importance, but I thought I'd note it as a curiousity.