Let's add incremental solving #18
Description
What is incremental solving
The incremental solving is such that you can write a query, and then you can issue commands. For example after (check-sat) you can issue
(get-value (blah..)) to get the value of a single variable. Or you can add new constraints and then issue (check-sat) again. We use this in hevm when we need to see how many places you can just from a dynamic JMP. We simply solve the constraints, and get a solution. Then I ban the solution via an (assert ...), and issue another (check-sat). If it's UNSAT, I know there are no more solutions. If it's SAT, I add one more (assert..) banning the new solution, too, and then issue (check-sat) again. If it's UNSAT now, I know there are only 2 solutions, etc. This is MUCH-MUCH faster (hundreds of times faster, sometimes more), than running 2 separate SMT queries, because the solver reuses the lemmas it generated while solving the 1st query.
Deleting constraints via incremental solving
Also, you can do more fancy things. For example, let's say that I got a solution. But I want the buffer to be < 100 bytes. Maybe the solution could be minimised. So I do this:
(push)
(assert ... buffer size < 100 ...)
(check-sat)
If I get UNSAT then normally, I'm screwed because I can't make a SAT out of an UNSAT... but! I did a PUSH! So. I can pop. That makes it as if I have never added that assert. Yay! So now if I do:
(pop)
(check-sat)
The solution is still sat. Now I can do:
(push)
(assert ... buffer size < 500...)
(check-sat)
If I get SAT now, all good.
So push and pop allow you to kind of "erase" information. It's incredibly useful in many cases.
In general, incremental solving allows you to add new constraints, and with push-pop it also allows you to delete constraints. Note that obviously push-pop has some overhead so it's not recommended unless you really need it.
How could it be added to jsi
The thing is that it's not entirely clear what's the best way to add incremental solving. There is the obvious way, and the non-obvious way. The obvious way is that the first one that solves the original set of constraints you attach to the user's "terminal" and let them query that solver. Usually they only query for values of models. This is kind of "first one wins and gets to interact with the user". It's kinda shitty but not terrible. A better version is that you keep information what the user is doing with the 1st solver that solved, and if the others solve, too, you replay the interaction with them.
Say solver 1 solved first. You display that to the user. They say (assert xyz). Now solver 1 is busy. Solver 2 just finished. You replay (assert xyz) to solver 2. Solver 2 may actually finish this faster, so you display result from solver 2 to the user. Now user adds one more (assert abc). You send that to Solver 2. Solver 2 is busy. Meanwhile, solver 1 finished. You replay (assert abc) to solver 1, and it finishes immediately with unsat. Now you can terminate both solvers and display unsat to the user.