diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -4,6 +4,10 @@ ## Released changes +### 0.4.1 + +- add support for different SAT solvers + ### 0.4.0.3 - fix terminal spamming due to process abortion on Windows diff --git a/call-alloy.cabal b/call-alloy.cabal --- a/call-alloy.cabal +++ b/call-alloy.cabal @@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.0. +-- This file has been generated from package.yaml by hpack version 0.36.0. -- -- see: https://github.com/sol/hpack name: call-alloy -version: 0.4.0.3 +version: 0.4.1 synopsis: A simple library to call Alloy given a specification description: Please see the README on GitHub at category: Language @@ -23,6 +23,7 @@ ChangeLog.md data-files: alloy/RunAlloy.class + alloy/SATSolver.class org.alloytools.alloy.dist.jar commons-cli/commons-cli-1.5.0.jar commons-cli/NOTICE.txt @@ -53,8 +54,8 @@ build-depends: async >=2.2.1 && <2.3 , base >=4.12 && <5 - , bytestring >=0.10.4 && <0.12 - , containers ==0.6.* + , bytestring >=0.10.4 && <0.13 + , containers >=0.6 && <0.8 , directory ==1.3.* , extra ==1.7.* , filepath ==1.4.* @@ -67,7 +68,7 @@ if os(windows) cpp-options: -DWINDOWS build-depends: - Win32 >=2.5 && <2.14 + Win32 >=2.5 && <2.15 else build-depends: unix >=2.7 && <2.9 @@ -93,9 +94,9 @@ build-depends: async >=2.2.1 && <2.3 , base >=4.12 && <5 - , bytestring >=0.10.4 && <0.12 + , bytestring >=0.10.4 && <0.13 , call-alloy - , containers ==0.6.* + , containers >=0.6 && <0.8 , directory ==1.3.* , extra ==1.7.* , filepath ==1.4.* @@ -110,7 +111,7 @@ if os(windows) cpp-options: -DWINDOWS build-depends: - Win32 >=2.5 && <2.14 + Win32 >=2.5 && <2.15 else build-depends: unix >=2.7 && <2.9 diff --git a/data/alloy/RunAlloy.class b/data/alloy/RunAlloy.class Binary files a/data/alloy/RunAlloy.class and b/data/alloy/RunAlloy.class differ diff --git a/data/alloy/SATSolver.class b/data/alloy/SATSolver.class new file mode 100644 Binary files /dev/null and b/data/alloy/SATSolver.class differ diff --git a/src/Language/Alloy/Call.hs b/src/Language/Alloy/Call.hs --- a/src/Language/Alloy/Call.hs +++ b/src/Language/Alloy/Call.hs @@ -12,7 +12,8 @@ (as it is required by Alloy). -} module Language.Alloy.Call ( - CallAlloyConfig (maxInstances, noOverflow, timeout), + CallAlloyConfig (maxInstances, noOverflow, satSolver, timeout), + SatSolver (..), defaultCallAlloyConfig, existsInstance, getInstances, diff --git a/src/Language/Alloy/Internal/Call.hs b/src/Language/Alloy/Internal/Call.hs --- a/src/Language/Alloy/Internal/Call.hs +++ b/src/Language/Alloy/Internal/Call.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-| @@ -11,18 +12,22 @@ It provides data types and functions to interact with Alloy. -} module Language.Alloy.Internal.Call ( - CallAlloyConfig (maxInstances, noOverflow, timeout), + CallAlloyConfig (maxInstances, noOverflow, satSolver, timeout), + SatSolver (..), defaultCallAlloyConfig, getRawInstances, getRawInstancesWith, ) where import qualified Data.ByteString as BS ( - hGetLine, intercalate, stripPrefix, ) -import qualified Data.ByteString.Char8 as BS (unlines) +import qualified Data.ByteString.Char8 as BS ( + hGetLine, + putStrLn, + unlines, + ) import Control.Concurrent ( threadDelay, @@ -74,7 +79,8 @@ ) import Language.Alloy.RessourceNames ( - className, classPackage, + className, + classPackage, ) import Language.Alloy.Ressources ( alloyJar, @@ -84,6 +90,60 @@ import Paths_call_alloy (getDataDir) {-| +Available SAT solvers. +-} +data SatSolver + = BerkMin + -- ^ BerkMin + -- + -- * not tested + | Glucose + -- ^ Glucose + -- + -- * incremental + | Glucose41 + -- ^ Glucose41 + -- + -- * incremental + | Lingeling + -- ^ Lingeling + -- + -- * not incremental + | MiniSat + -- ^ MiniSat + -- + -- * incremental + | MiniSatProver + -- ^ MiniSatProver + -- + -- * incremental + | PLingeling + -- ^ PLingeling + -- + -- * not incremental + | SAT4J + -- ^ SAT4J + -- + -- * incremental + | Spear + -- ^ Spear + -- + -- * not tested + deriving (Bounded, Enum, Eq, Read, Show) + +toParameter :: SatSolver -> String +toParameter = \case + BerkMin -> "BERKMIN" + Glucose -> "GLUCOSE" + Glucose41 -> "GLUCOSE41" + Lingeling -> "LINGELING" + MiniSat -> "MINISAT" + MiniSatProver -> "MINISAT_PROVER" + PLingeling -> "PLINGELING" + SAT4J -> "SAT4J" + Spear -> "SPEAR" + +{-| Configuration for calling alloy. These are: * maximal number of instances to retrieve ('Nothing' for all) @@ -96,6 +156,9 @@ maxInstances :: !(Maybe Integer), -- | whether to not overflow when calculating numbers within Alloy noOverflow :: !Bool, + -- | the 'SatSolver' to choose. Note that some are not incremental, + -- i.e. will return only one solution, even if 'maxInstances' is set higher. + satSolver :: !SatSolver, -- | the time in microseconds after which to forcibly kill Alloy -- ('Nothing' for never) timeout :: !(Maybe Int) @@ -106,11 +169,13 @@ * retrieve all instances * do not overflow + * 'SAT4J' -} defaultCallAlloyConfig :: CallAlloyConfig defaultCallAlloyConfig = CallAlloyConfig { maxInstances = Nothing, noOverflow = True, + satSolver = SAT4J, timeout = Nothing } @@ -151,6 +216,7 @@ $ ["-cp", classPath, classPackage ++ '.' : className, "-i", show $ fromMaybe (-1) $ maxInstances config] ++ ["-o" | not $ noOverflow config] + ++ ["-s", toParameter (satSolver config)] createProcess callAlloy { std_out = CreatePipe, std_in = CreatePipe, @@ -191,7 +257,7 @@ (out, err) <- fst <$> concurrently (concurrently (getOutput hout) (getOutput herr)) evaluateAlloy - printContentOnError abort ph + printContentOnError out abort ph let err' = removeInfoLines err unless (null err') $ fail $ unpack $ BS.unlines err' return $ fmap (BS.intercalate "\n") @@ -211,11 +277,13 @@ getOutput h = catch (getOutput' h) (\(_ :: IOException) -> return [partialInstance]) - printContentOnError abort ph = do + printContentOnError out abort ph = do code <- waitForProcess ph aborted <- maybe (return False) readIORef abort when (code == ExitFailure 1 && not aborted) - $ putOutLn $ "Failed parsing the Alloy code:\n" <> content + $ putOutLn $ "Failed parsing the Alloy code?:\n" <> content + when (code == ExitFailure 2 && not aborted) + $ withLock outLock $ BS.putStrLn $ BS.unlines out partialInstance :: ByteString partialInstance = "---PARTIAL_INSTANCE---" diff --git a/test/Language/Alloy/CallSpec.hs b/test/Language/Alloy/CallSpec.hs --- a/test/Language/Alloy/CallSpec.hs +++ b/test/Language/Alloy/CallSpec.hs @@ -5,6 +5,8 @@ module Language.Alloy.CallSpec (spec) where import Control.Concurrent.Async (forConcurrently) +import Data.Foldable (for_) +import Data.List ((\\)) import Data.Map (Map) import Data.Set (Set) import Data.String.Interpolate (i) @@ -12,6 +14,7 @@ import Language.Alloy.Call ( CallAlloyConfig (..), + SatSolver (..), defaultCallAlloyConfig, existsInstance, getInstances, @@ -39,6 +42,16 @@ getInstances (Just 1) "pred a (a: Int) { a > a }\nrun a" `shouldReturn` [] it "giving not enough time should return no result" $ getInstancesWith cfg "pred a (a: Int) { a >= a }\nrun a" `shouldReturn` [] + for_ solvers $ \solver -> + it ("using solver " ++ show solver ++ " generates an instance") $ do + xs <- length <$> getInstancesWith + cfg { + maxInstances = Just 1, + satSolver = solver, + timeout = Nothing + } + (graph 2) + xs `shouldBe` 1 it "called in parallel does not create issues" $ do ys <- forConcurrently [1 .. 6] $ \x -> length <$> getInstances (Just $ x ^ (3 :: Integer)) (graph x) @@ -53,6 +66,8 @@ maxInstances = Nothing, timeout = Just 0 } + untested = [BerkMin, Spear] + solvers = [minBound ..] \\ untested graph :: Integer -> String graph x = [i|