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

{-# LANGUAGE ForeignFunctionInterface #-}
module Data.HasCacBDD (
  -- * Types
  Bdd, Assignment,
  -- * Creation of new BDDs
  top, bot, var,
  -- * Combination and Manipulation of BDDs
  neg, con, dis, imp, equ, xor, conSet, disSet, xorSet,
  exists, forall, forallSet, existsSet,
  restrict, restrictSet, restrictLaw,
  ifthenelse, gfp, relabel, relabelFun,
  substit, substitSimul,
  -- * Evaluation
  evaluate, evaluateFun,
  -- * Get satisfying assignments
  allSats, allSatsWith, satCountWith, anySat, anySatWith,
  -- * Variables
  firstVarOf, maxVarOf, allVarsOf, allVarsOfSorted,
  -- * Sub-BDDs and length
  thenOf, elseOf, subsOf, sizeOf,
  -- * Show and convert to trees
  BddTree(..), unravel, ravel,
  -- * Print some debugging information
  maximumvar, showInfo
) where

import Control.Arrow (Arrow(first))
import Foreign.C (CInt(..))
import Foreign.Ptr (Ptr)
import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree)
import System.IO.Unsafe (unsafePerformIO)
import Data.List (nub,(\\),sort)
import Data.Maybe (fromJust)
import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf)

-- | The CacBDD datatype has no structure because
-- from our perspective BDDs are just pointers.
newtype Bdd = Bdd (ForeignPtr CacBDD)
type CacBDD = ()

-- | An assignment of boolean values to variables/integers.
type Assignment = [(Int,Bool)]

finalize :: Ptr CacBDD -> Bdd
finalize :: Ptr CacBDD -> Bdd
finalize Ptr CacBDD
ptr = ForeignPtr CacBDD -> Bdd
Bdd (forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. FinalizerPtr a -> Ptr a -> IO (ForeignPtr a)
newForeignPtr forall a. FinalizerPtr a
finalizerFree Ptr CacBDD
ptr)

finalizeMgr :: Ptr CacXBddManager -> XBddManager
finalizeMgr :: Ptr CacBDD -> XBddManager
finalizeMgr Ptr CacBDD
ptr = ForeignPtr CacBDD -> XBddManager
XBddManager (forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. FinalizerPtr a -> Ptr a -> IO (ForeignPtr a)
newForeignPtr forall a. FinalizerPtr a
finalizerFree Ptr CacBDD
ptr)

type CacXBddManager = ()
newtype XBddManager = XBddManager (ForeignPtr CacXBddManager)

type NullOp = Ptr CacBDD -> Ptr CacXBddManager -> IO (Ptr CacBDD)
type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD)
type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO (Ptr CacBDD)

foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: Word -> IO (Ptr CacBDD)
foreign import ccall unsafe "BDDNodeC.h XBDDManager_new" xBddManager_new :: CInt -> IO (Ptr CacXBddManager)
foreign import ccall unsafe "BDDNodeC.h XBDDManager_ShowInfo" xBddManager_showInfo :: Ptr CacXBddManager -> IO ()
foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddOne"  xBddManager_BddOne  :: NullOp
foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddZero" xBddManager_BddZero :: NullOp
foreign import ccall unsafe "BDDNodeC.h XBDDManager_BddVar"  xBddManager_BddVar  :: Ptr CacBDD -> Ptr CacXBddManager -> CInt -> IO (Ptr CacBDD)
foreign import ccall unsafe "BDDNodeC.h XBDDManager_Ite"     xBddManager_Ite     :: Ptr CacBDD -> Ptr CacXBddManager -> BinaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Equal"  bdd_Operator_Equal  :: Ptr CacBDD -> Ptr CacBDD -> IO Bool
foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Not"    bdd_Operator_Not    :: UnaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Or"     bdd_Operator_Or     :: BinaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Operator_And"    bdd_Operator_And    :: BinaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Operator_Xor"    bdd_Operator_Xor    :: BinaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Exist"           bdd_Exist           :: BinaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Universal"       bdd_Universal       :: BinaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Restrict"        bdd_Restrict        :: BinaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Variable"        bdd_Variable        :: Ptr CacBDD -> IO CInt
foreign import ccall unsafe "BDDNodeC.h BDD_Then"            bdd_Then            :: UnaryOp
foreign import ccall unsafe "BDDNodeC.h BDD_Else"            bdd_Else            :: UnaryOp

-- | The maximum number of variables
maximumvar :: Int
maximumvar :: Int
maximumvar = Int
1048576

