{-|
Module      : PrintableBdd
Description : A wrapper module implementing a Binary Decision Diagram system that can be 
              printed in either text or latex. This module internally uses the Data.HasCacBDD module. 
Copyright   : (c) Jesper Kuiper, 2021
                  Leander van Boven, 2021
                  Ramon Meffert, 2021
License     : BSD3
-}

module PrintableBdd
( -- * BDD type
  Bdd
  -- ** BDD fields
, bdd
, str
, tex 
  -- * Other types
, Assignment
, VarLabeller
  -- * Creating new BDDs
, varl
, var
, top
, bot
  -- * BDD Operators
  -- ** Unary operator
, neg
  -- ** Binary operators
, con
, dis
, imp
, equ
, xor
  -- ** N-ary operators
, conSet
, disSet
, xorSet
  -- ** Quantification
, foralll
, forall
, existsl
, exists
  -- ** N-ary quantification
, forallSetl
, forallSet
, existsSetl
, existsSet
-- ** Substitution
, substitl
, substit
-- * Variable inspection
, allVarsOf
-- * Evaluation
, evaluate
, evaluateFun
) where

import qualified Data.HasCacBDD as B
import Data.Bifunctor ( Bifunctor(second) )
import Data.List ( intercalate )

import Data.Set (Set)

-- | Printable data wrapper for the `Data.HasCacBDD.Bdd` record.
data Bdd = Bdd
  { -- | The formula represented as a unicode string for direct printing.
    Bdd -> String
str :: String

    -- | The formula represented as a string, formatted in LaTeX.
  , Bdd -> String
tex :: String

    -- | The binary decision diagram, as a `Data.HasCacBDD.Bdd` type. 
  , Bdd -> Bdd
bdd :: B.Bdd
  } deriving ( Bdd -> Bdd -> Bool
(Bdd -> Bdd -> Bool) -> (Bdd -> Bdd -> Bool) -> Eq Bdd
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bdd -> Bdd -> Bool
$c/= :: Bdd -> Bdd -> Bool
== :: Bdd -> Bdd -> Bool
$c== :: Bdd -> Bdd -> Bool
Eq, ReadPrec [Bdd]
ReadPrec Bdd
Int -> ReadS Bdd
ReadS [Bdd]
(Int -> ReadS Bdd)
-> ReadS [Bdd] -> ReadPrec Bdd -> ReadPrec [Bdd] -> Read Bdd
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Bdd]
$creadListPrec :: ReadPrec [Bdd]
readPrec :: ReadPrec Bdd
$creadPrec :: ReadPrec Bdd
readList :: ReadS [Bdd]
$creadList :: ReadS [Bdd]
readsPrec :: Int -> ReadS Bdd
$creadsPrec :: Int -> ReadS Bdd
Read )

instance Show Bdd where
  show :: Bdd -> String
show = Bdd -> String
str

-- | An assignment is a valuation for a set of variables, i.e. a valuation as to whether a variable is true or false. 
type Assignment = [(Int, Bool)]

-- | The printable BDD can label their variables, instead of using integers. A VarLabeller type is a function that encodes
--   a variable integer to its corresponding name.
type VarLabeller = (Int -> String)

-- | Encodes an arbitrary function that takes a single `Data.HasCacBDD.Bdd` argument to its printable counterpart.
directly :: (B.Bdd -> a) -> (Bdd -> a)
directly :: (Bdd -> a) -> Bdd -> a
directly = ((Bdd -> a) -> (Bdd -> Bdd) -> Bdd -> a)
-> (Bdd -> Bdd) -> (Bdd -> a) -> Bdd -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bdd -> a) -> (Bdd -> Bdd) -> Bdd -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Bdd -> Bdd
bdd

-- | Encodes a nullary function of Data.HasCacBDD to its printable counterpart.
nullary :: String -> String -> B.Bdd -> Bdd
nullary :: String -> String -> Bdd -> Bdd
nullary = String -> String -> Bdd -> Bdd
Bdd

