{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
----------------------------------------------------------------------
-- |
-- Module      :  Data.DecisionDiagram.BDD
-- Copyright   :  (c) Masahiro Sakai 2021
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  unstable
-- Portability :  non-portable
--
-- Reduced Ordered Binary Decision Diagrams (ROBDD).
--
-- References:
--
-- * Bryant, "Graph-Based Algorithms for Boolean Function Manipulation,"
--   in IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691,
--   Aug. 1986, doi: [10.1109/TC.1986.1676819](https://doi.org/10.1109/TC.1986.1676819).
--   <https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf>
--
----------------------------------------------------------------------
module Data.DecisionDiagram.BDD
  (
  -- * The BDD type
    BDD (Leaf, Branch)

  -- * Item ordering
  , ItemOrder (..)
  , AscOrder
  , DescOrder
  , withDefaultOrder
  , withAscOrder
  , withDescOrder
  , withCustomOrder

  -- * Boolean operations
  , true
  , false
  , var
  , notB
  , (.&&.)
  , (.||.)
  , xor
  , (.=>.)
  , (.<=>.)
  , ite
  , andB
  , orB

  -- * Pseudo-boolean constraints
  , pbAtLeast
  , pbAtMost
  , pbExactly
  , pbExactlyIntegral

  -- * Quantification
  , forAll
  , exists
  , existsUnique
  , forAllSet
  , existsSet
  , existsUniqueSet

  -- * Query
  , support
  , evaluate
  , numNodes

  -- * Restriction / Cofactor
  , restrict
  , restrictSet
  , restrictLaw

  -- * Substition / Composition
  , subst
  , substSet

  -- * Satisfiability
  , anySat
  , allSat
  , anySatComplete
  , allSatComplete
  , countSat
  , uniformSatM

  -- * (Co)algebraic structure
  , Sig (..)
  , inSig
  , outSig

  -- * Fold
  , fold
  , fold'

  -- * Unfold
  , unfoldHashable
  , unfoldOrd

  -- * Fixpoints
  , lfp
  , gfp

  -- * Conversion from/to graphs
  , Graph
  , toGraph
  , toGraph'
  , fromGraph
  , fromGraph'
  ) where

import Control.Exception (assert)
import Control.Monad
#if !MIN_VERSION_mwc_random(0,15,0)
import Control.Monad.Primitive
#endif
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Data.Bits (Bits (shiftL))
import qualified Data.Foldable as Foldable
import Data.Function (on)
import Data.Hashable
import qualified Data.HashMap.Lazy as HashMap
import qualified Data.HashTable.Class as H
import qualified Data.HashTable.ST.Cuckoo as C
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List (sortBy)
import Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map
import Data.Proxy
import Data.Ratio
import qualified Data.Vector as V
import GHC.Stack
import Numeric.Natural
#if MIN_VERSION_mwc_random(0,15,0)
import System.Random.MWC (Uniform (..))
import System.Random.Stateful (StatefulGen (..))
#else
import System.Random.MWC (Gen, Variate (..))
#endif
import System.Random.MWC.Distributions (bernoulli)
import Text.Read

import Data.DecisionDiagram.BDD.Internal.ItemOrder
import Data.DecisionDiagram.BDD.Internal.Node (Sig (..), Graph)
import qualified Data.DecisionDiagram.BDD.Internal.Node as Node

infixr 3 .&&.
infixr 2 .||.
infixr 1 .=>.
infix 1 .<=>.

-- ------------------------------------------------------------------------

defaultTableSize :: Int
defaultTableSize :: Int
defaultTableSize = Int
256

-- ------------------------------------------------------------------------

-- | Reduced ordered binary decision diagram representing boolean function
newtype BDD a = BDD Node.Node
  deriving (BDD a -> BDD a -> Bool
(BDD a -> BDD a -> Bool) -> (BDD a -> BDD a -> Bool) -> Eq (BDD a)
forall a. BDD a -> BDD a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BDD a -> BDD a -> Bool
$c/= :: forall a. BDD a -> BDD a -> Bool
== :: BDD a -> BDD a -> Bool
$c== :: forall a. BDD a -> BDD a -> Bool
Eq, Eq (BDD a)
Eq (BDD a)
-> (Int -> BDD a -> Int) -> (BDD a -> Int) -> Hashable (BDD a)
Int -> BDD a -> Int
BDD a -> Int
forall a. Eq (BDD a)
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall a. Int -> BDD a -> Int
forall a. BDD a -> Int
hash :: BDD a -> Int
$chash :: forall a. BDD a -> Int
hashWithSalt :: Int -> BDD a -> Int
$chashWithSalt :: forall a. Int -> BDD a -> Int
$cp1Hashable :: forall a. Eq (BDD a)
Hashable)

pattern F :: BDD a
pattern $bF :: BDD a
$mF :: forall r a. BDD a -> (Void# -> r) -> (Void# -> r) -> r
F = Leaf False

pattern T :: BDD a
pattern $bT :: BDD a
$mT :: forall r a. BDD a -> (Void# -> r) -> (Void# -> r) -> r
T = Leaf True

pattern Leaf :: Bool -> BDD a
pattern $bLeaf :: Bool -> BDD a
$mLeaf :: forall r a. BDD a -> (Bool -> r) -> (Void# -> r) -> r
Leaf b = BDD (Node.Leaf b)

-- | Smart constructor that takes the BDD reduction rules into account
pattern Branch :: Int -> BDD a -> BDD a -> BDD a
pattern $bBranch :: Int -> BDD a -> BDD a -> BDD a
$mBranch :: forall r a.
BDD a -> (Int -> BDD a -> BDD a -> r) -> (Void# -> r) -> r
Branch x lo hi <- BDD (Node.Branch x (BDD -> lo) (BDD -> hi)) where
  Branch Int
x (BDD Node
lo) (BDD Node
hi)
    | Node
lo Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
== Node
hi = Node -> BDD a
forall a. Node -> BDD a
BDD Node
lo
    | Bool
otherwise = Node -> BDD a
forall a. Node -> BDD a
BDD (Int -> Node -> Node -> Node
Node.Branch Int
x Node
lo Node
hi)

{-# COMPLETE T, F, Branch #-}
{-# COMPLETE Leaf, Branch #-}

nodeId :: BDD a -> Int
nodeId :: BDD a -> Int
nodeId (BDD Node
node) = Node -> Int
Node.nodeId Node
node

data BDDCase2 a
  = BDDCase2LT Int (BDD a) (BDD a)
  | BDDCase2GT Int (BDD a) (BDD a)
  | BDDCase2EQ Int (BDD a) (BDD a) (BDD a) (BDD a)
  | BDDCase2EQ2 Bool Bool

bddCase2 :: forall a. ItemOrder a => Proxy a -> BDD a -> BDD a -> BDDCase2 a
bddCase2 :: Proxy a -> BDD a -> BDD a -> BDDCase2 a
bddCase2 Proxy a
_ (Branch Int
ptop BDD a
p0 BDD a
p1) (Branch Int
qtop BDD a
q0 BDD a
q1) =
  case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
ptop Int
qtop of
    Ordering
LT -> Int -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDDCase2 a
BDDCase2LT Int
ptop BDD a
p0 BDD a
p1
    Ordering
GT -> Int -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDDCase2 a
BDDCase2GT Int
qtop BDD a
q0 BDD a
q1
    Ordering
EQ -> Int -> BDD a -> BDD a -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDD a -> BDD a -> BDDCase2 a
BDDCase2EQ Int
ptop BDD a
p0 BDD a
p1 BDD a
q0 BDD a
q1
bddCase2 Proxy a
_ (Branch Int
ptop BDD a
p0 BDD a
p1) BDD a
_ = Int -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDDCase2 a
BDDCase2LT Int
ptop BDD a
p0 BDD a
p1
bddCase2 Proxy a
_ BDD a
_ (Branch Int
qtop BDD a
q0 BDD a
q1) = Int -> BDD a -> BDD a -> BDDCase2 a
forall a. Int -> BDD a -> BDD a -> BDDCase2 a
BDDCase2GT Int
qtop BDD a
q0 BDD a
q1
bddCase2 Proxy a
_ (Leaf Bool
b1) (Leaf Bool
b2) = Bool -> Bool -> BDDCase2 a
forall a. Bool -> Bool -> BDDCase2 a
BDDCase2EQ2 Bool
b1 Bool
b2

level :: BDD a -> Level a
level :: BDD a -> Level a
level (Branch Int
x BDD a
_ BDD a
_) = Int -> Level a
forall a. Int -> Level a
NonTerminal Int
x
level (Leaf Bool
_) = Level a
forall a. Level a
Terminal

-- ------------------------------------------------------------------------

instance Show (BDD a) where
  showsPrec :: Int -> BDD a -> ShowS
showsPrec Int
d BDD a
a   = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"fromGraph " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Graph Sig, Int) -> ShowS
forall a. Show a => a -> ShowS
shows (BDD a -> (Graph Sig, Int)
forall a. BDD a -> (Graph Sig, Int)
toGraph BDD a
a)

instance Read (BDD a) where
  readPrec :: ReadPrec (BDD a)
readPrec = ReadPrec (BDD a) -> ReadPrec (BDD a)
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec (BDD a) -> ReadPrec (BDD a))
-> ReadPrec (BDD a) -> ReadPrec (BDD a)
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec (BDD a) -> ReadPrec (BDD a)
forall a. Int -> ReadPrec a -> ReadPrec a
prec Int
10 (ReadPrec (BDD a) -> ReadPrec (BDD a))
-> ReadPrec (BDD a) -> ReadPrec (BDD a)
forall a b. (a -> b) -> a -> b
$ do
    Ident String
"fromGraph" <- ReadPrec Lexeme
lexP
    (Graph Sig, Int)
gv <- ReadPrec (Graph Sig, Int)
forall a. Read a => ReadPrec a
readPrec
    BDD a -> ReadPrec (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Graph Sig, Int) -> BDD a
forall a. HasCallStack => (Graph Sig, Int) -> BDD a
fromGraph (Graph Sig, Int)
gv)

  readListPrec :: ReadPrec [BDD a]
readListPrec = ReadPrec [BDD a]
forall a. Read a => ReadPrec [a]
readListPrecDefault

-- ------------------------------------------------------------------------

-- | True
true :: BDD a
true :: BDD a
true = BDD a
forall a. BDD a
T

-- | False
false :: BDD a
false :: BDD a
false = BDD a
forall a. BDD a
F

-- | A variable \(x_i\)
var :: Int -> BDD a
var :: Int -> BDD a
var Int
ind = Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind BDD a
forall a. BDD a
F BDD a
forall a. BDD a
T

-- | Negation of a boolean function
notB :: BDD a -> BDD a
notB :: BDD a -> BDD a
notB BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f (Leaf Bool
b) = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> BDD a
forall a. Bool -> BDD a
Leaf (Bool -> Bool
not Bool
b))
      f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> ST s (BDD a)
f BDD a
bdd

apply :: forall a. ItemOrder a => Bool -> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
apply :: Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
apply Bool
isCommutative BDD a -> BDD a -> Maybe (BDD a)
func BDD a
bdd1 BDD a
bdd2 = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
isCommutative BDD a -> BDD a -> Maybe (BDD a)
func
  BDD a -> BDD a -> ST s (BDD a)
op BDD a
bdd1 BDD a
bdd2

mkApplyOp :: forall a s. ItemOrder a => Bool -> (BDD a -> BDD a -> Maybe (BDD a)) -> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp :: Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
isCommutative BDD a -> BDD a -> Maybe (BDD a)
func = do
  HashTable s (BDD a, BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a, BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> BDD a -> ST s (BDD a)
f BDD a
a BDD a
b | Just BDD a
c <- BDD a -> BDD a -> Maybe (BDD a)
func BDD a
a BDD a
b = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
c
      f BDD a
n1 BDD a
n2 = do
        let key :: (BDD a, BDD a)
key = if Bool
isCommutative Bool -> Bool -> Bool
&& BDD a -> Int
forall a. BDD a -> Int
nodeId BDD a
n2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< BDD a -> Int
forall a. BDD a -> Int
nodeId BDD a
n1 then (BDD a
n2, BDD a
n1) else (BDD a
n1, BDD a
n2)
        Maybe (BDD a)
m <- HashTable s (BDD a, BDD a) (BDD a)
-> (BDD a, BDD a) -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a, BDD a) (BDD a)
h (BDD a, BDD a)
key
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> BDD a -> BDD a -> BDDCase2 a
forall a. ItemOrder a => Proxy a -> BDD a -> BDD a -> BDDCase2 a
bddCase2 (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) BDD a
n1 BDD a
n2 of
              BDDCase2GT Int
x2 BDD a
lo2 BDD a
hi2 -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
n1 BDD a
lo2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
n1 BDD a
hi2)
              BDDCase2LT Int
x1 BDD a
lo1 BDD a
hi1 -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x1) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
n2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
n2)
              BDDCase2EQ Int
x BDD a
lo1 BDD a
hi1 BDD a
lo2 BDD a
hi2 -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
lo2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
hi2)
              BDDCase2EQ2 Bool
