ersatz 0.4.13 → 0.5

raw patch · 14 files changed

+210/−27 lines, 14 filesdep +HUnitdep +test-frameworkdep +test-framework-hunitdep ~basedep ~containersdep ~data-defaultPVP ok

version bump matches the API change (PVP)

Dependencies added: HUnit, test-framework, test-framework-hunit

Dependency ranges changed: base, containers, data-default

API changes (from Hackage documentation)

Files

• .hlint.yaml +2/−0
• CHANGELOG.md +37/−0
• README.md +1/−1
• ersatz.cabal +20/−3
• src/Ersatz/Bit.hs +5/−4
• src/Ersatz/Codec.hs +13/−3
• src/Ersatz/Problem.hs +7/−5
• src/Ersatz/Solution.hs +3/−0
• src/Ersatz/Solver.hs +32/−3
• src/Ersatz/Solver/DepQBF.hs +15/−1
• src/Ersatz/Variable.hs +3/−3
• tests/HUnit.hs +38/−0
• tests/Speed.hs +5/−1
• tests/Z001.hs +29/−3

@@ -7,3 +7,5 @@     name: Use lambda-case  - ignore: {name: Hoist not, within: [Ersatz.Bit]} # This is how we define `any`, ya dingus+- ignore: {name: Use ||, within: [Ersatz.Relation.Prop]} # This is a different `or`+- ignore: {name: Use &&, within: [Ersatz.Relation.Prop]} # This is a different `and`

@@ -1,3 +1,40 @@+0.5 [2023.09.08]+----------------+* The `forall` function in `Ersatz.Variable` has been renamed to+  `forall_`, since a future version of GHC will make the use of `forall` as an+  identifier an error.+* The types of `decode` and `solveWith` have been slightly less general:++  ```diff+  -decode :: MonadPlus f => Solution -> a -> f     (Decoded a)+  +decode ::                Solution -> a -> Maybe (Decoded a)++  -solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n     (Decoded a))+  +solveWith :: (Monad m,              HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a))+  ```++  That is, these functions now use `Maybe` instead of an arbitrary `MonadPlus`.+  This change came about because:++  1. Practically all uses of `solveWith` in the wild are already picking `n` to+     be `Maybe`, and+  2. The behavior of `decode` and `solveWith` for `MonadPlus` instances besides+     `Maybe` could  produce surprising results, as this behavior was not well+     specified.+* Fix a bug in which `decode` could return inconsistent results with solution+  that underconstrain variables. For instance:++  ```hs+  do b <- exists+     pure [b, not b]+  ```++  Previously, this could decode to `[False, False]` (an invalid assignment).+  `ersatz` now adopts the convention that unconstrained non-negative `Literal`s+  will always be assigned `False`, and unconstrained negative `Literal`s will+  always be assigned `True`. This means that the example above would now decode+  to `[False, True]`.+ 0.4.13 [2022.11.01] ------------------- * Make the examples compile with `mtl-2.3.*`.

@@ -46,7 +46,7 @@ ```haskell verify_currying :: (MonadQSAT s m) => m () verify_currying = do-  (x::Bit, y::Bit, z::Bit) <- forall+  (x::Bit, y::Bit, z::Bit) <- forall_   assert $ ((x && y) ==> z) === (x ==> y ==> z) ``` 

@@ -1,5 +1,5 @@ name:           ersatz-version:        0.4.13+version:        0.5 license:        BSD3 license-file:   LICENSE author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi@@ -82,7 +82,9 @@               , GHC == 8.8.4               , GHC == 8.10.7               , GHC == 9.0.2-              , GHC == 9.2.2+              , GHC == 9.2.7+              , GHC == 9.4.5+              , GHC == 9.6.2 extra-source-files:   .gitignore   .hlint.yaml@@ -168,7 +170,7 @@   build-depends:     array                >= 0.2      && < 0.6,     base                 >= 4.9      && < 5,-    bytestring           >= 0.10.4.0 && < 0.12,+    bytestring           >= 0.10.4.0 && < 0.13,     containers           >= 0.2.0.1  && < 0.7,     data-default         >= 0.5      && < 0.8,     lens                 >= 4        && < 6,@@ -270,6 +272,21 @@ -- --   hs-source-dirs: tests --   Main-is: properties.hs++test-suite hunit+  type: exitcode-stdio-1.0+  main-is: HUnit.hs+  hs-source-dirs: tests+  build-depends:+    base,+    containers,+    data-default,+    ersatz,+    HUnit >= 1.2,+    test-framework >= 0.6,+    test-framework-hunit >= 0.2+  default-language: Haskell2010+  ghc-options: -Wall  test-suite speed   type: exitcode-stdio-1.0

