Data.BoolSimplifier

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.

Documentation

data QOrTyp

We'll start with three types of formulas: disjunctions, conjunctions, and atoms

Instances

Show QOrTyp

QNot QOrTyp

PPConstQR QOrTyp

Ord a => CombineQ a QAtomTyp QOrTyp

Ord a => CombineQ a QOrTyp QAtomTyp

Ord a => CombineQ a QOrTyp QOrTyp

Ord a => CombineQ a QOrTyp QAndTyp

Ord a => CombineQ a QAndTyp QOrTyp

PPQueryRep (QueryRep QOrTyp (Ion String))

data QAndTyp

Instances

Show QAndTyp

QNot QAndTyp

PPConstQR QAndTyp

Ord a => CombineQ a QAtomTyp QAndTyp

Ord a => CombineQ a QOrTyp QAndTyp

Ord a => CombineQ a QAndTyp QAtomTyp

Ord a => CombineQ a QAndTyp QOrTyp

Ord a => CombineQ a QAndTyp QAndTyp

PPQueryRep (QueryRep QAndTyp (Ion String))

data QAtomTyp

Instances

QNot QAtomTyp

HasClause fife QAtomTyp

Ord a => CombineQ a QAtomTyp QAtomTyp

Ord a => CombineQ a QAtomTyp QOrTyp

Ord a => CombineQ a QAtomTyp QAndTyp

Ord a => CombineQ a QOrTyp QAtomTyp

Ord a => CombineQ a QAndTyp QAtomTyp

PPQueryRep (QueryRep QAtomTyp (Ion String))

type family QFlipTyp t :: *

disjunction is the dual of conjunction and vice-versa

data QueryRep qtyp a where

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 :: Ord a => a -> QueryRep QAtomTyp a

QOp :: (Show qtyp, Ord a) => Set (QueryRep QAtomTyp a) -> Set (QueryRep (QFlipTyp qtyp) a) -> QueryRep qtyp a

Instances

Eq a => Eq (QueryRep qtyp a)

Ord a => Ord (QueryRep qtyp a)

Show a => Show (QueryRep qtyp a)

PPQueryRep (QueryRep qtyp String)

PPQueryRep (QueryRep QAtomTyp (Ion String))

PPQueryRep (QueryRep QAndTyp (Ion String))

PPQueryRep (QueryRep QOrTyp (Ion String))

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

convenience constructors, not particularly smart

qAnd :: Ord a => Set (QueryRep QAtomTyp a) -> Set (QueryRep QOrTyp a) -> QueryRep QAndTyp a

class PPQueryRep a where

pretty printer class

Methods

ppQueryRep :: a -> String

Instances

PPQueryRep (QueryRep qtyp String)

PPQueryRep (QueryRep QAtomTyp (Ion String))

PPQueryRep (QueryRep QAndTyp (Ion String))

PPQueryRep (QueryRep QOrTyp (Ion 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

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))

class HasClause fife qtyp where

QueryReps can be queried for clauses within them, and clauses within them can be extracted.

Methods

hasClause :: QueryRep fife a -> QueryRep qtyp a -> Bool

stripClause :: QueryRep qtyp a -> QueryRep fife a -> QueryRep fife a

Instances

~ * (QFlipTyp fife) qtyp => HasClause fife qtyp

HasClause fife QAtomTyp

andqs :: Ord a => CombineQ a qtyp QAndTyp => [QueryRep qtyp a] -> QueryRep QAndTyp a

convenience functions

orqs :: Ord a => CombineQ a qtyp QOrTyp => [QueryRep qtyp a] -> QueryRep QOrTyp a

class CombineQ a qtyp1 qtyp2 where

smart constructors for QueryRep

Methods

andq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QAndTyp a

orq :: QueryRep qtyp1 a -> QueryRep qtyp2 a -> QueryRep QOrTyp a

Instances

Ord a => CombineQ a QAtomTyp QAtomTyp

Ord a => CombineQ a QAtomTyp QOrTyp

Ord a => CombineQ a QAtomTyp QAndTyp

Ord a => CombineQ a QOrTyp QAtomTyp

Ord a => CombineQ a QOrTyp QOrTyp

Ord a => CombineQ a QOrTyp QAndTyp

Ord a => CombineQ a QAndTyp QAtomTyp

Ord a => CombineQ a QAndTyp QOrTyp

Ord a => CombineQ a QAndTyp QAndTyp

simplifyQueryRep :: (Ord a, Show (QFlipTyp qtyp), Show (QFlipTyp (QFlipTyp qtyp)), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp a -> QueryRep qtyp a

(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))

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))

fixSimplifyQueryRep :: (QueryRep qtyp a -> QueryRep qtyp a) -> QueryRep qtyp a -> QueryRep qtyp a

Takes any given simplifier and repeatedly applies it until it ceases to reduce the size of the query reprepresentation.

data Ion a

We can wrap any underying atom dype in an Ion to give it a polarity and add handling of not to our simplification tools.

Constructors

Neg a

Pos a

Instances

Eq a => Eq (Ion a)

Ord a => Ord (Ion a)

Show a => Show (Ion a)

PPQueryRep (QueryRep QAtomTyp (Ion String))

PPQueryRep (QueryRep QAndTyp (Ion String))

PPQueryRep (QueryRep QOrTyp (Ion String))

qAtom :: Ord a => a -> QueryRep QAtomTyp (Ion a)

isEmptyQR, isConstQR :: QueryRep qtyp a -> Bool

class PPConstQR qtyp where

Methods

ppConstQR :: QueryRep qtyp a -> String

Instances

PPConstQR a

PPConstQR QAndTyp

PPConstQR QOrTyp

class QNot qtyp where

Associated Types

type QNeg qtyp

Methods

qNot :: QueryRep qtyp (Ion a) -> QueryRep (QNeg qtyp) (Ion a)

Instances

QNot QAtomTyp

QNot QAndTyp

QNot QOrTyp

simplifyIons :: (Ord a, Show (QFlipTyp qtyp), QFlipTyp (QFlipTyp qtyp) ~ qtyp) => QueryRep qtyp (Ion a) -> QueryRep qtyp (Ion a)

  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