_ Bool
_ -> String -> ST s (BDD a)
forall a. HasCallStack => String -> a
error String
"apply: should not happen"
            HashTable s (BDD a, BDD a) (BDD a)
-> (BDD a, BDD a) -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a, BDD a) (BDD a)
h (BDD a, BDD a)
key BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  (BDD a -> BDD a -> ST s (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a -> BDD a -> ST s (BDD a)
f

-- | Conjunction of two boolean function
(.&&.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.&&. :: BDD a -> BDD a -> BDD a
(.&&.) BDD a
bdd1 BDD a
bdd2 = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp
  BDD a -> BDD a -> ST s (BDD a)
op BDD a
bdd1 BDD a
bdd2

mkAndOp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp :: ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp = Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
True BDD a -> BDD a -> Maybe (BDD a)
forall a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
T BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
b
    f BDD a
F BDD a
_ = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
F
    f BDD a
a BDD a
T = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
_ BDD a
F = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
F
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | Disjunction of two boolean function
(.||.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.||. :: BDD a -> BDD a -> BDD a
(.||.) BDD a
bdd1 BDD a
bdd2 = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp
  BDD a -> BDD a -> ST s (BDD a)
op BDD a
bdd1 BDD a
bdd2

mkOrOp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp :: ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp = Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
True BDD a -> BDD a -> Maybe (BDD a)
forall a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
T BDD a
_ = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
F BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
b
    f BDD a
_ BDD a
T = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
a BDD a
F = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | XOR
xor :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
xor :: BDD a -> BDD a -> BDD a
xor BDD a
bdd1 BDD a
bdd2 = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp
  BDD a -> BDD a -> ST s (BDD a)
op BDD a
bdd1 BDD a
bdd2

mkXOROp :: forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp :: ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp = Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a))
-> ST s (BDD a -> BDD a -> ST s (BDD a))
mkApplyOp Bool
True BDD a -> BDD a -> Maybe (BDD a)
forall a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
F BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
b
    f BDD a
a BDD a
F = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
a
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
F
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | Implication
(.=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.=>. :: BDD a -> BDD a -> BDD a
(.=>.) = Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
forall a.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
apply Bool
False BDD a -> BDD a -> Maybe (BDD a)
forall a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f BDD a
F BDD a
_ = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
T BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
b
    f BDD a
_ BDD a
T = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | Equivalence
(.<=>.) :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
.<=>. :: BDD a -> BDD a -> BDD a
(.<=>.) = Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
forall a.
ItemOrder a =>
Bool
-> (BDD a -> BDD a -> Maybe (BDD a)) -> BDD a -> BDD a -> BDD a
apply Bool
True BDD a -> BDD a -> Maybe (BDD a)
forall a a. BDD a -> BDD a -> Maybe (BDD a)
f
  where
    f :: BDD a -> BDD a -> Maybe (BDD a)
f (Leaf Bool
b1) (Leaf Bool
b2) = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just (Bool -> BDD a
forall a. Bool -> BDD a
Leaf (Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2))
    f BDD a
a BDD a
b | BDD a
a BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
b = BDD a -> Maybe (BDD a)
forall a. a -> Maybe a
Just BDD a
forall a. BDD a
T
    f BDD a
_ BDD a
_ = Maybe (BDD a)
forall a. Maybe a
Nothing

-- | If-then-else
ite :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a -> BDD a
ite :: BDD a -> BDD a -> BDD a -> BDD a
ite BDD a
c' BDD a
t' BDD a
e' = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a, BDD a, BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a, BDD a, BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> BDD a -> BDD a -> ST s (BDD a)
f (Leaf Bool
b) BDD a
t BDD a
e = if Bool
b then BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
t else BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
e
      f BDD a
_ BDD a
t BDD a
e | BDD a
t BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
e = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
t
      f BDD a
c BDD a
t BDD a
e = do
        case [Level a] -> Level a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [BDD a -> Level a
forall a. BDD a -> Level a
level BDD a
c, BDD a -> Level a
forall a. BDD a -> Level a
level BDD a
t, BDD a -> Level a
forall a. BDD a -> Level a
level BDD a
e] of
          Level a
Terminal -> String -> ST s (BDD a)
forall a. HasCallStack => String -> a
error String
"should not happen"
          NonTerminal Int
x -> do
            let key :: (BDD a, BDD a, BDD a)
key = (BDD a
c, BDD a
t, BDD a
e)
            Maybe (BDD a)
m <- HashTable s (BDD a, BDD a, BDD a) (BDD a)
-> (BDD a, BDD a, BDD a) -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a, BDD a, BDD a) (BDD a)
h (BDD a, BDD a, BDD a)
key
            case Maybe (BDD a)
m of
              Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
              Maybe (BDD a)
Nothing -> do
                let (BDD a
c0, BDD a
c1) = case BDD a
c of{ Branch Int
x' BDD a
lo BDD a
hi | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x -> (BDD a
lo, BDD a
hi); BDD a
_ -> (BDD a
c, BDD a
c) }
                    (BDD a
t0, BDD a
t1) = case BDD a
t of{ Branch Int
x' BDD a
lo BDD a
hi | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x -> (BDD a
lo, BDD a
hi); BDD a
_ -> (BDD a
t, BDD a
t) }
                    (BDD a
e0, BDD a
e1) = case BDD a
e of{ Branch Int
x' BDD a
lo BDD a
hi | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x -> (BDD a
lo, BDD a
hi); BDD a
_ -> (BDD a
e, BDD a
e) }
                BDD a
ret <- (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x) (BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
c0 BDD a
t0 BDD a
e0) (BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
c1 BDD a
t1 BDD a
e1)
                HashTable s (BDD a, BDD a, BDD a) (BDD a)
-> (BDD a, BDD a, BDD a) -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a, BDD a, BDD a) (BDD a)
h (BDD a, BDD a, BDD a)
key BDD a
ret
                BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
c' BDD a
t' BDD a
e'

-- | Conjunction of a list of BDDs.
andB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a
andB :: f (BDD a) -> BDD a
andB f (BDD a)
xs = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp
  (BDD a -> BDD a -> ST s (BDD a))
-> BDD a -> f (BDD a) -> ST s (BDD a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM BDD a -> BDD a -> ST s (BDD a)
op BDD a
forall a. BDD a
true f (BDD a)
xs

-- | Disjunction of a list of BDDs.
orB :: forall f a. (Foldable f, ItemOrder a) => f (BDD a) -> BDD a
orB :: f (BDD a) -> BDD a
orB f (BDD a)
xs = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
op <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp
  (BDD a -> BDD a -> ST s (BDD a))
-> BDD a -> f (BDD a) -> ST s (BDD a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM BDD a -> BDD a -> ST s (BDD a)
op BDD a
forall a. BDD a
false f (BDD a)
xs

-- ------------------------------------------------------------------------

-- | Pseudo-boolean constraint, /w1*x1 + w2*x2 + … ≥ k/.
pbAtLeast :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a
pbAtLeast :: IntMap w -> w -> BDD a
pbAtLeast IntMap w
xs w
k0 = ((Int, w) -> Sig (Int, w)) -> (Int, w) -> BDD a
forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd (Int, w) -> Sig (Int, w)
f (Int
0, w
k0)
  where
    xs' :: V.Vector (Int, w)
    xs' :: Vector (Int, w)
xs' = [(Int, w)] -> Vector (Int, w)
forall a. [a] -> Vector a
V.fromList ([(Int, w)] -> Vector (Int, w)) -> [(Int, w)] -> Vector (Int, w)
forall a b. (a -> b) -> a -> b
$ ((Int, w) -> (Int, w) -> Ordering) -> [(Int, w)] -> [(Int, w)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) (Int -> Int -> Ordering)
-> ((Int, w) -> Int) -> (Int, w) -> (Int, w) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, w) -> Int
forall a b. (a, b) -> a
fst) ([(Int, w)] -> [(Int, w)]) -> [(Int, w)] -> [(Int, w)]
forall a b. (a -> b) -> a -> b
$ IntMap w -> [(Int, w)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap w
xs
    ys :: V.Vector (w, w)
    ys :: Vector (w, w)
ys = ((Int, w) -> (w, w) -> (w, w))
-> (w, w) -> Vector (Int, w) -> Vector (w, w)
forall a b. (a -> b -> b) -> b -> Vector a -> Vector b
V.scanr (\(Int
_, w
w) (w
lb,w
ub) -> if w
w w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
0 then (w
lb, w
ubw -> w -> w
forall a. Num a => a -> a -> a
+w
w) else (w
lbw -> w -> w
forall a. Num a => a -> a -> a
+w
w, w
ub)) (w
0,w
0) Vector (Int, w)
xs'

    f :: (Int, w) -> Sig (Int, w)
    f :: (Int, w) -> Sig (Int, w)
f (!Int
i, !w
k)
      | Bool -> Bool
not (w
k w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
ub) = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
      | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Int, w) -> Int
forall a. Vector a -> Int
V.length Vector (Int, w)
xs' Bool -> Bool -> Bool
&& w
0 w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
      | w
lb w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True -- all remaining variables are don't-care
      | Bool
otherwise = Int -> (Int, w) -> (Int, w) -> Sig (Int, w)
forall a. Int -> a -> a -> Sig a
SBranch Int
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
k) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
kw -> w -> w
forall a. Num a => a -> a -> a
-w
w)
      where
        (w
lb,w
ub) = Vector (w, w)
ys Vector (w, w) -> Int -> (w, w)
forall a. Vector a -> Int -> a
V.! Int
i
        (Int
x, w
w) = Vector (Int, w)
xs' Vector (Int, w) -> Int -> (Int, w)
forall a. Vector a -> Int -> a
V.! Int
i