@@ -27,7 +27,7 @@ import qualified Prelude  import Control.Applicative-import Control.Monad (MonadPlus(..), liftM2, liftM3)+import Control.Monad (liftM2, liftM3) import Data.Foldable (toList) import qualified Data.Foldable as Foldable import qualified Data.Traversable as Traversable@@ -123,8 +123,7 @@   type Decoded Bit = Bool   encode = bool   decode sol b-      = maybe (pure False <|> pure True) pure $-        solutionStableName sol (unsafePerformIO (makeStableName' b))+      = solutionStableName sol (unsafePerformIO (makeStableName' b))      -- The StableName didn’t have an associated literal with a solution,      -- recurse to compute the value.     <|> case b of@@ -135,7 +134,9 @@             decode sol $ if p then ct else cf           Not c'  -> not <$> decode sol c'           Var l   -> decode sol l-          Run _ -> mzero+          Run _ -> Nothing+      -- If all else false, just return False.+    <|> Just False     where       andMaybeBools :: [Maybe Bool] -> Maybe Bool       andMaybeBools mbs

@@ -30,13 +30,23 @@ -- | This class describes data types that can be marshaled to or from a SAT solver. class Codec a where   type Decoded a :: Type-  -- | Return a value based on the solution if one can be determined.-  decode :: MonadPlus f => Solution -> a -> f (Decoded a)+  -- | Return 'Just' a value based on the solution if one can be determined.+  -- Otherwise, return 'Nothing'.+  decode :: Solution -> a -> Maybe (Decoded a)   encode :: Decoded a -> a +-- | By convention, the 'decode' implementation will return 'False' for+-- unconstrained non-negative 'Literal's and 'True' for unconstrained negative+-- 'Literal's. instance Codec Literal where   type Decoded Literal = Bool-  decode s a = maybe (pure False <|> pure True) pure (solutionLiteral s a)+  decode s a = case solutionLiteral s a of+                 sol@(Just _) -> sol+                 Nothing+                   | i >= 0    -> Just False+                   | otherwise -> Just True+    where+      i = literalId a   encode True  = literalTrue   encode False = literalFalse 

@@ -53,6 +53,7 @@ import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import qualified Data.List as List+import qualified Data.List.NonEmpty as NE import Ersatz.Internal.Formula import Ersatz.Internal.Literal import Ersatz.Internal.StableName@@ -247,12 +248,12 @@                     , intDec (Seq.length tClauses)                     ]     quantified = foldMap go tQuantGroups-      where go ls = bLine0 (q (head ls) : map (intDec . getQuant) ls)+      where go ls = bLine0 (q (NE.head ls) : map (intDec . getQuant) (NE.toList ls))             q Exists{} = char7 'e'             q Forall{} = char7 'a'     clauses = foldMap bClause tClauses -    tQuantGroups = List.groupBy eqQuant (qdimacsQuantified t)+    tQuantGroups = NE.groupBy eqQuant (qdimacsQuantified t)       where         eqQuant :: Quant -> Quant -> Bool         eqQuant Exists{} Exists{} = True@@ -311,9 +312,10 @@   -- "Unbound atoms are to be considered as being existentially quantified in   -- the first (i.e., the outermost) quantified set." per QDIMACS standard.   -- Skip the implicit first existentials.-  qdimacsQuantified q-    | IntSet.null (q^.universals) = []-    | otherwise = quants [head qUniversals..lastAtom'] qUniversals+  qdimacsQuantified q =+    case qUniversals of+      []    -> []+      (i:_) -> quants [i..lastAtom'] qUniversals     where       lastAtom'   = qdimacsNumVariables q       qUniversals = IntSet.toAscList (q^.universals)

@@ -24,6 +24,9 @@  data Solution = Solution   { solutionLiteral    :: Literal -> Maybe Bool+    -- ^ If a 'Literal' is uniquely assigned to a particular value, this will+    -- return 'Just' of that value. If a 'Literal' is unconstrained (i.e., it+    -- can be assigned either 'True' or 'False'), this will return 'Nothing'.   , solutionStableName :: StableName () -> Maybe Bool   } 

@@ -14,7 +14,6 @@   , solveWith   ) where -import Control.Monad import Control.Monad.State import Data.Default import Ersatz.Codec@@ -24,9 +23,39 @@ import Ersatz.Solver.Minisat import Ersatz.Solver.Z3 +-- | @'solveWith' solver prob@ solves a SAT problem @prob@ with the given+-- @solver@. It returns a pair consisting of:+--+-- 1. A 'Result' that indicates if @prob@ is satisfiable ('Satisfied'),+--    unsatisfiable ('Unsatisfied'), or if the solver could not determine any+--    results ('Unsolved').+--+-- 2. A 'Decoded' answer that was decoded using the solution to @prob@. Note+--    that this answer is only meaningful if the 'Result' is 'Satisfied' and+--    the answer value is in a 'Just'.+--+-- Here is a small example of how to use 'solveWith':+--+-- @+-- import Ersatz+--+-- main :: IO ()+-- main = do+--   res <- 'solveWith' minisat $ do+--     (b1 :: Bit) <- exists+--     (b2 :: Bit) <- exists+--     assert (b1 === b2)+--     pure [b1, b2]+--   case res of+--     (Satisfied, Just answer) -> print answer+--     _ -> fail "Could not solve problem"+-- @+--+-- Depending on the whims of @minisat@, this program may print either+-- @[False, False]@ or @[True, True]@. solveWith ::-  (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) =>-  Solver s m -> StateT s m a -> m (Result, n (Decoded a))+  (Monad m, HasSAT s, Default s, Codec a) =>+  Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a)) solveWith solver m = do   (a, problem) <- runStateT m def   (res, litMap) <- solver problem

