{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE CPP #-}

#define OPTIMIZE_WQO

module Language.REST.WQOConstraints.ADT
  (  ConstraintsADT(..)
  , addConstraint
  , adtOC
  , intersect
  , union
  )
where

import GHC.Generics (Generic)

import Data.Hashable
import Control.Monad.State.Lazy
import qualified Data.Set as S
import qualified Data.Maybe as Mb
import qualified Data.Map.Strict as M
import qualified Language.REST.Internal.WQO as WQO
import qualified Language.REST.WQOConstraints as OC
import Language.REST.SMT
import Language.REST.Op
import System.IO (Handle)
import Text.Printf

type WQO = WQO.WQO

-- | Represents constraints over a WQO on @a@
data ConstraintsADT a =
 -- | @Sat wqo@ represents satisfiable constraints: those that permit each relation in @wqo@.
    Sat (WQO a)
  | Unsat
    -- | @Union c1 c2@ permits orderings of P1 and orderings of P2
  | Union (ConstraintsADT a) (ConstraintsADT a)
    -- | @Intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2
  | Intersect (ConstraintsADT a) (ConstraintsADT a)
  deriving (ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c/= :: forall a. Eq a => ConstraintsADT a -> ConstraintsADT a -> Bool
== :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c== :: forall a. Eq a => ConstraintsADT a -> ConstraintsADT a -> Bool
Eq, ConstraintsADT a -> ConstraintsADT a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (ConstraintsADT a)
forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Ordering
forall a.
Ord a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
min :: ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
$cmin :: forall a.
Ord a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
max :: ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
$cmax :: forall a.
Ord a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
>= :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c>= :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
> :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c> :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
<= :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c<= :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
< :: ConstraintsADT a -> ConstraintsADT a -> Bool
$c< :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Bool
compare :: ConstraintsADT a -> ConstraintsADT a -> Ordering
$ccompare :: forall a. Ord a => ConstraintsADT a -> ConstraintsADT a -> Ordering
Ord, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (ConstraintsADT a) x -> ConstraintsADT a
forall a x. ConstraintsADT a -> Rep (ConstraintsADT a) x
$cto :: forall a x. Rep (ConstraintsADT a) x -> ConstraintsADT a
$cfrom :: forall a x. ConstraintsADT a -> Rep (ConstraintsADT a) x
Generic, forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall {a}. Hashable a => Eq (ConstraintsADT a)
forall a. Hashable a => Int -> ConstraintsADT a -> Int
forall a. Hashable a => ConstraintsADT a -> Int
hash :: ConstraintsADT a -> Int
$chash :: forall a. Hashable a => ConstraintsADT a -> Int
hashWithSalt :: Int -> ConstraintsADT a -> Int
$chashWithSalt :: forall a. Hashable a => Int -> ConstraintsADT a -> Int
Hashable)

instance {-# OVERLAPPING #-} (ToSMTVar a Int) => ToSMT (ConstraintsADT a) Bool where
  toSMT :: ConstraintsADT a -> SMTExpr Bool
toSMT (Sat WQO a
w)           = forall a b. ToSMT a b => a -> SMTExpr b
toSMT WQO a
w
  toSMT ConstraintsADT a
Unsat             = SMTExpr Bool
smtFalse
  toSMT (Union ConstraintsADT a
w1 ConstraintsADT a
w2)     = [SMTExpr Bool] -> SMTExpr Bool
Or  [forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w1, forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w2]
  toSMT (Intersect ConstraintsADT a
w1 ConstraintsADT a
w2) = [SMTExpr Bool] -> SMTExpr Bool
And [forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w1, forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w2]

{-# SPECIALIZE cost :: ConstraintsADT Op -> Int #-}
cost :: (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost :: forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost (Union ConstraintsADT a
lhs ConstraintsADT a
rhs)     = forall a. Ord a => a -> a -> a
min (forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs) (forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs)
cost (Intersect ConstraintsADT a
lhs ConstraintsADT a
rhs) = forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs forall a. Num a => a -> a -> a
+ forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs
cost (Sat WQO a
wqo)           = forall a. Set a -> Int
S.size forall a b. (a -> b) -> a -> b
$ forall a. Ord a => WQO a -> Set a
WQO.elems WQO a
wqo
cost ConstraintsADT a
Unsat               = Int
100

-- | @intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2
intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a

#ifdef OPTIMIZE_WQO
-- Optimization
intersect :: forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect (Sat WQO a
t) (Sat WQO a
u) =
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. ConstraintsADT a
Unsat forall a. WQO a -> ConstraintsADT a
Sat (forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
t WQO a
u)
#endif

intersect (Sat WQO a
w) ConstraintsADT a
v            | WQO a
w forall a. Eq a => a -> a -> Bool
== forall a. WQO a
WQO.empty = ConstraintsADT a
v
intersect ConstraintsADT a
v            (Sat WQO a
w) | WQO a
w forall a. Eq a => a -> a -> Bool
== forall a. WQO a
WQO.empty = ConstraintsADT a
v
intersect ConstraintsADT a
_ ConstraintsADT a
Unsat     = forall a. ConstraintsADT a
Unsat
intersect ConstraintsADT a
Unsat ConstraintsADT a
_     = forall a. ConstraintsADT a
Unsat
intersect ConstraintsADT a
t1 ConstraintsADT a
t2 | ConstraintsADT a
t1 forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t2 = ConstraintsADT a
t1
intersect ConstraintsADT a
t1 (Union ConstraintsADT a
t2 ConstraintsADT a
t3) | ConstraintsADT a
t1 forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t2 Bool -> Bool -> Bool
|| ConstraintsADT a
t1 forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t3 = ConstraintsADT a
t1
#ifdef OPTIMIZE_WQO
intersect (Sat WQO a
w1) (Intersect (Sat WQO a
w2) ConstraintsADT a
t2) =
  case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
w1 WQO a
w2 of
    Just WQO a
w' -> forall a. WQO a -> ConstraintsADT a
Sat WQO a
w' forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`intersect` ConstraintsADT a
t2
    Maybe (WQO a)
Nothing -> forall a. ConstraintsADT a
Unsat
intersect (Sat WQO a
w1) (Intersect ConstraintsADT a
t2 (Sat WQO a
w2)) =
  case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
w1 WQO a
w2 of
    Just WQO a
w' -> forall a. WQO a -> ConstraintsADT a
Sat WQO a
w' forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`intersect` ConstraintsADT a
t2
    Maybe (WQO a)
Nothing -> forall a. ConstraintsADT a
Unsat
intersect (Intersect ConstraintsADT a
t1 (Sat WQO a
w1)) (Sat WQO a
w2) =
  case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
w1 WQO a
w2 of
    Just WQO a
w' -> ConstraintsADT a
t1 forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`intersect` forall a. WQO a -> ConstraintsADT a
Sat WQO a
w'
    Maybe (WQO a)
Nothing -> forall a. ConstraintsADT a
Unsat
intersect (Intersect (Sat WQO a
w1) ConstraintsADT a
t1) (Sat WQO a
w2) =
  case forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
w1 WQO a
w2 of
    Just WQO a
w' -> ConstraintsADT a
t1 forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
`intersect` forall a. WQO a -> ConstraintsADT a
Sat WQO a
w'
    Maybe (WQO a)
Nothing -> forall a. ConstraintsADT a
Unsat
#endif
intersect ConstraintsADT a
t1 ConstraintsADT a
t2            = forall a. ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
Intersect ConstraintsADT a
t1 ConstraintsADT a
t2

-- | @union c1 c2@ permits orderings of P1 and orderings of P2
union :: Eq a => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union :: forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union (Sat WQO a
w) ConstraintsADT a
_            | WQO a
w forall a. Eq a => a -> a -> Bool
== forall a. WQO a
WQO.empty = forall a. WQO a -> ConstraintsADT a
Sat WQO a
w
union ConstraintsADT a
_            (Sat WQO a
w) | WQO a
w forall a. Eq a => a -> a -> Bool
== forall a. WQO a
WQO.empty = forall a. WQO a -> ConstraintsADT a
Sat WQO a
w
union (Intersect ConstraintsADT a
a ConstraintsADT a
b)  ConstraintsADT a
c | ConstraintsADT a
a forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c Bool -> Bool -> Bool
|| ConstraintsADT a
b forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c = ConstraintsADT a
c
union ConstraintsADT a
a (Intersect ConstraintsADT a
b ConstraintsADT a
c)  | ConstraintsADT a
a forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
b Bool -> Bool -> Bool
|| ConstraintsADT a
a forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c = ConstraintsADT a
a
union ConstraintsADT a
a (Union ConstraintsADT a
b ConstraintsADT a
c)      | ConstraintsADT a
a forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
b           = forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union ConstraintsADT a
a ConstraintsADT a
c
union ConstraintsADT a
Unsat ConstraintsADT a
s     = ConstraintsADT a
s
union ConstraintsADT a
s ConstraintsADT a
Unsat     = ConstraintsADT a
s
union ConstraintsADT a
c1 ConstraintsADT a
c2 | ConstraintsADT a
c1 forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c2 = ConstraintsADT a
c1
union ConstraintsADT a
c1 ConstraintsADT a
c2            = forall a. ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
Union ConstraintsADT a
c1 ConstraintsADT a
c2

-- | @addConstraint o c@ strengthes @c@ to also contain every relation in @o@
addConstraint
 :: (Ord a, Hashable a) => WQO a -> ConstraintsADT a -> ConstraintsADT a
addConstraint :: forall a.
(Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
addConstraint WQO a
o = forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect (forall a. WQO a -> ConstraintsADT a
Sat WQO a
o)

notStrongerThan
  :: (Eq a, ToSMTVar a Int)
  => ConstraintsADT a
  -> ConstraintsADT a
  -> SMTExpr Bool
notStrongerThan :: forall a.
(Eq a, ToSMTVar a Int) =>
ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool
notStrongerThan ConstraintsADT a
t1 ConstraintsADT a
t2 | ConstraintsADT a
t1 forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t2            = SMTExpr Bool
smtTrue
notStrongerThan ConstraintsADT a
t1 ConstraintsADT a
_  | ConstraintsADT a
t1 forall a. Eq a => a -> a -> Bool
== forall a. ConstraintsADT a
noConstraints = SMTExpr Bool
smtTrue
notStrongerThan ConstraintsADT a
t1 ConstraintsADT a
t2            = SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool
Implies (forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
t2) (forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
t1)

noConstraints :: ConstraintsADT a
noConstraints :: forall a. ConstraintsADT a
noConstraints = forall a. WQO a -> ConstraintsADT a
Sat forall a. WQO a
WQO.empty

unsatisfiable :: ConstraintsADT a
unsatisfiable :: forall a. ConstraintsADT a
unsatisfiable = forall a. ConstraintsADT a
Unsat

{-# SPECIALIZE getConstraints :: ConstraintsADT Op -> [WQO Op] #-}
getConstraints :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> [WQO a]
getConstraints :: forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> [WQO a]
getConstraints ConstraintsADT a
adt = -- trace' ("Get constraints, size : " ++ (show $ dnfSize adt)) $
  forall s a. State s a -> s -> a
evalState (forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
adt) (forall a.
Map (ConstraintsADT a) (GCResult a)
-> Map (WQO a, WQO a) (Maybe (WQO a)) -> GCState a
GCState forall k a. Map k a
M.empty forall k a. Map k a
M.empty)

data GCState a = GCState {
    forall a. GCState a -> Map (ConstraintsADT a) (GCResult a)
cs :: M.Map (ConstraintsADT a) (GCResult a)
  , forall a. GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
ms :: M.Map (WQO a, WQO a) (Maybe (WQO a))
}

type GCResult a = [WQO a]

type GCMonad a = State (GCState a) (GCResult a)

cached :: (Ord a) => ConstraintsADT a -> GCMonad a -> GCMonad a
cached :: forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
key GCMonad a
thunk = do
  Map (ConstraintsADT a) (GCResult a)
cache <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a. GCState a -> Map (ConstraintsADT a) (GCResult a)
cs
  case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ConstraintsADT a
key Map (ConstraintsADT a) (GCResult a)
cache of
    Just GCResult a
result -> forall {p} {p}. p -> p -> p
trace'' String
"ADT Cache hit" forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return GCResult a
result
    Maybe (GCResult a)
Nothing     -> forall {p} {p}. p -> p -> p
trace'' String
"ADT Cache miss" forall a b. (a -> b) -> a -> b
$ do
      GCResult a
result <- forall {p} {p}. p -> p -> p
trace'' String
"Do thunk" GCMonad a
thunk
      forall {p} {p}. p -> p -> p
trace'' String
"Done" forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\GCState a
st -> GCState a
st{cs :: Map (ConstraintsADT a) (GCResult a)
cs = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ConstraintsADT a
key GCResult a
result (forall a. GCState a -> Map (ConstraintsADT a) (GCResult a)
cs GCState a
st)})
      forall (m :: * -> *) a. Monad m => a -> m a
return GCResult a
result
 where
   trace'' :: p -> p -> p
trace'' p
_  p
x = p
x
   -- trace' = trace

cached' :: (Hashable a, Show a, Ord a) => (WQO a, WQO a) -> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
cached' :: forall a.
(Hashable a, Show a, Ord a) =>
(WQO a, WQO a)
-> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
cached' (WQO a
lhs, WQO a
rhs) Maybe (WQO a)
thunk = do
  Map (WQO a, WQO a) (Maybe (WQO a))
cache <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a. GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
ms
  case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (WQO a
lhs, WQO a
rhs) Map (WQO a, WQO a) (Maybe (WQO a))
cache of
    Just Maybe (WQO a)
result -> forall {p} {p}. p -> p -> p
trace'' String
"WQO Cache hit" forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (WQO a)
result
    Maybe (Maybe (WQO a))
Nothing     -> forall {p} {p}. p -> p -> p
trace'' (String
"WQO Cache miss" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (WQO a
lhs, WQO a
rhs)) forall a b. (a -> b) -> a -> b
$ do
      forall {p} {p}. p -> p -> p
trace'' String
"Done" forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\GCState a
st -> GCState a
st{ms :: Map (WQO a, WQO a) (Maybe (WQO a))
ms = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (WQO a
rhs, WQO a
lhs) Maybe (WQO a)
thunk forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (WQO a
lhs, WQO a
rhs) Maybe (WQO a)
thunk (forall a. GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
ms GCState a
st)})
      forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (WQO a)
thunk
 where
   trace'' :: p -> p -> p
trace'' p
_  p
x = p
x
   -- trace' = trace

getConstraints' :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' :: forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' (Sat WQO a
w)         = forall (m :: * -> *) a. Monad m => a -> m a
return [WQO a
w]
getConstraints' ConstraintsADT a
Unsat           = forall (m :: * -> *) a. Monad m => a -> m a
return []
getConstraints' c :: ConstraintsADT a
c@(Union ConstraintsADT a
lhs ConstraintsADT a
rhs) =
  forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c forall a b. (a -> b) -> a -> b
$ do
    [WQO a]
c1' <- forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c1 forall a b. (a -> b) -> a -> b
$ forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c1
    [WQO a]
c2' <- forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c2 forall a b. (a -> b) -> a -> b
$ forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c2
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [WQO a]
c1' forall a. [a] -> [a] -> [a]
++ [WQO a]
c2'
  where
      (ConstraintsADT a
c1, ConstraintsADT a
c2) =
        if forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs forall a. Ord a => a -> a -> Bool
< forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs
        then (ConstraintsADT a
lhs, ConstraintsADT a
rhs)
        else (ConstraintsADT a
rhs, ConstraintsADT a
lhs)
getConstraints' c :: ConstraintsADT a
c@(Intersect ConstraintsADT a
lhs ConstraintsADT a
rhs) = forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c forall a b. (a -> b) -> a -> b
$ do
  [WQO a]
c1' <- forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c1 forall a b. (a -> b) -> a -> b
$ forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c1
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [WQO a]
c1'
    then forall (m :: * -> *) a. Monad m => a -> m a
return []
    else forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c2 (forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c2) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [WQO a] -> [WQO a] -> GCMonad a
go [WQO a]
c1'
  where
      go :: [WQO a] -> [WQO a] -> State (GCState a) [WQO a]
      go :: [WQO a] -> [WQO a] -> GCMonad a
go [WQO a]
c1' [WQO a]
c2' = forall {a}. [Maybe a] -> [a]
flatten forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (do
          WQO a
wqo1 <- [WQO a]
c1'
          WQO a
wqo2 <- [WQO a]
c2'
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall a.
(Hashable a, Show a, Ord a) =>
(WQO a, WQO a)
-> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
cached' (WQO a
wqo1, WQO a
wqo2) forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
wqo1 WQO a
wqo2))
      flatten :: [Maybe a] -> [a]
flatten = forall {a}. [Maybe a] -> [a]
Mb.catMaybes
      (ConstraintsADT a
c1, ConstraintsADT a
c2) =
        if forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs forall a. Ord a => a -> a -> Bool
> forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs
        then (ConstraintsADT a
lhs, ConstraintsADT a
rhs)
        else (ConstraintsADT a
rhs, ConstraintsADT a
lhs)

permits
  :: (Ord a, Hashable a, Show a)
  => ConstraintsADT a
  -> WQO.WQO a
  -> Bool
permits :: forall a.
(Ord a, Hashable a, Show a) =>
ConstraintsADT a -> WQO a -> Bool
permits ConstraintsADT a
adt WQO a
wqo = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
wqo) (forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> [WQO a]
getConstraints ConstraintsADT a
adt)

isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool
isSatisfiable :: forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> SMTExpr Bool
isSatisfiable = forall a b. ToSMT a b => a -> SMTExpr b
toSMT

instance (Eq a, Hashable a,  Show a) => Show (ConstraintsADT a) where
  show :: ConstraintsADT a -> String
show (Sat WQO a
w)         = forall a. Show a => a -> String
show WQO a
w
  show ConstraintsADT a
Unsat           = String
"⊥"
  show (Union ConstraintsADT a
w ConstraintsADT a
t )    = forall r. PrintfType r => String -> r
printf String
"(%s ∨\n %s)" (forall a. Show a => a -> String
show ConstraintsADT a
w) (forall a. Show a => a -> String
show ConstraintsADT a
t)
  show (Intersect ConstraintsADT a
w ConstraintsADT a
t) = forall r. PrintfType r => String -> r
printf String
"(%s ∧ %s)" (forall a. Show a => a -> String
show ConstraintsADT a
w) (forall a. Show a => a -> String
show ConstraintsADT a
t)