-- | Pseudo-boolean constraint, /w1*x1 + w2*x2 + … ≤ k/.
pbAtMost :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a
pbAtMost :: IntMap w -> w -> BDD a
pbAtMost IntMap w
xs w
k0 = ((Int, w) -> Sig (Int, w)) -> (Int, w) -> BDD a
forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd (Int, w) -> Sig (Int, w)
f (Int
0, w
k0)
  where
    xs' :: V.Vector (Int, w)
    xs' :: Vector (Int, w)
xs' = [(Int, w)] -> Vector (Int, w)
forall a. [a] -> Vector a
V.fromList ([(Int, w)] -> Vector (Int, w)) -> [(Int, w)] -> Vector (Int, w)
forall a b. (a -> b) -> a -> b
$ ((Int, w) -> (Int, w) -> Ordering) -> [(Int, w)] -> [(Int, w)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) (Int -> Int -> Ordering)
-> ((Int, w) -> Int) -> (Int, w) -> (Int, w) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, w) -> Int
forall a b. (a, b) -> a
fst) ([(Int, w)] -> [(Int, w)]) -> [(Int, w)] -> [(Int, w)]
forall a b. (a -> b) -> a -> b
$ IntMap w -> [(Int, w)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap w
xs
    ys :: V.Vector (w, w)
    ys :: Vector (w, w)
ys = ((Int, w) -> (w, w) -> (w, w))
-> (w, w) -> Vector (Int, w) -> Vector (w, w)
forall a b. (a -> b -> b) -> b -> Vector a -> Vector b
V.scanr (\(Int
_, w
w) (w
lb,w
ub) -> if w
w w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
0 then (w
lb, w
ubw -> w -> w
forall a. Num a => a -> a -> a
+w
w) else (w
lbw -> w -> w
forall a. Num a => a -> a -> a
+w
w, w
ub)) (w
0,w
0) Vector (Int, w)
xs'

    f :: (Int, w) -> Sig (Int, w)
    f :: (Int, w) -> Sig (Int, w)
f (!Int
i, !w
k)
      | Bool -> Bool
not (w
lb w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k) = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
      | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Int, w) -> Int
forall a. Vector a -> Int
V.length Vector (Int, w)
xs' Bool -> Bool -> Bool
&& w
0 w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
      | w
ub w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True -- all remaining variables are don't-care
      | Bool
otherwise = Int -> (Int, w) -> (Int, w) -> Sig (Int, w)
forall a. Int -> a -> a -> Sig a
SBranch Int
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
k) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
kw -> w -> w
forall a. Num a => a -> a -> a
-w
w)
      where
        (w
lb,w
ub) = Vector (w, w)
ys Vector (w, w) -> Int -> (w, w)
forall a. Vector a -> Int -> a
V.! Int
i
        (Int
x, w
w) = Vector (Int, w)
xs' Vector (Int, w) -> Int -> (Int, w)
forall a. Vector a -> Int -> a
V.! Int
i

-- | Pseudo-boolean constraint, /w1*x1 + w2*x2 + … = k/.
--
-- If weight type is 'Integral', 'pbExactlyIntegral' is more efficient.
pbExactly :: forall a w. (ItemOrder a, Real w) => IntMap w -> w -> BDD a
pbExactly :: IntMap w -> w -> BDD a
pbExactly IntMap w
xs w
k0 = ((Int, w) -> Sig (Int, w)) -> (Int, w) -> BDD a
forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd (Int, w) -> Sig (Int, w)
f (Int
0, w
k0)
  where
    xs' :: V.Vector (Int, w)
    xs' :: Vector (Int, w)
xs' = [(Int, w)] -> Vector (Int, w)
forall a. [a] -> Vector a
V.fromList ([(Int, w)] -> Vector (Int, w)) -> [(Int, w)] -> Vector (Int, w)
forall a b. (a -> b) -> a -> b
$ ((Int, w) -> (Int, w) -> Ordering) -> [(Int, w)] -> [(Int, w)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) (Int -> Int -> Ordering)
-> ((Int, w) -> Int) -> (Int, w) -> (Int, w) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, w) -> Int
forall a b. (a, b) -> a
fst) ([(Int, w)] -> [(Int, w)]) -> [(Int, w)] -> [(Int, w)]
forall a b. (a -> b) -> a -> b
$ IntMap w -> [(Int, w)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap w
xs
    ys :: V.Vector (w, w)
    ys :: Vector (w, w)
ys = ((Int, w) -> (w, w) -> (w, w))
-> (w, w) -> Vector (Int, w) -> Vector (w, w)
forall a b. (a -> b -> b) -> b -> Vector a -> Vector b
V.scanr (\(Int
_, w
w) (w
lb,w
ub) -> if w
w w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
0 then (w
lb, w
ubw -> w -> w
forall a. Num a => a -> a -> a
+w
w) else (w
lbw -> w -> w
forall a. Num a => a -> a -> a
+w
w, w
ub)) (w
0,w
0) Vector (Int, w)
xs'

    f :: (Int, w) -> Sig (Int, w)
    f :: (Int, w) -> Sig (Int, w)
f (!Int
i, !w
k)
      | Bool -> Bool
not (w
lb w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k Bool -> Bool -> Bool
&& w
k w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
ub) = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
      | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Int, w) -> Int
forall a. Vector a -> Int
V.length Vector (Int, w)
xs' Bool -> Bool -> Bool
&& w
0 w -> w -> Bool
forall a. Eq a => a -> a -> Bool
== w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
      | Bool
otherwise = Int -> (Int, w) -> (Int, w) -> Sig (Int, w)
forall a. Int -> a -> a -> Sig a
SBranch Int
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
k) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
kw -> w -> w
forall a. Num a => a -> a -> a
-w
w)
      where
        (w
lb,w
ub) = Vector (w, w)
ys Vector (w, w) -> Int -> (w, w)
forall a. Vector a -> Int -> a
V.! Int
i
        (Int
x, w
w) = Vector (Int, w)
xs' Vector (Int, w) -> Int -> (Int, w)
forall a. Vector a -> Int -> a
V.! Int
i

-- | Similar to 'pbExactly' but more efficient.
pbExactlyIntegral :: forall a w. (ItemOrder a, Real w, Integral w) => IntMap w -> w -> BDD a
pbExactlyIntegral :: IntMap w -> w -> BDD a
pbExactlyIntegral IntMap w
xs w
k0 = ((Int, w) -> Sig (Int, w)) -> (Int, w) -> BDD a
forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd (Int, w) -> Sig (Int, w)
f (Int
0, w
k0)
  where
    xs' :: V.Vector (Int, w)
    xs' :: Vector (Int, w)
xs' = [(Int, w)] -> Vector (Int, w)
forall a. [a] -> Vector a
V.fromList ([(Int, w)] -> Vector (Int, w)) -> [(Int, w)] -> Vector (Int, w)
forall a b. (a -> b) -> a -> b
$ ((Int, w) -> (Int, w) -> Ordering) -> [(Int, w)] -> [(Int, w)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) (Int -> Int -> Ordering)
-> ((Int, w) -> Int) -> (Int, w) -> (Int, w) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, w) -> Int
forall a b. (a, b) -> a
fst) ([(Int, w)] -> [(Int, w)]) -> [(Int, w)] -> [(Int, w)]
forall a b. (a -> b) -> a -> b
$ IntMap w -> [(Int, w)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap w
xs
    ys :: V.Vector (w, w)
    ys :: Vector (w, w)
ys = ((Int, w) -> (w, w) -> (w, w))
-> (w, w) -> Vector (Int, w) -> Vector (w, w)
forall a b. (a -> b -> b) -> b -> Vector a -> Vector b
V.scanr (\(Int
_, w
w) (w
lb,w
ub) -> if w
w w -> w -> Bool
forall a. Ord a => a -> a -> Bool
>= w
0 then (w
lb, w
ubw -> w -> w
forall a. Num a => a -> a -> a
+w
w) else (w
lbw -> w -> w
forall a. Num a => a -> a -> a
+w
w, w
ub)) (w
0,w
0) Vector (Int, w)
xs'
    ds :: V.Vector w
    ds :: Vector w
ds = (w -> w -> w) -> Vector w -> Vector w
forall a. (a -> a -> a) -> Vector a -> Vector a
V.scanr1 (\w
w w
d -> if w
w w -> w -> Bool
forall a. Eq a => a -> a -> Bool
/= w
0 then w -> w -> w
forall a. Integral a => a -> a -> a
gcd w
w w
d else w
d) (((Int, w) -> w) -> Vector (Int, w) -> Vector w
forall a b. (a -> b) -> Vector a -> Vector b
V.map (Int, w) -> w
forall a b. (a, b) -> b
snd Vector (Int, w)
xs')

    f :: (Int, w) -> Sig (Int, w)
    f :: (Int, w) -> Sig (Int, w)
f (!Int
i, !w
k)
      | Bool -> Bool
not (w
lb w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
k Bool -> Bool -> Bool
&& w
k w -> w -> Bool
forall a. Ord a => a -> a -> Bool
<= w
ub) = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
      | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (Int, w) -> Int
forall a. Vector a -> Int
V.length Vector (Int, w)
xs' Bool -> Bool -> Bool
&& w
0 w -> w -> Bool
forall a. Eq a => a -> a -> Bool
== w
k = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
True
      | w
d w -> w -> Bool
forall a. Eq a => a -> a -> Bool
/= w
0 Bool -> Bool -> Bool
&& w
k w -> w -> w
forall a. Integral a => a -> a -> a
`mod` w
d w -> w -> Bool
forall a. Eq a => a -> a -> Bool
/= w
0 = Bool -> Sig (Int, w)
forall a. Bool -> Sig a
SLeaf Bool
False
      | Bool
otherwise = Int -> (Int, w) -> (Int, w) -> Sig (Int, w)
forall a. Int -> a -> a -> Sig a
SBranch Int
x (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
k) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, w
kw -> w -> w
forall a. Num a => a -> a -> a
-w
w)
      where
        (w
lb,w
ub) = Vector (w, w)
ys Vector (w, w) -> Int -> (w, w)
forall a. Vector a -> Int -> a
V.! Int
i
        (Int
x, w
w) = Vector (Int, w)
xs' Vector (Int, w) -> Int -> (Int, w)
forall a. Vector a -> Int -> a
V.! Int
i
        d :: w
d = Vector w
ds Vector w -> Int -> w
forall a. Vector a -> Int -> a
V.! Int
i

-- ------------------------------------------------------------------------

-- | Universal quantification (∀)
forAll :: forall a. ItemOrder a => Int -> BDD a -> BDD a
forAll :: Int -> BDD a -> BDD a
forAll Int
x BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
andOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- if Int
ind Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x
                   then BDD a -> BDD a -> ST s (BDD a)
andOp BDD a
lo BDD a
hi
                   else (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  BDD a -> ST s (BDD a)
f BDD a
bdd

-- | Existential quantification (∃)
exists :: forall a. ItemOrder a => Int -> BDD a -> BDD a
exists :: Int -> BDD a -> BDD a
exists Int
x BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
orOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- if Int
ind Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x
                   then BDD a -> BDD a -> ST s (BDD a)
orOp BDD a
lo BDD a
hi
                   else (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  BDD a -> ST s (BDD a)
f BDD a
bdd

-- | Unique existential quantification (∃!)
existsUnique :: forall a. ItemOrder a => Int -> BDD a -> BDD a
existsUnique :: Int -> BDD a -> BDD a
existsUnique Int
x BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
xorOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
ind Int
x of
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
              Ordering
EQ -> BDD a -> BDD a -> ST s (BDD a)
xorOp BDD a
lo BDD a
hi
              Ordering
GT -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f BDD a
_ = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
  BDD a -> ST s (BDD a)
f BDD a
bdd

-- | Universal quantification (∀) over a set of variables
forAllSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a
forAllSet :: IntSet -> BDD a -> BDD a
forAllSet IntSet
vars BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
andOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkAndOp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [Int] -> BDD a -> ST s (BDD a)
f xxs :: [Int]
xxs@(Int
x : [Int]
xs) n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
ind Int
x of
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
lo) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
hi)
              Ordering
EQ -> do
                BDD a
r0 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
lo
                BDD a
r1 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
hi
                BDD a -> BDD a -> ST s (BDD a)
andOp BDD a
r0 BDD a
r1
              Ordering
GT -> [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
n
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f [Int]
_ BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  [Int] -> BDD a -> ST s (BDD a)
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
vars)) BDD a
bdd

