runtimeverification · rv-jenkins · Aug 6, 2020 · Jul 15, 2020 · Jul 16, 2020 · Jul 16, 2020
diff --git a/kore/src/Kore/Builtin/AssociativeCommutative.hs b/kore/src/Kore/Builtin/AssociativeCommutative.hs
@@ -426,10 +426,9 @@ updateConcreteElements
     -> [(TermLike Concrete, value)]
     -> Maybe (Map (TermLike Concrete) value)
 updateConcreteElements elems newElems =
-    TermLike.assertConstructorLikeKeys allKeys
-        $ Foldable.foldrM (uncurry insertMissing) elems newElems
-      where
-        allKeys = Map.keys elems <> fmap fst newElems
+    Foldable.foldrM (uncurry insertMissing) elems newElems
+    & TermLike.assertConstructorLikeKeys (Map.keys elems)
+    & TermLike.assertConstructorLikeKeys (fst <$> newElems)
 
 {- | Sort the abstract elements.
 
@@ -767,7 +766,7 @@ unifyEqualsNormalized
                 (unzip . Map.toList)
                     (Domain.concreteElements unwrapped)
 
-    return (unifierTerm `withCondition` unifierCondition)
+    return (unifierTerm `Pattern.withCondition` unifierCondition)
   where
     sort1 = termLikeSort first
 

diff --git a/kore/src/Kore/Debug.hs b/kore/src/Kore/Debug.hs
@@ -1,5 +1,4 @@
 {-# OPTIONS_GHC -Wno-unused-top-binds    #-}
-{-# OPTIONS_GHC -fno-prof-auto #-}
 
 {- |
 Copyright   : (c) Runtime Verification, 2018

diff --git a/kore/src/Kore/Internal/Conditional.hs b/kore/src/Kore/Internal/Conditional.hs
@@ -6,8 +6,6 @@ Representation of conditional terms.
 
 -}
 
-{-# OPTIONS_GHC -fno-prof-auto #-}
-
 module Kore.Internal.Conditional
     ( Conditional (..)
     , withoutTerm

diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs
@@ -90,6 +90,7 @@ module Kore.Internal.TermLike
     , mkEndianness
     , mkSignedness
     , mkDefined
+    , unDefined
     -- * Predicate constructors
     , mkBottom_
     , mkCeil_
@@ -1557,6 +1558,16 @@ mkDefined = updateCallStack . worker
 mkDefinedAtTop :: Ord variable => TermLike variable -> TermLike variable
 mkDefinedAtTop = synthesize . DefinedF . Defined
 
+{- | Remove (recursively) the 'Defined' wrappers throughout a 'TermLike'.
+ -}
+unDefined :: TermLike variable -> TermLike variable
+unDefined =
+    Recursive.unfold $ \termLike ->
+        let attrs :< termLikeF = Recursive.project termLike in
+        case termLikeF of
+            DefinedF defined -> Recursive.project (getDefined defined)
+            _ -> attrs :< termLikeF
+
 {- | Construct an 'Endianness' pattern.
  -}
 mkEndianness

diff --git a/kore/src/Kore/Log/InfoReachability.hs b/kore/src/Kore/Log/InfoReachability.hs
@@ -36,7 +36,6 @@ instance Entry InfoReachability where
 primDoc :: Prim -> Maybe (Doc ann)
 primDoc Simplify = Just "simplifying the claim"
 primDoc CheckImplication = Just "checking the implication"
-primDoc InferDefined = Just "inferring that the configuration is defined"
 primDoc ApplyClaims = Just "applying claims"
 primDoc ApplyAxioms = Just "applying axioms"
 primDoc _ = Nothing

diff --git a/kore/src/Kore/Step/Axiom/Matcher.hs b/kore/src/Kore/Step/Axiom/Matcher.hs
@@ -171,6 +171,7 @@ matchOne pair =
     <|> matchBuiltinSet  pair
     <|> matchInj         pair
     <|> matchOverload    pair
+    <|> matchDefined     pair
     )
     & Error.maybeT (defer pair) return
 
@@ -408,6 +409,15 @@ matchOverload
     -> MaybeT (MatcherT variable simplifier) ()
 matchOverload termPair = Error.hushT (matchOverloading termPair) >>= push
 
+matchDefined
+    :: (MatchingVariable variable, MonadSimplify simplifier)
+    => Pair (TermLike variable)
+    -> MaybeT (MatcherT variable simplifier) ()
+matchDefined (Pair term1 term2)
+  | Defined_ def1 <- term1 = push (Pair def1 term2)
+  | Defined_ def2 <- term2 = push (Pair term1 def2)
+  | otherwise = empty
+
 -- * Implementation
 
 type MatchingVariable variable = InternalVariable variable

diff --git a/kore/src/Kore/Step/SMT/Translate.hs b/kore/src/Kore/Step/SMT/Translate.hs
@@ -211,6 +211,7 @@ translatePredicateWith translateTerm predicate =
                 (<|>)
                     (translateApplication app)
                     (translateUninterpreted SMT.tInt pat)
+            DefinedF (Defined child) -> translateInt child
             _ -> empty
 
     -- | Translate a functional pattern in the builtin Bool sort for SMT.
@@ -230,6 +231,7 @@ translatePredicateWith translateTerm predicate =
                 (<|>)
                     (translateApplication app)
                     (translateUninterpreted SMT.tBool pat)
+            DefinedF (Defined child) -> translateBool child
             _ -> empty
 
     translateApplication :: Application Symbol p -> Translator m variable SExpr

diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs
@@ -239,13 +239,14 @@ andEqualsFunctions notSimplifier =
     , (AndT,    \_ _ s -> Builtin.KEqual.unifyIfThenElse s)
     , (BothT,   \_ _ _ -> Builtin.Endianness.unifyEquals)
     , (BothT,   \_ _ _ -> Builtin.Signedness.unifyEquals)
-    , (BothT,   \_ _ s -> Builtin.Map.unifyEquals s)
+    , (BothT,   \_ _ s -> unifyDefinedModifier (Builtin.Map.unifyEquals s))
     , (EqualsT, \_ _ s -> Builtin.Map.unifyNotInKeys s notSimplifier)
-    , (BothT,   \_ _ s -> Builtin.Set.unifyEquals s)
+    , (BothT,   \_ _ s -> unifyDefinedModifier (Builtin.Set.unifyEquals s))
     , (BothT,   \_ t s -> Builtin.List.unifyEquals t s)
     , (BothT,   \_ _ _ -> domainValueAndConstructorErrors)
     , (BothT,   \_ _ _ -> domainValueAndEqualsAssumesDifferent)
     , (BothT,   \_ _ _ -> stringLiteralAndEqualsAssumesDifferent)
+    , (BothT,   \_ _ s -> unifyDefined s)
     , (AndT,    \_ _ _ t1 t2 -> Error.hoistMaybe $ functionAnd t1 t2)
     ]
 
@@ -330,7 +331,8 @@ equalAndEquals
     -> TermLike variable
     -> MaybeT unifier (Pattern variable)
 equalAndEquals first second
-  | first == second =
+  | unDefined first == unDefined second =
+    -- TODO (thomas.tuegel): Preserve defined and simplified flags.
     return (Pattern.fromTermLike first)
 equalAndEquals _ _ = empty
 
@@ -699,16 +701,14 @@ functionAnd
     -> Maybe (Pattern variable)
 functionAnd first second
   | isFunctionPattern first, isFunctionPattern second =
-    return Conditional
-        { term = first  -- different for Equals
-        -- Ceil predicate not needed since first being
-        -- bottom will make the entire term bottom. However,
-        -- one must be careful to not just drop the term.
-        , predicate =
-            Predicate.markSimplified
-            $ makeEqualsPredicate_ first second
-        , substitution = mempty
-        }
+    makeEqualsPredicate_ first second
+    & Predicate.markSimplified
+    -- Ceil predicate not needed since first being
+    -- bottom will make the entire term bottom. However,
+    -- one must be careful to not just drop the term.
+    & Condition.fromPredicate
+    & Pattern.withCondition first  -- different for Equals
+    & pure
   | otherwise = empty
 
 bytesDifferent
@@ -723,3 +723,53 @@ bytesDifferent
   | bytesFirst /= bytesSecond
     = return Pattern.bottom
 bytesDifferent _ _ = empty
+
+{- | Unwrap a 'Defined' term if it is not handled elsewhere.
+ -}
+unifyDefined
+    :: MonadUnify unifier
+    => TermSimplifier variable unifier
+    -> TermLike variable
+    -> TermLike variable
+    -> MaybeT unifier (Pattern variable)
+unifyDefined unifyChildren term1 term2
+  | Defined_ child1 <- term1 = lift $ unifyChildren child1 term2
+  | Defined_ child2 <- term2 = lift $ unifyChildren term1 child2
+  | otherwise = empty
+
+unifyDefinedModifier
+    :: InternalVariable variable
+    => Monad monad
+    => (TermLike variable -> TermLike variable -> monad (Pattern variable))
+    -> TermLike variable
+    -> TermLike variable
+    -> monad (Pattern variable)
+unifyDefinedModifier unify (Defined_ def1) (Defined_ def2) = do
+    unified <- unify def1 def2
+    let Conditional { term } = unified
+        term'
+          | term == def1 || term == def2
+          = mkDefined term
+          | otherwise = term
+        unified' = term' <$ unified
+    pure unified'
+unifyDefinedModifier unify (Defined_ def1) term2 = do
+    unified <- unify def1 term2
+    let Conditional { term } = unified
+        term'
+          | unDefined term == unDefined def1
+          = mkDefined term
+          | otherwise = term
+        unified' = term' <$ unified
+    pure unified'
+unifyDefinedModifier unify term1 (Defined_ def2) = do
+    unified <- unify term1 def2
+    let Conditional { term } = unified
+        term'
+          | unDefined term == unDefined def2
+          = mkDefined term
+          | otherwise = term
+        unified' = term' <$ unified
+    pure unified'
+unifyDefinedModifier unify term1 term2 =
+    unify term1 term2
diff --git a/kore/src/Kore/Step/Simplification/Data.hs b/kore/src/Kore/Step/Simplification/Data.hs
@@ -9,7 +9,6 @@ Portability : portable
 -}
 
 {-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-prof-auto #-}
 
 module Kore.Step.Simplification.Data
     ( Simplifier

diff --git a/kore/src/Kore/Step/Transition.hs b/kore/src/Kore/Step/Transition.hs
@@ -6,8 +6,6 @@ License     : NCSA
 
 {-# LANGUAGE UndecidableInstances #-}
 
-{-# OPTIONS_GHC -fno-prof-auto #-}
-
 module Kore.Step.Transition
     ( TransitionT (..)
     , Transition

diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs
@@ -94,6 +94,7 @@ import Kore.Internal.Symbol
     )
 import Kore.Internal.TermLike
     ( isFunctionPattern
+    , mkDefined
     , mkIn
     , termLikeSort
     )
@@ -202,11 +203,6 @@ class Goal goal where
     -- checkImplication.
     isTriviallyValid :: goal -> Bool
 
-    inferDefined
-        :: MonadSimplify m
-        => goal
-        -> Strategy.TransitionT (Rule goal) m goal
-
     checkImplication
         :: MonadSimplify m
         => goal -> m (CheckImplicationResult goal)
@@ -313,8 +309,6 @@ instance Goal OnePathRule where
 
     isTriviallyValid = isTriviallyValid' _Unwrapped
 
-    inferDefined = inferDefined' _Unwrapped
-
 deriveSeqOnePath
     ::  MonadSimplify simplifier
     =>  [Rule OnePathRule]
@@ -342,7 +336,6 @@ instance Goal AllPathRule where
     simplify = simplify' _Unwrapped
     checkImplication = checkImplication' _Unwrapped
     isTriviallyValid = isTriviallyValid' _Unwrapped
-    inferDefined = inferDefined' _Unwrapped
     applyClaims claims = deriveSeqAllPath (map goalToRule claims)
 
     applyAxioms axiomss = \goal ->
@@ -418,15 +411,6 @@ instance Goal ReachabilityRule where
     isTriviallyValid (AllPath goal) = isTriviallyValid goal
     isTriviallyValid (OnePath goal) = isTriviallyValid goal
 
-    inferDefined (AllPath goal) =
-        inferDefined goal
-        & fmap AllPath
-        & allPathTransition
-    inferDefined (OnePath goal) =
-        inferDefined goal
-        & fmap OnePath
-        & onePathTransition
-
     applyClaims claims (AllPath goal) =
         applyClaims (mapMaybe maybeAllPath claims) goal
         & fmap (fmap AllPath)
@@ -515,12 +499,6 @@ transitionRule claims axiomGroups = transitionRuleWorker
     transitionRuleWorker Simplify (GoalRemainder goal) =
         GoalRemainder <$> simplify goal
 
-    transitionRuleWorker InferDefined (GoalRemainder goal) = do
-        results <- tryTransitionT (inferDefined goal)
-        case results of
-            [] -> return Proven
-            _ -> GoalRemainder <$> Transition.scatter results
-
     transitionRuleWorker CheckImplication (Goal goal) = do
         result <- checkImplication goal
         case result of
@@ -582,7 +560,6 @@ reachabilityFirstStep =
         , CheckGoalStuck
         , CheckGoalRemainder
         , Simplify
-        , InferDefined
         , TriviallyValid
         , CheckImplication
         , ApplyAxioms
@@ -598,7 +575,6 @@ reachabilityNextStep =
         , CheckGoalStuck
         , CheckGoalRemainder
         , Simplify
-        , InferDefined
         , TriviallyValid
         , CheckImplication
         , ApplyClaims
@@ -689,23 +665,9 @@ simplify'
     -> goal
     -> Strategy.TransitionT (Rule goal) m goal
 simplify' lensRulePattern =
-    Lens.traverseOf (lensRulePattern . RulePattern.leftPattern) $ \config -> do
-        configs <-
-            simplifyTopConfiguration config >>= SMT.Evaluator.filterMultiOr
-            & lift
-        if isBottom configs
-            then pure Pattern.bottom
-            else Foldable.asum (pure <$> configs)
-
-inferDefined'
-    :: MonadSimplify m
-    => Lens' goal (RulePattern VariableName)
-    -> goal
-    -> Strategy.TransitionT (Rule goal) m goal
-inferDefined' lensRulePattern =
     Lens.traverseOf (lensRulePattern . RulePattern.leftPattern) $ \config -> do
         let definedConfig =
-                Pattern.andCondition config
+                Pattern.andCondition (mkDefined <$> config)
                 $ from $ makeCeilPredicate_ (Conditional.term config)
         configs <-
             simplifyTopConfiguration definedConfig

diff --git a/kore/src/Kore/Strategies/ProofState.hs b/kore/src/Kore/Strategies/ProofState.hs
@@ -39,9 +39,6 @@ data Prim
     | Simplify
     | CheckImplication
     -- ^ Check if the claim's implication is valid.
-    | InferDefined
-    -- ^ Infer that the left-hand side of the claim is defined. This is related
-    -- to 'CheckImplication', but separated as an optimization.
     | TriviallyValid
     | ApplyClaims
     | ApplyAxioms
@@ -52,9 +49,8 @@ instance Pretty Prim where
     pretty CheckGoalRemainder = "Transition CheckGoalRemainder."
     pretty CheckGoalStuck = "Transition CheckGoalStuck."
     pretty ResetGoal = "Transition ResetGoal."
-    pretty Simplify = "Transition Simplify."
+    pretty Simplify = "simplify the claim"
     pretty CheckImplication = "Transition CheckImplication."
-    pretty InferDefined = "infer left-hand side is defined"
     pretty TriviallyValid = "Transition TriviallyValid."
     pretty ApplyClaims = "apply claims"
     pretty ApplyAxioms = "apply axioms"

diff --git a/kore/src/Kore/Unification/UnifierT.hs b/kore/src/Kore/Unification/UnifierT.hs
@@ -4,8 +4,6 @@ License     : NCSA
 
  -}
 
-{-# OPTIONS_GHC -fno-prof-auto #-}
-
 module Kore.Unification.UnifierT
     ( UnifierT (..)
     , runUnifierT

diff --git a/kore/src/Prof.hs b/kore/src/Prof.hs
@@ -4,8 +4,6 @@ License     : NCSA
 
 -}
 
-{-# OPTIONS_GHC -fno-prof-auto #-}
-
 module Prof
     ( MonadProf (..)
     , defaultTraceProf

diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs
@@ -6,8 +6,6 @@ License     : NCSA
 Maintainer  : thomas.tuegel@runtimeverification.com
 -}
 
-{-# OPTIONS_GHC -fno-prof-auto #-}
-
 module SMT
     ( SMT, getSMT
     , Solver