-- | Encodes a unary function (taking one `Data.HasCacBDD.Bdd` argument) of `Data.HasCacBDD` to its printable counterpart.
unary :: String -> String -> (B.Bdd -> B.Bdd) -> (Bdd -> Bdd)
unary :: String -> String -> (Bdd -> Bdd) -> Bdd -> Bdd
unary String
s String
t Bdd -> Bdd
f Bdd
b = String -> String -> Bdd -> Bdd
Bdd (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bdd -> String
str Bdd
b) (String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bdd -> String
tex Bdd
b) (Bdd -> Bdd
f (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
bdd Bdd
b)

-- | Encodes a binary function (taking two `Data.HasCacBDD.Bdd` arguments) of `Data.HasCacBDD` to its printable counterpart.
binary :: String -> String -> (B.Bdd -> B.Bdd -> B.Bdd) -> (Bdd -> Bdd -> Bdd)
binary :: String -> String -> (Bdd -> Bdd -> Bdd) -> Bdd -> Bdd -> Bdd
binary String
s String
t Bdd -> Bdd -> Bdd
f Bdd
b1 Bdd
b2 = String -> String -> Bdd -> Bdd
Bdd
  ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(", Bdd -> String
str Bdd
b1, String
" ", String
s, String
" ", Bdd -> String
str Bdd
b2, String
")"])
  ([String] -> String
unwords [String
"(", Bdd -> String
tex Bdd
b1, String
t, Bdd -> String
tex Bdd
b2, String
")"])
  (Bdd -> Bdd -> Bdd
f (Bdd -> Bdd
bdd Bdd
b1) (Bdd -> Bdd
bdd Bdd
b2))

-- | Encodes an n-ary function of `Data.HasCacBDD` to its printable counterpart.
nary :: String -> String -> ([B.Bdd] -> B.Bdd) -> ([Bdd] -> Bdd)
nary :: String -> String -> ([Bdd] -> Bdd) -> [Bdd] -> Bdd
nary String
s String
t [Bdd] -> Bdd
f [Bdd]
list = String -> String -> Bdd -> Bdd
Bdd
  (String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate (String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ") ((Bdd -> String) -> [Bdd] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bdd -> String
str [Bdd]
list) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")
  (String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate (String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ") ((Bdd -> String) -> [Bdd] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bdd -> String
tex [Bdd]
list) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") ")
  ([Bdd] -> Bdd
f ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$ (Bdd -> Bdd) -> [Bdd] -> [Bdd]
forall a b. (a -> b) -> [a] -> [b]
map Bdd -> Bdd
bdd [Bdd]
list)

-- | Encodes a binary quantification function of Data.HasCacBDD to its printable counterpart.
quant :: VarLabeller -> VarLabeller -> String -> String -> (Int -> B.Bdd -> B.Bdd) -> (Int -> Bdd -> Bdd)
quant :: VarLabeller
-> VarLabeller
-> String
-> String
-> (Int -> Bdd -> Bdd)
-> Int
-> Bdd
-> Bdd
quant VarLabeller
ls VarLabeller
lt String
s String
t Int -> Bdd -> Bdd
f Int
v Bdd
b = String -> String -> Bdd -> Bdd
Bdd
  ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
s, VarLabeller
ls Int
v, String
"(", Bdd -> String
str Bdd
b, String
")"])
  ([String] -> String
unwords [String
t, VarLabeller
lt Int
v, String
"\\left( ", Bdd -> String
tex Bdd
b, String
"\\right)"])
  (Int -> Bdd -> Bdd
f Int
v (Bdd -> Bdd
bdd Bdd
b))

