{-# 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
data ConstraintsADT a =
Sat (WQO a)
| Unsat
| Union (ConstraintsADT a) (ConstraintsADT a)
| 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 :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
#ifdef OPTIMIZE_WQO
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 :: 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
:: (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 =
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
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
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)
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