New release 2.4

[aytey]

@mikhailramalho has requested a new STP release, as we've had some API extensions since 2.3.3.

This is an issue to ensure we don't forget.

I'd like to not do this until #378 in.

[rgov]

I would think CI is about project infrastructure and not part of the release. If there are changes to how STP is built or integrated that would affect users, we may want to give the version number a larger bump to signify this, though I don't know if we are using semantic versioning yet.

[aytey]

Yeah, maybe you're right ... my concern is that we don't actually have CI until that branch is in (given Travis is gone).

[rgov]

In that case, sounds like there's a good argument to merge it in, as long as there are issues tracking future work (static builds etc.)

[ccadar]

Just curious, is there a new release being planned? The last one is really old now.

[TrevorHansen]

I'm keen to get a release out early next month. That'd fit in nicely with SMTCOMP 2022.

Of the listed issues, only #388 seems important to me. Is there anything else that should go in?

I'm working on a bunch of general speedups, most substantially to the PropagateEqualities class.

[msoos]

By the way, I think I made CMS a ton faster, in case you are interested. You'd need to use the devel version, but frankly, I should release too. TrevorHansen you have access to https://github.com/meelgroup/cryptominisat/, can you please check the devel branch there? Please use a877c721e44887646f3f1421c9ff4bf69102d399 -- I am working on it quite a bit and it may be broken on other commits.

[TrevorHansen]

To me these looks like nice cases to get done before the next release, which I'll work through unless anyone has better ideas?

• [] Get bitvector model as a vector of bool #357
• [] Additional SMTLib2 support #365
• [] Correcting command line argument for '--max_time' #373
• [] Solution soundness issue on QF_BV formula #383
• [] STP doesn't parse benchmark. #388
• [] Find maximum value? #425
• [] Make Minisat optional? #433

I've been tuning STP to solve difficult problems faster, not to solve easy problems faster. So the next release might be worse for some uses. Does anyone have problems that they'd like the next release to not be slower on?

[251]

I've been tuning STP to solve difficult problems faster, not to solve easy problems faster. [...] Does anyone have problems that they'd like the next release to not be slower on?

The easy problems actually. I gave a Dagstuhl talk a few years ago and one advantage of STP over other solvers (at that time) was the very low "start-up time". KLEE benefits a lot from it as many queries are trivially to solve in common benchmarks:

Please keep that use-case in mind.

[TrevorHansen]

Thanks @251.

The trend with STP has been to add more processing steps, which are justified for hard problems, but probably aren't required for yours. Is there some way for me to easily generate a typical KLEE workload so that I can check that the current master version isn't much slower?

I'd like to look at it a bit, but now it seems to me that it'd be nice to have something like "easy mode", where most of the simplifications are disabled, STP is run with a timeout (e.g. 1 second), then if the timeout is exceeded, STP automatically re-runs the problem in "hard mode" (with the expensive simplifications enabled).

[msoos]

Another option to consider is to run them as inprocessing rather than preprocessing ;) That would allow as to delay the processing to a later time, so it doesn't eat into the startup time. However, I am not sure if some preprocessing can be moved to inprocessing, to be honest. CryptoMiniSat does almost everything as inprocessing now, so startup time is minimized.

[TrevorHansen]

Another option to consider is to run them as inprocessing rather than preprocessing ;)

That's a nice idea. In my time there's only been a little bit of effort to get STP faster on easy problems. It's plausible to me that we could get STP 5x faster on easy problems without much effort.

[251]

I ran a single(!) experiment with different STP versions / SAT solvers. Below are 1h KLEE runs with DFS search heuristic - that means the queries are typically easier to solve and the experiments more deterministic (y-axis is number of explored instructions). As you can see, there is in most cases not much of an improvement, in some cases performance even decreases (expand, expr, nl).

The default heuristic is more non-deterministic, so take the results with a grain of salt.

Another observation is that STP master runs more often out of memory (2.3.3: 1x, master: 5x).

[aytey]

there is in most cases not much of an improvement, in some cases performance even decreases (expand, expr, nl).

So overall worse?

Another observation is that STP master runs more often out of memory (2.3.3: 1x, master: 5x).

Are you able to share a smt2 file (or something similar) for an instance that now times-out when previously it completed?

[251]

Just checked, three cases are crashes (maybe an API change?), e.g.:

error: STP Error: SimplifyAtomicFormula: NO atomic formula of the kind

error: STP Error: TransformArray: An array write is being attempted on a non-array

(one unclear due to truncated logs)

[aytey]

What's the easiest way for me to reproduce these myself? Build KLEE against STP's master and run a certain test?

[251]

Let me try to log the queries for the crashing cases.

[251]

I looked at nl as outlier - one of the queries that seem to run longer on my machine with STP master is attached (.kquery and .smt2).

> kleaver nl_26004.kquery

takes <0.1s with STP 2.3.3 and 3-4s with master (60d74cb). Is this sth. you can reproduce?

nl_26004.zip

[TrevorHansen]

Thanks @251

When I try with smtlib2 format it takes about 150ms. See below.

Could it be that case that reading from the counter example is really slow? When I try from the command-line the "get-value" doesn't work properly. You're doing this via the C-api right?

./stp --version && time ./stp  ../nl_26004.smt2 
STP version 2.3.3
STP version SHA string 60d74cb2489c70f017d72be14c0dee1a30baf2c9
STP compilation options CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS =  -Wall -Wextra -Wunused -pedantic -Wsign-compare -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -fno-omit-frame-pointer | COMPILE_DEFINES =  -D__STDC_LIMIT_MACROS -DUSE_CRYPTOMINISAT | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATICCOMPILE = OFF | TUNE_NATIVE = OFF | COVERAGE = OFF | FORCE_CMS = OFF | LIBS = /usr/local/lib/libminisat.so | ENABLE_TESTING = ON | ENABLE_PYTHON_INTERFACE = ON | PYTHON_EXECUTABLE = /usr/bin/python | PYTHON_LIBRARY =  | PYTHON_INCLUDE_DIRS =  |  | compilation date time = Aug  9 2022 09:42:23
c compiled with gcc version 8.4.0
sat
unsupported
unsupported
unsupported
unsupported
unsupported
unsupported
unsupported
unsupported
unsupported
unsupported
unsupported

real	0m0.147s
user	0m0.140s
sys	0m0.004s

[251]

Could it be that case that reading from the counter example is really slow?

Maybe but why?

You're doing this via the C-api right?

Yes: https://github.com/klee/klee/blob/c9de012b07426435b8bd3bb29082fbceddf403a3/lib/Solver/STPSolver.cpp#L201

[TrevorHansen]

Could it be that case that reading from the counter example is really slow?

Maybe but why?

When I run the smtlib2 instance on my machine it takes about 150ms, about 30x faster than when you run it via the C-api. The smtlib2 format doesn't do the get-values, unlike the c-api, that's why there's all the unsupported output, so I thought it was the most likely reason for the time discrepancy.

To progress this, what'd be most helpful for us is a script, e.g. a dockerfile, that does the runs that you used to produce the nl example file. Searching quickly I see these coreutils instructions. Is this what we need to do?

[mikhailramalho]

ping. Any updates on releasing a new version?