summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Data/BoolSimplifier.hs28
-rw-r--r--LICENSE47
-rw-r--r--boolsimplifier.cabal16
3 files changed, 54 insertions, 37 deletions
diff --git a/Data/BoolSimplifier.hs b/Data/BoolSimplifier.hs
index f12d614..9df79b5 100644
--- a/Data/BoolSimplifier.hs
+++ b/Data/BoolSimplifier.hs
@@ -7,6 +7,26 @@ Stability : experimental
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 @@ extractAtomCs cs = (opClauses, atomClauses)
{-|
-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 @@ getCommonClauseCs cs
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 @@ instance QNot QAndTyp where
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 (*)
diff --git a/LICENSE b/LICENSE
index c59ecdd..c5a937d 100644
--- a/LICENSE
+++ b/LICENSE
@@ -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:
+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.
- * 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.
-
-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.
diff --git a/boolsimplifier.cabal b/boolsimplifier.cabal
index ffde4c7..5735f62 100644
--- a/boolsimplifier.cabal
+++ b/boolsimplifier.cabal
@@ -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 @@ Cabal-version: >=1.6
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 \ No newline at end of file
+ location: http://hub.darcs.net/gershomb/boolsimplifier \ No newline at end of file