packages feed

logic-classes 1.4.6 → 1.4.7

raw patch · 11 files changed

+385/−39 lines, 11 filesdep −incremental-sat-solver

Dependencies removed: incremental-sat-solver

Files

+ Data/Boolean.hs view
@@ -0,0 +1,157 @@+{-# OPTIONS -fno-warn-incomplete-patterns #-}+-- |+-- Module      : Data.Boolean+-- Copyright   : Sebastian Fischer+-- License     : BSD3+-- +-- Maintainer  : Sebastian Fischer (sebf@informatik.uni-kiel.de)+-- Stability   : experimental+-- Portability : portable+-- +-- This library provides a representation of boolean formulas that is+-- used by the solver in "Data.Boolean.SatSolver".+-- +-- We also define a function to simplify formulas, a type for+-- conjunctive normalforms, and a function that creates them from+-- boolean formulas.+-- +module Data.Boolean ( ++  Boolean(..), ++  Literal(..), literalVar, invLiteral, isPositiveLiteral, ++  CNF, Clause, booleanToCNF++  ) where++import Data.Maybe ( mapMaybe )+import qualified Data.IntMap as IM++import Control.Monad ( guard, liftM )++-- | Boolean formulas are represented as values of type @Boolean@.+-- +data Boolean+  -- | Variables are labeled with an @Int@,+  = Var Int+  -- | @Yes@ represents /true/,+  | Yes+  -- | @No@ represents /false/,+  | No+  -- | @Not@ constructs negated formulas,+  | Not Boolean+  -- | and finally we provide conjunction+  | Boolean :&&: Boolean+  -- | and disjunction of boolean formulas.+  | Boolean :||: Boolean+ deriving Show++-- | Literals are variables that occur either positively or negatively.+-- +data Literal = Pos Int | Neg Int deriving (Eq, Show)++-- | This function returns the name of the variable in a literal.+-- +literalVar :: Literal -> Int+literalVar (Pos n) = n+literalVar (Neg n) = n++-- | This function negates a literal.+-- +invLiteral :: Literal -> Literal+invLiteral (Pos n) = Neg n+invLiteral (Neg n) = Pos n++-- | This predicate checks whether the given literal is positive.+-- +isPositiveLiteral :: Literal -> Bool+isPositiveLiteral (Pos _) = True+isPositiveLiteral _       = False++-- | Conjunctive normalforms are lists of lists of literals.+-- +type CNF     = [Clause]+type Clause  = [Literal]++-- | +-- We convert boolean formulas to conjunctive normal form by pushing+-- negations down to variables and repeatedly applying the+-- distributive laws.+-- +booleanToCNF :: Boolean -> CNF+booleanToCNF+  = mapMaybe (simpleClause . map literal . disjunction)+  . conjunction+  . asLongAsPossible distribute+  . asLongAsPossible pushNots+  . asLongAsPossible elim+ where+  elim (Not Yes)      = Just No+  elim (Not No)       = Just Yes+  elim (No  :&&: _)   = Just No+  elim (Yes :&&: x)   = Just x+  elim (_   :&&: No)  = Just No+  elim (x   :&&: Yes) = Just x +  elim (Yes :||: _)   = Just Yes+  elim (No  :||: x)   = Just x+  elim (_   :||: Yes) = Just Yes+  elim (x   :||: No)  = Just x+  elim _              = Nothing++  pushNots (Not (Not x))  = Just x+  pushNots (Not (x:&&:y)) = Just (Not x :||: Not y)+  pushNots (Not (x:||:y)) = Just (Not x :&&: Not y)+  pushNots _              = Nothing++  distribute (x:||:(y:&&:z)) = Just ((x:||:y):&&:(x:||:z))+  distribute ((x:&&:y):||:z) = Just ((x:||:z):&&:(y:||:z))+  distribute _               = Nothing++  literal (Var x)       = Pos x+  literal (Not (Var x)) = Neg x+++-- private helper functions++-- remove duplicate literals from clauses and drop clauses that+-- contain one literal both positively and negatively.+--+simpleClause :: Clause -> Maybe Clause+simpleClause = liftM (map lit . IM.toList) . foldl add (Just IM.empty)+ where+  lit (x,True)  = Pos x+  lit (x,False) = Neg x++  add mm l = do+    m <- mm+    let x = literalVar l; kind = isPositiveLiteral l+    maybe (Just (IM.insert x kind m))+          (\b -> guard (b==kind) >> Just m)+          (IM.lookup x m)++conjunction :: Boolean -> [Boolean]+conjunction b = flat b []+ where flat Yes      = id+       flat (x:&&:y) = flat x . flat y+       flat x        = (x:)++disjunction :: Boolean -> [Boolean]+disjunction b = flat b []+ where flat No       = id+       flat (x:||:y) = flat x . flat y+       flat x        = (x:)++asLongAsPossible :: (Boolean -> Maybe Boolean) -> Boolean -> Boolean+asLongAsPossible f = everywhere g+ where g x = maybe x (everywhere g) (f x)++everywhere :: (Boolean -> Boolean) -> Boolean -> Boolean+everywhere f = f . atChildren (everywhere f)++atChildren :: (Boolean -> Boolean) -> Boolean -> Boolean+atChildren f (Not x)  = Not (f x)+atChildren f (x:&&:y) = f x :&&: f y+atChildren f (x:||:y) = f x :||: f y+atChildren _ x        = x+
+ Data/Boolean/SatSolver.hs view
@@ -0,0 +1,183 @@+-- |+-- Module      : Data.Boolean.SatSolver+-- Copyright   : Sebastian Fischer+-- License     : BSD3+-- +-- Maintainer  : Sebastian Fischer (sebf@informatik.uni-kiel.de)+-- Stability   : experimental+-- Portability : portable+-- +-- This Haskell library provides an implementation of the+-- Davis-Putnam-Logemann-Loveland algorithm+-- (cf. <http://en.wikipedia.org/wiki/DPLL_algorithm>) for the boolean+-- satisfiability problem. It not only allows to solve boolean+-- formulas in one go but also to add constraints and query bindings+-- of variables incrementally.+-- +-- The implementation is not sophisticated at all but uses the basic+-- DPLL algorithm with unit propagation.+-- +module Data.Boolean.SatSolver (++  Boolean(..), SatSolver, Literal(..), literalVar, invLiteral, isPositiveLiteral, CNF, Clause, booleanToCNF,++  newSatSolver, isSolved, ++  lookupVar, assertTrue, assertTrue', branchOnVar, selectBranchVar, solve, isSolvable++  ) where++import Data.List+import Data.Boolean++import Control.Monad.Writer++import qualified Data.IntMap as IM++-- | A @SatSolver@ can be used to solve boolean formulas.+-- +data SatSolver = SatSolver { clauses :: CNF, bindings :: IM.IntMap Bool }+ deriving Show++-- | A new SAT solver without stored constraints.+-- +newSatSolver :: SatSolver+newSatSolver = SatSolver [] IM.empty++-- | This predicate tells whether all constraints are solved.+-- +isSolved :: SatSolver -> Bool+isSolved = null . clauses++-- |+-- We can lookup the binding of a variable according to the currently+-- stored constraints. If the variable is unbound, the result is+-- @Nothing@.+-- +lookupVar :: Int -> SatSolver -> Maybe Bool+lookupVar name = IM.lookup name . bindings++-- | +-- We can assert boolean formulas to update a @SatSolver@. The+-- assertion may fail if the resulting constraints are unsatisfiable.+-- +assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver+assertTrue formula solver = do+  newClauses <- foldl (addClause (bindings solver))+                      (return (clauses solver))+                      (booleanToCNF formula)+  simplify (solver { clauses = newClauses })++assertTrue' :: MonadPlus m => CNF -> SatSolver -> m SatSolver+assertTrue' formula solver = do+  newClauses <- foldl (addClause (bindings solver))+                      (return (clauses solver))+                      formula+  simplify (solver { clauses = newClauses })++-- |+-- This function guesses a value for the given variable, if it is+-- currently unbound. As this is a non-deterministic operation, the+-- resulting solvers are returned in an instance of @MonadPlus@.+-- +branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolver+branchOnVar name solver =+  maybe (branchOnUnbound name solver)+        (const (return solver))+        (lookupVar name solver)++-- |+-- We select a variable from the shortest clause hoping to produce a+-- unit clause.+--+selectBranchVar :: SatSolver -> Int+selectBranchVar = literalVar . head . head . sortBy shorter . clauses++-- | +-- This function guesses values for variables such that the stored+-- constraints are satisfied. The result may be non-deterministic and+-- is, hence, returned in an instance of @MonadPlus@.+-- +solve :: MonadPlus m => SatSolver -> m SatSolver+solve solver+  | isSolved solver = return solver+  | otherwise = branchOnUnbound (selectBranchVar solver) solver >>= solve++-- |+-- This predicate tells whether the stored constraints are+-- solvable. Use with care! This might be an inefficient operation. It+-- tries to find a solution using backtracking and returns @True@ if+-- and only if that fails.+-- +isSolvable :: SatSolver -> Bool+isSolvable = not . null . solve+++-- private helper functions++addClause :: MonadPlus m => IM.IntMap Bool -> m [Clause] -> Clause -> m [Clause]+addClause binds mclauses newClause = do+  oldClauses <- mclauses+  let unboundLits = foldl (addUnbound binds) (Just []) newClause+  maybe (return oldClauses)+        (\lits -> guard (not (null lits)) >> return (lits:oldClauses))+        unboundLits++addUnbound :: IM.IntMap Bool -> Maybe Clause -> Literal -> Maybe Clause+addUnbound binds mlits lit = do+  lits <- mlits+  maybe (Just (lit:lits))+        (\b -> guard (b /= isPositiveLiteral lit) >> return lits)+        (IM.lookup (literalVar lit) binds)++updateSolver :: MonadPlus m => CNF -> [(Int,Bool)] -> SatSolver -> m SatSolver+updateSolver cs bs solver = do+  bs' <- foldr (uncurry insertBinding) (return (bindings solver)) bs+  return $ solver { clauses = cs, bindings = bs' }++insertBinding :: MonadPlus m+              => Int -> Bool -> m (IM.IntMap Bool) -> m (IM.IntMap Bool)+insertBinding name newValue binds = do+  bs <- binds+  maybe (return (IM.insert name newValue bs))+        (\oldValue -> do guard (oldValue==newValue); return bs)+        (IM.lookup name bs)++simplify :: MonadPlus m => SatSolver -> m SatSolver+simplify solver = do+  (cs,bs) <- runWriterT . simplifyClauses . clauses $ solver+  updateSolver cs bs solver++simplifyClauses :: MonadPlus m => CNF -> WriterT [(Int,Bool)] m CNF+simplifyClauses [] = return []+simplifyClauses allClauses = do+  let shortestClause = head . sortBy shorter $ allClauses+  guard (not (null shortestClause))+  if null (tail shortestClause)+   then propagate (head shortestClause) allClauses >>= simplifyClauses+   else return allClauses++propagate :: MonadPlus m => Literal -> CNF -> WriterT [(Int,Bool)] m CNF+propagate literal allClauses = do+  tell [(literalVar literal, isPositiveLiteral literal)]+  return (foldr prop [] allClauses)+ where+  prop c cs | literal `elem` c = cs+            | otherwise        = filter (invLiteral literal/=) c : cs++branchOnUnbound :: MonadPlus m => Int -> SatSolver -> m SatSolver+branchOnUnbound name solver =+  guess (Pos name) solver `mplus` guess (Neg name) solver++guess :: MonadPlus m => Literal -> SatSolver -> m SatSolver+guess literal solver = do+  (cs,bs) <- runWriterT (propagate literal (clauses solver) >>= simplifyClauses)+  updateSolver cs bs solver++shorter :: [a] -> [a] -> Ordering+shorter []     []     = EQ+shorter []     _      = LT+shorter _      []     = GT+shorter (_:xs) (_:ys) = shorter xs ys++
Data/Logic/Classes/Literal.hs view
@@ -10,7 +10,6 @@     , foldAtomsLiteral     ) where -import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Combine (Combination(..)) import Data.Logic.Classes.Constants import qualified Data.Logic.Classes.FirstOrder as FOF@@ -18,7 +17,7 @@ import Data.Logic.Classes.Pretty (HasFixity(..), Fixity(..), FixityDirection(..)) import qualified Data.Logic.Classes.Propositional as P import Data.Logic.Classes.Negate-import Data.Logic.Harrison.Lib ({- instance Monad Failing -})+import Data.Logic.Failing (Failing(..)) import Text.PrettyPrint (Doc, (<>), text, parens, nest)  -- |Literals are the building blocks of the clause and implicative normal
+ Data/Logic/Failing.hs view
@@ -0,0 +1,27 @@+{-# LANGUAGE  DeriveDataTypeable, StandaloneDeriving #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Data.Logic.Failing+    ( Failing(Success, Failure)+    , failing+    ) where++import Control.Applicative.Error+import Data.Generics++failing :: ([String] -> b) -> (a -> b) -> Failing a -> b+failing f _ (Failure errs) = f errs+failing _ f (Success a)    = f a++instance Monad Failing where+  return = Success+  m >>= f =+      case m of+        (Failure errs) -> (Failure errs)+        (Success a) -> f a+  fail errMsg = Failure [errMsg]++deriving instance Typeable1 Failing+deriving instance Data a => Data (Failing a)+deriving instance Read a => Read (Failing a)+deriving instance Eq a => Eq (Failing a)+deriving instance Ord a => Ord (Failing a)
Data/Logic/Harrison/Lib.hs view
@@ -1,8 +1,7 @@ {-# LANGUAGE DeriveDataTypeable, RankNTypes, StandaloneDeriving #-} {-# OPTIONS_GHC -Wall -fno-warn-unused-binds #-} module Data.Logic.Harrison.Lib-    ( failing-    , tests+    ( tests     , setAny     , setAll     -- , itlist2@@ -35,35 +34,12 @@     , (∅)     ) where -import Control.Applicative.Error (Failing(..), ErrorMsg)-import Data.Generics+import Data.Logic.Failing (Failing(..), failing) import qualified Data.Map as Map import Data.Maybe import qualified Data.Set as Set import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual) --- | Case analysis for the 'Failing' type, from unpublished changes to --- the applicative-extras packages.  If the value is @'Failure'@, apply --- the first function to @[ErrorMsg]@; if it is @'Success' a@, apply --- the second function to @a@.-failing :: ([ErrorMsg] -> b) -> (a -> b) -> Failing a -> b-failing f _ (Failure errs) = f errs-failing _ f (Success a)    = f a- -instance Monad Failing where-  return = Success-  m >>= f =-      case m of-        (Failure errs) -> (Failure errs)-        (Success a) -> f a-  fail errMsg = Failure [errMsg]-  -deriving instance Typeable1 Failing-deriving instance Data a => Data (Failing a)-deriving instance Read a => Read (Failing a)-deriving instance Eq a => Eq (Failing a)-deriving instance Ord a => Ord (Failing a)- (∅) :: Set.Set a (∅) = Set.empty @@ -117,6 +93,7 @@ -- let can f x = try f x; true with Failure _ -> false;; can :: (t -> Failing a) -> t -> Bool can f x = failing (const True) (const False) (f x)+ {- let rec repeat f x = try repeat f (f x) with Failure _ -> x;;
Data/Logic/Harrison/Normal.hs view
@@ -15,7 +15,8 @@ import Data.Logic.Classes.Formula (Formula(atomic)) import Data.Logic.Classes.Literal (Literal, fromFirstOrder) import Data.Logic.Classes.Negate (Negatable, negated, (.~.))-import Data.Logic.Harrison.Lib (setAny, allpairs, failing)+import Data.Logic.Failing (failing)+import Data.Logic.Harrison.Lib (setAny, allpairs) import Data.Logic.Harrison.Skolem (nnf) import qualified Data.Set.Extra as Set import Prelude hiding (negate)
Data/Logic/Harrison/PropExamples.hs view
@@ -352,7 +352,7 @@ -- For large examples, should use "num" instead of "int" in these functions.  -- -------------------------------------------------------------------------  -bitlength :: forall b a. (Bits b, Num a) => b -> a+bitlength :: forall b a. (Num a, Num b, Bits b) => b -> a bitlength x = if x == 0 then 0 else 1 + bitlength (shiftR x 1);;  bit :: forall a b. (Num a, Eq a, Bits b, Integral b) => a -> b -> Bool
Data/Logic/Harrison/Resolution.hs view
@@ -8,7 +8,6 @@     , matchAtomsEq     ) where -import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Atom (Atom(match)) import Data.Logic.Classes.Combine (Combination(..)) import Data.Logic.Classes.Equals (AtomEq, zipAtomsEq)@@ -18,9 +17,10 @@ import Data.Logic.Classes.Propositional (PropositionalFormula) import Data.Logic.Classes.Term (Term(vt, foldTerm)) import Data.Logic.Classes.Variable (Variable(prefix))+import Data.Logic.Failing (Failing(..), failing) import Data.Logic.Harrison.FOL (subst, fv, generalize, list_disj, list_conj) import Data.Logic.Harrison.Lib (settryfind, allpairs, allsubsets, setAny, setAll,-                                allnonemptysubsets, (|->), apply, defined, failing)+                                allnonemptysubsets, (|->), apply, defined) import Data.Logic.Harrison.Normal (simpdnf, simpcnf, trivial) import Data.Logic.Harrison.Skolem (pnf, SkolemT, askolemize, specialize) import Data.Logic.Harrison.Tableaux (unify_literals)
Data/Logic/Harrison/Unif.hs view
@@ -6,9 +6,8 @@     , unifyAndApply     ) where -import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Term (Term(..), tsubst)-import Data.Logic.Harrison.Lib (failing)+import Data.Logic.Failing (Failing(..), failing) import qualified Data.Map as Map {- (* ========================================================================= *)@@ -34,6 +33,7 @@           if any (failing (const False) id . isTrivial env x) args           then Failure ["cyclic"]           else Success False+ {-     foldT (\ y -> y == x || (defined env y && istriv env x (apply env y)))           (\ _ args -> if any (istriv env x) args then error "cyclic" else False)
Data/Logic/Tests/Harrison/Unif.hs view
@@ -4,9 +4,8 @@     ( tests     ) where -import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Term (Term(fApp, vt), tsubst)-import Data.Logic.Harrison.Lib (failing)+import Data.Logic.Failing (Failing(..), failing) import Data.Logic.Harrison.Unif (fullUnify) import Data.Logic.Tests.HUnit () import Data.Logic.Types.Harrison.FOL (TermType)
logic-classes.cabal view
@@ -1,5 +1,5 @@ Name:             logic-classes-Version:          1.4.6+Version:          1.4.7 Synopsis:         Framework for propositional and first order logic, theorem proving Description:      Package to support Propositional and First Order Logic.  It includes classes                   representing the different types of formulas and terms, some instances of@@ -34,6 +34,7 @@                    Data.Logic.Classes.Skolem                    Data.Logic.Classes.Term                    Data.Logic.Classes.Variable+                   Data.Logic.Failing                    Data.Logic.Harrison.DefCNF                    Data.Logic.Harrison.DP                    Data.Logic.Harrison.Equal@@ -70,13 +71,15 @@                    Data.Logic.Types.Harrison.Formulas.Propositional                    Data.Logic.Types.Harrison.Prop                    Data.Logic.Types.Propositional- Build-Depends:    applicative-extras, base >= 4.3 && < 5, containers, fgl, HUnit, incremental-sat-solver,+                   Data.Boolean+                   Data.Boolean.SatSolver+ Build-Depends:    applicative-extras, base >= 4.3 && < 5, containers, fgl, HUnit,                    mtl, syb-with-class, text, PropLogic >= 0.9.0.3, pretty, safecopy, set-extra, syb, template-haskell  Executable tests  GHC-Options: -Wall -O2  Main-Is: Data/Logic/Tests/Main.hs- Build-Depends: applicative-extras, base, containers, HUnit, incremental-sat-solver, mtl,+ Build-Depends: applicative-extras, base, containers, HUnit, mtl,                 pretty, PropLogic, safecopy, set-extra, syb, template-haskell  Other-Modules:    Data.Logic.Tests.Chiou0                    Data.Logic.Tests.Common