#5 "=" should be allowed on booleans

open
nobody
None
5
2009-05-09
2009-05-09
David Wagner
No

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

Discussion

  • David Wagner
    David Wagner
    2009-05-09

    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.