| Copyright | (c) Gershom Bazerman Jeff Polakow 2011 |
|---|---|
| License | BSD 3 Clause |
| Maintainer | [email protected] |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | Haskell98 |
Data.BoolSimplifier
Description
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)))"
Synopsis
- data QOrTyp
- data QAndTyp
- data QAtomTyp
- type family QFlipTyp t
- data QueryRep qtyp a where
- extractAs :: QueryRep qtyp a -> Set (QueryRep QAtomTyp a)
- extractCs :: QueryRep qtyp a -> Set (QueryRep (QFlipTyp qtyp) a)
- qOr :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QAndTyp a) -> QueryRep QOrTyp a
- qAnd :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QOrTyp a) -> QueryRep QAndTyp a
- class PPQueryRep a where
- ppQueryRep :: a -> String
- qop :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a
- extractAtomCs :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep qtyp a) -> (Set (QueryRep qtyp a), Set (QueryRep QAtomTyp a))
- class HasClause fife qtyp where
- andqs :: (Ord a, CombineQ a qtyp QAndTyp) => [QueryRep qtyp a] -> QueryRep QAndTyp a
- orqs :: (Ord a, CombineQ a qtyp QOrTyp) => [QueryRep qtyp a] -> QueryRep QOrTyp a
- class CombineQ a qtyp1 qtyp2 where
- simplifyQueryRep :: (Ord a, Show (QFlipTyp qtyp), Show (QFlipTyp (QFlipTyp qtyp)), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp a -> QueryRep qtyp a
- getCommonClauseAs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep QAtomTyp a, Set (QueryRep fife a), Set (QueryRep fife a))
- getCommonClauseCs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep (QFlipTyp fife) a, Set (QueryRep fife a), Set (QueryRep fife a))
- fixSimplifyQueryRep :: (QueryRep qtyp a -> QueryRep qtyp a) -> QueryRep qtyp a -> QueryRep qtyp a
- data Ion a
- qAtom :: Ord a => a -> QueryRep QAtomTyp (Ion a)
- isEmptyQR :: QueryRep qtyp a -> Bool
- isConstQR :: QueryRep qtyp a -> Bool
- class PPConstQR qtyp where
- class QNot qtyp where
- simplifyIons :: (Ord a, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp (Ion a) -> QueryRep qtyp (Ion a)
- maximumByNote :: String -> (a -> a -> Ordering) -> [a] -> a
Documentation
We'll start with three types of formulas: disjunctions, conjunctions, and atoms
Instances
| Show QOrTyp Source # | |
| PPConstQR QOrTyp Source # | |
| QNot QOrTyp Source # | |
| Ord a => CombineQ a QAndTyp QOrTyp Source # | |
| Ord a => CombineQ a QAtomTyp QOrTyp Source # | |
| Ord a => CombineQ a QOrTyp QAndTyp Source # | |
| Ord a => CombineQ a QOrTyp QAtomTyp Source # | |
| Ord a => CombineQ a QOrTyp QOrTyp Source # | |
| PPQueryRep (QueryRep QOrTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| type QFlipTyp QOrTyp Source # | |
Defined in Data.BoolSimplifier | |
| type QNeg QOrTyp Source # | |
Defined in Data.BoolSimplifier | |
Instances
| Show QAndTyp Source # | |
| PPConstQR QAndTyp Source # | |
| QNot QAndTyp Source # | |
| Ord a => CombineQ a QAndTyp QAndTyp Source # | |
| Ord a => CombineQ a QAndTyp QAtomTyp Source # | |
| Ord a => CombineQ a QAndTyp QOrTyp Source # | |
| Ord a => CombineQ a QAtomTyp QAndTyp Source # | |
| Ord a => CombineQ a QOrTyp QAndTyp Source # | |
| PPQueryRep (QueryRep QAndTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| type QFlipTyp QAndTyp Source # | |
Defined in Data.BoolSimplifier | |
| type QNeg QAndTyp Source # | |
Defined in Data.BoolSimplifier | |
Instances
| QNot QAtomTyp Source # | |
| HasClause fife QAtomTyp Source # | |
| Ord a => CombineQ a QAndTyp QAtomTyp Source # | |
| Ord a => CombineQ a QAtomTyp QAndTyp Source # | |
| Ord a => CombineQ a QAtomTyp QAtomTyp Source # | |
| Ord a => CombineQ a QAtomTyp QOrTyp Source # | |
| Ord a => CombineQ a QOrTyp QAtomTyp Source # | |
| PPQueryRep (QueryRep QAtomTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| type QNeg QAtomTyp Source # | |
Defined in Data.BoolSimplifier | |
data QueryRep qtyp a where Source #
A formula is either an atom (of some type, e.g. String).
A non-atomic formula (which is either a disjunction or a conjunction) is
n-ary and consists of a Set of atoms and a set of non-atomic subformulas of
dual connective, i.e. the non-atomic subformulas of a disjunction must all
be conjunctions. The type system enforces this since there is no QFlipTyp
instance for QAtomTyp.
Constructors
| QAtom :: forall a. Ord a => a -> QueryRep QAtomTyp a | |
| QOp :: forall qtyp a. (Show qtyp, Ord a) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a |
Instances
| Show a => Show (QueryRep qtyp a) Source # | |
| PPQueryRep (QueryRep QAndTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| PPQueryRep (QueryRep QAtomTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| PPQueryRep (QueryRep QOrTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| PPQueryRep (QueryRep qtyp String) Source # | |
Defined in Data.BoolSimplifier | |
| Eq a => Eq (QueryRep qtyp a) Source # | |
| Ord a => Ord (QueryRep qtyp a) Source # | |
Defined in Data.BoolSimplifier Methods compare :: QueryRep qtyp a -> QueryRep qtyp a -> Ordering # (<) :: QueryRep qtyp a -> QueryRep qtyp a -> Bool # (<=) :: QueryRep qtyp a -> QueryRep qtyp a -> Bool # (>) :: QueryRep qtyp a -> QueryRep qtyp a -> Bool # (>=) :: QueryRep qtyp a -> QueryRep qtyp a -> Bool # max :: QueryRep qtyp a -> QueryRep qtyp a -> QueryRep qtyp a # min :: QueryRep qtyp a -> QueryRep qtyp a -> QueryRep qtyp a # | |
qOr :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QAndTyp a) -> QueryRep QOrTyp a Source #
convenience constructors, not particularly smart
qAnd :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QOrTyp a) -> QueryRep QAndTyp a Source #
class PPQueryRep a where Source #
pretty printer class
Methods
ppQueryRep :: a -> String Source #
Instances
| PPQueryRep (QueryRep QAndTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| PPQueryRep (QueryRep QAtomTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| PPQueryRep (QueryRep QOrTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| PPQueryRep (QueryRep qtyp String) Source # | |
Defined in Data.BoolSimplifier | |
qop :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a Source #
smart constructor for QOp
does following optimization: a /\ (a \/ b) <-> a, or dually: a \/ (a /\ b) <-> a
extractAtomCs :: (Ord a, Show qtyp, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => Set (QueryRep qtyp a) -> (Set (QueryRep qtyp a), Set (QueryRep QAtomTyp a)) Source #
class HasClause fife qtyp where Source #
QueryReps can be queried for clauses within them, and clauses within them can be extracted.
Methods
hasClause :: QueryRep fife a -> QueryRep qtyp a -> Bool Source #
stripClause :: QueryRep qtyp a -> QueryRep fife a -> QueryRep fife a Source #
andqs :: (Ord a, CombineQ a qtyp QAndTyp) => [QueryRep qtyp a] -> QueryRep QAndTyp a Source #
convenience functions
class CombineQ a qtyp1 qtyp2 where Source #
smart constructors for QueryRep
Methods
andq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QAndTyp a Source #
orq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QOrTyp a Source #
Instances
| Ord a => CombineQ a QAndTyp QAndTyp Source # | |
| Ord a => CombineQ a QAndTyp QAtomTyp Source # | |
| Ord a => CombineQ a QAndTyp QOrTyp Source # | |
| Ord a => CombineQ a QAtomTyp QAndTyp Source # | |
| Ord a => CombineQ a QAtomTyp QAtomTyp Source # | |
| Ord a => CombineQ a QAtomTyp QOrTyp Source # | |
| Ord a => CombineQ a QOrTyp QAndTyp Source # | |
| Ord a => CombineQ a QOrTyp QAtomTyp Source # | |
| Ord a => CombineQ a QOrTyp QOrTyp Source # | |
simplifyQueryRep :: (Ord a, Show (QFlipTyp qtyp), Show (QFlipTyp (QFlipTyp qtyp)), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp a -> QueryRep qtyp a Source #
(a /\ b) \/ (a /\ c) \/ d <-> (a /\ (b \/ c)) \/ d (and also the dual)
getCommonClauseAs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep QAtomTyp a, Set (QueryRep fife a), Set (QueryRep fife a)) Source #
Given a set of QueryReps, extracts a common clause if possible, returning the clause, the terms from which the clause has been extracted, and the rest.
getCommonClauseCs :: Ord a => Set (QueryRep fife a) -> Maybe (QueryRep (QFlipTyp fife) a, Set (QueryRep fife a), Set (QueryRep fife a)) Source #
fixSimplifyQueryRep :: (QueryRep qtyp a -> QueryRep qtyp a) -> QueryRep qtyp a -> QueryRep qtyp a Source #
Takes any given simplifier and repeatedly applies it until it ceases to reduce the size of the query reprepresentation.
We can wrap any underying atom dype in an Ion to give it a "polarity" and add handling of "not" to our simplification tools.
Instances
| Show a => Show (Ion a) Source # | |
| Eq a => Eq (Ion a) Source # | |
| Ord a => Ord (Ion a) Source # | |
| PPQueryRep (QueryRep QAndTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| PPQueryRep (QueryRep QAtomTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
| PPQueryRep (QueryRep QOrTyp (Ion String)) Source # | |
Defined in Data.BoolSimplifier | |
simplifyIons :: (Ord a, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp (Ion a) -> QueryRep qtyp (Ion a) Source #
a /\ (b \/ ~b) /\ (c \/ d) <-> a /\ (c \/ d)
a /\ ~a /\ (b \/ c) <-> False
(a \/ ~a) /\ (b \/ ~b) <-> True (*)and duals
N.B. 0-ary \/ is False and 0-ary /\ is True
maximumByNote :: String -> (a -> a -> Ordering) -> [a] -> a Source #