smtlib-backends-z3 (empty) → 0.2

raw patch · 7 files changed

+253/−0 lines, 7 filesdep +basedep +bytestringdep +containerssetup-changed

Dependencies added: base, bytestring, containers, inline-c, smtlib-backends, smtlib-backends-tests, smtlib-backends-z3, tasty, tasty-hunit

Files

CHANGELOG.md +3/−0
LICENSE +21/−0
Setup.hs +3/−0
smtlib-backends-z3.cabal +68/−0
src/SMTLIB/Backends/Z3.hs +103/−0
tests/Examples.hs +29/−0
tests/Main.hs +26/−0

+ CHANGELOG.md view

@@ -0,0 +1,3 @@+# v0.2+- make test-suite compatible with `smtlib-backends-0.2`+- add usage examples in the test-suite

+ 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-z3.cabal view

@@ -0,0 +1,68 @@+name:               smtlib-backends-z3+version:            0.2+synopsis:           An SMT-LIB backend implemented using Z3's C API.+description:+  This library implements an SMT-LIB backend (in the sense of the smtlib-backends+  package) using inlined calls to Z3's C API. It is thus in particular faster+  than the standard backends relying on running solvers as external processes, as+  the OS doesn't need to spawn processes and handle pipes between them.++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+  subdir:   smtlib-backends-z3++source-repository this+  type:     git+  location: https://github.com/tweag/smtlib-backends+  tag:      0.2+  subdir:   smtlib-backends-z3++library+  hs-source-dirs:   src+  ghc-options:      -Wall -Wunused-packages+  exposed-modules:  SMTLIB.Backends.Z3+  build-depends:+      base             >=4.14    && <4.17.0+    , bytestring       >=0.10.12 && <0.11+    , containers       >=0.6.4   && <0.7+    , inline-c         >=0.9.1   && <0.10+    , smtlib-backends  >=0.2     && <0.3++  -- inspired from haskell-z3+  if (os(osx) || os(windows))+    extra-libraries: z3++  else+    extra-libraries:+      gomp+      z3+      gomp++  default-language: Haskell2010++test-suite test+  type:             exitcode-stdio-1.0+  hs-source-dirs:   tests+  main-is:          Main.hs+  other-modules:    Examples+  ghc-options:      -threaded -Wall -Wunused-packages+  build-depends:+      base+    , bytestring+    , smtlib-backends+    , smtlib-backends-tests+    , smtlib-backends-z3+    , tasty+    , tasty-hunit++  default-language: Haskell2010

+ src/SMTLIB/Backends/Z3.hs view

