Safe Haskell	None
Language	GHC2024

Circuit.Logics.Prop

Description

Classical propositional formulas and evaluation.

The formula AST is the "syntax"; Bool (and other Boolean carriers) are compile targets for evalProp.

Synopsis

Documentation

Propositional formula over variable names v.

Constructors

Instances details

Functor Prop Source #
Instance details Defined in Circuit.Logics.Prop Methods fmap :: (a -> b) -> Prop a -> Prop b # (<$) :: a -> Prop b -> Prop a #
Eq v => Eq (Prop v) Source #
Instance details Defined in Circuit.Logics.Prop Methods (==) :: Prop v -> Prop v -> Bool # (/=) :: Prop v -> Prop v -> Bool #
Ord v => Ord (Prop v) Source #
Instance details Defined in Circuit.Logics.Prop Methods compare :: Prop v -> Prop v -> Ordering # (<) :: Prop v -> Prop v -> Bool # (<=) :: Prop v -> Prop v -> Bool # (>) :: Prop v -> Prop v -> Bool # (>=) :: Prop v -> Prop v -> Bool # max :: Prop v -> Prop v -> Prop v # min :: Prop v -> Prop v -> Prop v #
Read v => Read (Prop v) Source #
Instance details Defined in Circuit.Logics.Prop Methods readsPrec :: Int -> ReadS (Prop v) # readList :: ReadS [Prop v] # readPrec :: ReadPrec (Prop v) # readListPrec :: ReadPrec [Prop v] #
Show v => Show (Prop v) Source #
Instance details Defined in Circuit.Logics.Prop Methods showsPrec :: Int -> Prop v -> ShowS # show :: Prop v -> String # showList :: [Prop v] -> ShowS #

Evaluate a formula given a valuation into a complemented Heyting algebra.

Three-valued eval: atoms may be unknown; connectives use H3 tables.

Not on H3 uses the Heyting-style pseudo-complement a ==> HFalse.

Cheap structural simplify (constants only).