Commit 4e3682e7 authored by Bastian Kauschke's avatar Bastian Kauschke

implement coalgebra minimization

parent 230aebfa
......@@ -37,6 +37,7 @@ library
, Data.SumBag
, Data.Bits.Monoid
, Copar.RefinementInterface
, Copar.MinimizationInterface
, Copar.Functors
, Copar.FunctorDescription
, Copar.FunctorPrinter
......@@ -65,6 +66,7 @@ library
, Copar.Coalgebra.Parser.Class
, Copar.Coalgebra.Parser.Internal
, Copar.Coalgebra.Printer
, Copar.Minimize
, Copar.PartitionPrinter
, Copar.Dot
, Copar.PrettyShow
......
......@@ -45,7 +45,7 @@ printEncoding encoding symbols sorts =
list <- MV.replicate (size encoding) []
V.rforM_ edges $
\edge -> MV.modify list ((desortedLabel @f (label edge), printState (to edge)):) (from edge)
V.freeze list
V.freeze list
printState :: State -> Build.Builder
printState state = maybe (morphismPoint state) Build.fromText (HM.lookup state (fromSymbolTable symbols))
......@@ -32,12 +32,14 @@ import Type.Reflection
import Copar.FunctorExpression.Parser
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.Coalgebra.Parser.Class
import Copar.Coalgebra.Printer
import Copar.PrettyShow
type Suitable f
= ( RefinementInterface f
, MinimizationInterface f
, ParseMorphism f
, PrintMorphism f
, Eq1 f
......
......@@ -49,6 +49,7 @@ import Copar.Coalgebra.Parser
import Copar.Coalgebra.Printer
import qualified Copar.Parser.Lexer as L
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.Functors.Polynomial hiding ( PolyF1(..) )
import qualified Copar.Functors.Polynomial as Poly
import qualified Copar.Functors.SomeFunctor as SF
......@@ -58,6 +59,7 @@ import Copar.Parser.Types
import qualified Data.Vector.Utils as V
import Data.Primitive.SmallArray
import Data.Function (on)
data Inner f a = Direct a | Absorbed (f a)
......@@ -253,7 +255,26 @@ instance RefinementInterface f => RefinementInterface (AbsorbingPolynomial f) wh
doUpdate _ PolyWeightToSub =
(PolyWeightToSub, PolyF3ToSub, PolyWeightToRest)
instance MinimizationInterface f => MinimizationInterface (AbsorbingPolynomial f) where
merge (AbsorbingPolynomial poly) lbls =
concatMap updateInner
$ NonEmpty.groupBy ((==) `on` labelIdx)
$ NonEmpty.sortBy (compare `on` labelIdx) lbls
where
labelIdx (PolyLabel i _) = i
updateInner :: NonEmpty (PolyLabel f) -> [PolyLabel f]
updateInner ((PolyLabel i (Just inner)):|ll) = map (\v -> PolyLabel i (Just v)) $ merge (innerFunctor i) (inner:|(innerLbls ll))
updateInner ((PolyLabel i Nothing):|ll) = (PolyLabel i Nothing):ll
innerLbls l = map (\(PolyLabel _ lbl) -> fromJust lbl) l
innerFunctors = V.fromList $ toList poly
innerFunctor :: Int -> f ()
innerFunctor i = case innerFunctors V.! i of
Direct _ -> undefined -- If labels exist for i this has to be an absorbed functor.
Absorbed f -> f
-- | Parse morphism for inner functor
--
-- If the inner value is just a variable, return (Nothing, [(x, Nothing)]). If
......
......@@ -23,6 +23,7 @@ import qualified Data.Text.Prettyprint as Doc
import Data.Text.Prettyprint ((<+>))
import Copar.RefinementInterface
import Copar.MinimizationInterface
import qualified Copar.Parser.Lexer as L
import Copar.FunctorExpression.Parser
import Copar.Coalgebra.Parser
......@@ -79,3 +80,6 @@ instance ParseMorphism Bag where
instance RefinementInterface Bag where
init = init @(GroupValued Int)
update = update @(GroupValued Int)
instance MinimizationInterface Bag where
merge _ = merge (GroupValued @Int ())
......@@ -24,6 +24,7 @@ import Copar.FunctorExpression.Parser
import Copar.Functors.GroupValued
import qualified Copar.Parser.Lexer as L
import Copar.RefinementInterface
import Copar.MinimizationInterface
newtype Distribution x = Distribution x
......@@ -88,3 +89,6 @@ instance RefinementInterface Distribution where
!toCwithoutS = w - toS
!f3 = mkGroupF3 toCwithoutS toS
in (toS, f3, toCwithoutS)
instance MinimizationInterface Distribution where
merge _ = merge (GroupValued @EqDouble ())
......@@ -26,6 +26,7 @@ import Data.Foldable.Utils
import Data.Ratio
import Data.Functor.Classes
import qualified Data.List as List
import Data.Vector (Vector)
import qualified Data.Vector as V
import Text.Megaparsec
......@@ -38,6 +39,7 @@ import qualified Data.Text.Lazy.Builder.Int as Build
import Data.Float.Utils (EqDouble(..))
import qualified Data.Vector.Utils as V
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.Coalgebra.Parser
import Copar.Coalgebra.Printer
import Copar.FunctorExpression.Parser
......@@ -234,7 +236,7 @@ parseMorphismPointHelper inner weightParser sanity = do
{-# SPECIALIZE parseMorphismPointHelper :: MorphParser l f1 Int -> MorphParser l f1 EqDouble -> Bool -> MorphParser l f1 (EqDouble, Vector (Int, EqDouble)) #-}
instance PrintMorphism (GroupValued Int) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem (List.sortOn snd edges) <> "}"
where printElem (value, state) = state <> ": " <> Build.decimal value
instance ParseMorphism (GroupValued Int) where
......@@ -243,7 +245,7 @@ instance ParseMorphism (GroupValued Int) where
=<< (not <$> noSanityChecks)
instance PrintMorphism (GroupValued EqDouble) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem (List.sortOn snd edges) <> "}"
where printElem (EqDouble value, state) = state <> ": " <> printFloat value
instance ParseMorphism (GroupValued EqDouble) where
......@@ -252,7 +254,7 @@ instance ParseMorphism (GroupValued EqDouble) where
=<< (not <$> noSanityChecks)
instance PrintMorphism (GroupValued OrderedComplex) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem (List.sortOn snd edges) <> "}"
where
printElem (OrderedComplex value, state) =
state <> ": " <>
......@@ -266,7 +268,7 @@ instance ParseMorphism (GroupValued OrderedComplex) where
=<< (not <$> noSanityChecks)
instance PrintMorphism (GroupValued (Ratio Int)) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " printElem (List.sortOn snd edges) <> "}"
where
printElem (value, state) =
state <> ": " <>
......@@ -295,3 +297,6 @@ instance (IsGroupF3 m, Ord m, Num m) => RefinementInterface (GroupValued m) wher
, mkGroupF3 toCwithoutS toS
, toCwithoutS
)
instance (IsGroupF3 m, Ord m, Num m) => MinimizationInterface (GroupValued m) where
merge _ weights = filter (/=0) [sum weights]
......@@ -38,6 +38,7 @@ import qualified Data.Text.Lazy.Builder.Int as Build
import qualified Data.Vector.Utils as V
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.FunctorDescription
import qualified Copar.Parser.Lexer as L
import Copar.FunctorExpression.Parser
......@@ -211,6 +212,9 @@ instance (Monoid m, Ord m) => RefinementInterface (SlowMonoidValued m) where
w2 = (sumRest <> sumS, toCWithoutS)
in (w1, f3, w2)
instance (Monoid m, Ord m) => MinimizationInterface (SlowMonoidValued m) where
merge _ lbls = filter (/=mempty) [fold lbls]
instance PrintMorphism (SlowMonoidValued (Max Int)) where
printMorphismPoint _ _ edges = "{" <> sepFold ", " printEdge edges <> "}"
where printEdge ((Max value), state) = state <> ": " <> Build.decimal value
......
......@@ -25,7 +25,6 @@ import Data.Bifunctor
import Data.Foldable.Utils
import Data.Foldable (fold)
import Data.Traversable (mapAccumL)
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Word (Word8)
......@@ -38,7 +37,7 @@ import Data.Either ( lefts
import qualified Data.Vector.Utils as V
import Data.Text (Text)
import Data.Maybe (fromJust)
import qualified Data.List as List
import Data.Vector (Vector)
import qualified Data.Vector as V
import qualified Data.Vector.Unboxed as VU
......@@ -58,6 +57,7 @@ import Copar.Coalgebra.Printer
import qualified Copar.Parser.Lexer as L
import Copar.Parser.Types
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.FunctorExpression.Parser
import Copar.FunctorDescription
......@@ -303,32 +303,36 @@ printSumPoint (Sum sum) f1 edges =
printProductPoint :: Product () -> F1 Polynomial -> [(Label Polynomial, Build.Builder)] -> Build.Builder
printProductPoint (Product prod) f1 edges' =
let inner = sepFold ", " id (snd (mapAccumL printFactor (0, edges') prod))
let inner = sepFold ", " id (snd (mapAccumL printFactor (0, 0) prod))
in if NonEmpty.length prod /= 1 then "(" <> inner <> ")" else inner
where
printFactor :: (Int, [(Label Polynomial, Build.Builder)])
edges = V.fromList . map snd $ List.sortOn fst edges'
printFactor :: (Int, Int)
-> Factor ()
-> ((Int, [(Label Polynomial, Build.Builder)]), Build.Builder)
printFactor (ct, edges) (Const IntSet) = ((ct + 1, edges), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edges) (Const NatSet) = ((ct + 1, edges), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edges) (Const (FiniteNatSet _)) = ((ct + 1, edges), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edges) (Const (ExplicitSet elems)) =
((ct + 1, edges), Build.fromText $ elems V.! (polyF1Constants f1 VU.! ct))
printFactor (ct, edges) (Identity ()) = ((ct, rest), snd var)
where (var, rest) = fromJust $ List.uncons edges
printFactor (ct, edges) (Exponential () (ExplicitExp elems)) =
let ((ct', edges'), elems') = mapAccumL (printExp Build.fromText) (ct, edges) elems
in ((ct', edges'), "{" <> sepFold ", " id elems' <> "}")
printFactor (ct, edges) (Exponential () (FiniteNatExp size)) =
let ((ct', edges'), elems') = mapAccumL (printExp Build.decimal) (ct, edges) (take size [(0 :: Int)..])
in ((ct', edges'), "{" <> sepFold ", " id elems' <> "}")
-> ((Int, Int), Build.Builder)
printFactor (ct, edge) (Const IntSet) = ((ct + 1, edge), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edge) (Const NatSet) = ((ct + 1, edge), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edge) (Const (FiniteNatSet _)) = ((ct + 1, edge), Build.decimal (polyF1Constants f1 VU.! ct))
printFactor (ct, edge) (Const (ExplicitSet elems)) =
((ct + 1, edge), Build.fromText $ elems V.! (polyF1Constants f1 VU.! ct))
printFactor (ct, edge) (Identity ()) = ((ct, edge + 1), edges V.! edge)
printFactor (ct, edge) (Exponential () (ExplicitExp elems)) =
let ((ct', edge'), elems') = mapAccumL (printExp Build.fromText) (ct, edge) elems
in ((ct', edge'), "{" <> sepFold ", " id elems' <> "}")
printFactor (ct, edge) (Exponential () (FiniteNatExp size)) =
let ((ct', edge'), elems') = mapAccumL (printExp Build.decimal) (ct, edge) (take size [(0 :: Int)..])
in ((ct', edge'), "{" <> sepFold ", " id elems' <> "}")
printExp :: (a -> Build.Builder)
-> (Int, [(Label Polynomial, Build.Builder)])
-> (Int, Int)
-> a
-> ((Int, [(Label Polynomial, Build.Builder)]), Build.Builder)
printExp toBuilder (ct, edges) elem = ((ct, rest), toBuilder elem <> ": " <> snd var)
where (var, rest) = fromJust $ List.uncons edges
-> ((Int, Int), Build.Builder)
printExp toBuilder (ct, edge) elem =
((ct, edge + 1), toBuilder elem <> ": " <> edges V.! edge)
instance MinimizationInterface Polynomial where
merge _ = NonEmpty.toList
instance ParseMorphism Polynomial where
parseMorphismPoint (Polynomial expr) = parseSum1 expr
......
......@@ -16,6 +16,7 @@ import Data.Bits
import Data.Foldable.Utils
import Text.Megaparsec
import Data.List as List
import qualified Data.Vector as V
import qualified Data.Vector.Utils as V
import Data.Eq.Deriving (deriveEq1)
......@@ -24,6 +25,7 @@ import qualified Data.Text.Prettyprint as Doc
import Data.Text.Prettyprint ((<+>))
import Copar.RefinementInterface
import Copar.MinimizationInterface
import qualified Copar.Parser.Lexer as L
import Copar.FunctorExpression.Parser
import Copar.Coalgebra.Parser
......@@ -83,7 +85,7 @@ type instance F1 Powerset = Bool
type instance F3 Powerset = PowerF3
instance PrintMorphism Powerset where
printMorphismPoint _ _ edges = "{" <> sepFold ", " snd edges <> "}"
printMorphismPoint _ _ edges = "{" <> sepFold ", " snd (List.sortOn snd edges) <> "}"
instance ParseMorphism Powerset where
parseMorphismPoint (Powerset inner) = do
......@@ -126,3 +128,6 @@ instance RefinementInterface Powerset where
!weightToCwithoutS = packWeight (toRest || toS > 0) toCwithoutS
in
(weightToS, f3, weightToCwithoutS)
instance MinimizationInterface Powerset where
merge _ _ = [()]
......@@ -40,6 +40,7 @@ import Copar.FunctorExpression.Parser
import Copar.PrettyShow
import Copar.RefinementInterface
import Copar.MinimizationInterface
import Copar.FunctorDescription
......@@ -200,6 +201,20 @@ instance RefinementInterface SomeFunctor where
Just HRefl -> Just l
#endif
instance MinimizationInterface SomeFunctor where
merge (SomeFunctor (f :: f' ())) lbls =
#ifdef RELEASE
map SomeLabel (unsafeCoerce (merge f (unsafeCoerce lbls)))
#else
map (SomeLabel (typeRep @f')) $ merge f (fmap isSameType lbls)
where
isSameType :: SomeLabel -> Label f'
isSameType (SomeLabel f2 l) = case eqTypeRep f2 $ typeRep @f' of
-- this case should not happen.
Nothing -> error "Inconsistent internal state: Labels for different functors in SomeFunctor"
Just HRefl -> l
#endif
instance PrintMorphism SomeFunctor where
printMorphismPoint (SomeFunctor (f :: f' ())) f1 edges =
printMorphismPoint f (mapF1 f1) (mapMaybe mapEdges edges)
......@@ -228,5 +243,4 @@ instance ParseMorphism SomeFunctor where
#else
let newSuccs = V.map (\(x, y) -> (x, SomeLabel fRep y)) succs
#endif
return (newF1, newSuccs)
module Copar.MinimizationInterface
( MinimizationInterface(..)
) where
import Copar.RefinementInterface
import Data.List.NonEmpty
class RefinementInterface f => MinimizationInterface f where
-- | Merges the given labels.
--
-- Note: As merge [] = [] would always hold,
-- we can instead use NonEmpty here which simplifies the
-- implementation and is slightly more performant.
merge :: f () -> NonEmpty (Label f) -> [Label f]
module Copar.Minimize (minimize) where
import qualified Data.HashMap.Strict as HM
import Data.MorphismEncoding as Encoding
import Data.Partition
import qualified Data.Text as T
import Data.Foldable.Utils
import qualified Data.Vector as V
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe (mapMaybe)
import Copar.FunctorExpression.Type
import Copar.FunctorExpression.Desorting
import Copar.FunctorExpression.Sorts (Sort, sortTable)
import Copar.Coalgebra.Parser
import Copar.RefinementInterface
import Copar.MinimizationInterface
import GHC.Float (integerLogBase)
import Text.Printf
-- | Minimizes the given coalgebra by merging equivalent states.
minimize :: forall f. (Foldable f, Functor f, MinimizationInterface f)
=> FunctorExpression f Sort
-> Encoding (Label (Desorted f)) (F1 (Desorted f))
-> SymbolTable
-> Partition
-> (Encoding (Label (Desorted f)) (F1 (Desorted f)), SymbolTable)
minimize f encoding symbolTable part =
( minimizeEncoding f encoding part
, minimizeSymbolTable symbolTable (toBlocks part)
)
-- | Minimizes the given encoding based on the given `Partition` by merging labels using
-- the `MinimizationInterface` of `f`.
minimizeEncoding :: forall f. (Foldable f, Functor f, MinimizationInterface f)
=> FunctorExpression f Sort
-> Encoding (Label (Desorted f)) (F1 (Desorted f))
-> Partition
-> Encoding (Label (Desorted f)) (F1 (Desorted f))
minimizeEncoding f encoding part =
Encoding.new
-- States are only in the same block if they have the same F1, so
-- we can just use the F1 of the first state of each block here.
(V.fromList $ map getF1 (toBlocks part))
-- Merge edges with the same origin and target using `f`s `MinimizationInterface`.
((combineEdges encoding (sortTable f) part) . V.toList $ edges encoding)
where
getF1 (v:_) = structure encoding V.! v
getF1 _ = undefined -- This is unreachable, there are no empty blocks.
combineEdges :: forall f. (MinimizationInterface f)
=> Encoding (Label (Desorted f)) (F1 (Desorted f))
-> V.Vector (f ())
-> Partition
-> [Edge (Label (Desorted f))]
-> V.Vector (Edge (Label (Desorted f)))
combineEdges encoding sorts part edges =
-- All relevant groups of edges which we have to `merge`.
let groupedEdges =
NonEmpty.groupBy (\a b -> from a == from b && to a == to b) $
sortEdges (mapMaybe (updateEdge part) edges)
in V.fromList . List.concat $ map mergeEdges groupedEdges
where
-- The functor sort of the given state.
--
-- As we have already updated the states here, we have to first look
-- at the original `state` which is the first state of the relevant block.
partitionSort state = fromEnum (sortedSort $ typeOf encoding (head $ statesOfBlock part (Block state))) - 1
mergeEdges :: NonEmpty (Edge (Label (Desorted f))) -> [Edge (Label (Desorted f))]
mergeEdges (e:|ll) = map
-- Edges in a group only differ in their `Label`, so we can reuse the first edge
-- to rebuild after unwrapping the `label` of each element.
(\v -> Edge (from e) (mapDesortedLabel @f @f (const v) $ label e) (to e))
(merge (sorts V.! (partitionSort $ from e)) (NonEmpty.map (desortedLabel @f . label) (e:|ll)))
sortEdges :: [Edge lbl] -> [Edge lbl]
sortEdges = List.sortBy (\a b -> compare (from a, to a) (from b, to b))
-- | Removes all edges which are not at the front of a block and updates `from` and `to` for the
-- remaining ones.
updateEdge :: Partition -> Edge f -> Maybe (Edge f)
updateEdge part e =
let block = blockOfState part $ from e
in if head (statesOfBlock part block) == from e then
Just (Edge (fromBlock block) (label e) (fromBlock (blockOfState part $ to e))) else Nothing
-- | Merges the symbols of all states in a given block.
--
-- We try quite hard to keep all of this deterministic, so we sort both the names of all states
-- in a block as well as padding the block numbers with zero so that the block number `09` remains in front of `10`.
minimizeSymbolTable :: SymbolTable -> [[State]] -> SymbolTable
minimizeSymbolTable symbols part =
SymbolTable { fromSymbolTable = HM.fromList partitions }
where
partitions = map (\(v, (i, n)) -> (i, T.pack (printf "s%0*d" ((+1) . (integerLogBase 10) . toInteger $ length blocks) v) <> "_" <> n))
$ zip [(0 :: Int)..] blocks
blocks = (filter ((/=mempty) . snd) (List.sortOn snd (zip [0..] (map nameBlock part))))
nameBlock block = sepFold "_" id (List.sort (mapMaybe (flip HM.lookup (fromSymbolTable symbols)) block))
......@@ -28,9 +28,9 @@ module Data.Partition
import Data.Foldable (toList)
import Control.Monad (forM_)
import Control.Monad.ST (runST)
import Control.DeepSeq
import qualified Data.HashMap.Strict as M
import qualified Data.Set as S
import Data.Vector (Vector)
import qualified Data.Vector as V
......@@ -110,12 +110,12 @@ fromBlocks states = -- TODO Check validity of input
-- | Return the partition as list of blocks, where each block is represented by
-- its elements.
toBlocks :: Partition -> [[State]]
toBlocks :: Partition -> [[State]] -- TODO directly return a Vector here instead
toBlocks p =
let
blockMap = V.ifoldr' (\s (Block b) m -> M.insertWith (++) b [s] m) M.empty (stateAssignment p)
in
M.elems blockMap
map reverse $ V.toList (runST $ do
blocks <- VM.replicate (numBlocks p) []
V.imapM_ (\st block -> VM.modify blocks (st:) (fromBlock block)) (stateAssignment p)
V.freeze blocks)
-- | The block that the given state is in.
blockOfState :: Partition -> State -> Block
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment