-- | Helper module for Bdd-to-Formula conversion.
module SMCDEL.Other.BDD2Form where

import Data.HasCacBDD
import SMCDEL.Language hiding (Bot,Top)
import qualified SMCDEL.Language (Form(Bot,Top))

-- | Convert a `Bdd` from HasCacBDD to SMCDEL `Form`ulas.
formOf :: Bdd -> Form
formOf :: Bdd -> Form
formOf = Form -> Form
simplify (Form -> Form) -> (Bdd -> Form) -> Bdd -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BddTree -> Form
formOfTree (BddTree -> Form) -> (Bdd -> BddTree) -> Bdd -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> BddTree
unravel where
  formOfTree :: BddTree -> Form
  formOfTree :: BddTree -> Form
formOfTree BddTree
Bot                = Form
SMCDEL.Language.Bot
  formOfTree BddTree
Top                = Form
SMCDEL.Language.Top
  formOfTree (Var Int
n BddTree
Top  BddTree
Bot)   = Prp -> Form
PrpF (Int -> Prp
P Int
n)
  formOfTree (Var Int
n BddTree
Bot  BddTree
Top)   = Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
n)
  formOfTree (Var Int
n BddTree
Top  BddTree
right) = [Form] -> Form
Disj [ Prp -> Form
PrpF (Int -> Prp
P Int
n), BddTree -> Form
formOfTree BddTree
right ]
  formOfTree (Var Int
n BddTree
Bot  BddTree
right) = [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
n), BddTree -> Form
formOfTree BddTree
right ]
  formOfTree (Var Int
n BddTree
left BddTree
Top)   = [Form] -> Form
Disj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
n), BddTree -> Form
formOfTree BddTree
left ]
  formOfTree (Var Int
n BddTree
left BddTree
Bot)   = [Form] -> Form
Conj [ Prp -> Form
PrpF (Int -> Prp
P Int
n), BddTree -> Form
formOfTree BddTree
left ]
  formOfTree (Var Int
n BddTree
left BddTree
right) =
    [Form] -> Form
Disj [ [Form] -> Form
Conj [ Prp -> Form
PrpF (Int -> Prp
P Int
n), BddTree -> Form
formOfTree BddTree
left ] ,
            [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
n), BddTree -> Form
formOfTree BddTree
right ] ]