hasmtlib 1.3.1 → 2.0.0

raw patch · 30 files changed

+556/−191 lines, 30 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +18/−0
• README.md +17/−11
• hasmtlib.cabal +4/−1
• src/Language/Hasmtlib.hs +6/−0
• src/Language/Hasmtlib/Boolean.hs +13/−0
• src/Language/Hasmtlib/Codec.hs +1/−0
• src/Language/Hasmtlib/Counting.hs +1/−0
• src/Language/Hasmtlib/Equatable.hs +1/−0
• src/Language/Hasmtlib/Internal/Expr.hs +1/−102
• src/Language/Hasmtlib/Internal/Expr/Num.hs +1/−0
• src/Language/Hasmtlib/Internal/Parser.hs +3/−1
• src/Language/Hasmtlib/Internal/Render.hs +15/−2
• src/Language/Hasmtlib/Iteable.hs +10/−9
• src/Language/Hasmtlib/Orderable.hs +15/−14
• src/Language/Hasmtlib/Solver/CVC5.hs +2/−0
• src/Language/Hasmtlib/Solver/Common.hs +33/−19
• src/Language/Hasmtlib/Solver/MathSAT.hs +7/−0
• src/Language/Hasmtlib/Solver/OpenSMT.hs +9/−0
• src/Language/Hasmtlib/Solver/Yices.hs +2/−0
• src/Language/Hasmtlib/Solver/Z3.hs +2/−1
• src/Language/Hasmtlib/Type/Expr.hs +15/−4
• src/Language/Hasmtlib/Type/MonadSMT.hs +67/−7
• src/Language/Hasmtlib/Type/OMT.hs +94/−0
• src/Language/Hasmtlib/Type/Option.hs +2/−0
• src/Language/Hasmtlib/Type/Pipe.hs +23/−6
• src/Language/Hasmtlib/Type/SMT.hs +7/−8
• src/Language/Hasmtlib/Type/SMTSort.hs +111/−0
• src/Language/Hasmtlib/Type/Solution.hs +3/−2
• src/Language/Hasmtlib/Type/Solver.hs +70/−2
• src/Language/Hasmtlib/Variable.hs +3/−2

@@ -6,6 +6,24 @@ 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.0.0 _(2024-07-23)_++### Added+- Arithmetic functions: `isIntSort`, `toIntSort` & `toRealSort`+- Asserting maybe-formulas: `assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()`+- Logical equivalence `(<==>)` & reverse logical implication `(<==)`+- Solvers: OpenSMT, OptiMathSAT+- Iterative refinement optimizations utilizing incremental stack+- Custom solver options via `Custom String String :: SMTOption`+- Optimization Modulo Theories (OMT) / MaxSMT support with: `minimize`, `maximize` & `assertSoft`++### Changed+- *(breaking change)* The functions `solver` and `debug` which create `Solver`s from `ProcessSolver`s are polymorph in the state `s` now.+This requires you to annotate the mentioned functions with the targetted state.+These are `SMT` and `OMT`.+For example, `solverWith (solver cvc5) $ do ...` becomes `solverWith (solver @SMT cvc5) $ do ...`.+- Prefix `xor` now has an `infix 4`+ ## v1.3.1 _(2024-07-12)_  ### Added

@@ -41,7 +41,7 @@  main :: IO () main = do-  res <- solveWith (solver cvc5) $ do+  res <- solveWith (solver @SMT cvc5) $ do     setLogic "QF_NRA"      u :: V3 (Expr RealSort) <- variable@@ -57,7 +57,6 @@  ## Features -### Supported - [x] SMTLib2-Sorts in the Haskell-Type   ```haskell     data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort@@ -72,7 +71,7 @@   ``` - [x] Pure API with Expression-instances for Num, Floating, Bounded, ...   ```haskell-    solveWith (solver yices) $ do+    solveWith (solver @SMT yices) $ do       setLogic "QF_BV"       x <- var @(BvSort 16)       y <- var@@ -81,12 +80,12 @@   ``` - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)   ```haskell-    -- | Function that turns a state (SMT) into a result and a solution+    -- | Function that turns a state (usually SMT or OMT) into a result and a solution     type Solver s m = s -> m (Result, Solution)   ```-- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT & MathSAT+- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT & OpenSMT   ```haskell-    (result, solution) <- solveWith (solver mathsat) $ do+    (result, solution) <- solveWith (solver @SMT mathsat) $ do       setLogic "QF_LIA"       assert $ ...   ```@@ -109,7 +108,7 @@   ``` - [x] Pure quantifiers `for_all` and `exists`   ```haskell-    solveWith (solver z3) $ do+    solveWith (solver @SMT z3) $ do       setLogic "LIA"       z <- var @IntSort       assert $ z === 0@@ -119,11 +118,18 @@               x + y === z       return z   ```+- [x] Optimization Modulo Theories (OMT) / MaxSMT+  ```haskell+    res <- solveWith (solver @OMT z3) $ do+      setLogic "QF_LIA"+      x <- var @IntSort -### Coming-- [ ] Observable sharing & access to the expression-tree (useful for rewriting, ...)-- [ ] (Maybe) signed BitVec with corresponding encoding on the type-level (unsigned, ones-complement, twos-complement)-- [ ] ...+      assert $ x >? -2+      assertSoftWeighted (x >? -1) 5.0+      minimize x++      return x+  ```  ## Examples There are some examples in [here](https://github.com/bruderj15/Hasmtlib/tree/master/src/Language/Hasmtlib/Example).

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               1.3.1+version:               2.0.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.@@ -40,12 +40,15 @@                      , Language.Hasmtlib.Solver.Common                      , Language.Hasmtlib.Solver.CVC5                      , Language.Hasmtlib.Solver.MathSAT+                     , Language.Hasmtlib.Solver.OpenSMT                      , Language.Hasmtlib.Solver.Yices                      , Language.Hasmtlib.Solver.Z3                      , Language.Hasmtlib.Type.Expr                      , Language.Hasmtlib.Type.MonadSMT                      , Language.Hasmtlib.Type.SMT+                     , Language.Hasmtlib.Type.OMT                      , Language.Hasmtlib.Type.Pipe+                     , Language.Hasmtlib.Type.SMTSort                      , Language.Hasmtlib.Type.Solution                      , Language.Hasmtlib.Type.Solver                      , Language.Hasmtlib.Type.Option

