Portability	non-portable
Stability	experimental
Maintainer	Edward Kmett <ekmett@gmail.com>
Safe Haskell	Trustworthy

Ersatz.Internal.Formula

Contents

Clauses
Formulas

Description

Synopsis

Clauses

newtype Clause Source

A disjunction of possibly negated atoms. Negated atoms are represented by negating the identifier.

Constructors

Clause
Fields clauseSet :: IntSet

Instances

Eq Clause
Ord Clause
Show Clause
Typeable Clause
Monoid Clause

clauseLiterals :: Clause -> [Literal]Source

Extract the (possibly negated) atoms referenced by a Clause.

Formulas

newtype Formula Source

A conjunction of clauses

Constructors

Formula
Fields formulaSet :: Set Clause

Instances

Eq Formula
Ord Formula
Show Formula
Typeable Formula
Monoid Formula

formulaEmpty :: Formula Source

A formula with no clauses

formulaLiteral :: Literal -> Formula Source

Assert a literal

formulaNot Source

Arguments

:: Literal	Output
-> Literal	Input
-> Formula

The boolean not operation

Derivation of the Tseitin transformation:

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

formulaAnd Source

Arguments

:: Literal	Output
-> [Literal]	Inputs
-> Formula

The boolean and operation

Derivation of the Tseitin transformation:

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

formulaOr Source

Arguments

:: Literal	Output
-> [Literal]	Inputs
-> 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)

formulaXor Source

Arguments

:: Literal	Output
-> Literal	Input
-> Literal	Input
-> Formula

The boolean xor operation

Derivation of the Tseitin transformation:

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

Left hand side:

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

Right hand side:

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

Result:

 (¬O | ¬A | ¬& (¬O | A | B)& (O | ¬A | B)& (O | A | ¬B)

formulaMux Source

Arguments

:: Literal	Output
-> Literal	False branch
-> Literal	True branch
-> Literal	Predicate/selector
-> 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 → ¬(& ¬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 → ¬(& ¬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