From 6cc7032cdecfccc651d4b7315862a42ad6ea10b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dan=20Ros=C3=A9n?= Date: Thu, 19 Apr 2012 18:09:59 +0200 Subject: [PATCH 1/2] Make equinox compile with ghc 7.4.1, perhaps not in the most elegant way --- Haskell/Equinox/ConSat.hs | 56 ++++++++++++++++----------------- Haskell/Equinox/FolSat.hs | 64 +++++++++++++++++++------------------- Haskell/Equinox/TermSat.hs | 6 ++-- Haskell/Flags.hs | 35 ++++++++++++--------- Haskell/Main.hs | 20 +++++++----- Haskell/Output.hs | 7 ++++- Haskell/ParseProblem.hs | 41 +++++++++++++----------- Haskell/Parsek.hs | 42 ++++++++++++------------- Haskell/Sat.hs | 2 +- 9 files changed, 145 insertions(+), 128 deletions(-) diff --git a/Haskell/Equinox/ConSat.hs b/Haskell/Equinox/ConSat.hs index a7dd793..3425071 100644 --- a/Haskell/Equinox/ConSat.hs +++ b/Haskell/Equinox/ConSat.hs @@ -5,7 +5,7 @@ module Equinox.ConSat , Weight -- :: * , wapp , weight - + , run -- :: C a -> IO a , lift -- :: IO a -> C a , contradiction -- :: C () @@ -22,7 +22,7 @@ module Equinox.ConSat , simplify -- :: C () ) where - + {- Equinox -- Copyright (c) 2003-2007, Koen Claessen @@ -51,10 +51,10 @@ import Data.Set( Set ) import qualified Data.Set as S import Data.Map( Map ) import qualified Data.Map as M -import IO +import System.IO import Flags import Control.Monad -import List( intersperse ) +import Data.List( intersperse ) import Observe @@ -72,7 +72,7 @@ instance Ord Lit where (a1 :=: b1) `compare` (a2 :=: b2) = upair a1 b1 `compare` upair a2 b2 (a1 :/=: b1) `compare` (a2 :/=: b2) = upair a1 b1 `compare` upair a2 b2 Bool b1 `compare` Bool b2 = b1 `compare` b2 - + Bool _ `compare` _ = LT _ `compare` Bool _ = GT Lit _ `compare` _ = LT @@ -99,7 +99,7 @@ neg (Bool b) = Bool (not b) data Weight = MkWeight{ depth :: !Int, siz :: !Int } deriving ( Eq, Ord ) - + wapp :: [Weight] -> Weight wapp ws = MkWeight (1 + maximum (0 : map depth ws)) (1 + sum (map siz ws)) @@ -189,7 +189,7 @@ setState :: State -> C () setState s = MkC (\_ -> return ((),s)) liftS :: Sat.S a -> C a -liftS m = MkC (\s -> do x <- m; return (x,s)) +liftS m = MkC (\s -> do x <- m; return (x,s)) lift :: IO a -> C a lift io = liftS (Sat.lift io) @@ -241,7 +241,7 @@ getModelValue (Bool b) = return b checkEqual :: Con -> Con -> C (Maybe Bool) checkEqual a b = do l <- norm (a :=: b) - getValue l + getValue l getRep :: Con -> C Con getRep a = @@ -291,7 +291,7 @@ addClause xs = do --lift (putStrLn (" [=> $true]")) --lift (hFlush stdout) return () - + [a :=: b] -> do --lift (putStrLn (" [=> " ++ show b ++ " := " ++ show a ++ "]")) --lift (hFlush stdout) @@ -312,17 +312,17 @@ addClause xs = LT -> a' :=: b' EQ -> Bool True GT -> b' :=: a' - + simp (a :/=: b) = neg `fmap` simp (a :=: b) simp l = return l - + showClause :: [Lit] -> String showClause c = concat . intersperse " | " . map show $ c - + solve :: Flags -> [Lit] -> C Bool solve flags xs = do xs' <- sequence [ norm x | x <- xs ] @@ -342,7 +342,7 @@ solve flags xs = where put v s = when (v <= verbose flags) $ lift $ do putStr s; hFlush stdout putLn v s = when (v <= verbose flags) $ lift $ do putStrLn s; hFlush stdout - + putTemp s = lift $ do putStr s hFlush stdout @@ -359,7 +359,7 @@ solve flags xs = check xs = do putLn 4 "--> ConSat: checking..." putTemp "(equ)" - + -- gather & set permanent positive equalities s <- getState peqs <- getPeqs [] (M.toList (compares s)) @@ -368,12 +368,12 @@ solve flags xs = setRep a b | (a,b) <- peqs ] - + -- gather & rebuild compares table info (eqs,neqs,comps) <- getEqNeq [] [] [] (M.toList (compares s)) - + let compares' = M.toList $ M.fromListWith (++) [ (ab,[x]) | (ab,x) <- comps ] - + bs1 <- sequence [ or `fmap` if a /= b then sequence @@ -405,14 +405,14 @@ solve flags xs = ] | ((a,b),x:ys) <- compares' ] - + s <- getState setState s{ compares = M.fromList [ (ab,x) | (ab@(a,b),x:_) <- compares' , a /= b ] } - + let eqTab = classes M.empty eqs graph = M.fromListWith S.union [ (x,S.singleton y) | (x,y) <- eqs ++ map swap eqs ] swap (x,y) = (y,x) @@ -446,7 +446,7 @@ solve flags xs = Just True -> do --lift (putStrLn ("top-true: " ++ show x ++ " " ++ show ab)) getPeqs (ab:peqs) abxs _ -> do getPeqs peqs abxs - + getEqNeq eqs neqs comps [] = do return (eqs,neqs,comps) @@ -460,11 +460,11 @@ solve flags xs = if bl then getEqNeq (ab:eqs) neqs comps' abxs else getEqNeq eqs (ab:neqs) comps' abxs - + rep eqTab x = case M.lookup x eqTab of Just x' -> x' - Nothing -> x + Nothing -> x classes eqTab [] = cut eqTab (M.keys eqTab) where @@ -498,24 +498,24 @@ solve flags xs = where bfs' backs ((x,z):xys) xys' | x == y = path (M.insert x z backs) [] y - + bfs' backs ((x,z):xys) xys' | M.lookup x backs == Nothing = bfs' (M.insert x z backs) xys ([(v,x) | v <- neighbors x] ++ xys') - + bfs' backs (_:xys) xys' = bfs' backs xys xys' - + bfs' backs [] [] = error "bfs: no path!" - + bfs' backs [] xys' = bfs' backs (reverse xys') [] - + neighbors x = case M.lookup x graph of Just xs -> S.toList xs Nothing -> error "bfs: not a node!" - + path backs p y | x == y = p | otherwise = case M.lookup y backs of diff --git a/Haskell/Equinox/FolSat.hs b/Haskell/Equinox/FolSat.hs index 96a4f21..1a25bce 100644 --- a/Haskell/Equinox/FolSat.hs +++ b/Haskell/Equinox/FolSat.hs @@ -26,8 +26,8 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. import Form import qualified Sat import Name( name, prim, (%), tr ) -import List hiding ( union, insert, delete ) -import Maybe +import Data.List hiding ( union, insert, delete ) +import Data.Maybe import Equinox.Fair import Equinox.TermSat hiding ( Lit(..) ) import Equinox.TermSat ( Lit ) @@ -37,7 +37,7 @@ import qualified Data.Set as S import Data.Map( Map ) import qualified Data.Map as M import Data.Maybe( isJust, fromJust ) -import IO +import System.IO import Flags import Control.Monad import Equinox.PSequence @@ -70,7 +70,7 @@ prove flags theory oblig = where cs = concatMap (norm []) (theory ++ oblig) (groundCs,nonGroundCs) = partition isGround cs - syms = S.filter (not . isVarSymbol) (symbols cs) + syms = S.filter (not . isVarSymbol) (symbols cs) ----------------------------------------------------------------------------- @@ -135,12 +135,12 @@ solveFOL flags syms st cls = , t == bool , nam == name "$answer" ] ++ [ name "$no_answer" ::: ([] :-> bool) ] - + min = head $ [ mn | mn@(nam ::: (_ :-> t)) <- S.toList syms , t == bool , nam == name "$min" - ] ++ [ name "$no_min" ::: ([] :-> bool) ] + ] ++ [ name "$no_min" ::: ([] :-> bool) ] refine rf mOldModel st ths = do ans <- getTable answer @@ -162,7 +162,7 @@ solveFOL flags syms st cls = else return () return Unsatisfiable - + -- found a candidate model, let's check it _ -> do model <- getModel mOldModel st @@ -195,7 +195,7 @@ solveFOL flags syms st cls = getModel mOldModel st = do tabs <- getModelTables st' <- getRep st - + let dom = S.toList $ S.fromList $ st' : [ c @@ -246,23 +246,23 @@ solveWithConflict flags mins ass = addClause (T.neg a : map T.neg mins) b <- solve flags (a:ass) if b then try mins else return () - + try mins return Nothing else do ls <- conflict let ass' = map neg ls - + let try [] = do return (Just ls) - + try (ass:asss) = do mls <- solveWithConflict flags [] ass case mls of Nothing -> do try asss _ -> do lift $ putStr "<>" return mls - + in try [ ass' \\ [a] | a <- ass' ] ----------------------------------------------------------------------------- @@ -281,12 +281,12 @@ clauseThread cl = thread True funs && deps `S.isSubsetOf` same model then skip dom deps else check ref model send) - + skip dom deps = do return ( do return False , thread dom deps ) - + check ref model send = Sat.run $ do vs <- sequence [ newValue (domain model) | x <- xs ] dom <- Sat.newLit @@ -301,12 +301,12 @@ clauseThread cl = thread True funs sequence_ [ buildLit (base,stars) st dom mmap fmap vmap l | l <- cl ] - + let findAllSubs i | i > 100 = -- an arbitrary choice! just testing -- ouch do Sat.lift (send '>') return (Left []) - + findAllSubs i = do b <- solveMin [ Sat.neg (v =? st) | v <- vs ] ([dom] ++ ms) if b then @@ -362,19 +362,19 @@ addClauseSub sub cl = where term (Var x) = do return (fromJust $ M.lookup x sub) - + term (Fun f [t]) | show f == "$weak" = do term t - + term (Fun f ts) = do as <- sequence [ term t | t <- ts ] f `app` as - + atom (s :=: t) = do a <- term s b <- term t return (a T.:=: b) - + literal (Pos a) = atom a literal (Neg a) = neg `fmap` atom a @@ -421,10 +421,10 @@ build opts@(base,stars) st mmap fmap vmap (Fun f ts) = let opts' | show f == "$answer" = (Sat.mkFalse,stars) | otherwise = opts vs <- sequence [ build opts' st mmap fmap vmap t | t <- ts ] - + let entries hist [] = do return [] - + entries hist ((xs,y):tab) = do e <- conj ( [ v =? x | (v,x) <- vs `zip` xs, x /= st ] ++ [ Sat.neg e | (zs,e) <- hist, and (zipWith over zs xs) ] @@ -442,9 +442,9 @@ build opts@(base,stars) st mmap fmap vmap (Fun f ts) = do return () es <- entries ((xs,e):hist) tab return (e:es) - + x `over` y = x==st || y==st || x==y - + es <- entries [] tab Sat.addClause (Sat.neg m : es) return z @@ -454,17 +454,17 @@ build opts@(base,stars) st mmap fmap vmap (Fun f ts) = Just tab' -> tab' Nothing -> [] ys = S.toList (S.fromList (map snd tab)) - + tab = ( map snd $ sort [ (number (==st) xs,(xs,y)) | (xs,y) <- tab' ] ) ++ [(replicate (arity f) st, df)] where number p = length . filter p - + df | isFunSymbol f = head (results ++ [st]) | otherwise = st - + results = map snd . reverse . sort @@ -493,7 +493,7 @@ solveMin xs as = if b then mins a else return True else do return True - + in do a <- Sat.newLit mins a else @@ -511,7 +511,7 @@ atMostOr k x ls | k == 0 = atMostOr k x ls | k >= length ls = do return () - + atMostOr k y ls = do Sat.addClause (y : map Sat.neg lsa) if not (null lsb) then @@ -583,7 +583,7 @@ newValue xs = new (map head . group . sort $ xs) where new [x] = do return [(x,Sat.mkTrue)] - + new [x,y] = do l <- Sat.newLit return [(x,Sat.neg l), (y, l)] @@ -597,7 +597,7 @@ newValue xs = new (map head . group . sort $ xs) getModelValueValue :: Value a -> Sat.S a getModelValueValue [(x,_)] = do return x - + getModelValueValue ((x,l):xls) = do b <- Sat.getModelValue l if b then return x else getModelValueValue xls @@ -609,7 +609,7 @@ writeModel file fs = do tabs <- getModelTables let ts = M.toList tabs lift $ writeFile file $ unlines $ concat $ intersperse [""] $ - [ [ show a ++ " := " ++ rep S.empty ts c ] + [ [ show a ++ " := " ++ rep S.empty ts c ] | (a,[([],c)]) <- ts , isFunSymbol a , take 2 (show a) == "a_" diff --git a/Haskell/Equinox/TermSat.hs b/Haskell/Equinox/TermSat.hs index 8d7a3d0..79b5333 100644 --- a/Haskell/Equinox/TermSat.hs +++ b/Haskell/Equinox/TermSat.hs @@ -57,11 +57,11 @@ import Data.Set( Set ) import qualified Data.Set as S import Data.Map( Map ) import qualified Data.Map as M -import List -import Maybe +import Data.List +import Data.Maybe import Form( Symbol ) import Flags -import IO +import System.IO import Control.Monad data State diff --git a/Haskell/Flags.hs b/Haskell/Flags.hs index c177380..79e99c2 100644 --- a/Haskell/Flags.hs +++ b/Haskell/Flags.hs @@ -33,6 +33,11 @@ OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -} +import System.Exit + ( exitWith + , ExitCode(..) + ) + import System.Environment ( getArgs ) @@ -41,17 +46,17 @@ import GHC.Environment ( getFullArgs ) -import System +import System.IO -import List +import Data.List ( groupBy , intersperse , (\\) ) -import Char +import Data.Char -import CPUTime +import System.CPUTime import Control.Monad.Instances() @@ -83,7 +88,7 @@ data Flags , temp :: FilePath , filelist :: Maybe FilePath , nrOfThreads :: Int - + -- infinox , elimit :: Int , plimit :: Int @@ -96,8 +101,8 @@ data Flags , outfile :: Maybe FilePath , prover :: Prover , leo :: Bool - - + + -- primitive , thisFile :: FilePath , files :: [FilePath] @@ -161,7 +166,7 @@ initFlags = , filelist = Nothing , leo = False , prover = E - + -- primitive , thisFile = "" , files = [] @@ -379,7 +384,7 @@ options = ] } - + , Option { long = "filelist" , tools = [Paradox, Equinox, Infinox] @@ -435,7 +440,7 @@ getFlags tool = putStr (unlines err) putStrLn "Try --help." exitWith (ExitFailure (-1)) - + Right f -> do t <- getNrOfThreads return f{ start = unPico picoT @@ -526,25 +531,25 @@ argNum = MkArg [""] $ \xs -> x:xs | all isDigit x -> Right (read x, xs) ('-':x):xs | all isDigit x -> Right (-read x, xs) _ -> Left ["expected a number"] - + argFile :: Arg FilePath argFile = MkArg [""] $ \xs -> case xs of x:xs -> Right (x, xs) _ -> Left ["expected a file"] - + argName :: Arg FilePath argName = MkArg [""] $ \xs -> case xs of x:xs -> Right (x, xs) _ -> Left ["expected a name"] - + argDots :: Arg FilePath argDots = MkArg [""] $ \xs -> case xs of x:xs -> Right (x, xs) _ -> Left ["expected a dot-spec"] - + argNums :: Arg [Int] argNums = MkArg [""] $ \xs -> case xs of @@ -576,7 +581,7 @@ argList as = MkArg ["<" ++ concat (intersperse " | " as) ++ ">*"] $ \xs -> where w = takeWhile (/= ',') s r = tail (dropWhile (/= ',') s) - + elts _ = Left ["argument list garbled"] parseFlags :: Tool -> Flags -> [String] -> Either [String] Flags diff --git a/Haskell/Main.hs b/Haskell/Main.hs index a581d1f..77830d3 100644 --- a/Haskell/Main.hs +++ b/Haskell/Main.hs @@ -26,11 +26,15 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. import Form import Control.Concurrent import Control.Exception -import System import Flags import ParseProblem import Clausify -import IO( hSetBuffering, stdout, BufferMode(..) ) +import System.IO( hSetBuffering, stdout, BufferMode(..) ) + +import System.Exit + ( exitWith + , ExitCode(..) + ) import Output @@ -90,24 +94,24 @@ main' solveProblem = n = length obligs let ?flags = ?flags{ thisFile = file } --sequence_ [ print t | t <- theory ] - + putOfficial ("SOLVING: " ++ file) case obligs of -- Satisfiable/Unsatisfiable [] -> do ans <- solveProblem theory [] putResult (show ans) - + -- CounterSatisfiable/Theorem [oblig] -> do ans <- solveProblem theory oblig putResult (show (toConjectureAnswer ans)) - + -- Unknown/Theorem obligs -> do let solveAll i [] = do return Theorem - + solveAll i (oblig:obligs) = do putSubHeader ("Part " ++ show i ++ "/" ++ show n) ans <- solveProblem theory oblig @@ -115,12 +119,12 @@ main' solveProblem = case ans of Unsatisfiable -> solveAll (i+1) obligs _ -> return (NoAnswerConjecture GaveUp) - + ans <- solveAll 1 obligs putResult (show ans) | file <- files ?flags ] - + require :: Bool -> IO () -> IO () require False m = do m; exitWith (ExitFailure 1) require True m = do return () diff --git a/Haskell/Output.hs b/Haskell/Output.hs index 050dfbf..7628f61 100644 --- a/Haskell/Output.hs +++ b/Haskell/Output.hs @@ -23,7 +23,12 @@ OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -} -import System +import System.Exit + ( exitWith + , ExitCode(..) + ) + +import System.IO import Flags import Form diff --git a/Haskell/ParseProblem.hs b/Haskell/ParseProblem.hs index e705389..daac217 100644 --- a/Haskell/ParseProblem.hs +++ b/Haskell/ParseProblem.hs @@ -23,13 +23,16 @@ OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -} -import System +import System.Exit ( exitWith , ExitCode(..) - , getEnv ) -import Char +import System.Environment + ( getEnv + ) + +import Data.Char ( isSpace , isAlpha , isAlphaNum @@ -38,25 +41,25 @@ import Char , isLower ) -import List +import Data.List ( intersperse , (\\) , tails , nub ) -import IO +import System.IO ( hFlush , stdout - , try ) -import System.IO.Error +import System.IO.Error as IO ( ioError , userError + , try ) -import Monad +import Control.Monad ( guard ) @@ -100,7 +103,7 @@ readProblemWithRoots roots name = do putStrLn "PARSE ERROR:" sequence [ putWarning s | s <- err ] exitWith (ExitFailure 1) - + Right (includes,clauses) -> do putStrLn "OK" hFlush stdout @@ -109,10 +112,10 @@ readProblemWithRoots roots name = where name_p | '.' `elem` name = name | otherwise = name ++ ".p" - + findFile [] = do return Nothing - + findFile (name:names) = do -- on Cygwin, the variable TPTP expects Windows paths! -- putStrLn ("(trying '" ++ name ++ "'...)") @@ -136,7 +139,7 @@ white = do munch isSpace option () $ do char '%' "" - many (satisfy (/= '\n')) + many (satisfy (/= '\n')) char '\n' white <|> @@ -147,11 +150,11 @@ white = do anyChar anyChar return () - + body (_:s) = do anyChar body s - + body [] = do return () body s @@ -278,7 +281,7 @@ atom bnd = form :: Bnd -> P Form form bnd = do foper bnd ops - "formula" + "formula" where ops = [ ("<=>", Equiv) , ("<~>", \x y -> nt (x `Equiv` y)) @@ -314,7 +317,7 @@ funit bnd = token ":" f <- funit ((`S.union` S.fromList vs) `fmap` bnd) return (foldr q f (map (\v -> name v ::: V top) vs)) - "formula unit" + "formula unit" lit :: P Form lit = @@ -323,7 +326,7 @@ lit = do token "~" a <- atom Nothing return (nt a) - "literal" + "literal" claus :: P Form claus = @@ -380,7 +383,7 @@ formula = return (s,t) | (s,t) <- typeList ] - + typeList = [ ("axiom", Fact) -- .. , ("theorem", Fact) -- I see no reason to distinguish these @@ -435,7 +438,7 @@ parseP s = , "Please report this as a bug in the parser." ] where - commas op = concat . intersperse (", " ++ op ++ " ") + commas op = concat . intersperse (", " ++ op ++ " ") ------------------------------------------------------------------------- -- the end. diff --git a/Haskell/Parsek.hs b/Haskell/Parsek.hs index 66b3379..f0129eb 100644 --- a/Haskell/Parsek.hs +++ b/Haskell/Parsek.hs @@ -28,17 +28,17 @@ module Parsek ( Parser -- :: * -> * -> *; Functor, Monad, MonadPlus , Expect -- :: *; = [String] , Unexpect -- :: *; = [String] - + -- parsers , satisfy -- :: Show s => (s -> Bool) -> Parser s s , look -- :: Parser s [s] , succeeds -- :: Parser s a -> Parser s (Maybe a) , string -- :: (Eq s, Show s) => [s] -> Parser s [s] - + , char -- :: Eq s => s -> Parser s s , noneOf -- :: Eq s => [s] -> Parser s s , oneOf -- :: Eq s => [s] -> Parser s s - + , spaces -- :: Parser Char () , space -- :: Parser Char Char , newline -- :: Parser Char Char @@ -71,14 +71,14 @@ module Parsek , chainl -- :: Parser s a -> Parser s (a -> a -> a) -> a -> Parser s a , chainr1 -- :: Parser s a -> Parser s (a -> a -> a) -> Parser s a , chainr -- :: Parser s a -> Parser s (a -> a -> a) -> a -> Parser s a - + , skipMany1 -- :: Parser s a -> Parser s () , skipMany -- :: Parser s a -> Parser s () , many1 -- :: Parser s a -> Parser s [a] , many -- :: Parser s a -> Parser s [a] , sepBy1 -- :: Parser s a -> Parser s sep -> Parser s [a] , sepBy -- :: Parser s a -> Parser s sep -> Parser s [a] - + -- parsing & parse methods , ParseMethod -- :: * -> * -> * -> * -> * , ParseResult -- :: * -> * -> *; = Either (e, Expect, Unexpect) r @@ -91,27 +91,27 @@ module Parsek , allResults -- :: ParseMethod s a (Maybe s) [a] , allResultsStaged -- :: ParseMethod s a (Maybe s) [[a]] , completeResults -- :: ParseMethod s a (Maybe s) [a] - + , shortestResultWithLeftover -- :: ParseMethod s a (Maybe s) (a,[s]) , longestResultWithLeftover -- :: ParseMethod s a (Maybe s) (a,[s]) , longestResultsWithLeftover -- :: ParseMethod s a (Maybe s) ([a],[s]) , allResultsWithLeftover -- :: ParseMethod s a (Maybe s) [(a,[s])] - + , completeResultsWithLine -- :: ParseMethod Char a Int [a] ) where - -import Monad + +import Control.Monad ( MonadPlus(..) , guard ) -import List +import Data.List ( union , intersperse ) -import Char +import Data.Char infix 0 infixr 1 <|>, <<|> @@ -148,7 +148,7 @@ instance Functor (Parser s) where instance Monad (Parser s) where return a = Parser (\fut -> fut a) - + Parser f >>= k = Parser (\fut -> f (\a -> let Parser g = k a in g fut)) @@ -158,7 +158,7 @@ instance Monad (Parser s) where instance MonadPlus (Parser s) where mzero = Parser (\fut exp -> Fail exp []) - + mplus (Parser f) (Parser g) = Parser (\fut exp -> f fut exp `plus` g fut exp) @@ -234,7 +234,7 @@ string s = then inputs xs else Fail (if null exp then [show s] else exp) [show [c]] ) - + in inputs s ) @@ -307,7 +307,7 @@ between :: Parser s open -> Parser s close -> Parser s a -> Parser s a between open close p = do open; x <- p; close; return x -- repetition - + skipMany1,skipMany :: Parser s a -> Parser s () skipMany1 p = do p; skipMany p skipMany p = let scan = (do p; scan) <|> return () in scan @@ -337,7 +337,7 @@ chainl1 p op = scan where scan = do x <- p; rest x rest x = (do f <- op; y <- p; rest (f x y)) <|> return x - + ------------------------------------------------------------------------- -- type ParseMethod, ParseResult @@ -395,7 +395,7 @@ longestResults p xs = scan p [] [] xs scan (Fail _ _) [] old _ = Right old scan (Fail _ _) new _ _ = Right new scan (Look f) new old xs = scan (f xs) new old xs - + allResultsStaged :: ParseMethod s a (Maybe s) [[a]] allResultsStaged p xs = Right (scan p [] xs) where @@ -404,7 +404,7 @@ allResultsStaged p xs = Right (scan p [] xs) scan (Result res p) ys xs = scan p (res:ys) xs scan (Fail _ _) ys _ = [ys] scan (Look f) ys xs = scan (f xs) ys xs - + allResults :: ParseMethod s a (Maybe s) [a] allResults p xs = scan p xs where @@ -471,9 +471,9 @@ longestResultsWithLeftover p xs = scan p empty empty xs scan (Fail _ _) ([],_) old _ = Right old scan (Fail _ _) new _ _ = Right new scan (Look f) new old xs = scan (f xs) new old xs - + empty = ([],Nothing) - + allResultsWithLeftover :: ParseMethod s a (Maybe s) [(a,[s])] allResultsWithLeftover p xs = scan p xs where @@ -503,7 +503,7 @@ completeResultsWithLine p xs = scan p 1 xs case scan p n xs of Left _ -> [] Right ress -> ress - + '\n' |> n = n+1 _ |> n = n diff --git a/Haskell/Sat.hs b/Haskell/Sat.hs index bfcee58..b55020d 100644 --- a/Haskell/Sat.hs +++ b/Haskell/Sat.hs @@ -69,7 +69,7 @@ import Foreign.Marshal.Alloc ( malloc, free ) import System.IO ( FilePath ) import Foreign.Storable ( Storable ) import Control.Exception ( finally ) -import Random +import System.Random import Form ( Signed(..), the, sign ) From b0ab9d655bd0d510038c8fed6b1bdabee34144c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dan=20Ros=C3=A9n?= Date: Thu, 19 Apr 2012 18:12:09 +0200 Subject: [PATCH 2/2] Make paradox compile with ghc 7.4.1 --- Haskell/Paradox/AnalysisTypes.hs | 16 ++--- Haskell/Paradox/Flatten.hs | 105 +++++++++++++++--------------- Haskell/Paradox/Instantiate.hs | 24 +++---- Haskell/Paradox/Main.hs | 36 +++++----- Haskell/Paradox/SolveInstances.hs | 50 +++++++------- 5 files changed, 117 insertions(+), 114 deletions(-) diff --git a/Haskell/Paradox/AnalysisTypes.hs b/Haskell/Paradox/AnalysisTypes.hs index 44dc51e..42d5668 100644 --- a/Haskell/Paradox/AnalysisTypes.hs +++ b/Haskell/Paradox/AnalysisTypes.hs @@ -45,12 +45,12 @@ import Data.STRef , writeSTRef ) -import Char +import Data.Char ( ord , chr ) -import List +import Data.List ( nub ) @@ -103,7 +103,7 @@ inferTerm (Fun f xs) = inferAndUnify :: Symbol -> [Term] -> [TypeId s] -> T s () inferAndUnify s xs ts - | length xs == length ts = + | length xs == length ts = sequence_ [ do t' <- inferTerm x t =:= t' @@ -155,7 +155,7 @@ runT' (MkT m) = ] typeIds' <- sequence - [ do ((_,eq),t,_) <- typeInfo t' + [ do ((_,eq),t,_) <- typeInfo t' return (t,eq) | t' <- [ t | (_,ts) <- M.toList ps', t <- ts ] ++ [ t | (_,(ts,tr)) <- M.toList fs', t <- tr:ts ] @@ -349,7 +349,7 @@ typeInfo (MkTypeId i ref) = Right t -> do (inf,i,c) <- typeInfo t writeSTRef ref (Right (MkTypeId i c)) return (inf,i,c) - + touchEq :: TypeId s -> Equality -> T s () touchEq t eq' = do ((n,eq),_,ref) <- lift (typeInfo t) @@ -417,17 +417,17 @@ MkTypeId i1 ref1 =:= MkTypeId i2 ref2 = do writeSTRef ref1 (Right (MkTypeId i2 ref2)) writeSTRef ref2 (Left (n1+n2,(eq1 `max` eq2))) return (i2,ref2) - + | otherwise -> do writeSTRef ref2 (Right (MkTypeId i1 ref1)) writeSTRef ref1 (Left (n1+n2,(eq1 `max` eq2))) return (i1,ref1) - + Right (MkTypeId i2' ref2') -> do (i,ref) <- unify i1 ref1 i2' ref2' writeSTRef ref2 (Right (MkTypeId i ref)) return (i,ref) - + Right (MkTypeId i1' ref1') -> do (i,ref) <- unify i1' ref1' i2 ref2 writeSTRef ref1 (Right (MkTypeId i ref)) diff --git a/Haskell/Paradox/Flatten.hs b/Haskell/Paradox/Flatten.hs index e0b1aa1..8779323 100644 --- a/Haskell/Paradox/Flatten.hs +++ b/Haskell/Paradox/Flatten.hs @@ -29,19 +29,22 @@ import Data.Set( Set ) import qualified Data.Set as S import Data.Map( Map ) import qualified Data.Map as M -import List ( (\\), sortBy, minimumBy, partition ) import Paradox.AnalysisTypes import Paradox.Instantiate -import Maybe +import Data.Maybe ( fromJust ) -import Monad +import Control.Monad ( mplus ) -import List +import Data.List ( groupBy + , (\\) + , sortBy + , minimumBy + , partition , sort ) @@ -61,10 +64,10 @@ macify cs = ([(t,length ts)|(t,ts) <- cliques], flattenedCs, functionCs) ] ] ++ splitAll (concatMap (flatten assignCons) (defCs ++ coreCs)) - + (ds, defCs, coreCs) = definitions cs - + functionCs = [ Uniq (Bind y ( [ Pos (t :=: Var y) ] @@ -128,21 +131,21 @@ findClique [] units = [] findClique ts units = S.toList (largestClique S.empty graph) where cons = S.fromList ts - + (posInfo, negInfo) = foldr gather (S.empty, S.empty) units where gather (Pos p) (pos, neg) = (pos `S.union` inst p, neg) gather (Neg p) (pos, neg) = (pos, neg `S.union` inst p) - + inst p = S.fromList [ norm (subst sub p) | sub <- subs (S.toList (free p)) ] where norm (a :=: b) | b < a = b :=: a norm p = p - + subs [] = [ids] subs (x:xs) = [ (x |=> t) |+| sub | sub <- subs xs, t <- ts ] - - edges = + + edges = [ (a,b) | (a,b) <- pairs (S.toList cons) , a `notEqual` b @@ -163,8 +166,8 @@ findClique ts units = S.toList (largestClique S.empty graph) replace a b a' | a == a' = b replace a b (Fun f xs) = Fun f (map (replace a b) xs) - - graph = + + graph = M.fromListWith S.union $ concat [ [(a, S.singleton b), (b, S.singleton a)] | (a,b) <- edges @@ -172,7 +175,7 @@ findClique ts units = S.toList (largestClique S.empty graph) ++ [ (a, S.empty) | a <- ts ] - + largestClique cl gr | M.null gr = cl | S.size cl >= 1 + S.size bs @@ -207,7 +210,7 @@ definitions cs = ([ f | (_, Fun f _) <- list ], defCs, coreCs) ] where ts = topterms cs - + list = [ (t, Fun (df % i ::: (map typ xs :-> typ t)) xs) | (t,i) <- deepTerms `zip` [1..] @@ -234,13 +237,13 @@ definitions cs = ([ f | (_, Fun f _) <- list ], defCs, coreCs) norm (Fun f xs) sub ws k = norms xs sub ws $ \xs' sub' ws' -> k (Fun f xs') sub' ws' - + norms [] sub ws k = k [] sub ws norms (t:ts) sub ws k = norm t sub ws $ \t' sub' ws' -> norms ts sub' ws' $ \ts' sub'' ws'' -> k (t':ts') sub'' ws'' - + isOkTerm top (Var _) = False isOkTerm top (Fun _ xs) = any (not . isVar) xs -- && S.size (free xs) <= 1 @@ -249,7 +252,7 @@ definitions cs = ([ f | (_, Fun f _) <- list ], defCs, coreCs) where isVar (Var _) = True isVar _ = False - + isAlreadyConnected vs (Var v) = vs `S.isSubsetOf` S.fromList [v] isAlreadyConnected vs (Fun _ xs) = vs `S.isSubsetOf` S.fromList [ v | Var v <- xs ] || any (isAlreadyConnected vs) xs @@ -270,7 +273,7 @@ definitions cs = ([ f | (_, Fun f _) <- list ], defCs, coreCs) replaceLit (Neg a) = Neg (replaceAtom a) replaceAtom (a :=: b) = replace a :=: replace b - + replace (Var v) = Var v replace t@(Fun f xs) = case M.lookup t' tab of @@ -286,12 +289,12 @@ flatten :: (Map Term Term) -> Clause -> [Clause] flatten assignCons ls = simplify (defs ++ flatLs) where fls = free ls - + vs = [ v | i <- [1..] , let v = vr % i ] - + tab = M.fromList [ (t,v) @@ -301,11 +304,11 @@ flatten assignCons ls = simplify (defs ++ flatLs) Var v -> v _ -> fv ::: V (typ t) ] - + var t = case M.lookup t assignCons of Just ci -> ci - Nothing + Nothing | tdomain (typ t) == Just 1 -> Fun (elt 1) [] | otherwise -> Var (case M.lookup t tab of Just t' -> t' @@ -316,12 +319,12 @@ flatten assignCons ls = simplify (defs ++ flatLs) | (t@(Fun f ts), v) <- M.toList tab , M.lookup t assignCons == Nothing ] - + flatLs = [ flat `fmap` l | l <- ls ] - + flat (Fun p ts :=: b) | b == truth = p `prd` map var ts @@ -348,11 +351,11 @@ simplify = simp , c3 <- substVarEq c2 , c4 <- substFunEq c3 ] - + trivial ls | any ((`S.member` S.fromList ls) . negat) ls = [] | otherwise = [ls] - + identEq ls = case [ () | Pos (s :=: t) <- ls @@ -360,33 +363,33 @@ simplify = simp ] of [] -> [ls] _ -> [] - + substVarEq ls = substVar [] ls where substVar ls' (Neg (Var v :=: Var w) : ls) = simp (subst (v |=> Var w) (ls' ++ ls)) - + substVar ls' (Neg (Var v :=: t@(Fun c [])) : ls) | isElt c = simp (subst (v |=> t) (ls' ++ ls)) - + substVar ls' (Neg ((Fun c1 []) :=: t@(Fun c2 [])) : ls) | isElt c1 && isElt c2 && c1 /= c2 = [] - + substVar ls' (l:ls) = substVar (l:ls') ls - + substVar ls' [] = [ls'] - + substFunEq ls = substFun [] ls where substFun ls' (l@(Neg (t :=: Var v)) : ls) | not (v `S.member` free t) = substTerm v t [] (ls' ++ ls) (substFun (l:ls') ls) - + substFun ls' (l:ls) = substFun (l:ls') ls - + substFun ls' [] = [ls'] @@ -396,7 +399,7 @@ simplify = simp where leftSubst = t1 == Var v && isSmall t2 rightSubst = t2 == Var v && isSmall t1 - + isSmall (Var _) = True isSmall (Fun c []) = isElt c isSmall _ = False @@ -404,7 +407,7 @@ simplify = simp substTerm v t ls' (l:ls) k | v `S.member` free l = k | otherwise = substTerm v t (l:ls') ls k - + substTerm v t ls' [] k = simp ls' @@ -419,7 +422,7 @@ purify cs where (ps,cs') = pure M.empty cs (ps',cs'') = purify cs' - + pure tab [] = ( removePs , [ c @@ -433,7 +436,7 @@ purify cs | (p,sgns) <- M.toList tab , S.size sgns == 1 ] - + setPs = S.fromList [ p | (p,_) <- removePs ] isRemoveP (Fun p _ :=: b) = b == truth && p `S.member` setPs isRemoveP _ = False @@ -442,7 +445,7 @@ purify cs where posP = S.fromList [ p | Pos (Fun p xs :=: b) <- c, b == truth ] negP = S.fromList [ p | Neg (Fun p xs :=: b) <- c, b == truth ] - + occurs = M.fromList $ [ (pn,S.singleton True) | pn <- S.toList $ posP `S.difference` negP ] ++ @@ -463,7 +466,7 @@ splitAll cs = splitting 1 cs (\_ -> []) connections = [ (v,ws) - | (v,ws) <- + | (v,ws) <- M.toList $ M.fromListWith S.union [ (v,S.fromList ws) @@ -509,27 +512,27 @@ splitAll cs = splitting 1 cs (\_ -> []) break i ls k = case [ ls' - + -- only try when number of variables is at least 3 | S.size (free ls) >= 3 - + -- for all "non-recursive" definitions in ls , def@(Neg (t@(Fun _ _) :=: Var y)) <- ls , not (y `S.member` free t) - + -- gather literals which contain y , let (lsWithY, lsWithoutY) = partition ((y `S.member`) . free) (ls \\ [def]) - + -- there should be at least 2 such literals ... , lWithY:(lsWithY'@(_:_)) <- [lsWithY] - + -- now, partition the literals containing y -- into two separate groups, not containing -- any overlapping variables except the variables in def , let connToY = y `S.delete` free lsWithY ok = free def - + (lsLeft, lsRight) = part (free lWithY) [lWithY] [] lsWithY' where @@ -537,15 +540,15 @@ splitAll cs = splitting 1 cs (\_ -> []) part vs left right (l:ls) | S.size ((ws `S.intersection` vs) `S.difference` ok) == 0 = part vs left (l:right) ls - + | otherwise = part (vs `S.union` ws) (l:left) right ls where ws = free l - + -- they should not all end up on one side , not (null lsRight) - + -- construct the new clause with the extra literal , let y' = prim "C" % i ::: typing y ls' = [ def @@ -558,7 +561,7 @@ splitAll cs = splitting 1 cs (\_ -> []) -- _ -> set ls : k i [] -> ls : k i (ls':_) -> splitting (i+1) [ls'] k - + select :: [a] -> [(a,[a])] select [] = [] select (x:xs) = (x,xs) : [ (y,x:ys) | (y,ys) <- select xs ] diff --git a/Haskell/Paradox/Instantiate.hs b/Haskell/Paradox/Instantiate.hs index 9caebac..3d0f11f 100644 --- a/Haskell/Paradox/Instantiate.hs +++ b/Haskell/Paradox/Instantiate.hs @@ -29,7 +29,7 @@ import Data.Set( Set ) import qualified Data.Set as S import Data.Map( Map ) import qualified Data.Map as M -import List hiding ( insert, delete, union ) +import Data.List hiding ( insert, delete, union ) import Paradox.AnalysisTypes import Flags @@ -62,13 +62,13 @@ instantiate flags predefs cs qcs = c1 `siz` c2 = length c1 `compare` length c2 iqcs = [1..] `zip` qcs - + syms = symbols cs isGround c = S.size (free c) == 0 - + con k = Fun (elt k) [] - + listType = head $ [ tp | nil ::: ([] :-> tp) <- S.toList syms, nil == name "$nil" ] ++ [ Type (prim "list") Nothing Full ] @@ -86,7 +86,7 @@ instantiate flags predefs cs qcs = where transp [] = repeat [] transp xss = concat [ x | x:_ <- xss ] : transp [ xs | _:xs <- xss ] - + symmForType tp _ | tp == listType = -- d == 1 [ [ [ Pos (fnil :=: con 1) ] @@ -127,7 +127,7 @@ instantiate flags predefs cs qcs = fnil = Fun (name "$nil" ::: ([] :-> listType)) [] ftail (xs,xs') = prd (name "$tail" ::: ([listType,listType] :-> bool)) [xs,xs'] fhead xs = Fun (name "$head" ::: ([listType] :-> elemType)) [xs] - + symmForType tp predef = zipWith (\k f -> f k) [1..] -- do not use symmetries before predef size @@ -176,7 +176,7 @@ instantiate flags predefs cs qcs = ] where numCons = predef + length allCons - + allCons = [ t | Uniq (Bind v c) <- qcs @@ -209,10 +209,10 @@ instantiate flags predefs cs qcs = where dom = (dm % k) ::: ([] :-> bool) domk = dom `prd` [] - + newCon = con k allCons = newCon : oldCons - + qclauses = [ c | (i,qc) <- iqcs @@ -224,7 +224,7 @@ instantiate flags predefs cs qcs = | c <- qclauses , not (isGround c) ] - + clauses = [ ForAll ( -- constant equalities @@ -256,7 +256,7 @@ instantiate flags predefs cs qcs = ++ qclauses ) ] - + atLeastOne :: QClause -> [Clause] atLeastOne (Uniq (Bind v@(_ ::: V tp) c)) = [ pre @@ -269,7 +269,7 @@ instantiate flags predefs cs qcs = | k > k' -> [] _ -> [(Neg domk :)] ] - + atMostOne :: Int -> QClause -> [Clause] atMostOne i (Uniq (Bind v@(_ ::: V tp) c)) = [ [negat l, a] diff --git a/Haskell/Paradox/Main.hs b/Haskell/Paradox/Main.hs index dc3cf4c..e57f576 100644 --- a/Haskell/Paradox/Main.hs +++ b/Haskell/Paradox/Main.hs @@ -39,19 +39,19 @@ import Paradox.SolveInstances import Output -import IO +import System.IO ( hFlush , stdout ) -import List +import Data.List ( group , sort , nub , intersperse ) -import System +import System.Exit ( exitWith , ExitCode(..) ) @@ -64,12 +64,12 @@ main = do putStrLn "Paradox, version 4.0, 2010-06-29." --putStrLn "*** NOTE: THIS IS A NON-STANDARD, DELIBERATELY UNSOUND VERSION!" Main.main Paradox solveProblem - + ------------------------------------------------------------------------- -- problem solveProblem :: (?flags :: Flags) => [Clause] -> [Clause] -> IO ClauseAnswer -solveProblem theory oblig = +solveProblem theory oblig = do {- putStrLn "==> Input clauses" sequence_ [ putStrLn (showClause c) | c <- csIn ] @@ -137,28 +137,28 @@ solveProblem theory oblig = bigDom = if isFinite then maxDomain else 9999999 -- max domain size big = 999999999 - + isize v = case tdomain t of Nothing -> bigDom Just k -> k where - V t = typing v - + V t = typing v + groupN :: Ord a => [a] -> [(Int,a)] groupN = map (\xs -> (length xs, head xs)) . group . sort - + mask :: Symbolic a => a -> [(Int, Int)] mask c = groupN . map isize . S.toList . free $ c - + masks = groupN $ map mask fcs ++ map mask qcs - + estimate n = let x = sum [ fromIntegral a * product [ (fromIntegral n' `min` n) ^ fromIntegral b @@ -166,7 +166,7 @@ solveProblem theory oblig = ] | (a,msk) <- masks ] - + in x -- spy "est" (n,x) `seq` x ns' = [ i | i <- [1..n], i >= minSize ] @@ -181,7 +181,7 @@ solveProblem theory oblig = numFuns = length [ () | f <- S.toList syms, _ :-> b <- [typing f], b /= bool ] numCons = length [ () | c <- S.toList syms, [] :-> b <- [typing c], b /= bool ] - + (isFinite,maxDomain,maxDom,whyDom) = minn [ (numCons == numFuns, maximum (1 : [ n | t <- typs , Just n <- [tsize t] @@ -197,15 +197,15 @@ solveProblem theory oblig = ns -> (True, mn, show mn, " (" ++ why ++ ")") where (mn,why) = foldr1 (\(a,x) (b,y) -> if a < b then (a,x) else (b,y)) ns - + limited c = case c of Pos (Var x :=: t) : ls | not (x `S.member` free t) && lim x ls -> Just n - + Pos (t :=: Var x) : ls | not (x `S.member` free t) && lim x ls -> Just n - + _ -> Nothing where lim x [] = True @@ -214,8 +214,8 @@ solveProblem theory oblig = lim x (Pos (t :=: Var y) : ls) | x == y && not (x `S.member` free t) = lim x ls lim x _ = False - + n = length c - + --------------------------------------------------------------------------- -- the end. diff --git a/Haskell/Paradox/SolveInstances.hs b/Haskell/Paradox/SolveInstances.hs index 39b1d18..45dc798 100644 --- a/Haskell/Paradox/SolveInstances.hs +++ b/Haskell/Paradox/SolveInstances.hs @@ -33,12 +33,12 @@ import Data.Map( Map ) import qualified Data.Map as M import Data.IORef import Flags -import List( sortBy, intersperse ) -import IO +import Data.List( sortBy, intersperse ) +import System.IO import Paradox.Instantiate import Output import Paradox.AnalysisTypes -import Monad +import Control.Monad {- data Loc = Loc @@ -60,7 +60,7 @@ getLit = undefined solveInstances :: Flags -> [(Symbol,Bool)] -> Int -> [(Int,Bool,Symbol,[ClauseSet])] -> IO (ClauseAnswer,Int) solveInstances flags predsPure minSize css = do ref <- newIORef (M.empty,M.empty) - + let getFunLoc f = do (tabf,tabp) <- lift $ readIORef ref case M.lookup f tabf of @@ -68,7 +68,7 @@ solveInstances flags predsPure minSize css = lift $ writeIORef ref (M.insert f loc tabf,tabp) return loc Just loc -> do return loc - + getPredLoc p = do (tabf,tabp) <- lift $ readIORef ref case M.lookup p tabp of @@ -76,13 +76,13 @@ solveInstances flags predsPure minSize css = lift $ writeIORef ref (tabf,M.insert p loc tabp) return loc Just loc -> do return loc - + processClauseSet k (ForAll cs) = do sequence_ [ processClause Nothing k c | c <- cs ] - + processClauseSet k (ForAllNew k' cs) = do sequence_ [ processClause (Just k') k c | c <- cs ] - + processClause mn k c = do ls' <- mapM processLit ls let args = [ isize t | v <- vs, let V t = typing v ] @@ -108,16 +108,16 @@ solveInstances flags predsPure minSize css = where ls = c vs = S.toList (free c) - + isize t = case tdomain t of Just n -> n `min` k Nothing -> k - + processLit l = do a <- processAtom (the l) return (fmap (const a) l) - + processAtom (Fun f xs :=: y) | y /= truth && not (isElt f) = do loc <- getFunLoc f if arity f /= length xs then error ("arity fel! " ++ show (f,typing f)) else return () @@ -125,27 +125,27 @@ solveInstances flags predsPure minSize css = where xs' = map processTerm xs y' = processTerm y - + processAtom (Fun p xs :=: b) | b == truth = do loc <- getPredLoc p return (loc :@ xs') where xs' = map processTerm xs - + processAtom (a :=: b) = do loc <- getPredLoc (eq ::: ([top,top] :-> bool)) return (loc :@ (map processTerm [a,b])) - + processTerm (Var v) = ArgV (v `ind` vs) - + processTerm (Fun (c ::: _) []) | isEltName c = ArgN (getIndex c) - + x `ind` (y:ys) | x == y = 1 - | otherwise = 1 + (x `ind` ys) - + | otherwise = 1 + (x `ind` ys) + domains minSize [] = do return (NoAnswerClause GaveUp,minSize) @@ -156,24 +156,24 @@ solveInstances flags predsPure minSize css = return () --lift $ sequence_ [ putStrLn s | c <- clauses, s <- showClauseSet c ] let clauses' = flat clauses - + flat [] = [] flat (ForAll cs : ds) = map (\c -> ForAll [c]) cs ++ flat ds flat (ForAllNew k' cs : ds) = map (\c -> ForAllNew k' [c]) cs ++ flat ds tot = length clauses' - + sequence_ [ do --lift $ print c processClauseSet k c - | (i,c) <- [1..] `zip` clauses' + | (i,c) <- [1..] `zip` clauses' ] - + assumption <- getPredLoc assump >>= \l -> return (Pos (l :@ [])) ass <- getLit assumption - + --simplify True False - + --lift $ putStrLn ("solving...") r <- if minSize > k then return False else solve [ass] if r then @@ -317,7 +317,7 @@ printTheModel flags k ref predsPure = putStrLnTSTP s | tstp flags = lift $ putStrLn s | otherwise = return () - + (x,_) `first` (y,_) = show x `compare` show y tdomain' t = case tdomain t of