module Theory.Constraint.Solver.Simplify (
simplifySystem
) where
import Debug.Trace
import Prelude hiding (id, (.))
import qualified Data.DAG.Simple as D
import Data.Data
import Data.Either (partitionEithers)
import qualified Data.Foldable as F
import Data.List
import qualified Data.Map as M
import Data.Monoid (Monoid(..))
import qualified Data.Set as S
import Control.Basics
import Control.Category
import Control.Monad.Disj
import Control.Monad.Fresh
import Control.Monad.Reader
import Control.Monad.State (gets)
import Extension.Data.Label
import Extension.Prelude
import Theory.Constraint.Solver.Goals
import Theory.Constraint.Solver.Reduction
import Theory.Constraint.Solver.Types
import Theory.Constraint.System
import Theory.Model
import Theory.Text.Pretty
simplifySystem :: Reduction ()
simplifySystem = do
go (0 :: Int) [Changed]
exploitUniqueMsgOrder
removeSolvedSplitGoals
where
go n changes0
| Unchanged == mconcat changes0 = return ()
| otherwise = do
se0 <- gets id
void substSystem
(c1,c2,c3) <- enforceNodeUniqueness
c4 <- enforceEdgeUniqueness
c5 <- solveUniqueActions
c6 <- reduceFormulas
c7 <- evalFormulaAtoms
c8 <- insertImpliedFormulas
let changes = filter ((Changed ==) . snd) $
[ ("unique fresh instances (DG4)", c1)
, ("unique K↓-facts (N5↓)", c2)
, ("unique K↑-facts (N5↑)", c3)
, ("unique (linear) edges (DG2 and DG3)", c4)
, ("solve unambiguous actions (S_@)", c5)
, ("decompose trace formula", c6)
, ("propagate atom valuation to formula", c7)
, ("saturate under ∀-clauses (S_∀)", c8)
]
traceIfLooping
| n <= 10 = id
| otherwise = trace $ render $ vsep
[ text "Simplifier iteration" <-> int n <> colon
, fsep $ text "The reduction-rules for" :
(punctuate comma $ map (text . fst) changes) ++
[text "were applied to the following constraint system."]
, nest 2 (prettySystem se0)
]
traceIfLooping $ go (n + 1) (map snd changes)
exploitUniqueMsgOrder :: Reduction ()
exploitUniqueMsgOrder = do
kdConcs <- gets (M.fromList . map (\(i, _, m) -> (m, i)) . allKDConcs)
kuActions <- gets (M.fromList . map (\(i, _, m) -> (m, i)) . allKUActions)
F.mapM_ (uncurry insertLess) $ M.intersectionWith (,) kdConcs kuActions
enforceNodeUniqueness :: Reduction (ChangeIndicator, ChangeIndicator, ChangeIndicator)
enforceNodeUniqueness =
(,,)
<$> (merge (const $ return Unchanged) freshRuleInsts)
<*> (merge (solveRuleEqs SplitNow) kdConcs)
<*> (merge (solveFactEqs SplitNow) kuActions)
where
freshRuleInsts se = do
(i, ru) <- M.toList $ get sNodes se
guard (isFreshRule ru)
return (ru, ((), i))
kdConcs sys = (\(i, ru, m) -> (m, (ru, i))) <$> allKDConcs sys
kuActions se = (\(i, fa, m) -> (m, (fa, i))) <$> allKUActions se
merge :: Ord b
=> ([Equal a] -> Reduction ChangeIndicator)
-> (System -> [(b,(a,NodeId))])
-> Reduction ChangeIndicator
merge solver candidates = do
changes <- gets (map mergers . groupSortOn fst . candidates)
mconcat <$> sequence changes
where
mergers [] = unreachable "enforceUniqueness"
mergers ((_,(xKeep, iKeep)):remove) =
mappend <$> solver (map (Equal xKeep . fst . snd) remove)
<*> solveNodeIdEqs (map (Equal iKeep . snd . snd) remove)
enforceEdgeUniqueness :: Reduction ChangeIndicator
enforceEdgeUniqueness = do
se <- gets id
let edges = S.toList (get sEdges se)
(<>) <$> mergeNodes eSrc eTgt edges
<*> mergeNodes eTgt eSrc (filter (proveLinearConc se . eSrc) edges)
where
proveLinearConc se (v, i) =
maybe False (isLinearFact . (get (rConc i))) $
M.lookup v $ get sNodes se
mergeNodes mergeEnd compareEnd edges
| null eqs = return Unchanged
| otherwise = do
contradictoryIf (not $ and [snd l == snd r | Equal l r <- eqs])
solveNodeIdEqs $ map (fmap fst) eqs
where
eqs = concatMap (merge mergeEnd) $ groupSortOn compareEnd edges
merge _ [] = error "exploitEdgeProps: impossible"
merge proj (keep:remove) = map (Equal (proj keep) . proj) remove
solveUniqueActions :: Reduction ChangeIndicator
solveUniqueActions = do
rules <- nonSilentRules <$> askM pcRules
actionAtoms <- gets unsolvedActionAtoms
let uniqueActions = [ x | [x] <- group (sort ruleActions) ]
ruleActions = [ (tag, length ts)
| ru <- rules, Fact tag ts <- get rActs ru ]
isUnique (Fact tag ts) =
(tag, length ts) `elem` uniqueActions
&& null [ () | t <- ts, FUnion _ <- return (viewTerm2 t) ]
trySolve (i, fa)
| isUnique fa = solveGoal (ActionG i fa) >> return Changed
| otherwise = return Unchanged
mconcat <$> mapM trySolve actionAtoms
reduceFormulas :: Reduction ChangeIndicator
reduceFormulas = do
formulas <- getM sFormulas
applyChangeList $ do
fm <- S.toList formulas
guard (reducibleFormula fm)
return $ do modM sFormulas $ S.delete fm
insertFormula fm
evalFormulaAtoms :: Reduction ChangeIndicator
evalFormulaAtoms = do
ctxt <- ask
valuation <- gets (partialAtomValuation ctxt)
formulas <- getM sFormulas
applyChangeList $ do
fm <- S.toList formulas
case simplifyGuarded valuation fm of
Just fm' -> return $ do
case fm of
GDisj disj -> markGoalAsSolved "simplified" (DisjG disj)
_ -> return ()
modM sFormulas $ S.delete fm
modM sSolvedFormulas $ S.insert fm
insertFormula fm'
Nothing -> []
partialAtomValuation :: ProofContext -> System -> LNAtom -> Maybe Bool
partialAtomValuation ctxt sys =
eval
where
runMaude = (`runReader` get pcMaudeHandle ctxt)
before = alwaysBefore sys
lessRel = rawLessRel sys
nodesAfter = \i -> filter (i /=) $ S.toList $ D.reachableSet [i] lessRel
nonUnifiableNodes :: NodeId -> NodeId -> Bool
nonUnifiableNodes i j = maybe False (not . runMaude) $
(unifiableRuleACInsts) <$> M.lookup i (get sNodes sys)
<*> M.lookup j (get sNodes sys)
eval ato = case ato of
Action (ltermNodeId' -> i) fa
| ActionG i fa `M.member` get sGoals sys -> Just True
| otherwise ->
case M.lookup i (get sNodes sys) of
Just ru
| any (fa ==) (get rActs ru) -> Just True
| all (not . runMaude . unifiableLNFacts fa) (get rActs ru) -> Just False
_ -> Nothing
Less (ltermNodeId' -> i) (ltermNodeId' -> j)
| i == j || j `before` i -> Just False
| i `before` j -> Just True
| isLast sys i && isInTrace sys j -> Just False
| isLast sys j && isInTrace sys i &&
nonUnifiableNodes i j -> Just True
| otherwise -> Nothing
EqE x y
| x == y -> Just True
| not (runMaude (unifiableLNTerms x y)) -> Just False
| otherwise ->
case (,) <$> ltermNodeId x <*> ltermNodeId y of
Just (i, j)
| i `before` j || j `before` i -> Just False
| nonUnifiableNodes i j -> Just False
_ -> Nothing
Last (ltermNodeId' -> i)
| isLast sys i -> Just True
| any (isInTrace sys) (nodesAfter i) -> Just False
| otherwise ->
case get sLastAtom sys of
Just j | nonUnifiableNodes i j -> Just False
_ -> Nothing
insertImpliedFormulas :: Reduction ChangeIndicator
insertImpliedFormulas = do
sys <- gets id
hnd <- getMaudeHandle
applyChangeList $ do
clause <- (S.toList $ get sFormulas sys) ++
(S.toList $ get sLemmas sys)
implied <- impliedFormulas hnd sys clause
if ( implied `S.notMember` get sFormulas sys &&
implied `S.notMember` get sSolvedFormulas sys )
then return (insertFormula implied)
else []
impliedFormulas :: MaudeHandle -> System -> LNGuarded -> [LNGuarded]
impliedFormulas hnd sys gf0 =
case openGuarded gf `evalFresh` avoid gf of
Just (All, _vs, antecedent, succedent) -> do
let (actionsEqs, otherAtoms) = first sortGAtoms . partitionEithers $
map prepare antecedent
succedent' = gall [] otherAtoms succedent
subst <- candidateSubsts emptySubst actionsEqs
return $ unskolemizeLNGuarded $ applySkGuarded subst succedent'
_ -> []
where
gf = skolemizeGuarded gf0
prepare (Action i fa) = Left (GAction (i,fa))
prepare (EqE s t) = Left (GEqE (s,t))
prepare ato = Right (fmap (fmapTerm (fmap Free)) ato)
sysActions = do (i, fa) <- allActions sys
return (skolemizeTerm (varTerm i), skolemizeFact fa)
candidateSubsts subst [] = return subst
candidateSubsts subst ((GAction a):as) = do
sysAct <- sysActions
subst' <- (`runReader` hnd) $ matchAction sysAct (applySkAction subst a)
candidateSubsts (compose subst' subst) as
candidateSubsts subst ((GEqE eq):as) = do
let (s,t) = applySkTerm subst <$> eq
(term,pat) | frees s == [] = (s,t)
| frees t == [] = (t,s)
| otherwise = error $ "impliedFormulas: impossible, "
++ "equality not guarded as checked"
++"by 'Guarded.formulaToGuarded'."
subst' <- (`runReader` hnd) $ matchTerm term pat
candidateSubsts (compose subst' subst) as
data SkConst = SkName Name
| SkConst LVar
deriving( Eq, Ord, Show, Data, Typeable )
type SkTerm = VTerm SkConst LVar
type SkFact = Fact SkTerm
type SkSubst = Subst SkConst LVar
type SkGuarded = LGuarded SkConst
type BSkTerm = VTerm SkConst BLVar
type BSkAtom = Atom BSkTerm
instance IsConst SkConst
skolemizeTerm :: LNTerm -> SkTerm
skolemizeTerm = fmapTerm conv
where
conv :: Lit Name LVar -> Lit SkConst LVar
conv (Var v) = Con (SkConst v)
conv (Con n) = Con (SkName n)
skolemizeFact :: LNFact -> Fact SkTerm
skolemizeFact = fmap skolemizeTerm
skolemizeAtom :: BLAtom -> BSkAtom
skolemizeAtom = fmap skolemizeBTerm
skolemizeGuarded :: LNGuarded -> SkGuarded
skolemizeGuarded = mapGuardedAtoms (const skolemizeAtom)
applySkTerm :: SkSubst -> SkTerm -> SkTerm
applySkTerm subst t = applyVTerm subst t
applySkFact :: SkSubst -> SkFact -> SkFact
applySkFact subst = fmap (applySkTerm subst)
applySkAction :: SkSubst -> (SkTerm,SkFact) -> (SkTerm,SkFact)
applySkAction subst (t,f) = (applySkTerm subst t, applySkFact subst f)
skolemizeBTerm :: VTerm Name BLVar -> BSkTerm
skolemizeBTerm = fmapTerm conv
where
conv :: Lit Name BLVar -> Lit SkConst BLVar
conv (Var (Free x)) = Con (SkConst x)
conv (Var (Bound b)) = Var (Bound b)
conv (Con n) = Con (SkName n)
unskolemizeBTerm :: BSkTerm -> VTerm Name BLVar
unskolemizeBTerm t = fmapTerm conv t
where
conv :: Lit SkConst BLVar -> Lit Name BLVar
conv (Con (SkConst x)) = Var (Free x)
conv (Var (Bound b)) = Var (Bound b)
conv (Var (Free v)) = error $ "unskolemizeBTerm: free variable " ++
show v++" found in "++show t
conv (Con (SkName n)) = Con n
unskolemizeBLAtom :: BSkAtom -> BLAtom
unskolemizeBLAtom = fmap unskolemizeBTerm
unskolemizeLNGuarded :: SkGuarded -> LNGuarded
unskolemizeLNGuarded = mapGuardedAtoms (const unskolemizeBLAtom)
applyBSkTerm :: SkSubst -> VTerm SkConst BLVar -> VTerm SkConst BLVar
applyBSkTerm subst =
go
where
go t = case viewTerm t of
Lit l -> applyBLLit l
FApp o as -> fApp o (map go as)
applyBLLit :: Lit SkConst BLVar -> VTerm SkConst BLVar
applyBLLit l@(Var (Free v)) =
maybe (lit l) (fmapTerm (fmap Free)) (imageOf subst v)
applyBLLit l = lit l
applyBSkAtom :: SkSubst -> Atom (VTerm SkConst BLVar) -> Atom (VTerm SkConst BLVar)
applyBSkAtom subst = fmap (applyBSkTerm subst)
applySkGuarded :: SkSubst -> LGuarded SkConst -> LGuarded SkConst
applySkGuarded subst = mapGuardedAtoms (const $ applyBSkAtom subst)
matchAction :: (SkTerm, SkFact) -> (SkTerm, SkFact) -> WithMaude [SkSubst]
matchAction (i1, fa1) (i2, fa2) =
solveMatchLTerm sortOfSkol (i1 `matchWith` i2 <> fa1 `matchFact` fa2)
where
sortOfSkol (SkName n) = sortOfName n
sortOfSkol (SkConst v) = lvarSort v
matchTerm :: SkTerm -> SkTerm -> WithMaude [SkSubst]
matchTerm s t =
solveMatchLTerm sortOfSkol (s `matchWith` t)
where
sortOfSkol (SkName n) = sortOfName n
sortOfSkol (SkConst v) = lvarSort v