smtlib-backends-z3 0.3 → 0.3.1

raw patch · 4 files changed

+45/−9 lines, 4 filesdep ~basedep ~bytestringdep ~smtlib-backendsnew-uploader

Dependency ranges changed: base, bytestring, smtlib-backends

Files

• CHANGELOG.md +9/−0
• smtlib-backends-z3.cabal +7/−5
• src/SMTLIB/Backends/Z3.hs +13/−0
• tests/Examples.hs +16/−4

@@ -3,6 +3,15 @@ All notable changes to the smtlib-backends-z3 library will be documented in this file. +## next++### Added++## v0.3.1 _(2024-01-29)_++### Added+- note about `Z3.Config` limitations+ ## v0.3 _(2023-02-03)_  ### Added

@@ -1,5 +1,5 @@ name:               smtlib-backends-z3-version:            0.3+version:            0.3.1 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@@ -10,7 +10,9 @@ license:            MIT license-file:       LICENSE author:             Quentin Aristote-maintainer:         quentin.aristote@tweag.io+maintainer:+  facundo.dominguez@tweag.io, gabriel.hondet@tweag.io, mathieu.montin@tweag.io+ build-type:         Simple category:           SMT cabal-version:      >=1.10@@ -29,12 +31,12 @@  library   hs-source-dirs:   src-  c-sources: cbits/z3.c+  c-sources:        cbits/z3.c   ghc-options:      -Wall -Wunused-packages   exposed-modules:  SMTLIB.Backends.Z3   build-depends:-      base             >=4.14    && <4.18-    , bytestring       >=0.10.12 && <0.12+      base             >=4.14    && <4.20+    , bytestring       >=0.10.12 && <0.13     , smtlib-backends  >=0.3     && <0.4    -- inspired from haskell-z3

@@ -40,6 +40,19 @@   { -- | A list of options to set during the solver's initialization.     -- Each pair is of the form @(paramId, paramValue)@, e.g.     -- @(":produce-models", "true")@.+    --+    -- Note that Z3 has different kinds of parameters, and not all of+    -- them can be set here. In particular, there are the so called+    -- global and module parameters with a value that affects+    -- all solver instances. We have found some of these global+    -- parameters to be ignored when provided here. You might have more+    -- luck setting them after starting the solver:+    --+    -- > command_ solver "(set-option :parameter_name value)"+    --+    -- Or using `Z3_global_param_set` from the Z3 API directly.+    --+    -- > foreign import capi unsafe "z3.h Z3_global_param_set" c_Z3_global_param_set :: CString -> CString -> IO ()     parameters :: [(BS.ByteString, BS.ByteString)]   } 

@@ -38,26 +38,38 @@ -- | How to set options at initialization time. settingOptions :: IO () settingOptions =+  Z3.with (Z3.Config [("dump_models2", "true")])+  -- (Z3.Config [(":produce-unsat-cores", "true")])+  $+    \handle2 ->+      initSolver NoQueuing (Z3.toBackend handle2) >>= \solver2 ->+   -- the Z3 C API is special (as a backend) in that some of its options can only be   -- set when the object representing the state of the solver is created   -- hence the 'Z3.new' and 'Z3.with' functions allow for setting options at   -- initialization time-  Z3.with Z3.defaultConfig+  Z3.with (Z3.Config [])   -- (Z3.Config [(":produce-unsat-cores", "true")])-  $+   $     \handle -> do       -- we don't enable queuing so that commands are checked for correctness       solver <- initSolver NoQueuing (Z3.toBackend handle)       -- this is for example the case of the @:produce-assertions@ parameter, and not       -- the case of the @:print-success@ one       command_ solver "(set-option :print-success true)"+ --     command_ solver2 "(set-option :dump_models true)"+ --     command_ solver "(set-option :dump_models true)"       -- the following would fail, returning       -- @       -- (error "line 1 column 33: error setting ':produce-unsat-cores',       --         option value cannot be modified after initialization")       -- @-      result <- command solver "(set-option :produce-unsat-cores true)"-      assertBool ("Expecting error message, got: " ++ LBS.unpack result) $ "(error" `LBS.isPrefixOf` result+--      result <- command solver "(set-option :produce-unsat-cores true)"+--      assertBool ("Expecting error message, got: " ++ LBS.unpack result) $ "(error" `LBS.isPrefixOf` result+      command_ solver "(declare-fun x () Int)"+      command_ solver "(assert (= x 10))"+      r <- command solver "(check-sat)"+      print r       return ()  -- | An example on how to force the content of the queue to be evaluated.