-- | 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_, existsSet, forallSet,
  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,
  -- * Variable Orderings
  optimalOrder,
  -- * 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.Function (on)
import Data.List ((\\), minimumBy, nub, permutations, 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 ()
type UnaryOp = Ptr CacBDD -> Ptr CacBDD -> IO ()
type BinaryOp = Ptr CacBDD -> Ptr CacBDD -> Ptr CacBDD -> IO ()

foreign import ccall unsafe "BDDNodeC.h BDD_new" bdd_new :: 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 ()
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
$ do
    Ptr CacBDD
b <- IO (Ptr CacBDD)
bdd_new
    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) -> IO CacBDD)
-> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. (a -> b) -> a -> b
$ NullOp
nulloperator Ptr CacBDD
b
    Ptr CacBDD -> IO (Ptr CacBDD)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Ptr CacBDD
b
{-# 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
$ do
  Ptr CacBDD
b <- IO (Ptr CacBDD)
bdd_new
  ForeignPtr CacBDD -> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr ((Ptr CacBDD -> IO CacBDD) -> IO CacBDD)
-> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. (a -> b) -> a -> b
$ NullOp
unioperator Ptr CacBDD
b
  Ptr CacBDD -> IO (Ptr CacBDD)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Ptr CacBDD
b
{-# 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
$ do
  Ptr CacBDD
b <- IO (Ptr CacBDD)
bdd_new
  ForeignPtr CacBDD -> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr1 ((Ptr CacBDD -> IO CacBDD) -> IO CacBDD)
-> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. (a -> b) -> a -> b
$
    ForeignPtr CacBDD -> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
fptr2 ((Ptr CacBDD -> IO CacBDD) -> IO CacBDD)
-> NullOp -> Ptr CacBDD -> IO CacBDD
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BinaryOp
binoperator Ptr CacBDD
b
  Ptr CacBDD -> IO (Ptr CacBDD)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Ptr CacBDD
b
{-# 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) = 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 :: 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) = 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 b a. (b -> a -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 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
$ do
      Ptr CacBDD
b <- IO (Ptr CacBDD)
bdd_new
      ForeignPtr CacBDD -> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
test (\Ptr CacBDD
t ->
        ForeignPtr CacBDD -> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
yes (\Ptr CacBDD
y ->
          ForeignPtr CacBDD -> (Ptr CacBDD -> IO CacBDD) -> IO CacBDD
forall a b. ForeignPtr a -> (Ptr a -> IO b) -> IO b
withForeignPtr ForeignPtr CacBDD
no (\Ptr CacBDD
n ->
            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
m -> Ptr CacBDD -> Ptr CacBDD -> BinaryOp
xBddManager_Ite Ptr CacBDD
b Ptr CacBDD
m Ptr CacBDD
t Ptr CacBDD
y Ptr CacBDD
n))))
      Ptr CacBDD -> IO (Ptr CacBDD)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Ptr CacBDD
b
{-# 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 a. Eq a => a -> [a] -> 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 b a. (b -> a -> b) -> b -> [a] -> b
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 a. Eq a => a -> [a] -> 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 b a. (b -> a -> b) -> b -> [a] -> b
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 b a. (b -> a -> b) -> b -> [a] -> b
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 a. Ord a => [a] -> a
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 n :: Int
n = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (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 node / sub-BDDs of a given BDD.
-- This includes the root node, 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 Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = [Bdd]
done
    | Bdd
b Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = [Bdd]
done
    | Bdd
b Bdd -> [Bdd] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 Bdd -> [Bdd] -> [Bdd]
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 = [Bdd] -> Int
forall a. [a] -> 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 -> Bdd) -> (BddTree, String) -> (Bdd, String)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first BddTree -> Bdd
ravel) (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
$c== :: BddTree -> BddTree -> Bool
== :: BddTree -> BddTree -> Bool
$c/= :: BddTree -> BddTree -> Bool
/= :: 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
$creadsPrec :: Int -> ReadS BddTree
readsPrec :: Int -> ReadS BddTree
$creadList :: ReadS [BddTree]
readList :: ReadS [BddTree]
$creadPrec :: ReadPrec BddTree
readPrec :: ReadPrec BddTree
$creadListPrec :: ReadPrec [BddTree]
readListPrec :: ReadPrec [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
$cshowsPrec :: Int -> BddTree -> ShowS
showsPrec :: Int -> BddTree -> ShowS
$cshow :: BddTree -> String
show :: BddTree -> String
$cshowList :: [BddTree] -> ShowS
showList :: [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 n :: Int
n = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ 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 a. Eq a => a -> [a] -> 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 n :: Int
n = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ 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 n :: Int
n = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ 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
      n :: Int
n = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Bdd -> Maybe Int
firstVarOf Bdd
b
      rest :: Assignment
rest = Maybe Assignment -> Assignment
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Assignment -> Assignment) -> Maybe Assignment -> Assignment
forall a b. (a -> b) -> a -> b
$ 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 a. [a] -> 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. HasCallStack => [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 list of 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)

-- | Get the number of satisfying assignments, given a list of variables.
-- Note that the given list 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 a. [a] -> 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 a. [a] -> 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
      curvar :: Int
curvar = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ 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 a. Num a => [a] -> a
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. HasCallStack => [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)

-- | Find an optimal variable-reording.
-- Returns a relabelling @r@ such that @sizeOf (relabel r b)@ is minimal.
optimalOrder :: Bdd -> [(Int,Int)]
optimalOrder :: Bdd -> [(Int, Int)]
optimalOrder Bdd
b = ([(Int, Int)] -> [(Int, Int)] -> Ordering)
-> [[(Int, Int)]] -> [(Int, Int)]
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ([(Int, Int)] -> Int)
-> [(Int, Int)]
-> [(Int, Int)]
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (\[(Int, Int)]
r -> Bdd -> Int
sizeOf ([(Int, Int)] -> Bdd -> Bdd
relabel [(Int, Int)]
r Bdd
b))) [[(Int, Int)]]
allPermut where
  allPermut :: [[(Int, Int)]]
allPermut = ([Int] -> [(Int, Int)]) -> [[Int]] -> [[(Int, Int)]]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Bdd -> [Int]
allVarsOf Bdd
b)) ([[Int]] -> [[(Int, Int)]]) -> [[Int]] -> [[(Int, Int)]]
forall a b. (a -> b) -> a -> b
$ [Int] -> [[Int]]
forall a. [a] -> [[a]]
permutations (Bdd -> [Int]
allVarsOf 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 a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bdd
top
  , Bdd -> Gen Bdd
forall a. a -> Gen a
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 a b. Gen (a -> b) -> Gen a -> Gen b
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 a b. Gen (a -> b) -> Gen a -> Gen b
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 a b. Gen (a -> b) -> Gen a -> Gen b
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 a b. Gen (a -> b) -> Gen a -> Gen b
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 a b. Gen (a -> b) -> Gen a -> Gen b
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 a b. Gen (a -> b) -> Gen a -> Gen b
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 a b. Gen (a -> b) -> Gen a -> Gen b
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 a b. Gen (a -> b) -> Gen a -> Gen b
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 a b. Gen (a -> b) -> Gen a -> Gen b
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)