Commit b2b6e982 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

first running version with new CExp AST

parent 4a2a5c34
......@@ -20,7 +20,7 @@ main = do
usage = "<file>"
ec :: Program -> IO (Maybe (Result (CExp Rational)))
ec p = runAny (ect (fst (gen p)) (0 :: CExp Rational))
ec p = runAny (ect (fst (gen p)) (zero :: CExp Rational))
......
......@@ -141,7 +141,7 @@ cmp _ _ = yellow
run1 :: (?to :: Int) => Problem -> IO Outcome
run1 (Problem pid p) = do
start <- getCurrentTime
let exe = InferEt.runAny . flip InferEt.ect (0 :: CExp Rational) . fst $ gen p
let exe = InferEt.runAny . flip InferEt.ect zero . fst $ gen p
rM <- timeout ?to exe
let stM = case rM of
Nothing -> Timeout
......@@ -216,56 +216,33 @@ printBenchmarkTex (Benchmark _ ps) =
, "\\\\"]
texStatus Timeout = "timeout"
texStatus Failed = "?"
texStatus (Success c _) = texMax c
texStatus (Success c _) = texCExp c
escaped [] = []
escaped ('_':xs) = '\\' : '_' : escaped xs
escaped (x:xs) = x : escaped xs
math s = "$" <> s <> "$"
parens t = "(" <> t <> ")"
braces t = "{" <> t <> "}"
a <+> b = a <> " " <> b
mulf = "\\mulf"
addf = "\\plusf"
divf = "\\divf"
-- parens t = "(" <> t <> ")"
-- braces t = "{" <> t <> "}"
-- a <+> b = a <> " " <> b
-- mulf = "\\mulf"
-- addf = "\\plusf"
-- divf = "\\divf"
texInt i = "\\bm" <> braces (show i)
texFrac q
| denominator q == 1 = texInt (numerator q)
| otherwise = braces (texInt (numerator q)) <> divf <> braces (texInt (denominator q))
-- texInt i = "\\bm" <> braces (show i)
-- texFrac q
-- | denominator q == 1 = texInt (numerator q)
-- | otherwise = braces (texInt (numerator q)) <> divf <> braces (texInt (denominator q))
-- BExp
texDisj (Disj (S.toList -> ds)) = intercalate " \\vee " (map texConj ds)
texConj (Conj (S.toList -> es)) = intercalate " \\wedge " (map texLit es)
texLit (e1 :>=: e2) = texExp e1 <+> "\\ge" <+> texExp e2
texExp = show . PP.pretty
-- CExp
texMax :: CExp Rational -> String
texMax (Max []) = "\\zerof"
texMax (Max [gs]) = texGS gs
texMax (Max gs) = "\\maxf" <> parens (intercalate ", " (map texGS gs))
texGS (GS (M.toList -> ms)) = intercalate " \\plusf " (map texNPF ms)
texNPF (b, p1 :% p2)
| p2 == 1 = "\\bracf" <> braces (texDisj b) <+> mulf <+> parens (texNP p1)
| otherwise = "\\bracf" <> braces (texDisj b) <+> mulf <+> (parens (texNP p1) <> divf <> texNP p2)
texNP :: NormPoly Rational -> String
texNP = texPoly texNorm texFrac
texNorm (Norm e) = "\\normf" <> braces (texExp e)
-- Poly
texPoly tv tc e = texMonos (P.toMonos e) where
texMonos [] = "\\zerof"
texMonos ms = intercalate " \\plusf " $ map texMono ms
texMono (c,m)
| c == 1 = concatMap texPower (P.toPowers m)
| otherwise = tc c <+> mulf <+> concatMap texPower (P.toPowers m)
texPower (v,d)
| d == 1 = tv v
| d > 1 = tv v <> "^" <> show d
| otherwise = ""
-- texDisj (Disj (S.toList -> ds)) = intercalate " \\vee " (map texConj ds)
-- texConj (Conj (S.toList -> es)) = intercalate " \\wedge " (map texLit es)
-- texLit (e1 :>=: e2) = texExp e1 <+> "\\ge" <+> texExp e2
-- texExp :: Exp -> String
-- texExp = show . PP.pretty
texCExp = show . PP.pretty
printBenchmarkMd :: (?to :: Int) => Benchmark -> IO ()
......
......@@ -25,7 +25,7 @@ library
transformers,
mtl,
ansi-wl-pprint,
megaparsec >= 7.0,
megaparsec,
parser-combinators >= 1.0,
uniplate,
list-t,
......@@ -44,7 +44,6 @@ library
PWhile.InferEt
PWhile.SampleEt
PWhile.Testbed.Examples
PWhile.Testbed.Development
PWhile.Testbed.Absynth.Polynomial
PWhile.Testbed.DSL
PWhile.Util
......@@ -53,6 +52,7 @@ library
DeriveDataTypeable
FlexibleInstances
FlexibleContexts
TypeSynonymInstances
GeneralizedNewtypeDeriving
OverloadedStrings
default-language: Haskell2010
......
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
{-# LANGUAGE PatternSynonyms #-}
module Data.PWhile.BoolExpression
(
Conj (..)
, lits, conjs
, lits, conjs, variables
, Literal (..)
, DNF (..)
, BLit
......@@ -33,7 +29,8 @@ import qualified Data.Set as S
import qualified Data.Set.Internal as SI
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.PWhile.Expression
import Data.PWhile.Expression hiding (variables)
import qualified Data.PWhile.Expression as E
data Literal p q = p :>=: q
deriving (Eq, Ord, Read, Show, Data)
......@@ -136,6 +133,8 @@ instance Substitutable BExp where
| e1 :>=: e2 <- S.toList cs ]
| Conj cs <- conjs b]
variables :: BExp -> S.Set Var
variables g = S.unions [ E.variables a `S.union` E.variables b | (a :>=: b) <- S.toList (literals g)]
-- pretty
----------------------------------------------------------------------
......
This diff is collapsed.
{-# LANGUAGE DeriveTraversable #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
{-# LANGUAGE StandaloneDeriving, ViewPatterns, PatternSynonyms, DeriveDataTypeable, OverloadedStrings, CPP #-}
{-# LANGUAGE FlexibleInstances, StandaloneDeriving, ViewPatterns, PatternSynonyms, OverloadedStrings, DeriveDataTypeable #-}
module Data.PWhile.Expression
(
-- expressions
Var (..)
, Expression
, Exp
, Lam (..)
, pattern Constant
, pattern AddConst
, variable
......@@ -20,78 +19,74 @@ module Data.PWhile.Expression
, prettyFrac
)
where
import qualified Data.Set as S
import Data.Data
import Data.String
import qualified GUBS.Polynomial as P
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.Data
import qualified Data.Map as M
import Data.Ratio
import Data.String
newtype Var = Var String
deriving (Eq, Ord, Read, Show, Data)
-- Variables
----------------------------------------------------------------------
data Var
= Named String
-- TODO: remove
| Ix Int
deriving (Data, Eq, Ord, Show, Read)
-- Expressions
----------------------------------------------------------------------
type Expression c = P.Polynomial Var c
type Exp = Expression Int
type Exp = P.Polynomial Var Int
instance Num c => IsString (Expression c) where
fromString = P.variable . Var
instance IsString Exp where
fromString = P.variable . Named
class Substitutable a where
substitute :: Var -> Exp -> a -> a
constant :: (Eq c, Num c) => c -> Expression c
constant = P.coefficient
instance Substitutable Exp where
substitute v e = P.substitute s where
s v' | v == v' = e
| otherwise = P.variable v'
variable :: Num c => Var -> Expression c
variable = P.variable
variables :: Expression c -> S.Set Var
variables = S.fromList . P.variables
constant :: Int -> Exp
constant = P.coefficient
const_ :: (Eq c, Ord v, Num c) => P.Polynomial v c -> Maybe c
-- patterns
const_ :: (Ord v, Eq c, Num c) => P.Polynomial v c -> Maybe c
const_ (P.norm -> e)
| null (P.variables e) = Just $ sum $ P.coefficients e
| otherwise = Nothing
pattern Constant :: (Eq c, Ord v, Num c) => c -> P.Polynomial v c
pattern Constant :: (Ord v, Eq c, Num c) => c -> P.Polynomial v c
pattern Constant i <- (const_ -> Just i)
addConst_ :: (Eq c, Num c, Ord v) => P.Polynomial v c -> (P.Polynomial v c,c)
addConst_ :: (Ord v, Eq c, Num c) => P.Polynomial v c -> (P.Polynomial v c,c)
addConst_ e = (e - P.coefficient c, c)
where c = P.coefficientOf (P.fromPowers []) e
pattern AddConst :: (Ord v, Eq c, Num c) => P.Polynomial v c -> c -> P.Polynomial v c
pattern AddConst e i <- (addConst_ -> (e,i))
variable :: Var -> Exp
variable = P.variable
variables :: Exp -> [Var]
variables = P.variables
-- substitutions
----------------------------------------------------------------------
class Substitutable a where
substitute :: Var -> Exp -> a -> a
instance (Eq c, Num c) => Substitutable (Expression c) where
substitute v e = P.substitute s where
s v' | v == v' = e'
| otherwise = P.variable v'
e' = fromIntegral `fmap` e
-- distributions
----------------------------------------------------------------------
deriving instance Read (P.Monomial Var)
deriving instance Read Exp
deriving instance (Read v, Ord v) => Read (P.Monomial v)
deriving instance (Read c, Read v, Ord v) => Read (P.Polynomial v c)
deriving instance Data (P.Monomial Var)
deriving instance Data Exp
-- deriving instance (Read c) => Read (NormPoly c)
newtype Lam = Lam Exp deriving (Data, Eq, Ord, Read, Show)
data Dist e
= Discrete [(Exp,e)]
| Rand e
| Rand e -- TODO => Uniform
deriving (Data, Eq, Read, Ord, Show)
discrete :: [(Exp,e)] -> Dist e
......@@ -113,8 +108,7 @@ bernoulli (a,b) e1 e2 = Discrete [(a, e1), (b, e2)]
----------------------------------------------------------------------
instance PP.Pretty Var where
pretty (Named s) = PP.text s
pretty (Ix i) = PP.underline (PP.int i)
pretty (Var v) = PP.text v
prettyFrac :: (Exp,Exp) -> PP.Doc
prettyFrac (n,d)
......
......@@ -8,13 +8,13 @@ module Data.PWhile.Program
)
where
import Data.Data
import qualified Data.Set as Set
import Data.Data
import qualified Data.Set as S
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.PWhile.Expression hiding (variables)
import Data.PWhile.Expression hiding (variables)
import qualified Data.PWhile.Expression as E
import Data.PWhile.BoolExpression
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.PWhile.BoolExpression hiding (variables)
type Label = Int
type Invariant = BExp
......@@ -24,7 +24,7 @@ data C where
Abort :: C
Skip :: C
Tic :: Exp -> C
Ass :: String -> Dist Exp -> C
Ass :: Var -> Dist Exp -> C
-- comp
NonDet :: C -> C -> C
Choice :: [(Exp,C)] -> C
......@@ -42,10 +42,10 @@ instance Monoid C where
mempty = Skip
instance PP.Pretty C where
pretty Abort = PP.text "Abort"
pretty Skip = PP.text "Skip"
pretty (Tic e) = PP.text "Tick" PP.<> PP.parens (PP.pretty e)
pretty (Ass v d) = PP.text v PP.<+> PP.text ":~" PP.<+> PP.align (PP.pretty d)
pretty Abort = PP.text "Abort"
pretty Skip = PP.text "Skip"
pretty (Tic e) = PP.text "Tick" PP.<> PP.parens (PP.pretty e)
pretty (Ass (Var v) d) = PP.text v PP.<+> PP.text ":~" PP.<+> PP.align (PP.pretty d)
pretty (NonDet c1 c2) =
PP.text "NonDet"
......@@ -69,17 +69,15 @@ instance PP.Pretty C where
pretty (Seq c1 c2) = PP.pretty c1 PP.<$> PP.pretty c2
subPrograms :: C -> [C]
subPrograms c@(NonDet c1 c2) = c : (subPrograms c1 ++ subPrograms c2)
subPrograms c@(Choice cs) = c : concatMap (subPrograms . snd) cs
subPrograms c@(NonDet c1 c2) = c : (subPrograms c1 ++ subPrograms c2)
subPrograms c@(Choice cs) = c : concatMap (subPrograms . snd) cs
subPrograms c@(Cond _ _ _ c1 c2) = c : (subPrograms c1 ++ subPrograms c2)
subPrograms c@(While _ _ _ c1) = c : (subPrograms c1)
subPrograms c@(Seq c1 c2) = c : (subPrograms c1 ++ subPrograms c2)
subPrograms c = [c]
subPrograms c@(While _ _ _ c1) = c : subPrograms c1
subPrograms c@(Seq c1 c2) = c : (subPrograms c1 ++ subPrograms c2)
subPrograms c = [c]
variables :: C -> Set.Set Var
-- TODO
variables c = Set.unions [ Set.fromList (Named n : distVars d)
| Ass n d <- subPrograms c]
variables :: C -> S.Set Var
variables c = S.unions [ S.insert n (distVars d) | Ass n d <- subPrograms c]
where
distVars (Discrete cs) = concat [E.variables f ++ E.variables e | (f,e) <- cs]
distVars (Discrete cs) = S.unions [E.variables f `S.union` E.variables e | (f,e) <- cs]
distVars (Rand e) = E.variables e
......@@ -41,14 +41,14 @@ import PWhile.Util
--- * Solver Monad ---------------------------------------------------------------------------------------------------
type CostExpression = C.CExp Rational
type CExp = C.CExp Rational
type MemoT = St.StateT (M.Map (Knd,C,CostExpression) CostExpression)
type MemoT = St.StateT (M.Map (Knd,C,CExp) CExp)
runMemoT :: Monad m => MemoT m v -> m v
runMemoT = flip St.evalStateT M.empty
memoized :: (Knd -> C -> CostExpression -> SolveM CostExpression) -> Knd -> C -> CostExpression -> SolveM CostExpression
memoized :: (Knd -> C -> CExp -> SolveM CExp) -> Knd -> C -> CExp -> SolveM CExp
memoized f k c e = do
memo <- liftMemoT St.get
case M.lookup (k,c,e) memo of
......@@ -156,24 +156,28 @@ runAny m = listToMaybe <$> run Any m
-- estimating expectations
----------------------------------------------------------------------
discreteExpectation :: [(E.Exp, e)] -> (e -> SolveM CostExpression) -> SolveM CostExpression
rankFromCExp :: C.CExp c -> [C.GExp c]
rankFromCExp = filter (not . isConst) . C.gExps
where isConst (C.GExp _ e) = null (E.variables e)
discreteExpectation :: [(E.Exp, e)] -> (e -> SolveM CExp) -> SolveM CExp
discreteExpectation ls f =
C.divBy <$> (sum <$> sequence [scale w <$> f e | (w,e) <- ls])
<*> pure (sum (fst `map` ls))
where
scale (E.Constant r) a = fromIntegral r * a
scale e a = C.fromPowers [(C.norm e, 1)] * a
boundedSum :: (E.Exp -> CostExpression) -> (E.Exp, E.Exp) -> SolveM CostExpression
boundedSum f (l,o) =
case f vi of
C.Max [] -> return 0
C.Max [C.GS s] -> sum <$> sequence [ bs (C.guarded b (C.toCost e)) | (b,e) <- M.toList s ]
fi -> bs fi
where
i = E.Named "@i"
C.divBy <$> (C.sum <$> sequence [C.scale w <$> f e | (w,e) <- ls'])
<*> pure (sum [e | (e,_) <- ls'])
where ls' = [ (fmap fromIntegral w, e) | (w,e) <- ls ]
boundedSum :: (E.Exp -> CExp) -> (E.Exp, E.Exp) -> SolveM CExp
boundedSum f (l,o) = logBlkIdM msg $ bs fi where
i = E.Var "@i"
vi = E.variable i
bs fi = logBlkIdM ("[sum] " ++ renderPretty (PP.text "sum" PP.<> PP.tupled [ PP.pretty l, PP.pretty o, PP.pretty fi])) $ do
fi = f vi
msg = "[sum] " ++ renderPretty (PP.text "sum" PP.<> PP.tupled [ PP.pretty l, PP.pretty o, PP.pretty fi])
bs g | g == C.zero = return C.zero
bs (C.Plus g1 g2) = C.plus <$> bs g1 <*> bs g2
bs g = do
logMsg2 "norms" ns
(ui,s,dir) <- alternative [(uiDown, o, "Down"), (uiUp, l, "Up")]
logMsg2 ("SumFn["++dir++"]") ui
......@@ -181,272 +185,213 @@ boundedSum f (l,o) =
logMsg2 "Solution" f'
return (E.substitute i s f')
where
uiDown = UpperInvariant { inv = o .>= vi
, cond = vi .>= l
, cost = fi
, step = (C.toCost . E.substitute i (vi - 1)) `map` ns
, cont = 0
, limt = ns }
uiUp = UpperInvariant { inv = vi .>= l
, cond = o .>= vi
, cost = fi
, step = (C.toCost . E.substitute i (vi + 1)) `map` ns
, cont = 0
, limt = ns }
ns = fromCExp fi
-- ns = ni : ns' ++ [ni * n' | n' <- ns']
where
-- ns' = fromCExp fi
-- ni = C.fromNorm (C.norm (vi + 1))
fromCExp (C.Max as) = concatMap fromGS as
fromGS (C.GS s) = concat
[ [ng * ne] | (g,p) <- M.toList s
, ng <- fromBExp g -- .&& vi .>= l .&& o .>= vi
, ne <- fromFrac p]
-- fromBExp Top = [ 1, C.fromNorm (P.variable (E.Named "@i") `C.diff` 0) ]
fromBExp bexp = [ C.fromNorm ((b - 1) `C.diff` a)
| (a :>=: b) <- S.toList (literals bexp)]
fromFrac (n C.:% _) = [ P.fromMono m | (_,m) <- P.toMonos n] -- C.fromNorm `map` P.variables n
expectation :: E.Dist E.Exp -> (E.Exp -> CostExpression) -> SolveM CostExpression
uiDown = UpperInvariant {
inv = o .>= vi
, cnd = vi .>= l
, cost = g
, step = (E.substitute i (vi - 1) . C.fromGExp) `map` ns
, cont = C.zero
, limt = ns }
uiUp = UpperInvariant {
inv = vi .>= l
, cnd = o .>= vi
, cost = g
, step = (E.substitute i (vi + 1) . C.fromGExp) `map` ns
, cont = C.zero
, limt = ns }
ns = rankFromCExp g
-- where
-- fromCExp (C.E e) = fromExp e
-- fromCExp (C.Div f _) = fromCExp f
-- fromCExp (C.Plus f1 f2) = fromCExp f1 `S.union` fromCExp f2
-- fromCExp (C.Sup f1 f2) = fromCExp f1 `S.union` fromCExp f2
-- fromCExp (C.Cond g f1 f2) = S.fromList
-- [ ng `C.mulG` n1 | ng <- 1 : S.toList (fromBExp g)
-- , n1 <- S.toList (fromCExp f1)]
-- ++ [ ng `C.mulG` n2 | ng <- 1 : S.toList (fromBExp (neg g))
-- , n2 <- S.toList (fromCExp f2)]
-- fromBExp bexp = S.fromList [ C.norm (b - a - 1)
-- | (a :>=: b) <- S.toList (literals bexp)]
-- fromExp e = S.fromList [ P.fromMono m
-- | (_,m) <- P.toMonos e ]
expectation :: E.Dist E.Exp -> (E.Exp -> CExp) -> SolveM CExp
expectation (E.Discrete ls) f = discreteExpectation ls (return . f)
-- expectation (E.Rand (E.Constant n)) f =
-- discreteExpectation [(1,E.constant i) | i <- [0..n-1]] (return . f)
expectation (E.Rand n) f =
logBlkIdM ("[expectation] " ++ "rand(" ++ show (PP.pretty n) ++ ")") $ do
let (vi,vj) = (E.Named "@i", E.Named "@j")
let (vi,vj) = (E.Var "@i", E.Var "@j")
(fi,fj) = (f (E.variable vi), f (E.variable vj))
logMsg2 "f" fi
C.guarded (n .> 0) <$>
case n of
_ | fi == fj -> return fi
| Just g <- linFn fi vi (C.scale (1 / 2) (C.fromExp n)) -> return g
-- TODO!
-- | Just g <- linFn fi vi (C.scale (1 / 2) (C.E n)) -> return g
E.Constant n' -> discreteExpectation [(1,E.constant i) | i <- [0..n'-1]] (return . f)
_ | otherwise -> C.divBy <$> boundedSum f (0,n-1) <*> pure n
_ | otherwise -> C.divBy <$> boundedSum f (0,n-1) <*> pure (fmap fromIntegral n)
where
noccur v (C.Norm e) = v `notElem` E.variables e
linFn :: CostExpression -> E.Var -> CostExpression -> Maybe (CostExpression)
linFn (C.guardedExpressions -> [(Top,p C.:% q)]) v avg
| not (v `S.member` C.variables (C.toCost q)) =
(*) <$> (sum <$> sequence [linMono m v avg | m <- P.toMonos p ])
<*> pure (C.toCost (1 C.:% q))
linFn _ _ _ = Nothing
linMono (coeff,P.toPowers -> powers) v avg = C.scale coeff <$> lin powers where
lin [] = return 1
lin (p:ps)
| v `noccur` fst p = (*) (C.fromPowers [p]) <$> lin ps
lin ((C.Norm e,1):ps) = (*) <$> linExp e v avg <*> con ps
lin _ = Nothing
con [] = return 1
con (p:ps)
| v `noccur` fst p = (*) (C.fromPowers [p]) <$> con ps
con _ = Nothing
linExp :: E.Exp -> E.Var -> CostExpression -> Maybe (CostExpression)
linExp e v avg
| c >= 0 && d >= 0
&& E.constant c * E.variable v + E.constant d == e =
Just (C.scale (toRational c) avg + C.constant (toRational d))
| otherwise = Nothing
where
c = P.coefficientOf (P.fromPowers [(v,1)]) e
d = P.coefficientOf (P.fromPowers []) e
noccur v e = v `notElem` E.variables e
-- TODO: add linFn
-- linFn :: CExp -> E.Var -> CExp -> Maybe (CExp)
-- linFn (C.guardedExpressions -> [(Top,p C.:% q)]) v avg
-- | not (v `S.member` C.variables (C.toCost q)) =
-- (*) <$> (sum <$> sequence [linMono m v avg | m <- P.toMonos p ])
-- <*> pure (C.toCost (1 C.:% q))
-- linFn _ _ _ = Nothing
-- linMono (coeff,P.toPowers -> powers) v avg = C.scale coeff <$> lin powers where
-- lin [] = return 1
-- lin (p:ps)
-- | v `noccur` fst p = (*) (C.fromPowers [p]) <$> lin ps
-- lin ((C.Norm e,1):ps) = (*) <$> linExp e v avg <*> con ps
-- lin _ = Nothing
-- con [] = return 1
-- con (p:ps)
-- | v `noccur` fst p = (*) (C.fromPowers [p]) <$> con ps
-- con _ = Nothing
-- linExp :: E.Exp -> E.Var -> CExp -> Maybe (CExp)
-- linExp e v avg
-- | c >= 0 && d >= 0
-- && E.constant c * E.variable v + E.constant d == e =
-- Just (C.scale (toRational c) avg + C.constant (toRational d))
-- | otherwise = Nothing
-- where
-- c = P.coefficientOf (P.fromPowers [(v,1)]) e
-- d = P.coefficientOf (P.fromPowers []) e
-- Expectation Transformer
----------------------------------------------------------------------
extractRanking :: C -> BExp -> BExp -> CostExpression -> CostExpression -> SolveM [P.Monomial C.Norm]
extractRanking body i cnd g f = do
extractRanking :: C -> BExp -> BExp -> CExp -> CExp -> SolveM [C.GExp Rational]
extractRanking body i c g f = do
combine <-
(logMsg "additive" >> pure additive)
<|> (logMsg "multiplicative" >> pure multiplicative)
-- <|> (logMsg "quadratic" >> pure quadratic)
rankFromBExp <-
(logMsg "optimistic" >> pure (rankFromBExpWith optimistic))
<|> (logMsg "shift" >> pure (rankFromBExpWith shift))
-- <|> (logMsg "relaxed" >> pure (rankFromBExpWith relaxed))
<|> (logMsg "squared-optimistic" >> pure (squared (rankFromBExpWith optimistic)))
-- <|> (logMsg "relaxed-diff" >> pure (S.union diffs . normsFromBExpWith relaxed))
gRank <- combine <$> sequence [ (,) <$> rankFromBExp (i .&& cnd .&& b) <*> pure (rankFromExp e)
| (b,e) <- C.guardedExpressions g]
fRank <-