@@ -32,6 +32,20 @@ parseLiteral ('-':xs) = (read xs, False) parseLiteral xs = (read xs, True) +-- Parse the QDIMACS output format, which is described in+-- http://www.qbflib.org/qdimacs.html#output+parseOutput :: String -> [(Int, Bool)]+parseOutput out =+  case lines out of+    (_preamble:certLines) -> map parseCertLine certLines+    [] -> error "QDIMACS output without preamble"+  where+    parseCertLine :: String -> (Int, Bool)+    parseCertLine certLine =+      case words certLine of+        (_v:lit:_) -> parseLiteral lit+        _ -> error $ "Malformed QDIMACS certificate line: " ++ certLine+ -- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable. depqbfPath :: MonadIO m => FilePath -> Solver QSAT m depqbfPath path problem = liftIO $@@ -47,6 +61,6 @@     return $ (,) result $       case result of         Satisfied ->-          I.fromList $ map (parseLiteral . head . tail . words) $ tail $ lines out+          I.fromList $ parseOutput out         _ ->           I.empty

@@ -15,7 +15,7 @@ module Ersatz.Variable   ( Variable(..) #ifndef HLINT-  , forall+  , forall_ #endif   , exists @@ -32,8 +32,8 @@ exists = literally literalExists  #ifndef HLINT-forall :: (Variable a, MonadQSAT s m)  => m a-forall = literally literalForall+forall_ :: (Variable a, MonadQSAT s m) => m a+forall_ = literally literalForall #endif  class GVariable f where

@@ -0,0 +1,38 @@+-- | @HUnit@-based unit tests for @ersatz@.+module Main where++import Prelude hiding ((||), (&&), not)++import Data.Default+import qualified Data.IntMap.Strict as IntMap++import Test.Framework+import Test.Framework.Providers.HUnit+import Test.HUnit (Assertion, (@?=))++import Ersatz+import Ersatz.Internal.Literal++main :: IO ()+main = defaultMain tests++tests :: [Test]+tests =+  [ testGroup "unit tests"+      [ testCase "unconstrained literals" case_unconstrained_literals+      ]+  ]++-- A regression test for #60 and #76.+case_unconstrained_literals :: Assertion+case_unconstrained_literals =+    decode sol [b1, not b1, b2, not b2, b1 || b2, b1 && b2] @?=+      Just [False, True, False, True, False, False]+      -- There are other valid answers, but in practice, ersatz will choose this+      -- one due to the convention that the Codec Literal instance always+      -- assigns non-negative unconstrained Literals to False and negative+      -- unconstrained Literals to True.+  where+    sol = solutionFrom (IntMap.fromList [(1, True)]) (def :: SAT)+    b1 = Var $ Literal 2+    b2 = Var $ Literal 3

@@ -16,8 +16,12 @@   putStrLn $ unwords [ "n",  show n ]   (s, mgs) <- solveWith anyminisat $ do       gs <- replicateM n exists-      forM_ (zip gs $ tail gs) $ \ (x,y) -> assert ( x /== y )+      forM_ (zipTail gs) $ \ (x,y) -> assert ( x /== y )       return (gs :: [Bit])   case (s, mgs) of      (Satisfied, Just gs) -> do print $ length $ filter id gs      _ -> do return ()++zipTail :: [a] -> [(a, a)]+zipTail []         = []+zipTail xss@(_:xs) = zip xss xs

@@ -41,6 +41,8 @@   unknown :: MonadSAT s m => m a  -- | square matrices+--+-- Invariant: @dim >= 2@ newtype Matrix (dim::Nat)  a = Matrix [[a]]   deriving ( Show, Equatable, Orderable ) @@ -68,9 +70,33 @@  for = flip map -topleft (Matrix xss) = head (head xss)-botright (Matrix xss) = last (last xss)-topright (Matrix xss) = last (head xss)+topleft (Matrix xss) =+  case xss of+    ((x:_):_) -> x+    _ -> matrixInvariantViolated++botright (Matrix xss)+  | Just (_, xs) <- unsnoc xss+  , Just (_, x)  <- unsnoc xs+  = x+  | otherwise+  = matrixInvariantViolated++topright (Matrix xss)+  | xs:_ <- xss+  , Just (_, x) <- unsnoc xs+  = x+  | otherwise+  = matrixInvariantViolated++unsnoc :: [a] -> Maybe ([a], a)+unsnoc []     = Nothing+unsnoc (x:xs) = case unsnoc xs of+                  Nothing    -> Just ([], x)+                  Just (a,b) -> Just (x:a, b)++matrixInvariantViolated :: a+matrixInvariantViolated = error "Matrix invariant violated"  monotone m = positive (topleft m) && positive (botright m)