Hoogle Search

Within LTS Haskell 24.48 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

  1. formulaMux :: Literal -> Literal -> Literal -> Literal -> Formula

    ersatz 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.html

  2. formulaNot :: Literal -> Literal -> Formula

    ersatz Ersatz.Internal.Formula

    The boolean not operation Derivation of the Tseitin transformation: 

    O ≡ ¬A
(O → ¬A) & (¬O → A)
(¬O | ¬A) & (O | A)

  3. formulaOr :: Literal -> [Literal] -> Formula

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

  4. formulaSet :: Formula -> Seq Clause

    ersatz Ersatz.Internal.Formula

    No documentation available.

  5. formulaXor :: Literal -> Literal -> Literal -> Formula

    ersatz Ersatz.Internal.Formula

    The boolean xor operation Derivation of the Tseitin transformation: 

    O ≡ A ⊕ B
O ≡ ((¬A & B) | (A & ¬B))
(O → ((¬A & B) | (A & ¬B))) & (¬O → ¬((¬A & B) | (A & ¬B)))
    Left hand side: 
    O → ((¬A & B) | (A & ¬B))
¬O | ((¬A & B) | (A & ¬B))
¬O | ((¬A | A) & (¬A | ¬B) & (A | B) & (¬B | B))
¬O | ((¬A | ¬B) & (A | B))
(¬O | ¬A | ¬B) & (¬O | A | B)
    Right hand side: 
    ¬O → ¬((¬A & B) | (A & ¬B))
O | ¬((¬A & B) | (A & ¬B))
O | (¬(¬A & B) & ¬(A & ¬B))
O | ((A | ¬B) & (¬A | B))
(O | ¬A | B) & (O | A | ¬B)
    Result: 
    (¬O | ¬A | ¬B) & (¬O | A | B) & (O | ¬A | B) & (O | A | ¬B)

  6. formula :: HasSAT s => Lens' s Formula

    ersatz Ersatz.Problem

    No documentation available.

  7. forall_ :: (Variable a, MonadQSAT s m) => m a

    ersatz Ersatz.Variable

    No documentation available.

  8. forkIOWithThrowToParent :: IO () -> IO ThreadId

    faktory Faktory.Prelude

    No documentation available.

  9. forward :: Sign

    fftw-ffi Numeric.FFTW.FFI

    No documentation available.

  10. forMonoid :: Monoid i => Args i i

    fold-debounce-conduit Data.Conduit.FoldDebounce

    Args for monoids. Input events are appended to the tail.

Page 162 of many | Previous | Next