@@ -2,10 +2,12 @@   (     module Language.Hasmtlib.Type.MonadSMT   , module Language.Hasmtlib.Type.SMT+  , module Language.Hasmtlib.Type.OMT   , module Language.Hasmtlib.Type.Pipe   , module Language.Hasmtlib.Type.Expr   , module Language.Hasmtlib.Type.Solver   , module Language.Hasmtlib.Type.Option+  , module Language.Hasmtlib.Type.SMTSort   , module Language.Hasmtlib.Type.Solution   , module Language.Hasmtlib.Type.ArrayMap   , module Language.Hasmtlib.Integraled@@ -20,16 +22,19 @@   , module Language.Hasmtlib.Solver.CVC5   , module Language.Hasmtlib.Solver.Z3   , module Language.Hasmtlib.Solver.Yices+  , module Language.Hasmtlib.Solver.OpenSMT   , module Language.Hasmtlib.Solver.MathSAT   )   where  import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMT+import Language.Hasmtlib.Type.OMT import Language.Hasmtlib.Type.Pipe import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.Solver import Language.Hasmtlib.Type.Option+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap import Language.Hasmtlib.Integraled@@ -44,4 +49,5 @@ import Language.Hasmtlib.Solver.CVC5 import Language.Hasmtlib.Solver.Z3 import Language.Hasmtlib.Solver.Yices+import Language.Hasmtlib.Solver.OpenSMT import Language.Hasmtlib.Solver.MathSAT

@@ -35,12 +35,25 @@   (==>) :: b -> b -> b   x ==> y = not x || y +  -- | Logical implication with arrow reversed.+  --+  -- @+  -- forall x y. (x ==> y) === (y <== x)+  -- @+  (<==) :: b -> b -> b+  y <== x = not x || y++  -- | Logical equivalence.+  (<==>) :: b -> b -> b+  x <==> y = (x ==> y) && (y ==> x)+   -- | Logical negation   not :: b -> b    -- | Exclusive-or   xor :: b -> b -> b +  infix 4 `xor`   infixr 3 &&   infixr 2 ||   infixr 0 ==>

@@ -10,6 +10,7 @@ import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Boolean import Data.Kind import Data.Coerce

@@ -3,6 +3,7 @@ import Prelude hiding (not, (&&), (||), or) import Language.Hasmtlib.Internal.Expr.Num () import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Equatable import Language.Hasmtlib.Orderable import Language.Hasmtlib.Iteable

@@ -6,6 +6,7 @@  import Prelude hiding (not, (&&)) import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Boolean import Data.Int import Data.Word

