boolean-normal-forms (empty) → 0.0.0.1
raw patch · 32 files changed
+1474/−0 lines, 32 filesdep +QuickCheckdep +basedep +boolean-normal-formssetup-changed
Dependencies added: QuickCheck, base, boolean-normal-forms, cond, containers, tasty, tasty-quickcheck
Files
- LICENSE +20/−0
- README.md +15/−0
- Setup.hs +2/−0
- boolean-normal-forms.cabal +70/−0
- doc-formulae/cnf.svg +22/−0
- doc-formulae/dnf.svg +22/−0
- doc-formulae/nnf.svg +59/−0
- src/Data/Algebra/Boolean/CNF.hs +15/−0
- src/Data/Algebra/Boolean/CNF/List.hs +92/−0
- src/Data/Algebra/Boolean/CNF/Set.hs +105/−0
- src/Data/Algebra/Boolean/CoBoolean.hs +50/−0
- src/Data/Algebra/Boolean/DNF.hs +15/−0
- src/Data/Algebra/Boolean/DNF/List.hs +92/−0
- src/Data/Algebra/Boolean/DNF/Set.hs +105/−0
- src/Data/Algebra/Boolean/FreeBoolean.hs +56/−0
- src/Data/Algebra/Boolean/NNF.hs +15/−0
- src/Data/Algebra/Boolean/NNF/Set.hs +102/−0
- src/Data/Algebra/Boolean/NNF/Tree.hs +93/−0
- src/Data/Algebra/Boolean/Negable.hs +67/−0
- src/Data/Algebra/Boolean/NormalForm.hs +40/−0
- tests/BooleanLaws.hs +91/−0
- tests/CNFList.hs +33/−0
- tests/CNFSet.hs +37/−0
- tests/DNFList.hs +33/−0
- tests/DNFSet.hs +37/−0
- tests/FreeBoolean.hs +33/−0
- tests/FreeBooleanTests.hs +24/−0
- tests/Main.hs +25/−0
- tests/NNFSet.hs +37/−0
- tests/NNFTree.hs +33/−0
- tests/NegableLaws.hs +15/−0
- tests/SimplifyLaws.hs +19/−0
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2014 Oleg Grenrus++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ README.md view
@@ -0,0 +1,15 @@+# Boolean normal forms++[](https://travis-ci.org/phadej/boolean-normal-forms)++This library provides types that might be useful in symbolic manipulation of propositional logic expressions.++## Features++- **CNF** (list and set)+- **DNF** (list and set)+- **NNF** (tree and set)+- FreeBoolean type useful in testing++Distributed under MIT license+© Oleg Grenrus 2014
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ boolean-normal-forms.cabal view
@@ -0,0 +1,70 @@+name: boolean-normal-forms+version: 0.0.0.1+synopsis: Boolean normal form: NNF, DNF & CNF+description: The provided types that might be useful in symbolic manipulation of propositional logic expressions.+license: MIT+license-file: LICENSE+author: Oleg Grenrus+maintainer: oleg.grenrus@iki.fi+copyright: © Oleg Grenrus 2014+category: Data+build-type: Simple+cabal-version: >=1.10+extra-source-files: README.md+extra-doc-files: doc-formulae/*.svg++library+ hs-source-dirs: src+ exposed-modules: Data.Algebra.Boolean.NormalForm,+ Data.Algebra.Boolean.FreeBoolean,+ Data.Algebra.Boolean.NNF,+ Data.Algebra.Boolean.DNF,+ Data.Algebra.Boolean.CNF,+ Data.Algebra.Boolean.Negable,+ Data.Algebra.Boolean.CoBoolean,+ Data.Algebra.Boolean.NNF.Set,+ Data.Algebra.Boolean.NNF.Tree,+ Data.Algebra.Boolean.DNF.List,+ Data.Algebra.Boolean.DNF.Set,+ Data.Algebra.Boolean.CNF.List,+ Data.Algebra.Boolean.CNF.Set+ other-extensions: DeriveFunctor,+ DeriveDataTypeable,+ ConstraintKinds,+ TypeFamilies,+ ScopedTypeVariables+ build-depends: base >=4.6 && <4.8,+ containers >=0.5 && <0.6,+ cond >=0.4.1 && <0.5+ default-language: Haskell2010+ ghc-options: -Wall+ -O2+ -fwarn-tabs+ -fspec-constr-count=6+ -fmax-simplifier-iterations=10+ -fdicts-cheap++test-suite test+ default-language: Haskell2010+ type: exitcode-stdio-1.0+ hs-source-dirs: tests+ main-is: Main.hs+ other-modules: BooleanLaws,+ CNFList,+ CNFSet,+ DNFList,+ DNFSet,+ FreeBoolean,+ FreeBooleanTests,+ NegableLaws,+ NNFSet,+ NNFTree,+ SimplifyLaws+ ghc-options: -Wall -O2 -fno-warn-orphans+ build-depends: base >=4.6 && <4.8,+ containers >= 0.5 && <0.6,+ cond >=0.4.1 && <0.5,+ tasty >=0.8,+ tasty-quickcheck >=0.8.0.3,+ QuickCheck >=2.7 && <=2.8,+ boolean-normal-forms
+ doc-formulae/cnf.svg view
@@ -0,0 +1,22 @@+<?xml version='1.0' encoding='ISO-8859-1'?>+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">+<!-- This file was generated by dvisvgm 1.0.11 () -->+<!-- Sat May 10 16:17:17 2014 -->+<svg height='23.6598pt' version='1.1' viewBox='215.558 74.4999 37.3843 23.6598' width='37.3843pt' xmlns='http://www.w3.org/2000/svg' xmlns:xlink='http://www.w3.org/1999/xlink'>+<defs>+<path d='M2.268 -4.375C2.268 -4.487 2.184 -4.641 1.988 -4.641C1.799 -4.641 1.596 -4.459 1.596 -4.256C1.596 -4.137 1.687 -3.99 1.876 -3.99C2.079 -3.99 2.268 -4.186 2.268 -4.375ZM0.84 -0.819C0.812 -0.728 0.777 -0.644 0.777 -0.525C0.777 -0.196 1.057 0.07 1.442 0.07C2.142 0.07 2.45 -0.896 2.45 -1.001C2.45 -1.092 2.359 -1.092 2.338 -1.092C2.24 -1.092 2.233 -1.05 2.205 -0.973C2.044 -0.413 1.736 -0.126 1.463 -0.126C1.323 -0.126 1.288 -0.217 1.288 -0.371C1.288 -0.532 1.337 -0.665 1.4 -0.819C1.47 -1.008 1.547 -1.197 1.624 -1.379C1.687 -1.547 1.939 -2.184 1.967 -2.268C1.988 -2.338 2.009 -2.422 2.009 -2.492C2.009 -2.821 1.729 -3.087 1.344 -3.087C0.651 -3.087 0.329 -2.135 0.329 -2.016C0.329 -1.925 0.427 -1.925 0.448 -1.925C0.546 -1.925 0.553 -1.96 0.574 -2.037C0.756 -2.639 1.064 -2.891 1.323 -2.891C1.435 -2.891 1.498 -2.835 1.498 -2.646C1.498 -2.485 1.456 -2.38 1.281 -1.946L0.84 -0.819Z' id='g1-105'/>+<path d='M3.073 -4.375C3.073 -4.494 2.982 -4.641 2.793 -4.641C2.59 -4.641 2.401 -4.445 2.401 -4.256C2.401 -4.144 2.485 -3.99 2.681 -3.99C2.87 -3.99 3.073 -4.172 3.073 -4.375ZM1.589 0.343C1.47 0.826 1.099 1.232 0.686 1.232C0.595 1.232 0.511 1.218 0.434 1.19C0.616 1.106 0.672 0.938 0.672 0.833C0.672 0.665 0.539 0.574 0.399 0.574C0.182 0.574 0 0.763 0 0.987C0 1.253 0.273 1.428 0.693 1.428S1.932 1.176 2.149 0.322L2.779 -2.184C2.8 -2.261 2.814 -2.324 2.814 -2.429C2.814 -2.814 2.485 -3.087 2.065 -3.087C1.288 -3.087 0.84 -2.114 0.84 -2.016C0.84 -1.925 0.938 -1.925 0.959 -1.925C1.043 -1.925 1.05 -1.946 1.099 -2.051C1.274 -2.457 1.638 -2.891 2.044 -2.891C2.219 -2.891 2.282 -2.772 2.282 -2.548C2.282 -2.471 2.268 -2.373 2.261 -2.338L1.589 0.343Z' id='g1-106'/>+<path d='M3.73 -3.78C3.55 -4.15 3.26 -4.42 2.81 -4.42C1.64 -4.42 0.4 -2.95 0.4 -1.49C0.4 -0.55 0.95 0.11 1.73 0.11C1.93 0.11 2.43 0.07 3.03 -0.64C3.11 -0.22 3.46 0.11 3.94 0.11C4.29 0.11 4.52 -0.12 4.68 -0.44C4.85 -0.8 4.98 -1.41 4.98 -1.43C4.98 -1.53 4.89 -1.53 4.86 -1.53C4.76 -1.53 4.75 -1.49 4.72 -1.35C4.55 -0.7 4.37 -0.11 3.96 -0.11C3.69 -0.11 3.66 -0.37 3.66 -0.57C3.66 -0.79 3.68 -0.87 3.79 -1.31C3.9 -1.73 3.92 -1.83 4.01 -2.21L4.37 -3.61C4.44 -3.89 4.44 -3.91 4.44 -3.95C4.44 -4.12 4.32 -4.22 4.15 -4.22C3.91 -4.22 3.76 -4 3.73 -3.78ZM3.08 -1.19C3.03 -1.01 3.03 -0.99 2.88 -0.82C2.44 -0.27 2.03 -0.11 1.75 -0.11C1.25 -0.11 1.11 -0.66 1.11 -1.05C1.11 -1.55 1.43 -2.78 1.66 -3.24C1.97 -3.83 2.42 -4.2 2.82 -4.2C3.47 -4.2 3.61 -3.38 3.61 -3.32S3.59 -3.2 3.58 -3.15L3.08 -1.19Z' id='g0-97'/>+<path d='M9.7 13.62C9.75 13.76 9.83 14 10.12 14C10.36 14 10.54 13.81 10.54 13.58C10.54 13.53 10.54 13.51 10.48 13.35L5.93 0.23C5.86 0.09 5.71 0 5.55 0C5.26 0 5.17 0.24 5.13 0.37L0.62 13.35C0.56 13.51 0.56 13.53 0.56 13.58C0.56 13.82 0.75 14 0.98 14C1.27 14 1.34 13.77 1.39 13.64L5.55 1.68L9.7 13.62Z' id='g2-94'/>+<path d='M5.13 13.63C5.17 13.76 5.26 14 5.55 14S5.92 13.77 5.97 13.63L10.48 0.65C10.54 0.49 10.54 0.47 10.54 0.42C10.54 0.18 10.35 0 10.12 0C9.83 0 9.76 0.23 9.71 0.36L5.55 12.32L1.4 0.38C1.35 0.24 1.27 0 0.98 0C0.74 0 0.56 0.19 0.56 0.42C0.56 0.47 0.56 0.49 0.62 0.65L5.13 13.63Z' id='g2-95'/>+</defs>+<g id='page1'>+<use x='215.558' xlink:href='#g2-94' y='75.4999'/>+<use x='219.699' xlink:href='#g1-105' y='96.7986'/>+<use x='228.336' xlink:href='#g2-95' y='75.4999'/>+<use x='232.034' xlink:href='#g1-106' y='96.7986'/>+<use x='241.113' xlink:href='#g0-97' y='85'/>+<use x='246.399' xlink:href='#g1-105' y='86.5'/>+<use x='249.229' xlink:href='#g1-106' y='86.5'/>+</g>+</svg>
+ doc-formulae/dnf.svg view
@@ -0,0 +1,22 @@+<?xml version='1.0' encoding='ISO-8859-1'?>+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">+<!-- This file was generated by dvisvgm 1.0.11 () -->+<!-- Sat May 10 16:17:16 2014 -->+<svg height='23.6598pt' version='1.1' viewBox='215.558 74.4999 37.3843 23.6598' width='37.3843pt' xmlns='http://www.w3.org/2000/svg' xmlns:xlink='http://www.w3.org/1999/xlink'>+<defs>+<path d='M3.73 -3.78C3.55 -4.15 3.26 -4.42 2.81 -4.42C1.64 -4.42 0.4 -2.95 0.4 -1.49C0.4 -0.55 0.95 0.11 1.73 0.11C1.93 0.11 2.43 0.07 3.03 -0.64C3.11 -0.22 3.46 0.11 3.94 0.11C4.29 0.11 4.52 -0.12 4.68 -0.44C4.85 -0.8 4.98 -1.41 4.98 -1.43C4.98 -1.53 4.89 -1.53 4.86 -1.53C4.76 -1.53 4.75 -1.49 4.72 -1.35C4.55 -0.7 4.37 -0.11 3.96 -0.11C3.69 -0.11 3.66 -0.37 3.66 -0.57C3.66 -0.79 3.68 -0.87 3.79 -1.31C3.9 -1.73 3.92 -1.83 4.01 -2.21L4.37 -3.61C4.44 -3.89 4.44 -3.91 4.44 -3.95C4.44 -4.12 4.32 -4.22 4.15 -4.22C3.91 -4.22 3.76 -4 3.73 -3.78ZM3.08 -1.19C3.03 -1.01 3.03 -0.99 2.88 -0.82C2.44 -0.27 2.03 -0.11 1.75 -0.11C1.25 -0.11 1.11 -0.66 1.11 -1.05C1.11 -1.55 1.43 -2.78 1.66 -3.24C1.97 -3.83 2.42 -4.2 2.82 -4.2C3.47 -4.2 3.61 -3.38 3.61 -3.32S3.59 -3.2 3.58 -3.15L3.08 -1.19Z' id='g0-97'/>+<path d='M2.268 -4.375C2.268 -4.487 2.184 -4.641 1.988 -4.641C1.799 -4.641 1.596 -4.459 1.596 -4.256C1.596 -4.137 1.687 -3.99 1.876 -3.99C2.079 -3.99 2.268 -4.186 2.268 -4.375ZM0.84 -0.819C0.812 -0.728 0.777 -0.644 0.777 -0.525C0.777 -0.196 1.057 0.07 1.442 0.07C2.142 0.07 2.45 -0.896 2.45 -1.001C2.45 -1.092 2.359 -1.092 2.338 -1.092C2.24 -1.092 2.233 -1.05 2.205 -0.973C2.044 -0.413 1.736 -0.126 1.463 -0.126C1.323 -0.126 1.288 -0.217 1.288 -0.371C1.288 -0.532 1.337 -0.665 1.4 -0.819C1.47 -1.008 1.547 -1.197 1.624 -1.379C1.687 -1.547 1.939 -2.184 1.967 -2.268C1.988 -2.338 2.009 -2.422 2.009 -2.492C2.009 -2.821 1.729 -3.087 1.344 -3.087C0.651 -3.087 0.329 -2.135 0.329 -2.016C0.329 -1.925 0.427 -1.925 0.448 -1.925C0.546 -1.925 0.553 -1.96 0.574 -2.037C0.756 -2.639 1.064 -2.891 1.323 -2.891C1.435 -2.891 1.498 -2.835 1.498 -2.646C1.498 -2.485 1.456 -2.38 1.281 -1.946L0.84 -0.819Z' id='g1-105'/>+<path d='M3.073 -4.375C3.073 -4.494 2.982 -4.641 2.793 -4.641C2.59 -4.641 2.401 -4.445 2.401 -4.256C2.401 -4.144 2.485 -3.99 2.681 -3.99C2.87 -3.99 3.073 -4.172 3.073 -4.375ZM1.589 0.343C1.47 0.826 1.099 1.232 0.686 1.232C0.595 1.232 0.511 1.218 0.434 1.19C0.616 1.106 0.672 0.938 0.672 0.833C0.672 0.665 0.539 0.574 0.399 0.574C0.182 0.574 0 0.763 0 0.987C0 1.253 0.273 1.428 0.693 1.428S1.932 1.176 2.149 0.322L2.779 -2.184C2.8 -2.261 2.814 -2.324 2.814 -2.429C2.814 -2.814 2.485 -3.087 2.065 -3.087C1.288 -3.087 0.84 -2.114 0.84 -2.016C0.84 -1.925 0.938 -1.925 0.959 -1.925C1.043 -1.925 1.05 -1.946 1.099 -2.051C1.274 -2.457 1.638 -2.891 2.044 -2.891C2.219 -2.891 2.282 -2.772 2.282 -2.548C2.282 -2.471 2.268 -2.373 2.261 -2.338L1.589 0.343Z' id='g1-106'/>+<path d='M9.7 13.62C9.75 13.76 9.83 14 10.12 14C10.36 14 10.54 13.81 10.54 13.58C10.54 13.53 10.54 13.51 10.48 13.35L5.93 0.23C5.86 0.09 5.71 0 5.55 0C5.26 0 5.17 0.24 5.13 0.37L0.62 13.35C0.56 13.51 0.56 13.53 0.56 13.58C0.56 13.82 0.75 14 0.98 14C1.27 14 1.34 13.77 1.39 13.64L5.55 1.68L9.7 13.62Z' id='g2-94'/>+<path d='M5.13 13.63C5.17 13.76 5.26 14 5.55 14S5.92 13.77 5.97 13.63L10.48 0.65C10.54 0.49 10.54 0.47 10.54 0.42C10.54 0.18 10.35 0 10.12 0C9.83 0 9.76 0.23 9.71 0.36L5.55 12.32L1.4 0.38C1.35 0.24 1.27 0 0.98 0C0.74 0 0.56 0.19 0.56 0.42C0.56 0.47 0.56 0.49 0.62 0.65L5.13 13.63Z' id='g2-95'/>+</defs>+<g id='page1'>+<use x='215.558' xlink:href='#g2-95' y='75.4999'/>+<use x='219.699' xlink:href='#g1-105' y='96.7986'/>+<use x='228.336' xlink:href='#g2-94' y='75.4999'/>+<use x='232.034' xlink:href='#g1-106' y='96.7986'/>+<use x='241.113' xlink:href='#g0-97' y='85'/>+<use x='246.399' xlink:href='#g1-105' y='86.5'/>+<use x='249.229' xlink:href='#g1-106' y='86.5'/>+</g>+</svg>
+ doc-formulae/nnf.svg view
@@ -0,0 +1,59 @@+<?xml version='1.0' encoding='ISO-8859-1'?>+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">+<!-- This file was generated by dvisvgm 1.0.11 () -->+<!-- Sat May 10 16:18:00 2014 -->+<svg height='69.4444pt' version='1.1' viewBox='182.119 78.0556 104.762 69.4444' width='104.762pt' xmlns='http://www.w3.org/2000/svg' xmlns:xlink='http://www.w3.org/1999/xlink'>+<defs>+<path d='M3.03 -3.16H4.73C6.15 -3.16 7.54 -4.2 7.54 -5.32C7.54 -6.09 6.88 -6.83 5.57 -6.83H2.33C2.14 -6.83 2.03 -6.83 2.03 -6.64C2.03 -6.52 2.12 -6.52 2.32 -6.52C2.45 -6.52 2.63 -6.51 2.75 -6.5C2.91 -6.48 2.97 -6.45 2.97 -6.34C2.97 -6.3 2.96 -6.27 2.93 -6.15L1.59 -0.78C1.49 -0.39 1.47 -0.31 0.68 -0.31C0.51 -0.31 0.4 -0.31 0.4 -0.12C0.4 0 0.52 0 0.55 0C0.83 0 1.54 -0.03 1.82 -0.03C2.03 -0.03 2.25 -0.02 2.46 -0.02C2.68 -0.02 2.9 0 3.11 0C3.18 0 3.31 0 3.31 -0.2C3.31 -0.31 3.22 -0.31 3.03 -0.31C2.66 -0.31 2.38 -0.31 2.38 -0.49C2.38 -0.55 2.4 -0.6 2.41 -0.66L3.03 -3.16ZM3.75 -6.14C3.84 -6.49 3.86 -6.52 4.29 -6.52H5.25C6.08 -6.52 6.61 -6.25 6.61 -5.56C6.61 -5.17 6.41 -4.31 6.02 -3.95C5.52 -3.5 4.92 -3.42 4.48 -3.42H3.07L3.75 -6.14Z' id='g1-80'/>+<path d='M4.38 -0.06C5.93 -0.65 7.4 -2.43 7.4 -4.36C7.4 -5.97 6.34 -7.05 4.85 -7.05C2.69 -7.05 0.49 -4.78 0.49 -2.45C0.49 -0.79 1.61 0.22 3.05 0.22C3.3 0.22 3.64 0.18 4.03 0.07C3.99 0.69 3.99 0.71 3.99 0.84C3.99 1.16 3.99 1.94 4.82 1.94C6.01 1.94 6.49 0.11 6.49 0C6.49 -0.07 6.42 -0.1 6.38 -0.1C6.3 -0.1 6.28 -0.05 6.26 0.01C6.02 0.72 5.44 0.97 5.09 0.97C4.63 0.97 4.48 0.7 4.38 -0.06ZM2.49 -0.14C1.71 -0.45 1.37 -1.23 1.37 -2.13C1.37 -2.82 1.63 -4.24 2.39 -5.32C3.12 -6.34 4.06 -6.8 4.79 -6.8C5.79 -6.8 6.52 -6.02 6.52 -4.68C6.52 -3.68 6.01 -1.34 4.33 -0.4C4.28 -0.75 4.18 -1.48 3.45 -1.48C2.92 -1.48 2.43 -0.98 2.43 -0.46C2.43 -0.26 2.49 -0.15 2.49 -0.14ZM3.11 -0.03C2.97 -0.03 2.65 -0.03 2.65 -0.46C2.65 -0.86 3.03 -1.26 3.45 -1.26S4.06 -1.02 4.06 -0.41C4.06 -0.26 4.05 -0.25 3.95 -0.21C3.69 -0.1 3.39 -0.03 3.11 -0.03Z' id='g1-81'/>+<path d='M8.34 -2.3C7.79 -1.88 7.52 -1.47 7.44 -1.34C6.99 -0.65 6.91 -0.02 6.91 -0.01C6.91 0.11 7.03 0.11 7.11 0.11C7.28 0.11 7.29 0.09 7.33 -0.09C7.56 -1.07 8.15 -1.91 9.28 -2.37C9.4 -2.41 9.43 -2.43 9.43 -2.5S9.37 -2.6 9.35 -2.61C8.91 -2.78 7.7 -3.28 7.32 -4.96C7.29 -5.08 7.28 -5.11 7.11 -5.11C7.03 -5.11 6.91 -5.11 6.91 -4.99C6.91 -4.97 7 -4.34 7.42 -3.67C7.62 -3.37 7.91 -3.02 8.34 -2.7H0.91C0.73 -2.7 0.55 -2.7 0.55 -2.5S0.73 -2.3 0.91 -2.3H8.34Z' id='g0-33'/>+<path d='M6.11 -3.2C6.11 -3.53 6.08 -3.56 5.76 -3.56H0.9C0.73 -3.56 0.55 -3.56 0.55 -3.36S0.73 -3.16 0.9 -3.16H5.71V-1.25C5.71 -1.07 5.71 -0.89 5.91 -0.89S6.11 -1.07 6.11 -1.25V-3.2Z' id='g0-58'/>+<path d='M4.09 -6.28H6.88C7.05 -6.28 7.23 -6.28 7.23 -6.48S7.05 -6.68 6.88 -6.68H0.91C0.76 -6.68 0.55 -6.68 0.55 -6.48S0.76 -6.28 0.91 -6.28H3.69V-0.36C3.69 -0.21 3.69 0 3.89 0S4.09 -0.18 4.09 -0.36V-6.28Z' id='g0-62'/>+<path d='M4.09 -6.32C4.09 -6.5 4.09 -6.68 3.89 -6.68S3.69 -6.47 3.69 -6.32V-0.4H0.91C0.76 -0.4 0.55 -0.4 0.55 -0.2S0.76 0 0.91 0H6.88C7.05 0 7.23 0 7.23 -0.2S7.05 -0.4 6.88 -0.4H4.09V-6.32Z' id='g0-63'/>+<path d='M3.56 -5.77C3.48 -5.94 3.42 -5.98 3.33 -5.98C3.2 -5.98 3.17 -5.91 3.11 -5.77L0.62 -0.18C0.56 -0.05 0.55 -0.03 0.55 0.02C0.55 0.13 0.64 0.22 0.75 0.22C0.82 0.22 0.9 0.2 0.98 0.01L3.33 -5.29L5.68 0.01C5.77 0.22 5.87 0.22 5.91 0.22C6.02 0.22 6.11 0.13 6.11 0.02C6.11 0 6.11 -0.02 6.05 -0.14L3.56 -5.77Z' id='g0-94'/>+<path d='M6.04 -5.58C6.1 -5.71 6.11 -5.73 6.11 -5.78C6.11 -5.89 6.02 -5.98 5.91 -5.98C5.81 -5.98 5.75 -5.91 5.68 -5.76L3.33 -0.47L0.98 -5.77C0.9 -5.96 0.82 -5.98 0.75 -5.98C0.64 -5.98 0.55 -5.89 0.55 -5.78C0.55 -5.76 0.55 -5.74 0.61 -5.62L3.1 0.01C3.18 0.18 3.24 0.22 3.33 0.22C3.46 0.22 3.49 0.15 3.55 0.01L6.04 -5.58Z' id='g0-95'/>+<path d='M3.31 2.4C3.31 2.37 3.31 2.35 3.14 2.18C1.89 0.92 1.57 -0.97 1.57 -2.5C1.57 -4.24 1.95 -5.98 3.18 -7.23C3.31 -7.35 3.31 -7.37 3.31 -7.4C3.31 -7.47 3.27 -7.5 3.21 -7.5C3.11 -7.5 2.21 -6.82 1.62 -5.55C1.11 -4.45 0.99 -3.34 0.99 -2.5C0.99 -1.72 1.1 -0.51 1.65 0.62C2.25 1.85 3.11 2.5 3.21 2.5C3.27 2.5 3.31 2.47 3.31 2.4Z' id='g2-40'/>+<path d='M2.89 -2.5C2.89 -3.28 2.78 -4.49 2.23 -5.62C1.63 -6.85 0.77 -7.5 0.67 -7.5C0.61 -7.5 0.57 -7.46 0.57 -7.4C0.57 -7.37 0.57 -7.35 0.76 -7.17C1.74 -6.18 2.31 -4.59 2.31 -2.5C2.31 -0.79 1.94 0.97 0.7 2.23C0.57 2.35 0.57 2.37 0.57 2.4C0.57 2.46 0.61 2.5 0.67 2.5C0.77 2.5 1.67 1.82 2.26 0.55C2.77 -0.55 2.89 -1.66 2.89 -2.5Z' id='g2-41'/>+</defs>+<g id='page1'>+<use x='215.611' xlink:href='#g0-62' y='85'/>+<use x='226.167' xlink:href='#g0-33' y='85'/>+<use x='238.944' xlink:href='#g0-63' y='85'/>+<use x='215.611' xlink:href='#g0-63' y='100'/>+<use x='226.167' xlink:href='#g0-33' y='100'/>+<use x='238.944' xlink:href='#g0-62' y='100'/>+<use x='202.247' xlink:href='#g0-58' y='115'/>+<use x='208.913' xlink:href='#g0-58' y='115'/>+<use x='215.58' xlink:href='#g1-80' y='115'/>+<use x='226.167' xlink:href='#g0-33' y='115'/>+<use x='238.944' xlink:href='#g1-80' y='115'/>+<use x='182.119' xlink:href='#g0-58' y='130'/>+<use x='188.786' xlink:href='#g2-40' y='130'/>+<use x='192.674' xlink:href='#g1-80' y='130'/>+<use x='202.706' xlink:href='#g0-95' y='130'/>+<use x='211.594' xlink:href='#g1-81' y='130'/>+<use x='219.5' xlink:href='#g2-41' y='130'/>+<use x='226.167' xlink:href='#g0-33' y='130'/>+<use x='238.944' xlink:href='#g2-40' y='130'/>+<use x='242.833' xlink:href='#g0-58' y='130'/>+<use x='249.5' xlink:href='#g1-80' y='130'/>+<use x='259.531' xlink:href='#g0-94' y='130'/>+<use x='268.42' xlink:href='#g0-58' y='130'/>+<use x='275.087' xlink:href='#g1-81' y='130'/>+<use x='282.992' xlink:href='#g2-41' y='130'/>+<use x='182.119' xlink:href='#g0-58' y='145'/>+<use x='188.786' xlink:href='#g2-40' y='145'/>+<use x='192.674' xlink:href='#g1-80' y='145'/>+<use x='202.706' xlink:href='#g0-94' y='145'/>+<use x='211.594' xlink:href='#g1-81' y='145'/>+<use x='219.5' xlink:href='#g2-41' y='145'/>+<use x='226.167' xlink:href='#g0-33' y='145'/>+<use x='238.944' xlink:href='#g2-40' y='145'/>+<use x='242.833' xlink:href='#g0-58' y='145'/>+<use x='249.5' xlink:href='#g1-80' y='145'/>+<use x='259.531' xlink:href='#g0-95' y='145'/>+<use x='268.42' xlink:href='#g0-58' y='145'/>+<use x='275.087' xlink:href='#g1-81' y='145'/>+<use x='282.992' xlink:href='#g2-41' y='145'/>+</g>+</svg>
+ src/Data/Algebra/Boolean/CNF.hs view
@@ -0,0 +1,15 @@+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+-- This module re-exports 'Set'-based implementation.+--------------------------------------------------------------------+module Data.Algebra.Boolean.CNF (+ module Data.Algebra.Boolean.CNF.Set+) where++import Data.Algebra.Boolean.CNF.Set
+ src/Data/Algebra/Boolean/CNF/List.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.CNF.List (+ CNF(..),+ fromDoubleList,+ toDoubleList,+ fromNNF,+ module Data.Algebra.Boolean.NormalForm+ ) where++import Prelude hiding ((||),(&&),not,any,all,and,or)+import Data.Monoid+import Data.Either (partitionEithers)+import Data.Typeable++import Data.Algebra.Boolean.NormalForm+import Data.Algebra.Boolean.Negable hiding (not)+import qualified Data.Algebra.Boolean.Negable as Negable++import Data.Algebra.Boolean.NNF.Tree++import Data.Algebra.Boolean++-- | Boolean formula in Conjunction Normal Form+--+-- <<doc-formulae/cnf.svg>>+newtype CNF a = CNF { unCNF :: [[a]] }+ deriving (Eq, Ord, Show, Read, Functor, Typeable)++instance CoBoolean1 CNF where+ toBooleanWith f = all (any f) . unCNF++instance CoBoolean a => CoBoolean (CNF a) where+ toBoolean = toBooleanWith toBoolean++fromDoubleList :: [[a]] -> CNF a+fromDoubleList = CNF++toDoubleList :: CNF a -> [[a]]+toDoubleList = unCNF++cnfNot :: Negable a => CNF a -> CNF a+cnfNot = any and . map (map $ toNormalForm . Negable.not) . unCNF++instance Negable a => Negable (CNF a) where+ not = cnfNot++instance Negable a => Boolean (CNF a) where+ false = CNF [[]]+ true = CNF []+ (CNF a) && (CNF b) = CNF (a <> b)+ (CNF a) || (CNF b) = CNF [ a' <> b' | a' <- a, b' <- b ]+ not = cnfNot++fromNNF :: Negable a => NNF a -> CNF a+fromNNF = toBooleanWith toNormalForm++instance NormalForm CNF where+ type NFConstraint CNF a = Negable a++ toNormalForm x = CNF [[x]]++ simplify f = CNF . p . g . map (h . map f') . unCNF+ where f' x = case f x of+ Just b -> Right b+ Nothing -> Left x+ h :: [Either a Bool] -> Either [a] Bool+ h disj | True `elem` r = Right True+ | null l = Right False+ | otherwise = Left l+ where (l, r) = partitionEithers disj+ g :: [Either a Bool] -> Either [a] Bool+ g conj | False `elem` r = Right False+ | null l = Right True+ | otherwise = Left l+ where (l, r) = partitionEithers conj+ p :: Either [[a]] Bool -> [[a]]+ p (Right True) = []+ p (Right False) = [[]]+ p (Left x) = x++ fromFreeBoolean = fromNNF . toBooleanWith toNormalForm
+ src/Data/Algebra/Boolean/CNF/Set.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.CNF.Set (+ CNF(..),+ fromDoubleList,+ toDoubleList,+ fromNNF,+ module Data.Algebra.Boolean.NormalForm+ ) where++import Prelude hiding ((||),(&&),not,and,or,any,all)+import Data.Monoid+import Data.Typeable++import Data.Set (Set)+import qualified Data.Set as Set++import Data.List (sortBy, foldl')+import Data.Function (on)++import Data.Algebra.Boolean.NormalForm+import Data.Algebra.Boolean.Negable hiding (not)+import qualified Data.Algebra.Boolean.Negable as Negable++import Data.Algebra.Boolean.NNF.Tree++import Data.Algebra.Boolean++-- | Boolean formula in Conjunction Normal Form+--+-- <<doc-formulae/cnf.svg>>+newtype CNF a = CNF { unCNF :: Set (Set a) }+ deriving (Eq, Ord, Show, Read, Typeable)++instance CoBoolean1 CNF where+ toBooleanWith f = all (any f) . unCNF++instance CoBoolean a => CoBoolean (CNF a) where+ toBoolean = toBooleanWith toBoolean++toDoubleList :: CNF a -> [[a]]+toDoubleList = map Set.toList . Set.toList . unCNF++fromDoubleList :: (Ord a) => [[a]] -> CNF a+fromDoubleList = CNF . Set.fromList . map Set.fromList++cnfNot :: (Ord a, Negable a) => CNF a -> CNF a+cnfNot = any and . map (map $ toNormalForm . Negable.not) . toDoubleList++instance (Ord a, Negable a) => Negable (CNF a) where+ not = cnfNot++instance (Ord a, Negable a) => Boolean (CNF a) where+ false = CNF $ Set.singleton Set.empty+ true = CNF Set.empty+ (CNF a) && (CNF b) = CNF (a <> b)+ (CNF a) || (CNF b) = CNF $ Set.fromList [a' <> b' | a' <- Set.toList a, b' <- Set.toList b ]+ not = cnfNot++fromLeft :: Either a b -> a+fromLeft (Left x) = x+fromLeft _ = error "fromLeft called on Right value"++optimize :: Ord a => Set (Set a) -> Set (Set a)+optimize = Set.fromList . f . sortBy (flip compare `on` Set.size) . Set.toList+ where f disj = foldl' g disj disj+ g disj item = filter (not . Set.isProperSubsetOf item) disj++fromNNF :: (Ord a, Negable a) => NNF a -> CNF a+fromNNF = toBooleanWith toNormalForm++instance NormalForm CNF where+ type NFConstraint CNF a = (Negable a, Ord a)++ toNormalForm = CNF . Set.singleton . Set.singleton++ simplify f = CNF . optimize . p . g . Set.map h . Set.map (Set.map f') . unCNF+ where f' x = case f x of+ Just b -> Right b+ Nothing -> Left x+ h :: Ord a => Set (Either a Bool) -> Either (Set a) Bool+ h disj | Right True `Set.member` disj = Right True+ | Set.null l = Right False+ | otherwise = Left l+ where l = Set.mapMonotonic fromLeft $ fst $ Set.split (Right minBound) disj+ g :: Ord a => Set (Either a Bool) -> Either (Set a) Bool+ g conj | Right False `Set.member` conj = Right False+ | Set.null l = Right True+ | otherwise = Left l+ where l = Set.mapMonotonic fromLeft $ fst $ Set.split (Right minBound) conj+ p :: Either (Set (Set a)) Bool -> Set (Set a)+ p (Right True) = Set.empty+ p (Right False) = Set.singleton Set.empty+ p (Left x) = x++ fromFreeBoolean = fromNNF . toBooleanWith toNormalForm
+ src/Data/Algebra/Boolean/CoBoolean.hs view
@@ -0,0 +1,50 @@+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.CoBoolean (+ CoBoolean(..),+ CoBoolean1(..),+ toBool,+ toBoolWith+) where++import Data.Algebra.Boolean++-- | A class to values translable to booleans.+class CoBoolean a where+ -- | Cast value to 'Boolean'.+ toBoolean :: Boolean b => a -> b++-- | Less polymorphic version of 'toBoolean'.+toBool :: CoBoolean a => a -> Bool+toBool = toBoolean++-- | A polymorphic class of values translable to booleans.+class CoBoolean1 b where+ -- | Cast value to 'Boolean'.+ toBooleanWith :: Boolean c => (a -> c) -> b a -> c++-- | Less polymorphic version of 'toBooleanWith'.+toBoolWith :: CoBoolean1 b => (a -> Bool) -> b a -> Bool+toBoolWith = toBooleanWith++instance CoBoolean Bool where+ toBoolean = fromBool++instance (CoBoolean f, CoBoolean g) => CoBoolean (Either f g) where+ toBoolean (Left x) = toBoolean x+ toBoolean (Right x) = toBoolean x++instance CoBoolean (Maybe a) where+ toBoolean (Just _) = true+ toBoolean Nothing = false++instance CoBoolean1 Maybe where+ toBooleanWith f (Just x) = f x+ toBooleanWith _ Nothing = false
+ src/Data/Algebra/Boolean/DNF.hs view
@@ -0,0 +1,15 @@+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+-- This module re-exports 'Set'-based implementation.+--------------------------------------------------------------------+module Data.Algebra.Boolean.DNF (+ module Data.Algebra.Boolean.DNF.Set+) where++import Data.Algebra.Boolean.DNF.Set
+ src/Data/Algebra/Boolean/DNF/List.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.DNF.List (+ DNF(..),+ fromDoubleList,+ toDoubleList,+ fromNNF,+ module Data.Algebra.Boolean.NormalForm+ ) where++import Prelude hiding ((||),(&&),not,any,all,and,or)+import Data.Monoid+import Data.Either (partitionEithers)+import Data.Typeable++import Data.Algebra.Boolean.NormalForm+import Data.Algebra.Boolean.Negable hiding (not)+import qualified Data.Algebra.Boolean.Negable as Negable++import Data.Algebra.Boolean.NNF.Tree++import Data.Algebra.Boolean++-- | Boolean formula in Disjunction Normal Form+--+-- <<doc-formulae/dnf.svg>>+newtype DNF a = DNF { unDNF :: [[a]] }+ deriving (Eq, Ord, Show, Read, Functor, Typeable)++instance CoBoolean1 DNF where+ toBooleanWith f = any (all f) . unDNF++instance CoBoolean a => CoBoolean (DNF a) where+ toBoolean = toBooleanWith toBoolean++fromDoubleList :: [[a]] -> DNF a+fromDoubleList = DNF++toDoubleList :: DNF a -> [[a]]+toDoubleList = unDNF++dnfNot :: Negable a => DNF a -> DNF a+dnfNot = all or . map (map $ toNormalForm . Negable.not) . unDNF++instance Negable a => Negable (DNF a) where+ not = dnfNot++instance Negable a => Boolean (DNF a) where+ true = DNF [[]]+ false = DNF []+ (DNF a) || (DNF b) = DNF (a <> b)+ (DNF a) && (DNF b) = DNF [ a' <> b' | a' <- a, b' <- b ]+ not = dnfNot++fromNNF :: Negable a => NNF a -> DNF a+fromNNF = toBooleanWith toNormalForm++instance NormalForm DNF where+ type NFConstraint DNF a = Negable a++ toNormalForm x = DNF [[x]]++ simplify f = DNF . q . h . map (g . map f') . unDNF+ where f' x = case f x of+ Just b -> Right b+ Nothing -> Left x+ h :: [Either a Bool] -> Either [a] Bool+ h disj | True `elem` r = Right True+ | null l = Right False+ | otherwise = Left l+ where (l, r) = partitionEithers disj+ g :: [Either a Bool] -> Either [a] Bool+ g conj | False `elem` r = Right False+ | null l = Right True+ | otherwise = Left l+ where (l, r) = partitionEithers conj+ q :: Either [[a]] Bool -> [[a]]+ q (Right True) = [[]]+ q (Right False) = []+ q (Left x) = x++ fromFreeBoolean = fromNNF . toBooleanWith toNormalForm
+ src/Data/Algebra/Boolean/DNF/Set.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.DNF.Set (+ DNF(..),+ fromDoubleList,+ toDoubleList,+ fromNNF,+ module Data.Algebra.Boolean.NormalForm+ ) where++import Prelude hiding ((||),(&&),not,and,or,any,all)+import Data.Monoid+import Data.Typeable++import Data.Set (Set)+import qualified Data.Set as Set++import Data.List (sortBy, foldl')+import Data.Function (on)++import Data.Algebra.Boolean.NormalForm+import Data.Algebra.Boolean.Negable hiding (not)+import qualified Data.Algebra.Boolean.Negable as Negable++import Data.Algebra.Boolean.NNF.Tree++import Data.Algebra.Boolean++-- | Boolean formula in Disjunction Normal Form+--+-- <<doc-formulae/dnf.svg>>+newtype DNF a = DNF { unDNF :: Set (Set a) }+ deriving (Eq, Ord, Show, Read, Typeable)++instance CoBoolean1 DNF where+ toBooleanWith f = any (all f) . unDNF++instance CoBoolean a => CoBoolean (DNF a) where+ toBoolean = toBooleanWith toBoolean++toDoubleList :: DNF a -> [[a]]+toDoubleList = map Set.toList . Set.toList . unDNF++fromDoubleList :: (Ord a) => [[a]] -> DNF a+fromDoubleList = DNF . Set.fromList . map Set.fromList++dnfNot :: (Ord a, Negable a) => DNF a -> DNF a+dnfNot = all or . map (map $ toNormalForm . Negable.not) . toDoubleList++instance (Ord a, Negable a) => Negable (DNF a) where+ not = dnfNot++instance (Ord a, Negable a) => Boolean (DNF a) where+ true = DNF $ Set.singleton Set.empty+ false = DNF Set.empty+ (DNF a) || (DNF b) = DNF (a <> b)+ (DNF a) && (DNF b) = DNF $ Set.fromList [a' <> b' | a' <- Set.toList a, b' <- Set.toList b ]+ not = dnfNot++fromLeft :: Either a b -> a+fromLeft (Left x) = x+fromLeft _ = error "fromLeft called on Right value"++optimize :: Ord a => Set (Set a) -> Set (Set a)+optimize = Set.fromList . f . sortBy (compare `on` Set.size) . Set.toList+ where f conj = foldl' g conj conj+ g conj item = filter (not . Set.isProperSubsetOf item) conj++fromNNF :: (Ord a, Negable a) => NNF a -> DNF a+fromNNF = toBooleanWith toNormalForm++instance NormalForm DNF where+ type NFConstraint DNF a = (Negable a, Ord a)++ toNormalForm = DNF . Set.singleton . Set.singleton++ simplify f = DNF . optimize . q . h . Set.map g . Set.map (Set.map f') . unDNF+ where f' x = case f x of+ Just b -> Right b+ Nothing -> Left x+ h :: Ord a => Set (Either a Bool) -> Either (Set a) Bool+ h disj | Right True `Set.member` disj = Right True+ | Set.null l = Right False+ | otherwise = Left l+ where l = Set.mapMonotonic fromLeft $ fst $ Set.split (Right minBound) disj+ g :: Ord a => Set (Either a Bool) -> Either (Set a) Bool+ g conj | Right False `Set.member` conj = Right False+ | Set.null l = Right True+ | otherwise = Left l+ where l = Set.mapMonotonic fromLeft $ fst $ Set.split (Right minBound) conj+ q :: Either (Set (Set a)) Bool -> Set (Set a)+ q (Right True) = Set.singleton Set.empty+ q (Right False) = Set.empty+ q (Left x) = x++ fromFreeBoolean = fromNNF . toBooleanWith toNormalForm
+ src/Data/Algebra/Boolean/FreeBoolean.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveDataTypeable #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.FreeBoolean (+ FreeBoolean(..),+ module Data.Algebra.Boolean.CoBoolean+) where++import Data.Typeable++import Data.Algebra.Boolean.CoBoolean+import Data.Algebra.Boolean.Negable hiding (not)+import qualified Data.Algebra.Boolean.Negable as Negable++import Prelude hiding ((||),(&&),not,any,all)+import Data.Algebra.Boolean++-- | Free 'Boolean' type, does not perform any optimizations on the structure. Useful only in tests.+--+-- Consider using 'Data.Algebra.Boolean.NNF'.+data FreeBoolean a = FBValue a+ | FBTrue+ | FBFalse+ | FBNot (FreeBoolean a)+ | FBAnd (FreeBoolean a) (FreeBoolean a)+ | FBOr (FreeBoolean a) (FreeBoolean a)+ deriving (Eq, Ord, Show, Read, Functor, Typeable)++instance CoBoolean1 FreeBoolean where+ toBooleanWith f (FBValue x) = f x+ toBooleanWith _ FBTrue = true+ toBooleanWith _ FBFalse = false+ toBooleanWith f (FBNot x) = not $ toBooleanWith f x+ toBooleanWith f (FBOr a b) = toBooleanWith f a || toBooleanWith f b+ toBooleanWith f (FBAnd a b) = toBooleanWith f a && toBooleanWith f b++instance CoBoolean a => CoBoolean (FreeBoolean a) where+ toBoolean = toBooleanWith toBoolean++instance Negable (FreeBoolean a) where+ not = FBNot++instance Boolean (FreeBoolean a) where+ true = FBTrue+ false = FBFalse+ (||) = FBOr+ (&&) = FBAnd+ not = FBNot
+ src/Data/Algebra/Boolean/NNF.hs view
@@ -0,0 +1,15 @@+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+-- This module re-exports tree-based implementation.+--------------------------------------------------------------------+module Data.Algebra.Boolean.NNF (+ module Data.Algebra.Boolean.NNF.Tree+) where++import Data.Algebra.Boolean.NNF.Tree
+ src/Data/Algebra/Boolean/NNF/Set.hs view
@@ -0,0 +1,102 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.NNF.Set (+ NNF(..),+ module Data.Algebra.Boolean.NormalForm+ ) where++import Data.Set (Set)+import qualified Data.Set as Set++import Data.Algebra.Boolean.NormalForm+import Data.Algebra.Boolean.Negable hiding (not)+import qualified Data.Algebra.Boolean.Negable as Negable++import Prelude hiding ((||),(&&),not,any,all)+import Data.Algebra.Boolean++import Data.Typeable++-- | Boolean formula in Negation Normal Form+--+-- 'Boolean' operations will perform transformations as below:+--+-- <<doc-formulae/nnf.svg>>+data NNF a = NNFTrue+ | NNFFalse+ | NNFValue a+ | NNFOr (Set (NNF a))+ | NNFAnd (Set (NNF a))+ deriving (Eq, Ord, Show, Read, Typeable)++instance CoBoolean a => CoBoolean (NNF a) where+ toBoolean = toBooleanWith toBoolean++instance CoBoolean1 NNF where+ toBooleanWith _ NNFTrue = true+ toBooleanWith _ NNFFalse = false+ toBooleanWith f (NNFValue x) = f x+ toBooleanWith f (NNFOr xs) = any (toBooleanWith f) xs+ toBooleanWith f (NNFAnd xs) = all (toBooleanWith f) xs++orList :: Ord a => [NNF a] -> NNF a+orList x+ | Set.null s = NNFFalse+ | Set.member NNFTrue s = NNFTrue+ | otherwise = NNFOr s+ where s = Set.fromList $ filter (/= NNFFalse) $ concatMap g x+ g (NNFOr xs) = concatMap g $ Set.toList xs+ g y = [y]++andList :: Ord a => [NNF a] -> NNF a+andList x+ | Set.null s = NNFTrue+ | Set.member NNFFalse s = NNFFalse+ | otherwise = NNFAnd s+ where s = Set.fromList $ filter (/= NNFTrue) $ concatMap g x+ g (NNFAnd xs) = concatMap g $ Set.toList xs+ g y = [y]++nnfNot :: (Negable a, Ord a) => NNF a -> NNF a+nnfNot NNFTrue = NNFFalse+nnfNot NNFFalse = NNFTrue+nnfNot (NNFValue x) = NNFValue $ Negable.not x+nnfNot (NNFOr xs) = NNFAnd $ Set.map not xs+nnfNot (NNFAnd xs) = NNFOr $ Set.map not xs++instance (Ord a, Negable a) => Negable (NNF a) where+ not = nnfNot++instance (Ord a, Negable a) => Boolean (NNF a) where+ true = NNFTrue+ false = NNFFalse++ a || b = orList [a, b]+ a && b = andList [a, b]++ not = nnfNot++instance NormalForm NNF where+ type NFConstraint NNF a = (Ord a, Negable a)++ toNormalForm = NNFValue++ simplify f (NNFValue x) = case f x of+ Just True -> NNFTrue+ Just False -> NNFFalse+ Nothing -> NNFValue x+ simplify _ NNFTrue = NNFTrue+ simplify _ NNFFalse = NNFFalse+ simplify f (NNFAnd xs) = andList $ map (simplify f) $ Set.toList xs+ simplify f (NNFOr xs) = orList $ map (simplify f) $ Set.toList xs++ fromFreeBoolean = toBooleanWith toNormalForm
+ src/Data/Algebra/Boolean/NNF/Tree.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.NNF.Tree (+ NNF(..),+ module Data.Algebra.Boolean.NormalForm+ ) where++import Prelude hiding ((||),(&&),not)++import Data.Algebra.Boolean.NormalForm+import Data.Algebra.Boolean.Negable hiding (not)+import qualified Data.Algebra.Boolean.Negable as Negable++import Data.Algebra.Boolean++import Data.Typeable++-- | Boolean formula in Negation Normal Form+--+-- 'Boolean' operations will perform transformations as below:+--+-- <<doc-formulae/nnf.svg>>+data NNF a = NNFTrue+ | NNFFalse+ | NNFValue a+ | NNFOr (NNF a) (NNF a)+ | NNFAnd (NNF a) (NNF a)+ deriving (Eq, Ord, Show, Read, Functor, Typeable)++instance CoBoolean a => CoBoolean (NNF a) where+ toBoolean = toBooleanWith toBoolean++instance CoBoolean1 NNF where+ toBooleanWith _ NNFTrue = true+ toBooleanWith _ NNFFalse = false+ toBooleanWith f (NNFValue x) = f x+ toBooleanWith f (NNFOr a b) = toBooleanWith f a || toBooleanWith f b+ toBooleanWith f (NNFAnd a b) = toBooleanWith f a && toBooleanWith f b++nnfNot :: Negable a => NNF a -> NNF a+nnfNot (NNFTrue) = NNFFalse+nnfNot NNFFalse = NNFTrue+nnfNot (NNFValue x) = NNFValue $ Negable.not x+nnfNot (NNFOr a b) = NNFAnd (not a) (not b)+nnfNot (NNFAnd a b) = NNFOr (not a) (not b)++nnfOr :: NNF a -> NNF a -> NNF a+nnfOr NNFTrue _ = NNFTrue+nnfOr _ NNFTrue = NNFTrue+nnfOr NNFFalse NNFFalse = NNFFalse+nnfOr a b = NNFOr a b++nnfAnd :: NNF a -> NNF a -> NNF a+nnfAnd NNFFalse _ = NNFFalse+nnfAnd _ NNFFalse = NNFFalse+nnfAnd NNFTrue NNFTrue = NNFTrue+nnfAnd a b = NNFAnd a b++instance Negable a => Negable (NNF a) where+ not = nnfNot++instance Negable a => Boolean (NNF a) where+ true = NNFTrue+ false = NNFFalse+ (||) = nnfOr+ (&&) = nnfAnd+ not = nnfNot++instance NormalForm NNF where+ type NFConstraint NNF a = Negable a++ toNormalForm = NNFValue++ simplify f (NNFValue x) = case f x of+ Just True -> NNFTrue+ Just False -> NNFFalse+ Nothing -> NNFValue x+ simplify _ NNFTrue = NNFTrue+ simplify _ NNFFalse = NNFFalse+ simplify f (NNFAnd a b) = nnfAnd (simplify f a) (simplify f b)+ simplify f (NNFOr a b) = nnfOr (simplify f a) (simplify f b)++ fromFreeBoolean = toBooleanWith toNormalForm
+ src/Data/Algebra/Boolean/Negable.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveDataTypeable #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.Negable (+ Neg(..),+ Negable(..)+)+ where++import Data.Algebra.Boolean.CoBoolean++import Data.Monoid+import Data.Typeable++import Prelude hiding (not)+import qualified Prelude as P++import qualified Data.Algebra.Boolean as B++-- | Free 'Negable'.+data Neg a = Pos a -- ^ Positive value+ | Neg a -- ^ Negative value+ deriving (Eq, Ord, Show, Read, Functor, Typeable)++instance CoBoolean (Neg a) where+ toBoolean (Pos _) = B.true+ toBoolean (Neg _) = B.false++instance CoBoolean1 Neg where+ toBooleanWith f (Pos x) = f x+ toBooleanWith f (Neg x) = B.not $ f x++-- | Class to represent invertible values.+--+-- Must obey the double negation law: @not (not x) = x@+--+-- The negation appears only in leafs of normal forms, and the underlying proposition class+-- might have built-in negation, thus we use 'Negable'.+class Negable x where+ -- | Invert the value.+ not :: x -> x++instance Negable (Neg a) where+ not (Pos x) = Neg x+ not (Neg x) = Pos x++instance Negable Bool where+ not = P.not++instance Monoid m => Negable (Maybe m) where+ not (Just _) = Nothing+ not Nothing = Just mempty++instance (Negable a, Negable b) => Negable (a, b) where+ not (x, y) = (not x, not y)++instance (Negable a, Negable b) => Negable (Either a b) where+ not (Left x) = Left $ not x+ not (Right y) = Right $ not y
+ src/Data/Algebra/Boolean/NormalForm.hs view
@@ -0,0 +1,40 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeFamilies #-}+--------------------------------------------------------------------+-- |+-- Copyright : © Oleg Grenrus 2014+-- License : MIT+-- Maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+-- Stability : experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Data.Algebra.Boolean.NormalForm (+ NormalForm(..),+ module Data.Algebra.Boolean.CoBoolean+ ) where++import Data.Algebra.Boolean.CoBoolean+import Data.Algebra.Boolean.FreeBoolean++import GHC.Exts (Constraint)++-- | Class unifying different boolean normal forms.+class CoBoolean1 nf => NormalForm nf where+ -- | 'NormalForm' could be constrained, so the 'Set' based implementations could be included.+ type NFConstraint nf a :: Constraint+ type NFConstraint nf a = ()++ -- | Lift a value into normal form.+ toNormalForm :: a -> nf a++ -- | Simplify the formula, if some terms are ⊥ or ⊤.+ simplify :: (NFConstraint nf a) => (a -> Maybe Bool) -> nf a -> nf a++ -- | transform from free boolean form+ fromFreeBoolean :: (NFConstraint nf a) => FreeBoolean a -> nf a++instance NormalForm FreeBoolean where+ toNormalForm = FBValue+ simplify _ = id+ fromFreeBoolean = id
+ tests/BooleanLaws.hs view
@@ -0,0 +1,91 @@+module BooleanLaws (monotoneLaws, nonMonotoneLaws) where++import Test.Tasty+import Test.Tasty.QuickCheck as QC++import Prelude hiding ((||),(&&),not)+import Data.Algebra.Boolean++associativityOrProp :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool+associativityOrProp eq x y z = (x || (y || z)) `eq` ((x || y) || z)++associativityAndProp :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool+associativityAndProp eq x y z = (x || (y || z)) `eq` ((x || y) || z)++commutativeOrProp :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool+commutativeOrProp eq x y = (x || y) `eq` (y || x)++commutativeAndProp :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool+commutativeAndProp eq x y = (x && y) `eq` (y && x)++distributivity1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool+distributivity1Prop eq x y z = (x && (y || z)) `eq` ((x && y) || (x && z))++distributivity2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> a -> Bool+distributivity2Prop eq x y z = (x || (y && z)) `eq` ((x || y) && (x || z))++identityOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+identityOrProp eq x = (x || false) `eq` x++identityAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+identityAndProp eq x = (x && true) `eq` x++annihilatorOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+annihilatorOrProp eq x = (x || true) `eq` true++annihilatorAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+annihilatorAndProp eq x = (x && false) `eq` false++idempotenceOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+idempotenceOrProp eq x = (x || x) `eq` x++idempotenceAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+idempotenceAndProp eq x = (x && x) `eq` x++absorption1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool+absorption1Prop eq x y = (x && (x || y)) `eq` x++absorption2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool+absorption2Prop eq x y = (x || (x && y)) `eq` x++complementationOrProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+complementationOrProp eq x = (x || not x) `eq` true++complementationAndProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+complementationAndProp eq x = (x && not x) `eq` false++doubleNegationProp :: Boolean a => (a -> a -> Bool) -> a -> Bool+doubleNegationProp eq x = not (not x) `eq` x++deMorgan1Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool+deMorgan1Prop eq x y = (not x && not y) `eq` not (x || y)++deMorgan2Prop :: Boolean a => (a -> a -> Bool) -> a -> a -> Bool+deMorgan2Prop eq x y = (not x || not y) `eq` not (x && y)++monotoneLaws :: (Arbitrary a, Show a, Boolean a) => (a -> a -> Bool) -> TestTree+monotoneLaws eq = testGroup "Monotone boolean laws"+ [ QC.testProperty "associativity or" $ associativityOrProp eq+ , QC.testProperty "associativity and" $ associativityAndProp eq+ , QC.testProperty "commutativity or" $ commutativeOrProp eq+ , QC.testProperty "commutativity and" $ commutativeAndProp eq+ , QC.testProperty "distributivity 1" $ distributivity1Prop eq+ , QC.testProperty "distributivity 2" $ distributivity2Prop eq+ , QC.testProperty "identity or" $ identityOrProp eq+ , QC.testProperty "identity and" $ identityAndProp eq+ , QC.testProperty "annihilator or" $ annihilatorOrProp eq+ , QC.testProperty "annihilator and" $ annihilatorAndProp eq+ , QC.testProperty "idempotence or" $ idempotenceOrProp eq+ , QC.testProperty "idempotence and" $ idempotenceAndProp eq+ , QC.testProperty "absorption 1" $ absorption1Prop eq+ , QC.testProperty "absorption 2" $ absorption2Prop eq+ ]++nonMonotoneLaws :: (Arbitrary a, Show a, Boolean a) => (a -> a -> Bool) -> TestTree+nonMonotoneLaws eq = testGroup "Non monotone boolean laws"+ [ QC.testProperty "complementation or" $ complementationOrProp eq+ , QC.testProperty "complementation and" $ complementationAndProp eq+ , QC.testProperty "double negation" $ doubleNegationProp eq+ , QC.testProperty "de Morgan 1" $ deMorgan1Prop eq+ , QC.testProperty "de Morgan 2" $ deMorgan2Prop eq+ ]
+ tests/CNFList.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE ScopedTypeVariables #-}+module CNFList (tests) where++import BooleanLaws+import SimplifyLaws+import BooleanModelLaws++import FreeBoolean++import Test.Tasty+import Test.QuickCheck++import Control.Applicative+import Data.Function (on)++import Data.Algebra.Boolean.Negable (Negable, Neg(..))+import Data.Algebra.Boolean.CNF.List++instance Arbitrary a => Arbitrary (Neg a) where+ arbitrary = oneof [ Pos <$> arbitrary, Pos <$> arbitrary ]++instance (Negable a, Arbitrary a) => Arbitrary (CNF a) where+ arbitrary = fromFreeBoolean <$> arbitrary++tests :: TestTree+tests = testGroup "CNF list implementation"+ [ monotoneLaws eq+ , simplifyLaws (undefined :: CNF (Either Bool Bool))+ , booleanModelLaws (undefined :: CNF (Either Bool Bool))+ ]++eq :: CNF (Neg Int) -> CNF (Neg Int) -> Bool+eq = (==) `on` toBool
+ tests/CNFSet.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE ScopedTypeVariables #-}+module CNFSet (tests) where++import BooleanLaws+import NegableLaws+import SimplifyLaws+import BooleanModelLaws++import FreeBoolean++import Test.Tasty+import Test.QuickCheck++import Control.Applicative+import Data.Monoid+import Data.Function (on)++import Data.Algebra.Boolean.Negable (Negable)+import Data.Algebra.Boolean.CNF.Set++instance Arbitrary a => Arbitrary (Sum a) where+ arbitrary = Sum <$> arbitrary++instance (Ord a, Negable a, Arbitrary a) => Arbitrary (CNF a) where+ arbitrary = fromFreeBoolean <$> arbitrary++tests :: TestTree+tests = testGroup "CNF set implementation"+ [ monotoneLaws eq+ , nonMonotoneLaws eq+ , negableLaws eq+ , simplifyLaws (undefined :: CNF (Either Bool Bool))+ , booleanModelLaws (undefined :: CNF (Either Bool Bool))+ ]++eq :: CNF (Maybe (Sum Int)) -> CNF (Maybe (Sum Int)) -> Bool+eq = (==) `on` toBool
+ tests/DNFList.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE ScopedTypeVariables #-}+module DNFList (tests) where++import BooleanLaws+import SimplifyLaws+import BooleanModelLaws++import FreeBoolean++import Test.Tasty+import Test.QuickCheck++import Control.Applicative+import Data.Function (on)++import Data.Algebra.Boolean.Negable (Negable, Neg(..))+import Data.Algebra.Boolean.DNF.List++instance Arbitrary a => Arbitrary (Neg a) where+ arbitrary = oneof [ Pos <$> arbitrary, Pos <$> arbitrary ]++instance (Negable a, Arbitrary a) => Arbitrary (DNF a) where+ arbitrary = fromFreeBoolean <$> arbitrary++tests :: TestTree+tests = testGroup "DNF list implementation"+ [ monotoneLaws eq+ , simplifyLaws (undefined :: DNF (Either Bool Bool))+ , booleanModelLaws (undefined :: DNF (Either Bool Bool))+ ]++eq :: DNF (Neg Int) -> DNF (Neg Int) -> Bool+eq = (==) `on` toBool
+ tests/DNFSet.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE ScopedTypeVariables #-}+module DNFSet (tests) where++import BooleanLaws+import NegableLaws+import SimplifyLaws+import BooleanModelLaws++import FreeBoolean++import Test.Tasty+import Test.QuickCheck++import Control.Applicative+import Data.Monoid+import Data.Function (on)++import Data.Algebra.Boolean.Negable (Negable)+import Data.Algebra.Boolean.DNF.Set++instance Arbitrary a => Arbitrary (Sum a) where+ arbitrary = Sum <$> arbitrary++instance (Ord a, Negable a, Arbitrary a) => Arbitrary (DNF a) where+ arbitrary = fromFreeBoolean <$> arbitrary++tests :: TestTree+tests = testGroup "DNF set implementation"+ [ monotoneLaws eq+ , nonMonotoneLaws eq+ , negableLaws eq+ , simplifyLaws (undefined :: DNF (Either Bool Bool))+ , booleanModelLaws (undefined :: DNF (Either Bool Bool))+ ]++eq :: DNF (Maybe (Sum Int)) -> DNF (Maybe (Sum Int)) -> Bool+eq = (==) `on` toBool
+ tests/FreeBoolean.hs view
@@ -0,0 +1,33 @@+module FreeBoolean (+ freeBooleanHeight,+ module Data.Algebra.Boolean.FreeBoolean+ ) where++import Test.Tasty.QuickCheck++import Control.Applicative++import Data.Algebra.Boolean.FreeBoolean++instance Arbitrary a => Arbitrary (FreeBoolean a) where+ arbitrary = sized arbitrary'+ where arbitrary' 0 = frequency [+ (10, FBValue <$> arbitrary),+ (1, pure FBTrue),+ (1, pure FBFalse)+ ]+ arbitrary' n = oneof [+ FBValue <$> arbitrary,+ FBNot <$> arbitrary'',+ FBAnd <$> arbitrary'' <*> arbitrary'',+ FBOr <$> arbitrary'' <*> arbitrary''+ ]+ where arbitrary'' = arbitrary' $ n `div` 2++freeBooleanHeight :: FreeBoolean a -> Int+freeBooleanHeight FBTrue = 0+freeBooleanHeight FBFalse = 0+freeBooleanHeight (FBValue _) = 0+freeBooleanHeight (FBNot x) = 1 + freeBooleanHeight x+freeBooleanHeight (FBAnd a b) = 1 + max (freeBooleanHeight a) (freeBooleanHeight b)+freeBooleanHeight (FBOr a b) = 1 + max (freeBooleanHeight a) (freeBooleanHeight b)
+ tests/FreeBooleanTests.hs view
@@ -0,0 +1,24 @@+module FreeBooleanTests where++import BooleanLaws+import NegableLaws+import SimplifyLaws+import BooleanModelLaws++import FreeBoolean++import Data.Function (on)++import Test.Tasty++tests :: TestTree+tests = testGroup "Free boolean"+ [ monotoneLaws eq+ , nonMonotoneLaws eq+ , negableLaws eq+ , simplifyLaws (undefined :: FreeBoolean (Either Bool Bool))+ , booleanModelLaws (undefined :: FreeBoolean (Either Bool Bool))+ ]++eq :: FreeBoolean Int -> FreeBoolean Int -> Bool+eq = (==) `on` toBoolWith (1==)
+ tests/Main.hs view
@@ -0,0 +1,25 @@+module Main (main) where++import qualified NNFTree+import qualified NNFSet+import qualified DNFList+import qualified DNFSet+import qualified CNFList+import qualified CNFSet+import qualified FreeBooleanTests as FBT++import Test.Tasty++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests = testGroup "Tests" [+ NNFTree.tests,+ NNFSet.tests,+ CNFList.tests,+ CNFSet.tests,+ DNFList.tests,+ DNFSet.tests,+ FBT.tests+ ]
+ tests/NNFSet.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE ScopedTypeVariables #-}+module NNFSet (tests) where++import BooleanLaws+import NegableLaws+import SimplifyLaws+import BooleanModelLaws++import FreeBoolean++import Test.Tasty+import Test.QuickCheck++import Control.Applicative+import Data.Monoid+import Data.Function (on)++import Data.Algebra.Boolean.Negable (Negable)+import Data.Algebra.Boolean.NNF.Set++instance Arbitrary a => Arbitrary (Sum a) where+ arbitrary = Sum <$> arbitrary++instance (Ord a, Negable a, Arbitrary a) => Arbitrary (NNF a) where+ arbitrary = fromFreeBoolean <$> arbitrary++tests :: TestTree+tests = testGroup "NNF set implementation"+ [ monotoneLaws eq+ , nonMonotoneLaws eq+ , negableLaws eq+ , simplifyLaws (undefined :: NNF (Either Bool Bool))+ , booleanModelLaws (undefined :: NNF (Either Bool Bool))+ ]++eq :: NNF (Maybe (Sum Int)) -> NNF (Maybe (Sum Int)) -> Bool+eq = (==) `on` toBool
+ tests/NNFTree.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE ScopedTypeVariables #-}+module NNFTree (tests) where++import BooleanLaws+import NegableLaws+import SimplifyLaws+import BooleanModelLaws++import FreeBoolean++import Test.Tasty+import Test.QuickCheck++import Control.Applicative+import Data.Function (on)++import Data.Algebra.Boolean.Negable (Negable)+import Data.Algebra.Boolean.NNF.Tree++instance (Negable a, Arbitrary a) => Arbitrary (NNF a) where+ arbitrary = fromFreeBoolean <$> arbitrary++tests :: TestTree+tests = testGroup "NNF tree implementation"+ [ monotoneLaws eq+ , nonMonotoneLaws eq+ , negableLaws eq+ , simplifyLaws (undefined :: NNF (Either Bool Bool))+ , booleanModelLaws (undefined :: NNF (Either Bool Bool))+ ]++eq :: NNF Bool -> NNF Bool -> Bool+eq = (==) `on` toBool
+ tests/NegableLaws.hs view
@@ -0,0 +1,15 @@+module NegableLaws (negableLaws) where++import Test.Tasty+import Test.Tasty.QuickCheck as QC++import Prelude hiding (not)+import Data.Algebra.Boolean.Negable++doubleNegationProp :: Negable a => (a -> a -> Bool) -> a -> Bool+doubleNegationProp eq x = not (not x) `eq` x++negableLaws :: (Arbitrary a, Show a, Negable a) => (a -> a -> Bool) -> TestTree+negableLaws eq = testGroup "Negable laws"+ [ QC.testProperty "double negation" $ doubleNegationProp eq+ ]
+ tests/SimplifyLaws.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ConstraintKinds #-}+module SimplifyLaws (simplifyLaws) where++import Test.Tasty+import Test.Tasty.QuickCheck as QC++import Data.Algebra.Boolean.CoBoolean+import Data.Algebra.Boolean.NormalForm++simplifyProperty :: (CoBoolean a, NormalForm nf, NFConstraint nf (Either a Bool)) => nf (Either a Bool) -> Bool+simplifyProperty nf = toBooleanWith toBoolean (simplify f nf) == (toBooleanWith toBoolean nf :: Bool)+ where f (Right b) = Just b+ f (Left _) = Nothing++simplifyLaws :: forall a nf. (CoBoolean a, NormalForm nf, NFConstraint nf (Either a Bool), Show (nf (Either a Bool)), Arbitrary (nf (Either a Bool))) => nf (Either a Bool) -> TestTree+simplifyLaws _ = QC.testProperty "simplify property" prop+ where prop :: nf (Either a Bool) -> Bool+ prop = simplifyProperty