hasmtlib 2.7.0 → 2.7.1

raw patch · 9 files changed

+189/−57 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib/Counting.hs +80/−19
• src/Language/Hasmtlib/Internal/Uniplate1.hs +5/−0
• src/Language/Hasmtlib/Type/Debugger.hs +14/−4
• src/Language/Hasmtlib/Type/Expr.hs +42/−3
• src/Language/Hasmtlib/Type/OMT.hs +1/−6
• src/Language/Hasmtlib/Type/SMT.hs +1/−5
• src/Language/Hasmtlib/Type/Solver.hs +36/−19

@@ -6,6 +6,15 @@ 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.1 _(2024-10-05)_++### Changed+- Cardinality constraints in `Language.Hasmtlib.Counting` now use specialized and more efficient encodings for a few cases.+- Debugging with debugger `statistically` now prints a more comprehensive overview about the problem size.+- Fixed bug where setting multiple custom `SMTOption`s would only set the most recent.+- Fixed bug where timeout for `SMT`/`OMT` would not work.+- Added smart constructors for `ite`.+ ## v2.7.0 _(2024-09-12)_  ### Added

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.7.0+version:               2.7.1 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.

@@ -12,7 +12,7 @@  E.g. if your logic is \"QF_LIA\" you would want @'count'' \@'IntSort' $ ...@ -It is worth noting that some cardinality constraints use optimized encodings, such as @'atLeast' 1 ≡ 'or'@.+It is worth noting that some cardinality constraints use optimized encodings for special cases. -} module Language.Hasmtlib.Counting (@@ -27,19 +27,24 @@    -- * At-Most , atMost+, amoSqrt+, amoQuad ) where -import Prelude hiding (not, (&&), (||), or)+import Prelude hiding (not, (&&), (||), and, or, all, any) import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Boolean+import Data.Foldable (toList)+import Data.List (transpose) import Data.Proxy+import Control.Lens  -- | Wrapper for 'count' which takes a 'Proxy'. count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t count' _ = sum . fmap (\b -> ite b 1 0)-{-# INLINEABLE count' #-}+{-# INLINE count' #-}  -- | Out of many bool-expressions build a formula which encodes how many of them are 'true'. count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t@@ -47,28 +52,84 @@ {-# INLINE count #-}  -- | Out of many bool-expressions build a formula which encodes that __at most__ @k@ of them are 'true'.-atMost  :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort-atMost (Constant 0) = nand-atMost (Constant 1) = atMostOneLinear+--+--   'atMost' is defined as follows:+--+-- @+-- 'atMost' 0 = 'nand'+-- 'atMost' 1 = 'amoSqrt'+-- 'atMost' k = ('<=?' k) . 'count'+-- @+atMost  :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort+atMost 0 = nand+atMost 1 = amoSqrt atMost k = (<=? k) . count {-# INLINE atMost #-} -atMostOneLinear :: (Foldable f, Boolean b) => f b -> b-atMostOneLinear xs =-  let (_, sz) = foldr (plus . (, false)) (false, false) xs-   in not sz-  where-    plus (xe, xz) (ye, yz) = (xe || ye, xz || yz || (xe && ye))- -- | Out of many bool-expressions build a formula which encodes that __at least__ @k@ of them are 'true'.-atLeast :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort-atLeast (Constant 0) = const true-atLeast (Constant 1) = or+--+--   'atLeast' is defined as follows:+--+-- @+-- 'atLeast' 0 = 'const' 'true'+-- 'atLeast' 1 = 'or'+-- 'atLeast' k = ('>=?' k) . 'count'+-- @+atLeast :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort+atLeast 0 = const true+atLeast 1 = or atLeast k = (>=? k) . count {-# INLINE atLeast #-}  -- | Out of many bool-expressions build a formula which encodes that __exactly__ @k@ of them are 'true'.-exactly :: forall t f. (Functor f, Foldable f, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort-exactly (Constant 0) = nand-exactly k = (=== k) . count+--+--   'exactly' is defined as follows:+--+-- @+-- 'exactly' 0 xs = 'nand' xs+-- 'exactly' 1 xs = 'atLeast' \@t 1 xs '&&' 'atMost' \@t 1 xs+-- 'exactly' k xs = 'count' xs '===' k+-- @+exactly :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort+exactly 0 xs = nand xs+exactly 1 xs = atLeast @t 1 xs && atMost @t 1 xs+exactly k xs = count xs === k {-# INLINE exactly #-}++-- | The squareroot-encoding, also called product-encoding, is a special encoding for @atMost 1@.+--+--   The original product-encoding provided by /Jingchao Chen/ in /A New SAT Encoding of the At-Most-One Constraint (2010)/+--   used auxiliary variables and would therefore be monadic.+--   It requires \( 2 \sqrt{n} + \mathcal{O}(\sqrt[4]{n}) \) auxiliary variables and+--   \( 2n + 4\sqrt{n} + \mathcal{O}(\sqrt[4]{n}) \) clauses.+--+--   To make this encoding pure, all auxiliary variables are replaced with a disjunction of size \( \mathcal{O}(\sqrt{n}) \).+--   Therefore zero auxiliary variables are required and technically clause-count remains the same, although the clauses get bigger.+amoSqrt :: (Foldable f, Boolean b) => f b -> b+amoSqrt xs+  | length xs < 10 = amoQuad $ toList xs+  | otherwise =+      let n = toInteger $ length xs+          p = ceiling $ sqrt $ fromInteger n+          rows = splitEvery (fromInteger p) $ toList xs+          columns = transpose rows+          vs = or <$> rows+          us = or <$> columns+       in amoSqrt vs && amoSqrt us &&+          and (imap (\j r -> and $ imap (\i x -> (x ==> us !! i) && (x ==> vs !! j)) r) rows)+  where+    splitEvery n = takeWhile (not . null) . map (take n) . iterate (drop n)++-- | The quadratic-encoding, also called pairwise-encoding, is a special encoding for @atMost 1@.+--+--   It's the naive encoding for the at-most-one-constraint and produces \( \binom{n}{2} \) clauses and no auxiliary variables..+amoQuad :: Boolean b => [b] -> b+amoQuad as = and $ do+  ys <- subs 2 as+  return $ any not ys+  where+    subs :: Int -> [a] -> [[a]]+    subs 0 _ = [[]]+    subs _ [] = []+    subs k (x : xs) = map (x :) (subs (k -1) xs) <> subs k xs+{-# INLINE amoQuad #-}