-- | Existential quantification (∃) over a set of variables
existsSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a
existsSet :: IntSet -> BDD a -> BDD a
existsSet IntSet
vars BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
orOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkOrOp
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [Int] -> BDD a -> ST s (BDD a)
f xxs :: [Int]
xxs@(Int
x : [Int]
xs) n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
ind Int
x of
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
lo) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
hi)
              Ordering
EQ -> do
                BDD a
r0 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
lo
                BDD a
r1 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
hi
                BDD a -> BDD a -> ST s (BDD a)
orOp BDD a
r0 BDD a
r1
              Ordering
GT -> [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
n
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f [Int]
_ BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  [Int] -> BDD a -> ST s (BDD a)
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
vars)) BDD a
bdd

-- | Unique existential quantification (∃!) over a set of variables
existsUniqueSet :: forall a. ItemOrder a => IntSet -> BDD a -> BDD a
existsUniqueSet :: IntSet -> BDD a -> BDD a
existsUniqueSet IntSet
vars BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> BDD a -> ST s (BDD a)
xorOp <- ST s (BDD a -> BDD a -> ST s (BDD a))
forall a s. ItemOrder a => ST s (BDD a -> BDD a -> ST s (BDD a))
mkXOROp
  HashTable s ([Int], BDD a) (BDD a)
h <- Int -> ST s (HashTable s ([Int], BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [Int] -> BDD a -> ST s (BDD a)
f xxs :: [Int]
xxs@(Int
x : [Int]
xs) n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        let key :: ([Int], BDD a)
key = ([Int]
xxs, BDD a
n)
        Maybe (BDD a)
m <- HashTable s ([Int], BDD a) (BDD a)
-> ([Int], BDD a) -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s ([Int], BDD a) (BDD a)
h ([Int], BDD a)
key
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
ind Int
x of
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
lo) ([Int] -> BDD a -> ST s (BDD a)
f [Int]
xxs BDD a
hi)
              Ordering
EQ -> do
                BDD a
r0 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
lo
                BDD a
r1 <- [Int] -> BDD a -> ST s (BDD a)
f [Int]
xs BDD a
hi
                BDD a -> BDD a -> ST s (BDD a)
xorOp BDD a
r0 BDD a
r1
              Ordering
GT -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
            HashTable s ([Int], BDD a) (BDD a)
-> ([Int], BDD a) -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s ([Int], BDD a) (BDD a)
h ([Int], BDD a)
key BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
      f (Int
_ : [Int]
_) BDD a
_ = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
F
      f [] BDD a
a = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
a
  [Int] -> BDD a -> ST s (BDD a)
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
vars)) BDD a
bdd

-- ------------------------------------------------------------------------

