Safe Haskell | Unsafe |
---|---|

Language | Haskell98 |

This module contains an efficient representation of algebraic boolean formulas.

## Synopsis

- mapOfSet :: Ord a => Set a -> Map a Int
- setOfMap :: Ord a => Map a Int -> Set a
- split_even :: [a] -> ([a], [a])
- type Exp = Set IntSet
- listOfExp :: Exp -> [[Int]]
- expOfList :: [[Int]] -> Exp
- exp_and :: Exp -> Exp -> Exp
- exp_xor :: Exp -> Exp -> Exp
- exp_false :: Exp
- exp_true :: Exp
- exp_not :: Exp -> Exp
- exp_var :: Int -> Exp
- vars_of_exp :: Exp -> [Int]
- exp_eval :: Exp -> Map Int Bool -> Bool
- valuations_of_vars :: [Int] -> [Map Int Bool]
- truth_table_of_exp :: [Int] -> Exp -> [Bool]
- exp_of_truth_table :: Int -> [Bool] -> Exp

# Auxiliary functions

split_even :: [a] -> ([a], [a]) Source #

Split a list in the middle.

# Expressions

type Exp = Set IntSet Source #

The type of algebraic boolean expressions.

We represent boolean expressions using "and" and "xor" as the
primitive connectives. Equivalently, we can regard booleans as the
elements of the two-element field *F*_{2}, with operations "*"
(times) and "+" (plus).

An algebraic expression
`x1*x2*x3 + y1*y2*y3 + z1*z2`

is encoded as
`{{x1,x2,x3},{y1,y2,y3},{z1,z2}}`

.

In particular,
`{} == False == 0`

and
`{{}} == True == 1`

.

# Properties of expressions

The important property of expressions is that two formulas have the same truth table iff they are syntactically equal. This makes the equality test of wires theoretically straightforward.

## Truth tables

A *valuation* on a set of variables is a map from variables to
booleans. This can be thought of as a row in a truth table. A
*truth table* is a map from valuations to booleans, but we just
represent this as a list of booleans, listed in lexicographically
increasing order of valuations.

vars_of_exp :: Exp -> [Int] Source #

Get the variables used in an expression.

exp_eval :: Exp -> Map Int Bool -> Bool Source #

Evaluate the expression with respect to the given valuation. A
*valuation* is a map from variables to booleans, i.e., a row in a
truth table.

valuations_of_vars :: [Int] -> [Map Int Bool] Source #

Construct the list of all 2^{n} valuations for a given
list of *n* variables.

truth_table_of_exp :: [Int] -> Exp -> [Bool] Source #

Build the truth table for the given expression, on the given list of variables. The truth table is returned as a list of booleans in lexicographic order of valuations. For example, if

1 2 | exp F F | f1 F T | f2 T F | f3 T T | f4

then the output of the function is `[f1,f2,f3,f4]`

.

exp_of_truth_table :: Int -> [Bool] -> Exp Source #

Return an expression realizing the given truth table. Uses variables starting with the given number.