-- | Encodes an n-ary binary quantification function of Data.HasCacBDD to its printable counterpart.
quantSet :: VarLabeller -> VarLabeller -> String -> String -> ([Int] -> B.Bdd -> B.Bdd) -> ([Int] -> Bdd -> Bdd)
quantSet :: VarLabeller
-> VarLabeller
-> String
-> String
-> ([Int] -> Bdd -> Bdd)
-> [Int]
-> Bdd
-> Bdd
quantSet VarLabeller
ls VarLabeller
lt String
s String
t [Int] -> Bdd -> Bdd
f [Int]
v Bdd
b = String -> String -> Bdd -> Bdd
Bdd
  ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
s, String
"{", String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (VarLabeller -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map VarLabeller
ls [Int]
v), String
"}", String
"(", Bdd -> String
str Bdd
b, String
")"])
  ([String] -> String
unwords [String
t, String
"\\left{", String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" , " (VarLabeller -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map VarLabeller
lt [Int]
v), String
"\\right}", String
"(", Bdd -> String
str Bdd
b, String
")"]) 
  ([Int] -> Bdd -> Bdd
f [Int]
v (Bdd -> Bdd
bdd Bdd
b))

{-
      Nullary operators
-}

-- | Encode a labelled integer as a BDD variable. Note that the first labeller is for text, the second for LaTeX. The variable is indexed by any integer from 0 to 1.000.000.
-- 
-- >>> slabel n = "var" ++ (show n)
-- >>> tlabel n = "p_" ++ (show n)
-- >>> foo = varl slabel tlabel 0
-- >>> foo
-- var0
-- >>> tex foo
-- p_0
varl :: VarLabeller -> VarLabeller -> Int -> Bdd
varl :: VarLabeller -> VarLabeller -> Int -> Bdd
varl VarLabeller
ls VarLabeller
lt Int
i = String -> String -> Bdd -> Bdd
nullary (VarLabeller
ls Int
i) (VarLabeller
lt Int
i) (Int -> Bdd
B.var Int
i)

-- | Encode an unlabelled integer as a BDD variable. The variable is indexed by any integer from 0 to 1.000.000.
var :: Int -> Bdd
var :: Int -> Bdd
var = VarLabeller -> VarLabeller -> Int -> Bdd
varl VarLabeller
forall a. Show a => a -> String
show VarLabeller
forall a. Show a => a -> String
show

-- | True constant.
--
-- >>> top
-- ⊤
top :: Bdd
top :: Bdd
top = String -> String -> Bdd -> Bdd
nullary String
"⊤" String
"\\top " Bdd
B.top

-- | False constant.
--
-- >>> bot
-- ⊥
bot :: Bdd
bot :: Bdd
bot = String -> String -> Bdd -> Bdd
nullary String
"⊥" String
"\\bot " Bdd
B.bot


{-
      Unary operators
-}

{- |
Negation.

>>> neg foo
¬(foo)
-}
neg :: Bdd -> Bdd
neg :: Bdd -> Bdd
neg = String -> String -> (Bdd -> Bdd) -> Bdd -> Bdd
unary String
"¬" String
"\\neg" Bdd -> Bdd
B.neg


{-
      Binary operators
-}

-- | Conjunction. 
-- 
-- >>> foo `con` bar
-- (foo ∧ bar)
con :: Bdd -> Bdd -> Bdd
con :: Bdd -> Bdd -> Bdd
con = String -> String -> (Bdd -> Bdd -> Bdd) -> Bdd -> Bdd -> Bdd
binary String
"∧" String
"\\wedge" Bdd -> Bdd -> Bdd
B.con

-- | Disjunction.
--
-- >>> foo `dis` bar
-- (foo ∨ bar)
dis :: Bdd -> Bdd -> Bdd
dis :: Bdd -> Bdd -> Bdd
dis = String -> String -> (Bdd -> Bdd -> Bdd) -> Bdd -> Bdd -> Bdd
binary String
"∨" String
"\\vee" Bdd -> Bdd -> Bdd
B.dis