@@ -1,19 +1,15 @@-{-# LANGUAGE TypeFamilyDependencies #-}-{-# LANGUAGE NoStarIsType #-} {-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE UndecidableInstances #-}  module Language.Hasmtlib.Internal.Expr where -import Language.Hasmtlib.Internal.Bitvec import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.ArrayMap+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Boolean-import Data.GADT.Compare import Data.Map hiding (toList) import Data.List (intercalate)-import Data.Kind import Data.Proxy import Data.Coerce import Data.Foldable (toList)@@ -22,27 +18,11 @@ import Control.Lens import GHC.TypeLits --- | Sorts in SMTLib2 - used as promoted type (data-kind).-data SMTSort =-    BoolSort                      -- ^ Sort of Bool-  | IntSort                       -- ^ Sort of Int-  | RealSort                      -- ^ Sort of Real-  | BvSort Nat                    -- ^ Sort of BitVec with length n-  | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v- -- | An internal SMT variable with a phantom-type which holds an 'Int' as it's identifier. type role SMTVar phantom newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int } deriving (Show, Eq, Ord) $(makeLenses ''SMTVar) --- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'.-type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where-  HaskellType IntSort         = Integer-  HaskellType RealSort        = Double-  HaskellType BoolSort        = Bool-  HaskellType (BvSort n)      = Bitvec n-  HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)- -- | A wrapper for values of 'SMTSort's. data Value (t :: SMTSort) where   IntValue   :: HaskellType IntSort    -> Value IntSort@@ -70,79 +50,6 @@   SArraySort _ _ -> ArrayValue {-# INLINEABLE wrapValue #-} --- | Singleton for 'SMTSort'.-data SSMTSort (t :: SMTSort) where-  SIntSort   :: SSMTSort IntSort-  SRealSort  :: SSMTSort RealSort-  SBoolSort  :: SSMTSort BoolSort-  SBvSort    :: KnownNat n => Proxy n -> SSMTSort (BvSort n)-  SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)--deriving instance Show (SSMTSort t)-deriving instance Eq   (SSMTSort t)-deriving instance Ord  (SSMTSort t)--instance GEq SSMTSort where-  geq SIntSort SIntSort       = Just Refl-  geq SRealSort SRealSort     = Just Refl-  geq SBoolSort SBoolSort     = Just Refl-  geq (SBvSort n) (SBvSort m) = case sameNat n m of-    Just Refl -> Just Refl-    Nothing   -> Nothing-  geq _ _                     = Nothing--instance GCompare SSMTSort where-  gcompare SBoolSort SBoolSort     = GEQ-  gcompare SIntSort SIntSort       = GEQ-  gcompare SRealSort SRealSort     = GEQ-  gcompare (SBvSort n) (SBvSort m) = case cmpNat n m of-    LTI -> GLT-    EQI -> GEQ-    GTI -> GGT-  gcompare (SArraySort k v) (SArraySort k' v') = case gcompare (sortSing' k) (sortSing' k') of-    GLT -> GLT-    GEQ -> case gcompare (sortSing' v) (sortSing' v') of-      GLT -> GLT-      GEQ -> GEQ-      GGT -> GGT-    GGT -> GGT-  gcompare SBoolSort _        = GLT-  gcompare _ SBoolSort        = GGT-  gcompare SIntSort _         = GLT-  gcompare _ SIntSort         = GGT-  gcompare SRealSort _        = GLT-  gcompare _ SRealSort        = GGT-  gcompare (SArraySort _ _) _ = GLT-  gcompare _ (SArraySort _ _) = GGT---- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.-class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t-instance KnownSMTSort IntSort                  where sortSing = SIntSort-instance KnownSMTSort RealSort                 where sortSing = SRealSort-instance KnownSMTSort BoolSort                 where sortSing = SBoolSort-instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)-instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where-   sortSing = SArraySort (Proxy @k) (Proxy @v)---- | Wrapper for 'sortSing' which takes a 'Proxy'-sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t-sortSing' _ = sortSing @t---- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k------ @--- AllC '[]       k = ()--- AllC (c ': cs) k = (c k, AllC cs k)--- @-type AllC :: [k -> Constraint] -> k -> Constraint-type family AllC cs k :: Constraint where-  AllC '[]       k = ()-  AllC (c ': cs) k = (c k, AllC cs k)---- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.-data SomeSMTSort cs f where-  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f- -- | An existential wrapper that hides some known 'SMTSort'. type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f @@ -250,14 +157,6 @@ instance KnownNat n => Bounded (Expr (BvSort n)) where   minBound = Constant $ BvValue minBound   maxBound = Constant $ BvValue maxBound--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)-  {-# INLINEABLE render #-}  instance Render (SMTVar t) where   render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)

@@ -3,6 +3,7 @@ import Prelude hiding (div, mod, quotRem, rem, quot, divMod) import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Integraled+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Iteable import Language.Hasmtlib.Equatable import Language.Hasmtlib.Orderable

@@ -6,12 +6,14 @@ import Prelude hiding (not, (&&), (||), and , or) import Language.Hasmtlib.Internal.Bitvec import Language.Hasmtlib.Internal.Render+import Language.Hasmtlib.Internal.Expr.Num () import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Equatable import Language.Hasmtlib.Orderable import Language.Hasmtlib.Boolean import Language.Hasmtlib.Iteable import Language.Hasmtlib.Codec+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap import Data.Bit@@ -339,7 +341,7 @@   _   <- char '(' >> skipSpace >> string "to_real" >> skipSpace   dec <- anyValue decimal   _   <- skipSpace >> char ')'-  +   return $ fromInteger dec {-# INLINEABLE parseToRealDouble #-} 

@@ -2,9 +2,10 @@  import Data.ByteString.Builder import Data.Foldable (foldl')+import Data.Sequence import GHC.TypeNats --- | Render values to their SMTLib2-Lisp form, represented as @Builder@.+-- | Render values to their SMTLib2-Lisp form, represented as 'Builder'. class Render a where   render :: a -> Builder @@ -28,9 +29,17 @@     | otherwise = formatDouble standardDefaultPrecision x   {-# INLINEABLE render #-} +instance Render Char where+  render = char8+  {-# INLINE render #-}++instance Render String where+  render = string8+  {-# INLINE render #-}+ instance Render Builder where   render = id-  {-# INLINEABLE render #-}+  {-# INLINE render #-}  renderUnary :: Render a => Builder -> a -> Builder renderUnary op x = "(" <> op <> " " <> render x <> ")"@@ -49,3 +58,7 @@   where     renderedXs = foldl' (\s x -> s <> " " <> render x) mempty xs {-# INLINEABLE renderNary #-}++-- | Render values to their sequential SMTLib2-Lisp form, represented as a 'Seq' 'Builder'.+class RenderSeq a where+  renderSeq :: a -> Seq Builder

@@ -3,15 +3,16 @@ module Language.Hasmtlib.Iteable where  import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.SMTSort import Data.Sequence (Seq) import Data.Tree-  + -- | If condition (p :: b) then (t :: a) else (f :: a)---   +-- --    >>> ite true "1" "2" --        "1" --    >>> ite false 100 42---        42 +--        42 class Iteable b a where   ite :: b -> a -> a -> a   default ite :: (Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a@@ -38,18 +39,18 @@  instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c) => Iteable (Expr BoolSort) (a,b,c) where   ite p (a,b,c) (a',b',c') = (ite p a a', ite p b b', ite p c c')-  + instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d) => Iteable (Expr BoolSort) (a,b,c,d) where   ite p (a,b,c,d) (a',b',c',d') = (ite p a a', ite p b b', ite p c c', ite p d d')-  + instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e) => Iteable (Expr BoolSort) (a,b,c,d,e) where   ite p (a,b,c,d,e) (a',b',c',d',e') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e')-  + instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f) => Iteable (Expr BoolSort) (a,b,c,d,e,f) where   ite p (a,b,c,d,e,f) (a',b',c',d',e',f') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f')-  + instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g) where-  ite p (a,b,c,d,e,f,g) (a',b',c',d',e',f',g') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g')  -  +  ite p (a,b,c,d,e,f,g) (a',b',c',d',e',f',g') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g')+ instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g, Iteable (Expr BoolSort) h) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g,h) where   ite p (a,b,c,d,e,f,g,h) (a',b',c',d',e',f',g',h') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g', ite p h h')