-- | Fold over the graph structure of the BDD.
--
-- It takes two functions that substitute 'Branch'  and 'Leaf' respectively.
--
-- Note that its type is isomorphic to @('Sig' b -> b) -> BDD a -> b@.
fold :: (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold :: (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold Int -> b -> b -> b
br Bool -> b
lf (BDD Node
node) = (Int -> b -> b -> b) -> (Bool -> b) -> Node -> b
forall a. (Int -> a -> a -> a) -> (Bool -> a) -> Node -> a
Node.fold Int -> b -> b -> b
br Bool -> b
lf Node
node

-- | Strict version of 'fold'
fold' :: (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold' :: (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold' Int -> b -> b -> b
br Bool -> b
lf (BDD Node
node) = (Int -> b -> b -> b) -> (Bool -> b) -> Node -> b
forall a. (Int -> a -> a -> a) -> (Bool -> a) -> Node -> a
Node.fold' Int -> b -> b -> b
br Bool -> b
lf Node
node

mkFold'Op :: (Int -> b -> b -> b) -> (Bool -> b) -> ST s (BDD a -> ST s b)
mkFold'Op :: (Int -> b -> b -> b) -> (Bool -> b) -> ST s (BDD a -> ST s b)
mkFold'Op Int -> b -> b -> b
br Bool -> b
lf = do
  Node -> ST s b
op <- (Int -> b -> b -> b) -> (Bool -> b) -> ST s (Node -> ST s b)
forall a s.
(Int -> a -> a -> a) -> (Bool -> a) -> ST s (Node -> ST s a)
Node.mkFold'Op Int -> b -> b -> b
br Bool -> b
lf
  (BDD a -> ST s b) -> ST s (BDD a -> ST s b)
forall (m :: * -> *) a. Monad m => a -> m a
return ((BDD a -> ST s b) -> ST s (BDD a -> ST s b))
-> (BDD a -> ST s b) -> ST s (BDD a -> ST s b)
forall a b. (a -> b) -> a -> b
$ \(BDD Node
node) -> Node -> ST s b
op Node
node

-- ------------------------------------------------------------------------

-- | Top-down construction of BDD, memoising internal states using 'Hashable' instance.
unfoldHashable :: forall a b. (ItemOrder a, Eq b, Hashable b) => (b -> Sig b) -> b -> BDD a
unfoldHashable :: (b -> Sig b) -> b -> BDD a
unfoldHashable b -> Sig b
f b
b = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s b (Sig b)
h <- Int -> ST s (HashTable s b (Sig b))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let g :: [b] -> ST s ()
g [] = () -> ST s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      g (b
x : [b]
xs) = do
        Maybe (Sig b)
r <- HashTable s b (Sig b) -> b -> ST s (Maybe (Sig b))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s b (Sig b)
h b
x
        case Maybe (Sig b)
r of
          Just Sig b
_ -> [b] -> ST s ()
g [b]
xs
          Maybe (Sig b)
Nothing -> do
            let fx :: Sig b
fx = b -> Sig b
f b
x
            HashTable s b (Sig b) -> b -> Sig b -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s b (Sig b)
h b
x Sig b
fx
            [b] -> ST s ()
g ([b]
xs [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ Sig b -> [b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList Sig b
fx)
  [b] -> ST s ()
g [b
b]
  [(b, Sig b)]
xs <- HashTable s b (Sig b) -> ST s [(b, Sig b)]
forall (h :: * -> * -> * -> *) s k v.
HashTable h =>
h s k v -> ST s [(k, v)]
H.toList HashTable s b (Sig b)
h
  let h2 :: HashMap b (BDD a)
h2 = [(b, BDD a)] -> HashMap b (BDD a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList [(b
x, Sig (BDD a) -> BDD a
forall a. Sig (BDD a) -> BDD a
inSig ((b -> BDD a) -> Sig b -> Sig (BDD a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HashMap b (BDD a)
h2 HashMap b (BDD a) -> b -> BDD a
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
HashMap.!) Sig b
s)) | (b
x,Sig b
s) <- [(b, Sig b)]
xs]
  BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (BDD a -> ST s (BDD a)) -> BDD a -> ST s (BDD a)
forall a b. (a -> b) -> a -> b
$ HashMap b (BDD a)
forall a. HashMap b (BDD a)
h2 HashMap b (BDD a) -> b -> BDD a
forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
HashMap.! b
b

-- | Top-down construction of BDD, memoising internal states using 'Ord' instance.
unfoldOrd :: forall a b. (ItemOrder a, Ord b) => (b -> Sig b) -> b -> BDD a
unfoldOrd :: (b -> Sig b) -> b -> BDD a
unfoldOrd b -> Sig b
f b
b = Map b (BDD a)
m2 Map b (BDD a) -> b -> BDD a
forall k a. Ord k => Map k a -> k -> a
Map.! b
b
  where
    m1 :: Map b (Sig b)
    m1 :: Map b (Sig b)
m1 = Map b (Sig b) -> [b] -> Map b (Sig b)
g Map b (Sig b)
forall k a. Map k a
Map.empty [b
b]

    m2 :: Map b (BDD a)
    m2 :: Map b (BDD a)
m2 = (Sig b -> BDD a) -> Map b (Sig b) -> Map b (BDD a)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Sig (BDD a) -> BDD a
forall a. Sig (BDD a) -> BDD a
inSig (Sig (BDD a) -> BDD a) -> (Sig b -> Sig (BDD a)) -> Sig b -> BDD a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> BDD a) -> Sig b -> Sig (BDD a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Map b (BDD a)
m2 Map b (BDD a) -> b -> BDD a
forall k a. Ord k => Map k a -> k -> a
Map.!)) Map b (Sig b)
m1

    g :: Map b (Sig b) -> [b] -> Map b (Sig b)
g Map b (Sig b)
m [] = Map b (Sig b)
m
    g Map b (Sig b)
m (b
x : [b]
xs) =
      case b -> Map b (Sig b) -> Maybe (Sig b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup b
x Map b (Sig b)
m of
        Just Sig b
_ -> Map b (Sig b) -> [b] -> Map b (Sig b)
g Map b (Sig b)
m [b]
xs
        Maybe (Sig b)
Nothing ->
          let fx :: Sig b
fx = b -> Sig b
f b
x
           in Map b (Sig b) -> [b] -> Map b (Sig b)
g (b -> Sig b -> Map b (Sig b) -> Map b (Sig b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert b
x Sig b
fx Map b (Sig b)
m) ([b]
xs [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ Sig b -> [b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList Sig b
fx)

-- ------------------------------------------------------------------------

-- | All the variables that this BDD depends on.
support :: BDD a -> IntSet
support :: BDD a -> IntSet
support BDD a
bdd = (forall s. ST s IntSet) -> IntSet
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s IntSet) -> IntSet)
-> (forall s. ST s IntSet) -> IntSet
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> ST s IntSet
op <- ST s (BDD a -> ST s IntSet)
forall s a. ST s (BDD a -> ST s IntSet)
mkSupportOp
  BDD a -> ST s IntSet
op BDD a
bdd

mkSupportOp :: ST s (BDD a -> ST s IntSet)
mkSupportOp :: ST s (BDD a -> ST s IntSet)
mkSupportOp = (Int -> IntSet -> IntSet -> IntSet)
-> (Bool -> IntSet) -> ST s (BDD a -> ST s IntSet)
forall b s a.
(Int -> b -> b -> b) -> (Bool -> b) -> ST s (BDD a -> ST s b)
mkFold'Op Int -> IntSet -> IntSet -> IntSet
f Bool -> IntSet
forall p. p -> IntSet
g
  where
    f :: Int -> IntSet -> IntSet -> IntSet
f Int
x IntSet
lo IntSet
hi = Int -> IntSet -> IntSet
IntSet.insert Int
x (IntSet
lo IntSet -> IntSet -> IntSet
`IntSet.union` IntSet
hi)
    g :: p -> IntSet
g p
_ = IntSet
IntSet.empty

-- | Evaluate a boolean function represented as BDD under the valuation
-- given by @(Int -> Bool)@, i.e. it lifts a valuation function from
-- variables to BDDs.
evaluate :: (Int -> Bool) -> BDD a -> Bool
evaluate :: (Int -> Bool) -> BDD a -> Bool
evaluate Int -> Bool
f = BDD a -> Bool
forall a. BDD a -> Bool
g
  where
    g :: BDD a -> Bool
g (Leaf Bool
b) = Bool
b
    g (Branch Int
x BDD a
lo BDD a
hi)
      | Int -> Bool
f Int
x = BDD a -> Bool
g BDD a
hi
      | Bool
otherwise = BDD a -> Bool
g BDD a
lo

-- | Count the number of nodes in a BDD viewed as a rooted directed acyclic graph.
--
-- See also 'toGraph'.
numNodes :: BDD a -> Int
numNodes :: BDD a -> Int
numNodes (BDD Node
node) = Node -> Int
Node.numNodes Node
node

-- ------------------------------------------------------------------------

-- | Compute \(F|_{x_i} \) or \(F|_{\neg x_i} \).
--
-- \[
-- F|_{x_i}(\ldots, x_{i-1}, x_{i+1}, \ldots) = F(\ldots, x_{i-1}, \mathrm{True}, x_{i+1}, \ldots)
-- \]
-- \[
-- F|_{\neg x_i}(\ldots, x_{i-1}, x_{i+1}, \ldots) = F(\ldots, x_{i-1}, \mathrm{False}, x_{i+1}, \ldots)
-- \]
restrict :: forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a
restrict :: Int -> Bool -> BDD a -> BDD a
restrict Int
x Bool
val BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> ST s (BDD a)
f n :: BDD a
n@(Leaf Bool
_) = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
      f n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
ind Int
x of
              Ordering
GT -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) (BDD a -> ST s (BDD a)
f BDD a
lo) (BDD a -> ST s (BDD a)
f BDD a
hi)
              Ordering
EQ -> if Bool
val then BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
hi else BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
lo
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> ST s (BDD a)
f BDD a
bdd

-- | Compute \(F|_{\{x_i = v_i\}_i} \).
restrictSet :: forall a. ItemOrder a => IntMap Bool -> BDD a -> BDD a
restrictSet :: IntMap Bool -> BDD a -> BDD a
restrictSet IntMap Bool
val BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [(Int, Bool)] -> BDD a -> ST s (BDD a)
f [] BDD a
n = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
      f [(Int, Bool)]
_ n :: BDD a
n@(Leaf Bool
_) = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
      f xxs :: [(Int, Bool)]
xxs@((Int
x,Bool
v) : [(Int, Bool)]
xs) n :: BDD a
n@(Branch Int
ind BDD a
lo BDD a
hi) = do
        Maybe (BDD a)
m <- HashTable s (BDD a) (BDD a) -> BDD a -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (BDD a)
h BDD a
n
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
ind Int
x of
              Ordering
GT -> [(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xs BDD a
n
              Ordering
LT -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
ind) ([(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xxs BDD a
lo) ([(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xxs BDD a
hi)
              Ordering
EQ -> if Bool
v then [(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xs BDD a
hi else [(Int, Bool)] -> BDD a -> ST s (BDD a)
f [(Int, Bool)]
xs BDD a
lo
            HashTable s (BDD a) (BDD a) -> BDD a -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (BDD a)
h BDD a
n BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  [(Int, Bool)] -> BDD a -> ST s (BDD a)
f (((Int, Bool) -> (Int, Bool) -> Ordering)
-> [(Int, Bool)] -> [(Int, Bool)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) (Int -> Int -> Ordering)
-> ((Int, Bool) -> Int) -> (Int, Bool) -> (Int, Bool) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, Bool) -> Int
forall a b. (a, b) -> a
fst) (IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Bool
val)) BDD a
bdd

-- | Compute generalized cofactor of F with respect to C.
--
-- Note that C is the first argument.
restrictLaw :: forall a. ItemOrder a => BDD a -> BDD a -> BDD a
restrictLaw :: BDD a -> BDD a -> BDD a
restrictLaw BDD a
law BDD a
bdd = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a, BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a, BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> BDD a -> ST s (BDD a)
f BDD a
T BDD a
n = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
      f BDD a
F BDD a
_ = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
T  -- Is this correct?
      f BDD a
_ n :: BDD a
n@(Leaf Bool
_) = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
n
      f BDD a
n1 BDD a
n2 | BDD a
n1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
n2 = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
forall a. BDD a
T
      f BDD a
n1 BDD a
n2 = do
        Maybe (BDD a)
m <- HashTable s (BDD a, BDD a) (BDD a)
-> (BDD a, BDD a) -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a, BDD a) (BDD a)
h (BDD a
n1, BDD a
n2)
        case Maybe (BDD a)
m of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            BDD a
ret <- case Proxy a -> BDD a -> BDD a -> BDDCase2 a
forall a. ItemOrder a => Proxy a -> BDD a -> BDD a -> BDDCase2 a
bddCase2 (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) BDD a
n1 BDD a
n2 of
              BDDCase2GT Int
x2 BDD a
lo2 BDD a
hi2 -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
n1 BDD a
lo2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
n1 BDD a
hi2)
              BDDCase2EQ Int
x1 BDD a
lo1 BDD a
hi1 BDD a
lo2 BDD a
hi2
                | BDD a
lo1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
forall a. BDD a
F  -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
hi2
                | BDD a
hi1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
forall a. BDD a
F  -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
lo2
                | Bool
otherwise -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x1) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
lo2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
hi2)
              BDDCase2LT Int
x1 BDD a
lo1 BDD a
hi1
                | BDD a
lo1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
forall a. BDD a
F  -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
n2
                | BDD a
hi1 BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
forall a. BDD a
F  -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
n2
                | Bool
otherwise -> (BDD a -> BDD a -> BDD a)
-> ST s (BDD a) -> ST s (BDD a) -> ST s (BDD a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x1) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo1 BDD a
n2) (BDD a -> BDD a -> ST s (BDD a)
f BDD a
hi1 BDD a
n2)
              BDDCase2EQ2 Bool
_ Bool
_ -> String -> ST s (BDD a)
forall a. HasCallStack => String -> a
error String
"restrictLaw: should not happen"
            HashTable s (BDD a, BDD a) (BDD a)
-> (BDD a, BDD a) -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a, BDD a) (BDD a)
h (BDD a
n1, BDD a
n2) BDD a
ret
            BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> BDD a -> ST s (BDD a)
f BDD a
law BDD a
bdd

-- ------------------------------------------------------------------------

-- | @subst x N M@ computes substitution M[x ↦ N].
--
-- Note the order of the arguments.
-- This operation is also known as /Composition/.
subst :: forall a. ItemOrder a => Int -> BDD a -> BDD a -> BDD a
subst :: Int -> BDD a -> BDD a -> BDD a
subst Int
x BDD a
n BDD a
m = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a, BDD a, BDD a) (BDD a)
h <- Int -> ST s (HashTable s (BDD a, BDD a, BDD a) (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: BDD a -> BDD a -> BDD a -> ST s (BDD a)
f (Branch Int
x' BDD a
lo BDD a
_) BDD a
mhi BDD a
n2 | Int
xInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
x' = BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
lo BDD a
mhi BDD a
n2
      f BDD a
mlo (Branch Int
x' BDD a
_ BDD a
hi) BDD a
n2 | Int
xInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
x' = BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
mlo BDD a
hi BDD a
n2
      f BDD a
mlo BDD a
_ BDD a
F = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (BDD a -> ST s (BDD a)) -> BDD a -> ST s (BDD a)
forall a b. (a -> b) -> a -> b
$ Int -> Bool -> BDD a -> BDD a
forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a
restrict Int
x Bool
False BDD a
mlo
      f BDD a
_ BDD a
mhi BDD a
T = BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return (BDD a -> ST s (BDD a)) -> BDD a -> ST s (BDD a)
forall a b. (a -> b) -> a -> b
$ Int -> Bool -> BDD a -> BDD a
forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a
restrict Int
x Bool
True BDD a
mhi
      f BDD a
mlo BDD a
mhi BDD a
n2 = do
        Maybe (BDD a)
u <- HashTable s (BDD a, BDD a, BDD a) (BDD a)
-> (BDD a, BDD a, BDD a) -> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a, BDD a, BDD a) (BDD a)
h (BDD a
mlo, BDD a
mhi, BDD a
n2)
        case Maybe (BDD a)
u of
          Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
          Maybe (BDD a)
Nothing -> do
            case [Level a] -> Level a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ((BDD a -> Level a) -> [BDD a] -> [Level a]
forall a b. (a -> b) -> [a] -> [b]
map BDD a -> Level a
forall a. BDD a -> Level a
level [BDD a
mlo, BDD a
mhi, BDD a
n2]) of
              Level a
Terminal -> String -> ST s (BDD a)
forall a. HasCallStack => String -> a
error String
"should not happen"
              NonTerminal Int
x' -> do
                let (BDD a
mll, BDD a
mlh) =
                      case BDD a
mlo of
                        Branch Int
x'' BDD a
mll' BDD a
mlh' | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x'' -> (BDD a
mll', BDD a
mlh')
                        BDD a
_ -> (BDD a
mlo, BDD a
mlo)
                    (BDD a
mhl, BDD a
mhh) =
                      case BDD a
mhi of
                        Branch Int
x'' BDD a
mhl' BDD a
mhh' | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x'' -> (BDD a
mhl', BDD a
mhh')
                        BDD a
_ -> (BDD a
mhi, BDD a
mhi)
                    (BDD a
n2l, BDD a
n2h) =
                      case BDD a
n2 of
                        Branch Int
x'' BDD a
n2l' BDD a
n2h' | Int
x' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x'' -> (BDD a
n2l', BDD a
n2h')
                        BDD a
_ -> (BDD a
n2, BDD a
n2)
                BDD a
r0 <- BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
mll BDD a
mhl BDD a
n2l
                BDD a
r1 <- BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
mlh BDD a
mhh BDD a
n2h
                let ret :: BDD a
ret = Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x' BDD a
r0 BDD a
r1
                HashTable s (BDD a, BDD a, BDD a) (BDD a)
-> (BDD a, BDD a, BDD a) -> BDD a -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a, BDD a, BDD a) (BDD a)
h (BDD a
mlo, BDD a
mhi, BDD a
n2) BDD a
ret
                BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  BDD a -> BDD a -> BDD a -> ST s (BDD a)
f BDD a
m BDD a
m BDD a
n

-- | Simultaneous substitution.
--
-- Note that this is not the same as repeated application of 'subst'.
substSet :: forall a. ItemOrder a => IntMap (BDD a) -> BDD a -> BDD a
substSet :: IntMap (BDD a) -> BDD a -> BDD a
substSet IntMap (BDD a)
s BDD a
m = (forall s. ST s (BDD a)) -> BDD a
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (BDD a)) -> BDD a)
-> (forall s. ST s (BDD a)) -> BDD a
forall a b. (a -> b) -> a -> b
$ do
  BDD a -> ST s IntSet
supportOp <- ST s (BDD a -> ST s IntSet)
forall s a. ST s (BDD a -> ST s IntSet)
mkSupportOp

  HashTable
  s
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
h <- Int
-> ST
     s
     (HashTable
        s
        ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
        (BDD a))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let -- f :: IntMap (BDD a) -> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST _ (BDD a)
      f :: IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned IntMap (BDD a)
_ | Bool -> Bool -> Bool
forall a. HasCallStack => Bool -> a -> a
assert ([(IntMap Bool, BDD a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(IntMap Bool, BDD a)]
conditioned Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 Bool -> Bool -> Bool
&& ((IntMap Bool, BDD a) -> Bool) -> [(IntMap Bool, BDD a)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(IntMap Bool
cond, BDD a
_) -> IntMap Bool -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet IntMap Bool
cond IntSet -> IntSet -> Bool
`IntSet.isSubsetOf` IntMap (BDD a) -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet IntMap (BDD a)
conditions) [(IntMap Bool, BDD a)]
conditioned) Bool
False = ST s (BDD a)
forall a. HasCallStack => a
undefined
      f IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned IntMap (BDD a)
remaining = do
        let l1 :: Level a
l1 = [Level a] -> Level a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Level a] -> Level a) -> [Level a] -> Level a
forall a b. (a -> b) -> a -> b
$ ((IntMap Bool, BDD a) -> Level a)
-> [(IntMap Bool, BDD a)] -> [Level a]
forall a b. (a -> b) -> [a] -> [b]
map (BDD a -> Level a
forall a. BDD a -> Level a
level (BDD a -> Level a)
-> ((IntMap Bool, BDD a) -> BDD a)
-> (IntMap Bool, BDD a)
-> Level a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap Bool, BDD a) -> BDD a
forall a b. (a, b) -> b
snd) [(IntMap Bool, BDD a)]
conditioned
            -- remaining' = IntMap.filterWithKey (\x _ -> l1 <= NonTerminal x) remaining
        IntMap (BDD a)
