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

#define OPTIMIZE_WQO

module Language.REST.WQOConstraints.ADT where

import GHC.Generics (Generic)

import Debug.Trace
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
(ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> Eq (ConstraintsADT a)
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, Eq (ConstraintsADT a)
Eq (ConstraintsADT a)
-> (ConstraintsADT a -> ConstraintsADT a -> Ordering)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> Bool)
-> (ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a)
-> (ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a)
-> Ord (ConstraintsADT a)
ConstraintsADT a -> ConstraintsADT a -> Bool
ConstraintsADT a -> ConstraintsADT a -> Ordering
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
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
$cp1Ord :: forall a. Ord a => Eq (ConstraintsADT a)
Ord, (forall x. ConstraintsADT a -> Rep (ConstraintsADT a) x)
-> (forall x. Rep (ConstraintsADT a) x -> ConstraintsADT a)
-> Generic (ConstraintsADT a)
forall x. Rep (ConstraintsADT a) x -> ConstraintsADT a
forall x. ConstraintsADT a -> Rep (ConstraintsADT a) x
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, Int -> ConstraintsADT a -> Int
ConstraintsADT a -> Int
(Int -> ConstraintsADT a -> Int)
-> (ConstraintsADT a -> Int) -> Hashable (ConstraintsADT a)
forall a. Hashable a => Int -> ConstraintsADT a -> Int
forall a. Hashable a => ConstraintsADT a -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
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)           = WQO a -> SMTExpr Bool
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  [ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w1, ConstraintsADT a -> SMTExpr Bool
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 [ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
w1, ConstraintsADT a -> SMTExpr Bool
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 :: ConstraintsADT a -> Int
cost (Union ConstraintsADT a
lhs ConstraintsADT a
rhs)     = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs) (ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs)
cost (Intersect ConstraintsADT a
lhs ConstraintsADT a
rhs) = ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
rhs
cost (Sat WQO a
wqo)           = Set a -> Int
forall a. Set a -> Int
S.size (Set a -> Int) -> Set a -> Int
forall a b. (a -> b) -> a -> b
$ WQO a -> Set a
forall a. Ord a => WQO a -> Set a
WQO.elems WQO a
wqo
cost ConstraintsADT a
Unsat               = Int
100

minDepth :: ConstraintsADT a -> Int
minDepth :: ConstraintsADT a -> Int
minDepth (Union ConstraintsADT a
lhs ConstraintsADT a
rhs)     = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
minDepth ConstraintsADT a
lhs) (ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
minDepth ConstraintsADT a
rhs)
minDepth (Intersect ConstraintsADT a
lhs ConstraintsADT a
rhs) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
minDepth ConstraintsADT a
lhs) (ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
minDepth ConstraintsADT a
rhs)
minDepth ConstraintsADT a
_                   = Int
1

maxDepth :: ConstraintsADT a -> Int
maxDepth :: ConstraintsADT a -> Int
maxDepth (Union ConstraintsADT a
lhs ConstraintsADT a
rhs)     = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
maxDepth ConstraintsADT a
lhs) (ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
maxDepth ConstraintsADT a
rhs)
maxDepth (Intersect ConstraintsADT a
lhs ConstraintsADT a
rhs) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
maxDepth ConstraintsADT a
lhs) (ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
maxDepth ConstraintsADT a
rhs)
maxDepth ConstraintsADT a
_                   = Int
1

intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a

#ifdef OPTIMIZE_WQO
-- Optimization
intersect :: ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect (Sat WQO a
t) (Sat WQO a
u) =
  case WQO a -> WQO a -> Maybe (WQO a)
forall a.
(Ord a, Eq a, Hashable a) =>
WQO a -> WQO a -> Maybe (WQO a)
WQO.merge WQO a
t WQO a
u of
    Just WQO a
t' -> WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
t'
    Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
#endif

