Remove explicit `IO` from our SMT interface

[VictorCMiraldo]

What

This PR does two large, but intertwined, pieces of work:

1. Isolates the interface to the SMT solver from the rest of the code, preparing pirouette to interact with a solver through:

   solve :: SharedContext lang -> Problem lang res -> res

2. In this process, I also used the more modern typed-process to launch the SMT process instead of how SimpleSMT used to do it.
3. Cleans and refactors a lot of the symbolic evaluation engine

Partially applying something to solve should cause further calls to share that shared context. Here's a gist showing a little experiment I did in this direction: https://gist.github.com/VictorCMiraldo/b7c448bb2bcf4b49962082970d61f64a

It doesn't use that solve function just yet, we need some further cleanup (#106) to start using it. Nevertheless, the interface with the symbolic evaluation engine is already defined in terms of a problem GADT:

data SolverProblem lang :: * -> * where
  CheckProperty :: (LanguagePretty lang) => CheckPropertyProblem lang -> SolverProblem lang PruneResult
  CheckPath :: CheckPathProblem lang -> SolverProblem lang Bool

It is only inside the interpretation of those problems that we interact directly with the solver; anywhere else in the symbolic engine we just call solveProblem for now and in a next PR, will become just solve.

Why

Having an explicit IO monad (or a MonadIO m constraint) simply because we need to talk to an SMT solver is a bad idea. For one, it means we cannot be lazy enough and are always performing more work than we should (#97); Secondly, this implies an unnecessary sentimentality to our backend: why can't we easily explore disjoint branches in parallel?

[VictorCMiraldo]

The last commit broke our tests. Our session with the solver now only sends empty assert statements:

[send: 120238] (set-option :produce-models true )
[send: 120238] (set-logic ALL )
[send: 120238] (declare-datatype pir_Delta ((pir_D (pir_D_1 Int ) (pir_D_2 Int ) ) ) )
[send: 120238] (declare-fun pir_odd (Int ) Bool )
[send: 120238] (declare-fun pir_even (Int ) Bool )
[send: 120238] (declare-fun pir_and (Bool Bool ) Bool )
[send: 120238] (declare-fun pir_snd (pir_Delta ) Int )
[send: 120238] (declare-fun pir_fst (pir_Delta ) Int )
[send: 120238] (declare-fun pir_ohearn (pir_Delta ) pir_Delta )
[send: 120238] (push 1 )
[send: 120238] (declare-fun pir___result () pir_Delta )
[send: 120238] (declare-fun pir_x () pir_Delta )
[send: 120238] (check-sat )
[recv: 120238] sat
[send: 120238] (pop 1 )
[send: 120238] (push 1 )
[send: 120238] (declare-fun pir___result () pir_Delta )
[send: 120238] (declare-fun pir_s0 () Int )
[send: 120238] (declare-fun pir_s1 () Int )
[send: 120238] (declare-fun pir_s2 () Int )
[send: 120238] (declare-fun pir_s3 () Int )
[send: 120238] (declare-fun pir_x () pir_Delta )
[send: 120238] (assert true ) -- HERE: empty assert!!
[send: 120238] (assert true )
[send: 120238] (check-sat )
[recv: 120238] sat

For the record, this is the same part of the session with the solver from commit 96b78f4a6a9c9ff1270319265531544c48a17979 (with the compilation error fixed)

[send: 115976] (set-option :produce-models true )
[send: 115976] (set-logic ALL )
[send: 115976] (declare-datatype pir_Delta ((pir_D (pir_D_1 Int ) (pir_D_2 Int ) ) ) )
[send: 115976] (declare-fun pir_odd (Int ) Bool )
[send: 115976] (declare-fun pir_even (Int ) Bool )
[send: 115976] (declare-fun pir_and (Bool Bool ) Bool )
[send: 115976] (declare-fun pir_snd (pir_Delta ) Int )
[send: 115976] (declare-fun pir_fst (pir_Delta ) Int )
[send: 115976] (declare-fun pir_ohearn (pir_Delta ) pir_Delta )
[send: 115976] (push 1 )
[send: 115976] (declare-fun pir___result () pir_Delta )
[send: 115976] (declare-fun pir_x () pir_Delta )
[send: 115976] (check-sat )
[recv: 115976] sat
[send: 115976] (pop 1 )
[send: 115976] (push 1 )
[send: 115976] (declare-fun pir___result () pir_Delta )
[send: 115976] (declare-fun pir_s0 () Int )
[send: 115976] (declare-fun pir_s1 () Int )
[send: 115976] (declare-fun pir_s2 () Int )
[send: 115976] (declare-fun pir_s3 () Int )
[send: 115976] (declare-fun pir_x () pir_Delta )
[send: 115976] (assert (= pir_x ((as pir_D pir_Delta ) pir_s2 pir_s3 ) ) ) -- HERE: Non-empty assert
[send: 115976] (assert (= pir___result ((as pir_D pir_Delta ) pir_s0 pir_s1 ) ) )
[send: 115976] (check-sat )
[recv: 115976] sat

[VictorCMiraldo]

While stripping everything Pirouette-specific from our API with the SMT solver, I noticed that we rely on PirouetteReadDefs in multiple places, which is perfectly fine. The problem is that PirouetteReadDefs has a few too many dependencies, in particular, the Logger monad and PrtOpts are no longer used, pirouette is not meant as a standalone executable anymore. These should be removed at some point.

[serras]

While stripping everything Pirouette-specific from our API with the SMT solver, I noticed that we rely on PirouetteReadDefs in multiple places, which is perfectly fine. The problem is that PirouetteReadDefs has a few too many dependencies, in particular, the Logger monad and PrtOpts are no longer used, pirouette is not meant as a standalone executable anymore. These should be removed at some point.

This would be very welcome! I've struggled with this in the past, mostly because of PirouetteReadDefs being defined as its own Reader thing, making it difficult to compose with others.

[VictorCMiraldo]

@0xd34df00d thanks for the review! I fixed all I could on this iteration and I added a lock to MStack to make sure no race condition can happen. That is untested code and I'll resort to really using it in the next PR; worst case scenario it doesn't work and we postpone relying on the pure solve for a while longer :)

edit: I removed the solve function; it is not used ATM and it should be introduced in its own PR, it's certainly a beast that needs attention

[VictorCMiraldo]

This would be very welcome! I've struggled with this in the past, mostly because of PirouetteReadDefs being defined as its own Reader thing, making it difficult to compose with others.

@serras, I hope to do this today!