remaining' <- do
          IntSet
tmp <- ([IntSet] -> IntSet) -> ST s [IntSet] -> ST s IntSet
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions (ST s [IntSet] -> ST s IntSet) -> ST s [IntSet] -> ST s IntSet
forall a b. (a -> b) -> a -> b
$ ((IntMap Bool, BDD a) -> ST s IntSet)
-> [(IntMap Bool, BDD a)] -> ST s [IntSet]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (BDD a -> ST s IntSet
supportOp (BDD a -> ST s IntSet)
-> ((IntMap Bool, BDD a) -> BDD a)
-> (IntMap Bool, BDD a)
-> ST s IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap Bool, BDD a) -> BDD a
forall a b. (a, b) -> b
snd) [(IntMap Bool, BDD a)]
conditioned
          IntMap (BDD a) -> ST s (IntMap (BDD a))
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap (BDD a) -> ST s (IntMap (BDD a)))
-> IntMap (BDD a) -> ST s (IntMap (BDD a))
forall a b. (a -> b) -> a -> b
$ IntMap (BDD a) -> IntSet -> IntMap (BDD a)
forall a. IntMap a -> IntSet -> IntMap a
IntMap.restrictKeys IntMap (BDD a)
remaining IntSet
tmp
        let l :: Level a
l = [Level a] -> Level a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Level a] -> Level a) -> [Level a] -> Level a
forall a b. (a -> b) -> a -> b
$ Level a
l1 Level a -> [Level a] -> [Level a]
forall a. a -> [a] -> [a]
: (BDD a -> Level a) -> [BDD a] -> [Level a]
forall a b. (a -> b) -> [a] -> [b]
map BDD a -> Level a
forall a. BDD a -> Level a
level (IntMap (BDD a) -> [BDD a]
forall a. IntMap a -> [a]
IntMap.elems IntMap (BDD a)
remaining' [BDD a] -> [BDD a] -> [BDD a]
forall a. [a] -> [a] -> [a]
++ IntMap (BDD a) -> [BDD a]
forall a. IntMap a -> [a]
IntMap.elems IntMap (BDD a)
conditions)
        Bool -> ST s () -> ST s ()
forall a. HasCallStack => Bool -> a -> a
assert ((Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
c -> Int -> Level a
forall a. Int -> Level a
NonTerminal Int
c Level a -> Level a -> Bool
forall a. Ord a => a -> a -> Bool
<= Level a
l) (IntMap (BDD a) -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys IntMap (BDD a)
conditions)) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ () -> ST s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        case Level a
l of
          Level a
Terminal -> do
            case IntMap (BDD a)