manager :: XBddManager
manager :: XBddManager
manager = Ptr CacBDD -> XBddManager
finalizeMgr (forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ CInt -> IO (Ptr CacBDD)
xBddManager_new (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
maximumvar))
{-# NOINLINE manager #-}

fromManager :: NullOp -> Bdd
fromManager :: NullOp -> Bdd
fromManager NullOp
nulloperator = let (XBddManager ForeignPtr CacBDD
mptr) = XBddManager
manager in
  Ptr CacBDD -> Bdd
finalize forall a b. (a -> b) -> a -> b
$ forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$
    forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
mptr forall a b. (a -> b) -> a -> b
$ NullOp
nulloperator (forall a. IO a -> a
unsafePerformIO (Word -> IO (Ptr CacBDD)
bdd_new Word
8))
{-# NOINLINE fromManager #-}

withBDD :: UnaryOp -> Bdd -> Bdd
withBDD :: NullOp -> Bdd -> Bdd
withBDD NullOp
unioperator (Bdd ForeignPtr CacBDD
fptr) = Ptr CacBDD -> Bdd
finalize forall a b. (a -> b) -> a -> b
$ forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$
  forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr forall a b. (a -> b) -> a -> b
$ NullOp
unioperator (forall a. IO a -> a
unsafePerformIO (Word -> IO (Ptr CacBDD)
bdd_new Word
8))
{-# NOINLINE withBDD #-}

withTwoBDDs :: BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs :: BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
binoperator (Bdd ForeignPtr CacBDD
fptr1) (Bdd ForeignPtr CacBDD
fptr2) = Ptr CacBDD -> Bdd
finalize forall a b. (a -> b) -> a -> b
$ forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$
  forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr1 forall a b. (a -> b) -> a -> b
$
    forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. BinaryOp
binoperator (forall a. IO a -> a
unsafePerformIO (Word -> IO (Ptr CacBDD)
bdd_new Word
8))
{-# NOINLINE withTwoBDDs #-}

fromBDD :: (Ptr CacBDD -> IO a) -> Bdd -> a
fromBDD :: forall a. (Ptr CacBDD -> IO a) -> Bdd -> a
fromBDD Ptr CacBDD -> IO a
property (Bdd ForeignPtr CacBDD
fptr1) = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$
  forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr1 Ptr CacBDD -> IO a
property
{-# NOINLINE fromBDD #-}

fromTwoBDDs :: (Ptr CacBDD -> Ptr CacBDD -> IO a) -> Bdd -> Bdd -> a
fromTwoBDDs :: forall a. (Ptr CacBDD -> Ptr CacBDD -> IO a) -> Bdd -> Bdd -> a
fromTwoBDDs Ptr CacBDD -> Ptr CacBDD -> IO a
binproperty (Bdd ForeignPtr CacBDD
fptr1) (Bdd ForeignPtr CacBDD
fptr2) = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$
  forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr1 forall a b. (a -> b) -> a -> b
$
    forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ptr CacBDD -> Ptr CacBDD -> IO a
binproperty
{-# NOINLINE fromTwoBDDs #-}

-- | Restrict a single variable to a given value
restrict :: Bdd -> (Int,Bool) -> Bdd
restrict :: Bdd -> (Int, Bool) -> Bdd
restrict Bdd
b (Int
n,Bool
bit) = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Restrict Bdd
b (if Bool
bit then Int -> Bdd
var Int
n else Bdd -> Bdd
neg (Int -> Bdd
var Int
n))
{-# NOINLINE restrict #-}

-- | Restrict with a (partial) assignment
restrictSet :: Bdd -> Assignment -> Bdd
restrictSet :: Bdd -> Assignment -> Bdd
restrictSet Bdd
b Assignment
bits = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Restrict Bdd
b ([Bdd] -> Bdd
conSet forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Int
n,Bool
bit) -> if Bool
bit then Int -> Bdd
var Int
n else Bdd -> Bdd
neg (Int -> Bdd
var Int
n)) Assignment
bits)
{-# NOINLINE restrictSet #-}

-- | Restrict with a law. Note that the law is the second parameter!
restrictLaw :: Bdd -> Bdd -> Bdd
restrictLaw :: Bdd -> Bdd -> Bdd
restrictLaw = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Restrict
{-# NOINLINE restrictLaw #-}

-- | Existential Quantification
exists :: Int -> Bdd -> Bdd
exists :: Int -> Bdd -> Bdd
exists Int
n Bdd
b = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Exist Bdd
b (Int -> Bdd
var Int
n)
{-# NOINLINE exists #-}

-- | Universal Quantification
forall :: Int -> Bdd -> Bdd
forall :: Int -> Bdd -> Bdd
forall Int
n Bdd
b = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Universal Bdd
b (Int -> Bdd
var Int
n)
{-# NOINLINE forall #-}

-- | Big Existential Quantification
existsSet :: [Int] -> Bdd -> Bdd
existsSet :: [Int] -> Bdd -> Bdd
existsSet [Int]
ns Bdd
b = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Bdd -> Bdd
exists) Bdd
b [Int]
ns

-- | Big Universal Quantification
forallSet :: [Int] -> Bdd -> Bdd
forallSet :: [Int] -> Bdd -> Bdd
forallSet [Int]
ns Bdd
b = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Bdd -> Bdd
forall) Bdd
b [Int]
ns

-- | True constant
top :: Bdd
top :: Bdd
top = NullOp -> Bdd
fromManager NullOp
xBddManager_BddOne
{-# NOINLINE top #-}

-- | False constant
bot :: Bdd
bot :: Bdd
bot = NullOp -> Bdd
fromManager NullOp
xBddManager_BddZero
{-# NOINLINE bot #-}

-- | 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?
var :: Int -> Bdd
var :: Int -> Bdd
var Int
n = NullOp -> Bdd
fromManager (\Ptr CacBDD
bptr Ptr CacBDD
mptr -> Ptr CacBDD -> Ptr CacBDD -> CInt -> IO (Ptr CacBDD)
xBddManager_BddVar Ptr CacBDD
bptr Ptr CacBDD
mptr (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
nforall a. Num a => a -> a -> a
+Int
1)))
{-# NOINLINE var #-}

-- | If ... then ... else ...
ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd
ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (Bdd ForeignPtr CacBDD
test) (Bdd ForeignPtr CacBDD
yes) (Bdd ForeignPtr CacBDD
no) =
  let (XBddManager ForeignPtr CacBDD
mptr) = XBddManager
manager in
    Ptr CacBDD -> Bdd
finalize forall a b. (a -> b) -> a -> b
$ forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$
      forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
test (\Ptr CacBDD
t ->
        forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
yes (\Ptr CacBDD
y ->
          forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
no (\Ptr CacBDD
n ->
            forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
mptr (\Ptr CacBDD
m -> Ptr CacBDD -> Ptr CacBDD -> BinaryOp
xBddManager_Ite (forall a. IO a -> a
unsafePerformIO (Word -> IO (Ptr CacBDD)
bdd_new Word
8)) Ptr CacBDD
m Ptr CacBDD
t Ptr CacBDD
y Ptr CacBDD
n))))
{-# NOINLINE ifthenelse #-}

instance Eq Bdd where
  Bdd
b1 == :: Bdd -> Bdd -> Bool
== Bdd
b2 = Bdd -> Bdd -> Bool
same Bdd
b1 Bdd
b2

same :: Bdd -> Bdd -> Bool
same :: Bdd -> Bdd -> Bool
same = forall a. (Ptr CacBDD -> Ptr CacBDD -> IO a) -> Bdd -> Bdd -> a
fromTwoBDDs Ptr CacBDD -> Ptr CacBDD -> IO Bool
bdd_Operator_Equal
{-# NOINLINE same #-}

-- | Negation
neg :: Bdd -> Bdd
neg :: Bdd -> Bdd
neg = NullOp -> Bdd -> Bdd
withBDD NullOp
bdd_Operator_Not
{-# NOINLINE neg #-}

-- | Equivalence aka Biimplication
equ :: Bdd -> Bdd -> Bdd
equ :: Bdd -> Bdd -> Bdd
equ Bdd
b1 Bdd
b2 = Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd
imp Bdd
b1 Bdd
b2) (Bdd -> Bdd -> Bdd
imp Bdd
b2 Bdd
b1) -- ugly...
{-# NOINLINE equ #-}

-- | Implication, via disjunction and negation.
-- Somehow this is faster than calling LessEqual?
imp :: Bdd -> Bdd -> Bdd
imp :: Bdd -> Bdd -> Bdd
imp Bdd
b1 = Bdd -> Bdd -> Bdd
dis (Bdd -> Bdd
neg Bdd
b1)
{-# NOINLINE imp #-}

-- | Conjunction
con :: Bdd -> Bdd -> Bdd
con :: Bdd -> Bdd -> Bdd
con = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Operator_And
{-# NOINLINE con #-}

-- | Disjunction
dis :: Bdd -> Bdd -> Bdd
dis :: Bdd -> Bdd -> Bdd
dis = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Operator_Or
{-# NOINLINE dis #-}

-- | Exclusive Or
xor :: Bdd -> Bdd -> Bdd
xor :: Bdd -> Bdd -> Bdd
xor = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Operator_Xor
{-# NOINLINE xor #-}

-- | Big Conjunction
conSet :: [Bdd] -> Bdd
conSet :: [Bdd] -> Bdd
conSet [] = Bdd
top
conSet (Bdd
b:[Bdd]
bs) =
  if Bdd
bot forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Bdd
bforall a. a -> [a] -> [a]
:[Bdd]
bs)
    then Bdd
bot
    else forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Bdd -> Bdd -> Bdd
con Bdd
b [Bdd]
bs
{-# NOINLINE conSet #-}

-- | Big Disjunction
disSet :: [Bdd] -> Bdd
disSet :: [Bdd] -> Bdd
disSet [] = Bdd
bot
disSet (Bdd
b:[Bdd]
bs) =
  if Bdd
top forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Bdd
bforall a. a -> [a] -> [a]
:[Bdd]
bs)
    then Bdd
top
    else forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Bdd -> Bdd -> Bdd
dis Bdd
b [Bdd]
bs
{-# NOINLINE disSet #-}

-- | Big Xor
xorSet :: [Bdd] -> Bdd
xorSet :: [Bdd] -> Bdd
xorSet [] = Bdd
bot
xorSet (Bdd
b:[Bdd]
bs) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Bdd -> Bdd -> Bdd
xor Bdd
b [Bdd]
bs
{-# NOINLINE xorSet #-}

-- | Greatest fixpoint for a given operator.
gfp :: (Bdd -> Bdd) -> Bdd
gfp :: (Bdd -> Bdd) -> Bdd
gfp Bdd -> Bdd
operator = Bdd -> Bdd -> Bdd
gfpStep Bdd
top (Bdd -> Bdd
operator Bdd
top) where
  gfpStep :: Bdd -> Bdd -> Bdd
  gfpStep :: Bdd -> Bdd -> Bdd
gfpStep Bdd
current Bdd
next =
    if Bdd
current forall a. Eq a => a -> a -> Bool
== Bdd
next
      then Bdd
current
      else Bdd -> Bdd -> Bdd
gfpStep Bdd
next (Bdd -> Bdd
operator Bdd
next)

-- | Then-branch of a given BDD, setting firstVarOf to True.
thenOf :: Bdd -> Bdd
thenOf :: Bdd -> Bdd
thenOf = NullOp -> Bdd -> Bdd
withBDD NullOp
bdd_Then

-- | Else-branch of a given BDD, setting firstVarOf to False.
elseOf :: Bdd -> Bdd
elseOf :: Bdd -> Bdd
elseOf = NullOp -> Bdd -> Bdd
withBDD NullOp
bdd_Else

-- | The first variable of a given BDD, if there is one.
firstVarOf :: Bdd -> Maybe Int
firstVarOf :: Bdd -> Maybe Int
firstVarOf Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = forall a. Maybe a
Nothing
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = forall a. Maybe a
Nothing
  | Bool
otherwise = forall a. a -> Maybe a
Just (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. (Ptr CacBDD -> IO a) -> Bdd -> a
fromBDD Ptr CacBDD -> IO CInt
bdd_Variable Bdd
b) forall a. Num a => a -> a -> a
-(Int
1::Int))

-- | The maximum variable of a given BDD, if there is one.
maxVarOf ::  Bdd -> Maybe Int
maxVarOf :: Bdd -> Maybe Int
maxVarOf Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = forall a. Maybe a
Nothing
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = forall a. Maybe a
Nothing
  | Bool
otherwise = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral CInt
v forall a. Num a => a -> a -> a
- (Int
1::Int), Maybe Int
m1, Maybe Int
m2 ] where
      v :: CInt
v = forall a. (Ptr CacBDD -> IO a) -> Bdd -> a
fromBDD Ptr CacBDD -> IO CInt
bdd_Variable Bdd
b
      m1 :: Maybe Int
m1 = Bdd -> Maybe Int
maxVarOf forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
thenOf Bdd
b
      m2 :: Maybe Int
m2 = Bdd -> Maybe Int
maxVarOf forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
elseOf Bdd
b

-- | All variables in a given BDD, *not* sorted, lazy.
allVarsOf :: Bdd -> [Int]
allVarsOf :: Bdd -> [Int]
allVarsOf Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = []
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = []
  | Bool
otherwise = let (Just Int
n) = Bdd -> Maybe Int
firstVarOf Bdd
b in Int
n forall a. a -> [a] -> [a]
: forall a. Eq a => [a] -> [a]
nub (Bdd -> [Int]
allVarsOf (Bdd -> Bdd
thenOf Bdd
b) forall a. [a] -> [a] -> [a]
++ Bdd -> [Int]
allVarsOf (Bdd -> Bdd
elseOf Bdd
b))

-- | All variables in a given BDD, sorted, *not* lazy.
allVarsOfSorted :: Bdd -> [Int]
allVarsOfSorted :: Bdd -> [Int]
allVarsOfSorted = forall a. Ord a => [a] -> [a]
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> [Int]
allVarsOf

-- | List all node / sub-BDDs of a given BDD.
-- This includes the root node of b itself, but omits terminal nodes.
subsOf :: Bdd -> [Bdd]
subsOf :: Bdd -> [Bdd]
subsOf = [Bdd] -> Bdd -> [Bdd]
subsOf' [] where
  subsOf' :: [Bdd] -> Bdd -> [Bdd]
subsOf' [Bdd]
done Bdd
b
    | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = [Bdd]
done
    | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = [Bdd]
done
    | Bdd
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Bdd]
done = [Bdd]
done
    | Bool
otherwise     = let intermedDone :: [Bdd]
intermedDone = [Bdd] -> Bdd -> [Bdd]
subsOf' [Bdd]
done (Bdd -> Bdd
thenOf Bdd
b)
                       in Bdd
b forall a. a -> [a] -> [a]
: [Bdd] -> Bdd -> [Bdd]
subsOf' [Bdd]
intermedDone (Bdd -> Bdd
elseOf Bdd
b)

-- | Size of the BDD, the number of non-terminal nodes.
sizeOf :: Bdd -> Int
sizeOf :: Bdd -> Int
sizeOf = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> [Bdd]
subsOf

instance Show Bdd where
  show :: Bdd -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> BddTree
unravel

instance Read Bdd where
  readsPrec :: Int -> ReadS Bdd
readsPrec Int
k String
input = forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first BddTree -> Bdd
ravel) (forall a. Read a => Int -> ReadS a
readsPrec Int
k String
input)

-- | A simple tree definition to show BDDs as text.
data BddTree = Bot | Top | Var Int BddTree BddTree deriving (BddTree -> BddTree -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BddTree -> BddTree -> Bool
$c/= :: BddTree -> BddTree -> Bool
== :: BddTree -> BddTree -> Bool
$c== :: BddTree -> BddTree -> Bool
Eq,ReadPrec [BddTree]
ReadPrec BddTree
Int -> ReadS BddTree
ReadS [BddTree]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [BddTree]
$creadListPrec :: ReadPrec [BddTree]
readPrec :: ReadPrec BddTree
$creadPrec :: ReadPrec BddTree
readList :: ReadS [BddTree]
$creadList :: ReadS [BddTree]
readsPrec :: Int -> ReadS BddTree
$creadsPrec :: Int -> ReadS BddTree
Read,Int -> BddTree -> ShowS
[BddTree] -> ShowS
BddTree -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BddTree] -> ShowS
$cshowList :: [BddTree] -> ShowS
show :: BddTree -> String
$cshow :: BddTree -> String
showsPrec :: Int -> BddTree -> ShowS
$cshowsPrec :: Int -> BddTree -> ShowS
Show)

-- | Convert a BDD to a tree.
unravel :: Bdd -> BddTree
unravel :: Bdd -> BddTree
unravel Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = BddTree
Bot
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = BddTree
Top
  | Bool
otherwise = Int -> BddTree -> BddTree -> BddTree
Var Int
n (Bdd -> BddTree
unravel (Bdd -> Bdd
thenOf Bdd
b)) (Bdd -> BddTree
unravel (Bdd -> Bdd
elseOf Bdd
b)) where (Just Int
n) = Bdd -> Maybe Int
firstVarOf Bdd
b

-- | Convert a tree to a BDD.
ravel :: BddTree -> Bdd
ravel :: BddTree -> Bdd
ravel BddTree
Bot = Bdd
bot
ravel BddTree
Top = Bdd
top
ravel (Var Int
n BddTree
nthen BddTree
nelse) = Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (Int -> Bdd
var Int
n) (BddTree -> Bdd
ravel BddTree
nthen) (BddTree -> Bdd
ravel BddTree
nelse)

-- | Evaluate a BDD given an assignment.
-- Returns Nothing if the assignment does not cover allVarsOf b.
evaluate :: Bdd -> Assignment -> Maybe Bool
evaluate :: Bdd -> Assignment -> Maybe Bool
evaluate Bdd
b Assignment
ass =
  if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst Assignment
ass) (Bdd -> [Int]
allVarsOf Bdd
b)
    then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Bdd
top forall a. Eq a => a -> a -> Bool
== Bdd -> Assignment -> Bdd
restrictSet Bdd
b Assignment
ass
    else forall a. Maybe a
Nothing

-- | Evaluate a BDD given a total assignment function.
evaluateFun :: Bdd -> (Int -> Bool) -> Bool
evaluateFun :: Bdd -> (Int -> Bool) -> Bool
evaluateFun Bdd
b Int -> Bool
f
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = Bool
False
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = Bool
True
  | Bool
otherwise =
      let (Just Int
n) = Bdd -> Maybe Int
firstVarOf Bdd
b
      in Bdd -> (Int -> Bool) -> Bool
evaluateFun ((if Int -> Bool
f Int
n then Bdd -> Bdd
thenOf else Bdd -> Bdd
elseOf) Bdd
b) Int -> Bool
f

-- | Get all satisfying assignments. These will be partial, i.e. only
-- contain (a subset of) the variables that actually occur in the BDD.
allSats :: Bdd -> [Assignment]
allSats :: Bdd -> [Assignment]
allSats Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = []
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = [ [] ]
  | Bool
otherwise =
      [ (Int
n,Bool
True)forall a. a -> [a] -> [a]
:Assignment
rest | Assignment
rest <- Bdd -> [Assignment]
allSats (Bdd -> Bdd
thenOf Bdd
b) ] forall a. [a] -> [a] -> [a]
++ [ (Int
n,Bool
False)forall a. a -> [a] -> [a]
:Assignment
rest | Assignment
rest <- Bdd -> [Assignment]
allSats (Bdd -> Bdd
elseOf Bdd
b) ]
      where (Just Int
n) = Bdd -> Maybe Int
firstVarOf Bdd
b

-- | Get the lexicographically smallest satisfying assignment, if there is any.
anySat :: Bdd -> Maybe Assignment
anySat :: Bdd -> Maybe Assignment
anySat Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = forall a. Maybe a
Nothing
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = forall a. a -> Maybe a
Just []
  | Bool
otherwise = forall a. a -> Maybe a
Just ((Int
n,Bool
hastobetrue)forall a. a -> [a] -> [a]
:Assignment
rest) where
      hastobetrue :: Bool
hastobetrue = Bdd -> Bdd
elseOf Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot
      (Just Int
n)    = Bdd -> Maybe Int
firstVarOf Bdd
b
      (Just Assignment
rest) = if Bool
hastobetrue then Bdd -> Maybe Assignment
anySat (Bdd -> Bdd
thenOf Bdd
b) else Bdd -> Maybe Assignment
anySat (Bdd -> Bdd
elseOf Bdd
b)

-- | Given a set of all variables, complete an assignment.
completeAss :: [Int] -> Assignment -> [Assignment]
completeAss :: [Int] -> Assignment -> [Assignment]
completeAss [Int]
allvars Assignment
ass =
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall {b}. [(Int, b)] -> [Int]
addvars Assignment
ass)
    then [Assignment
ass]
    else forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Int] -> Assignment -> [Assignment]
completeAss [Int]
allvars) (forall {a}. [(a, Bool)] -> a -> [[(a, Bool)]]
extend Assignment
ass (forall a. [a] -> a
head (forall {b}. [(Int, b)] -> [Int]
addvars Assignment
ass)))
  where
    addvars :: [(Int, b)] -> [Int]
addvars [(Int, b)]
s = [Int]
allvars forall a. Eq a => [a] -> [a] -> [a]
\\ forall a. Ord a => [a] -> [a]
sort (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Int, b)]
s)
    extend :: [(a, Bool)] -> a -> [[(a, Bool)]]
extend [(a, Bool)]
s a
v = [ (a
v,Bool
False)forall a. a -> [a] -> [a]
:[(a, Bool)]
s, (a
v,Bool
True)forall a. a -> [a] -> [a]
:[(a, Bool)]
s ]

-- | Get all complete assignments, given a set of all variables.
-- In particular this will include variables not in the BDD.
allSatsWith :: [Int] -> Bdd -> [Assignment]
allSatsWith :: [Int] -> Bdd -> [Assignment]
allSatsWith [Int]
allvars Bdd
b = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Int] -> Assignment -> [Assignment]
completeAss [Int]
allvars) (Bdd -> [Assignment]
allSats Bdd
b)

-- | Given a set of all variables, get the number of satisfying assignments.
-- Note that allvars must be nub'd and sorted.
satCountWith :: [Int] -> Bdd -> Int
satCountWith :: [Int] -> Bdd -> Int
satCountWith [Int]
allvars Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = Int
2 forall a b. (Num a, Integral b) => a -> b -> a
^ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
allvars
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = Int
0
  | Bool
otherwise = (Int
2 forall a b. (Num a, Integral b) => a -> b -> a
^ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
varsjumped) forall a. Num a => a -> a -> a
* Int
posbelow where
      (Just Int
curvar) = Bdd -> Maybe Int
firstVarOf Bdd
b
      varsjumped :: [Int]
varsjumped = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> a -> Bool
< Int
curvar) [Int]
allvars
      varsleft :: [Int]
varsleft   = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> a -> Bool
> Int
curvar) [Int]
allvars
      posbelow :: Int
posbelow   = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [[Int] -> Bdd -> Int
satCountWith [Int]
varsleft (Bdd -> Bdd
branch Bdd
b) | Bdd -> Bdd
branch <- [Bdd -> Bdd
thenOf,Bdd -> Bdd
elseOf] ]

-- | Given a set of all variables, get the lexicographically smallest complete
-- satisfying assignment, if there is any.
anySatWith :: [Int] -> Bdd -> Maybe Assignment
anySatWith :: [Int] -> Bdd -> Maybe Assignment
anySatWith [Int]
allvars Bdd
b = case Bdd -> Maybe Assignment
anySat Bdd
b of
  Maybe Assignment
Nothing -> forall a. Maybe a
Nothing
  Just Assignment
partass -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ [Int] -> Assignment -> [Assignment]
completeAss [Int]
allvars Assignment
partass

-- | Relabel variables according to the given mapping.
-- Note that the mapping list must be sorted!
relabel :: [(Int,Int)] -> Bdd -> Bdd
relabel :: [(Int, Int)] -> Bdd -> Bdd
relabel [] Bdd
b = Bdd
b
relabel rel :: [(Int, Int)]
rel@((Int
n,Int
newn):[(Int, Int)]
rest) Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot = Bdd
b
  | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top = Bdd
b
  | Bool
otherwise = case forall a. Ord a => a -> a -> Ordering
compare Int
n (forall a. HasCallStack => Maybe a -> a
fromJust (Bdd -> Maybe Int
firstVarOf Bdd
b)) of
                  Ordering
LT -> [(Int, Int)] -> Bdd -> Bdd
relabel [(Int, Int)]
rest Bdd
b
                  Ordering
EQ -> Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (Int -> Bdd
var Int
newn) ([(Int, Int)] -> Bdd -> Bdd
relabel [(Int, Int)]
rest (Bdd -> Bdd
thenOf Bdd
b)) ([(Int, Int)] -> Bdd -> Bdd
relabel [(Int, Int)]
rest (Bdd -> Bdd
elseOf Bdd
b))
                  Ordering
GT -> Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (Int -> Bdd
var (forall a. HasCallStack => Maybe a -> a
fromJust (Bdd -> Maybe Int
firstVarOf Bdd
b))) ([(Int, Int)] -> Bdd -> Bdd
relabel [(Int, Int)]
rel (Bdd -> Bdd
thenOf Bdd
b)) ([(Int, Int)] -> Bdd -> Bdd
relabel [(Int, Int)]
rel (Bdd -> Bdd
elseOf Bdd
b))

-- | Relabel variables according to the given function.
relabelFun :: (Int -> Int) -> Bdd -> Bdd
relabelFun :: (Int -> Int) -> Bdd -> Bdd
relabelFun Int -> Int
f Bdd
b = case Bdd -> Maybe Int
firstVarOf Bdd
b of
  Maybe Int
Nothing -> Bdd
b
  Just Int
m  -> Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (Int -> Bdd
var (Int -> Int
f Int
m)) ((Int -> Int) -> Bdd -> Bdd
relabelFun Int -> Int
f (Bdd -> Bdd
thenOf Bdd
b)) ((Int -> Int) -> Bdd -> Bdd
relabelFun Int -> Int
f (Bdd -> Bdd
elseOf Bdd
b))

-- | Substitute a BDD for a given variable in another BDD.
substit :: Int -> Bdd -> Bdd -> Bdd
substit :: Int -> Bdd -> Bdd -> Bdd
substit Int
n Bdd
psi Bdd
b =
  case Bdd -> Maybe Int
firstVarOf Bdd
b of
    Maybe Int
Nothing -> Bdd
b
    Just Int
k  -> case forall a. Ord a => a -> a -> Ordering
compare Int
n Int
k of
      Ordering
LT -> Bdd
b
      Ordering
EQ -> Bdd -> Bdd -> Bdd -> Bdd
ifthenelse Bdd
psi (Bdd -> Bdd
thenOf Bdd
b) (Bdd -> Bdd
elseOf Bdd
b)
      Ordering
GT -> Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (Int -> Bdd
var Int
k) (Int -> Bdd -> Bdd -> Bdd
substit Int
n Bdd
psi (Bdd -> Bdd
thenOf Bdd
b)) (Int -> Bdd -> Bdd -> Bdd
substit Int
n Bdd
psi (Bdd -> Bdd
elseOf Bdd
b))

-- | Simultaneous substitution of BDDs for variables.
-- Note that this is not the same as folding `substit`.
substitSimul :: [(Int,Bdd)] -> Bdd -> Bdd
substitSimul :: [(Int, Bdd)] -> Bdd -> Bdd
substitSimul []    Bdd
b = Bdd
b
substitSimul [(Int, Bdd)]
repls Bdd
b =
  case Bdd -> Maybe Int
firstVarOf Bdd
b of
    Maybe Int
Nothing -> Bdd
b
    Just Int
k  -> case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
k [(Int, Bdd)]
repls of
      Maybe Bdd
Nothing  -> Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (Int -> Bdd
var Int
k) ([(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
repls forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
thenOf Bdd
b) ([(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
repls forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
elseOf Bdd
b)
      Just Bdd
psi -> Bdd -> Bdd -> Bdd -> Bdd
ifthenelse Bdd
psi     ([(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
repls forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
thenOf Bdd
b) ([(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
repls forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
elseOf Bdd
b)

-- | Show internal statistics.
showInfo :: IO ()
showInfo :: IO CacBDD
showInfo = forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
mptr Ptr CacBDD -> IO CacBDD
xBddManager_showInfo where (XBddManager ForeignPtr CacBDD
mptr) = XBddManager
manager

-- | QuickCheck Arbitrary instances for BDDs
instance Arbitrary Bdd where
  arbitrary :: Gen Bdd
arbitrary = forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen Bdd
randombdd
  shrink :: Bdd -> [Bdd]
shrink Bdd
b | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
top  = []
           | Bdd
b forall a. Eq a => a -> a -> Bool
== Bdd
bot  = []
           | Bool
otherwise = [Bdd -> Bdd
thenOf Bdd
b, Bdd -> Bdd
elseOf Bdd
b]

randomvarnumber :: Gen Int
randomvarnumber :: Gen Int
randomvarnumber = forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
100)

randombdd ::  Int -> Gen Bdd
randombdd :: Int -> Gen Bdd
randombdd Int
0 = forall a. [Gen a] -> Gen a
oneof
  [ forall (f :: * -> *) a. Applicative f => a -> f a
pure Bdd
top
  , forall (f :: * -> *) a. Applicative f => a -> f a
pure Bdd
bot
  , Int -> Bdd
var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
randomvarnumber
  ]
randombdd Int
n = forall a. [Gen a] -> Gen a
oneof
  [ Int -> Bdd
var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
randomvarnumber
  , Bdd -> Bdd
neg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bdd
smallerbdd
  , Bdd -> Bdd -> Bdd
con forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bdd
smallerbdd forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  , Bdd -> Bdd -> Bdd
dis forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bdd
smallerbdd forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  , Bdd -> Bdd -> Bdd
imp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bdd
smallerbdd forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  , Bdd -> Bdd -> Bdd
equ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bdd
smallerbdd forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  , Bdd -> Bdd -> Bdd
xor forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bdd
smallerbdd forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  , Int -> Bdd -> Bdd
exists forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
randomvarnumber forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  , [Int] -> Bdd -> Bdd
existsSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Gen a -> Gen [a]
listOf Gen Int
randomvarnumber forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  , Int -> Bdd -> Bdd
forall forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
randomvarnumber forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  , [Int] -> Bdd -> Bdd
forallSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Gen a -> Gen [a]
listOf Gen Int
randomvarnumber forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bdd
smallerbdd
  ]
  where
    smallerbdd :: Gen Bdd
smallerbdd = Int -> Gen Bdd
randombdd (Int
n forall a. Integral a => a -> a -> a
`div` Int
2)