picologic 0.1 → 0.1.1

raw patch · 3 files changed

+10/−11 lines, 3 filesdep ~base

Dependency ranges changed: base

Files

picologic.cabal +3/−3
src/Picologic/AST.hs +0/−1
src/Picologic/Solver.hs +7/−7

picologic.cabal view

@@ -1,5 +1,5 @@ name:                picologic-version:             0.1+version:             0.1.1 synopsis:            Utilities for symbolic predicate logic expressions homepage:            https://github.com/sdiehl/picologic license:             MIT@@ -32,7 +32,7 @@   hs-source-dirs:      src   other-extensions:    DeriveDataTypeable, BangPatterns   build-depends:       -    base        >= 4.6 && <4.7,+    base        >= 4.6 && <4.8,     picosat     >= 0.1 && <0.2,     containers  >= 0.5 && <0.6,     mtl         >= 2.1 && <2.2,@@ -47,7 +47,7 @@     other-modules: Picologic.Repl     other-extensions:    DeriveDataTypeable, BangPatterns     build-depends:       -      base        >= 4.6 && <4.7,+      base        >= 4.6 && <4.8,       picosat     >= 0.1 && <0.2,       containers  >= 0.5 && <0.6,       mtl         >= 2.1 && <2.2,

src/Picologic/AST.hs view

@@ -20,7 +20,6 @@ import Data.Maybe import qualified Data.Map as M - newtype Ident = Ident String   deriving (Eq, Ord, Show, Data, Typeable)

src/Picologic/Solver.hs view

@@ -7,7 +7,7 @@ import Picosat  import Data.List-import Data.Map as M+import qualified Data.Map as M import Control.Monad.Writer  data Clause@@ -22,19 +22,19 @@ solveProp :: Expr -> IO Solutions solveProp p = solveAll cs >>= return . Solutions . fmap (backSubst vs')   where-    cs = fmap toInts $ execWriter $ clauses vs (cnf p)+    cs = filter (not . null) $ fmap toInts $ execWriter $ clauses vs (cnf p)     vs  = M.fromList $ zip vars [1..]     vs' = M.fromList $ zip [1..] vars     vars = variables (cnf p)  -- | Yield the integer clauses given to the SAT solver. clausesExpr :: Expr -> [[Int]]-clausesExpr p = fmap toInts $ execWriter $ clauses vs (cnf p)+clausesExpr p = filter (not . null) $ fmap toInts $ execWriter $ clauses vs (cnf p)   where     vs = M.fromList $ zip vars [1..]     vars = variables (cnf p) -backSubst :: Map Int Ident -> Solution -> [Expr]+backSubst :: M.Map Int Ident -> Solution -> [Expr] backSubst env (Solution xs) = fmap go xs   where     go x | x >= 0 = Var (env M.! x)@@ -44,6 +44,7 @@  toInts :: Clause -> [Int] toInts (CL xs) = fmap (\(CV n) -> n) xs+toInts (CV x) = [x]  neg :: Clause -> Clause neg (CV n) = CV (-n)@@ -64,10 +65,9 @@   Conj e1 e2 -> do     cs1 <- clauses env e1     cs2 <- clauses env e2-    tell [combine cs1 cs2]-    return (combine cs1 cs2)+    tell [cs1, cs2]+    return (CL [])   Disj e1 e2 -> do     cs1 <- clauses env e1     cs2 <- clauses env e2-    tell [combine cs1 cs2]     return (combine cs1 cs2)