-- | See 'ConstraintsADT'
adtOC :: (Handle, Handle) -> OC.WQOConstraints ConstraintsADT IO
adtOC :: (Handle, Handle) -> WQOConstraints ConstraintsADT IO
adtOC (Handle, Handle)
z3 = forall (m :: * -> *) (m' :: * -> *) (impl :: * -> *).
(m Bool -> m' Bool)
-> WQOConstraints impl m -> WQOConstraints impl m'
OC.liftC ((Handle, Handle) -> SMTExpr Bool -> IO Bool
checkSat' (Handle, Handle)
z3) WQOConstraints ConstraintsADT SMTExpr
adtOC'

adtOC' :: OC.WQOConstraints ConstraintsADT SMTExpr
adtOC' :: WQOConstraints ConstraintsADT SMTExpr
adtOC' = forall (impl :: * -> *) (m :: * -> *).
(forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a)
-> (forall a.
    (Show a, Eq a, Ord a, Hashable a) =>
    impl a -> impl a -> impl a)
-> (forall a.
    (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
    impl a -> m Bool)
-> (forall a.
    (ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
    impl a -> impl a -> m Bool)
-> (forall a. (Eq a, Ord a, Hashable a) => impl a)
-> (forall a.
    (Show a, Eq a, Ord a, Hashable a) =>
    impl a -> WQO a -> Bool)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    impl a -> impl a -> impl a)
-> (forall a. impl a)
-> (forall a. impl a -> Maybe (WQO a))
-> WQOConstraints impl m
OC.OC
  forall a.
(Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
addConstraint
  forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect
  forall a.
(ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> SMTExpr Bool
isSatisfiable
  forall a.
(Eq a, ToSMTVar a Int) =>
ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool
notStrongerThan
  forall a. ConstraintsADT a
noConstraints
  forall a.
(Ord a, Hashable a, Show a) =>
ConstraintsADT a -> WQO a -> Bool
permits
  forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union
  forall a. ConstraintsADT a
unsatisfiable
  forall a. HasCallStack => a
undefined