Allow limited forms of incrementality

[LeventErkok]

Full incremental interface to SMT-solvers would be tough, since the "single-call" assumption is rather baked-in to our architecture.

However, a limited form of interactivity might be possible. Currently, we already do an automated interaction sequence: We keep the pipe open and send commands on demand to receive model values. One idea would be to allow the users to tell us what other commands to send down.

Currently, the interaction looks like this:

1. Construct the problem
2. Send it down the pipe o the solver, wait for response
3. If unsat, kill the pipe and quit
4. If sat, send model-extraction commands

Step 3 and 4 above is the "hard-coded" continuation that we have. Why not give access to this to the user? Instead of doing this part automatically, we can allow the user to observe the output from the solver, and then issue commands as they wish. They can even further issue new constraints, and new-check-sat commands. In particular, steps 3-4 can be repeated ad infinitum: Instead of kiling the pipe.

There's some design space issues to consider here: Exactly what that continuation should look like. I suspect a Request-Response like framework; might fit the best. But this should be possible to implement after a couple of iterations on the precise use cases.

[rohit507]

Seconding this.

Just to add some specificity to the question of interface: For my own work with SBV, incrementality would be incredibly useful. I'm not sure how possible this would be, but an ideal world would allow us to work with a problem as follows.

• Set up initial model of constraints A (our general model of the problem space)
• Push an additional set of constraints B (the specific problem we want to solve) onto the stack.
• Solve A + B
  • If SAT : (gather example solutions of different broad classes)
    • Pop B
    • Add further constraints to A (To prevent us from finding solutions of the same class as this one)
    • Push B
    • Rinse / Repeat (Stopping when you get any UNSAT results, a few good solutions are fine)
  • If UNSAT : (find some information about why B is UNSAT)
    • Pop B
    • Relax the problem B to get a weaker B'
    • Push B'
    • Rinse / Repeat (Stopping when you can't narrow down the problematic portion of B further)

I'm not sure how easily we could express this model with the continuation framework you're thinking of, but it seems like it should be possible. There'd be a bunch of state to drag around though, especially when we're trying to shrink the failing problem to find the explicit issue.

P.S: I'm not sure how reasonable this is, but I'm willing to help if you have any guidance on how.

[LeventErkok]

Thanks for the feedback!

Indeed, I think this'll be a useful addition. SBV is already structured so it passes a "standard" continuation to the engine that orchestrates the communication. My current thinking is as follows. We'll add a new field to SMTConfig, so the user can "register" his/her own continuation:

   interactWithSolver :: Maybe Cont

where Cont is something like:

  type Cont = ([String] -> IO [SMTResult])   -- the "standard continuation of SBV
            -> (Request -> IO Response)      -- the interaction function
            -> IO [SMTResult]                -- final result

That is, the user will get a handle onto what SBV would have done (the first argument); but he can first communicate with the solver via the interaction function, eventually returning the results back. He can call the standard continuation eventually, or can also completely ignore it. The rest of SBV would just work as is.

The question here is what should Request and Response be?

A simple answer is merely String. That is, the user sends arbitrary strings down, and the solver responds with arbitrary strings. Another could be a simple AST (maybe just SExprs) with an extensible DSL around it that contains a bunch of cooked commands, along the lines of check-sat, assert, push, pop etc. No doubt we'll have to carry around some state, but it's hard to guess what exactly that should be.

I think I'll start with experimenting with String for the time being and see what sort of a design emerges. If you can craft a particular test scenario that I can play with (i.e., an actual SBV program), and what sort of interaction you'd do, that would really help!

[rohit507]

Hmm, is the idea that we'd only be able to call [String] -> IO [SMTResult] once in interactWithSolver?

Also, I'm not clear on whether there's a good way to get the [String] needed to add constraints to the Symbolic that the first closure is evaluating over.

I'll see if I can't whip together a simple toy example of my use case.

[LeventErkok]

I'm not sure.. Hence my hesitation to commit to any particular design for the time being. I'm experimenting currently in the "interactive" branch, but it isn't usable quite yet. You're welcome to take a look.

But yes: A toy example that would serve your needs would greatly help the design.

[LeventErkok]

Update as of May 25, 2017.

The "interactive" branch has come along quite a bit. For instance, we can now run:

import Data.SBV
import Data.SBV.Control

p :: Goal
p = do a <- sInteger "a"
       b <- sInteger "b"

       constrain $ a .>= 0
       constrain $ b .>= 0

       query $ do assert $ a+2 .>= 5
                  assert $ a+b .< 12

                  cs <- checkSat

                  case cs of
                    Sat -> io $ putStrLn "Everything is OK"
                    r   -> error $ "Something went bad, got: " ++ show r

                  -- Query a/b
                  av <- getValue a
                  bv <- getValue b
                  io $ putStrLn $ "(a,b) = " ++ show (av,bv)

                  -- Now assert so that we get even a bigger value..
                  assert $ a .> literal (av + bv)

                  -- Tell SBV to resume, i.e., call check-sat, collect-the results, etc.
                  sbvResume

main :: IO ()
main = print =<< satWith z3{verbose=False} p

And it behaves as you would expect. Dropping this note here to seek feedback from early adaptors. (@rohit507)

[LeventErkok]

@rohit507 This is now merged into the master branch, so you can directly experiment from there. No need to build from the interactive branch.

[LeventErkok]

@rohit507 The new query infrastructure is handling this sort of thing, though the design is quite different than what I sketched above. (As expected.) Please see the new code (to be released on Hackage soon) and do let me know if you've any issues. Closing this ticket in the meantime, feel free to open it if you find issues with the new system.