Documentation

data WQOConstraints impl m Source #

type ConstraintGen oc base lifted m = forall m'. WQOConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base) Source #

liftC :: (m Bool -> m' Bool) -> WQOConstraints impl m -> WQOConstraints impl m' Source #

cmapConstraints :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m Source #

numOrderings :: (Show a, Ord a, Eq a, Ord a, Hashable a) => Set a -> WQOConstraints oc m -> oc a -> Int Source #

isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => WQOConstraints oc m -> oc a -> m Bool Source #

intersectAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a Source #

unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a Source #

intersectRelation :: (Ord a, Eq a, Ord a, Hashable a, Show a) => WQOConstraints oc m -> oc a -> (a, a, Relation) -> oc a Source #

runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity Source #

singleton :: (Eq a, Ord a, Hashable a) => WQOConstraints oc m -> WQO a -> oc a Source #