-
Notifications
You must be signed in to change notification settings - Fork 2
/
TypeFamily.hs
69 lines (56 loc) · 2.08 KB
/
TypeFamily.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
{-#LANGUAGE TypeFamilies, EmptyDataDecls, ImplicitParams #-}
module TypeFamily where
import Cudd
type family C a
type family V a
type family A a
type family S a
type family R a
data CUDDBDD
data VarData = VarData {variables :: [DdNode], indices :: [Int], varsCube :: DdNode, sortedInds :: [Int]}
type instance C CUDDBDD = DdManager
type instance V CUDDBDD = VarData
type instance A CUDDBDD = DdNode
type instance S CUDDBDD = [[SatBit]]
type instance R CUDDBDD = [Bool]
type UnOpType a = a -> a
type BinOpType a = a -> a -> a
type TernOpType a = a -> a -> a -> a
class BOp i where
iteOp :: i -> C i -> TernOpType (A i)
xnorOp, andOp, orOp, xorOp, impOp :: i -> C i -> BinOpType (A i)
notOp :: i -> C i -> UnOpType (A i)
topOp, botOp :: i -> C i -> A i
exists, forall :: i -> C i -> V i -> UnOpType (A i)
class Satisfiable i where
sat :: i -> C i -> A i -> S i
satOne :: i -> C i -> A i -> Maybe (R i)
extract :: i -> C i -> V i -> R i -> R i
expand :: i -> C i -> [V i] -> S i -> [[R i]]
expandOne :: i -> C i -> V i -> S i -> [R i]
oneSat :: i -> C i -> V i -> A i -> Maybe (R i)
instance BOp CUDDBDD where
iteOp i = cuddBddIte
xnorOp i = cuddBddXnor
xorOp i = cuddBddXor
andOp i = cuddBddAnd
orOp i = cuddBddOr
impOp i = cuddBddImp
notOp i = cuddNot
topOp i = cuddReadOne
botOp i = cuddReadLogicZero
exists i m vs n = cuddBddExistAbstract m n (varsCube vs)
forall i m vs n = cuddBddUnivAbstract m n (varsCube vs)
instance Satisfiable CUDDBDD where
sat i = cuddAllSat
satOne i m a = map (==One) `fmap` cuddOneSat m a
extract i = undefined
expand i = undefined
expandOne i = undefined
oneSat i = undefined
test :: (BOp i, Satisfiable i, ?inst :: i) => C i -> A i -> A i -> S i
test c x y = sat ?inst c (andOp ?inst c x y)
{-
test :: (?inst :: i, ?m :: C i, BOp i) => V i -> A i -> A i
test = exists ?inst ?m
-}