-- | Logical implication.
--
-- >>> foo `imp` bar
-- (foo ⟶ bar)
imp :: Bdd -> Bdd -> Bdd
imp :: Bdd -> Bdd -> Bdd
imp = String -> String -> (Bdd -> Bdd -> Bdd) -> Bdd -> Bdd -> Bdd
binary String
"⟶" String
"\\rightarrow" Bdd -> Bdd -> Bdd
B.imp

-- | Logical bi-implication or equivalence.
--
-- >>> foo `equ` bar
-- (foo ⟷ bar)
equ :: Bdd -> Bdd -> Bdd
equ :: Bdd -> Bdd -> Bdd
equ = String -> String -> (Bdd -> Bdd -> Bdd) -> Bdd -> Bdd -> Bdd
binary String
"⟷" String
"\\leftrightarrow" Bdd -> Bdd -> Bdd
B.equ

-- | Exlusive or.
--
-- >>> foo `xor` bar 
-- (foo ⊻ bar)
xor :: Bdd -> Bdd -> Bdd
xor :: Bdd -> Bdd -> Bdd
xor = String -> String -> (Bdd -> Bdd -> Bdd) -> Bdd -> Bdd -> Bdd
binary String
"⊻" String
"\\oplus" Bdd -> Bdd -> Bdd
B.xor


{-
      Quantification operators
-}

-- | Labelled binary universal quantification. Note that the first VarLabeller works for direct printing and the VarLabeller is for latex.
--
-- >>> slabel n = "var" ++ (show n)
-- >>> tlabel n = "p_" ++ (show n)
-- >>> foo = foralll slabel tlabel 0 $ varl slabel tlabel 0 `imp` varl slabel tlabel 1
-- >>> foo
-- ∀var0(var0 ⟶ var1)
-- >>> tex foo
-- \\forall p_0 (p_0 \\rightarrow p_1)
foralll :: VarLabeller -> VarLabeller -> Int -> Bdd -> Bdd
foralll :: VarLabeller -> VarLabeller -> Int -> Bdd -> Bdd
foralll VarLabeller
ls VarLabeller
lt = VarLabeller
-> VarLabeller
-> String
-> String
-> (Int -> Bdd -> Bdd)
-> Int
-> Bdd
-> Bdd
quant VarLabeller
ls VarLabeller
lt String
"∀" String
"\\forall" Int -> Bdd -> Bdd
B.forall

-- | Unlabelled binary universal quantification. 
-- 
-- >>> forall 0 foo
-- ∀0(foo)
forall :: Int -> Bdd -> Bdd
forall :: Int -> Bdd -> Bdd
forall = VarLabeller -> VarLabeller -> Int -> Bdd -> Bdd
foralll VarLabeller
forall a. Show a => a -> String
show VarLabeller
forall a. Show a => a -> String
show

-- | Labelled binary existential quantification.
--
-- >>> slabel n = "var" ++ (show n)
-- >>> tlabel n = "p_" ++ (show n)
-- >>> foo = existsl slabel tlabel 0 $ (varl slabel tlabel 0) `imp` (varl slabel tlabel 1)
-- >>> foo
-- ∃var0(var0 ⟶ var1)
-- >>> tex foo
-- \\exists (p_0 \\rightarrow p_1) 
existsl :: VarLabeller -> VarLabeller -> Int -> Bdd -> Bdd
existsl :: VarLabeller -> VarLabeller -> Int -> Bdd -> Bdd
existsl VarLabeller
ls VarLabeller
lt = VarLabeller
-> VarLabeller
-> String
-> String
-> (Int -> Bdd -> Bdd)
-> Int
-> Bdd
-> Bdd
quant VarLabeller
ls VarLabeller
lt String
"∃" String
"\\exists" Int -> Bdd -> Bdd
B.exists

-- | Unlabelled binary existential quantification
--
-- >>> exists 0 foo
-- ∃0(foo)
exists :: Int -> Bdd -> Bdd
exists :: Int -> Bdd -> Bdd
exists = VarLabeller -> VarLabeller -> Int -> Bdd -> Bdd
existsl VarLabeller
forall a. Show a => a -> String
show VarLabeller
forall a. Show a => a -> String
show

