Ersatz.Internal.Formula

Clauses

newtype Clause

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

Constructors

Clause

Fields

• clauseSet :: IntSet

Instances

Eq Clause

Methods

(==) :: Clause -> Clause -> Bool

(/=) :: Clause -> Clause -> Bool

Ord Clause

Methods

compare :: Clause -> Clause -> Ordering

(<) :: Clause -> Clause -> Bool

(<=) :: Clause -> Clause -> Bool

(>) :: Clause -> Clause -> Bool

(>=) :: Clause -> Clause -> Bool

max :: Clause -> Clause -> Clause

min :: Clause -> Clause -> Clause

Show Clause

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

Semigroup Clause

Methods

(<>) :: Clause -> Clause -> Clause

sconcat :: NonEmpty Clause -> Clause

stimes :: Integral b => b -> Clause -> Clause

Monoid Clause

Methods

mempty :: Clause

mappend :: Clause -> Clause -> Clause

mconcat :: [Clause] -> Clause

clauseLiterals :: Clause -> [Literal]

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

fromLiteral :: Literal -> Clause

Formulas

newtype Formula

A conjunction of clauses

Constructors

Formula

Fields

• formulaSet :: Seq Clause

Instances

Eq Formula

Methods

(==) :: Formula -> Formula -> Bool

(/=) :: Formula -> Formula -> Bool

Ord Formula

Methods

compare :: Formula -> Formula -> Ordering

(<) :: Formula -> Formula -> Bool

(<=) :: Formula -> Formula -> Bool

(>) :: Formula -> Formula -> Bool

(>=) :: Formula -> Formula -> Bool

max :: Formula -> Formula -> Formula

min :: Formula -> Formula -> Formula

Show Formula

Methods

showsPrec :: Int -> Formula -> ShowS

show :: Formula -> String

showList :: [Formula] -> ShowS

Semigroup Formula

Methods

(<>) :: Formula -> Formula -> Formula

sconcat :: NonEmpty Formula -> Formula

stimes :: Integral b => b -> Formula -> Formula

Monoid Formula

Methods

mempty :: Formula

mappend :: Formula -> Formula -> Formula

mconcat :: [Formula] -> Formula

formulaEmpty :: Formula

A formula with no clauses

formulaLiteral :: Literal -> Formula

Assert a literal

fromClause :: Clause -> Formula

formulaNot

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

Arguments

:: Literal

Output

-> [Literal]

Inputs

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

formulaOr

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

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

formulaMux

Arguments

:: Literal

Output

-> Literal

False branch

-> Literal

True branch

-> Literal

Predicate/selector

-> Formula

with redundant clauses, cf. discussion in Een and Sorensen, Translating Pseudo Boolean Constraints ..., p. 7 http://minisat.se/Papers.html

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)

formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formula

formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formula