PAKCS
Exported names: Imported modules:

Module Dimacs.Build

This module defines some operation to support the construction of Boolean formulas.

Author: Sven Hueser

Version: September 2017

Summary of exported operations:

va :: Int -> Boolean   
A Boolean variable with an index.
no :: Boolean -> Boolean   
Boolean negation.
nv :: Int -> Boolean   
Negated variable with an index.
(./\) :: Boolean -> Boolean -> Boolean   
Conjunction.
(.\/) :: Boolean -> Boolean -> Boolean   
Disjunction.
xor :: Boolean -> Boolean -> Boolean   
Exclusive or.
nnf :: Boolean -> Boolean   
cnf :: Boolean -> Boolean   
dist :: Boolean -> Boolean -> Boolean   
flatten :: Boolean -> Boolean   
flattenAnd :: [Boolean] -> [Boolean]   
flattenOr :: [Boolean] -> [Boolean]   
nubB :: Boolean -> Boolean   
toCNF :: Boolean -> Boolean   
filterTauts :: Boolean -> Boolean   
isTaut :: Boolean -> Bool   

Exported operations:

va :: Int -> Boolean   

A Boolean variable with an index. Note that the index should be a positive number.

Further infos:
  • solution complete, i.e., able to compute all solutions

no :: Boolean -> Boolean   

Boolean negation.

Further infos:
  • solution complete, i.e., able to compute all solutions

nv :: Int -> Boolean   

Negated variable with an index. Note that the index should be a positive number.

(./\) :: Boolean -> Boolean -> Boolean   

Conjunction.

Further infos:
  • defined as right-associative infix operator with precedence 3

(.\/) :: Boolean -> Boolean -> Boolean   

Disjunction.

Further infos:
  • defined as right-associative infix operator with precedence 2

xor :: Boolean -> Boolean -> Boolean   

Exclusive or.

nnf :: Boolean -> Boolean   

cnf :: Boolean -> Boolean   

dist :: Boolean -> Boolean -> Boolean   

flatten :: Boolean -> Boolean   

flattenAnd :: [Boolean] -> [Boolean]   

flattenOr :: [Boolean] -> [Boolean]   

nubB :: Boolean -> Boolean   

toCNF :: Boolean -> Boolean   

isTaut :: Boolean -> Bool