HasCacBDD-0.2.0.0: Haskell bindings for CacBDD
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.HasCacBDD

Description

Haskell bindings for CacBDD, a BDD Package with Dynamic Cache Management.

Synopsis

Types

data Bdd Source #

The CacBDD datatype has no structure because from our perspective BDDs are just pointers.

Instances

Instances details
Arbitrary Bdd Source #

QuickCheck Arbitrary instances for BDDs

Instance details

Defined in Data.HasCacBDD

Methods

arbitrary :: Gen Bdd #

shrink :: Bdd -> [Bdd] #

Read Bdd Source # 
Instance details

Defined in Data.HasCacBDD

Show Bdd Source # 
Instance details

Defined in Data.HasCacBDD

Methods

showsPrec :: Int -> Bdd -> ShowS #

show :: Bdd -> String #

showList :: [Bdd] -> ShowS #

Eq Bdd Source # 
Instance details

Defined in Data.HasCacBDD

Methods

(==) :: Bdd -> Bdd -> Bool #

(/=) :: Bdd -> Bdd -> Bool #

type Assignment = [(Int, Bool)] Source #

An assignment of boolean values to variables/integers.

Creation of new BDDs

top :: Bdd Source #

True constant

bot :: Bdd Source #

False constant

var :: Int -> Bdd Source #

Variable, indexed by any integer from 0 to 1.000.000 FIXME: Segfaults if n is negative or out of range. Can we add a safety check without affecting performance?

Combination and Manipulation of BDDs

neg :: Bdd -> Bdd Source #

Negation

con :: Bdd -> Bdd -> Bdd Source #

Conjunction

dis :: Bdd -> Bdd -> Bdd Source #

Disjunction

imp :: Bdd -> Bdd -> Bdd Source #

Implication, via disjunction and negation. Somehow this is faster than calling LessEqual?

equ :: Bdd -> Bdd -> Bdd Source #

Equivalence aka Biimplication

xor :: Bdd -> Bdd -> Bdd Source #

Exclusive Or

conSet :: [Bdd] -> Bdd Source #

Big Conjunction

disSet :: [Bdd] -> Bdd Source #

Big Disjunction

xorSet :: [Bdd] -> Bdd Source #

Big Xor

exists_ :: Int -> Bdd -> Bdd Source #

Existential Quantification

forall_ :: Int -> Bdd -> Bdd Source #

Universal Quantification

existsSet :: [Int] -> Bdd -> Bdd Source #

Big Existential Quantification

forallSet :: [Int] -> Bdd -> Bdd Source #

Big Universal Quantification

restrict :: Bdd -> (Int, Bool) -> Bdd Source #

Restrict a single variable to a given value

restrictSet :: Bdd -> Assignment -> Bdd Source #

Restrict with a (partial) assignment

restrictLaw :: Bdd -> Bdd -> Bdd Source #

Restrict with a law. Note that the law is the second parameter!

ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd Source #

If ... then ... else ...

gfp :: (Bdd -> Bdd) -> Bdd Source #

Greatest fixpoint for a given operator.

relabel :: [(Int, Int)] -> Bdd -> Bdd Source #

Relabel variables according to the given mapping. Note that the mapping list must be sorted!

relabelFun :: (Int -> Int) -> Bdd -> Bdd Source #

Relabel variables according to the given function.

substit :: Int -> Bdd -> Bdd -> Bdd Source #

Substitute a BDD for a given variable in another BDD.

substitSimul :: [(Int, Bdd)] -> Bdd -> Bdd Source #

Simultaneous substitution of BDDs for variables. Note that this is not the same as folding substit.

Evaluation

evaluate :: Bdd -> Assignment -> Maybe Bool Source #

Evaluate a BDD given an assignment. Returns Nothing if the assignment does not cover allVarsOf b.

evaluateFun :: Bdd -> (Int -> Bool) -> Bool Source #

Evaluate a BDD given a total assignment function.

Get satisfying assignments

allSats :: Bdd -> [Assignment] Source #

Get all satisfying assignments. These will be partial, i.e. only contain (a subset of) the variables that actually occur in the BDD.

allSatsWith :: [Int] -> Bdd -> [Assignment] Source #

Get all complete assignments, given a set of all variables. In particular this will include variables not in the BDD.

satCountWith :: [Int] -> Bdd -> Int Source #

Given a set of all variables, get the number of satisfying assignments. Note that allvars must be nub'd and sorted.

anySat :: Bdd -> Maybe Assignment Source #

Get the lexicographically smallest satisfying assignment, if there is any.

anySatWith :: [Int] -> Bdd -> Maybe Assignment Source #

Given a set of all variables, get the lexicographically smallest complete satisfying assignment, if there is any.

Variables

firstVarOf :: Bdd -> Maybe Int Source #

The first variable of a given BDD, if there is one.

maxVarOf :: Bdd -> Maybe Int Source #

The maximum variable of a given BDD, if there is one.

allVarsOf :: Bdd -> [Int] Source #

All variables in a given BDD, *not* sorted, lazy.

allVarsOfSorted :: Bdd -> [Int] Source #

All variables in a given BDD, sorted, *not* lazy.

Sub-BDDs and length

thenOf :: Bdd -> Bdd Source #

Then-branch of a given BDD, setting firstVarOf to True.

elseOf :: Bdd -> Bdd Source #

Else-branch of a given BDD, setting firstVarOf to False.

subsOf :: Bdd -> [Bdd] Source #

List all node / sub-BDDs of a given BDD. This includes the root node of b itself, but omits terminal nodes.

sizeOf :: Bdd -> Int Source #

Size of the BDD, the number of non-terminal nodes.

Show and convert to trees

data BddTree Source #

A simple tree definition to show BDDs as text.

Constructors

Bot 
Top 
Var Int BddTree BddTree 

Instances

Instances details
Read BddTree Source # 
Instance details

Defined in Data.HasCacBDD

Show BddTree Source # 
Instance details

Defined in Data.HasCacBDD

Eq BddTree Source # 
Instance details

Defined in Data.HasCacBDD

Methods

(==) :: BddTree -> BddTree -> Bool #

(/=) :: BddTree -> BddTree -> Bool #

unravel :: Bdd -> BddTree Source #

Convert a BDD to a tree.

ravel :: BddTree -> Bdd Source #

Convert a tree to a BDD.

Print some debugging information

maximumvar :: Int Source #

The maximum number of variables

showInfo :: IO () Source #

Show internal statistics.