diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/hasmtlib.cabal b/hasmtlib.cabal --- a/hasmtlib.cabal +++ b/hasmtlib.cabal @@ -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. diff --git a/src/Language/Hasmtlib/Counting.hs b/src/Language/Hasmtlib/Counting.hs --- a/src/Language/Hasmtlib/Counting.hs +++ b/src/Language/Hasmtlib/Counting.hs @@ -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 #-} diff --git a/src/Language/Hasmtlib/Internal/Uniplate1.hs b/src/Language/Hasmtlib/Internal/Uniplate1.hs --- a/src/Language/Hasmtlib/Internal/Uniplate1.hs +++ b/src/Language/Hasmtlib/Internal/Uniplate1.hs @@ -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) diff --git a/src/Language/Hasmtlib/Type/Debugger.hs b/src/Language/Hasmtlib/Type/Debugger.hs --- a/src/Language/Hasmtlib/Type/Debugger.hs +++ b/src/Language/Hasmtlib/Type/Debugger.hs @@ -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 } diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs --- a/src/Language/Hasmtlib/Type/Expr.hs +++ b/src/Language/Hasmtlib/Type/Expr.hs @@ -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 diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs --- a/src/Language/Hasmtlib/Type/OMT.hs +++ b/src/Language/Hasmtlib/Type/OMT.hs @@ -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 diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs --- a/src/Language/Hasmtlib/Type/SMT.hs +++ b/src/Language/Hasmtlib/Type/SMT.hs @@ -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 diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs --- a/src/Language/Hasmtlib/Type/Solver.hs +++ b/src/Language/Hasmtlib/Type/Solver.hs @@ -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