@@ -3,6 +3,7 @@ module Language.Hasmtlib.Internal.Uniplate1 where  import Language.Hasmtlib.Internal.Constraint+import Data.Functor.Identity import Data.Kind  type Uniplate1 :: (k -> Type) -> [k -> Constraint] -> Constraint@@ -11,6 +12,10 @@  transformM1 :: (Monad m, Uniplate1 f cs, AllC cs b) => (forall a. AllC cs a => f a -> m (f a)) -> f b -> m (f b) transformM1 f x = uniplate1 (transformM1 f) x >>= f++transform1 :: (Uniplate1 f cs, AllC cs b) => (forall a. AllC cs a => f a -> f a) -> f b -> f b+transform1 f = runIdentity . transformM1 (Identity . f)+{-# INLINE transform1 #-}  lazyParaM1 :: (Monad m, Uniplate1 f cs, AllC cs b) => (forall a. AllC cs a => f a -> m (f a) -> m (f a)) -> f b -> m (f b) lazyParaM1 f x = f x (uniplate1 (lazyParaM1 f) x)

@@ -25,8 +25,10 @@  import Language.Hasmtlib.Type.SMT import Language.Hasmtlib.Type.OMT-import Data.Sequence as Seq hiding ((|>), filter)-import Data.ByteString.Lazy hiding (singleton)+import Language.Hasmtlib.Type.Expr+import Language.Hasmtlib.Type.SMTSort+import Data.Sequence as Seq hiding ((|>))+import Data.ByteString.Lazy (ByteString, split) import Data.ByteString.Lazy.UTF8 (toString) import Data.ByteString.Builder import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8@@ -158,15 +160,23 @@ instance StateDebugger SMT where   statistically = silently     { debugState = \s -> do-      putStrLn $ "Variables:  " ++ show (Seq.length (s^.vars))+      putStrLn $ "Bool Vars:  " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ s^.vars)+      putStrLn $ "Arith Vars: " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ s^.vars)       putStrLn $ "Assertions: " ++ show (Seq.length (s^.formulas))+      putStrLn $ "Size:       " ++ show (sum $ fmap exprSize $ s^.formulas)     }  instance StateDebugger OMT where   statistically = silently     { debugState = \omt -> do-      putStrLn $ "Variables:       " ++ show (Seq.length (omt^.smt.vars))+      putStrLn $ "Bool Vars:       " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ omt^.smt.vars)+      putStrLn $ "Arith Vars:      " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ 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))+      let omtSize = sum (fmap exprSize $ omt^.smt.formulas)+                  + sum (fmap (exprSize . view formula) $ omt^.softFormulas)+                  + sum (fmap (\(SomeSMTSort (Minimize expr)) -> exprSize expr) $ omt^.targetMinimize)+                  + sum (fmap (\(SomeSMTSort (Maximize expr)) -> exprSize expr) $ omt^.targetMaximize)+      putStrLn $ "Size:            " ++ show omtSize     }

