boolsimplifier 0.1.7 → 0.1.8
raw patch · 3 files changed
+54/−37 lines, 3 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Data.BoolSimplifier: isEmptyQR, isConstQR :: QueryRep qtyp a -> Bool
+ Data.BoolSimplifier: isConstQR :: QueryRep qtyp a -> Bool
+ Data.BoolSimplifier: isEmptyQR :: QueryRep qtyp a -> Bool
Files
- Data/BoolSimplifier.hs +24/−4
- LICENSE +22/−25
- boolsimplifier.cabal +8/−8
Data/BoolSimplifier.hs view
@@ -7,6 +7,26 @@ Machinery for representing and simplifying simple propositional formulas. Type families are used to maintain a simple normal form, taking advantage of the duality between \"And\" and \"Or\". Additional tools are provided to pull out common atoms in subformulas and otherwise iterate until a simplified fixpoint. Full and general simplification is NP-hard, but the tools here can take typical machine-generated formulas and perform most simplifications that could be spotted and done by hand by a reasonable programmer. +While there are many functions below, only 'qAtom', 'andq'(s), 'orq'(s), and 'qNot' need be used directly to build expressions. 'simplifyQueryRep' performs a basic simplification, 'simplifyIons' works on expressions with negation to handle their reduction, and 'fixSimplifyQueryRep' takes a function built out of any combination of basic simplifiers (you can write your own ones taking into account any special properties of your atoms) and runs it repeatedly until it ceases to reduce the size of your target expression.++The general notion is either that you build up an expression with these combinators directly, simplify it further, and then transform it to a target semantics, or that an expression in some AST may be converted into a normal form expression using such combinators, and then simplified and transformed back to the original AST.++Here are some simple interactions:++> Prelude Data.BoolSimplifier> (qAtom "A") `orq` (qAtom "B")+> QOp | fromList [QAtom Pos "A",QAtom Pos "B"] fromList []++> Prelude Data.BoolSimplifier> ppQueryRep $ (qAtom "A") `orq` (qAtom "B")+> "(A | B)"++> Prelude Data.BoolSimplifier> ppQueryRep $ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A"))+> "(A)"++> Prelude Data.BoolSimplifier> ppQueryRep $ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A" `orq` qAtom "C"))+> "((A | B) & (A | C))"++> Prelude Data.BoolSimplifier> ppQueryRep $ simplifyQueryRep $ ((qAtom "A") `orq` (qAtom "B") `andq` (qAtom "A" `orq` qAtom "C"))+> "((A | (B & C)))" -} {-# LANGUAGE@@ -156,7 +176,7 @@ {-| -QueryReps can be queried for clauses within them, and clauses within them can be extracted. +QueryReps can be queried for clauses within them, and clauses within them can be extracted. -} class HasClause fife qtyp@@ -271,12 +291,12 @@ mp = mkClauseMap cs (maxClause, countMax) = maximumByNote "getCommonClause" (comparing snd) $ M.toList mp mkClauseMap = foldr go M.empty . F.concatMap (S.toList . extractCs)- + go c x = M.insertWith (+) c 1 x hasClauseLocal (QOp _ css) c@(QOp _ _) = c `S.member` css hasClauseLocal _ _ = False- + stripClauseLocal c (QOp as css) = QOp as (S.delete c css) stripClauseLocal _ x = x @@ -364,7 +384,7 @@ type QNeg QAndTyp = QOrTyp qNot (QOp as cs) = QOp (S.map qNot as) (S.map qNot cs) --- | +-- | -- > a /\ (b \/ ~b) /\ (c \/ d) <-> a /\ (c \/ d) -- > a /\ ~a /\ (b \/ c) <-> False -- > (a \/ ~a) /\ (b \/ ~b) <-> True (*)
LICENSE view
@@ -1,30 +1,27 @@-Copyright (c)2012, Gershom Bazerman, Jeff Polakow+Copyright (c) Gershom Bazerman 2012 All rights reserved. Redistribution and use in source and binary forms, with or without-modification, are permitted provided that the following conditions are met:-- * Redistributions of source code must retain the above copyright- notice, this list of conditions and the following disclaimer.-- * Redistributions in binary form must reproduce the above- copyright notice, this list of conditions and the following- disclaimer in the documentation and/or other materials provided- with the distribution.-- * Neither the name of Gershom Bazerman, Jeff Polakow nor the names of other- contributors may be used to endorse or promote products derived- from this software without specific prior written permission.+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission. -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS-"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT-LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR-A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT-OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,-SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT-LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,-DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY-THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.
boolsimplifier.cabal view
@@ -1,5 +1,5 @@ Name: boolsimplifier-Version: 0.1.7+Version: 0.1.8 Synopsis: Simplification tools for simple propositional formulas. Description: Normal form representation for boolean expressions. Typically simplifies such expressions, but is not guaranteed to produce the absolute simplest form.@@ -22,18 +22,18 @@ Library -- Modules exported by the library. Exposed-modules: Data.BoolSimplifier- + -- Packages needed in order to build this package. Build-depends: base >= 4, base < 7, containers >= 0.4- + ghc-options: -Wall -- Modules not exported by this package.- -- Other-modules: - + -- Other-modules:+ -- Extra tools (e.g. alex, hsc2hs, ...) needed to build the source.- -- Build-tools: - + -- Build-tools:+ source-repository head type: darcs- location: http://patch-tag.com/r/gershomb/boolsimplifier+ location: http://hub.darcs.net/gershomb/boolsimplifier