packages feed

picologic 0.1.1 → 0.1.2

raw patch · 8 files changed

+534/−61 lines, 8 filesdep +QuickCheckdep +picologicdep ~basedep ~containersdep ~mtl

Dependencies added: QuickCheck, picologic

Dependency ranges changed: base, containers, mtl, parsec, picosat, pretty

Files

picologic.cabal view
@@ -1,5 +1,5 @@ name:                picologic-version:             0.1.1+version:             0.1.2 synopsis:            Utilities for symbolic predicate logic expressions homepage:            https://github.com/sdiehl/picologic license:             MIT@@ -28,16 +28,20 @@     Picologic,     Picologic.Solver,     Picologic.AST,-    Picologic.Parser+    Picologic.Parser,+    Picologic.Pretty,+    Picologic.Tseitin+  other-modules:+    Picologic.Lexer   hs-source-dirs:      src   other-extensions:    DeriveDataTypeable, BangPatterns   build-depends:       -    base        >= 4.6 && <4.8,-    picosat     >= 0.1 && <0.2,-    containers  >= 0.5 && <0.6,-    mtl         >= 2.1 && <2.2,-    pretty      >= 1.1 && <1.2,-    parsec      >= 3.1 && <3.2+    base >= 2   && <5,+    picosat,+    containers,+    mtl,+    pretty,+    parsec   default-language:    Haskell2010  executable picologic@@ -47,7 +51,7 @@     other-modules: Picologic.Repl     other-extensions:    DeriveDataTypeable, BangPatterns     build-depends:       -      base        >= 4.6 && <4.8,+      base        >= 2   && <5,       picosat     >= 0.1 && <0.2,       containers  >= 0.5 && <0.6,       mtl         >= 2.1 && <2.2,@@ -58,3 +62,25 @@     default-language:    Haskell2010   else     buildable: False++--Todo: how to fail 'cabal test' on a QuickCheck error?+Test-Suite picologic-quickcheck+   type:       exitcode-stdio-1.0+   main-is:    tests.hs+   hs-source-dirs: tests+   build-depends: +      base >= 2 && <5,+      QuickCheck,+      containers,+      picosat,+      mtl,+      pretty,+      picologic++Test-Suite pretty-print-test+   type:       exitcode-stdio-1.0+   main-is:    PrettyPrintTest.hs+   hs-source-dirs: tests+   build-depends: +      base >= 2 && <5,+      picologic
src/Picologic/AST.hs view
@@ -34,7 +34,7 @@   | Disj      Expr Expr  -- ^ Logical disjunction   | Iff       Expr Expr  -- ^ Logical biconditional   | Implies   Expr Expr  -- ^ Material implication-  deriving (Eq, Ord, Show, Data, Typeable)+  deriving (Eq, Ord, Data, Typeable)  -- | Evaluate expression. eval :: Ctx -> Expr -> Bool@@ -57,14 +57,15 @@     go (Implies e1 e2) !vs = go e1 vs ++ go e2 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)           -> e+  Neg (Neg e)           -> nnf e    Conj e1 e2            -> nnf e1 `Conj` nnf e2-  Neg (Conj e1 e2)      -> nnf $ Neg e1 `Conj` Neg 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@@ -72,15 +73,16 @@   Implies e1 e2         -> nnf $ Neg e1 `Disj` e2   Neg (Implies e1 e2)   -> nnf $ e1 `Conj` Neg e2 -  Iff e1 e2             -> let a = e1 `Conj` e2-                               b = Neg e1 `Conj` Neg e2-                               in nnf $ a `Disj` b+  Iff e1 e2             -> let a = e1 `Disj` Neg e2+                               b = Neg e1 `Disj` e2+                               in nnf $ a `Conj` b    Neg (Iff e1 e2)       -> let a = e1 `Disj` e2                                b = Neg e1 `Disj` Neg e2                                in nnf $ a `Conj` b  -- | Conjunctive normal form.+-- (May result in exponential growth) cnf :: Expr -> Expr cnf = simp . cnf' . nnf   where@@ -97,8 +99,8 @@ -- | Remove tautologies. simp :: Expr -> Expr simp ex = case ex of-  Disj e1 (Neg e2) | e1 == e2 -> e1-  Disj (Neg e1) e2 | e1 == e2 -> e1+  -- Disj e1 (Neg e2) | e1 == e2 -> True+  -- Disj (Neg e1) e2 | e1 == e2 -> True   Disj e1 e2 -> Disj (simp e1) (simp e2)   Conj e1 e2       | e1 == e2 -> e1                    | otherwise -> Conj (simp e1) (simp e2)
+ src/Picologic/Lexer.hs view
@@ -0,0 +1,74 @@+module Picologic.Lexer (+  Parser,+  Op,+  contents,+  parens,+  reservedOp,+  reserved,+  identifier,+) where++import Control.Monad.Identity++import Text.Parsec+import Text.Parsec.Language (haskellStyle)+import qualified Text.Parsec.Token as Tok+import qualified Text.Parsec.Expr as Ex++type Parser   = ParsecT String () Identity+type Lexer    = Tok.GenTokenParser String () Identity+type Language = Tok.GenLanguageDef String () Identity+type Op       = Ex.Operator String () Identity++-------------------------------------------------------------------------------+-- Lexer+-------------------------------------------------------------------------------++reservedOps :: [String]+reservedOps = [+    "->",+    "&",+    "|",+    "<->",+    "~"+  ]++reservedNames :: [String]+reservedNames = []++lexerStyle :: Language+lexerStyle = haskellStyle+  { Tok.commentStart    = "{-"+  , Tok.commentEnd      = "-}"+  , Tok.commentLine     = "--"+  , Tok.nestedComments  = True+  , Tok.identStart      = letter+  , Tok.identLetter     = alphaNum+  , Tok.opStart         = Tok.opLetter lexerStyle+  , Tok.opLetter        = oneOf "`~!@$%^&*-+=;:<>./?#"+  , Tok.reservedOpNames = reservedOps+  , Tok.reservedNames   = reservedNames+  , Tok.caseSensitive   = True+  }++lexer :: Lexer+lexer = Tok.makeTokenParser lexerStyle++reservedOp :: String -> Parser ()+reservedOp = Tok.reservedOp lexer++reserved :: String -> Parser ()+reserved = Tok.reserved lexer++identifier :: Parser String+identifier = Tok.identifier lexer++parens :: Parser a -> Parser a+parens = Tok.parens lexer++contents :: Parser a -> Parser a+contents p = do+  Tok.whiteSpace lexer+  r <- p+  eof+  return r
+ src/Picologic/Pretty.hs view
@@ -0,0 +1,73 @@+module Picologic.Pretty (+  ppExprU,+  ppExprA,+  ppExprLisp,+  ppSolutions,+) where++import Picologic.AST (Expr(..), Ident(..), Solutions(..))+import Text.PrettyPrint+import Data.List (intersperse)++-- | Pretty print with unicode symbols.+ppExprU :: Expr -> Doc+ppExprU ex = case ex of+  Var (Ident n) -> text n+  Neg expr      -> char '¬' <> ppExprU expr+  Conj a b      -> con '∧' a b+  Disj a b      -> con '∨' a b+  Implies a b   -> con '→' a b+  Iff a b       -> con '↔' a b+  where con c a b =+          parens $ sep [ppExprU a, char c <+> ppExprU b]++-- | Pretty print with ascii symbols.+ppExprA :: Expr -> Doc+ppExprA ex = case ex of+  Var (Ident n)  ->  text n+  Neg expr       ->  char '~' <> ppExprA expr+  Conj e1 e2     ->  parens $ ppExprA e1 <+> char '&' <+> ppExprA e2+  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++-- | Pretty print into S-Expressions+ppExprLisp :: Expr -> Doc+ppExprLisp ex = case ex of+  Var (Ident n)       -> text n+  Conj a b            -> con "and" $ ands [a, b]+  Disj a b            -> con "or" $ ors [a, b]+  Implies a b         -> con "==>" [a, b]+  Iff a b             -> con "==" $ iffs [a, b]+  Neg (Var (Ident n)) -> text $ "-" ++ n+  Neg (Conj a b)      -> con "nand" $ ands [a, b]+  Neg (Disj a b)      -> con "nor" $ ors [a, b]+  Neg (Iff a b)       -> con "xor" $ iffs [a, b]+  Neg expr            -> parens $ text "not" <+> ppExprLisp expr+  where con c xs =+          parens $+          sep [text c,+               nest 1 $ sep $ map ppExprLisp xs]++ands [] = []+ands (Conj a b : xs) = ands [a] ++ ands [b] ++ ands xs+ands (x:xs) = x : ands xs++ors [] = []+ors (Disj a b : xs) = ors [a] ++ ors [b] ++ ors xs+ors (x:xs) = x : ors xs++iffs [] = []+iffs (Iff a b : xs) = iffs [a] ++ iffs [b] ++ iffs xs+iffs (x:xs) = x : iffs xs++instance Show Expr where+  show = show . ppExprLisp+++ppSolutions :: Solutions -> String+ppSolutions (Solutions xs) =+  concat (concat $ intersperse ["\n"] (fmap showExprs xs))++showExprs :: [Expr] -> [String]+showExprs xs = intersperse " " $ fmap (render . ppExprU) xs
src/Picologic/Solver.hs view
@@ -1,38 +1,81 @@ module Picologic.Solver (   solveProp,-  clausesExpr,+  solveCNF,+  solveOneCNF,+  clausesExpr ) where  import Picologic.AST+import Picologic.Pretty import Picosat  import Data.List import qualified Data.Map as M import Control.Monad.Writer -data Clause-  = CV Int       -- ^Clause variable ( a or -a )-  | CL [Clause]  -- ^Set of clause under disjuntion+-- | Yield the solutions for an expression using the PicoSAT solver.+solveProp :: Expr -> IO Solutions+solveProp p = solveCNF $ cnf p -instance Show Clause where-  show (CV i) = show i-  show (CL xs) = concat (intersperse " " (fmap show xs))+-- | 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+  where+    cs = clausesFromCNF p+    ds = cnfToDimacs vs cs+    vs  = M.fromList $ zip vars [1..]+    vs' = M.fromList $ zip [1..] vars+    vars = variables p --- | Yield the soutions for an expressions using the PicosSAT solver.-solveProp :: Expr -> IO Solutions-solveProp p = solveAll cs >>= return . Solutions . fmap (backSubst vs')+-- | 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   where-    cs = filter (not . null) $ fmap toInts $ execWriter $ clauses vs (cnf p)+    cs = clausesFromCNF p+    ds = cnfToDimacs vs cs     vs  = M.fromList $ zip vars [1..]     vs' = M.fromList $ zip [1..] vars-    vars = variables (cnf p)+    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]]++ands :: [Expr] -> [Expr]+ands [] = []+ands (Conj a b : xs) = ands [a] ++ ands [b] ++ ands xs+ands (x:xs) = x : ands xs++ors :: [Expr] -> [Expr]+ors [] = []+ors (Disj a b : xs) = ors [a] ++ ors [b] ++ ors xs+ors (x:xs) = x : ors xs++cnfToDimacs :: M.Map Ident Int -> [[Expr]] -> [[Int]]+cnfToDimacs vs cs = map (map encode) cs+  where encode (Var ident)       = vs M.! ident+        encode (Neg (Var ident)) = negate $ vs M.! ident+  + -- | Yield the integer clauses given to the SAT solver. clausesExpr :: Expr -> [[Int]]-clausesExpr p = filter (not . null) $ fmap toInts $ execWriter $ clauses vs (cnf p)+clausesExpr p = ds   where-    vs = M.fromList $ zip vars [1..]-    vars = variables (cnf p)+    cs = clausesFromCNF p+    vs  = M.fromList $ zip vars [1..]+    vars = variables p+    ds = cnfToDimacs vs cs  backSubst :: M.Map Int Ident -> Solution -> [Expr] backSubst env (Solution xs) = fmap go xs@@ -42,32 +85,3 @@ backSubst _ Unsatisfiable = [] backSubst _ Unknown = [] -toInts :: Clause -> [Int]-toInts (CL xs) = fmap (\(CV n) -> n) xs-toInts (CV x) = [x]--neg :: Clause -> Clause-neg (CV n) = CV (-n)-neg (CL xs) = CL (fmap neg xs)--combine :: Clause -> Clause -> Clause-combine (CL x) (CL y) = CL (x++y)-combine (CL x) y = combine (CL x) (CL [y])-combine x (CL y) = combine (CL [x]) (CL y)-combine x y = CL [x, y]--clauses :: M.Map Ident Int -> Expr -> Writer [Clause] Clause-clauses env ex = case ex of-  Var v -> return $ CV (env M.! v)-  Neg x -> do-    cs <- clauses env x-    return (neg cs)-  Conj e1 e2 -> do-    cs1 <- clauses env e1-    cs2 <- clauses env e2-    tell [cs1, cs2]-    return (CL [])-  Disj e1 e2 -> do-    cs1 <- clauses env e1-    cs2 <- clauses env e2-    return (combine cs1 cs2)
+ src/Picologic/Tseitin.hs view
@@ -0,0 +1,182 @@+module Picologic.Tseitin+       (tseitinCNF,+        dropTseitinVarsInSolutions,+        dropTseitinVars,+        +       ) where++-- TODO: How efficient is the `mappend` used by Writer?+-- TODO: For cases like (Conj (Conj a b) c) the introduction+--       of one Tseitin var can be enough.+-- TODO: The outermost (Conj (Conj ...) ...) needn't be+--       Tseitin encoded at all.+--       Also, the (Disj (Disj ...) ...) below, needn't be encoded+--       when they use only variables or negated variables.+--       Tseitin transformation can be used specifically there to+--       turn other expressions into variables.++import Prelude hiding (or, and)++import Picologic.AST+import Control.Monad.State.Strict+import Control.Monad.Writer.Strict++type TS a = StateT Int (Writer [Expr]) a++evalTS :: TS a -> (a, [Expr])+evalTS action = +  runWriter (evalStateT action 1)++var :: TS Expr+var = do+  n <- get+  put $ succ n+  return $ Var $ Ident $ "ts*" ++ show n++or xs = foldl1 Disj xs+and xs = foldl1 Conj xs++tseitinCNF :: Expr -> Expr+tseitinCNF e =+  let (var, clauses) = evalTS $ tseitin $ simplify e+  in and (var : clauses)++neg (Neg x) = x+neg x       = Neg x++tseitin :: Expr -> TS Expr++tseitin lit@(Var _) = return lit++tseitin lit@(Neg (Var _)) = return lit++tseitin (Conj x y) = do+  a <- tseitin x+  b <- tseitin y+  c <- var+  tell [or [neg a, neg b, c],+        or [a, neg c],+        or [b, neg c]]+  return c++tseitin (Neg (Conj x y)) = do+  a <- tseitin x+  b <- tseitin y+  c <- var+  tell [or [neg a, neg b, neg c],+        or [a, c],+        or [b, c]]+  return c++tseitin (Disj x y) = do+  a <- tseitin x+  b <- tseitin y+  c <- var+  tell [or [a, b, neg c],+        or [neg a, c],+        or [neg b, c]]+  return c++tseitin (Neg (Disj x y)) = do+  a <- tseitin x+  b <- tseitin y+  c <- var+  tell [or [a, b, c],+        or [neg a, neg c],+        or [neg b, neg c]]+  return c+++-- |+-- @+-- (c -> (a -> b)) & (-c -> -(a->b))+-- (-c | (-a | b)) & (c | (a&-b))+-- (-a|b|-c) & (a|c) & (-b|c)+-- @+tseitin (Implies x y) = do+  a <- tseitin x+  b <- tseitin y+  c <- var+  tell [or [neg a, b, neg c],+        or [a, c],+        or [neg b, c]]+  return c++-- |+-- @+-- (c -> -(a -> b)) & (-c -> (a->b))+-- (-c | (a&-b)) & (c | (-a|b))+-- (a|-c) & (-b|-c) & (-a|b|c)+-- @+tseitin (Neg (Implies x y)) = do+  a <- tseitin x+  b <- tseitin y+  c <- var+  tell [or [a, neg c],+        or [neg b, neg c],+        or [neg a, b, c]]+  return c++-- |+-- @+-- (c -> a == b) & (-c -> a /= b)+-- (-c | ((-a|b) & (a|-b))) & (c | ((a|b) & (-a|-b)))+-- (-a|b|-c) & (a|-b|-c) & (a|b|c) & (-a|-b|c)+-- @+tseitin (Iff x y) = do+  a <- tseitin x+  b <- tseitin y+  c <- var+  tell [or [neg a, b, neg c],+        or [a, neg b, neg c],+        or [a, b, c],+        or [neg a, neg b, c]]+  return c++-- |+-- @+-- (c -> a /= b) & (-c -> a == b)+-- (-c | ((a|b) & (-a|-b))) & (c | ((-a|b) & (a|-b)))+-- (a|b|-c) & (-a|-b|-c) & (-a|b|c) & (a|-b|c)+-- @+tseitin (Neg (Iff x y)) = do+  a <- tseitin x+  b <- tseitin y+  c <- var+  tell [or [a, b, neg c],+        or [neg a, neg b, neg c],+        or [neg a, b, c],+        or [a, neg b, c]]+  return c++tseitin (Neg x) = do+  a <- tseitin x+  c <- var+  tell [or [neg a, neg c],+        or [a, c]]+  return c++dropTseitinVarsInSolutions (Solutions xs) =+  Solutions $ map dropTseitinVars xs++dropTseitinVars :: [Expr] -> [Expr]+dropTseitinVars = filter (\x -> not $ isTseitinLiteral x)++isTseitinLiteral :: Expr -> Bool+isTseitinLiteral lit =+  case lit of+    (Var (Ident nm)) -> tseitinName nm+    (Neg (Var (Ident nm))) -> tseitinName nm++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/PrettyPrintTest.hs view
@@ -0,0 +1,17 @@+import Picologic++main = print $ ppExprLisp d+  where a =+          Disj (Var (Ident "some-var"))+               (Disj (Var (Ident "another-var"))+                     (Iff (Var (Ident "ggg"))+                          (Neg (Iff (Neg (Var (Ident "var-x")))+                                    (Var (Ident "origin"))))))+        b = +          Conj (Var (Ident "var-y"))+               (Conj (Var (Ident "ccc"))+                     (Iff (Var (Ident "ddddd"))+                          (Neg (Iff (Neg (Var (Ident "abcdefg")))+                                    (Var (Ident "ggg"))))))+        c = Disj a b+        d = Conj c c
+ tests/tests.hs view
@@ -0,0 +1,85 @@+import Picologic.AST+import Picologic.Tseitin+import Picologic.Solver+import Picologic.Pretty++import Test.QuickCheck+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"]+          tree n =+            oneof+            [do a <- tree (pred n)+                return $ Neg a,+             do l <- arbitrary+                let n2 = l `mod` n+                a <- tree n2+                b <- tree (n-n2)+                con <- elements [Conj, Disj, Implies, Iff]+                return $ con a b]+  shrink (Var _) = []+  shrink (Neg (Neg x)) = [x, Neg x] ++ map Neg (shrink x)+  shrink (Neg x) = [x] ++ map Neg (shrink x)+  shrink (Conj a b) = [a, b]+                     ++ map (Conj a) (shrink b)+                     ++ map (\aa-> Conj aa b) (shrink a)+  shrink (Disj a b) = [a, b]+                     ++ map (Disj a) (shrink b)+                     ++ map (\aa-> Disj aa b) (shrink a)+  shrink (Implies a b) = [a, b]+                     ++ map (Implies a) (shrink b)+                     ++ map (\aa-> Implies aa b) (shrink a)+  shrink (Iff a b) = [a, b]+                     ++ map (Iff a) (shrink b)+                     ++ map (\aa-> Iff aa b) (shrink a)+++env = M.fromList [(Ident "a", True),+                  (Ident "b", True),+                  (Ident "c", False),+                  (Ident "d", False)]++test_nnf :: Expr -> Bool+test_nnf e = eval env e == eval env (nnf e)++test_cnf :: Expr -> Bool+test_cnf e = eval env e == eval env (cnf e)++test_tseitin :: Expr -> Bool+test_tseitin e = unsafePerformIO test+  where test = do+          let ts = tseitinCNF e+          -- putStrLn "\nexpr"+          -- print $ ppExprLisp e+          -- putStrLn "tseitin"+          -- print $ ppExprLisp ts+          -- putStrLn "tseitin clauses"+          -- mapM_ print $ clausesExpr ts+          as <- solveCNF $ cnf e+          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++qc = verboseCheckWith (stdArgs { maxSuccess = 1000 })++-- how to make an error fail a 'cabal test'?+qcwf p = verboseCheckWith (stdArgs { maxSuccess = 1000 })+         (whenFail exitFailure p)++main = do+  putStrLn "nnf"+  qc test_nnf+  putStrLn "cnf"+  qc test_cnf+  putStrLn "tseitin"+  qc test_tseitin