Incremental STP Solving

[sreeshmaheshwar]

Does STP support incremental SMT solving techniques (e.g. reusing learned lemmas) as other solvers, like Z3 and Boolector, do? (Can't find anything in the docs about how to enable an incremental solver and haven't observed any performance differences when using push and pop in an incremental way with STP + QF_ABV + MiniSat)

If not, are there any plans for this?

[TrevorHansen]

You're right that STP doesn't keep learned clauses between invocations to the SAT solver.

It has some simple analysis, for example if a problem is unsatisfiable, and you push more frames onto it, STP knows that those problems are unsatisfiable, too.

There's lots we could do to make incremental solving faster. If you provide us with some problems that are really slow with STP ,compared to other solvers, I'll see if there's anything we can do to speed up STP's solving of them.