Skip to content
GitLab
Commit 610ba2ed authored by Gebhart97's avatar Gebhart97
Browse files

Reworked Sylvan-Haskell Bindings and some Fixes

parent a594aa49
Hide whitespace changes
Inline Side-by-side
examples/int-valuedSymbolicTest deleted 100644 → 0
View file @ a594aa49
q1: {q3: 2}
q2: {q3: 2}
q3: {q2: 1}
examples/powersetSymbolicTest deleted 100644 → 0
View file @ a594aa49
x: { x, y }
y: { }
z: { x }
d: { d }
e: { e }
f: { e, f, x, y, z }
g: { z }
h: { }
\ No newline at end of file
src/Copar/Symbolic/SymbolicUtils.hs
View file @ 610ba2ed
......@@ -56,7 +56,7 @@ import qualified Copar.Parser.Lexer as L
import Copar.RewriteFunctors (applyFunctorRewrites)
import Data.Typeable (Proxy (..))
--import Debug.Trace
import Debug.Trace
--
-- BDD-variables are allocated as follows: Let n = ceil(log_2(|S|))
......@@ -209,7 +209,7 @@ decodePartitionHelper partition varsBlocks stateBitSize nextBlock = do
else do
let polarities = encodeInteger stateBitSize nextBlock
block <- cube varsBlocks polarities
statesEnc <- andExists partition block varsBlocks
statesEnc <- bddAndExists partition block varsBlocks
states <- decodeStates statesEnc stateBitSize stateBitSize
if (length states) == 0
then decodePartitionHelper partition varsBlocks stateBitSize (nextBlock+1)
......@@ -243,16 +243,25 @@ edgeToBDD varsEdges stateBitSize labelType e = do
leaf <- makefractionleaf (numerator (unsafeCoerce (label e))) (denominator (unsafeCoerce (label e)))
ite res leaf sylvanFalse
edgesToBDD :: PrimMonad m => V.Vector (Edge a) -> BDD -> Int -> LabelType -> m BDD
edgesToBDD edgesVec varsEdges stateBitSize labelType =
V.mapM (edgeToBDD varsEdges stateBitSize labelType) edgesVec
>>= V.foldM' (flip bor) sylvanFalse
edgesToBDD :: PrimMonad m => V.Vector (Edge a) -> BDD -> Int -> LabelType -> OrType -> m BDD
edgesToBDD edgesVec varsEdges stateBitSize labelType orType =
case orType of
OrOp -> V.mapM (edgeToBDD varsEdges stateBitSize labelType) edgesVec
>>= V.foldM' (flip bor) sylvanFalse
PlusOrOp -> V.mapM (edgeToBDD varsEdges stateBitSize labelType) edgesVec
>>= V.foldM' (flip bplus) sylvanFalse
MinOrOp -> V.mapM (edgeToBDD varsEdges stateBitSize labelType) edgesVec
>>= V.foldM' (flip bmin) sylvanFalse
MaxOrOp -> V.mapM (edgeToBDD varsEdges stateBitSize labelType) edgesVec
>>= V.foldM' (flip bmax) sylvanFalse
--transitionsToBDD :: PrimMonad m => Encoding a f1 -> BDD -> Int -> LabelType -> m BDD
--transitionsToBDD coalgebra varsEdges stateBitSize labelType = edgesToBDD (edges coalgebra) varsEdges stateBitSize labelType
data LabelType = NoLabel | PolynomialLabel | IntLabel | RealLabel | RationalLabel deriving (Enum, Eq)
data OrType = OrOp | PlusOrOp | MinOrOp | MaxOrOp deriving (Enum, Eq)
class (Typeable f, Ord (F1 f), Ord (Label f)) => SymbolicInterface f where
encodeEdges :: PrimMonad m => TypeRep f -> Int -> V.Vector (Edge (Label f)) -> m BDD
symbolicSig :: PrimMonad m => TypeRep f -> BDD -> BDD -> BDD -> m BDD
......@@ -262,37 +271,43 @@ class (Typeable f, Ord (F1 f), Ord (Label f)) => SymbolicInterface f where
instance SymbolicInterface Powerset where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, 0)
edgesToBDD edgesVec varsEdges stateBitSize PolynomialLabel
edgesToBDD edgesVec varsEdges stateBitSize PolynomialLabel OrOp
symbolicSig _ varsTo transitionBDD partitionBDD = andExists transitionBDD partitionBDD varsTo
symbolicSig _ varsTo transitionBDD partitionBDD = bddAndExists transitionBDD partitionBDD varsTo
instance SymbolicInterface Polynomial where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, (sizeOf (0::Int)))
edgesToBDD edgesVec varsEdges stateBitSize NoLabel
edgesToBDD edgesVec varsEdges stateBitSize NoLabel OrOp
symbolicSig _ varsTo transitionBDD partitionBDD = andExists transitionBDD partitionBDD varsTo
symbolicSig _ varsTo transitionBDD partitionBDD = bddAndExists transitionBDD partitionBDD varsTo
instance SymbolicInterface IntValued where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, 0)
edgesToBDD edgesVec varsEdges stateBitSize IntLabel
edgesToBDD edgesVec varsEdges stateBitSize IntLabel PlusOrOp
symbolicSig _ varsTo transitionBDD partitionBDD = mtbddAndExists transitionBDD partitionBDD varsTo
symbolicSig _ varsTo transitionBDD partitionBDD = do
sig <- bplus transitionBDD partitionBDD
abstractPlus sig varsTo
instance SymbolicInterface RealValued where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, 0)
edgesToBDD edgesVec varsEdges stateBitSize RealLabel
edgesToBDD edgesVec varsEdges stateBitSize RealLabel PlusOrOp
symbolicSig _ varsTo transitionBDD partitionBDD = mtbddAndExists transitionBDD partitionBDD varsTo
symbolicSig _ varsTo transitionBDD partitionBDD = do
sig <- bplus transitionBDD partitionBDD
abstractPlus sig varsTo
instance SymbolicInterface RationalValued where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, 0)
edgesToBDD edgesVec varsEdges stateBitSize RationalLabel
edgesToBDD edgesVec varsEdges stateBitSize RationalLabel PlusOrOp
symbolicSig _ varsTo transitionBDD partitionBDD = mtbddAndExists transitionBDD partitionBDD varsTo
symbolicSig _ varsTo transitionBDD partitionBDD = do
sig <- bplus transitionBDD partitionBDD
abstractPlus sig varsTo
-- Sadly I do not really know how to make Complex valued leaves in Sylvan. Maybe mtbdd_makeleaf with a custom type could be used,
-- but I don't know how well custom Types are supported in this version of Sylvan.
......@@ -308,38 +323,38 @@ instance SymbolicInterface Distribution where
instance SymbolicInterface MaxIntValued where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, 0)
edgesToBDD edgesVec varsEdges stateBitSize IntLabel
edgesToBDD edgesVec varsEdges stateBitSize IntLabel MaxOrOp
symbolicSig _ varsTo transitionBDD partitionBDD = do
sig <- band transitionBDD partitionBDD
mtbddAbstractMax sig varsTo
sig <- bmax transitionBDD partitionBDD
abstractMax sig varsTo
instance SymbolicInterface MinIntValued where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, 0)
edgesToBDD edgesVec varsEdges stateBitSize IntLabel
edgesToBDD edgesVec varsEdges stateBitSize IntLabel MinOrOp
symbolicSig _ varsTo transitionBDD partitionBDD = do
sig <- band transitionBDD partitionBDD
mtbddAbstractMin sig varsTo
sig <- bmin transitionBDD partitionBDD
abstractMin sig varsTo
instance SymbolicInterface MaxDoubleValued where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, 0)
edgesToBDD edgesVec varsEdges stateBitSize RealLabel
edgesToBDD edgesVec varsEdges stateBitSize RealLabel MaxOrOp
symbolicSig _ varsTo transitionBDD partitionBDD = do
sig <- band transitionBDD partitionBDD
mtbddAbstractMax sig varsTo
sig <- bmax transitionBDD partitionBDD
abstractMax sig varsTo
instance SymbolicInterface MinDoubleValued where
encodeEdges _ stateBitSize edgesVec = do
varsEdges <- createVarsEdges (stateBitSize, 0)
edgesToBDD edgesVec varsEdges stateBitSize RealLabel
edgesToBDD edgesVec varsEdges stateBitSize RealLabel MinOrOp
symbolicSig _ varsTo transitionBDD partitionBDD = do
sig <- band transitionBDD partitionBDD
mtbddAbstractMin sig varsTo
sig <- bmin transitionBDD partitionBDD
abstractMin sig varsTo
-- To get the other monoid valued, mtbdd_abstract could maybe be used (would have to expand the Sylvan-Haskell bindings and write bitwise and/or as a mtbdd_abstract_op)
......@@ -370,15 +385,22 @@ refinenementStep signature partition stateBitSize currentNewBlockNum cache block
_ -> do
v1 <- getvar partition
v2 <- getvar signature
if (((fromIntegral v2) - 10) < stateBitSize && signature /= sylvanFalse)
b1 <- isleaf partition
b2 <- isleaf signature
let s1 = ((fromIntegral v1) - 10 - stateBitSize)
s2 = ((fromIntegral v2) - 10)
sTop <- if (b1 == 1) then (if (b2 == 1) then return (-1::Int) else return s2)
else if (s1 < s2) then return s1
else return s2
if ((sTop >= 0) && (sTop < stateBitSize))
then do
lowS <- getlow signature
lowP <- if (((fromIntegral v1) - 10) - stateBitSize) == ((fromIntegral v2) - 10) then getlow partition else return partition
highS <- gethigh signature
highP <- if (((fromIntegral v1) - 10) - stateBitSize) == ((fromIntegral v2) - 10) then gethigh partition else return partition
lowS <- if (sTop == s2 && b2 /= 1) then getlow signature else return signature
lowP <- if (sTop == s1 && b1 /= 1) then getlow partition else return partition
highS <- if (sTop == s2 && b2 /= 1) then gethigh signature else return signature
highP <- if (sTop == s1 && b1 /= 1) then gethigh partition else return partition
(low, currentNewBlockNum', cache', blocks') <- refinenementStep lowS lowP stateBitSize currentNewBlockNum cache blocks
(high, currentNewBlockNum'', cache'', blocks'') <- refinenementStep highS highP stateBitSize currentNewBlockNum' cache' blocks'
var <- (ithVar ((fromIntegral ((fromIntegral v2) + stateBitSize))::BDDVar))
var <- (ithVar ((fromIntegral (sTop + 10 + stateBitSize))::BDDVar))
result <- ite var high low
return (result, currentNewBlockNum'', cache'', blocks'')
else
......@@ -649,8 +671,9 @@ refineSymbolicNew coalgebra = do
--a Block from the Block Map or a completely new Block.
refinenementStepHelper :: PrimMonad m => Int -> (BDD, Int, M.Map (BDD, BDD) BDD, M.Map BDD BDD) -> SomeBDD
-> m (BDD, Int, M.Map (BDD, BDD) BDD, M.Map BDD BDD)
refinenementStepHelper stateBitSize (partitionBDD, currentNewBlockNum, _, _) (SomeBDD _ signatureBDD) =
refinenementStep signatureBDD partitionBDD stateBitSize currentNewBlockNum M.empty M.empty
refinenementStepHelper stateBitSize (partitionBDD, currentNewBlockNum, _, _) (SomeBDD _ signatureBDD) = --do
-- re <- bddToArray signatureBDD
refinenementStep signatureBDD partitionBDD stateBitSize currentNewBlockNum M.empty M.empty --`debug` (show re)
refineRecurseNew :: PrimMonad m => BDD -> Int -> Int -> V.Vector (SomeBDD) -> BDD -> m P.Partition
refineRecurseNew varsTo stateBitSize currentNewBlockNum transitionBDDs partitionBDD = do
......@@ -663,18 +686,19 @@ refineRecurseNew varsTo stateBitSize currentNewBlockNum transitionBDDs partition
bddToArray :: PrimMonad m => BDD -> m [Int]
bddToArray bdd =
if bdd == sylvanFalse
then return [0]
else if bdd == sylvanTrue
then return [1]
else do
c <- getvar bdd
v1 <- getlow bdd
v2 <- gethigh bdd
low <- bddToArray v1
high <- bddToArray v2
return ([(fromIntegral c)] ++ low ++ high)
bddToArray bdd = do
v <- isleaf bdd
if v == 1
then do
val <- getvalue bdd
return [val]
else do
c <- getvar bdd
v1 <- getlow bdd
v2 <- gethigh bdd
low <- bddToArray v1
high <- bddToArray v2
return ([(fromIntegral c)] ++ low ++ high)
-- The following duplicates a lot of code, because the existing machinery is
-- tied to the `Suitable` class, which doesn't imply `SymSuitable`
......@@ -769,4 +793,4 @@ parseCoalgebraSymbolically config name input =
where functorParsers = map someSymFunctorExprParser (L.sortBy (flip compare `on` symDynPrecedence) registeredSymFunctors)
--debug = flip trace
debug = flip trace
src/sylvan-haskell/Sylvan.hs
View file @ 610ba2ed
......@@ -109,53 +109,101 @@ foreign import ccall safe "sylvan_gc_disable"
gcDisable :: PrimMonad m => m ()
gcDisable = unsafePrimToPrim c_gcDisable
neg :: BDD -> BDD
neg (BDD x) = BDD $ xor c_sylvanComplement x
foreign import ccall safe "mtbdd_neg_stub"
c_neg :: CBDD -> IO CBDD
foreign import ccall safe "sylvan_ite_stub"
c_ite :: CBDD -> CBDD -> CBDD -> IO CBDD
neg :: PrimMonad m => BDD -> m BDD
neg (BDD x) = liftM BDD $ unsafePrimToPrim $ c_neg x
ite :: PrimMonad m => BDD -> BDD -> BDD -> m BDD
ite (BDD a) (BDD b) (BDD c) = liftM BDD $ unsafePrimToPrim $ c_ite a b c
foreign import ccall safe "mtbdd_cmpl_stub"
c_cmpl :: CBDD -> IO CBDD
foreign import ccall safe "sylvan_xor_stub"
c_xor :: CBDD -> CBDD -> IO CBDD
cmpl :: PrimMonad m => BDD -> m BDD
cmpl (BDD x) = liftM BDD $ unsafePrimToPrim $ c_cmpl x
bxor :: PrimMonad m => BDD -> BDD -> m BDD
bxor (BDD a) (BDD b) = liftM BDD $ unsafePrimToPrim $ c_xor a b
comp :: BDD -> BDD
comp (BDD x) = BDD $ xor c_sylvanComplement x
bequiv :: PrimMonad m => BDD -> BDD -> m BDD
bequiv a b = liftM neg $ bxor a b
foreign import ccall safe "mtbdd_ite_stub"
c_ite :: CBDD -> CBDD -> CBDD -> IO CBDD
ite :: PrimMonad m => BDD -> BDD -> BDD -> m BDD
ite (BDD a) (BDD b) (BDD c) = liftM BDD $ unsafePrimToPrim $ c_ite a b c
foreign import ccall safe "sylvan_and_stub"
foreign import ccall safe "mtbdd_and_stub"
c_and :: CBDD -> CBDD -> IO CBDD
band :: PrimMonad m => BDD -> BDD -> m BDD
band (BDD a) (BDD b) = liftM BDD $ unsafePrimToPrim $ c_and a b
bor :: PrimMonad m => BDD -> BDD -> m BDD
bor a b = liftM neg $ band (neg a) (neg b)
bor a b = liftM comp $ band (comp a) (comp b)
bnand :: PrimMonad m => BDD -> BDD -> m BDD
bnand a b = liftM neg $ band a b
bnand a b = liftM comp $ band a b
bnor :: PrimMonad m => BDD -> BDD -> m BDD
bnor a b = liftM neg $ bor a b
bnor a b = liftM comp $ bor a b
bimp :: PrimMonad m => BDD -> BDD -> m BDD
bimp a b = liftM neg $ band a (neg b)
bimp a b = liftM comp $ band a (comp b)
bimpinv :: PrimMonad m => BDD -> BDD -> m BDD
bimpinv a b = liftM neg $ band (neg a) b
bimpinv a b = liftM comp $ band (comp a) b
biimp :: PrimMonad m => BDD -> BDD -> m BDD
biimp = bequiv
biimp = bddequiv
diff :: PrimMonad m => BDD -> BDD -> m BDD
diff a b = band a (neg b)
diff a b = band a (comp b)
less :: PrimMonad m => BDD -> BDD -> m BDD
less a b = band (neg a) b
less a b = band (comp a) b
foreign import ccall safe "sylvan_xor_stub"
c_xor :: CBDD -> CBDD -> IO CBDD
bddxor :: PrimMonad m => BDD -> BDD -> m BDD
bddxor (BDD a) (BDD b) = liftM BDD $ unsafePrimToPrim $ c_xor a b
bddequiv :: PrimMonad m => BDD -> BDD -> m BDD
bddequiv a b = liftM comp $ bddxor a b
foreign import ccall safe "mtbdd_plus_stub"
c_plus :: CBDD -> CBDD -> IO CBDD
bplus :: PrimMonad m => BDD -> BDD -> m BDD
bplus (BDD a) (BDD b) = liftM BDD $ unsafePrimToPrim $ c_plus a b
--bplusor :: PrimMonad m => BDD -> BDD -> m BDD
--bplusor a b = liftM comp $ bplus (comp a) (comp b)
foreign import ccall safe "mtbdd_minus_stub"
c_minus :: CBDD -> CBDD -> IO CBDD
bminus :: PrimMonad m => BDD -> BDD -> m BDD
bminus (BDD a) (BDD b) = liftM BDD $ unsafePrimToPrim $ c_minus a b
--bminusor :: PrimMonad m => BDD -> BDD -> m BDD
--bminusor a b = liftM comp $ bminus (comp a) (comp b)
foreign import ccall safe "mtbdd_min_stub"
c_min :: CBDD -> CBDD -> IO CBDD
bmin :: PrimMonad m => BDD -> BDD -> m BDD
bmin (BDD a) (BDD b) = liftM BDD $ unsafePrimToPrim $ c_min a b
--bminor :: PrimMonad m => BDD -> BDD -> m BDD
--bminor a b = liftM comp $ bmin (comp a) (comp b)
foreign import ccall safe "mtbdd_max_stub"
c_max :: CBDD -> CBDD -> IO CBDD
bmax :: PrimMonad m => BDD -> BDD -> m BDD
bmax (BDD a) (BDD b) = liftM BDD $ unsafePrimToPrim $ c_max a b
--bmaxor :: PrimMonad m => BDD -> BDD -> m BDD
--bmaxor a b = liftM comp $ bmax (comp a) (comp b)
foreign import ccall safe "sylvan_exists_stub"
c_exists :: CBDD -> CBDD -> IO CBDD
......@@ -164,19 +212,19 @@ exists :: PrimMonad m => BDD -> BDD -> m BDD
exists (BDD a) (BDD variables) = liftM BDD $ unsafePrimToPrim $ c_exists a variables
forall :: PrimMonad m => BDD -> BDD -> m BDD
forall a variables = liftM neg $ exists (neg a) variables
forall a variables = liftM comp $ exists (comp a) variables
foreign import ccall safe "sylvan_and_exists_stub"
c_and_exists :: CBDD -> CBDD -> CBDD -> IO CBDD
andExists :: PrimMonad m => BDD -> BDD -> BDD -> m BDD
andExists (BDD a) (BDD b) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_and_exists a b vars
bddAndExists :: PrimMonad m => BDD -> BDD -> BDD -> m BDD
bddAndExists (BDD a) (BDD b) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_and_exists a b vars
foreign import ccall safe "sylvan_mtbdd_and_exists_stub"
foreign import ccall safe "mtbdd_and_exists_stub"
c_mtbbd_and_exists :: CBDD -> CBDD -> CBDD -> IO CBDD
mtbddAndExists :: PrimMonad m => BDD -> BDD -> BDD -> m BDD
mtbddAndExists (BDD a) (BDD b) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_mtbbd_and_exists a b vars
andExists :: PrimMonad m => BDD -> BDD -> BDD -> m BDD
andExists (BDD a) (BDD b) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_mtbbd_and_exists a b vars
foreign import ccall safe "mtbdd_set_from_array"
c_setFromArray :: Ptr CBDDVar -> CSize -> IO CBDD
......@@ -198,8 +246,8 @@ mapAdd (BDDMap m) var (BDD x) = liftM BDDMap $ unsafePrimToPrim $ c_mapAdd m (fr
foreign import ccall safe "sylvan_compose_stub"
c_compose :: CBDD -> CBDDMap -> IO CBDD
compose :: PrimMonad m => BDD -> BDDMap -> m BDD
compose (BDD f) (BDDMap m) = liftM BDD $ unsafePrimToPrim $ c_compose f m
bddCompose :: PrimMonad m => BDD -> BDDMap -> m BDD
bddCompose (BDD f) (BDDMap m) = liftM BDD $ unsafePrimToPrim $ c_compose f m
foreign import ccall safe "mtbdd_getvar"
c_getvar :: CBDD -> IO (CUInt)
......@@ -207,6 +255,18 @@ foreign import ccall safe "mtbdd_getvar"
getvar :: PrimMonad m => BDD -> m BDDVar
getvar (BDD bdd) = fmap fromIntegral $ unsafePrimToPrim $ c_getvar bdd
foreign import ccall safe "mtbdd_getvalue"
c_getvalue :: CBDD -> IO (CULong)
getvalue :: PrimMonad m => BDD -> m Int
getvalue (BDD bdd) = fmap fromIntegral $ unsafePrimToPrim $ c_getvalue bdd
foreign import ccall safe "mtbdd_isleaf"
c_isleaf :: CBDD -> IO (CUInt)
isleaf :: PrimMonad m => BDD -> m Int
isleaf (BDD bdd) = fmap fromIntegral $ unsafePrimToPrim $ c_isleaf bdd
foreign import ccall safe "mtbdd_getlow"
c_getlow :: CBDD -> IO (CBDD)
......@@ -244,17 +304,29 @@ foreign import ccall safe "mtbdd_fraction"
makefractionleaf :: PrimMonad m => Word64 -> Word64 -> m BDD
makefractionleaf n d = liftM BDD $ unsafePrimToPrim $ c_makefractionleaf (fromIntegral n) (fromIntegral d)
foreign import ccall safe "sylvan_mtbdd_abstract_min_stub"
foreign import ccall safe "mtbdd_abstract_min_stub"
c_mtbdd_abstract_min :: CBDD -> CBDD -> IO CBDD
mtbddAbstractMin :: PrimMonad m => BDD -> BDD -> m BDD
mtbddAbstractMin (BDD a) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_mtbdd_abstract_min a vars
abstractMin :: PrimMonad m => BDD -> BDD -> m BDD
abstractMin (BDD a) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_mtbdd_abstract_min a vars
foreign import ccall safe "sylvan_mtbdd_abstract_max_stub"
foreign import ccall safe "mtbdd_abstract_max_stub"
c_mtbdd_abstract_max :: CBDD -> CBDD -> IO CBDD
mtbddAbstractMax :: PrimMonad m => BDD -> BDD -> m BDD
mtbddAbstractMax (BDD a) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_mtbdd_abstract_max a vars
abstractMax :: PrimMonad m => BDD -> BDD -> m BDD
abstractMax (BDD a) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_mtbdd_abstract_max a vars
foreign import ccall safe "mtbdd_abstract_plus_stub"
c_mtbdd_abstract_plus :: CBDD -> CBDD -> IO CBDD
abstractPlus :: PrimMonad m => BDD -> BDD -> m BDD
abstractPlus (BDD a) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_mtbdd_abstract_plus a vars
foreign import ccall safe "mtbdd_abstract_times_stub"
c_mtbdd_abstract_times :: CBDD -> CBDD -> IO CBDD
abstractTimes :: PrimMonad m => BDD -> BDD -> m BDD
abstractTimes (BDD a) (BDD vars) = liftM BDD $ unsafePrimToPrim $ c_mtbdd_abstract_times a vars
----TODO: doesnt seem to exist
--foreign import ccall safe "sylvan_report_stats"
......
src/sylvan-haskell/stubs.c
View file @ 610ba2ed
#include <sylvan.h>
BDD sylvan_ite_stub(BDD a, BDD b, BDD c){
BDD mtbdd_ite_stub(BDD a, BDD b, BDD c){
LACE_ME;
return mtbdd_ite(a, b, c);
}
BDD sylvan_and_stub(BDD a, BDD b){
BDD mtbdd_neg_stub(BDD a){
LACE_ME;
return mtbdd_negate(a);
}
BDD mtbdd_cmpl_stub(BDD a){
LACE_ME;
return mtbdd_cmpl(a);
}
BDD mtbdd_and_stub(BDD a, BDD b){
LACE_ME;
return mtbdd_times(a, b);
}
BDD mtbdd_plus_stub(BDD a, BDD b){
LACE_ME;
return mtbdd_plus(a, b);
}
BDD mtbdd_minus_stub(BDD a, BDD b){
LACE_ME;
return mtbdd_minus(a, b);
}
BDD mtbdd_max_stub(BDD a, BDD b){
LACE_ME;
return mtbdd_max(a, b);
}
BDD mtbdd_min_stub(BDD a, BDD b){
LACE_ME;
return mtbdd_min(a, b);
}
BDD sylvan_xor_stub(BDD a, BDD b){
LACE_ME;
return sylvan_xor(a, b);
......@@ -25,17 +56,27 @@ BDD sylvan_and_exists_stub(BDD a, BDD b, BDD variables){
return sylvan_and_exists(a, b, variables);
}
BDD sylvan_mtbdd_and_exists_stub(BDD a, BDD b, BDD variables){
BDD mtbdd_and_exists_stub(BDD a, BDD b, BDD variables){
LACE_ME;
return mtbdd_and_exists(a, b, variables);
}
BDD sylvan_mtbdd_abstract_min_stub(BDD a, BDD variables){
BDD mtbdd_abstract_plus_stub(BDD a, BDD variables){
LACE_ME;
return mtbdd_abstract_plus(a, variables);
}
BDD mtbdd_abstract_times_stub(BDD a, BDD variables){
LACE_ME;
return mtbdd_abstract_times(a, variables);
}
BDD mtbdd_abstract_min_stub(BDD a, BDD variables){
LACE_ME;
return mtbdd_abstract_min(a, variables);
}
BDD sylvan_mtbdd_abstract_max_stub(BDD a, BDD variables){
BDD mtbdd_abstract_max_stub(BDD a, BDD variables){
LACE_ME;
return mtbdd_abstract_max(a, variables);
}
......@@ -50,3 +91,8 @@ void sylvan_gc_stub(){
sylvan_gc();
}
struct ComplexNumber
{
float imag;
float real;
};
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment