{-# LANGUAGE ForeignFunctionInterface #-}
module Data.HasCacBDD (
Bdd, Assignment,
top, bot, var,
neg, con, dis, imp, equ, xor, conSet, disSet, xorSet,
exists, forall, forallSet, existsSet,
restrict, restrictSet, restrictLaw,
ifthenelse, gfp, relabel, relabelFun,
substit, substitSimul,
evaluate, evaluateFun,
allSats, allSatsWith, satCountWith, anySat, anySatWith,
firstVarOf, maxVarOf, allVarsOf, allVarsOfSorted,
thenOf, elseOf, subsOf, sizeOf,
BddTree(..), unravel, ravel,
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)
newtype Bdd = Bdd (ForeignPtr CacBDD)
type CacBDD = ()
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
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 :: 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 #-}
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 #-}
restrictLaw :: Bdd -> Bdd -> Bdd
restrictLaw :: Bdd -> Bdd -> Bdd
restrictLaw = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Restrict
{-# NOINLINE restrictLaw #-}
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 #-}
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 #-}
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
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
top :: Bdd
top :: Bdd
top = NullOp -> Bdd
fromManager NullOp
xBddManager_BddOne
{-# NOINLINE top #-}
bot :: Bdd
bot :: Bdd
bot = NullOp -> Bdd
fromManager NullOp
xBddManager_BddZero
{-# NOINLINE bot #-}
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 #-}
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 #-}
neg :: Bdd -> Bdd
neg :: Bdd -> Bdd
neg = NullOp -> Bdd -> Bdd
withBDD NullOp
bdd_Operator_Not
{-# NOINLINE neg #-}
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)
{-# NOINLINE equ #-}
imp :: Bdd -> Bdd -> Bdd
imp :: Bdd -> Bdd -> Bdd
imp Bdd
b1 = Bdd -> Bdd -> Bdd
dis (Bdd -> Bdd
neg Bdd
b1)
{-# NOINLINE imp #-}
con :: Bdd -> Bdd -> Bdd
con :: Bdd -> Bdd -> Bdd
con = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Operator_And
{-# NOINLINE con #-}
dis :: Bdd -> Bdd -> Bdd
dis :: Bdd -> Bdd -> Bdd
dis = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Operator_Or
{-# NOINLINE dis #-}
xor :: Bdd -> Bdd -> Bdd
xor :: Bdd -> Bdd -> Bdd
xor = BinaryOp -> Bdd -> Bdd -> Bdd
withTwoBDDs BinaryOp
bdd_Operator_Xor
{-# NOINLINE xor #-}
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 #-}
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 #-}
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 #-}
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)
thenOf :: Bdd -> Bdd
thenOf :: Bdd -> Bdd
thenOf = NullOp -> Bdd -> Bdd
withBDD NullOp
bdd_Then
elseOf :: Bdd -> Bdd
elseOf :: Bdd -> Bdd
elseOf = NullOp -> Bdd -> Bdd
withBDD NullOp
bdd_Else
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))
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
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))
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
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)
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)
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)
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
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 :: 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
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
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
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)
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 ]
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)
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] ]
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 :: [(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))
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))
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))
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)
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
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)