-- | 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 Foreign.C
import Foreign.Ptr (Ptr)
import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree)
import System.IO.Unsafe
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 (IO (ForeignPtr CacBDD) -> ForeignPtr CacBDD
forall a. IO a -> a
unsafePerformIO (IO (ForeignPtr CacBDD) -> ForeignPtr CacBDD)
-> IO (ForeignPtr CacBDD) -> ForeignPtr CacBDD
forall a b. (a -> b) -> a -> b
$ FinalizerPtr CacBDD -> Ptr CacBDD -> IO (ForeignPtr CacBDD)
forall a. FinalizerPtr a -> Ptr a -> IO (ForeignPtr a)
newForeignPtr FinalizerPtr CacBDD
forall a. FinalizerPtr a
finalizerFree Ptr CacBDD
ptr)

finalizeMgr :: Ptr CacXBddManager -> XBddManager
finalizeMgr :: Ptr CacBDD -> XBddManager
finalizeMgr Ptr CacBDD
ptr = ForeignPtr CacBDD -> XBddManager
XBddManager (IO (ForeignPtr CacBDD) -> ForeignPtr CacBDD
forall a. IO a -> a
unsafePerformIO (IO (ForeignPtr CacBDD) -> ForeignPtr CacBDD)
-> IO (ForeignPtr CacBDD) -> ForeignPtr CacBDD
forall a b. (a -> b) -> a -> b
$ FinalizerPtr CacBDD -> Ptr CacBDD -> IO (ForeignPtr CacBDD)
forall a. FinalizerPtr a -> Ptr a -> IO (ForeignPtr a)
newForeignPtr FinalizerPtr CacBDD
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 (IO (Ptr CacBDD) -> Ptr CacBDD
forall a. IO a -> a
unsafePerformIO (IO (Ptr CacBDD) -> Ptr CacBDD) -> IO (Ptr CacBDD) -> Ptr CacBDD
forall a b. (a -> b) -> a -> b
$ CInt -> IO (Ptr CacBDD)
xBddManager_new (Int -> CInt
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 (Ptr CacBDD -> Bdd) -> Ptr CacBDD -> Bdd
forall a b. (a -> b) -> a -> b
$ IO (Ptr CacBDD) -> Ptr CacBDD
forall a. IO a -> a
unsafePerformIO (IO (Ptr CacBDD) -> Ptr CacBDD) -> IO (Ptr CacBDD) -> Ptr CacBDD
forall a b. (a -> b) -> a -> b
$
    ForeignPtr CacBDD
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
mptr ((Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD))
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. (a -> b) -> a -> b
$ NullOp
nulloperator (IO (Ptr CacBDD) -> Ptr CacBDD
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 (Ptr CacBDD -> Bdd) -> Ptr CacBDD -> Bdd
forall a b. (a -> b) -> a -> b
$ IO (Ptr CacBDD) -> Ptr CacBDD
forall a. IO a -> a
unsafePerformIO (IO (Ptr CacBDD) -> Ptr CacBDD) -> IO (Ptr CacBDD) -> Ptr CacBDD
forall a b. (a -> b) -> a -> b
$
  ForeignPtr CacBDD
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr ((Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD))
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. (a -> b) -> a -> b
$ NullOp
unioperator (IO (Ptr CacBDD) -> Ptr CacBDD
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 (Ptr CacBDD -> Bdd) -> Ptr CacBDD -> Bdd
forall a b. (a -> b) -> a -> b
$ IO (Ptr CacBDD) -> Ptr CacBDD
forall a. IO a -> a
unsafePerformIO (IO (Ptr CacBDD) -> Ptr CacBDD) -> IO (Ptr CacBDD) -> Ptr CacBDD
forall a b. (a -> b) -> a -> b
$
  ForeignPtr CacBDD
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr1 ((Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD))
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. (a -> b) -> a -> b
$
    ForeignPtr CacBDD
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr2 ((Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD))
-> NullOp -> Ptr CacBDD -> IO (Ptr CacBDD)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BinaryOp
binoperator (IO (Ptr CacBDD) -> Ptr CacBDD
forall a. IO a -> a
unsafePerformIO (Word -> IO (Ptr CacBDD)
bdd_new Word
8))
{-# NOINLINE withTwoBDDs #-}

fromBDD :: (Ptr CacBDD -> IO a) -> Bdd -> a
fromBDD :: (Ptr CacBDD -> IO a) -> Bdd -> a
fromBDD Ptr CacBDD -> IO a
property (Bdd ForeignPtr CacBDD
fptr1) = IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$
  ForeignPtr CacBDD -> (Ptr CacBDD -> IO a) -> IO a
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 :: (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) = IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$
  ForeignPtr CacBDD -> (Ptr CacBDD -> IO a) -> IO a
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr1 ((Ptr CacBDD -> IO a) -> IO a) -> (Ptr CacBDD -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$
    ForeignPtr CacBDD -> (Ptr CacBDD -> IO a) -> IO a
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr2 ((Ptr CacBDD -> IO a) -> IO a)
-> (Ptr CacBDD -> Ptr CacBDD -> IO a) -> Ptr CacBDD -> IO a
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 ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$ ((Int, Bool) -> Bdd) -> Assignment -> [Bdd]
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 = (Bdd -> Int -> Bdd) -> Bdd -> [Int] -> Bdd
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Int -> Bdd -> Bdd) -> Bdd -> Int -> Bdd
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 = (Bdd -> Int -> Bdd) -> Bdd -> [Int] -> Bdd
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Int -> Bdd -> Bdd) -> Bdd -> Int -> Bdd
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 (Int -> CInt
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
nInt -> Int -> Int
forall 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 (Ptr CacBDD -> Bdd) -> Ptr CacBDD -> Bdd
forall a b. (a -> b) -> a -> b
$ IO (Ptr CacBDD) -> Ptr CacBDD
forall a. IO a -> a
unsafePerformIO (IO (Ptr CacBDD) -> Ptr CacBDD) -> IO (Ptr CacBDD) -> Ptr CacBDD
forall a b. (a -> b) -> a -> b
$
      ForeignPtr CacBDD
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
test (\Ptr CacBDD
t ->
        ForeignPtr CacBDD
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
yes (\Ptr CacBDD
y ->
          ForeignPtr CacBDD
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
no (\Ptr CacBDD
n ->
            ForeignPtr CacBDD
-> (Ptr CacBDD -> IO (Ptr CacBDD)) -> IO (Ptr CacBDD)
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 (IO (Ptr CacBDD) -> Ptr CacBDD
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 = (Ptr CacBDD -> Ptr CacBDD -> IO Bool) -> Bdd -> Bdd -> Bool
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 Bdd -> [Bdd] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Bdd
bBdd -> [Bdd] -> [Bdd]
forall a. a -> [a] -> [a]
:[Bdd]
bs)
    then Bdd
bot
    else (Bdd -> Bdd -> Bdd) -> Bdd -> [Bdd] -> Bdd
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 Bdd -> [Bdd] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Bdd
bBdd -> [Bdd] -> [Bdd]
forall a. a -> [a] -> [a]
:[Bdd]
bs)
    then Bdd
top
    else (Bdd -> Bdd -> Bdd) -> Bdd -> [Bdd] -> Bdd
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) = (Bdd -> Bdd -> Bdd) -> Bdd -> [Bdd] -> Bdd
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 Bdd -> Bdd -> Bool
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = Maybe Int
forall a. Maybe a
Nothing
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = Maybe Int
forall a. Maybe a
Nothing
  | Bool
otherwise = Int -> Maybe Int
forall a. a -> Maybe a
Just (CInt -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ((Ptr CacBDD -> IO CInt) -> Bdd -> CInt
forall a. (Ptr CacBDD -> IO a) -> Bdd -> a
fromBDD Ptr CacBDD -> IO CInt
bdd_Variable Bdd
b) Int -> Int -> Int
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = Maybe Int
forall a. Maybe a
Nothing
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = Maybe Int
forall a. Maybe a
Nothing
  | Bool
otherwise = [Maybe Int] -> Maybe Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ CInt -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral CInt
v Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
1::Int), Maybe Int
m1, Maybe Int
m2 ] where
      v :: CInt
v = (Ptr CacBDD -> IO CInt) -> Bdd -> CInt
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 (Bdd -> Maybe Int) -> Bdd -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
thenOf Bdd
b
      m2 :: Maybe Int
m2 = Bdd -> Maybe Int
maxVarOf (Bdd -> Maybe Int) -> Bdd -> Maybe Int
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = []
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = []
  | Bool
otherwise = let (Just Int
n) = Bdd -> Maybe Int
firstVarOf Bdd
b in Int
n Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub (Bdd -> [Int]
allVarsOf (Bdd -> Bdd
thenOf Bdd
b) [Int] -> [Int] -> [Int]
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 = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Int]) -> (Bdd -> [Int]) -> Bdd -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> [Int]
allVarsOf

-- | List all the sub-BDDs of a given BDD.
subsOf :: Bdd -> [Bdd]
subsOf :: Bdd -> [Bdd]
subsOf Bdd
b
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = []
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = []
  | Bool
otherwise = [Bdd] -> [Bdd]
forall a. Eq a => [a] -> [a]
nub ([Bdd] -> [Bdd]) -> [Bdd] -> [Bdd]
forall a b. (a -> b) -> a -> b
$ Bdd
b Bdd -> [Bdd] -> [Bdd]
forall a. a -> [a] -> [a]
: (Bdd -> [Bdd]
subsOf (Bdd -> Bdd
thenOf Bdd
b) [Bdd] -> [Bdd] -> [Bdd]
forall a. [a] -> [a] -> [a]
++ Bdd -> [Bdd]
subsOf (Bdd -> Bdd
elseOf Bdd
b))

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

instance Show Bdd where
  show :: Bdd -> String
show = BddTree -> String
forall a. Show a => a -> String
show (BddTree -> String) -> (Bdd -> BddTree) -> Bdd -> String
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 = ((BddTree, String) -> (Bdd, String))
-> [(BddTree, String)] -> [(Bdd, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\(BddTree
a,String
s) -> (BddTree -> Bdd
ravel BddTree
a, String
s)) (Int -> ReadS BddTree
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
(BddTree -> BddTree -> Bool)
-> (BddTree -> BddTree -> Bool) -> Eq BddTree
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]
(Int -> ReadS BddTree)
-> ReadS [BddTree]
-> ReadPrec BddTree
-> ReadPrec [BddTree]
-> Read 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
(Int -> BddTree -> ShowS)
-> (BddTree -> String) -> ([BddTree] -> ShowS) -> Show BddTree
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = BddTree
Bot
  | Bdd
b Bdd -> Bdd -> Bool
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 (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Int, Bool) -> Int) -> Assignment -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Bool) -> Int
forall a b. (a, b) -> a
fst Assignment
ass) (Bdd -> [Int]
allVarsOf Bdd
b)
    then Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bdd
top Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd -> Assignment -> Bdd
restrictSet Bdd
b Assignment
ass
    else Maybe Bool
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = Bool
False
  | Bdd
b Bdd -> Bdd -> Bool
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = []
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = [ [] ]
  | Bool
otherwise =
      [ (Int
n,Bool
True)(Int, Bool) -> Assignment -> Assignment
forall a. a -> [a] -> [a]
:Assignment
rest | Assignment
rest <- Bdd -> [Assignment]
allSats (Bdd -> Bdd
thenOf Bdd
b) ] [Assignment] -> [Assignment] -> [Assignment]
forall a. [a] -> [a] -> [a]
++ [ (Int
n,Bool
False)(Int, Bool) -> Assignment -> Assignment
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = Maybe Assignment
forall a. Maybe a
Nothing
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = Assignment -> Maybe Assignment
forall a. a -> Maybe a
Just []
  | Bool
otherwise = Assignment -> Maybe Assignment
forall a. a -> Maybe a
Just ((Int
n,Bool
hastobetrue)(Int, Bool) -> Assignment -> Assignment
forall a. a -> [a] -> [a]
:Assignment
rest) where
      hastobetrue :: Bool
hastobetrue = Bdd -> Bdd
elseOf Bdd
b Bdd -> Bdd -> Bool
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 [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Assignment -> [Int]
forall b. [(Int, b)] -> [Int]
addvars Assignment
ass)
    then [Assignment
ass]
    else (Assignment -> [Assignment]) -> [Assignment] -> [Assignment]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Int] -> Assignment -> [Assignment]
completeAss [Int]
allvars) (Assignment -> Int -> [Assignment]
forall a. [(a, Bool)] -> a -> [[(a, Bool)]]
extend Assignment
ass ([Int] -> Int
forall a. [a] -> a
head (Assignment -> [Int]
forall b. [(Int, b)] -> [Int]
addvars Assignment
ass)))
  where
    addvars :: [(Int, b)] -> [Int]
addvars [(Int, b)]
s = [Int]
allvars [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort (((Int, b) -> Int) -> [(Int, b)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, b) -> Int
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)(a, Bool) -> [(a, Bool)] -> [(a, Bool)]
forall a. a -> [a] -> [a]
:[(a, Bool)]
s, (a
v,Bool
True)(a, Bool) -> [(a, Bool)] -> [(a, Bool)]
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 = (Assignment -> [Assignment]) -> [Assignment] -> [Assignment]
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = Int
2 Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^ [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
allvars
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = Int
0
  | Bool
otherwise = (Int
2 Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^ [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
varsjumped) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
posbelow where
      (Just Int
curvar) = Bdd -> Maybe Int
firstVarOf Bdd
b
      varsjumped :: [Int]
varsjumped = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
curvar) [Int]
allvars
      varsleft :: [Int]
varsleft   = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
curvar) [Int]
allvars
      posbelow :: Int
posbelow   = [Int] -> Int
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 -> Maybe Assignment
forall a. Maybe a
Nothing
  Just Assignment
partass -> Assignment -> Maybe Assignment
forall a. a -> Maybe a
Just (Assignment -> Maybe Assignment) -> Assignment -> Maybe Assignment
forall a b. (a -> b) -> a -> b
$ [Assignment] -> Assignment
forall a. [a] -> a
head ([Assignment] -> Assignment) -> [Assignment] -> Assignment
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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = Bdd
b
  | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = Bdd
b
  | Bool
otherwise = case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n (Maybe Int -> Int
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 (Maybe Int -> Int
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 Int -> Int -> Ordering
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 Int -> [(Int, Bdd)] -> Maybe Bdd
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 (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
thenOf Bdd
b) ([(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
repls (Bdd -> Bdd) -> Bdd -> Bdd
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 (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
thenOf Bdd
b) ([(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
repls (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
elseOf Bdd
b)

-- | Show internal statistics.
showInfo :: IO ()
showInfo :: IO CacBDD
showInfo = ForeignPtr CacBDD -> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
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 = (Int -> Gen Bdd) -> Gen Bdd
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen Bdd
randombdd
  shrink :: Bdd -> [Bdd]
shrink Bdd
b | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top  = []
           | Bdd
b Bdd -> Bdd -> Bool
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 = (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
100)

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