-- | Labelled big binary universal quanficition. 
--
-- >>> slabel n = "var" ++ (show n)
-- >>> tlabel n = "p_" ++ (show n)
-- >>> foo = forallSetl slabel tlabel [0, 1] $ (varl slabel tlabel 0) `imp` (varl slabel tlabel 1)
-- >>> foo
-- ∀{var0, var1}(var0 ⟶ var1)
-- >>> tex foo
-- \\forall \\left{ p_0, p_1 \\right} (p_0 \\rightarrow p_1)
forallSetl :: VarLabeller -> VarLabeller -> [Int] -> Bdd -> Bdd
forallSetl :: VarLabeller -> VarLabeller -> [Int] -> Bdd -> Bdd
forallSetl VarLabeller
ls VarLabeller
lt = VarLabeller
-> VarLabeller
-> String
-> String
-> ([Int] -> Bdd -> Bdd)
-> [Int]
-> Bdd
-> Bdd
quantSet VarLabeller
ls VarLabeller
lt String
"∀" String
"\\forall" [Int] -> Bdd -> Bdd
B.forallSet

-- | Unlabelled big binary universal quantification. 
--
-- >>> forallSet [0,1,2] foo
-- ∀{0,1,2}(foo)
forallSet :: [Int] -> Bdd -> Bdd
forallSet :: [Int] -> Bdd -> Bdd
forallSet = VarLabeller -> VarLabeller -> [Int] -> Bdd -> Bdd
forallSetl VarLabeller
forall a. Show a => a -> String
show VarLabeller
forall a. Show a => a -> String
show

-- | Labelled big binary existential quantification.
--
-- >>> slabel n = "var" ++ (show n)
-- >>> tlabel n = "p_" ++ (show n)
-- >>> foo = existsSetl slabel tlabel [0, 1] $ (varl slabel tlabel 0) `imp` (varl slabel tlabel 1)
-- >>> foo
-- ∃{var0, var1}(var0 ⟶ var1)
-- >>> tex foo
-- \\exists \\left{ p_0, p_1 \\right} (p_0 \\rightarrow p_1)
existsSetl :: VarLabeller -> VarLabeller -> [Int] -> Bdd -> Bdd
existsSetl :: VarLabeller -> VarLabeller -> [Int] -> Bdd -> Bdd
existsSetl VarLabeller
ls VarLabeller
lt = VarLabeller
-> VarLabeller
-> String
-> String
-> ([Int] -> Bdd -> Bdd)
-> [Int]
-> Bdd
-> Bdd
quantSet VarLabeller
ls VarLabeller
lt String
"∃" String
"\\exists" [Int] -> Bdd -> Bdd
B.existsSet

-- | Unlabelled big binary existential quantification.
--
-- >>> existsSet [0,1,2] foo
-- ∃{0,1,2}(foo)
existsSet :: [Int] -> Bdd -> Bdd
existsSet :: [Int] -> Bdd -> Bdd
existsSet = VarLabeller -> VarLabeller -> [Int] -> Bdd -> Bdd
existsSetl VarLabeller
forall a. Show a => a -> String
show VarLabeller
forall a. Show a => a -> String
show

-- N-ary operators

-- | Big (setwise) conjunction.
--
-- >>> conSet [foo, bar, baz]
-- (foo ∧ bar ∧ baz)
conSet :: [Bdd] -> Bdd
conSet :: [Bdd] -> Bdd
conSet = String -> String -> ([Bdd] -> Bdd) -> [Bdd] -> Bdd
nary String
"∧" String
"\\wedge" [Bdd] -> Bdd
B.conSet


