packages feed

smtlib-backends (empty) → 0.2

raw patch · 5 files changed

+202/−0 lines, 5 filesdep +basedep +bytestringsetup-changed

Dependencies added: base, bytestring

Files

+ CHANGELOG.md view
@@ -0,0 +1,11 @@+see also the changelogs of `smtlib-backends-tests`, `smtlib-backends-process` and +`smtlib-backends-z3`++# v0.2+- split the `Process` module into its own library+- rename `SMTLIB.Backends`'s `ackCommand` to `command_`+- remove logging abilities+  - the user can always surround `command` or `command_` with their own logging+    functions+- improve read-me+
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) Tweag I/O Limited.++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple++main = defaultMain
+ smtlib-backends.cabal view
@@ -0,0 +1,39 @@+name:               smtlib-backends+version:            0.2+synopsis:+  Low-level functions for SMT-LIB-based interaction with SMT solvers. ++description:+  This library provides an extensible interface for interacting with SMT solvers+  using SMT-LIB. The smtlib-backends-process provides a backend that runs solvers+  as external processes, and the smtlib-backends-z3 package provides a backend that+  uses inlined calls to Z3's C API.++license:            MIT+license-file:       LICENSE+author:             Quentin Aristote+maintainer:         quentin.aristote@tweag.io+build-type:         Simple+category:           SMT+cabal-version:      >=1.10+extra-source-files: CHANGELOG.md++source-repository head+  type:     git+  location: https://github.com/tweag/smtlib-backends++source-repository this+  type:     git+  location: https://github.com/tweag/smtlib-backends+  tag:      0.2++library+  hs-source-dirs:   src+  ghc-options:      -Wall -Wunused-packages+  exposed-modules:  SMTLIB.Backends+  other-extensions: Safe+  build-depends:+      base        >=4.14    && <4.17.0+    , bytestring  >=0.10.12 && <0.11++  default-language: Haskell2010
+ src/SMTLIB/Backends.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE OverloadedStrings #-}++module SMTLIB.Backends (Backend (..), Solver, initSolver, command, command_) where++import Data.ByteString.Builder (Builder)+import qualified Data.ByteString.Lazy.Char8 as LBS+import Data.Char (isSpace)+import Data.IORef (IORef, atomicModifyIORef, newIORef)+import Data.List (intersperse)+import Prelude hiding (log)++-- | The type of solver backends. SMTLib2 commands are sent to a backend which+-- processes them and outputs the solver's response.+data Backend = Backend+  { -- | Send a command to the backend.+    send :: Builder -> IO LBS.ByteString+  }++type Queue = IORef Builder++-- | Push a command on the solver's queue of commands to evaluate.+-- The command must not produce any output when evaluated, unless it is the last+-- command added before the queue is flushed.+putQueue :: Queue -> Builder -> IO ()+putQueue q cmd = atomicModifyIORef q $ \cmds ->+  (cmds <> cmd, ())++-- | Empty the queue of commands to evaluate and return its content as a bytestring+-- builder.+flushQueue :: Queue -> IO Builder+flushQueue q = atomicModifyIORef q $ \cmds ->+  (mempty, cmds)++-- | A solver is essentially a wrapper around a solver backend. It also comes with+-- a function for logging the solver's activity, and an optional queue of commands+-- to send to the backend.+--+-- A solver can either be in eager mode or lazy mode. In eager mode, the queue of+-- commands isn't used and the commands are sent to the backend immediately. In+-- lazy mode, commands whose output are not strictly necessary for the rest of the+-- computation (typically the ones whose output should just be "success") and that+-- are sent through 'command_' are not sent to the backend immediately, but+-- rather written on the solver's queue. When a command whose output is actually+-- necessary needs to be sent, the queue is flushed and sent as a batch to the+-- backend.+--+-- Lazy mode should be faster as there usually is a non-negligible constant+-- overhead in sending a command to the backend. But since the commands are sent by+-- batches, a command sent to the solver will only produce an error when the queue+-- is flushed, i.e. when a command with interesting output is sent. You thus+-- probably want to stick with eager mode when debugging. Moreover, when commands+-- are sent by batches, only the last command in the batch may produce an output+-- for parsing to work properly. Hence the ":print-success" option is disabled in+-- lazy mode, and this should not be overriden manually.+data Solver = Solver+  { -- | The backend processing the commands.+    backend :: Backend,+    -- | An optional queue to write commands that are to be sent to the solver lazily.+    queue :: Maybe Queue+  }++-- | Create a new solver and initialize it with some options so that it behaves+-- correctly for our use.+-- In particular, the "print-success" option is disabled in lazy mode. This should+-- not be overriden manually.+initSolver ::+  Backend ->+  -- | whether to enable lazy mode (see 'Solver' for the meaning of this flag)+  Bool ->+  IO Solver+initSolver solverBackend lazy = do+  solverQueue <-+    if lazy+      then do+        ref <- newIORef mempty+        return $ Just ref+      else return Nothing+  let solver = Solver solverBackend solverQueue+  if lazy+    then return ()+    else -- this should not be enabled when the queue is used, as it messes with parsing+    -- the outputs of commands that are actually interesting+    -- TODO checking for correctness and enabling laziness can be made compatible+    -- but it would require the solver backends to return several outputs at once+    -- alternatively, we may consider that the user wanting both features should+    -- implement their own backend that deals with this+      setOption solver "print-success" "true"+  setOption solver "produce-models" "true"+  return solver++-- | Have the solver evaluate a SMT-LIB command.+-- This forces the queued commands to be evaluated as well, but their results are+-- *not* checked for correctness.+command :: Solver -> Builder -> IO LBS.ByteString+command solver cmd = do+  send (backend solver)+    =<< case queue solver of+      Nothing -> return $ cmd+      Just q -> (<> cmd) <$> flushQueue q++-- | A command with no interesting result.+-- In eager mode, the result is checked for correctness.+-- In lazy mode, (unless the queue is flushed and evaluated+-- right after) the command must not produce any output when evaluated, and+-- its output is thus in particular not checked for correctness.+command_ :: Solver -> Builder -> IO ()+command_ solver cmd =+  case queue solver of+    Nothing -> do+      res <- send (backend solver) cmd+      if trim res == "success"+        then return ()+        else+          fail $+            unlines+              [ "Unexpected result from the SMT solver:",+                "  Expected: success",+                "  Got: " ++ show res+              ]+    Just q -> putQueue q cmd+  where+    trim = LBS.dropWhile isSpace . LBS.reverse . LBS.dropWhile isSpace . LBS.reverse++setOption :: Solver -> Builder -> Builder -> IO ()+setOption solver name value = command_ solver $ list ["set-option", ":" <> name, value]++list :: [Builder] -> Builder+list bs = "(" <> mconcat (intersperse " " bs) <> ")"