-> [(IntMap Bool, BDD a)]
-> (IntMap (BDD a), [(IntMap Bool, BDD a)])
propagateFixed IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned of
              (IntMap (BDD a)
conditions', [(IntMap Bool, BDD a)]
conditioned') ->
                Bool -> ST s (BDD a) -> ST s (BDD a)
forall a. HasCallStack => Bool -> a -> a
assert (IntMap (BDD a) -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap (BDD a)
conditions' Bool -> Bool -> Bool
&& [(IntMap Bool, BDD a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(IntMap Bool, BDD a)]
conditioned' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (ST s (BDD a) -> ST s (BDD a)) -> ST s (BDD a) -> ST s (BDD a)
forall a b. (a -> b) -> a -> b
$
                  BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((IntMap Bool, BDD a) -> BDD a
forall a b. (a, b) -> b
snd ([(IntMap Bool, BDD a)] -> (IntMap Bool, BDD a)
forall a. [a] -> a
head [(IntMap Bool, BDD a)]
conditioned'))
          NonTerminal Int
x
            | Level a
l Level a -> Level a -> Bool
forall a. Eq a => a -> a -> Bool
== Level a
l1 Bool -> Bool -> Bool
&& Int
x Int -> IntMap (BDD a) -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (BDD a)
remaining' -> do
                let conditions' :: IntMap (BDD a)
conditions' = Int -> BDD a -> IntMap (BDD a) -> IntMap (BDD a)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x (IntMap (BDD a)
remaining' IntMap (BDD a) -> Int -> BDD a
forall a. IntMap a -> Int -> a
IntMap.! Int
x) IntMap (BDD a)
conditions
                    conditioned' :: [(IntMap Bool, BDD a)]
conditioned' = do
                      (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned
                      case BDD a
a of
                        Branch Int
x' BDD a
lo BDD a
hi | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' -> [(Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
False IntMap Bool
cond, BDD a
lo), (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
True IntMap Bool
cond, BDD a
hi)]
                        BDD a
_ -> [(IntMap Bool
cond, BDD a
a)]
                IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f IntMap (BDD a)
conditions' [(IntMap Bool, BDD a)]
conditioned' (Int -> IntMap (BDD a) -> IntMap (BDD a)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
x IntMap (BDD a)
remaining')
            | Bool
otherwise -> do
                case IntMap (BDD a)
-> [(IntMap Bool, BDD a)]
-> (IntMap (BDD a), [(IntMap Bool, BDD a)])
propagateFixed IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned of
                  (IntMap (BDD a)
conditions', [(IntMap Bool, BDD a)]
conditioned') -> do
                    let key :: ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
key = (IntMap (BDD a) -> [(Int, BDD a)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (BDD a)
conditions', [(IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Bool
cond, BDD a
a) | (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned'], IntMap (BDD a) -> [(Int, BDD a)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (BDD a)
remaining')  -- キーを減らせる?
                    Maybe (BDD a)
u <- HashTable
  s
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
-> ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
-> ST s (Maybe (BDD a))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable
  s
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
h ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
key
                    case Maybe (BDD a)
u of
                      Just BDD a
y -> BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
y
                      Maybe (BDD a)
Nothing -> do
                        let f0 :: BDD a -> BDD a
f0 (Branch Int
x' BDD a
lo BDD a
_) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' = BDD a
lo
                            f0 BDD a
a = BDD a
a
                            f1 :: BDD a -> BDD a
f1 (Branch Int
x' BDD a
_ BDD a
hi) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' = BDD a
hi
                            f1 BDD a
a = BDD a
a
                        BDD a
r0 <- IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f ((BDD a -> BDD a) -> IntMap (BDD a) -> IntMap (BDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map BDD a -> BDD a
forall a. BDD a -> BDD a
f0 IntMap (BDD a)
conditions') [(IntMap Bool
cond, BDD a -> BDD a
forall a. BDD a -> BDD a
f0 BDD a
a) | (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned'] ((BDD a -> BDD a) -> IntMap (BDD a) -> IntMap (BDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map BDD a -> BDD a
forall a. BDD a -> BDD a
f0 IntMap (BDD a)
remaining')
                        BDD a
r1 <- IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f ((BDD a -> BDD a) -> IntMap (BDD a) -> IntMap (BDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map BDD a -> BDD a
forall a. BDD a -> BDD a
f1 IntMap (BDD a)
conditions') [(IntMap Bool
cond, BDD a -> BDD a
forall a. BDD a -> BDD a
f1 BDD a
a) | (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned'] ((BDD a -> BDD a) -> IntMap (BDD a) -> IntMap (BDD a)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map BDD a -> BDD a
forall a. BDD a -> BDD a
f1 IntMap (BDD a)
remaining')
                        let ret :: BDD a
ret = Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x BDD a
r0 BDD a
r1
                        HashTable
  s
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
-> ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
-> BDD a
-> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable
  s
  ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
  (BDD a)
h ([(Int, BDD a)], [([(Int, Bool)], BDD a)], [(Int, BDD a)])
key BDD a
ret
                        BDD a -> ST s (BDD a)
forall (m :: * -> *) a. Monad m => a -> m a
return BDD a
ret
  IntMap (BDD a)
-> [(IntMap Bool, BDD a)] -> IntMap (BDD a) -> ST s (BDD a)
f IntMap (BDD a)
forall a. IntMap a
IntMap.empty [(IntMap Bool
forall a. IntMap a
IntMap.empty, BDD a
m)] IntMap (BDD a)
s

  where
    propagateFixed :: IntMap (BDD a) -> [(IntMap Bool, BDD a)] -> (IntMap (BDD a), [(IntMap Bool, BDD a)])
    propagateFixed :: IntMap (BDD a)
-> [(IntMap Bool, BDD a)]
-> (IntMap (BDD a), [(IntMap Bool, BDD a)])
propagateFixed IntMap (BDD a)
conditions [(IntMap Bool, BDD a)]
conditioned
      | IntMap Bool -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap Bool
fixed = (IntMap (BDD a)
conditions, [(IntMap Bool, BDD a)]
conditioned)
      | Bool
otherwise =
          ( IntMap (BDD a) -> IntMap Bool -> IntMap (BDD a)
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.difference IntMap (BDD a)
conditions IntMap Bool
fixed
          , [(IntMap Bool -> IntMap Bool -> IntMap Bool
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.difference IntMap Bool
cond IntMap Bool
fixed, BDD a
a) | (IntMap Bool
cond, BDD a
a) <- [(IntMap Bool, BDD a)]
conditioned, IntMap Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (IntMap Bool -> Bool) -> IntMap Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool -> Bool) -> IntMap Bool -> IntMap Bool -> IntMap Bool
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IntMap.intersectionWith Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) IntMap Bool
fixed IntMap Bool
cond]
          )
      where
        fixed :: IntMap Bool
fixed = (BDD a -> Maybe Bool) -> IntMap (BDD a) -> IntMap Bool
forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybe BDD a -> Maybe Bool
asBool IntMap (BDD a)
conditions

    asBool :: BDD a -> Maybe Bool
    asBool :: BDD a -> Maybe Bool
asBool (Leaf Bool
b) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
    asBool BDD a
_ = Maybe Bool
forall a. Maybe a
Nothing

-- ------------------------------------------------------------------------

-- | Least fixed point.
--
-- Monotonicity of the operator is assumed but not checked.
lfp :: ItemOrder a => (BDD a ->  BDD a) -> BDD a
lfp :: (BDD a -> BDD a) -> BDD a
lfp BDD a -> BDD a
f = BDD a -> BDD a
go BDD a
forall a. BDD a
false
  where
    go :: BDD a -> BDD a
go BDD a
curr
      | BDD a
curr BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
next = BDD a
curr
      | Bool
otherwise = BDD a -> BDD a
go BDD a
next
      where
        next :: BDD a
next = BDD a -> BDD a
f BDD a
curr

-- | Greatest fixed point.
--
-- Monotonicity of the operator is assumed but not checked.
gfp :: ItemOrder a => (BDD a ->  BDD a) -> BDD a
gfp :: (BDD a -> BDD a) -> BDD a
gfp BDD a -> BDD a
f = BDD a -> BDD a
go BDD a
forall a. BDD a
true
  where
    go :: BDD a -> BDD a
go BDD a
curr
      | BDD a
curr BDD a -> BDD a -> Bool
forall a. Eq a => a -> a -> Bool
== BDD a
next = BDD a
curr
      | Bool
otherwise = BDD a -> BDD a
go BDD a
next
      where
        next :: BDD a
next = BDD a -> BDD a
f BDD a
curr

-- ------------------------------------------------------------------------

findSatM :: MonadPlus m => BDD a -> m (IntMap Bool)
findSatM :: BDD a -> m (IntMap Bool)
findSatM = (Int -> m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool))
-> (Bool -> m (IntMap Bool)) -> BDD a -> m (IntMap Bool)
forall b a. (Int -> b -> b -> b) -> (Bool -> b) -> BDD a -> b
fold Int -> m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *).
MonadPlus m =>
Int -> m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
f Bool -> m (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => Bool -> m (IntMap a)
g
  where
    f :: Int -> m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
f Int
x m (IntMap Bool)
lo m (IntMap Bool)
hi = m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus ((IntMap Bool -> IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
False) m (IntMap Bool)
lo) ((IntMap Bool -> IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
True) m (IntMap Bool)
hi)
    g :: Bool -> m (IntMap a)
g Bool
b = if Bool
b then IntMap a -> m (IntMap a)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap a
forall a. IntMap a
IntMap.empty else m (IntMap a)
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- | Find one satisfying partial assignment
anySat :: BDD a -> Maybe (IntMap Bool)
anySat :: BDD a -> Maybe (IntMap Bool)
anySat = BDD a -> Maybe (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => BDD a -> m (IntMap Bool)
findSatM

-- | Enumerate all satisfying partial assignments
allSat :: BDD a -> [IntMap Bool]
allSat :: BDD a -> [IntMap Bool]
allSat = BDD a -> [IntMap Bool]
forall (m :: * -> *) a. MonadPlus m => BDD a -> m (IntMap Bool)
findSatM

findSatCompleteM :: forall a m. (MonadPlus m, ItemOrder a, HasCallStack) => IntSet -> BDD a -> m (IntMap Bool)
findSatCompleteM :: IntSet -> BDD a -> m (IntMap Bool)
findSatCompleteM IntSet
xs0 BDD a
bdd = (forall s. ST s (m (IntMap Bool))) -> m (IntMap Bool)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (m (IntMap Bool))) -> m (IntMap Bool))
-> (forall s. ST s (m (IntMap Bool))) -> m (IntMap Bool)
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a) (m (IntMap Bool))
h <- Int -> ST s (HashTable s (BDD a) (m (IntMap Bool)))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [Int] -> BDD a -> ST s (m (IntMap Bool))
f [Int]
_ (Leaf Bool
False) = m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (m (IntMap Bool) -> ST s (m (IntMap Bool)))
-> m (IntMap Bool) -> ST s (m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ m (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      f [Int]
xs (Leaf Bool
True) = m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (m (IntMap Bool) -> ST s (m (IntMap Bool)))
-> m (IntMap Bool) -> ST s (m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ (IntMap Bool -> Int -> m (IntMap Bool))
-> IntMap Bool -> [Int] -> m (IntMap Bool)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\IntMap Bool
m Int
x -> [m (IntMap Bool)] -> m (IntMap Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [IntMap Bool -> m (IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
v IntMap Bool
m) | Bool
v <- [Bool
False, Bool
True]]) IntMap Bool
forall a. IntMap a
IntMap.empty [Int]
xs
      f [Int]
xs n :: BDD a
n@(Branch Int
x BDD a
lo BDD a
hi) = do
        case (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Int
x2 -> Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
x2 Int
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT) [Int]
xs of
          ([Int]
ys, (Int
x':[Int]
xs')) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' -> do
            Maybe (m (IntMap Bool))
r <- HashTable s (BDD a) (m (IntMap Bool))
-> BDD a -> ST s (Maybe (m (IntMap Bool)))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (m (IntMap Bool))
h BDD a
n
            m (IntMap Bool)
ps <- case Maybe (m (IntMap Bool))
r of
              Just m (IntMap Bool)
ret -> m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return m (IntMap Bool)
ret
              Maybe (m (IntMap Bool))
Nothing -> do
                m (IntMap Bool)
r0 <- [Int] -> BDD a -> ST s (m (IntMap Bool))
f [Int]
xs' BDD a
lo
                m (IntMap Bool)
r1 <- ST s (m (IntMap Bool)) -> ST s (m (IntMap Bool))
forall s a. ST s a -> ST s a
unsafeInterleaveST (ST s (m (IntMap Bool)) -> ST s (m (IntMap Bool)))
-> ST s (m (IntMap Bool)) -> ST s (m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ [Int] -> BDD a -> ST s (m (IntMap Bool))
f [Int]
xs' BDD a
hi
                let ret :: m (IntMap Bool)
ret = (IntMap Bool -> IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
False) m (IntMap Bool)
r0 m (IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` (IntMap Bool -> IntMap Bool) -> m (IntMap Bool) -> m (IntMap Bool)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
True) m (IntMap Bool)
r1
                HashTable s (BDD a) (m (IntMap Bool))
-> BDD a -> m (IntMap Bool) -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (m (IntMap Bool))
h BDD a
n m (IntMap Bool)
ret
                m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return m (IntMap Bool)
ret
            m (IntMap Bool) -> ST s (m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (m (IntMap Bool) -> ST s (m (IntMap Bool)))
-> m (IntMap Bool) -> ST s (m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ do
              IntMap Bool
p <- m (IntMap Bool)
ps
              (IntMap Bool -> Int -> m (IntMap Bool))
-> IntMap Bool -> [Int] -> m (IntMap Bool)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\IntMap Bool
m Int
y -> [m (IntMap Bool)] -> m (IntMap Bool)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [IntMap Bool -> m (IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
y Bool
v IntMap Bool
m) | Bool
v <- [Bool
False, Bool
True]]) IntMap Bool
p [Int]
ys
          ([Int], [Int])
_ -> String -> ST s (m (IntMap Bool))
forall a. HasCallStack => String -> a
error (String
"findSatCompleteM: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" should not occur")
  [Int] -> BDD a -> ST s (m (IntMap Bool))
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
xs0)) BDD a
bdd

-- | Find one satisfying (complete) assignment over a given set of variables
--
-- The set of variables must be a superset of 'support'.
anySatComplete :: ItemOrder a => IntSet -> BDD a -> Maybe (IntMap Bool)
anySatComplete :: IntSet -> BDD a -> Maybe (IntMap Bool)
anySatComplete = IntSet -> BDD a -> Maybe (IntMap Bool)
forall a (m :: * -> *).
(MonadPlus m, ItemOrder a, HasCallStack) =>
IntSet -> BDD a -> m (IntMap Bool)
findSatCompleteM

-- | Enumerate all satisfying (complete) assignment over a given set of variables
--
-- The set of variables must be a superset of 'support'.
allSatComplete :: ItemOrder a => IntSet -> BDD a -> [IntMap Bool]
allSatComplete :: IntSet -> BDD a -> [IntMap Bool]
allSatComplete = IntSet -> BDD a -> [IntMap Bool]
forall a (m :: * -> *).
(MonadPlus m, ItemOrder a, HasCallStack) =>
IntSet -> BDD a -> m (IntMap Bool)
findSatCompleteM

{-# SPECIALIZE countSat :: ItemOrder a => IntSet -> BDD a -> Int #-}
{-# SPECIALIZE countSat :: ItemOrder a => IntSet -> BDD a -> Integer #-}
{-# SPECIALIZE countSat :: ItemOrder a => IntSet -> BDD a -> Natural #-}
-- | Count the number of satisfying (complete) assignment over a given set of variables.
--
-- The set of variables must be a superset of 'support'.
--
-- It is polymorphic in return type, but it is recommended to use 'Integer' or 'Natural'
-- because the size can be larger than fixed integer types such as @Int64@.
--
-- >>> countSat (IntSet.fromList [1..128]) (true :: BDD AscOrder)
-- 340282366920938463463374607431768211456
-- >>> import Data.Int
-- >>> maxBound :: Int64
-- 9223372036854775807
countSat :: forall a b. (ItemOrder a, Num b, Bits b, HasCallStack) => IntSet -> BDD a -> b
countSat :: IntSet -> BDD a -> b
countSat IntSet
xs BDD a
bdd = (forall s. ST s b) -> b
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s b) -> b) -> (forall s. ST s b) -> b
forall a b. (a -> b) -> a -> b
$ do
  HashTable s (BDD a) b
h <- Int -> ST s (HashTable s (BDD a) b)
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
  let f :: [Int] -> BDD a -> ST s b
f [Int]
_ (Leaf Bool
False) = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> ST s b) -> b -> ST s b
forall a b. (a -> b) -> a -> b
$ b
0
      f [Int]
ys (Leaf Bool
True) = b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> ST s b) -> b -> ST s b
forall a b. (a -> b) -> a -> b
$! b
1 b -> Int -> b
forall a. Bits a => a -> Int -> a
`shiftL` [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ys
      f [Int]
ys node :: BDD a
node@(Branch Int
x BDD a
lo BDD a
hi) = do
        case (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Int
x2 -> Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a) Int
x2 Int
x Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT) [Int]
ys of
          ([Int]
zs, Int
y' : [Int]
ys') | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y' -> do
            Maybe b
m <- HashTable s (BDD a) b -> BDD a -> ST s (Maybe b)
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) b
h BDD a
node
            b
n <- case Maybe b
m of
              Just b
n -> b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
n
              Maybe b
Nothing -> do
                b
n <- (b -> b -> b) -> ST s b -> ST s b -> ST s b
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 b -> b -> b
forall a. Num a => a -> a -> a
(+) ([Int] -> BDD a -> ST s b
f [Int]
ys' BDD a
lo) ([Int] -> BDD a -> ST s b
f [Int]
ys' BDD a
hi)
                HashTable s (BDD a) b -> BDD a -> b -> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) b
h BDD a
node b
n
                b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return b
n
            b -> ST s b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> ST s b) -> b -> ST s b
forall a b. (a -> b) -> a -> b
$! b
n b -> Int -> b
forall a. Bits a => a -> Int -> a
`shiftL` [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
zs
          ([Int]
_, [Int]
_) -> String -> ST s b
forall a. HasCallStack => String -> a
error (String
"countSat: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" should not occur")
  [Int] -> BDD a -> ST s b
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
xs)) BDD a
bdd

-- | Sample an assignment from uniform distribution over complete satisfiable assignments ('allSatComplete') of the BDD.
--
-- The function constructs a table internally and the table is shared across
-- multiple use of the resulting action (@m IntSet@).
-- Therefore, the code
--
-- @
-- let g = uniformSatM xs bdd gen
-- s1 <- g
-- s2 <- g
-- @
--
-- is more efficient than
--
-- @
-- s1 <- uniformSatM xs bdd gen
-- s2 <- uniformSatM xs bdd gen
-- @
-- .
#if MIN_VERSION_mwc_random(0,15,0)
uniformSatM :: forall a g m. (ItemOrder a, StatefulGen g m, HasCallStack) => IntSet -> BDD a -> g -> m (IntMap Bool)
#else
uniformSatM :: forall a m. (ItemOrder a, PrimMonad m, HasCallStack) => IntSet -> BDD a -> Gen (PrimState m) -> m (IntMap Bool)
#endif
uniformSatM :: IntSet -> BDD a -> g -> m (IntMap Bool)
uniformSatM IntSet
xs0 BDD a
bdd0 = IntMap Bool -> g -> m (IntMap Bool)
func IntMap Bool
forall a. IntMap a
IntMap.empty
  where
    func :: IntMap Bool -> g -> m (IntMap Bool)
func = (forall s. ST s (IntMap Bool -> g -> m (IntMap Bool)))
-> IntMap Bool -> g -> m (IntMap Bool)
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (IntMap Bool -> g -> m (IntMap Bool)))
 -> IntMap Bool -> g -> m (IntMap Bool))
-> (forall s. ST s (IntMap Bool -> g -> m (IntMap Bool)))
-> IntMap Bool
-> g
-> m (IntMap Bool)
forall a b. (a -> b) -> a -> b
$ do
      HashTable s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool))
h <- Int
-> ST
     s
     (HashTable
        s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool)))
forall s k v. Int -> ST s (HashTable s k v)
C.newSized Int
defaultTableSize
      let f :: [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
f [Int]
xs BDD a
bdd =
            case (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\Int
x2 -> Int -> Level a
forall a. Int -> Level a
NonTerminal Int
x2 Level a -> Level a -> Bool
forall a. Ord a => a -> a -> Bool
< BDD a -> Level a
forall a. BDD a -> Level a
level BDD a
bdd) [Int]
xs of
              ([Int]
ys, [Int]
xxs') -> do
                [Int]
xs' <- case (BDD a
bdd, [Int]
xxs') of
                         (Branch Int
x BDD a
_ BDD a
_, Int
x' : [Int]
xs') | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x' -> [Int] -> ST s [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return [Int]
xs'
                         (Branch Int
x BDD a
_ BDD a
_, [Int]
_) -> String -> ST s [Int]
forall a. HasCallStack => String -> a
error (String
"uniformSatM: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" should not occur")
                         (Leaf Bool
_, []) -> [Int] -> ST s [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                         (Leaf Bool
_, Int
_:[Int]
_) -> String -> ST s [Int]
forall a. HasCallStack => String -> a
error (String
"uniformSatM: should not happen")
                (Integer
s, IntMap Bool -> g -> m (IntMap Bool)
func0) <- [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
g [Int]
xs' BDD a
bdd
                let func' :: IntMap Bool -> g -> m (IntMap Bool)
func' !IntMap Bool
m !g
gen = do
#if MIN_VERSION_mwc_random(0,15,0)
                      [Bool]
vals <- Int -> m Bool -> m [Bool]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ys) (g -> m Bool
forall a g (m :: * -> *). (Uniform a, StatefulGen g m) => g -> m a
uniformM g
gen)
#else
                      vals <- replicateM (length ys) (uniform gen)
#endif
                      IntMap Bool -> g -> m (IntMap Bool)
func0 (IntMap Bool
m IntMap Bool -> IntMap Bool -> IntMap Bool
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` [(Int, Bool)] -> IntMap Bool
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
ys [Bool]
vals)) g
gen
                (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
s Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ys, IntMap Bool -> g -> m (IntMap Bool)
func')
          g :: [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
g [Int]
_ (Leaf Bool
True) = (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
1 :: Integer, \IntMap Bool
a g
_gen -> IntMap Bool -> m (IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap Bool
a)
          g [Int]
_ (Leaf Bool
False) = (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
0 :: Integer, \IntMap Bool
_a g
_gen -> String -> m (IntMap Bool)
forall a. HasCallStack => String -> a
error String
"uniformSatM: should not happen")
          g [Int]
xs bdd :: BDD a
bdd@(Branch Int
x BDD a
lo BDD a
hi) = do
            Maybe (Integer, IntMap Bool -> g -> m (IntMap Bool))
m <- HashTable s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> BDD a
-> ST s (Maybe (Integer, IntMap Bool -> g -> m (IntMap Bool)))
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool))
h BDD a
bdd
            case Maybe (Integer, IntMap Bool -> g -> m (IntMap Bool))
m of
              Just (Integer, IntMap Bool -> g -> m (IntMap Bool))
ret -> (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer, IntMap Bool -> g -> m (IntMap Bool))
ret
              Maybe (Integer, IntMap Bool -> g -> m (IntMap Bool))
Nothing -> do
                (Integer
n0, IntMap Bool -> g -> m (IntMap Bool)
func0) <- [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
f [Int]
xs BDD a
lo
                (Integer
n1, IntMap Bool -> g -> m (IntMap Bool)
func1) <- [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
f [Int]
xs BDD a
hi
                let s :: Integer
s = Integer
n0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n1
                    r :: Double
                    r :: Double
r = Ratio Integer -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Integer
n1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
s)
                Double -> ST s () -> ST s ()
seq Double
r (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ () -> ST s ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                let func' :: IntMap Bool -> g -> m (IntMap Bool)
func' !IntMap Bool
a !g
gen = do
                      Bool
b <- Double -> g -> m Bool
forall g (m :: * -> *). StatefulGen g m => Double -> g -> m Bool
bernoulli Double
r g
gen
                      if Bool
b then
                        IntMap Bool -> g -> m (IntMap Bool)
func1 (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
True IntMap Bool
a) g
gen
                      else
                        IntMap Bool -> g -> m (IntMap Bool)
func0 (Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
x Bool
False IntMap Bool
a) g
gen
                HashTable s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> BDD a
-> (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s ()
forall (h :: * -> * -> * -> *) k s v.
(HashTable h, Eq k, Hashable k) =>
h s k v -> k -> v -> ST s ()
H.insert HashTable s (BDD a) (Integer, IntMap Bool -> g -> m (IntMap Bool))
h BDD a
bdd (Integer
s, IntMap Bool -> g -> m (IntMap Bool)
func')
                (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
s, IntMap Bool -> g -> m (IntMap Bool)
func')
      ((Integer, IntMap Bool -> g -> m (IntMap Bool))
 -> IntMap Bool -> g -> m (IntMap Bool))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (IntMap Bool -> g -> m (IntMap Bool))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> IntMap Bool -> g -> m (IntMap Bool)
forall a b. (a, b) -> b
snd (ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
 -> ST s (IntMap Bool -> g -> m (IntMap Bool)))
-> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
-> ST s (IntMap Bool -> g -> m (IntMap Bool))
forall a b. (a -> b) -> a -> b
$ [Int]
-> BDD a -> ST s (Integer, IntMap Bool -> g -> m (IntMap Bool))
f ((Int -> Int -> Ordering) -> [Int] -> [Int]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Proxy a -> Int -> Int -> Ordering
forall a (proxy :: * -> *).
ItemOrder a =>
proxy a -> Int -> Int -> Ordering
compareItem (Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a)) (IntSet -> [Int]
IntSet.toList IntSet
xs0)) BDD a
bdd0

-- ------------------------------------------------------------------------

-- | 'Sig'-algebra stucture of 'BDD', \(\mathrm{in}_\mathrm{Sig}\).
inSig :: Sig (BDD a) -> BDD a
inSig :: Sig (BDD a) -> BDD a
inSig (SLeaf Bool
b) = Bool -> BDD a
forall a. Bool -> BDD a
Leaf Bool
b
inSig (SBranch Int
x BDD a
lo BDD a
hi) = Int -> BDD a -> BDD a -> BDD a
forall a. Int -> BDD a -> BDD a -> BDD a
Branch Int
x BDD a
lo BDD a
hi

-- | 'Sig'-coalgebra stucture of 'BDD', \(\mathrm{out}_\mathrm{Sig}\).
outSig :: BDD a -> Sig (BDD a)
outSig :: BDD a -> Sig (BDD a)
outSig (Leaf Bool
b) = Bool -> Sig (BDD a)
forall a. Bool -> Sig a
SLeaf Bool
b
outSig (Branch Int
x BDD a
lo BDD a
hi) = Int -> BDD a -> BDD a -> Sig (BDD a)
forall a. Int -> a -> a -> Sig a
SBranch Int
x BDD a
lo BDD a
hi

-- ------------------------------------------------------------------------

-- | Convert a BDD into a pointed graph
--
-- Nodes @0@ and @1@ are reserved for @SLeaf False@ and @SLeaf True@
-- even if they are not actually used. Therefore the result may be
-- larger than 'numNodes' if the leaf nodes are not used.
toGraph :: BDD a -> (Graph Sig, Int)
toGraph :: BDD a -> (Graph Sig, Int)
toGraph (BDD Node
node) = Node -> (Graph Sig, Int)
Node.toGraph Node
node

-- | Convert multiple BDDs into a graph
toGraph' :: Traversable t => t (BDD a) -> (Graph Sig, t Int)
toGraph' :: t (BDD a) -> (Graph Sig, t Int)
toGraph' t (BDD a)
bs = t Node -> (Graph Sig, t Int)
forall (t :: * -> *). Traversable t => t Node -> (Graph Sig, t Int)
Node.toGraph' ((BDD a -> Node) -> t (BDD a) -> t Node
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(BDD Node
node) -> Node
node) t (BDD a)
bs)

-- | Convert a pointed graph into a BDD
fromGraph :: HasCallStack => (Graph Sig, Int) -> BDD a
fromGraph :: (Graph Sig, Int) -> BDD a
fromGraph = (Sig (BDD a) -> BDD a) -> (Graph Sig, Int) -> BDD a
forall (f :: * -> *) a.
(Functor f, HasCallStack) =>
(f a -> a) -> (Graph f, Int) -> a
Node.foldGraph Sig (BDD a) -> BDD a
forall a. Sig (BDD a) -> BDD a
inSig

-- | Convert nodes of a graph into BDDs
fromGraph' :: HasCallStack => Graph Sig -> IntMap (BDD a)
fromGraph' :: Graph Sig -> IntMap (BDD a)
fromGraph' = (Sig (BDD a) -> BDD a) -> Graph Sig -> IntMap (BDD a)
forall (f :: * -> *) a.
(Functor f, HasCallStack) =>
(f a -> a) -> Graph f -> IntMap a
Node.foldGraphNodes Sig (BDD a) -> BDD a
forall a. Sig (BDD a) -> BDD a
inSig

-- ------------------------------------------------------------------------