Work at SourceForge, help us to make it a better place! We have an immediate need for a Support Technician in our San Francisco or Denver office.

Close

#4 "stp -p" outputs non-constant counterexample

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

"stp -h" suggests that "stp -p" will print a counterexample, if the input formula is Invalid.
But, running "stp -p" on the following input:

x, t : BOOLEAN;
ASSERT(t <=> x);
ASSERT(x);
QUERY(FALSE);

yields the following output:

Invalid.
ASSERT( x = t );
ASSERT( t = TRUE );

This is not what I wanted to see. It is not a valid counterexample. A counterexample should provide a concrete assignment (assigning either TRUE or FALSE to each boolean variable) that satisfies all of the ASSERTs. Here we do not yet have a concrete assignment.

If STP could perform constant propagation, or instantiate its template-counterexample to get a fully concrete counterexample, that would be a lot more helpful.

In theory, I could write my own program to parse the output of STP and perform constant propagation myself, but this would be annoying to do, and would require every user of "stp -p" to implement this. Since STP has the internal data structures to do this, I think it makes more sense for STP to do this.

This behavior is on the latest Subversion head. I will note that a pre-compiled version of STP that I had downloaded earlier (which is presumably an earlier version of STP) does not have this problem; it outputs fully concrete counterexamples.

I haven't fully characterized the cases where this bug appears, but it appears to be related to the "<=>" operator. All of the examples I know of where this comes up, use "<=>".

Oddly, if I turn off optimization, I get fully concrete counterexamples. In other words, "stp -p -a" works where "stp -p" fails. If I swap the order of the two ASSERTs above, I get a fully concrete counterexample. If I change "t <=> x" to "NOT(t XOR x)" (which ought to be equivalent?), I get a fully concrete counterexample. This makes me wonder if there is something funny in the optimization or rewriting.

Discussion