Module

Mycroft.Solver

Package
purescript-mycroft
Repository
afcondon/purescript-mycroft

The session layer: a solver kept in lockstep. The simple-smt trick — set :print-success immediately, so every command produces exactly one response s-expression and framing is trivial: write one form, read one form.

The transport is abstracted: newSolver speaks to a subprocess (z3 -in -smt2 by default); other backends (the WASM build, a remote solver) supply their own Transport via newSolverWith and inherit the whole veneer above this module unchanged.

#Solver Source

newtype Solver

#SolverConfig Source

type SolverConfig = { args :: Array String, cmd :: String, log :: Maybe (String -> Effect Unit) }

#Callbacks Source

type Callbacks = { onChunk :: String -> Effect Unit, onFailure :: String -> Effect Unit }

What a backend receives: where to deliver solver output (chunked, any framing) and where to report a dead backend.

#Transport Source

type Transport = { close :: Effect Unit, send :: String -> Effect Unit }

What a backend provides: write one line of SMTLib2, and tear the backend down (called at most once, by stop).

#newSolver Source

newSolver :: SolverConfig -> Aff Solver

The subprocess backend.

#newSolverWith Source

newSolverWith :: { log :: Maybe (String -> Effect Unit), start :: Callbacks -> Aff Transport } -> Aff Solver

Bring up a solver over any transport and put it in lockstep mode.

#command Source

command :: Solver -> SExpr -> Aff SExpr

Send one command, await its one response. Lockstep discipline: callers issue one command at a time (all the veneer functions do).

#ackCommand Source

ackCommand :: Solver -> SExpr -> Aff Unit

A command whose only acceptable response is the atom success.

Modules
Mycroft.SExpr
Mycroft.SmtLib
Mycroft.Solver