Proper 0.3.0.0 → 0.4.0.0
raw patch · 4 files changed
+157/−6 lines, 4 files
Files
- Proper.cabal +8/−4
- src/Proper/BDD.hs +131/−0
- src/Proper/Sentence.hs +16/−2
- test/Main.hs +2/−0
Proper.cabal view
@@ -2,10 +2,14 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: Proper-version: 0.3.0.0+version: 0.4.0.0 synopsis: An implementation of propositional logic in Haskell --- description: -license: BSD3 +description: Proper is both an executable theorem prover for Propositional logic+ and a library for incorporating propositional logic into other Haskell+ programs. See the github repo for examples of theorem files for the+ executable.++license: BSD3 license-file: LICENSE author: Dillon Huff maintainer: Dillon Huff@@ -18,7 +22,7 @@ library hs-source-dirs: src build-depends: base==4.5.*, containers- exposed-modules: Proper.Sentence, Proper.CNF, Proper.Clause+ exposed-modules: Proper.Sentence, Proper.CNF, Proper.Clause, Proper.BDD executable Proper main-is: Main.hs
+ src/Proper/BDD.hs view
@@ -0,0 +1,131 @@+module Proper.BDD(+ BDD, trueBDD, falseBDD, singletonBDD, negBDD,+ disBDD, conBDD, impBDD, bicBDD,+ isTaut) where++import Data.Map as M+import Data.List as L+import Data.Tuple as T++data BDD p =+ TrueNode |+ FalseNode |+ N p (BDD p) (BDD p)+ deriving (Eq, Show)+ +node :: (Eq p) => p -> BDD p -> BDD p -> BDD p+node v l r = case l == r of+ True -> l+ False -> N v l r+ +trueBDD = TrueNode+falseBDD = FalseNode+singletonBDD v = N v TrueNode FalseNode++negBDD :: (Eq p) => BDD p -> BDD p+negBDD TrueNode = FalseNode+negBDD FalseNode = TrueNode+negBDD (N p l r) = node p (negBDD l) (negBDD r)++disBDD :: (Ord p) => BDD p -> BDD p -> BDD p+disBDD TrueNode _ = TrueNode+disBDD _ TrueNode = TrueNode+disBDD FalseNode n = n+disBDD n FalseNode = n+disBDD l@(N p ll lr) r@(N q rl rr) = case compare p q of+ LT -> node q (disBDD l rl) (disBDD l rr)+ GT -> node p (disBDD ll r) (disBDD lr r)+ EQ -> node p (disBDD ll rl) (disBDD lr rr)+ +conBDD :: (Ord p) => BDD p -> BDD p -> BDD p+conBDD l r = negBDD (disBDD (negBDD l) (negBDD r))++impBDD :: (Ord p) => BDD p -> BDD p -> BDD p+impBDD l r = (disBDD (negBDD l) r)++bicBDD :: (Ord p) => BDD p -> BDD p -> BDD p+bicBDD l r = (conBDD (impBDD l r) (impBDD r l))++isTaut TrueNode = True+isTaut _ = False+{-+data BDD p = BDD (Map (BDDNode p) Int) (Map Int (BDDNode p)) Int+ deriving (Eq, Show)+ +data BDDNode p =+ TrueNode |+ FalseNode |+ N p Int Int+ deriving (Eq, Ord, Show)+ +negateNode :: BDDNode p -> BDDNode p+negateNode (N p l r) = N p r l+negateNode n = n++root :: (Ord p) => BDD p -> BDDNode+root (BDD nToInt _ _) = fst $ M.findMax nToInd++leftChild :: (Ord p) => BDD p -> BDD p+leftChild bdd@(BDD nToInt intToN n) = deleteTreeFrom (rightNode r) (deleteNode r bdd)+ where+ r = root bdd+ +deleteTreeFrom :: (Ord p) => BDDNode p -> BDD p -> BDD p+deleteTreeFrom (N p l r) bdd = deleteTreeFrom + +deleteNode :: (Ord p) => BDDNode p -> BDD p -> BDD p+deleteNode n bdd@(BDD nToInt intToN m) = BDD (M.delete n nToInt) (M.delete nInd intToN) m+ where+ nInd = case M.lookup n nToInt of+ Just ind -> ind+ Nothing -> m+1++trueBDD :: (Ord p) => BDD p+trueBDD = BDD (M.fromList [(TrueNode, 1)]) (M.fromList [(1, TrueNode)]) 2++falseBDD :: (Ord p) => BDD p+falseBDD = BDD (M.fromList [(FalseNode, 0)]) (M.fromList [(0, FalseNode)]) 2++singletonBDD :: (Ord p) => p -> BDD p+singletonBDD val = BDD (M.fromList sl) (M.fromList (L.map swap sl)) 3+ where+ sl = [(TrueNode, 1), (FalseNode, 0), (N val 1 0, 2)]+ +negBDD :: (Ord p) => BDD p -> BDD p+negBDD (BDD nToInt intToN n) = BDD negNToInt negIntToN n+ where+ negNToInt = mapKeys negateNode nToInt+ negIntToN = M.fromList $ L.map swap $ M.toList negNToInt+ +disBDD :: (Ord p) => BDD p -> BDD p -> BDD p+disBDD left right = case left == trueBDD || right == trueBDD of+ True -> trueBDD+ False -> case left == falseBDD && right == falseBDD of+ True -> falseBDD+ False -> disMerge left right+ +disMerge :: (Ord p) => BDD p -> BDD p -> BDD p+disMerge left right = case leftRoot == rightRoot of+ True -> makeBDD leftRoot (disBDD lrlc rrlc) (disBDD lrrc rrrc)+ False -> case leftRoot > rightRoot of+ True -> makeBDD leftRoot (disBDD lrlc rightRoot) (disBDD lrrc rightRoot)+ False -> makeBDD rightRoot (disBDD leftRoot rrlc) (disBDD leftRoot rrrc)+ where+ leftRoot = root left+ rightRoot = root right+ lrlc = leftChild leftRoot+ lrrc = rightChild leftRoot+ rrlc = leftChild rightRoot+ rrrc = rightChild rightRoot++isTaut :: (Ord p) => BDD p -> Bool+isTaut b = b == trueBDD++newBDD :: (Ord p) => BDD p+newBDD = BDD M.empty M.empty 2++addNode :: (Ord p) => BDD p -> BDDNode p -> (BDD p, Int)+addNode bdd@(BDD nToInt intToN n) newNode = case M.lookup newNode nToInt of+ Just nodeInd -> (bdd, nodeInd)+ Nothing -> (BDD (M.insert newNode (n+1) nToInt) (M.insert (n+1) newNode intToN) (n+1), n)+-}
src/Proper/Sentence.hs view
@@ -4,12 +4,13 @@ truthAssignment, evalSentence, isValidByTruthTable,- toCNF, theorem) where+ toCNF, theorem,+ bddCheckTaut) where import Data.Foldable import Data.Monoid import Data.Map as M-+import Proper.BDD import Proper.Clause import Proper.CNF import Proper.Utils@@ -217,3 +218,16 @@ cnfAxioms = Prelude.map toCNF axioms cnfNotHypothesis = toCNF (neg hypothesis) cnfFormNegThm = mergeCNFFormulas (cnfNotHypothesis:cnfAxioms)+ +-- BDD conversion code+ +bddCheckTaut :: (Ord s) => Sentence s -> Bool+bddCheckTaut sent = isTaut (toBDD sent)++toBDD :: (Ord s) => Sentence s -> BDD s+toBDD (Val n) = singletonBDD n+toBDD (Neg sent) = negBDD (toBDD sent)+toBDD (Dis f1 f2) = disBDD (toBDD f1) (toBDD f2)+toBDD (Con f1 f2) = conBDD (toBDD f1) (toBDD f2)+toBDD (Imp f1 f2) = impBDD (toBDD f1) (toBDD f2)+toBDD (Bic f1 f2) = bicBDD (toBDD f1) (toBDD f2)
test/Main.hs view
@@ -1,5 +1,6 @@ module Main(main) where +import Proper.BDDTests import Proper.CNFTests import Proper.LexerTests import Proper.ParserTests@@ -10,3 +11,4 @@ allCNFTests allLexerTests allParserTests+ allBDDTests