module SMCDEL.Internal.TaggedBDD where
import Data.Tagged
import Data.HasCacBDD hiding (Top,Bot)
import SMCDEL.Language
class TagForBDDs a where
multiplier :: Tagged a Bdd -> Int
multiplier Tagged a Bdd
_ = Int
2
unmvBdd :: Tagged a Bdd -> Bdd
unmvBdd = (Int -> Int) -> Bdd -> Bdd
relabelFun (\Int
n -> if Int -> Bool
forall a. Integral a => a -> Bool
even Int
n then Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2 else [Char] -> Int
forall a. HasCallStack => [Char] -> a
error ([Char]
"Odd: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)) (Bdd -> Bdd) -> (Tagged a Bdd -> Bdd) -> Tagged a Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tagged a Bdd -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag
mv :: Bdd -> Tagged a Bdd
mv = Int -> Bdd -> Tagged a Bdd
forall a. TagForBDDs a => Int -> Bdd -> Tagged a Bdd
cpMany Int
0
cp :: Bdd -> Tagged a Bdd
cp = Int -> Bdd -> Tagged a Bdd
forall a. TagForBDDs a => Int -> Bdd -> Tagged a Bdd
cpMany Int
1
cpMany :: Int -> Bdd -> Tagged a Bdd
cpMany Int
k Bdd
b = let x :: Tagged a Bdd
x = Bdd -> Tagged a Bdd
forall a. a -> Tagged a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bdd -> Tagged a Bdd) -> Bdd -> Tagged a Bdd
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Bdd -> Bdd
relabelFun (\Int
n -> (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k) Bdd
b
in if Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Tagged a Bdd -> Int
forall a. TagForBDDs a => Tagged a Bdd -> Int
multiplier Tagged a Bdd
x then [Char] -> Tagged a Bdd
forall a. HasCallStack => [Char] -> a
error [Char]
"Not enough markers!" else Tagged a Bdd
x
tagBddEval :: [Prp] -> Tagged a Bdd -> Bool
tagBddEval [Prp]
truths Tagged a Bdd
querybdd = Bdd -> (Int -> Bool) -> Bool
evaluateFun (Tagged a Bdd -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag Tagged a Bdd
querybdd) (\Int
n -> Int -> Prp
P Int
n Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
truths)
data Dubbel
instance TagForBDDs Dubbel where
multiplier :: Tagged Dubbel Bdd -> Int
multiplier = Int -> Tagged Dubbel Bdd -> Int
forall a b. a -> b -> a
const Int
2
data Tripel
instance TagForBDDs Tripel where
multiplier :: Tagged Tripel Bdd -> Int
multiplier = Int -> Tagged Tripel Bdd -> Int
forall a b. a -> b -> a
const Int
3
data Quadrupel
instance TagForBDDs Quadrupel where
multiplier :: Tagged Quadrupel Bdd -> Int
multiplier = Int -> Tagged Quadrupel Bdd -> Int
forall a b. a -> b -> a
const Int
4
totalRelBdd :: Tagged a Bdd
totalRelBdd :: forall a. Tagged a Bdd
totalRelBdd = Bdd -> Tagged a Bdd
forall a. a -> Tagged a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bdd
top
emptyRelBdd :: Tagged a Bdd
emptyRelBdd :: forall a. Tagged a Bdd
emptyRelBdd = Bdd -> Tagged a Bdd
forall a. a -> Tagged a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bdd
bot
allsamebdd :: TagForBDDs a => [Prp] -> Tagged a Bdd
allsamebdd :: forall a. TagForBDDs a => [Prp] -> Tagged a Bdd
allsamebdd [Prp]
ps = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> Tagged a [Bdd] -> Tagged a Bdd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Tagged a Bdd] -> Tagged a [Bdd]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ Bdd -> Bdd -> Bdd
equ (Bdd -> Bdd -> Bdd) -> Tagged a Bdd -> Tagged a (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> Tagged a Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
mv (Int -> Bdd
var Int
x) Tagged a (Bdd -> Bdd) -> Tagged a Bdd -> Tagged a Bdd
forall a b. Tagged a (a -> b) -> Tagged a a -> Tagged a b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bdd -> Tagged a Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
cp (Int -> Bdd
var Int
x) | (P Int
x) <- [Prp]
ps ]