Hoogle Search
Within LTS Haskell 24.35 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
formatSpine :: Spine -> Stringepub-metadata Codec.Epub.Format.Spine Format an epub Spine structure for pretty printing
formatSubline :: String -> Maybe String -> Stringepub-metadata Codec.Epub.Format.Util No documentation available.
formulaAnd :: Literal -> [Literal] -> Formulaersatz Ersatz.Internal.Formula The boolean and operation Derivation of the Tseitin transformation:
O ≡ (A & B & C) (O → (A & B & C)) & (¬O → ¬(A & B & C)) (¬O | (A & B & C)) & (O | ¬(A & B & C)) (¬O | A) & (¬O | B) & (¬O | C) & (O | ¬A | ¬B | ¬C)
-
ersatz Ersatz.Internal.Formula A formula with no clauses
formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formulaersatz Ersatz.Internal.Formula No documentation available.
formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formulaersatz Ersatz.Internal.Formula No documentation available.
formulaLiteral :: Literal -> Formulaersatz Ersatz.Internal.Formula Assert a literal
formulaMux :: Literal -> Literal -> Literal -> Literal -> Formulaersatz Ersatz.Internal.Formula The boolean else-then-if or mux operation Derivation of the Tseitin transformation:
O ≡ (F & ¬P) | (T & P) (O → ((F & ¬P) | (T & P))) & (¬O → ¬((F & ¬P) | (T & P)))
Left hand side:O → ((F & ¬P) | (T & P)) ¬O | ((F & ¬P) | (T & P)) ¬O | ((F | T) & (F | P) & (T | ¬P) & (¬P | P)) ¬O | ((F | T) & (F | P) & (T | ¬P)) (¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P)
Right hand side:¬O → ¬((F & ¬P) | (T & P)) O | ¬((F & ¬P) | (T & P)) O | (¬(F & ¬P) & ¬(T & P)) O | ((¬F | P) & (¬T | ¬P)) (O | ¬F | P) & (O | ¬T | ¬P)
Result:(¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P) & (O | ¬F | P) & (O | ¬T | ¬P)
with redundant clauses, cf. discussion in Een and Sorensen, Translating Pseudo Boolean Constraints ..., p. 7 http://minisat.se/Papers.htmlformulaNot :: Literal -> Literal -> Formulaersatz Ersatz.Internal.Formula The boolean not operation Derivation of the Tseitin transformation:
O ≡ ¬A (O → ¬A) & (¬O → A) (¬O | ¬A) & (O | A)
formulaOr :: Literal -> [Literal] -> Formulaersatz Ersatz.Internal.Formula The boolean or operation Derivation of the Tseitin transformation:
O ≡ (A | B | C) (O → (A | B | C)) & (¬O → ¬(A | B | C)) (¬O | (A | B | C)) & (O | ¬(A | B | C)) (¬O | A | B | C) & (O | (¬A & ¬B & ¬C)) (¬O | A | B | C) & (O | ¬A) & (O | ¬B) & (O | ¬C)