@@ -35,7 +35,7 @@     SMTVar(..), varId    -- * Expr type-  , Expr(..), isLeaf+  , Expr(..), isLeaf, exprSize    -- * Compare   -- ** Equatable@@ -91,6 +91,7 @@ import qualified Data.Bits as Bits import Data.Sequence (Seq) import Data.Tree (Tree)+import Data.STRef import Data.Monoid (Sum, Product, First, Last, Dual) import Data.String (IsString(..)) import Data.Text (pack)@@ -98,6 +99,8 @@ import Data.Foldable (toList) import qualified Data.Vector.Sized as V import Control.Lens hiding (from, to)+import Control.Monad.ST+import Control.Monad import GHC.TypeLits hiding (someNatVal) import GHC.TypeNats (someNatVal) import GHC.Generics@@ -184,6 +187,26 @@ isLeaf _ = False {-# INLINE isLeaf #-} +-- | Size of the expression.+--+--   Counts the amount of operations.+--+-- ==== __Examples__+--+--    >>> nodeSize $ x + y === x + y+--        3+--    >>> nodeSize $ false+--        0+exprSize :: KnownSMTSort t => Expr t -> Integer+exprSize expr = runST $ do+  nodesRef <- newSTRef 0+  _ <- transformM1+    (\expr' -> do+      unless (isLeaf expr') $ modifySTRef' nodesRef (+1)+      return expr')+    expr+  readSTRef nodesRef+ -- | Class that allows branching on predicates of type @b@ on branches of type @a@. -- --   If predicate (p :: b) then (t :: a) else (f :: a).@@ -202,8 +225,24 @@   ite p t f = ite p <$> t <*> f  instance Iteable (Expr BoolSort) (Expr t) where-  ite = Ite-  {-# INLINE ite #-}+  ite (Constant (BoolValue False)) _ f = f+  ite (Constant (BoolValue True)) t _  = t+  ite p t@(Ite p' t' f') f@(Ite p'' t'' f'')+    | p' == p'' && t' == t'' = Ite p' t' (Ite p f' f'')+    | p' == p'' && f' == f'' = Ite (not p') f' (Ite p t' t'')+    | otherwise = Ite p t f+  ite p t f@(Ite p' t' f')+    | p == p' = Ite p t f'+    | t == t' = Ite (p || p') t f'+    | otherwise = Ite p t f+  ite p t@(Ite p' t' f') f+    | p == p' = Ite p t' f+    | f == f' = Ite (p && p') t' f+    | otherwise = Ite p t f+  ite p t f+    | t == f = t+    | otherwise = Ite p t f+  {-# INLINEABLE ite #-}  instance Iteable Bool a where   ite p t f = if p then t else f

@@ -29,14 +29,12 @@ import Language.Hasmtlib.Internal.Sharing import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Type.Option import Language.Hasmtlib.Type.Expr 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) @@ -91,10 +89,7 @@     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)+  setOption opt = smt.options <>= pure opt    setLogic l = smt.mlogic ?= l 