intersect (Sat WQO a
w) ConstraintsADT a
v            | WQO a
w WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = ConstraintsADT a
v
intersect ConstraintsADT a
v            (Sat WQO a
w) | WQO a
w WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = ConstraintsADT a
v
intersect ConstraintsADT a
_ ConstraintsADT a
Unsat     = ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect ConstraintsADT a
Unsat ConstraintsADT a
_     = ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect ConstraintsADT a
t1 ConstraintsADT a
t2 | ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> Bool
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 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
t2 Bool -> Bool -> Bool
|| ConstraintsADT a
t1 ConstraintsADT a -> ConstraintsADT a -> Bool
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 WQO a -> WQO a -> Maybe (WQO a)
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 -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w') ConstraintsADT a
t2
    Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect (Sat WQO a
w1) (Intersect ConstraintsADT a
t2 (Sat WQO a
w2)) =
  case WQO a -> WQO a -> Maybe (WQO a)
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 -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w') ConstraintsADT a
t2
    Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect (Intersect ConstraintsADT a
t1 (Sat WQO a
w1)) (Sat WQO a
w2) =
  case WQO a -> WQO a -> Maybe (WQO a)
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 -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect ConstraintsADT a
t1 (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w')
    Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
intersect (Intersect (Sat WQO a
w1) ConstraintsADT a
t1) (Sat WQO a
w2) =
  case WQO a -> WQO a -> Maybe (WQO a)
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 -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect ConstraintsADT a
t1 (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w')
    Maybe (WQO a)
Nothing -> ConstraintsADT a
forall a. ConstraintsADT a
Unsat
#endif
intersect ConstraintsADT a
t1 ConstraintsADT a
t2            = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
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 :: ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union (Sat WQO a
w) ConstraintsADT a
_            | WQO a
w WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w
union ConstraintsADT a
_            (Sat WQO a
w) | WQO a
w WQO a -> WQO a -> Bool
forall a. Eq a => a -> a -> Bool
== WQO a
forall a. WQO a
WQO.empty = WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
w
union (Intersect ConstraintsADT a
a ConstraintsADT a
b)  ConstraintsADT a
c | ConstraintsADT a
a ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c Bool -> Bool -> Bool
|| ConstraintsADT a
b ConstraintsADT a -> ConstraintsADT a -> Bool
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 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
b Bool -> Bool -> Bool
|| ConstraintsADT a
a ConstraintsADT a -> ConstraintsADT a -> Bool
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 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
b           = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
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 ConstraintsADT a -> ConstraintsADT a -> Bool
forall a. Eq a => a -> a -> Bool
== ConstraintsADT a
c2 = ConstraintsADT a
c1
union ConstraintsADT a
c1 ConstraintsADT a
c2            = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
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 :: WQO a -> ConstraintsADT a -> ConstraintsADT a
addConstraint WQO a
o ConstraintsADT a
c = ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
intersect (WQO a -> ConstraintsADT a
forall a. WQO a -> ConstraintsADT a
Sat WQO a
o) ConstraintsADT a
c

relevantConstraints
  :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> S.Set a -> S.Set a -> ConstraintsADT a
relevantConstraints :: ConstraintsADT a -> Set a -> Set a -> ConstraintsADT a
relevantConstraints ConstraintsADT a
c Set a
_ Set a
_ = ConstraintsADT a
c

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

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

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

trace' :: String -> a -> a
trace' :: String -> a -> a
trace' = String -> a -> a
forall a. String -> a -> a
trace

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

data GCState a = GCState {
    GCState a -> Map (ConstraintsADT a) (GCResult a)
cs :: M.Map (ConstraintsADT a) (GCResult 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 :: ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
key GCMonad a
thunk = do
  Map (ConstraintsADT a) (GCResult a)
cache <- (GCState a -> Map (ConstraintsADT a) (GCResult a))
-> StateT
     (GCState a) Identity (Map (ConstraintsADT a) (GCResult a))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets GCState a -> Map (ConstraintsADT a) (GCResult a)
forall a. GCState a -> Map (ConstraintsADT a) (GCResult a)
cs
  case ConstraintsADT a
-> Map (ConstraintsADT a) (GCResult a) -> Maybe (GCResult a)
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 -> String -> GCMonad a -> GCMonad a
forall p p. p -> p -> p
trace'' (String
"ADT Cache hit") (GCMonad a -> GCMonad a) -> GCMonad a -> GCMonad a
forall a b. (a -> b) -> a -> b
$ GCResult a -> GCMonad a
forall (m :: * -> *) a. Monad m => a -> m a
return GCResult a
result
    Maybe (GCResult a)
Nothing     -> String -> GCMonad a -> GCMonad a
forall p p. p -> p -> p
trace'' (String
"ADT Cache miss") (GCMonad a -> GCMonad a) -> GCMonad a -> GCMonad a
forall a b. (a -> b) -> a -> b
$ do
      GCResult a
result <- String -> GCMonad a -> GCMonad a
forall p p. p -> p -> p
trace'' String
"Do thunk" GCMonad a
thunk
      String
-> StateT (GCState a) Identity () -> StateT (GCState a) Identity ()
forall p p. p -> p -> p
trace'' String
"Done" (StateT (GCState a) Identity () -> StateT (GCState a) Identity ())
-> StateT (GCState a) Identity () -> StateT (GCState a) Identity ()
forall a b. (a -> b) -> a -> b
$ (GCState a -> GCState a) -> StateT (GCState a) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\GCState a
st -> GCState a
st{cs :: Map (ConstraintsADT a) (GCResult a)
cs = ConstraintsADT a
-> GCResult a
-> Map (ConstraintsADT a) (GCResult a)
-> Map (ConstraintsADT a) (GCResult a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ConstraintsADT a
key GCResult a
result (GCState a -> Map (ConstraintsADT a) (GCResult a)
forall a. GCState a -> Map (ConstraintsADT a) (GCResult a)
cs GCState a
st)})
      GCResult a -> GCMonad a
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' :: (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 <- (GCState a -> Map (WQO a, WQO a) (Maybe (WQO a)))
-> StateT (GCState a) Identity (Map (WQO a, WQO a) (Maybe (WQO a)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
forall a. GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
ms
  case (WQO a, WQO a)
-> Map (WQO a, WQO a) (Maybe (WQO a)) -> Maybe (Maybe (WQO a))
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 -> String
-> State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a))
forall p p. p -> p -> p
trace'' (String
"WQO Cache hit") (State (GCState a) (Maybe (WQO a))
 -> State (GCState a) (Maybe (WQO a)))
-> State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a))
forall a b. (a -> b) -> a -> b
$ Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (WQO a)
result
    Maybe (Maybe (WQO a))
Nothing     -> String
-> State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a))
forall p p. p -> p -> p
trace'' (String
"WQO Cache miss" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (WQO a, WQO a) -> String
forall a. Show a => a -> String
show (WQO a
lhs, WQO a
rhs)) (State (GCState a) (Maybe (WQO a))
 -> State (GCState a) (Maybe (WQO a)))
