hasmtlib 2.6.3 → 2.7.0

raw patch · 23 files changed

+764/−453 lines, 23 filesdep +lifted-basedep +monad-controlPVP ok

version bump matches the API change (PVP)

Dependencies added: lifted-base, monad-control

API changes (from Hackage documentation)

Files

• CHANGELOG.md +23/−0
• hasmtlib.cabal +4/−2
• src/Language/Hasmtlib.hs +3/−2
• src/Language/Hasmtlib/Codec.hs +87/−0
• src/Language/Hasmtlib/Internal/Render.hs +260/−22
• src/Language/Hasmtlib/Solver/Bitwuzla.hs +13/−6
• src/Language/Hasmtlib/Solver/CVC5.hs +6/−3
• src/Language/Hasmtlib/Solver/Common.hs +0/−121
• src/Language/Hasmtlib/Solver/MathSAT.hs +13/−6
• src/Language/Hasmtlib/Solver/OpenSMT.hs +6/−3
• src/Language/Hasmtlib/Solver/Yices.hs +6/−3
• src/Language/Hasmtlib/Solver/Z3.hs +6/−3
• src/Language/Hasmtlib/Type/Bitvec.hs +0/−6
• src/Language/Hasmtlib/Type/Debugger.hs +172/−0
• src/Language/Hasmtlib/Type/Expr.hs +8/−150
• src/Language/Hasmtlib/Type/OMT.hs +5/−21
• src/Language/Hasmtlib/Type/Option.hs +0/−8
• src/Language/Hasmtlib/Type/Pipe.hs +25/−27
• src/Language/Hasmtlib/Type/Relation.hs +0/−1
• src/Language/Hasmtlib/Type/SMT.hs +0/−27
• src/Language/Hasmtlib/Type/SMTSort.hs +0/−11
• src/Language/Hasmtlib/Type/Solution.hs +6/−7
• src/Language/Hasmtlib/Type/Solver.hs +121/−24

