module Theory.Constraint.Solver.Contradictions (
Contradiction(..)
, substCreatesNonNormalTerms
, contradictions
, contradictorySystem
, prettyContradiction
) where
import Prelude hiding (id, (.))
import Data.Binary
import qualified Data.DAG.Simple as D (cyclic, reachableSet)
import Data.DeriveTH
import qualified Data.Foldable as F
import Data.List
import qualified Data.Map as M
import Data.Maybe (fromMaybe, listToMaybe)
import Data.Monoid
import qualified Data.Set as S
import Safe (headMay)
import Control.Basics
import Control.Category
import Control.DeepSeq
import Control.Monad.Reader
import qualified Extension.Data.Label as L
import Extension.Prelude
import Theory.Constraint.Solver.Types
import Theory.Constraint.System
import Theory.Model
import Theory.Tools.IntruderRules
import Theory.Text.Pretty
import Term.Rewriting.Norm (maybeNotNfSubterms, nf')
data Contradiction =
Cyclic
| NonNormalTerms
| ForbiddenExp
| ForbiddenBP
| ForbiddenKD
| ImpossibleChain
| NonInjectiveFactInstance (NodeId, NodeId, NodeId)
| IncompatibleEqs
| FormulasFalse
| SuperfluousLearn LNTerm NodeId
| NodeAfterLast (NodeId, NodeId)
deriving( Eq, Ord, Show )
contradictorySystem :: ProofContext -> System -> Bool
contradictorySystem ctxt = not . null . contradictions ctxt
contradictions :: ProofContext -> System -> [Contradiction]
contradictions ctxt sys = F.asum
[ guard (D.cyclic $ rawLessRel sys) *> pure Cyclic
, guard (hasNonNormalTerms sig sys) *> pure NonNormalTerms
, guard (hasForbiddenKD sys) *> pure ForbiddenKD
, guard (hasImpossibleChain sys) *> pure ImpossibleChain
, guard (enableDH msig && hasForbiddenExp sys) *> pure ForbiddenExp
, guard (enableBP msig && hasForbiddenBP sys) *> pure ForbiddenBP
, guard (eqsIsFalse $ L.get sEqStore sys) *> pure IncompatibleEqs
, guard (S.member gfalse $ L.get sFormulas sys) *> pure FormulasFalse
]
++
(NonInjectiveFactInstance <$> nonInjectiveFactInstances ctxt sys)
++
(NodeAfterLast <$> nodesAfterLast sys)
where
sig = L.get pcSignature ctxt
msig = mhMaudeSig . L.get pcMaudeHandle $ ctxt
hasForbiddenKD :: System -> Bool
hasForbiddenKD sys =
any isForbiddenKD $ M.elems $ L.get sNodes sys
where
isForbiddenKD ru = fromMaybe False $ do
[conc] <- return $ L.get rConcs ru
(DnK, t) <- kFactView conc
return $ neverContainsFreshPriv t
hasNonNormalTerms :: SignatureWithMaude -> System -> Bool
hasNonNormalTerms sig se =
any (not . (`runReader` hnd) . nf') (maybeNonNormalTerms hnd se)
where hnd = L.get sigmMaudeHandle sig
maybeNonNormalTerms :: MaudeHandle -> System -> [LNTerm]
maybeNonNormalTerms hnd se =
sortednub . concatMap getTerms . M.elems . L.get sNodes $ se
where getTerms (Rule _ ps cs as) = do
f <- ps++cs++as
t <- factTerms f
maybeNotNfSubterms (mhMaudeSig hnd) t
substCreatesNonNormalTerms :: MaudeHandle -> System -> LNSubst -> LNSubstVFresh -> Bool
substCreatesNonNormalTerms hnd sys fsubst =
\subst -> any (not . nfApply subst) terms
where terms = apply fsubst $ maybeNonNormalTerms hnd sys
nfApply subst0 t = t == t' || nf' t' `runReader` hnd
where tvars = freesList t
subst = restrictVFresh tvars subst0
t' = apply (freshToFreeAvoidingFast subst tvars) t
nonInjectiveFactInstances :: ProofContext -> System -> [(NodeId, NodeId, NodeId)]
nonInjectiveFactInstances ctxt se = do
Edge c@(i, _) (k, _) <- S.toList $ L.get sEdges se
let kFaPrem = nodeConcFact c se
kTag = factTag kFaPrem
kTerm = firstTerm kFaPrem
conflictingFact fa = factTag fa == kTag && firstTerm fa == kTerm
guard (kTag `S.member` L.get pcInjectiveFactInsts ctxt)
j <- S.toList $ D.reachableSet [i] less
let isCounterExample = (j /= i) && (j /= k) &&
maybe False checkRule (M.lookup j $ L.get sNodes se)
checkRule jRu = any conflictingFact (L.get rPrems jRu) &&
k `S.member` D.reachableSet [j] less
guard isCounterExample
return (i, j, k)
where
less = rawLessRel se
firstTerm = headMay . factTerms
nodesAfterLast :: System -> [(NodeId, NodeId)]
nodesAfterLast sys = case L.get sLastAtom sys of
Nothing -> []
Just i -> do j <- S.toList $ D.reachableSet [i] $ rawLessRel sys
guard (j /= i && isInTrace sys j)
return (i, j)
hasImpossibleChain :: System -> Bool
hasImpossibleChain sys =
any impossibleChain [ (c,p) | ChainG c p <- M.keys $ L.get sGoals sys ]
where
impossibleChain (c,p) = fromMaybe False $ do
(DnK, t_start) <- kFactView $ nodeConcFact c sys
(DnK, t_end) <- kFactView $ nodePremFact p sys
req_end_sym <- rootSym t_end
poss_end_syms <- possibleRootSyms t_start
return $ not (req_end_sym `elem` poss_end_syms)
rootSym :: LNTerm -> Maybe (Either LSort FunSym)
rootSym t =
case viewTerm t of
FApp sym _ -> return $ Right sym
Lit _ | sortOfLNTerm t == LSortMsg -> Nothing
| otherwise -> return $ Left (sortOfLNTerm t)
possibleRootSyms :: LNTerm -> Maybe [Either LSort FunSym]
possibleRootSyms t | neverContainsFreshPriv t = return []
possibleRootSyms t = case viewTerm2 t of
FExp a _b ->
((Right (NoEq expSym)):) <$> possibleRootSyms a
FPMult _b a ->
((Right <$> [NoEq expSym, NoEq pmultSym, C EMap])++) <$> possibleRootSyms a
FEMap _ _ -> return [Right (C EMap)]
_ -> case viewTerm t of
Lit _ -> (:[]) <$> rootSym t
FApp o args -> ((Right o):) . concat <$> mapM possibleRootSyms args
hasForbiddenExp :: System -> Bool
hasForbiddenExp sys =
any forbiddenDExp $ M.toList $ L.get sNodes sys
where
forbiddenDExp (i,ru) = fromMaybe False $ do
[p1,p2] <- return $ L.get rPrems ru
[conc] <- return $ L.get rConcs ru
(DnK, viewTerm2 -> FExp _ _) <- kFactView p1
(UpK, b ) <- kFactView p2
case kFactView conc of
Just (DnK, viewTerm2 -> FExp g c) ->
return $ (isSimpleTerm g && allMsgVarsKnownEarlier i (varTerm <$> frees g))
&& (niFactors c \\ niFactors b == [])
Just (DnK, g) ->
return $ isSimpleTerm g && allMsgVarsKnownEarlier i (varTerm <$> frees g)
_ -> return False
allMsgVarsKnownEarlier i args =
all (`elem` earlierMsgVars) (filter isMsgVar args)
where earlierMsgVars = do (j, _, t) <- allKUActions sys
guard $ isMsgVar t && alwaysBefore sys j i
return t
hasForbiddenBP :: System -> Bool
hasForbiddenBP sys =
(any isForbiddenDPMult $ M.elems $ L.get sNodes sys) ||
(any (isForbiddenDEMap sys) $ M.toList $ L.get sNodes sys) ||
(any (isForbiddenDEMapOrder sys) $ M.toList $ L.get sNodes sys)
isForbiddenDPMult :: Rule a -> Bool
isForbiddenDPMult ru = fromMaybe False $ do
[p1,p2] <- return $ L.get rPrems ru
[conc] <- return $ L.get rConcs ru
(DnK, viewTerm2 -> FPMult _ _) <- kFactView p1
(UpK, b ) <- kFactView p2
(DnK, viewTerm2 -> FPMult c p) <- kFactView conc
return $ neverContainsFreshPriv p
&& (niFactors c \\ niFactors b == [])
isForbiddenDEMap :: System -> (NodeId, RuleACInst) -> Bool
isForbiddenDEMap sys (i, ruExp) = fromMaybe False $ do
guard (isDExpRule ruExp)
ke_f <- resolveNodePremFact (i, PremIdx 1) sys
(UpK, ke) <- kFactView ke_f
ruEMap <- flip nodeRule sys <$>
listToMaybe [ ns | Edge (ns,_) (nt,pit) <- S.toList (L.get sEdges sys)
, nt == i, pit == PremIdx 0 ]
guard (isDEMapRule ruEMap)
[sP_f, rQ_f] <- return $ L.get rPrems ruEMap
(DnK, viewTerm2 -> FPMult s p) <- kFactView sP_f
(DnK, viewTerm2 -> FPMult r q) <- kFactView rQ_f
return (overComplicated s p ke || overComplicated r q ke)
where
overComplicated scalar point ke =
(niFactors scalar \\ niFactors ke == []) && neverContainsFreshPriv point
isForbiddenDEMapOrder :: System -> (NodeId, RuleACInst) -> Bool
isForbiddenDEMapOrder sys (i, ruDEMap) = fromMaybe False $ do
guard (isDEMapRule ruDEMap)
[f_p0, f_p1] <- return $ L.get rPrems ruDEMap
[f_c0] <- return $ L.get rConcs ruDEMap
(DnK, viewTerm2 -> FPMult s p) <- kFactView f_p0
(DnK, viewTerm2 -> FPMult r q) <- kFactView f_p1
(DnK, viewTerm2 -> FExp (viewTerm2 -> FEMap p' q') (viewTerm2 -> FMult as)) <- kFactView f_c0
guard (((p,q) == (p',q') || (p,q) == (q',p')) && as \\ [s,r] == [])
j1 <- lookupPremProvider (i,PremIdx 0)
j2 <- lookupPremProvider (i,PremIdx 1)
ruProto1 <- flip nodeRule sys <$> lookupPremProvider (j1, PremIdx 0)
ruProto2 <- flip nodeRule sys <$> lookupPremProvider (j2, PremIdx 0)
guard (isStandRule ruProto1 && isStandRule ruProto2)
return $ (factTags ruProto1) > (factTags ruProto2)
where
lookupPremProvider (k,prem) =
listToMaybe [ ns | Edge (ns,_) (nt,pit) <- S.toList (L.get sEdges sys)
, nt == k, pit == prem ]
factTags ru = map (map factTag) [L.get rPrems ru, L.get rConcs ru, L.get rActs ru]
isStandRule ru = ruleInfo (isStandName . L.get praciName) (const False) $ L.get rInfo ru
isStandName (StandRule _) = True
isStandName _ = False
prettyContradiction :: Document d => Contradiction -> d
prettyContradiction contra = case contra of
Cyclic -> text "cyclic"
IncompatibleEqs -> text "incompatible equalities"
NonNormalTerms -> text "non-normal terms"
ForbiddenExp -> text "non-normal exponentiation rule instance"
ForbiddenBP -> text "non-normal bilinear pairing rule instance"
ForbiddenKD -> text "forbidden KD-fact"
ImpossibleChain -> text "impossible chain"
NonInjectiveFactInstance cex -> text $ "non-injective facts " ++ show cex
FormulasFalse -> text "from formulas"
SuperfluousLearn m v ->
doubleQuotes (prettyLNTerm m) <->
text ("derived before and after") <->
doubleQuotes (prettyNodeId v)
NodeAfterLast (i,j) ->
text $ "node " ++ show j ++ " after last node " ++ show i
instance HasFrees Contradiction where
foldFrees f (SuperfluousLearn t v) = foldFrees f t `mappend` foldFrees f v
foldFrees f (NonInjectiveFactInstance x) = foldFrees f x
foldFrees f (NodeAfterLast x) = foldFrees f x
foldFrees _ _ = mempty
foldFreesOcc _ _ = const mempty
mapFrees f (SuperfluousLearn t v) = SuperfluousLearn <$> mapFrees f t <*> mapFrees f v
mapFrees f (NonInjectiveFactInstance x) = NonInjectiveFactInstance <$> mapFrees f x
mapFrees f (NodeAfterLast x) = NodeAfterLast <$> mapFrees f x
mapFrees _ c = pure c
$( derive makeBinary ''Contradiction)
$( derive makeNFData ''Contradiction)