@@ -6,6 +6,7 @@  import Prelude hiding (not, (&&), (||)) import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Equatable import Language.Hasmtlib.Iteable import Language.Hasmtlib.Boolean@@ -17,14 +18,14 @@ import GHC.TypeNats  -- | Compare two as as SMT-Expression.--- +-- -- @ -- x <- var @RealSort--- y <- var +-- y <- var -- assert $ x >? y -- assert $ x === min' 42 100 -- @--- +-- class Equatable a => Orderable a where   (<=?) :: a -> a -> Expr BoolSort   default (<=?) :: (Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort@@ -32,7 +33,7 @@    (>=?) :: a -> a -> Expr BoolSort   x >=? y = y <=? x-  +   (<?)  :: a -> a -> Expr BoolSort   x <? y = not $ y <=? x @@ -51,34 +52,34 @@  instance Orderable (Expr IntSort) where   (<?)     = LTH-  {-# INLINE (<?) #-}  +  {-# INLINE (<?) #-}   (<=?)    = LTHE-  {-# INLINE (<=?) #-}  +  {-# INLINE (<=?) #-}   (>=?)    = GTHE-  {-# INLINE (>=?) #-}  +  {-# INLINE (>=?) #-}   (>?)     = GTH   {-# INLINE (>?) #-}  instance Orderable (Expr RealSort) where   (<?)     = LTH-  {-# INLINE (<?) #-}  +  {-# INLINE (<?) #-}   (<=?)    = LTHE-  {-# INLINE (<=?) #-}  +  {-# INLINE (<=?) #-}   (>=?)    = GTHE-  {-# INLINE (>=?) #-}  +  {-# INLINE (>=?) #-}   (>?)     = GTH   {-# INLINE (>?) #-}  instance KnownNat n => Orderable (Expr (BvSort n)) where   (<?)     = BvuLT-  {-# INLINE (<?) #-}  +  {-# INLINE (<?) #-}   (<=?)    = BvuLTHE-  {-# INLINE (<=?) #-}  +  {-# INLINE (<=?) #-}   (>=?)    = BvuGTHE-  {-# INLINE (>=?) #-}  +  {-# INLINE (>=?) #-}   (>?)     = BvuGT   {-# INLINE (>?) #-}-  + class GEquatable f => GOrderable f where   (<?#)  :: f a -> f a -> Expr BoolSort   (<=?#) :: f a -> f a -> Expr BoolSort

@@ -3,5 +3,7 @@ import Language.Hasmtlib.Solver.Common import qualified SMTLIB.Backends.Process as P +-- | A 'ProcessSolver' for CVC5.+--   Requires binary @cvc5@ to be in path. cvc5 :: ProcessSolver cvc5 = ProcessSolver $ P.defaultConfig { P.exe = "cvc5", P.args = [] }

