new STP much slower on some examples

[ericwhitmansmith]

We upgraded STP today, and it seems much worse on some examples. For example, this query is easily proved Valid by the version of STP from May 27, 2022 (in 0.05 seconds), but the new STP was still running after 3 hours.

NODE0 : BITVECTOR(32);
QUERY (
LET NODE1 = (SBVLT(NODE0[31:0], 0bin00000000000000000000000000000000[31:0])) IN (
LET NODE2 = (NODE0[31:31]) IN (
LET NODE3 = BVSX(NODE2, 32) IN (
LET NODE4 = (0bin00000000000000000000000000000001[31:0] | NODE3[31:0]) IN (
LET NODE5 = (BVMULT(32,NODE0[31:0],NODE4[31:0])) IN (
LET NODE6 = (NODE0[31:0]) IN (
LET NODE7 = (NODE5 = NODE6) IN (
(NODE7 OR NODE1)))))))));

Can others reproduce the slowness? Thanks!

[aytey]

Just so we know, are you saying that:

• 93f7f2d works (== 0.05 seconds)
• 7b05982 doesn't work (>= 3 hours)

?

If you already know the commit hash that broke, that saves me the work!

[ericwhitmansmith]

What I'm seeing is this:

Version that works:

/usr/local/bin/stp-20220527 --version
STP version 2.3.3
STP version SHA string 8f47022

Version that doesn't work:

stp --version
STP version 2.3.3
STP version SHA string a9bc247

Unfortunately, I don't know when exactly it stopped working.

[ericwhitmansmith]

Okay, I believe the problem is introduced in d29b19d

[msoos]

Oh. Maybe we can revert that? @TrevorHansen what do you think? Is there something we can do to make sure we don't weaken our performance on other problems while making sure we are good on these too?

[TrevorHansen]

I’m not sure what’s best. Some background: * I ran STP on the smtlib qf_bv non-incremental benchmarks with different command line options, and updated the default configuration of STP to be the one that solved the most problems. * By setting command line options the old behaviour can be restored. * every change we make to STP that alters how problems are solved will make some problems slower to solve. To me it seems like we should have different configurations of STP for different types of problem/usage. So by default STP will continue to be tuned for smtlib, but for other uses, e.g. super easy problems, there’d be an —easy configuration. We’d just need problems to tune STP on?

…

On Wed, 19 Apr 2023 at 9:29 am, Mate Soos ***@***.***> wrote: Oh. Maybe we can revert that? @TrevorHansen <https://github.com/TrevorHansen> what do you think? Is there something we can do to make sure we don't weaken our performance on other problems while making sure we are good on these too? — Reply to this email directly, view it on GitHub <#463 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABPTD4WS7J3ISOY4Z3AG3G3XB4PVNANCNFSM6AAAAAAW6C45VU> . You are receiving this because you were mentioned.Message ID: ***@***.***>