@@ -0,0 +1,103 @@+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TemplateHaskell #-}++-- | A module providing a backend that sends commands to Z3 using its C API.+module SMTLIB.Backends.Z3+  ( Handle,+    new,+    close,+    with,+    toBackend,+  )+where++import Control.Exception (bracket)+import Data.ByteString.Builder.Extra+  ( defaultChunkSize,+    smallChunkSize,+    toLazyByteStringWith,+    untrimmedStrategy,+  )+import qualified Data.ByteString.Char8 as BS+import qualified Data.ByteString.Lazy.Char8 as LBS+import qualified Data.Map as M+import Foreign.ForeignPtr (ForeignPtr, finalizeForeignPtr, newForeignPtr)+import Foreign.Ptr (Ptr)+import qualified Language.C.Inline as C+import qualified Language.C.Inline.Context as C+import qualified Language.C.Inline.Unsafe as CU+import qualified Language.C.Types as C+import SMTLIB.Backends (Backend (..))++data LogicalContext++C.context+  ( C.baseCtx+      <> C.fptrCtx+      <> C.bsCtx+      <> mempty+        { C.ctxTypesTable =+            M.singleton (C.TypeName "Z3_context") [t|Ptr LogicalContext|]+        }+  )+C.include "z3.h"++data Handle = Handle+  { -- | A black-box representing the internal state of the solver.+    context :: ForeignPtr LogicalContext+  }++-- | Create a new solver instance.+new :: IO Handle+new = do+  let ctxFinalizer =+        [C.funPtr| void free_context(Z3_context ctx) {+                 Z3_del_context(ctx);+                 } |]++  {-+  We set the error handler to ignore errors. That way if an error happens it doesn't+  cause the whole program to crash, and the error message is simply transmitted to+  the Haskell layer inside the output of the 'send' method.+  -}+  ctx <-+    newForeignPtr ctxFinalizer+      =<< [CU.block| Z3_context {+                 Z3_config cfg = Z3_mk_config();+                 Z3_context ctx = Z3_mk_context(cfg);+                 Z3_del_config(cfg);++                 void ignore_error(Z3_context c, Z3_error_code e) {}+                 Z3_set_error_handler(ctx, ignore_error);++                 return ctx;+                 } |]+  return $ Handle ctx++-- | Release the resources associated with a Z3 instance.+close :: Handle -> IO ()+close = finalizeForeignPtr . context++-- | Create a Z3 instance, use it to run a computation and release its resources.+with :: (Handle -> IO a) -> IO a+with = bracket new close++-- | Create a solver backend out of a Z3 instance.+toBackend :: Handle -> Backend+toBackend handle =+  Backend $ \cmd -> do+    let ctx = context handle+    let cmd' =+          LBS.toStrict $+            toLazyByteStringWith+              (untrimmedStrategy smallChunkSize defaultChunkSize)+              "\NUL"+              cmd+    LBS.fromStrict+      <$> ( BS.packCString+              =<< [CU.exp| const char* {+               Z3_eval_smtlib2_string($fptr-ptr:(Z3_context ctx), $bs-ptr:cmd')+               }|]+          )

+ tests/Examples.hs view

@@ -0,0 +1,29 @@+{-# LANGUAGE OverloadedStrings #-}++module Examples (examples) where++import SMTLIB.Backends (command, initSolver)+import qualified SMTLIB.Backends.Z3 as Z3+import Test.Tasty+import Test.Tasty.HUnit++-- | The examples for the 'Z3' backend (using Z3 as a library).+examples :: [TestTree]+examples =+  [testCase "basic use" basicUse]++-- | Basic use of the 'Z3' backend.+basicUse :: IO ()+basicUse =+  -- 'Z3.with' runs a computation using the 'Z3' backend+  Z3.with $ \handle -> do+    -- first, we make the z3 handle into an actual backend+    let backend = Z3.toBackend handle+    -- then, we create a solver out of the backend+    -- we enable queuing (it's faster !)+    solver <- initSolver backend True+    -- we send a basic command to the solver and ignore the response+    -- we can write the command as a simple string because we have enabled the+    -- OverloadedStrings pragma+    _ <- command solver "(get-info :name)"+    return ()

+ tests/Main.hs view

@@ -0,0 +1,26 @@+{-# LANGUAGE OverloadedStrings #-}++import qualified Data.ByteString.Lazy.Char8 as LBS+import Examples (examples)+import SMTLIB.Backends+import SMTLIB.Backends.Tests+import qualified SMTLIB.Backends.Z3 as Z3+import Test.Tasty+import Test.Tasty.HUnit++main :: IO ()+main = do+  defaultMain $+    testGroup "Tests" $+      [ testBackend "Basic examples" validSources z3,+        testGroup "API usage examples" examples,+        testBackend "Error handling" failingSources z3+      ]+  where+    z3 todo = Z3.with $ todo . Z3.toBackend+    validSources = filter (\source -> name source `notElem` ["assertions", "unsat cores"]) sources+    failingSources =+      [ Source "invalid command" $ \solver -> do+          result <- command solver "this is not a valid command!!!"+          assertBool ("Expecting error message, got: " ++ LBS.unpack result) $ "(error" `LBS.isPrefixOf` result+      ]