@@ -1,7 +1,9 @@ module Language.Hasmtlib.Solver.Common 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)@@ -19,11 +21,11 @@ newtype ProcessSolver = ProcessSolver { conf :: P.Config }  -- | Creates a 'Solver' from a 'ProcessSolver'-solver :: MonadIO m => ProcessSolver -> Solver SMT m+solver :: (RenderSeq s, MonadIO m) => ProcessSolver -> Solver s m solver (ProcessSolver cfg) = processSolver cfg Nothing  -- | Creates a debugging 'Solver' from a 'ProcessSolver'-debug :: MonadIO m => ProcessSolver -> Solver SMT m+debug :: (RenderSeq s, Default (Debugger s), MonadIO m) => ProcessSolver -> Solver s m debug (ProcessSolver cfg) = processSolver cfg $ Just def  -- | Creates an interactive session with a solver by creating and returning an alive process-handle 'P.Handle'.@@ -32,44 +34,56 @@   handle  <- P.new cfg   liftM2 (,) (B.initSolver B.Queuing $ P.toBackend handle) (return handle) --- | A type holding actions to execute for debugging 'SMT' solving.-data Debugger = Debugger-  { debugSMT            :: SMT -> IO ()+-- | A type holding actions for debugging states.+data Debugger s = Debugger+  { debugState          :: s -> IO ()   , debugProblem        :: Seq Builder -> IO ()   , debugResultResponse :: ByteString -> IO ()   , debugModelResponse  :: ByteString -> IO ()   } -instance Default Debugger where+instance Default (Debugger SMT) where   def = Debugger-    { debugSMT            = \smt -> liftIO $ do-        putStrLn $ "Vars: "       ++ show (Seq.length (smt^.vars))-        putStrLn $ "Assertions: " ++ show (Seq.length (smt^.formulas))+    { 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 and--- +-- -- 5. close the process and clean up all resources.--- -processSolver :: MonadIO m => P.Config -> Maybe Debugger -> Solver SMT m-processSolver cfg debugger smt = do+--+processSolver :: (RenderSeq s, MonadIO m) => P.Config -> Maybe (Debugger s) -> Solver s m+processSolver cfg debugger s = do   liftIO $ P.with cfg $ \handle -> do-    maybe mempty (`debugSMT` smt) debugger+    maybe mempty (`debugState` s) debugger     pSolver <- B.initSolver B.Queuing $ P.toBackend handle -    let problem = renderSMT smt+    let problem = renderSeq s     maybe mempty (`debugProblem` problem) debugger      forM_ problem (B.command_ pSolver)

@@ -3,5 +3,12 @@ import Language.Hasmtlib.Solver.Common import qualified SMTLIB.Backends.Process as P +-- | A 'ProcessSolver' for MathSAT.+--   Requires binary @mathsat@ to be in path. mathsat :: ProcessSolver mathsat = ProcessSolver $ P.defaultConfig { P.exe = "mathsat", P.args = [] }++-- | A 'ProcessSolver' for OptiMathSAT.+--   Requires binary @optimathsat@ to be in path.+optimathsat :: ProcessSolver+optimathsat = ProcessSolver $ P.defaultConfig { P.exe = "optimathsat", P.args = ["-optimization=true"] }

@@ -0,0 +1,9 @@+module Language.Hasmtlib.Solver.OpenSMT where++import Language.Hasmtlib.Solver.Common+import qualified SMTLIB.Backends.Process as P++-- | A 'ProcessSolver' for OpenSMT.+--   Requires binary @opensmt@ to be in path.+opensmt :: ProcessSolver+opensmt = ProcessSolver $ P.defaultConfig { P.exe = "opensmt", P.args = [] }

@@ -3,5 +3,7 @@ import Language.Hasmtlib.Solver.Common import qualified SMTLIB.Backends.Process as P +-- | A 'ProcessSolver' for Yices.+--   Requires binary @yices-smt2@ to be in path. yices :: ProcessSolver yices = ProcessSolver $ P.defaultConfig { P.exe = "yices-smt2", P.args = ["--smt2-model-format"] }

@@ -3,6 +3,7 @@ import Language.Hasmtlib.Solver.Common import qualified SMTLIB.Backends.Process as P +-- | A 'ProcessSolver' for Z3.+--   Requires binary @z3@ to be in path. z3 :: ProcessSolver z3 = ProcessSolver P.defaultConfig-

@@ -2,14 +2,12 @@ {-# LANGUAGE ViewPatterns #-}  module Language.Hasmtlib.Type.Expr- ( SMTSort(..)- , SMTVar(..), varId- , HaskellType+ ( SMTVar(..), varId  , Value(..), unwrapValue, wrapValue- , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort, AllC  , Expr  , equal, distinct  , bvShL, bvLShR, bvConcat, bvRotL, bvRotR+ , toIntSort, toRealSort, isIntSort  , for_all , exists  , select, store  )@@ -17,6 +15,7 @@  import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Internal.Expr.Num ()+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Boolean import Data.Proxy import Data.List (genericLength)@@ -107,3 +106,15 @@ bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n) bvRotR   = BvRotR {-# INLINE bvRotR #-}++-- | Converts an expression of type 'IntSort' to type 'RealSort'.+toRealSort :: Expr IntSort  -> Expr RealSort+toRealSort = ToReal++-- | Converts an expression of type 'RealSort' to type 'IntSort'.+toIntSort :: Expr RealSort -> Expr IntSort+toIntSort = ToInt++-- | Checks whether an expression of type 'RealSort' may be safely converted to type 'IntSort'.+isIntSort :: Expr RealSort -> Expr BoolSort+isIntSort = IsInt

@@ -4,6 +4,7 @@  import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Type.Option+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Codec import Data.Proxy@@ -15,21 +16,21 @@   -- | Construct a variable.   --   This is mainly intended for internal use.   --   In the API use 'var'' instead.-  --   +  --   -- @   -- x :: SMTVar RealType <- smtvar' (Proxy @RealType)   -- @   smtvar' :: forall t. KnownSMTSort t => Proxy t -> m (SMTVar t)-  +   -- | Construct a variable as expression.-  -- +  --   -- @   -- x :: Expr RealType <- var' (Proxy @RealType)   -- @   var' :: forall t. KnownSMTSort t => Proxy t -> m (Expr t)    -- | Assert a boolean expression.-  -- +  --   -- @   -- x :: Expr IntType <- var @IntType   -- assert $ x + 5 === 42@@ -37,14 +38,14 @@   assert :: Expr BoolSort -> m ()    -- | Set an SMT-Solver-Option.-  -- +  --   -- @   -- setOption $ Incremental True   -- @   setOption :: SMTOption -> m ()    -- | Set the logic for the SMT-Solver to use.-  -- +  --   -- @   -- setLogic \"QF_LRA\"   -- @@@ -63,7 +64,7 @@ {-# INLINE smtvar #-}  -- | Create a constant.--- +-- --   >>> constant True --       Constant (BoolValue True) --@@ -79,6 +80,13 @@ constant = Constant . wrapValue {-# INLINE constant #-} +-- | Maybe assert a boolean expression.+--   Asserts given expression if 'Maybe' is a 'Just'.+--   Does nothing otherwise.+assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()+assertMaybe Nothing = return ()+assertMaybe (Just expr) = assert expr+ --   We need this separate so we get a pure API for quantifiers --   Ideally we would do that when rendering the expression --   However renderSMTLib2 is pure but we need a new quantified var which is stateful@@ -147,3 +155,55 @@ -- | First run 'checkSat' and then 'getModel' on the current problem. solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution) solve = liftM2 (,) checkSat getModel++-- | A 'MonadState' that holds an OMT-Problem.+--   An OMT-Problem is a 'SMT-Problem' with additional optimization targets.+class MonadSMT s m => MonadOMT s m where+  -- | Minimizes a numerical expression within the OMT-Problem.+  --+  --   For example, below minimization:+  --+  -- @+  -- x <- var @IntSort+  -- assert $ x >? -2+  -- minimize x+  -- @+  --+  --   will give @x := -1@ as solution.+  minimize :: (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()++  -- | Maximizes a numerical expression within the OMT-Problem.+  --+  --   For example, below maximization:+  --+  -- @+  -- x <- var @(BvSort 8)+  -- maximize x+  -- @+  --+  --   will give @x := 11111111@ as solution.+  maximize :: (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()++  -- | Asserts a soft boolean expression.+  --   May take a weight and an identifier for grouping.+  --+  --   For example, below a soft constraint with weight 2.0 and identifier \"myId\" for grouping:+  --+  -- @+  -- x <- var @BoolSort+  -- assertSoft x (Just 2.0) (Just "myId")+  -- @+  --+  --   Omitting the weight will default it to 1.0.+  --+  -- @+  -- x <- var @BoolSort+  -- y <- var @BoolSort+  -- assertSoft x+  -- assertSoft y (Just "myId")+  -- @+  assertSoft :: Expr BoolSort -> Maybe Double -> Maybe String -> m ()++-- | Like 'assertSoft' but forces a weight and omits the group-id.+assertSoftWeighted :: MonadOMT s m => Expr BoolSort -> Double -> m ()+assertSoftWeighted expr w = assertSoft expr (Just w) Nothing

@@ -0,0 +1,94 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE LambdaCase #-}++module Language.Hasmtlib.Type.OMT where++import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Internal.Render+import Language.Hasmtlib.Type.MonadSMT+import Language.Hasmtlib.Type.SMTSort+import Language.Hasmtlib.Type.Option+import Language.Hasmtlib.Type.SMT+import Data.List (isPrefixOf)+import Data.Default+import Data.Coerce+import Data.Sequence hiding ((|>), filter)+import Data.Data (toConstr, showConstr)+import Control.Monad.State+import Control.Lens hiding (List)++-- | An assertion of a booolean expression in OMT that may be weighted.+data SoftFormula = SoftFormula+  { _formula  :: Expr BoolSort+  , _mWeight  :: Maybe Double+  , _mGroupId :: Maybe String+  } deriving Show+$(makeLenses ''SoftFormula)++-- | A newtype for numerical expressions that are target of a minimization.+newtype Minimize t = Minimize { _targetMin :: Expr t }++-- | A newtype for numerical expressions that are target of a maximization.+newtype Maximize t = Maximize { _targetMax :: Expr t }++-- | The state of the OMT-problem.+data OMT = OMT+  { _smt            :: SMT                                  -- ^ The underlying 'SMT'-Problem+  , _targetMinimize :: !(Seq (SomeKnownSMTSort Minimize))   -- ^ All expressions to minimize+  , _targetMaximize :: !(Seq (SomeKnownSMTSort Maximize))   -- ^ All expressions to maximize+  , _softFormulas   :: !(Seq SoftFormula)                   -- ^ All soft assertions of boolean expressions+  }+$(makeLenses ''OMT)++instance Default OMT where+  def = OMT def mempty mempty mempty++instance MonadState OMT m => MonadSMT OMT m where+  smtvar' _ = fmap coerce $ (smt.lastVarId) <+= 1+  {-# INLINE smtvar' #-}++  var' p = do+    newVar <- smtvar' p+    smt.vars %= (|> SomeSMTSort newVar)+    return $ Var newVar+  {-# INLINE var' #-}++  assert expr = do+    omt <- get+    qExpr <- case omt^.smt.mlogic of+      Nothing    -> return expr+      Just logic -> if "QF" `isPrefixOf` logic then return expr else quantify expr+    modify $ \s -> s & (smt.formulas) %~ (|> qExpr)+  {-# INLINE assert #-}++  setOption opt = smt.options %= ((opt:) . filter (not . eqCon opt))+    where+      eqCon :: SMTOption -> SMTOption -> Bool+      eqCon l r = showConstr (toConstr l) == showConstr (toConstr r)++  setLogic l = smt.mlogic ?= l++instance MonadSMT OMT m => MonadOMT OMT m where+  minimize expr = targetMinimize %= (|> SomeSMTSort (Minimize expr))+  maximize expr = targetMaximize %= (|> SomeSMTSort (Maximize expr))+  assertSoft expr w gid = softFormulas %= (|> SoftFormula expr 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)

@@ -9,9 +9,11 @@     PrintSuccess  Bool              -- ^ Print \"success\" after each operation   | ProduceModels Bool              -- ^ Produce a satisfying assignment after each successful checkSat   | 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)

@@ -4,9 +4,11 @@ module Language.Hasmtlib.Type.Pipe where  import Language.Hasmtlib.Type.SMT+import Language.Hasmtlib.Type.OMT (SoftFormula(..), Minimize(..), Maximize(..)) import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Internal.Render+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Codec import Language.Hasmtlib.Internal.Parser hiding (var, constant)@@ -98,14 +100,29 @@       Left e    -> liftIO $ do         print model         error e-      Right sol -> -        return $ -          decode -            (DMap.singleton -              (sortSing @t) -              (IntValueMap $ IMap.singleton (sol^.solVar.varId) (sol^.solVal))) +      Right sol ->+        return $+          decode+            (DMap.singleton+              (sortSing @t)+              (IntValueMap $ IMap.singleton (sol^.solVar.varId) (sol^.solVal)))             v   getValue expr = do     model <- getModel     return $ decode model expr   {-# INLINEABLE getValue #-}++instance (MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m where+  minimize expr = do+    smt <- get+    liftIO $ B.command_ (smt^.pipe) $ render $ Minimize expr+  {-# INLINEABLE minimize #-}++  maximize expr = do+    smt <- get+    liftIO $ B.command_ (smt^.pipe) $ render $ Maximize expr+  {-# INLINEABLE maximize #-}++  assertSoft expr w gid = do+    smt <- get+    liftIO $ B.command_ (smt^.pipe) $ render $ SoftFormula expr w gid

@@ -6,6 +6,7 @@ import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.MonadSMT+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Option import Data.List (isPrefixOf) import Data.Default@@ -54,14 +55,12 @@    setLogic l = mlogic ?= l --- | Render a 'SMT'-Problem to SMTLib2-Syntax.---   Each element of the returned Sequence is a line.-renderSMT :: SMT -> Seq Builder-renderSMT smt =-     fromList (render <$> smt^.options)-  >< maybe mempty (singleton . renderSetLogic . stringUtf8) (smt^.mlogic)-  >< renderVars (smt^.vars)-  >< fmap renderAssert (smt^.formulas)+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"

@@ -0,0 +1,111 @@+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE UndecidableInstances #-}++module Language.Hasmtlib.Type.SMTSort where++import Language.Hasmtlib.Internal.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 Control.Lens+import GHC.TypeLits++-- | Sorts in SMTLib2 - used as promoted type (data-kind).+data SMTSort =+    BoolSort                      -- ^ Sort of Bool+  | IntSort                       -- ^ Sort of Int+  | RealSort                      -- ^ Sort of Real+  | BvSort Nat                    -- ^ Sort of BitVec with length n+  | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v++-- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'.+type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where+  HaskellType IntSort         = Integer+  HaskellType RealSort        = Double+  HaskellType BoolSort        = Bool+  HaskellType (BvSort n)      = Bitvec n+  HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)++-- | Singleton for 'SMTSort'.+data SSMTSort (t :: SMTSort) where+  SIntSort   :: SSMTSort IntSort+  SRealSort  :: SSMTSort RealSort+  SBoolSort  :: SSMTSort BoolSort+  SBvSort    :: KnownNat n => Proxy n -> SSMTSort (BvSort n)+  SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)++deriving instance Show (SSMTSort t)+deriving instance Eq   (SSMTSort t)+deriving instance Ord  (SSMTSort t)++instance GEq SSMTSort where+  geq SIntSort SIntSort       = Just Refl+  geq SRealSort SRealSort     = Just Refl+  geq SBoolSort SBoolSort     = Just Refl+  geq (SBvSort n) (SBvSort m) = case sameNat n m of+    Just Refl -> Just Refl+    Nothing   -> Nothing+  geq _ _                     = Nothing++instance GCompare SSMTSort where+  gcompare SBoolSort SBoolSort     = GEQ+  gcompare SIntSort SIntSort       = GEQ+  gcompare SRealSort SRealSort     = GEQ+  gcompare (SBvSort n) (SBvSort m) = case cmpNat n m of+    LTI -> GLT+    EQI -> GEQ+    GTI -> GGT+  gcompare (SArraySort k v) (SArraySort k' v') = case gcompare (sortSing' k) (sortSing' k') of+    GLT -> GLT+    GEQ -> case gcompare (sortSing' v) (sortSing' v') of+      GLT -> GLT+      GEQ -> GEQ+      GGT -> GGT+    GGT -> GGT+  gcompare SBoolSort _        = GLT+  gcompare _ SBoolSort        = GGT+  gcompare SIntSort _         = GLT+  gcompare _ SIntSort         = GGT+  gcompare SRealSort _        = GLT+  gcompare _ SRealSort        = GGT+  gcompare (SArraySort _ _) _ = GLT+  gcompare _ (SArraySort _ _) = GGT++-- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.+class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t+instance KnownSMTSort IntSort                  where sortSing = SIntSort+instance KnownSMTSort RealSort                 where sortSing = SRealSort+instance KnownSMTSort BoolSort                 where sortSing = SBoolSort+instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)+instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where+   sortSing = SArraySort (Proxy @k) (Proxy @v)++-- | Wrapper for 'sortSing' which takes a 'Proxy'+sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t+sortSing' _ = sortSing @t++-- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k+--+-- @+-- AllC '[]       k = ()+-- AllC (c ': cs) k = (c k, AllC cs k)+-- @+type AllC :: [k -> Constraint] -> k -> Constraint+type family AllC cs k :: Constraint where+  AllC '[]       k = ()+  AllC (c ': cs) k = (c k, AllC cs k)++-- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.+data SomeSMTSort cs f where+  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs 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)+  {-# INLINEABLE render #-}

@@ -5,7 +5,8 @@  module Language.Hasmtlib.Type.Solution where -import Language.Hasmtlib.Type.Expr+import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.SMTSort import Data.IntMap as IMap hiding (foldl) import Data.Dependent.Map as DMap import Data.Dependent.Map.Lens@@ -36,7 +37,7 @@ class Ord (HaskellType t) => OrdHaskellType t instance Ord (HaskellType t) => OrdHaskellType t --- | An existential wrapper that hides some known 'SMTSort' with an 'Ord' 'HaskellType' +-- | An existential wrapper that hides some known 'SMTSort' with an 'Ord' 'HaskellType' type SomeKnownOrdSMTSort f = SomeSMTSort '[KnownSMTSort, OrdHaskellType] f  -- | Create a 'Solution' from some 'SMTVarSol's.

@@ -1,7 +1,17 @@-module Language.Hasmtlib.Type.Solver where+module Language.Hasmtlib.Type.Solver+  ( WithSolver(..)+  , solveWith, interactiveWith+  , solveMinimized, solveMinimizedDebug+  , solveMaximized, solveMaximizedDebug+  )+where -import Language.Hasmtlib.Type.Pipe+import Language.Hasmtlib.Type.MonadSMT+import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution+import Language.Hasmtlib.Type.Pipe+import Language.Hasmtlib.Orderable import Language.Hasmtlib.Codec import qualified SMTLIB.Backends as B import qualified SMTLIB.Backends.Process as P@@ -94,3 +104,61 @@ interactiveWith (solver, handle) m = do    _ <- runStateT m $ withSolver solver    liftIO $ P.close handle++-- | Solves the current problem with respect to a minimal solution for a given numerical expression.+--+--   Does not rely on MaxSMT/OMT.+--   Instead uses iterative refinement.+--+--   If you want access to intermediate results, use 'solveMinimizedDebug' instead.+solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))+  => Expr t+  -> m (Result, Solution)+solveMinimized = solveOptimized Nothing (<?)++-- | Like 'solveMinimized' but with access to intermediate results.+solveMinimizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))+  => (Solution -> IO ())+  -> Expr t+  -> m (Result, Solution)+solveMinimizedDebug debug = solveOptimized (Just debug) (<?)++-- | Solves the current problem with respect to a maximal solution for a given numerical expression.+--+--   Does not rely on MaxSMT/OMT.+--   Instead uses iterative refinement.+--+--   If you want access to intermediate results, use 'solveMaximizedDebug' instead.+solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))+  => Expr t+  -> m (Result, Solution)+solveMaximized = solveOptimized Nothing (>?)++-- | Like 'solveMaximized' but with access to intermediate results.+solveMaximizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))+  => (Solution -> IO ())+  -> Expr t+  -> m (Result, Solution)+solveMaximizedDebug debug = solveOptimized (Just debug) (<?)++solveOptimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t)+  => Maybe (Solution -> IO ())+  -> (Expr t -> Expr t -> Expr BoolSort)+  -> Expr t+  -> m (Result, Solution)+solveOptimized mDebug op = go Unknown mempty+  where+    go oldRes oldSol target = do+      push+      (res, sol) <- solve+      case res of+        Sat   -> do+          case decode sol target of+            Nothing        -> return (Sat, mempty)+            Just targetSol -> do+              case mDebug of+                Nothing    -> pure ()+                Just debug -> liftIO $ debug sol+              assert $ target `op` encode targetSol+              go res sol target+        _ -> pop >> return (oldRes, oldSol)

@@ -4,13 +4,14 @@  import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Type.MonadSMT+import Language.Hasmtlib.Type.SMTSort import Data.Proxy  -- | Construct a variable datum of a data-type by creating variables for all its fields.--- +-- -- @ --    data V3 a = V3 a a a---    instance Variable a => V3 a +--    instance Variable a => V3 a -- @ -- --    >>> varV3 <- variable @(V3 (Expr RealType)) ; varV3