-> State (GCState a) (Maybe (WQO a))
-> State (GCState a) (Maybe (WQO a))
forall a b. (a -> b) -> a -> b
$ do
      String
-> StateT (GCState a) Identity () -> StateT (GCState a) Identity ()
forall p p. p -> p -> p
trace'' String
"Done" (StateT (GCState a) Identity () -> StateT (GCState a) Identity ())
-> StateT (GCState a) Identity () -> StateT (GCState a) Identity ()
forall a b. (a -> b) -> a -> b
$ (GCState a -> GCState a) -> StateT (GCState a) Identity ()
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 = (WQO a, WQO a)
-> Maybe (WQO a)
-> Map (WQO a, WQO a) (Maybe (WQO a))
-> Map (WQO a, WQO a) (Maybe (WQO a))
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 (Map (WQO a, WQO a) (Maybe (WQO a))
 -> Map (WQO a, WQO a) (Maybe (WQO a)))
-> Map (WQO a, WQO a) (Maybe (WQO a))
-> Map (WQO a, WQO a) (Maybe (WQO a))
forall a b. (a -> b) -> a -> b
$ (WQO a, WQO a)
-> Maybe (WQO a)
-> Map (WQO a, WQO a) (Maybe (WQO a))
-> Map (WQO a, WQO a) (Maybe (WQO a))
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 (GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
forall a. GCState a -> Map (WQO a, WQO a) (Maybe (WQO a))
ms GCState a
st)})
      Maybe (WQO a) -> State (GCState a) (Maybe (WQO a))
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' :: ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' (Sat WQO a
w)         = [WQO a] -> State (GCState a) [WQO a]
forall (m :: * -> *) a. Monad m => a -> m a
return [WQO a
w]
getConstraints' ConstraintsADT a
Unsat           = [WQO a] -> State (GCState a) [WQO a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
getConstraints' c :: ConstraintsADT a
c@(Union ConstraintsADT a
lhs ConstraintsADT a
rhs) =
  ConstraintsADT a
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c (State (GCState a) [WQO a] -> State (GCState a) [WQO a])
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a b. (a -> b) -> a -> b
$ do
    [WQO a]
c1' <- ConstraintsADT a
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c1 (State (GCState a) [WQO a] -> State (GCState a) [WQO a])
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a b. (a -> b) -> a -> b
$ ConstraintsADT a -> State (GCState a) [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c1
    [WQO a]
c2' <- ConstraintsADT a
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c2 (State (GCState a) [WQO a] -> State (GCState a) [WQO a])
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a b. (a -> b) -> a -> b
$ ConstraintsADT a -> State (GCState a) [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c2
    [WQO a] -> State (GCState a) [WQO a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([WQO a] -> State (GCState a) [WQO a])
-> [WQO a] -> State (GCState a) [WQO a]
forall a b. (a -> b) -> a -> b
$ [WQO a]
c1' [WQO a] -> [WQO a] -> [WQO a]
forall a. [a] -> [a] -> [a]
++ [WQO a]
c2'
  where
      (ConstraintsADT a
c1, ConstraintsADT a
c2) =
        if ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ConstraintsADT a -> Int
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) = ConstraintsADT a
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c (State (GCState a) [WQO a] -> State (GCState a) [WQO a])
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a b. (a -> b) -> a -> b
$ do
  [WQO a]
c1' <- ConstraintsADT a
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c1 (State (GCState a) [WQO a] -> State (GCState a) [WQO a])
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a b. (a -> b) -> a -> b
$ ConstraintsADT a -> State (GCState a) [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c1
  if [WQO a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [WQO a]
c1'
    then [WQO a] -> State (GCState a) [WQO a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    else (ConstraintsADT a
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a. Ord a => ConstraintsADT a -> GCMonad a -> GCMonad a
cached ConstraintsADT a
c2 (State (GCState a) [WQO a] -> State (GCState a) [WQO a])
-> State (GCState a) [WQO a] -> State (GCState a) [WQO a]
forall a b. (a -> b) -> a -> b
$ ConstraintsADT a -> State (GCState a) [WQO a]
forall a.
(Show a, Ord a, Hashable a) =>
ConstraintsADT a -> State (GCState a) [WQO a]
getConstraints' ConstraintsADT a
c2) State (GCState a) [WQO a]
-> ([WQO a] -> State (GCState a) [WQO a])
-> State (GCState a) [WQO a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [WQO a] -> [WQO a] -> State (GCState a) [WQO a]
go [WQO a]
c1'
  where
      go :: [WQO a] -> [WQO a] -> State (GCState a) [WQO a]
      go :: [WQO a] -> [WQO a] -> State (GCState a) [WQO a]
go [WQO a]
c1' [WQO a]
c2' = [Maybe (WQO a)] -> [WQO a]
forall b. [Maybe b] -> [b]
flatten ([Maybe (WQO a)] -> [WQO a])
-> StateT (GCState a) Identity [Maybe (WQO a)]
-> State (GCState a) [WQO a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ([StateT (GCState a) Identity (Maybe (WQO a))]
-> StateT (GCState a) Identity [Maybe (WQO a)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([StateT (GCState a) Identity (Maybe (WQO a))]
 -> StateT (GCState a) Identity [Maybe (WQO a)])
-> [StateT (GCState a) Identity (Maybe (WQO a))]
-> StateT (GCState a) Identity [Maybe (WQO a)]
forall a b. (a -> b) -> a -> b
$ do
          WQO a
wqo1 <- [WQO a]
c1'
          WQO a
wqo2 <- [WQO a]
c2'
          StateT (GCState a) Identity (Maybe (WQO a))
-> [StateT (GCState a) Identity (Maybe (WQO a))]
forall (m :: * -> *) a. Monad m => a -> m a
return ((WQO a, WQO a)
-> Maybe (WQO a) -> StateT (GCState a) Identity (Maybe (WQO a))
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) (Maybe (WQO a) -> StateT (GCState a) Identity (Maybe (WQO a)))
-> Maybe (WQO a) -> StateT (GCState a) Identity (Maybe (WQO a))
forall a b. (a -> b) -> a -> b
$ WQO a -> WQO a -> Maybe (WQO a)
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 b] -> [b]
flatten = (Maybe b -> [b]) -> [Maybe b] -> [b]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Maybe b -> [b]
forall a. Maybe a -> [a]
Mb.maybeToList
      (ConstraintsADT a
c1, ConstraintsADT a
c2) =
        if ConstraintsADT a -> Int
forall a. (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int
cost ConstraintsADT a
lhs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> ConstraintsADT a -> Int
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)

dnfSize :: ConstraintsADT a -> Int
dnfSize :: ConstraintsADT a -> Int
dnfSize (Sat WQO a
_w)       = Int
1
dnfSize ConstraintsADT a
Unsat         = Int
0
dnfSize (Union ConstraintsADT a
w1 ConstraintsADT a
w2) = ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
dnfSize ConstraintsADT a
w1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
dnfSize ConstraintsADT a
w2
dnfSize (Intersect ConstraintsADT a
w1 ConstraintsADT a
w2) = ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
dnfSize ConstraintsADT a
w1 Int -> Int -> Int
forall a. Num a => a -> a -> a
* ConstraintsADT a -> Int
forall a. ConstraintsADT a -> Int
dnfSize ConstraintsADT a
w2

-- toDNF (Union lhs rhs) = S.union (toDNF lhs) (toDNF rhs)
-- toDNF (Intersect lhs rhs) =
--   let
--     ldnf = toDNF lhs
--     rdnf = toDNF rhs
--   in
--     S.unions

simplify :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a
simplify :: ConstraintsADT a -> ConstraintsADT a
simplify ConstraintsADT a
_adt = ConstraintsADT a
forall a. HasCallStack => a
undefined
-- simplify adt = case getConstraints adt of
--   []     -> Unsat
--   (x:xs) -> foldl go (Sat x) xs
--   where
--     go a x = Union (Sat x) a

permits
  :: (Ord a, Hashable a, Show a)
  => ConstraintsADT a
  -> WQO.WQO a
  -> Bool
permits :: ConstraintsADT a -> WQO a -> Bool
permits ConstraintsADT a
adt WQO a
wqo = (WQO a -> Bool) -> [WQO a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (WQO a -> WQO a -> Bool
forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool
`WQO.notStrongerThan` WQO a
wqo) (ConstraintsADT a -> [WQO a]
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 :: ConstraintsADT a -> SMTExpr Bool
isSatisfiable ConstraintsADT a
s = ConstraintsADT a -> SMTExpr Bool
forall a b. ToSMT a b => a -> SMTExpr b
toSMT ConstraintsADT a
s
  -- trace (show (minDepth s) ++ " " ++ show (maxDepth s)) $ not $ null $ getConstraints s

instance (Eq a, Hashable a,  Show a) => Show (ConstraintsADT a) where
  -- show s = go 0 s where
  --   go n (Sat w)         = indent n $ show w
  --   go n Unsat           = indent n $ "⊥"
  --   go n (Union w t )    = indent n $ printf "∪\n%s\n%s" (go (n+1) w) (go (n+1) t)
  --   go n (Intersect w t) = indent n $ printf "∩\n%s\n%s" (go (n+1) w) (go (n+1) t)

  --   indent 0 s = s
  --   indent n s = take (n - 1) (repeat '|') ++ '+':s

  show :: ConstraintsADT a -> String
show (Sat WQO a
w)         = WQO a -> String
forall a. Show a => a -> String
show WQO a
w
  show ConstraintsADT a
Unsat           = String
"⊥"
  show (Union ConstraintsADT a
w ConstraintsADT a
t )    = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"(%s ∨\n %s)" (ConstraintsADT a -> String
forall a. Show a => a -> String
show ConstraintsADT a
w) (ConstraintsADT a -> String
forall a. Show a => a -> String
show ConstraintsADT a
t)
  show (Intersect ConstraintsADT a
w ConstraintsADT a
t) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"(%s ∧ %s)" (ConstraintsADT a -> String
forall a. Show a => a -> String
show ConstraintsADT a
w) (ConstraintsADT a -> String
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 = (SMTExpr Bool -> IO Bool)
-> WQOConstraints ConstraintsADT SMTExpr
-> WQOConstraints ConstraintsADT IO
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 a.
 (Eq a, Ord a, Hashable a) =>
 WQO a -> ConstraintsADT a -> ConstraintsADT a)
-> (forall a.
    (Show a, Eq a, Ord a, Hashable a) =>
    ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a)
-> (forall a.
    (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) =>
    ConstraintsADT a -> SMTExpr Bool)
-> (forall a.
    (ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
    ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool)
-> (forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a)
-> (forall a.
    (Show a, Eq a, Ord a, Hashable a) =>
    ConstraintsADT a -> WQO a -> Bool)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    ConstraintsADT a -> Set a -> Set a -> ConstraintsADT a)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a)
-> (forall a. ConstraintsADT a)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    ConstraintsADT a -> Set a)
-> (forall a. ConstraintsADT a -> Maybe (WQO a))
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    ConstraintsADT a -> ConstraintsADT a)
-> WQOConstraints ConstraintsADT SMTExpr
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 -> Set a -> Set a -> impl a)
-> (forall a.
    (Eq a, Ord a, Hashable a) =>
    impl a -> impl a -> impl a)
-> (forall a. impl a)
-> (forall a. (Eq a, Ord a, Hashable a) => impl a -> Set a)
-> (forall a. impl a -> Maybe (WQO a))
-> (forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a)
-> WQOConstraints impl m
OC.OC
  forall a.
(Eq a, Ord a, Hashable a) =>
WQO a -> ConstraintsADT a -> ConstraintsADT a
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
forall a.
(Show 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
forall a.
(ToSMTVar a Int, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> SMTExpr Bool
notStrongerThan
  forall a. ConstraintsADT a
forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a
noConstraints
  forall a.
(Ord a, Hashable a, Show a) =>
ConstraintsADT a -> WQO a -> Bool
forall a.
(Show a, Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> WQO a -> Bool
permits
  forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> Set a -> Set a -> ConstraintsADT a
relevantConstraints
  forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
forall a.
Eq a =>
ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a
union
  forall a. ConstraintsADT a
unsatisfiable
  forall a. (Eq a, Ord a, Hashable a) => ConstraintsADT a -> Set a
forall a. HasCallStack => a
undefined
  forall a. ConstraintsADT a -> Maybe (WQO a)
forall a. HasCallStack => a
undefined
  forall a.
(Eq a, Ord a, Hashable a) =>
ConstraintsADT a -> ConstraintsADT a
simplify