picologic 0.1.2 → 0.2.0
raw patch · 9 files changed
+223/−89 lines, 9 filesdep ~basedep ~containersdep ~mtl
Dependency ranges changed: base, containers, mtl, parsec, picosat, pretty
Files
- LICENSE +1/−1
- picologic.cabal +8/−8
- src/Picologic/AST.hs +118/−27
- src/Picologic/Lexer.hs +1/−1
- src/Picologic/Parser.hs +6/−1
- src/Picologic/Pretty.hs +14/−5
- src/Picologic/Solver.hs +38/−21
- src/Picologic/Tseitin.hs +7/−12
- tests/tests.hs +30/−13
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2014, Stephen Diehl+Copyright (c) 2014-2016, Stephen Diehl Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to
picologic.cabal view
@@ -1,5 +1,5 @@ name: picologic-version: 0.1.2+version: 0.2.0 synopsis: Utilities for symbolic predicate logic expressions homepage: https://github.com/sdiehl/picologic license: MIT@@ -36,12 +36,12 @@ hs-source-dirs: src other-extensions: DeriveDataTypeable, BangPatterns build-depends: - base >= 2 && <5,- picosat,- containers,- mtl,- pretty,- parsec+ base >= 4.6 && <4.10,+ picosat >= 0.1 && <0.2,+ containers >= 0.5 && <0.6,+ mtl >= 2.1 && <2.4,+ pretty >= 1.1 && <1.2,+ parsec >= 3.1 && <3.2 default-language: Haskell2010 executable picologic@@ -54,7 +54,7 @@ base >= 2 && <5, picosat >= 0.1 && <0.2, containers >= 0.5 && <0.6,- mtl >= 2.1 && <2.2,+ mtl >= 2.1 && <2.4, pretty >= 1.1 && <1.2, parsec >= 3.1 && <3.2, process >= 1.1 && <1.2,
src/Picologic/AST.hs view
@@ -13,6 +13,10 @@ cnf, nnf, simp,+ isConst,+ propConst,+ subst,+ partEval ) where import Data.List@@ -34,6 +38,8 @@ | Disj Expr Expr -- ^ Logical disjunction | Iff Expr Expr -- ^ Logical biconditional | Implies Expr Expr -- ^ Material implication+ | Top -- ^ Constant true+ | Bottom -- ^ Constant false deriving (Eq, Ord, Data, Typeable) -- | Evaluate expression.@@ -41,9 +47,11 @@ eval vs (Var v) = fromMaybe False (M.lookup v vs) eval vs (Neg expr) = not $ eval vs expr eval vs (Conj e1 e2) = eval vs e1 && eval vs e2-eval vs (Disj e1 e2) = eval vs e1 || eval vs e2-eval vs (Implies e1 e2) = not (eval vs e1) || eval vs e2+eval vs (Disj e1 e2) = eval vs e1 || eval vs e2+eval vs (Implies e1 e2) = not (eval vs e1) || eval vs e2 eval vs (Iff e1 e2) = eval vs e1 == eval vs e2+eval vs (Top) = True+eval vs (Bottom) = False -- | Variables in expression variables :: Expr -> [Ident]@@ -55,31 +63,28 @@ go (Disj e1 e2) !vs = go e1 vs ++ go e2 vs go (Iff e1 e2) !vs = go e1 vs ++ go e2 vs go (Implies e1 e2) !vs = go e1 vs ++ go e2 vs+ go (Top) !vs = vs+ go (Bottom) !vs = vs -- | Negation normal form. -- (May result in exponential growth) nnf :: Expr -> Expr-nnf ex = case ex of- e@(Var _) -> e- e@(Neg (Var _)) -> e- Neg (Neg e) -> nnf e-- Conj e1 e2 -> nnf e1 `Conj` nnf e2- Neg (Conj e1 e2) -> nnf $ Neg e1 `Disj` Neg e2-- Disj e1 e2 -> nnf e1 `Disj` nnf e2- Neg (Disj e1 e2) -> nnf $ Neg e1 `Conj` Neg e2-- Implies e1 e2 -> nnf $ Neg e1 `Disj` e2- Neg (Implies e1 e2) -> nnf $ e1 `Conj` Neg e2-- Iff e1 e2 -> let a = e1 `Disj` Neg e2- b = Neg e1 `Disj` e2- in nnf $ a `Conj` b+nnf = transformDown nnf1 . propConst - Neg (Iff e1 e2) -> let a = e1 `Disj` e2- b = Neg e1 `Disj` Neg e2- in nnf $ a `Conj` b+nnf1 :: Expr -> Expr+nnf1 ex = case ex of+ Neg (Neg e) -> nnf1 e+ Neg (Conj e1 e2) -> Neg e1 `Disj` Neg e2+ Neg (Disj e1 e2) -> Neg e1 `Conj` Neg e2+ Implies e1 e2 -> Neg e1 `Disj` e2+ Neg (Implies e1 e2) -> e1 `Conj` Neg e2+ Iff e1 e2 -> let a = e1 `Disj` Neg e2+ b = Neg e1 `Disj` e2+ in a `Conj` b+ Neg (Iff e1 e2) -> let a = e1 `Disj` e2+ b = Neg e1 `Disj` Neg e2+ in a `Conj` b+ e -> e -- | Conjunctive normal form. -- (May result in exponential growth)@@ -98,10 +103,96 @@ -- | Remove tautologies. simp :: Expr -> Expr-simp ex = case ex of- -- Disj e1 (Neg e2) | e1 == e2 -> True- -- Disj (Neg e1) e2 | e1 == e2 -> True- Disj e1 e2 -> Disj (simp e1) (simp e2)+simp = transformUp (propConst1 . simp1)++simp1 :: Expr -> Expr+simp1 ex = case ex of+ Disj e1 (Neg e2) | e1 == e2 -> Top+ Disj (Neg e1) e2 | e1 == e2 -> Top Conj e1 e2 | e1 == e2 -> e1- | otherwise -> Conj (simp e1) (simp e2) e -> e++-- | Test if expression is constant.+isConst :: Expr -> Bool+isConst Top = True+isConst Bottom = True+isConst e = False++-- | Transform expression up from the bottom.+transformUp :: (Expr -> Expr) -> Expr -> Expr+-- TODO: This could probably be done with Data.Data, but it's outside my capabilities for now. +transformUp f ex = case ex of+ Neg e -> f $ Neg (transformUp f e)+ Conj e1 e2 -> f $ Conj (transformUp f e1) (transformUp f e2)+ Disj e1 e2 -> f $ Disj (transformUp f e1) (transformUp f e2)+ Iff e1 e2 -> f $ Iff (transformUp f e1) (transformUp f e2)+ Implies e1 e2 -> f $ Implies (transformUp f e1) (transformUp f e2)+ e -> f e++-- | Transform expression down from the top.+transformDown :: (Expr -> Expr) -> Expr -> Expr+-- TODO: This could probably be done with Data.Data, but it's outside my capabilities for now. +transformDown f ex = case f ex of+ Neg e -> Neg (transformDown f e)+ Conj e1 e2 -> Conj (transformDown f e1) (transformDown f e2)+ Disj e1 e2 -> Disj (transformDown f e1) (transformDown f e2)+ Iff e1 e2 -> Iff (transformDown f e1) (transformDown f e2)+ Implies e1 e2 -> Implies (transformDown f e1) (transformDown f e2)+ e -> e++-- | Convert expression to list of all subexpressions.+toList :: Expr -> [Expr]+-- TODO: This could probably be done with Data.Data, but it's outside my capabilities for now.+toList ex = ex : case ex of+ Var ident -> []+ Neg e -> toList e+ Conj e1 e2 -> toList e1 ++ toList e2+ Disj e1 e2 -> toList e1 ++ toList e2+ Iff e1 e2 -> toList e1 ++ toList e2+ Implies e1 e2 -> toList e1 ++ toList e2+ Top -> []+ Bottom -> []++-- | Propagate constants (to simplify expression).+propConst :: Expr -> Expr+propConst = transformUp propConst1++propConst1 :: Expr -> Expr+propConst1 ex = case ex of+ Neg (Neg e) -> e+ Neg Top -> Bottom+ Neg Bottom -> Top+ Conj Top e2 -> e2+ Conj Bottom e2 -> Bottom+ Conj e1 Top -> e1+ Conj e1 Bottom -> Bottom+ Disj Top e2 -> Top+ Disj Bottom e2 -> e2+ Disj e1 Top -> Top+ Disj e1 Bottom -> e1+ Iff Top Bottom -> Bottom+ Iff Bottom Top -> Bottom+ Iff Bottom Bottom -> Top+ Iff Top e2 -> e2+ Iff Bottom e2 -> Neg e2+ Iff e1 Top -> e1+ Iff e1 Bottom -> Neg e1+ Implies Top e2 -> e2+ Implies Bottom e2 -> Top+ Implies e1 Top -> Top+ Implies e1 Bottom -> Neg e1+ e -> e++-- | Substitute expressions for variables. This doesn't resolve any potential variable name conflicts.+subst :: M.Map Ident Expr -> Expr -> Expr+subst vs = transformUp (propConst1 . subst1 vs)+ where+ subst1 vs ex = case ex of+ Var ident -> M.findWithDefault ex ident vs+ e -> e++-- | Partially evaluate expression.+partEval :: Ctx -> Expr -> Expr+partEval vs = subst (M.map constants vs)+ where constants True = Top+ constants False = Bottom
src/Picologic/Lexer.hs view
@@ -34,7 +34,7 @@ ] reservedNames :: [String]-reservedNames = []+reservedNames = ["1","0"] lexerStyle :: Language lexerStyle = haskellStyle
src/Picologic/Parser.hs view
@@ -32,11 +32,16 @@ x <- identifier return $ Var (Ident x) +constant :: Parser Expr+constant = (reserved "1" >> return Top)+ <|> (reserved "0" >> return Bottom)+ cexpr :: Parser Expr cexpr = Ex.buildExpressionParser operators cfactor cfactor :: Parser Expr-cfactor = var+cfactor = constant+ <|> var <|> parens cexpr parseExpr :: String -> Either ParseError Expr
src/Picologic/Pretty.hs view
@@ -5,10 +5,11 @@ ppSolutions, ) where -import Picologic.AST (Expr(..), Ident(..), Solutions(..))+import Data.List (intersperse, intercalate) import Text.PrettyPrint-import Data.List (intersperse) +import Picologic.AST (Expr(..), Ident(..), Solutions(..))+ -- | Pretty print with unicode symbols. ppExprU :: Expr -> Doc ppExprU ex = case ex of@@ -18,6 +19,8 @@ Disj a b -> con '∨' a b Implies a b -> con '→' a b Iff a b -> con '↔' a b+ Top -> char '⊤'+ Bottom -> char '⊥' where con c a b = parens $ sep [ppExprU a, char c <+> ppExprU b] @@ -30,6 +33,8 @@ Disj e1 e2 -> parens $ ppExprA e1 <+> char '|' <+> ppExprA e2 Implies e1 e2 -> parens $ ppExprA e1 <+> text "->" <+> ppExprA e2 Iff e1 e2 -> parens $ ppExprA e1 <+> text "<->" <+> ppExprA e2+ Top -> char '1'+ Bottom -> char '0' -- | Pretty print into S-Expressions ppExprLisp :: Expr -> Doc@@ -39,6 +44,8 @@ Disj a b -> con "or" $ ors [a, b] Implies a b -> con "==>" [a, b] Iff a b -> con "==" $ iffs [a, b]+ Top -> text "true"+ Bottom -> text "false" Neg (Var (Ident n)) -> text $ "-" ++ n Neg (Conj a b) -> con "nand" $ ands [a, b] Neg (Disj a b) -> con "nor" $ ors [a, b]@@ -62,12 +69,14 @@ iffs (x:xs) = x : iffs xs instance Show Expr where- show = show . ppExprLisp-+ show = show . ppExprA ppSolutions :: Solutions -> String ppSolutions (Solutions xs) =- concat (concat $ intersperse ["\n"] (fmap showExprs xs))+ concat (intercalate ["\n"] (fmap showExprs xs))++instance Show Solutions where+ show (Solutions sols) = show sols showExprs :: [Expr] -> [String] showExprs xs = intersperse " " $ fmap (render . ppExprU) xs
src/Picologic/Solver.hs view
@@ -2,7 +2,8 @@ solveProp, solveCNF, solveOneCNF,- clausesExpr+ clausesExpr,+ addVarsToSolutions ) where import Picologic.AST@@ -10,7 +11,9 @@ import Picosat import Data.List+import Data.Maybe(mapMaybe) import qualified Data.Map as M+import qualified Data.Set as S import Control.Monad.Writer -- | Yield the solutions for an expression using the PicoSAT solver.@@ -20,9 +23,14 @@ -- | Yield the solutions for an expression using the PicoSAT -- solver. The Expression must be in CNF form already. solveCNF :: Expr -> IO Solutions-solveCNF p = do- solutions <- solveAll ds- return $ Solutions $ fmap (backSubst vs') solutions+solveCNF p = if isConst p+ then+ return $ if eval M.empty p+ then Solutions [[]]+ else Solutions []+ else do+ solutions <- solveAll ds+ return $ Solutions $ mapMaybe (backSubst vs') solutions where cs = clausesFromCNF p ds = cnfToDimacs vs cs@@ -32,10 +40,15 @@ -- | Yield one single solution for an expression using the PicoSAT -- solver. The Expression must be in CNF form already.-solveOneCNF :: Expr -> IO [Expr]-solveOneCNF p = do- solution <- solve ds- return $ backSubst vs' solution+solveOneCNF :: Expr -> IO (Maybe [Expr])+solveOneCNF p = if isConst p+ then+ return $ if eval M.empty p+ then Just []+ else Nothing+ else do+ solution <- solve ds+ return $ backSubst vs' solution where cs = clausesFromCNF p ds = cnfToDimacs vs cs@@ -44,13 +57,12 @@ vars = variables p clausesFromCNF :: Expr -> [[Expr]]-clausesFromCNF p =- [ [ case lit of- v@(Var name) -> v- v@(Neg (Var name)) -> v- x -> error $ "input not in CNF: \n" ++ show p- | lit <- ors [clause] ]- | clause <- ands [p]]+clausesFromCNF p = [ [ case lit of+ v@(Var name) -> v+ v@(Neg (Var name)) -> v+ x -> error $ "input not in CNF: \n" ++ show p+ | lit <- ors [clause] ]+ | clause <- ands [p]] ands :: [Expr] -> [Expr] ands [] = []@@ -63,7 +75,7 @@ ors (x:xs) = x : ors xs cnfToDimacs :: M.Map Ident Int -> [[Expr]] -> [[Int]]-cnfToDimacs vs cs = map (map encode) cs+cnfToDimacs vs = map (map encode) where encode (Var ident) = vs M.! ident encode (Neg (Var ident)) = negate $ vs M.! ident @@ -77,11 +89,16 @@ vars = variables p ds = cnfToDimacs vs cs -backSubst :: M.Map Int Ident -> Solution -> [Expr]-backSubst env (Solution xs) = fmap go xs+backSubst :: M.Map Int Ident -> Solution -> Maybe [Expr]+backSubst env (Solution xs) = Just $ fmap go xs where go x | x >= 0 = Var (env M.! x)- go x | x < 0 = Neg (Var (env M.! (abs x)))-backSubst _ Unsatisfiable = []-backSubst _ Unknown = []+ go x | x < 0 = Neg (Var (env M.! abs x))+backSubst _ Unsatisfiable = Nothing+backSubst _ Unknown = Nothing +addVarsToSolutions :: [Ident] -> Solutions -> Solutions+addVarsToSolutions vars (Solutions sols) = Solutions $ concatMap addVarsToSolution sols+ where+ addVarsToSolution sol = map (sol ++) $ sequence [ [Var v, Neg(Var v)] | v <- newVars $ head sols ]+ newVars sol = vars \\ concatMap variables sol
src/Picologic/Tseitin.hs view
@@ -33,12 +33,12 @@ put $ succ n return $ Var $ Ident $ "ts*" ++ show n -or xs = foldl1 Disj xs-and xs = foldl1 Conj xs+or = foldl1 Disj+and = foldl1 Conj tseitinCNF :: Expr -> Expr tseitinCNF e =- let (var, clauses) = evalTS $ tseitin $ simplify e+ let (var, clauses) = evalTS $ tseitin $ propConst e in and (var : clauses) neg (Neg x) = x@@ -156,6 +156,10 @@ or [a, c]] return c +tseitin Top = return Top++tseitin Bottom = return Bottom+ dropTseitinVarsInSolutions (Solutions xs) = Solutions $ map dropTseitinVars xs @@ -171,12 +175,3 @@ tseitinName ('t':'s':'*':_) = True tseitinName _ = False -simplify :: Expr -> Expr-simplify (Neg (Neg x)) = simplify x-simplify v@(Var _) = v-simplify (Neg a) = neg $ simplify a-simplify (Conj a b) = Conj (simplify a) (simplify b)-simplify (Disj a b) = Disj (simplify a) (simplify b)-simplify (Implies a b) = Implies (simplify a) (simplify b)-simplify (Iff a b) = Iff (simplify a) (simplify b)-
tests/tests.hs view
@@ -4,15 +4,15 @@ import Picologic.Pretty import Test.QuickCheck+import Data.List import qualified Data.Map as M-import qualified Data.Set as S import System.Exit (exitFailure) import System.IO.Unsafe (unsafePerformIO) instance Arbitrary Expr where arbitrary = sized $ \n -> tree (round $ sqrt $ fromIntegral n :: Int)- where tree 0 = elements $ map (Var . Ident) ["a", "b", "c", "d"]+ where tree 0 = elements $ map (Var . Ident) (concat $ replicate 3 ["a", "b", "c", "d"]) ++ [Top, Bottom] tree n = oneof [do a <- tree (pred n)@@ -38,12 +38,15 @@ shrink (Iff a b) = [a, b] ++ map (Iff a) (shrink b) ++ map (\aa-> Iff aa b) (shrink a)+ shrink Top = []+ shrink Bottom = [] -env = M.fromList [(Ident "a", True),- (Ident "b", True),- (Ident "c", False),- (Ident "d", False)]+envl = [(Ident "a", True),+ (Ident "b", True),+ (Ident "c", False),+ (Ident "d", False)]+env = M.fromList envl test_nnf :: Expr -> Bool test_nnf e = eval env e == eval env (nnf e)@@ -54,6 +57,7 @@ test_tseitin :: Expr -> Bool test_tseitin e = unsafePerformIO test where test = do+ let vars = variables e let ts = tseitinCNF e -- putStrLn "\nexpr" -- print $ ppExprLisp e@@ -61,17 +65,28 @@ -- print $ ppExprLisp ts -- putStrLn "tseitin clauses" -- mapM_ print $ clausesExpr ts- as <- solveCNF $ cnf e+ let ce = cnf e+ as <- solveCNF ce bs0 <- solveCNF ts let bs = dropTseitinVarsInSolutions bs0- case (as, bs) of- (Solutions av, Solutions bv) -> do- --print ("as", av)- --print ("bs", bv)- return $ S.fromList av == S.fromList bv+ let as1 = addVarsToSolutions vars as+ let bs1 = addVarsToSolutions vars bs+ --print ("as", as)+ --print ("bs", bs)+ return $ normalize as1 == normalize bs1+ normalize (Solutions ssv) = sort $ map sort ssv -qc = verboseCheckWith (stdArgs { maxSuccess = 1000 })+test_partEval :: Expr -> Bool+test_partEval e = if eval env e+ then elast == Top+ else elast == Bottom+ where+ envs = map (\(i,v) -> M.singleton i v) envl+ elast = last $ scanl (flip partEval) e envs ++qc = verboseCheckWith (stdArgs { maxSuccess = 2000 })+ -- how to make an error fail a 'cabal test'? qcwf p = verboseCheckWith (stdArgs { maxSuccess = 1000 }) (whenFail exitFailure p)@@ -83,3 +98,5 @@ qc test_cnf putStrLn "tseitin" qc test_tseitin+ putStrLn "partEval"+ qc test_partEval