@@ -25,7 +25,6 @@ import Data.Default import Data.Coerce import Data.Sequence hiding ((|>), filter)-import Data.Data (toConstr, showConstr) import Data.HashMap.Lazy (HashMap) import Control.Monad.State import Control.Lens hiding (List)@@ -71,9 +70,6 @@     modify $ \s -> s & formulas %~ (|> qExpr)   {-# INLINE assert #-} -  setOption opt = options %= ((opt:) . filter (not . eqCon opt))-    where-      eqCon :: SMTOption -> SMTOption -> Bool-      eqCon l r = showConstr (toConstr l) == showConstr (toConstr r)+  setOption opt = options <>= pure opt    setLogic l = mlogic ?= l

@@ -83,7 +83,11 @@ -- 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+  handle <- liftIO $ Process.new cfg+  let timingOut io = case mTO of+        Nothing -> io+        Just t -> fromMaybe ("unknown", mempty) <$> timeout t io+  (rawRes, rawModel) <- liftIO $ timingOut $ do     maybe mempty (`debugState` s) debugger     pSolver <- Backend.initSolver Backend.Queuing $ Process.toBackend handle @@ -109,25 +113,31 @@     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 (`debugCheckSat` "(check-sat)") debugger+    resultResponse <- Backend.command pSolver renderCheckSat     maybe mempty (`debugResultResponse` resultResponse) debugger +    maybe mempty (`debugGetModel` "(get-model)") 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+    return (resultResponse, modelResponse)++  liftIO $ Process.close handle++  case parseOnly resultParser (toStrict rawRes) of+    Left e    -> error $ "Language.Hasmtlib.Type.Solver#solver: Error when paring (check-sat) response: "+                        <> e <> " | This is probably an error in Hasmtlib."+    Right res -> case res of         Unsat -> return (res, mempty)-        _     -> case parseOnly anyModelParser (toStrict modelResponse) of-          Left e    -> fail e+        _     -> case parseOnly anyModelParser (toStrict rawModel) of+          Left e    -> error $ "Language.Hasmtlib.Type.Solver#solver: Error when paring (get-model) response: "+                              <> e <> " | This is probably an error in Hasmtlib."           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)@.+--   after how many __microseconds__ the entire problem including problem construction,+--   solver interaction and solving time may time out. -- --   When timing out, the 'Result' will always be 'Unknown'. --@@ -313,9 +323,9 @@   -> Maybe (Expr t -> Expr t)   -> Maybe (Solution -> IO ())   -> m (Result, Solution)-solveOptimized op goal mStep mDebug = refine Unknown mempty goal+solveOptimized op goal mStep mDebug = refine Unsat mempty goal 0   where-    refine oldRes oldSol target = do+    refine oldRes oldSol target n_pushes = do       res <- checkSat       case res of         Sat   -> do@@ -329,9 +339,16 @@               push               let step = fromMaybe id mStep               assert $ target `op` step (encode targetSol)-              refine res sol target-        _ -> do-          pop-          case mStep of-            Nothing -> return (oldRes, oldSol)-            Just _  -> solveOptimized op goal Nothing mDebug -- make sure the very last step did not skip the optimal result+              refine res sol target (n_pushes + 1)+        r -> do+          if n_pushes < 1+          then return (r, mempty)+          else case mStep of+            Nothing -> do+              replicateM_ n_pushes pop+              return (oldRes, oldSol)+            Just _ -> do+              pop+              opt <- solveOptimized op goal Nothing mDebug -- make sure the very last step did not skip the optimal result+              replicateM_ (n_pushes - 1) pop+              return opt