@@ -6,6 +6,29 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [PVP versioning](https://pvp.haskell.org/). +## v2.7.0 _(2024-09-12)_++### Added+- Added helpful instances for standard types for `Codec` to ease deriving.+- Added decorator `timingout` in `Language.Hasmtlib.Type.Solver` to set a time-out for solvers.+Unfortunately as of SMTLib standard v2.6 there is no SMT-Option for this. Although some solvers like `Z3` (unreliably) support it,+we instead do it by internally coordinating the kill of the solver process from Haskell using `System.Timeout.Lifted#timeout`. Works like a charme.+- Added `Language.Hasmtlib.Type.Debugger` for debugging problem construction and solver interaction.++### Changed+- *(breaking change)* Completely revised the way solver process-configurations are handled and debugged.+Solvers which previously had the type `Process.Config` from `smtlib-backends` now have the type `SolverConfig` from `Language.Hasmtlib.Type.Solver`.+This bundles information on the executable of the solver with additional information such as debugging and time-outs.+Actual solver creation still is done by funtion `solver`. Therefore this change is only breaking, if you created custom solvers or debugged solvers.+- Debugging solvers changed from `solveWith (debug z3 def) $ ...` to `solveWith (solver $ debugging z3 def) $ ...`.+Also note that there are plenty debugging configurations besides `def` existing in `Language.Hasmtlib.Type.Debugger` now.+- Interactive solving before was a two-stepper like `iZ3 <- interactiveSolver z3 ; interactiveWith iZ3 $ ...`.+Leveraging `SolverConfig` this has been changed to a more uniform way with `interactiveWith z3 $ do ...`.+Also note that `debugInteractiveWith z3 $ ...` now is replaced by `interactiveWith (debugging def z3) $ ...`.++### Removed+- Removed `Language.Hasmtlib.Solver.Common`. Contents are now in `Language.Hasmtlib.Type.Solver`.+ ## v2.6.3 _(2024-09-07)_  ### Added

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.6.3+version:               2.7.0 synopsis:              A monad for interfacing with external SMT solvers description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.@@ -37,7 +37,6 @@                      , Language.Hasmtlib.Internal.Sharing                      , Language.Hasmtlib.Internal.Uniplate1                      , Language.Hasmtlib.Internal.Constraint-                     , Language.Hasmtlib.Solver.Common                      , Language.Hasmtlib.Solver.Bitwuzla                      , Language.Hasmtlib.Solver.CVC5                      , Language.Hasmtlib.Solver.MathSAT@@ -57,10 +56,13 @@                      , Language.Hasmtlib.Type.ArrayMap                      , Language.Hasmtlib.Type.Bitvec                      , Language.Hasmtlib.Type.Relation+                     , Language.Hasmtlib.Type.Debugger    build-depends:       array                        >= 0.5    && < 1                      , attoparsec                   >= 0.14.4 && < 1                      , base                         >= 4.17.2 && < 5+                     , lifted-base                  >= 0.2 && < 0.5+                     , monad-control                >= 1.0 && < 1.2                      , bytestring                   >= 0.11.5 && < 1                      , containers                   >= 0.6.7  && < 1                      , unordered-containers         >= 0.2.20 && < 0.3

@@ -32,7 +32,7 @@   -- ** Type   , module Language.Hasmtlib.Type.Solution   , module Language.Hasmtlib.Type.Solver-  , module Language.Hasmtlib.Solver.Common+  , module Language.Hasmtlib.Type.Debugger    -- ** Concrete solvers   , module Language.Hasmtlib.Solver.Z3@@ -61,11 +61,11 @@ import Language.Hasmtlib.Type.ArrayMap import Language.Hasmtlib.Type.Bitvec import Language.Hasmtlib.Type.Relation+import Language.Hasmtlib.Type.Debugger import Language.Hasmtlib.Boolean import Language.Hasmtlib.Codec import Language.Hasmtlib.Counting import Language.Hasmtlib.Variable-import Language.Hasmtlib.Solver.Common import Language.Hasmtlib.Solver.Bitwuzla import Language.Hasmtlib.Solver.CVC5 import Language.Hasmtlib.Solver.Z3@@ -73,3 +73,4 @@ import Language.Hasmtlib.Solver.OpenSMT import Language.Hasmtlib.Solver.MathSAT import Language.Hasmtlib.Internal.Sharing+import Language.Hasmtlib.Internal.Render ()

@@ -48,6 +48,8 @@ import Data.Dependent.Map as DMap import Data.Tree (Tree) import Data.Array (Array, Ix)+import Data.Word+import Data.Int import qualified Data.Text as Text import Data.Monoid (Sum, Product, First, Last, Dual) import qualified Data.Vector.Sized as V@@ -223,6 +225,91 @@   type Decoded (Array i e) = Array i (Decoded e)   decode = traverse . decode   encode = fmap encode++instance Codec Int where+  type Decoded Int = Int+  decode _ = Just+  encode = id++instance Codec Integer where+  type Decoded Integer = Integer+  decode _ = Just+  encode = id++instance Codec Natural where+  type Decoded Natural = Natural+  decode _ = Just+  encode = id++instance Codec Word where+  type Decoded Word = Word+  decode _ = Just+  encode = id++instance Codec Word8 where+  type Decoded Word8 = Word8+  decode _ = Just+  encode = id++instance Codec Word16 where+  type Decoded Word16 = Word16+  decode _ = Just+  encode = id++instance Codec Word32 where+  type Decoded Word32 = Word32+  decode _ = Just+  encode = id++instance Codec Word64 where+  type Decoded Word64 = Word64+  decode _ = Just+  encode = id++instance Codec Int8 where+  type Decoded Int8 = Int8+  decode _ = Just+  encode = id++instance Codec Int16 where+  type Decoded Int16 = Int16+  decode _ = Just+  encode = id++instance Codec Int32 where+  type Decoded Int32 = Int32+  decode _ = Just+  encode = id++instance Codec Int64 where+  type Decoded Int64 = Int64+  decode _ = Just+  encode = id++instance Codec Char where+  type Decoded Char = Char+  decode _ = Just+  encode = id++instance Codec Float where+  type Decoded Float = Float+  decode _ = Just+  encode = id++instance Codec Double where+  type Decoded Double = Double+  decode _ = Just+  encode = id++instance Codec Ordering where+  type Decoded Ordering = Ordering+  decode _ = Just+  encode = id++instance Codec Bool where+  type Decoded Bool = Bool+  decode _ = Just+  encode = id  class GCodec f where   type GDecoded f :: Type -> Type

@@ -1,35 +1,68 @@+{-# LANGUAGE LambdaCase #-}+ module Language.Hasmtlib.Internal.Render where -import Data.ByteString.Builder-import Data.Foldable (foldl')+import Language.Hasmtlib.Type.OMT+import Language.Hasmtlib.Type.SMT+import Language.Hasmtlib.Type.Expr+import Language.Hasmtlib.Type.Value+import Language.Hasmtlib.Type.Option+import Language.Hasmtlib.Type.SMTSort+import Language.Hasmtlib.Type.Bitvec+import Language.Hasmtlib.Type.ArrayMap+import Data.Coerce import Data.Sequence+import Data.Foldable (foldl')+import Data.Map (size, minViewWithKey)+import Data.ByteString.Builder+import Data.ByteString.Lazy.UTF8 (toString) import qualified Data.Text as Text import qualified Data.Text.Encoding as Text.Enc+import qualified Data.Vector.Sized as V+import Control.Lens hiding (op) import GHC.TypeNats +render1 :: Render a => Builder -> a -> Builder+render1 op x = "(" <> op <> " " <> render x <> ")"+{-# INLINE render1 #-}++render2 :: (Render a, Render b) => Builder -> a -> b -> Builder+render2 op x y = "(" <> op <> " " <> render x <> " " <> render y <> ")"+{-# INLINE render2 #-}++render3 :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder+render3 op x y z = "(" <> op <> " " <> render x <> " " <> render y <> " " <> render z <> ")"+{-# INLINE render3 #-}++renderN :: Render a => Builder -> [a] -> Builder+renderN op xs = "(" <> op <> renderedXs <> ")"+  where+    renderedXs = foldl' (\s x -> s <> " " <> render x) mempty xs+{-# INLINE renderN #-}+ -- | Render values to their SMTLib2-Lisp form, represented as 'Builder'. class Render a where   render :: a -> Builder  instance Render Bool where   render b = if b then "true" else "false"-  {-# INLINEABLE render #-}+  {-# INLINE render #-}  instance Render Nat where   render = integerDec . fromIntegral-  {-# INLINEABLE render #-}+  {-# INLINE render #-}  instance Render Integer where   render x     | x < 0     = "(- " <> integerDec (abs x) <> ")"     | otherwise = integerDec x-  {-# INLINEABLE render #-}+  {-# INLINE render #-}  instance Render Double where   render x     | x < 0     = "(- " <> formatDouble standardDefaultPrecision (abs x) <> ")"     | otherwise = formatDouble standardDefaultPrecision x-  {-# INLINEABLE render #-}+  {-# INLINE render #-}  instance Render Char where   render = char8@@ -47,24 +80,229 @@   render = Text.Enc.encodeUtf8Builder   {-# INLINE render #-} -renderUnary :: Render a => Builder -> a -> Builder-renderUnary op x = "(" <> op <> " " <> render x <> ")"-{-# INLINEABLE renderUnary #-}+instance Render (Bitvec enc n) where+  render = stringUtf8 . show+  {-# INLINE render #-} -renderBinary :: (Render a, Render b) => Builder -> a -> b -> Builder-renderBinary op x y = "(" <> op <> " " <> render x <> " " <> render y <> ")"-{-# INLINEABLE renderBinary #-}+instance Render (SMTVar t) where+  render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)+  {-# INLINE render #-} -renderTernary :: (Render a, Render b, Render c) => Builder -> a -> b -> c -> Builder-renderTernary op x y z = "(" <> op <> " " <> render x <> " " <> render y <> " " <> render z <> ")"-{-# INLINEABLE renderTernary #-}+instance Show (Value t) where+  show = toString . toLazyByteString . render -renderNary :: Render a => Builder -> [a] -> Builder-renderNary op xs = "(" <> op <> renderedXs <> ")"+instance Render (Value t) where+  render (IntValue x)   = render x+  render (RealValue x)  = render x+  render (BoolValue x)  = render x+  render (BvValue   v)  = "#b" <> render v+  render (ArrayValue arr) = case minViewWithKey (arr^.stored) of+    Nothing -> constRender $ arr^.arrConst+    Just ((k,v), stored')+      | size (arr^.stored) > 1 -> render $ ArrStore (Constant (wrapValue (arr & stored .~ stored'))) (Constant (wrapValue k)) (Constant (wrapValue v))+      | otherwise  -> constRender v+    where+      constRender v = "((as const " <> render (goSing arr) <> ") " <> render (wrapValue v) <> ")"+      goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)+      goSing _ = sortSing @(ArraySort k v)+  render (StringValue x) = "\"" <> render x <> "\""++instance KnownSMTSort t => Show (Expr t) where+  show = toString . toLazyByteString . render++instance KnownSMTSort t => Render (Expr t) where+  render (Var v)      = render v+  render (Constant c) = render c+  render (Plus x y)   = render2 (case sortSing' x of SBvSort _ _ -> "bvadd" ; _ -> "+") x y+  render (Minus x y)  = render2 (case sortSing' x of SBvSort _ _ -> "bvsub" ; _ -> "-") x y+  render (Neg x)      = render1  (case sortSing' x of SBvSort _ _ -> "bvneg" ; _ -> "-") x+  render (Mul x y)    = render2 (case sortSing' x of SBvSort _ _ -> "bvmul" ; _ -> "*") x y+  render (Abs x)      = render1  "abs" x+  render (Mod x y)    = render2 opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvurem"+          SSigned -> "bvsmod"+        _ -> "mod"+  render (Rem x y)    = render2 opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvurem"+          SSigned -> "bvsrem"+        _ -> "rem"+  render (IDiv x y)   = render2 opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvudiv"+          SSigned -> "bvsdiv"+        _ -> "div"+  render (Div x y)    = render2 "/" x y+  render (LTH x y)    = render2 opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvult"+          SSigned -> "bvslt"+        SStringSort -> "str.<"+        _ -> "<"+  render (LTHE x y)   = render2 opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvule"+          SSigned -> "bvsle"+        SStringSort -> "str.<="+        _ -> "<="+  render (EQU xs)     = renderN "=" $ V.toList xs+  render (Distinct xs)= renderN "distinct" $ V.toList xs+  render (GTHE x y)   = case sortSing' x of+    SBvSort enc _ -> case bvEncSing' enc of+      SUnsigned -> render2 "bvuge" x y+      SSigned   -> render2 "bvsge" x y+    SStringSort -> render2 "str.<=" y x+    _           -> render2 ">=" x y+  render (GTH x y)    = case sortSing' x of+    SBvSort enc _ -> case bvEncSing' enc of+      SUnsigned -> render2 "bvugt" x y+      SSigned   -> render2 "bvsgt" x y+    SStringSort -> render2 "str.<" y x+    _           -> render2 ">" x y+  render (Not x)      = render1  (case sortSing' x of SBvSort _ _ -> "bvnot" ; _ -> "not") x+  render (And x y)    = render2 (case sortSing' x of SBvSort _ _ -> "bvand" ; _ -> "and") x y+  render (Or x y)     = render2 (case sortSing' x of SBvSort _ _ -> "bvor" ; _ -> "or") x y+  render (Impl x y)   = render2 "=>" x y+  render (Xor x y)    = render2 (case sortSing' x of SBvSort _ _ -> "bvxor" ; _ -> "xor") x y+  render Pi           = "real.pi"+  render (Sqrt x)     = render1 "sqrt" x+  render (Exp x)      = render1 "exp" x+  render (Sin x)      = render1 "sin" x+  render (Cos x)      = render1 "cos" x+  render (Tan x)      = render1 "tan" x+  render (Asin x)     = render1 "arcsin" x+  render (Acos x)     = render1 "arccos" x+  render (Atan x)     = render1 "arctan" x+  render (ToReal x)   = render1 "to_real" x+  render (ToInt x)    = render1 "to_int" x+  render (IsInt x)    = render1 "is_int" x+  render (Ite p t f)  = render3 "ite" p t f+  render (BvNand x y)       = render2 "bvnand" (render x) (render y)+  render (BvNor x y)        = render2 "bvnor"  (render x) (render y)+  render (BvShL x y)        = render2 "bvshl"  (render x) (render y)+  render (BvLShR x y)       = render2 "bvlshr" (render x) (render y)+  render (BvAShR x y)       = render2 "bvashr" (render x) (render y)+  render (BvConcat x y)     = render2 "concat" (render x) (render y)+  render (BvRotL i x)       = render1 (render2 "_" ("rotate_left"  :: Builder) (render $ toInteger i)) (render x)+  render (BvRotR i x)       = render1 (render2 "_" ("rotate_right" :: Builder) (render $ toInteger i)) (render x)+  render (ArrSelect a i)    = render2  "select" (render a) (render i)+  render (ArrStore a i v)   = render3 "store"  (render a) (render i) (render v)+  render (StrConcat x y)        = render2 "str.++"  (render x) (render y)+  render (StrLength x)          = render1  "str.len" (render x)+  render (StrAt x i)            = render2 "str.at"  (render x) (render i)+  render (StrSubstring x i j)   = render3 "str.substr"  (render x) (render i) (render j)+  render (StrPrefixOf x y)      = render2 "str.prefixof" (render x) (render y)+  render (StrSuffixOf x y)      = render2 "str.suffixof" (render x) (render y)+  render (StrContains x y)      = render2 "str.contains" (render x) (render y)+  render (StrIndexOf x y i)     = render3 "str.indexof"     (render x) (render y) (render i)+  render (StrReplace x y y')    = render3 "str.replace"     (render x) (render y) (render y')+  render (StrReplaceAll x y y') = render3 "str.replace_all" (render x) (render y) (render y')+  render (ForAll mQvar f) = renderQuantifier "forall" mQvar f+  render (Exists mQvar f) = renderQuantifier "exists" mQvar f++renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder+renderQuantifier qname (Just qvar) f =+  render2+    qname+    ("(" <> render1 (render qvar) (sortSing @t) <> ")")+    expr   where-    renderedXs = foldl' (\s x -> s <> " " <> render x) mempty xs-{-# INLINEABLE renderNary #-}+    expr = render $ f $ Var qvar+renderQuantifier _ Nothing _ = mempty --- | Render values to their sequential SMTLib2-Lisp form, represented as a 'Seq' 'Builder'.-class RenderSeq a where-  renderSeq :: a -> Seq Builder+instance Render (SSMTSort t) where+  render SBoolSort   = "Bool"+  render SIntSort    = "Int"+  render SRealSort   = "Real"+  render (SBvSort _ p) = render2 "_" ("BitVec" :: Builder) (natVal p)+  render (SArraySort k v) = render2 "Array" (sortSing' k) (sortSing' v)+  render SStringSort   = "String"+  {-# INLINE render #-}++instance Render SMTOption where+  render (PrintSuccess  b) = render2 "set-option" (":print-success"  :: Builder) b+  render (ProduceModels b) = render2 "set-option" (":produce-models" :: Builder) b+  render (Incremental   b) = render2 "set-option" (":incremental"    :: Builder) b+  render (Custom k v)      = render2 "set-option" (":" <> render k) (render v)++instance Render SoftFormula where+  render sf = "(assert-soft " <> render (sf^.formula) <> " :weight " <> maybe "1" render (sf^.mWeight) <> renderGroupId (sf^.mGroupId) <> ")"+    where+      renderGroupId Nothing = mempty+      renderGroupId (Just groupId) = " :id " <> render groupId++instance KnownSMTSort t => Render (Minimize t) where+  render (Minimize expr) = "(minimize " <> render expr <> ")"++instance KnownSMTSort t => Render (Maximize t) where+  render (Maximize expr) = "(maximize " <> render expr <> ")"++renderSetLogic :: Builder -> Builder+renderSetLogic = render1 "set-logic"+{-# INLINE renderSetLogic #-}++renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder+renderDeclareVar v = render3 "declare-fun" v ("()" :: Builder) (sortSing @t)+{-# INLINE renderDeclareVar #-}++renderAssert :: Expr BoolSort -> Builder+renderAssert = render1 "assert"+{-# INLINE renderAssert #-}++renderGetValue :: SMTVar t -> Builder+renderGetValue x = render1 "get-value" $ "(" <> render x <> ")"+{-# INLINE renderGetValue #-}++renderPush :: Integer -> Builder+renderPush i = "(push "<> render i <>")"+{-# INLINE renderPush #-}++renderPop :: Integer -> Builder+renderPop i = "(pop "<> render i <>")"+{-# INLINE renderPop #-}++renderCheckSat :: Builder+renderCheckSat = "(check-sat)"+{-# INLINE renderCheckSat #-}++renderGetModel :: Builder+renderGetModel = "(get-model)"+{-# INLINE renderGetModel #-}++class RenderProblem s where+  renderOptions        :: s -> Seq Builder+  renderLogic          :: s -> Builder+  renderDeclareVars    :: s -> Seq Builder+  renderAssertions     :: s -> Seq Builder+  renderSoftAssertions :: s -> Seq Builder+  renderMinimizations  :: s -> Seq Builder+  renderMaximizations  :: s -> Seq Builder++instance RenderProblem SMT where+  renderOptions = fromList . fmap render . view options+  renderLogic = maybe mempty (renderSetLogic . stringUtf8) . view mlogic+  renderDeclareVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v) . view vars+  renderAssertions = fmap renderAssert . view formulas+  renderSoftAssertions _ = mempty+  renderMinimizations _ = mempty+  renderMaximizations _ = mempty++instance RenderProblem OMT where+  renderOptions = renderOptions . view smt+  renderLogic = renderLogic . view smt+  renderDeclareVars = renderDeclareVars . view smt+  renderAssertions = renderAssertions . view smt+  renderSoftAssertions = fmap render . view softFormulas+  renderMinimizations = fmap (\case SomeSMTSort minExpr -> render minExpr) . view targetMinimize+  renderMaximizations = fmap (\case SomeSMTSort maxExpr -> render maxExpr) . view targetMaximize

@@ -1,21 +1,28 @@ module Language.Hasmtlib.Solver.Bitwuzla where  import SMTLIB.Backends.Process+import Language.Hasmtlib.Type.Solver --- | A 'Config' for Bitwuzla.+-- | A 'SolverConfig' for Bitwuzla. --   Requires binary @bitwuzla@ to be in path. -- --   As of v0.5 Bitwuzla uses Cadical as SAT-Solver by default. --   Make sure it's default SAT-Solver binary - probably @cadical@ - is in path too.-bitwuzla :: Config-bitwuzla = defaultConfig { exe = "bitwuzla", args = [] }+bitwuzla :: SolverConfig s+bitwuzla = SolverConfig+  (defaultConfig { exe = "bitwuzla", args = [] })+  Nothing+  Nothing  --- | A 'Config' for Bitwuzla with Kissat as underlying sat-solver.+-- | A 'SolverConfig' for Bitwuzla with Kissat as underlying sat-solver. -- --   Requires binary @bitwuzla@ and to be in path. --   Will use the @kissat@ shipped with @bitwuzla@. -- --   It is recommended to build @bitwuzla@ from source for this to work as expected.-bitwuzlaKissat :: Config-bitwuzlaKissat = defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] }+bitwuzlaKissat :: SolverConfig s+bitwuzlaKissat = SolverConfig+  (defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] })+  Nothing+  Nothing

@@ -1,8 +1,11 @@ module Language.Hasmtlib.Solver.CVC5 where  import SMTLIB.Backends.Process+import Language.Hasmtlib.Type.Solver --- | A 'Config' for CVC5.+-- | A 'SolverConfig' for CVC5. --   Requires binary @cvc5@ to be in path.-cvc5 :: Config-cvc5 = defaultConfig { exe = "cvc5", args = [] }+cvc5 :: SolverConfig s+cvc5 = SolverConfig+  (defaultConfig { exe = "cvc5", args = [] })+  Nothing Nothing

@@ -1,121 +0,0 @@-{- |-This module handles common IO interaction with external SMT-Solvers via external processes.--It is built on top of Tweag's package @smtlib-backends@.--Although there already are several concrete solvers like @Z3@ in @Language.Hasmtlib.Solver.Z3@,-you may use this module to create your own solver bindings.--}-module Language.Hasmtlib.Solver.Common-(-  -- * Construction-  processSolver-, solver-, interactiveSolver--  -- * Debugging-, Debugger(..)-, debug-, def-)-where--import Language.Hasmtlib.Type.SMT-import Language.Hasmtlib.Type.OMT-import Language.Hasmtlib.Type.Solution-import Language.Hasmtlib.Internal.Render-import Language.Hasmtlib.Internal.Parser-import Data.Default-import Data.Sequence as Seq hiding ((|>), filter)-import Data.ByteString.Lazy hiding (singleton)-import Data.ByteString.Lazy.UTF8 (toString)-import Data.ByteString.Builder-import Data.Attoparsec.ByteString-import Control.Lens-import Control.Monad-import Control.Monad.IO.Class-import qualified SMTLIB.Backends.Process as Process-import qualified SMTLIB.Backends as Backend---- | Creates a 'Solver' from a 'Process.Config'.-solver :: (RenderSeq s, MonadIO m) => Process.Config -> Solver s m-solver cfg = processSolver cfg Nothing---- | Creates a debugging 'Solver' from a 'Process.Config'.-debug :: (RenderSeq s, MonadIO m) => Process.Config -> Debugger s -> Solver s m-debug cfg = processSolver cfg . Just---- | Creates an interactive session with a solver by creating and returning an alive process-handle 'Process.Handle'.---   Queues commands by default, see 'Backend.Queuing'.-interactiveSolver :: MonadIO m => Process.Config -> m (Backend.Solver, Process.Handle)-interactiveSolver cfg = liftIO $ do-  handle  <- Process.new cfg-  liftM2 (,) (Backend.initSolver Backend.Queuing $ Process.toBackend handle) (return handle)---- | A type holding actions for debugging states.-data Debugger s = Debugger-  { debugState          :: s -> IO ()               -- ^ Debug the entire state-  , debugProblem        :: Seq Builder -> IO ()     -- ^ Debug the linewise-rendered problem-  , debugResultResponse :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(check-sat)@-  , debugModelResponse  :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(get-model)@-  }--instance Default (Debugger SMT) where-  def = Debugger-    { debugState            = \s -> liftIO $ do-        putStrLn $ "Vars: "       ++ show (Seq.length (s^.vars))-        putStrLn $ "Assertions: " ++ show (Seq.length (s^.formulas))-    , debugProblem        = liftIO . mapM_ (putStrLn . toString . toLazyByteString)-    , debugResultResponse = liftIO . putStrLn . (\s -> "\n" ++ s ++ "\n") . toString-    , debugModelResponse  = liftIO . mapM_ (putStrLn . toString) . split 13-    }--instance Default (Debugger OMT) where-  def = Debugger-    { debugState          = \omt -> liftIO $ do-        putStrLn $ "Vars: "                 ++ show (Seq.length (omt^.smt.vars))-        putStrLn $ "Hard assertions: "      ++ show (Seq.length (omt^.smt.formulas))-        putStrLn $ "Soft assertions: "      ++ show (Seq.length (omt^.softFormulas))-        putStrLn $ "Optimization targets: " ++ show (Seq.length (omt^.targetMinimize) + Seq.length (omt^.targetMaximize))-    , debugProblem        = liftIO . mapM_ (putStrLn . toString . toLazyByteString)-    , debugResultResponse = liftIO . putStrLn . (\s -> "\n" ++ s ++ "\n") . toString-    , debugModelResponse  = liftIO . mapM_ (putStrLn . toString) . split 13-    }---- | A 'Solver' which holds an external process with a SMT-Solver.---   This will:------ 1. Encode the 'SMT'-problem,------ 2. start a new external process for the SMT-Solver,------ 3. send the problem to the SMT-Solver,------ 4. wait for an answer and parse it,------ 5. close the process and clean up all resources and------ 6. return the decoded solution.-processSolver :: (RenderSeq s, MonadIO m) => Process.Config -> Maybe (Debugger s) -> Solver s m-processSolver cfg debugger s = do-  liftIO $ Process.with cfg $ \handle -> do-    maybe mempty (`debugState` s) debugger-    pSolver <- Backend.initSolver Backend.Queuing $ Process.toBackend handle--    let problem = renderSeq s-    maybe mempty (`debugProblem` problem) debugger--    forM_ problem (Backend.command_ pSolver)-    resultResponse <- Backend.command pSolver "(check-sat)"-    maybe mempty (`debugResultResponse` resultResponse) debugger--    modelResponse  <- Backend.command pSolver "(get-model)"-    maybe mempty (`debugModelResponse` modelResponse) debugger--    case parseOnly resultParser (toStrict resultResponse) of-      Left e    -> fail e-      Right res -> case res of-        Unsat -> return (res, mempty)-        _     -> case parseOnly anyModelParser (toStrict modelResponse) of-          Left e    -> fail e-          Right sol -> return (res, sol)

@@ -1,13 +1,20 @@ module Language.Hasmtlib.Solver.MathSAT where  import SMTLIB.Backends.Process+import Language.Hasmtlib.Type.Solver --- | A 'Config' for MathSAT.+-- | A 'SolverConfig' for MathSAT. --   Requires binary @mathsat@ to be in path.-mathsat :: Config-mathsat = defaultConfig { exe = "mathsat", args = [] }+mathsat :: SolverConfig s+mathsat = SolverConfig+  (defaultConfig { exe = "mathsat", args = [] })+  Nothing+  Nothing --- | A 'Config' for OptiMathSAT.+-- | A 'SolverConfig' for OptiMathSAT. --   Requires binary @optimathsat@ to be in path.-optimathsat :: Config-optimathsat = defaultConfig { exe = "optimathsat", args = ["-optimization=true"] }+optimathsat :: SolverConfig s+optimathsat = SolverConfig+  (defaultConfig { exe = "optimathsat", args = ["-optimization=true"] })+  Nothing+  Nothing

@@ -1,8 +1,11 @@ module Language.Hasmtlib.Solver.OpenSMT where  import SMTLIB.Backends.Process+import Language.Hasmtlib.Type.Solver --- | A 'Config' for OpenSMT.+-- | A 'SolverConfig' for OpenSMT. --   Requires binary @opensmt@ to be in path.-opensmt :: Config-opensmt = defaultConfig { exe = "opensmt", args = [] }+opensmt :: SolverConfig s+opensmt = SolverConfig+  (defaultConfig { exe = "opensmt", args = [] })+  Nothing Nothing

@@ -1,8 +1,11 @@ module Language.Hasmtlib.Solver.Yices where  import SMTLIB.Backends.Process+import Language.Hasmtlib.Type.Solver --- | A 'Config' for Yices.+-- | A 'SolverConfig' for Yices. --   Requires binary @yices-smt2@ to be in path.-yices :: Config-yices = defaultConfig { exe = "yices-smt2", args = ["--smt2-model-format", "--incremental"] }+yices :: SolverConfig s+yices = SolverConfig+  (defaultConfig { exe = "yices-smt2", args = ["--smt2-model-format", "--incremental"] })+  Nothing Nothing

@@ -1,8 +1,11 @@ module Language.Hasmtlib.Solver.Z3 where  import SMTLIB.Backends.Process+import Language.Hasmtlib.Type.Solver --- | A 'Config' for Z3.+-- | A 'SolverConfig' for Z3. --   Requires binary @z3@ to be in path.-z3 :: Config-z3 = defaultConfig+z3 :: SolverConfig s+z3 = SolverConfig+  defaultConfig+  Nothing Nothing

@@ -45,9 +45,7 @@  import Prelude hiding ((&&), (||), not) import Language.Hasmtlib.Boolean-import Language.Hasmtlib.Internal.Render import Data.GADT.Compare-import Data.ByteString.Builder import Data.Bit import Data.Bits import Data.Coerce@@ -117,10 +115,6 @@ instance Show (Bitvec enc n) where   show = V.toList . V.map (\b -> if coerce b then '1' else '0') . coerce @_ @(V.Vector n Bit)   {-# INLINEABLE show #-}--instance Render (Bitvec enc n) where-  render = stringUtf8 . show-  {-# INLINE render #-}  instance (KnownBvEnc enc, KnownNat n) => Bits (Bitvec enc n) where   (.&.) = (&&)

@@ -0,0 +1,172 @@+{- |+This module provides debugging capabilites for the problem definition and communication with the external solver.+-}+module Language.Hasmtlib.Type.Debugger+  (+    -- * Type+    Debugger(..), StateDebugger(..)++    -- * Construction+    -- ** Volume+  , silently+  , noisy+  , verbosely++    -- ** Information+  , optionish+  , logicish+  , varish+  , assertionish+  , incrementalStackish, getValueish+  , responseish++  )+where++import Language.Hasmtlib.Type.SMT+import Language.Hasmtlib.Type.OMT+import Data.Sequence as Seq hiding ((|>), filter)+import Data.ByteString.Lazy hiding (singleton)+import Data.ByteString.Lazy.UTF8 (toString)+import Data.ByteString.Builder+import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8+import Data.Default+import Control.Lens hiding (op)++-- | A type holding actions for debugging states holding SMT-Problems.+data Debugger s = Debugger+  { debugState          :: s -> IO ()               -- ^ Debug the entire state+  , debugOption         :: Builder -> IO ()+  , debugLogic          :: Builder -> IO ()+  , debugVar            :: Builder -> IO ()+  , debugAssert         :: Builder -> IO ()+  , debugPush           :: Builder -> IO ()+  , debugPop            :: Builder -> IO ()+  , debugCheckSat       :: Builder -> IO ()+  , debugGetModel       :: Builder -> IO ()+  , debugGetValue       :: Builder -> IO ()+  , debugMinimize       :: Builder -> IO ()+  , debugMaximize       :: Builder -> IO ()+  , debugAssertSoft     :: Builder -> IO ()+  , debugResultResponse :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(check-sat)@+  , debugModelResponse  :: ByteString -> IO ()      -- ^ Debug the solvers raw response for @(get-model)@+  }++instance Default (Debugger s) where+  def = verbosely++printer :: Builder -> IO ()+printer = ByteString.Char8.putStrLn . toLazyByteString++-- | The silent 'Debugger'. Does not debug at all.+silently :: Debugger s+silently = Debugger+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)+  (const mempty)++-- | The noisy 'Debugger'.+--+--   Debugs the entire problem definition.+noisy :: Debugger s+noisy = Debugger+  (const mempty)+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  (const mempty)+  (const mempty)++-- | The verbose 'Debugger'.+--+--   Debugs all communication between Haskell and the external solver.+verbosely :: Debugger s+verbosely = Debugger+  (const mempty)+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  printer+  (ByteString.Char8.putStrLn . (\s -> "\n" <> s <> "\n"))+  (mapM_ (putStrLn . toString) . split 13)++-- | A 'Debugger' for debugging all rendered options that have been set.+optionish :: Debugger s+optionish = silently { debugOption = printer }++-- | A 'Debugger' for debugging the logic that has been set.+logicish :: Debugger s+logicish = silently { debugLogic = printer }++-- | A 'Debugger' for debugging all variable declarations.+varish :: Debugger s+varish = silently { debugVar = printer }++-- | A 'Debugger' for debugging all assertions.+assertionish :: Debugger s+assertionish = silently { debugAssert = printer, debugAssertSoft = printer }++-- | A 'Debugger' for debugging every push/pop-interaction with the solvers incremental stack.+incrementalStackish :: Debugger s+incrementalStackish = silently { debugPush = printer, debugPop = printer }++-- | A 'Debugger' for debugging every @(get-value)@ call to the solver.+getValueish :: Debugger s+getValueish = silently { debugGetValue = printer }++-- | A 'Debugger' for debugging the entire and raw responses of a solver for the commands @(check-sat)@ and @(get-model)@.+responseish :: Debugger s+responseish = silently+  { debugResultResponse = ByteString.Char8.putStrLn . (\s -> "\n" <> s <> "\n")+  , debugModelResponse = mapM_ (putStrLn . toString) . split 13+  }++-- | A class that allows debugging states.+class StateDebugger s where+  -- | Debugs information about the problem like the amount of variables and assertions.+  statistically :: Debugger s++instance StateDebugger SMT where+  statistically = silently+    { debugState = \s -> do+      putStrLn $ "Variables:  " ++ show (Seq.length (s^.vars))+      putStrLn $ "Assertions: " ++ show (Seq.length (s^.formulas))+    }++instance StateDebugger OMT where+  statistically = silently+    { debugState = \omt -> do+      putStrLn $ "Variables:       " ++ show (Seq.length (omt^.smt.vars))+      putStrLn $ "Hard assertions: " ++ show (Seq.length (omt^.smt.formulas))+      putStrLn $ "Soft assertions: " ++ show (Seq.length (omt^.softFormulas))+      putStrLn $ "Optimizations:   " ++ show (Seq.length (omt^.targetMinimize) + Seq.length (omt^.targetMaximize))+    }

@@ -77,15 +77,12 @@  import Prelude hiding (not, and, or, any, all, (&&), (||)) import Language.Hasmtlib.Internal.Uniplate1-import Language.Hasmtlib.Internal.Render-import Language.Hasmtlib.Type.Bitvec (BvEnc(..), KnownBvEnc(..), SBvEnc(..), bvEncSing')-import Language.Hasmtlib.Type.ArrayMap+import Language.Hasmtlib.Type.Bitvec (BvEnc(..), KnownBvEnc(..), SBvEnc(..)) import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Value import Language.Hasmtlib.Boolean import Data.GADT.Compare import Data.GADT.DeepSeq-import Data.Map hiding (toList) import Data.Coerce import Data.Proxy import Data.Int@@ -99,8 +96,6 @@ import Data.Text (pack) import Data.List(genericLength) import Data.Foldable (toList)-import Data.ByteString.Builder-import Data.ByteString.Lazy.UTF8 (toString) import qualified Data.Vector.Sized as V import Control.Lens hiding (from, to) import GHC.TypeLits hiding (someNatVal)@@ -697,13 +692,13 @@ -- | This instance is __partial__ for 'toRational', this method is only intended for use with constants. instance (KnownSMTSort t, Real (HaskellType t)) => Real (Expr t) where   toRational (Constant x) = toRational $ unwrapValue x-  toRational x = error $ "Real#toRational[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x+  toRational _ = error $ "Real#toRational[Expr " <> show (sortSing @t) <> "] only supported for constants."   {-# INLINE toRational #-}  -- | This instance is __partial__ for 'fromEnum', this method is only intended for use with constants. instance (KnownSMTSort t, Enum (HaskellType t)) => Enum (Expr t) where   fromEnum (Constant x) = fromEnum $ unwrapValue x-  fromEnum x = error $ "Enum#fromEnum[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x+  fromEnum _ = error $ "Enum#fromEnum[Expr " <> show (sortSing @t) <> "] only supported for constants."   {-# INLINE fromEnum #-}   toEnum = Constant . wrapValue . toEnum   {-# INLINE toEnum #-}@@ -715,7 +710,7 @@   divMod x y  = (IDiv x y, Mod x y)   {-# INLINE divMod #-}   toInteger (Constant x) = toInteger $ unwrapValue x-  toInteger x = error $ "Integer#toInteger[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x+  toInteger _ = error $ "Integer#toInteger[Expr " <> show (sortSing @t) <> "] only supported for constants."   {-# INLINE toInteger #-}  instance Boolean (Expr BoolSort) where@@ -789,7 +784,7 @@   complementBit b _ = Not b   {-# INLINE complementBit #-}   testBit (Constant (BoolValue b)) _ = b-  testBit sb _ = error $ "Bits#testBit[Expr BoolSort] is only supported for constants. Given: " <> show sb+  testBit _ _ = error "Bits#testBit[Expr BoolSort] is only supported for constants."   {-# INLINE testBit #-}   bitSizeMaybe _ = Just 1   {-# INLINE bitSizeMaybe #-}@@ -808,7 +803,7 @@   rotateR b _ = b   {-# INLINE rotateR #-}   popCount (Constant (BoolValue b)) = if b then 1 else 0-  popCount sb = error $ "Bits#popCount[Expr BoolSort] is only supported for constants. Given: " <> show sb+  popCount _ = error "Bits#popCount[Expr BoolSort] is only supported for constants."   {-# INLINE popCount #-}  -- | This instance is __partial__ for 'testBit' and 'popCount', it's only intended for use with constants ('Constant').@@ -826,7 +821,7 @@   bit = Constant . BvValue . Bits.bit   {-# INLINE bit #-}   testBit (Constant (BvValue b)) i = Bits.testBit b i-  testBit sb _ = error $ "Bits#testBit[Expr BvSort] is only supported for constants. Given: " <> show sb+  testBit _ _ = error "Bits#testBit[Expr BvSort] is only supported for constants."   {-# INLINE testBit #-}   bitSizeMaybe _ = Just $ fromIntegral $ natVal $ Proxy @n   {-# INLINE bitSizeMaybe #-}@@ -847,7 +842,7 @@   rotateR b i = BvRotR i b   {-# INLINE rotateR #-}   popCount (Constant (BvValue b)) = Bits.popCount b-  popCount sb = error $ "Bits#popCount[Expr BvSort] is only supported for constants. Given: " <> show sb+  popCount _ = error $ "Bits#popCount[Expr BvSort] is only supported for constants."   {-# INLINE popCount #-}  instance Semigroup (Expr StringSort) where@@ -863,143 +858,6 @@ instance IsString (Expr StringSort) where   fromString = Constant . StringValue . pack   {-# INLINE fromString #-}--instance Render (SMTVar t) where-  render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)-  {-# INLINE render #-}--instance Render (Value t) where-  render (IntValue x)   = render x-  render (RealValue x)  = render x-  render (BoolValue x)  = render x-  render (BvValue   v)  = "#b" <> render v-  render (ArrayValue arr) = case minViewWithKey (arr^.stored) of-    Nothing -> constRender $ arr^.arrConst-    Just ((k,v), stored')-      | size (arr^.stored) > 1 -> render $ ArrStore (Constant (wrapValue (arr & stored .~ stored'))) (Constant (wrapValue k)) (Constant (wrapValue v))-      | otherwise  -> constRender v-    where-      constRender v = "((as const " <> render (goSing arr) <> ") " <> render (wrapValue v) <> ")"-      goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)-      goSing _ = sortSing @(ArraySort k v)-  render (StringValue x) = "\"" <> render x <> "\""--instance KnownSMTSort t => Render (Expr t) where-  render (Var v)      = render v-  render (Constant c) = render c-  render (Plus x y)   = renderBinary (case sortSing' x of SBvSort _ _ -> "bvadd" ; _ -> "+") x y-  render (Minus x y)  = renderBinary (case sortSing' x of SBvSort _ _ -> "bvsub" ; _ -> "-") x y-  render (Neg x)      = renderUnary  (case sortSing' x of SBvSort _ _ -> "bvneg" ; _ -> "-") x-  render (Mul x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvmul" ; _ -> "*") x y-  render (Abs x)      = renderUnary  "abs" x-  render (Mod x y)    = renderBinary opStr x y-    where-      opStr = case sortSing' x of-        SBvSort enc _ -> case bvEncSing' enc of-          SUnsigned -> "bvurem"-          SSigned -> "bvsmod"-        _ -> "mod"-  render (Rem x y)    = renderBinary opStr x y-    where-      opStr = case sortSing' x of-        SBvSort enc _ -> case bvEncSing' enc of-          SUnsigned -> "bvurem"-          SSigned -> "bvsrem"-        _ -> "rem"-  render (IDiv x y)   = renderBinary opStr x y-    where-      opStr = case sortSing' x of-        SBvSort enc _ -> case bvEncSing' enc of-          SUnsigned -> "bvudiv"-          SSigned -> "bvsdiv"-        _ -> "div"-  render (Div x y)    = renderBinary "/" x y-  render (LTH x y)    = renderBinary opStr x y-    where-      opStr = case sortSing' x of-        SBvSort enc _ -> case bvEncSing' enc of-          SUnsigned -> "bvult"-          SSigned -> "bvslt"-        SStringSort -> "str.<"-        _ -> "<"-  render (LTHE x y)   = renderBinary opStr x y-    where-      opStr = case sortSing' x of-        SBvSort enc _ -> case bvEncSing' enc of-          SUnsigned -> "bvule"-          SSigned -> "bvsle"-        SStringSort -> "str.<="-        _ -> "<="-  render (EQU xs)     = renderNary "=" $ V.toList xs-  render (Distinct xs)= renderNary "distinct" $ V.toList xs-  render (GTHE x y)   = case sortSing' x of-    SBvSort enc _ -> case bvEncSing' enc of-      SUnsigned -> renderBinary "bvuge" x y-      SSigned   -> renderBinary "bvsge" x y-    SStringSort -> renderBinary "str.<=" y x-    _           -> renderBinary ">=" x y-  render (GTH x y)    = case sortSing' x of-    SBvSort enc _ -> case bvEncSing' enc of-      SUnsigned -> renderBinary "bvugt" x y-      SSigned   -> renderBinary "bvsgt" x y-    SStringSort -> renderBinary "str.<" y x-    _           -> renderBinary ">" x y-  render (Not x)      = renderUnary  (case sortSing' x of SBvSort _ _ -> "bvnot" ; _ -> "not") x-  render (And x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvand" ; _ -> "and") x y-  render (Or x y)     = renderBinary (case sortSing' x of SBvSort _ _ -> "bvor" ; _ -> "or") x y-  render (Impl x y)   = renderBinary "=>" x y-  render (Xor x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvxor" ; _ -> "xor") x y-  render Pi           = "real.pi"-  render (Sqrt x)     = renderUnary "sqrt" x-  render (Exp x)      = renderUnary "exp" x-  render (Sin x)      = renderUnary "sin" x-  render (Cos x)      = renderUnary "cos" x-  render (Tan x)      = renderUnary "tan" x-  render (Asin x)     = renderUnary "arcsin" x-  render (Acos x)     = renderUnary "arccos" x-  render (Atan x)     = renderUnary "arctan" x-  render (ToReal x)   = renderUnary "to_real" x-  render (ToInt x)    = renderUnary "to_int" x-  render (IsInt x)    = renderUnary "is_int" x-  render (Ite p t f)  = renderTernary "ite" p t f-  render (BvNand x y)       = renderBinary "bvnand" (render x) (render y)-  render (BvNor x y)        = renderBinary "bvnor"  (render x) (render y)-  render (BvShL x y)        = renderBinary "bvshl"  (render x) (render y)-  render (BvLShR x y)       = renderBinary "bvlshr" (render x) (render y)-  render (BvAShR x y)       = renderBinary "bvashr" (render x) (render y)-  render (BvConcat x y)     = renderBinary "concat" (render x) (render y)-  render (BvRotL i x)       = renderUnary (renderBinary "_" ("rotate_left"  :: Builder) (render $ toInteger i)) (render x)-  render (BvRotR i x)       = renderUnary (renderBinary "_" ("rotate_right" :: Builder) (render $ toInteger i)) (render x)-  render (ArrSelect a i)    = renderBinary  "select" (render a) (render i)-  render (ArrStore a i v)   = renderTernary "store"  (render a) (render i) (render v)-  render (StrConcat x y)        = renderBinary "str.++"  (render x) (render y)-  render (StrLength x)          = renderUnary  "str.len" (render x)-  render (StrAt x i)            = renderBinary "str.at"  (render x) (render i)-  render (StrSubstring x i j)   = renderTernary "str.substr"  (render x) (render i) (render j)-  render (StrPrefixOf x y)      = renderBinary "str.prefixof" (render x) (render y)-  render (StrSuffixOf x y)      = renderBinary "str.suffixof" (render x) (render y)-  render (StrContains x y)      = renderBinary "str.contains" (render x) (render y)-  render (StrIndexOf x y i)     = renderTernary "str.indexof"     (render x) (render y) (render i)-  render (StrReplace x y y')    = renderTernary "str.replace"     (render x) (render y) (render y')-  render (StrReplaceAll x y y') = renderTernary "str.replace_all" (render x) (render y) (render y')-  render (ForAll mQvar f) = renderQuantifier "forall" mQvar f-  render (Exists mQvar f) = renderQuantifier "exists" mQvar f--renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder-renderQuantifier qname (Just qvar) f =-  renderBinary-    qname-    ("(" <> renderUnary (render qvar) (sortSing @t) <> ")")-    expr-  where-    expr = render $ f $ Var qvar-renderQuantifier _ Nothing _ = mempty--instance Show (Value t) where-  show = toString . toLazyByteString . render--instance KnownSMTSort t => Show (Expr t) where-  show = toString . toLazyByteString . render  type instance Index   (Expr StringSort) = Expr IntSort type instance IxValue (Expr StringSort) = Expr StringSort

@@ -8,8 +8,12 @@ module Language.Hasmtlib.Type.OMT (   -- * SoftFormula+  -- ** Type   SoftFormula(..) +  -- ** Lens+, formula, mWeight, mGroupId+   -- * Optimization targets , Minimize(..), Maximize(..) @@ -23,7 +27,6 @@ where  import Language.Hasmtlib.Internal.Sharing-import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Option@@ -42,7 +45,7 @@   { _formula  :: Expr BoolSort    -- ^ The underlying soft formula   , _mWeight  :: Maybe Double     -- ^ Weight of the soft formula   , _mGroupId :: Maybe String     -- ^ Group-Id of the soft formula-  } deriving Show+  } $(makeLenses ''SoftFormula)  -- | A newtype for numerical expressions that are target of a minimization.@@ -108,22 +111,3 @@     sm <- use (smt.sharingMode)     sExpr <- runSharing sm expr     modifying softFormulas (|> SoftFormula sExpr w gid)--instance Render SoftFormula where-  render sf = "(assert-soft " <> render (sf^.formula) <> " :weight " <> maybe "1" render (sf^.mWeight) <> renderGroupId (sf^.mGroupId) <> ")"-    where-      renderGroupId Nothing = mempty-      renderGroupId (Just groupId) = " :id " <> render groupId--instance KnownSMTSort t => Render (Minimize t) where-  render (Minimize expr) = "(minimize " <> render expr <> ")"--instance KnownSMTSort t => Render (Maximize t) where-  render (Maximize expr) = "(maximize " <> render expr <> ")"--instance RenderSeq OMT where-  renderSeq omt =-       renderSeq (omt^.smt)-    <> fmap render (omt^.softFormulas)-    <> fmap (\case SomeSMTSort minExpr -> render minExpr) (omt^.targetMinimize)-    <> fmap (\case SomeSMTSort maxExpr -> render maxExpr) (omt^.targetMaximize)

@@ -3,9 +3,7 @@ -} module Language.Hasmtlib.Type.Option where -import Language.Hasmtlib.Internal.Render import Data.Data (Data)-import Data.ByteString.Builder  -- | Options for SMT-Solvers. data SMTOption =@@ -14,9 +12,3 @@   | Incremental   Bool              -- ^ Incremental solving   | Custom String String            -- ^ Custom options. First String is the option, second its value.   deriving (Show, Eq, Ord, Data)--instance Render SMTOption where-  render (PrintSuccess  b) = renderBinary "set-option" (":print-success"  :: Builder) b-  render (ProduceModels b) = renderBinary "set-option" (":produce-models" :: Builder) b-  render (Incremental   b) = renderBinary "set-option" (":incremental"    :: Builder) b-  render (Custom k v)      = renderBinary "set-option" (":" <> render k) (render v)

@@ -15,14 +15,14 @@   -- * Lens , lastPipeVarId, mPipeLogic , pipeSharingMode, pipeStableMap, incrSharedAuxs-, pipeSolver, isDebugging+, pipeSolver ) where  import Language.Hasmtlib.Internal.Sharing import Language.Hasmtlib.Internal.Render+import Language.Hasmtlib.Type.Debugger import Language.Hasmtlib.Type.Expr-import Language.Hasmtlib.Type.SMT import Language.Hasmtlib.Type.OMT (SoftFormula(..), Minimize(..), Maximize(..)) import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMTSort@@ -36,12 +36,10 @@ import Data.IntMap as IntMap (singleton) import Data.Dependent.Map as DMap import Data.Coerce-import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8 import Data.ByteString.Builder import Data.ByteString.Lazy hiding (filter, singleton, isPrefixOf) import Data.Attoparsec.ByteString hiding (Result) import Control.Monad.State-import Control.Monad import Control.Lens hiding (List) import System.Mem.StableName @@ -52,11 +50,11 @@ data Pipe = Pipe   { _lastPipeVarId     :: {-# UNPACK #-} !Int                                 -- ^ Last Id assigned to a new var   , _mPipeLogic        :: Maybe String                                        -- ^ Logic for the SMT-Solver-  , _pipeSharingMode   :: !SharingMode                                         -- ^ How to share common expressions+  , _pipeSharingMode   :: !SharingMode                                        -- ^ How to share common expressions   , _pipeStableMap     :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))  -- ^ Mapping between a 'StableName' and it's 'Expr' we may share   , _incrSharedAuxs    :: !(Seq (Seq (StableName ())))                        -- ^ Index of each 'Seq' ('StableName' ()) is incremental stack height where 'StableName' representing auxiliary var that has been shared   , _pipeSolver        :: !B.Solver                                           -- ^ Active pipe to the backend-  , _isDebugging       :: !Bool                                               -- ^ Flag if pipe shall debug+  , _mPipeDebugger      :: Maybe (Debugger Pipe)                                 -- ^ Debugger for communication with the external solver   } $(makeLenses ''Pipe) @@ -67,7 +65,7 @@     pipe <- get     modifying (incrSharedAuxs._last) (|> sn)     let cmd = renderAssert expr-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ maybe (return ()) (`debugAssert` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd   setSharingMode sm = pipeSharingMode .= sm @@ -79,7 +77,7 @@     pipe <- get     newVar <- smtvar' p     let cmd = renderDeclareVar newVar-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ maybe (return ()) (`debugVar` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd     return $ Var newVar   {-# INLINEABLE var' #-}@@ -91,45 +89,45 @@       Nothing    -> return sExpr       Just logic -> if "QF" `isPrefixOf` logic then return sExpr else quantify sExpr     let cmd = renderAssert qExpr-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ maybe (return ()) (`debugAssert` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd   {-# INLINEABLE assert #-}    setOption opt = do     pipe <- get     let cmd = render opt-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ maybe (return ()) (`debugOption` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd    setLogic l = do     mPipeLogic ?= l     pipe <- get     let cmd = renderSetLogic (stringUtf8 l)-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ maybe (return ()) (`debugLogic` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd  instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where   push = do     pipe <- get-    let cmd = "(push 1)"-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    let cmd = renderPush 1+    liftIO $ maybe (return ()) (`debugPush` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd     incrSharedAuxs <>= mempty    pop = do     pipe <- get-    let cmd = "(pop 1)"-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    let cmd = renderPop 1+    liftIO $ maybe (return ()) (`debugPop` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd     forMOf_ (incrSharedAuxs._last.folded) pipe (\sn -> pipeStableMap.at sn .= Nothing)     modifying incrSharedAuxs $ \case (auxs:>_) -> auxs ; auxs -> auxs    checkSat = do     pipe <- get-    let cmd = "(check-sat)"-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    let cmd = renderCheckSat+    liftIO $ maybe (return ()) (`debugCheckSat` cmd) (pipe^.mPipeDebugger)     result <- liftIO $ B.command (pipe^.pipeSolver) cmd-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn result+    liftIO $ maybe (return ()) (`debugResultResponse` result) (pipe^.mPipeDebugger)     case parseOnly resultParser (toStrict result) of       Left e    -> liftIO $ do         print result@@ -138,10 +136,10 @@    getModel = do     pipe   <- get-    let cmd = "(get-model)"-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    let cmd = renderGetModel+    liftIO $ maybe (return ()) (`debugGetModel` cmd) (pipe^.mPipeDebugger)     model <- liftIO $ B.command (pipe^.pipeSolver) cmd-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model+    liftIO $ maybe (return ()) (`debugModelResponse` model) (pipe^.mPipeDebugger)     case parseOnly anyModelParser (toStrict model) of       Left e    -> liftIO $ do         print model@@ -151,10 +149,10 @@   getValue :: forall t. KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))   getValue v@(Var x) = do     pipe   <- get-    let cmd = renderUnary "get-value" $ "(" <> render x <> ")"-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    let cmd = renderGetValue x+    liftIO $ maybe (return ()) (`debugGetValue` cmd) (pipe^.mPipeDebugger)     model <- liftIO $ B.command (pipe^.pipeSolver) cmd-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn model+    liftIO $ maybe (return ()) (`debugModelResponse` model) (pipe^.mPipeDebugger)     case parseOnly (getValueParser @t x) (toStrict model) of       Left e    -> liftIO $ do         print model@@ -175,7 +173,7 @@     pipe <- get     sExpr <- runSharing (pipe^.pipeSharingMode) expr     let cmd = render $ Minimize sExpr-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ maybe (return ()) (`debugMinimize` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd   {-# INLINEABLE minimize #-} @@ -183,7 +181,7 @@     pipe <- get     sExpr <- runSharing (pipe^.pipeSharingMode) expr     let cmd = render $ Maximize sExpr-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ maybe (return ()) (`debugMaximize` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd   {-# INLINEABLE maximize #-} @@ -191,6 +189,6 @@     pipe <- get     sExpr <- runSharing (pipe^.pipeSharingMode) expr     let cmd = render $ SoftFormula sExpr w gid-    when (pipe^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ maybe (return ()) (`debugAssertSoft` cmd) (pipe^.mPipeDebugger)     liftIO $ B.command_ (pipe^.pipeSolver) cmd   {-# INLINEABLE assertSoft #-}

@@ -61,7 +61,6 @@ -- so @a@ and @b@ have to be instances of 'Ix', -- and both \(A\) and \(B\) are intervals. newtype Relation a b = Relation (Array (a, b) (Expr BoolSort))-  deriving stock Show  instance (Ix a, Ix b) => Codec (Relation a b) where   type Decoded (Relation a b) = Array (a, b) Bool

@@ -13,14 +13,10 @@ , lastVarId, vars, formulas , mlogic, options , sharingMode, Language.Hasmtlib.Type.SMT.stableMap--  -- * Rendering-, renderSetLogic, renderDeclareVar, renderAssert, renderVars ) where  import Language.Hasmtlib.Internal.Sharing-import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Option@@ -30,7 +26,6 @@ import Data.Coerce import Data.Sequence hiding ((|>), filter) import Data.Data (toConstr, showConstr)-import Data.ByteString.Builder import Data.HashMap.Lazy (HashMap) import Control.Monad.State import Control.Lens hiding (List)@@ -82,25 +77,3 @@       eqCon l r = showConstr (toConstr l) == showConstr (toConstr r)    setLogic l = mlogic ?= l--instance RenderSeq SMT where-  renderSeq smt =-       fromList (render <$> smt^.options)-       >< maybe mempty (singleton . renderSetLogic . stringUtf8) (smt^.mlogic)-       >< renderVars (smt^.vars)-       >< fmap renderAssert (smt^.formulas)--renderSetLogic :: Builder -> Builder-renderSetLogic = renderUnary "set-logic"--renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder-renderDeclareVar v = renderTernary "declare-fun" v ("()" :: Builder) (sortSing @t)-{-# INLINEABLE renderDeclareVar #-}--renderAssert :: Expr BoolSort -> Builder-renderAssert = renderUnary "assert"-{-# INLINEABLE renderAssert #-}--renderVars :: Seq (SomeKnownSMTSort SMTVar) -> Seq Builder-renderVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v)-{-# INLINEABLE renderVars #-}

@@ -25,12 +25,10 @@  import Language.Hasmtlib.Internal.Constraint import Language.Hasmtlib.Type.Bitvec-import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.ArrayMap import Data.GADT.Compare import Data.Kind import Data.Proxy-import Data.ByteString.Builder import qualified Data.Text as Text import Control.Lens import GHC.TypeLits@@ -135,12 +133,3 @@  -- | An existential wrapper that hides some known 'SMTSort'. type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f--instance Render (SSMTSort t) where-  render SBoolSort   = "Bool"-  render SIntSort    = "Int"-  render SRealSort   = "Real"-  render (SBvSort _ p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)-  render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)-  render SStringSort   = "String"-  {-# INLINEABLE render #-}

@@ -10,8 +10,8 @@ -} module Language.Hasmtlib.Type.Solution (-  -- * Solver-  Solver, Result(..)+  -- * Result+  Result(..)    -- * Solution , Solution@@ -40,9 +40,6 @@ import Data.Dependent.Map.Lens import Control.Lens --- | Function that turns a state into a result and a solution.-type Solver s m = s -> m (Result, Solution)- -- | Results of check-sat commands. data Result = Unsat | Unknown | Sat deriving (Show, Eq, Ord) @@ -50,15 +47,17 @@  -- | Newtype for 'IntMap' 'Value' so we can use it as right-hand-side of 'DMap'. newtype IntValueMap t = IntValueMap (IntMap (Value t))-  deriving stock Show   deriving newtype (Semigroup, Monoid) +deriving stock instance Show (Value t) => Show (IntValueMap t)+ -- | A solution for a single variable. data SMTVarSol (t :: SMTSort) = SMTVarSol   { _solVar :: SMTVar t                       -- ^ A variable in the SMT-Problem   , _solVal :: Value t                        -- ^ An assignment for this variable in a solution-  } deriving Show+  } $(makeLenses ''SMTVarSol)+deriving stock instance Show (Value t) => Show (SMTVarSol t)  -- | Alias class for constraint 'Ord' ('HaskellType' t) class Ord (HaskellType t) => OrdHaskellType t

@@ -1,16 +1,30 @@+{-# LANGUAGE TemplateHaskell #-}+ {- | This module provides functions for having SMT-Problems solved by external solvers.++The base type for every solver is the 'SolverConfig'. It describes where the solver executable is located and how it should behave.+You can provide a time-out using the decorator 'timingout'.+Another decorator - 'debugging' - allows you to debug all the information you want. The actual debuggers can be found in "Language.Hasmtlib.Type.Debugger". -} module Language.Hasmtlib.Type.Solver   (-  -- * WithSolver-  WithSolver(..)+  -- * Solver configuration +  -- ** Type+  SolverConfig(..)++  -- ** Decoration+  , debugging, timingout++  -- ** Lens+  , processConfig, mTimeout, mDebugger+   -- * Stateful solving-  , solveWith+  , Solver, solver, solveWith    -- * Interactive solving-  , interactiveWith, debugInteractiveWith+  , interactiveWith    -- ** Minimzation   , solveMinimized@@ -20,26 +34,111 @@   ) where +import Language.Hasmtlib.Internal.Render+import Language.Hasmtlib.Internal.Parser import Language.Hasmtlib.Type.MonadSMT+import Language.Hasmtlib.Type.Debugger import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.Pipe import Language.Hasmtlib.Codec+import Data.ByteString.Lazy hiding (singleton) import qualified SMTLIB.Backends as Backend import qualified SMTLIB.Backends.Process as Process import Data.Default import Data.Maybe+import Data.Attoparsec.ByteString (parseOnly)+import Control.Lens hiding (op)+import Control.Monad import Control.Monad.State+import Control.Monad.Trans.Control+import System.Timeout.Lifted --- | Data that can have a 'Backend.Solver' which may be debugged.-class WithSolver a where-  -- | Create a value with a 'Backend.Solver' and a 'Bool' for whether to debug the 'Backend.Solver'.-  withSolver :: Backend.Solver -> Bool -> a+-- | Function that turns a state into a 'Result' and a 'Solution'.+type Solver s m = s -> m (Result, Solution) -instance WithSolver Pipe where-  withSolver = Pipe 0 Nothing def mempty mempty+-- | Configuration for solver processes.+data SolverConfig s = SolverConfig+  { _processConfig  :: Process.Config         -- ^ The underlying config of the process+  , _mTimeout       :: Maybe Int              -- ^ Timeout in microseconds+  , _mDebugger      :: Maybe (Debugger s)     -- ^ Debugger for communication with external solver+  }+$(makeLenses ''SolverConfig) +-- | Creates a 'Solver' which holds an external process with a SMT-Solver.+--+--   This will:+--+-- 1. Encode the SMT-problem,+--+-- 2. start a new external process for the SMT-Solver,+--+-- 3. send the problem to the SMT-Solver,+--+-- 4. wait for an answer and parse it,+--+-- 5. close the process and clean up all resources and+--+-- 6. return the decoded solution.+solver :: (RenderProblem s, MonadIO m) => SolverConfig s -> Solver s m+solver (SolverConfig cfg mTO debugger) s = do+  liftIO $ Process.with cfg $ \handle -> do+    maybe mempty (`debugState` s) debugger+    pSolver <- Backend.initSolver Backend.Queuing $ Process.toBackend handle++    let os   = renderOptions s+        l    = renderLogic s+        vs   = renderDeclareVars s+        as   = renderAssertions s+        sas  = renderSoftAssertions s+        mins = renderMinimizations s+        maxs = renderMaximizations s+    maybe mempty (forM_ os . debugOption) debugger+    forM_ os (Backend.command_ pSolver)+    maybe mempty (`debugLogic` l) debugger+    Backend.command_ pSolver l+    maybe mempty (forM_ vs . debugVar) debugger+    forM_ vs (Backend.command_ pSolver)+    maybe mempty (forM_ as . debugAssert) debugger+    forM_ as (Backend.command_ pSolver)+    maybe mempty (forM_ sas . debugAssertSoft) debugger+    forM_ sas (Backend.command_ pSolver)+    maybe mempty (forM_ mins . debugMinimize) debugger+    forM_ mins (Backend.command_ pSolver)+    maybe mempty (forM_ maxs . debugMaximize) debugger+    forM_ maxs (Backend.command_ pSolver)++    let timingOut io = case mTO of+          Nothing -> io+          Just t -> fromMaybe "unknown" <$> timeout t io+    resultResponse <- timingOut $ Backend.command pSolver renderCheckSat+    maybe mempty (`debugResultResponse` resultResponse) debugger++    modelResponse <- Backend.command pSolver renderGetModel+    maybe mempty (`debugModelResponse` modelResponse) debugger++    case parseOnly resultParser (toStrict resultResponse) of+      Left e    -> fail e+      Right res -> case res of+        Unsat -> return (res, mempty)+        _     -> case parseOnly anyModelParser (toStrict modelResponse) of+          Left e    -> fail e+          Right sol -> return (res, sol)++-- | Decorates a 'SolverConfig' with a timeout. The timeout is given as an 'Int' which specifies+--   after how many __microseconds__ the external solver process shall time out on @(check-sat)@.+--+--   When timing out, the 'Result' will always be 'Unknown'.+--+--   This uses 'timeout' internally.+timingout :: Int -> SolverConfig s -> SolverConfig s+timingout t cfg = cfg & mTimeout ?~ t++-- | Decorates a 'SolverConfig' with a 'Debugger'.+debugging :: Debugger s -> SolverConfig s -> SolverConfig s+debugging debugger cfg = cfg & mDebugger ?~ debugger+ -- | @'solveWith' solver prob@ solves a SMT problem @prob@ with the given -- @solver@. It returns a pair consisting of: --@@ -72,9 +171,9 @@ -- -- The solver will probably answer with @x := 1@. solveWith :: (Default s, Monad m, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))-solveWith solver m = do+solveWith solving m = do   (a, problem) <- runStateT m def-  (result, solution) <- solver problem+  (result, solution) <- solving problem    return (result, decode solution a) @@ -88,9 +187,7 @@ -- -- main :: IO () -- main = do---   cvc5Living <- interactiveSolver cvc5---   interactiveWith @Pipe cvc5Living $ do---     setOption $ Incremental True+--   interactiveWith z3 $ do --     setOption $ ProduceModels True --     setLogic \"QF_LRA\" --@@ -117,16 +214,16 @@ -- --   return () -- @-interactiveWith :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m ()-interactiveWith (solver, handle) m = do-  _ <- runStateT m $ withSolver solver False-  liftIO $ Process.close handle---- | Like 'interactiveWith' but it prints all communication with the solver to console.-debugInteractiveWith :: (WithSolver s, MonadIO m) => (Backend.Solver, Process.Handle) -> StateT s m () -> m ()-debugInteractiveWith (solver, handle) m = do-  _ <- runStateT m $ withSolver solver True+interactiveWith :: (MonadIO m, MonadBaseControl IO m) => SolverConfig Pipe -> StateT Pipe m a -> m (Maybe a)+interactiveWith cfg m = do+  handle <- liftIO $ Process.new $ cfg^.processConfig+  processSolver <- liftIO $ Backend.initSolver Backend.Queuing $ Process.toBackend handle+  let timingOut io = case cfg^.mTimeout of+        Nothing -> Just <$> io+        Just t -> timeout t io+  ma <- timingOut $ runStateT m $ Pipe 0 Nothing def mempty mempty processSolver (cfg^.mDebugger)   liftIO $ Process.close handle+  return $ fmap fst ma  -- | Solves the current problem with respect to a minimal solution for a given numerical expression. --