-- | Big (setwise) disjunction.
--
-- >>> disSet [foo, bar, baz]
-- (foo ∨ bar ∨ baz)
disSet :: [Bdd] -> Bdd
disSet :: [Bdd] -> Bdd
disSet = String -> String -> ([Bdd] -> Bdd) -> [Bdd] -> Bdd
nary String
"∨" String
"\\vee" [Bdd] -> Bdd
B.disSet

-- | Big (setwise) exclusive disjunction.
--
-- >>> xorSet [foo, bar, baz]
-- (foo ⊻ bar ⊻ baz)
xorSet :: [Bdd] -> Bdd
xorSet :: [Bdd] -> Bdd
xorSet = String -> String -> ([Bdd] -> Bdd) -> [Bdd] -> Bdd
nary String
"⊻" String
"\\oplus" [Bdd] -> Bdd
B.xorSet

-- Special operators

-- | Labelled substitution.
--
-- >>> label n = "var" ++ n
-- >>> subsitl label 0 top foo
-- [var0\⊤](foo)
substitl :: VarLabeller -> Int -> Bdd -> Bdd -> Bdd
substitl :: VarLabeller -> Int -> Bdd -> Bdd -> Bdd
substitl VarLabeller
l Int
i Bdd
s Bdd
f = String -> String -> Bdd -> Bdd
Bdd
  ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"[", VarLabeller
l Int
i, String
"\\", Bdd -> String
str Bdd
s, String
"](", Bdd -> String
str Bdd
f, String
")"])
  ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"\\left[ ", VarLabeller
l Int
i, String
" \\setminus ", Bdd -> String
tex Bdd
s, String
"\\right]\\left( ", Bdd -> String
tex Bdd
f, String
" )"])
  (Int -> Bdd -> Bdd -> Bdd
B.substit Int
i (Bdd -> Bdd
bdd Bdd
s) (Bdd -> Bdd
bdd Bdd
f))

-- | Unlabelled substitution.
--
-- >>> substit 0 top foo
-- [0\⊤]foo
substit :: Int -> Bdd -> Bdd -> Bdd
substit :: Int -> Bdd -> Bdd -> Bdd
substit = VarLabeller -> Int -> Bdd -> Bdd -> Bdd
substitl VarLabeller
forall a. Show a => a -> String
show

-- other

-- | Returns all variables (without labels) that occur within the given BDD.
--
-- >>> allVarsOf (var 0 `imp` (var 1 `dis` var 2))
-- [0,1,2]
allVarsOf :: Bdd -> [Int]
allVarsOf :: Bdd -> [Int]
allVarsOf = (Bdd -> [Int]) -> Bdd -> [Int]
forall a. (Bdd -> a) -> Bdd -> a
directly Bdd -> [Int]
B.allVarsOf

-- | Evaluate a BDD, given an assignment. Returns Nothing if the assignment doesn't contain all variables of the BDD.
--
-- >>> evaluate (var 0 `imp` var 1) [(0, True), (1, False)]
-- Just False 
-- >>> evaluate (var 0 `imp` var 1) [(0, True)]
-- Nothing
evaluate :: Bdd -> Assignment -> Maybe Bool
evaluate :: Bdd -> Assignment -> Maybe Bool
evaluate = (Bdd -> Assignment -> Maybe Bool)
-> Bdd -> Assignment -> Maybe Bool
forall a. (Bdd -> a) -> Bdd -> a
directly Bdd -> Assignment -> Maybe Bool
B.evaluate

-- | Evaluates a BDD, given a total assignment function.
--
-- >>> evaluateFun (var 0 `imp` var 1) (\ x -> if x == 0 then True else False)
-- False
evaluateFun :: Bdd -> (Int -> Bool) -> Bool
evaluateFun :: Bdd -> (Int -> Bool) -> Bool
evaluateFun = (Bdd -> (Int -> Bool) -> Bool) -> Bdd -> (Int -> Bool) -> Bool
forall a. (Bdd -> a) -> Bdd -> a
directly Bdd -> (Int -> Bool) -> Bool
B.evaluateFun