kore-exec: make --strategy all default; clean-up (#2209)

* strategy: make all default strategy

* strategy: remove heat-cool strategy options

* Remove heat-cool code

* Address review comment

Author: ana-pantilie

kore/app/exec/Main.hs

@@ -367,17 +367,13 @@ parseKoreExecOptions startTime =
         option (readSum "strategy" strategies)
             (  metavar "STRATEGY"
             <> long "strategy"
-            -- TODO (thomas.tuegel): Make defaultStrategy the default when it
-            -- works correctly.
-            <> value ("any", priorityAnyStrategy)
+            <> value ("all", priorityAllStrategy)
             <> help "Select rewrites using STRATEGY."
             )
       where
         strategies =
             [ ("any", priorityAnyStrategy)
             , ("all", priorityAllStrategy)
-            , ("any-heating-cooling", heatingCooling priorityAnyStrategy)
-            , ("all-heating-cooling", heatingCooling priorityAllStrategy)
             ]
     breadth =
         option auto

kore/src/Kore/Attribute/Axiom.hs

@@ -9,7 +9,6 @@ Maintainer  : thomas.tuegel@runtimeverification.com
 
 module Kore.Attribute.Axiom
     ( Axiom (..)
-    , HeatCool (..)
     , ProductionID (..)
     , Priority (..)
     , Owise (..)
@@ -61,7 +60,6 @@ import Kore.Attribute.Axiom.Symbolic
 import Kore.Attribute.Axiom.Unit
 import Kore.Attribute.Comm
 import Kore.Attribute.Functional
-import Kore.Attribute.HeatCool
 import Kore.Attribute.Idem
 import Kore.Attribute.Label
 import Kore.Attribute.Overload
@@ -95,9 +93,7 @@ import qualified SQL
  -}
 data Axiom symbol variable =
     Axiom
-    { heatCool :: !HeatCool
-    -- ^ An axiom may be denoted as a heating or cooling rule.
-    , productionID :: !ProductionID
+    { productionID :: !ProductionID
     -- ^ The identifier from the front-end identifying a rule or group of rules.
     , priority :: !Priority
     -- ^ A number associated to each rule,
@@ -148,8 +144,7 @@ data Axiom symbol variable =
 instance Default (Axiom symbol variable) where
     def =
         Axiom
-            { heatCool = def
-            , productionID = def
+            { productionID = def
             , priority = def
             , assoc = def
             , comm = def
@@ -177,8 +172,7 @@ instance
   where
     from =
         mconcat . sequence
-            [ from . heatCool
-            , from . productionID
+            [ from . productionID
             , from . priority
             , from . assoc
             , from . comm
@@ -207,9 +201,6 @@ instance From (Axiom symbol variable) PriorityAttributes where
             , simplificationAttr = simplification
             }
 
-instance From (Axiom symbol variable) HeatCool where
-    from Axiom { heatCool } = heatCool
-
 instance SQL.Column (Axiom SymbolOrAlias VariableName) where
     -- TODO (thomas.tuegel): Use a foreign key.
     defineColumn tableName _ =
@@ -234,8 +225,7 @@ parseAxiomAttribute
     -> Axiom SymbolOrAlias VariableName
     -> Parser (Axiom SymbolOrAlias VariableName)
 parseAxiomAttribute freeVariables attr =
-        typed @HeatCool (parseAttribute attr)
-        Monad.>=> typed @ProductionID (parseAttribute attr)
+        typed @ProductionID (parseAttribute attr)
         Monad.>=> typed @Priority (parseAttribute attr)
         Monad.>=> typed @Assoc (parseAttribute attr)
         Monad.>=> typed @Comm (parseAttribute attr)

kore/src/Kore/Attribute/HeatCool.hs

@@ -16,7 +16,6 @@ module Kore.Step
     , priorityAnyStrategy
     , TransitionRule
     , transitionRule
-    , heatingCooling
       -- * Re-exports
     , RulePattern
     , Natural
@@ -46,9 +45,6 @@ import qualified Kore.Step.RewriteStep as Step
 import Kore.Step.RulePattern
     ( RewriteRule (..)
     , RulePattern
-    , isCoolingRule
-    , isHeatingRule
-    , isNormalRule
     )
 import qualified Kore.Step.Simplification.Pattern as Pattern
     ( simplifyTopConfiguration
@@ -171,24 +167,3 @@ priorityAnyStrategy rewrites =
     anyRewrite sortedRewrites
   where
     sortedRewrites = sortOn Attribute.getPriorityOfAxiom rewrites
-
-{- | Heat the configuration, apply a normal rewrite, and cool the result.
- -}
--- TODO (thomas.tuegel): This strategy is not right because heating/cooling
--- rules must have side conditions if encoded as \rewrites, or they must be
--- \equals rules, which are not handled by this strategy.
-heatingCooling
-    :: From rule Attribute.HeatCool
-    => ([rule] -> Strategy (Prim rule))
-    -- ^ 'allRewrites' or 'anyRewrite'
-    -> [rule]
-    -> Strategy (Prim rule)
-heatingCooling rewriteStrategy rewrites =
-    Strategy.sequence [Strategy.many heat, normal, Strategy.try cool]
-  where
-    heatingRules = filter isHeatingRule rewrites
-    heat = rewriteStrategy heatingRules
-    normalRules = filter isNormalRule rewrites
-    normal = rewriteStrategy normalRules
-    coolingRules = filter isCoolingRule rewrites
-    cool = rewriteStrategy coolingRules

kore/src/Kore/Step.hs

@@ -146,9 +146,6 @@ instance TopBottom ClaimPattern where
 instance From ClaimPattern Attribute.PriorityAttributes where
     from = from @(Attribute.Axiom _ _) . attributes
 
-instance From ClaimPattern Attribute.HeatCool where
-    from = from @(Attribute.Axiom _ _) . attributes
-
 freeVariablesRight
     :: ClaimPattern
     -> FreeVariables RewritingVariableName

kore/src/Kore/Step/ClaimPattern.hs

@@ -14,9 +14,6 @@ module Kore.Step.RulePattern
     , UnifyingRule (..)
     , rulePattern
     , leftPattern
-    , isHeatingRule
-    , isCoolingRule
-    , isNormalRule
     , applySubstitution
     , topExistsToImplicitForall
     , isFreeOf
@@ -238,9 +235,6 @@ instance TopBottom (RulePattern variable) where
 instance From (RulePattern variable) Attribute.PriorityAttributes where
     from = from @(Attribute.Axiom _ _) . attributes
 
-instance From (RulePattern variable) Attribute.HeatCool where
-    from = from @(Attribute.Axiom _ _) . attributes
-
 -- | Creates a basic, unconstrained, Equality pattern
 rulePattern
     :: InternalVariable variable
@@ -271,30 +265,6 @@ leftPattern =
       where
         (left, condition) = Pattern.splitTerm pattern'
 
-{- | Does the axiom pattern represent a heating rule?
- -}
-isHeatingRule :: forall rule. From rule Attribute.HeatCool => rule -> Bool
-isHeatingRule rule =
-    case from @rule @Attribute.HeatCool rule of
-        Attribute.Heat -> True
-        _ -> False
-
-{- | Does the axiom pattern represent a cooling rule?
- -}
-isCoolingRule :: forall rule. From rule Attribute.HeatCool => rule -> Bool
-isCoolingRule rule =
-    case from @rule @Attribute.HeatCool rule of
-        Attribute.Cool -> True
-        _ -> False
-
-{- | Does the axiom pattern represent a normal rule?
- -}
-isNormalRule :: forall rule. From rule Attribute.HeatCool => rule -> Bool
-isNormalRule rule =
-    case from @rule @Attribute.HeatCool rule of
-        Attribute.Normal -> True
-        _ -> False
-
 -- | Converts the 'RHS' back to the term form.
 rhsToTerm
     :: InternalVariable variable
@@ -522,9 +492,6 @@ instance
 instance From (RewriteRule variable) Attribute.PriorityAttributes where
     from = from @(RulePattern _) . getRewriteRule
 
-instance From (RewriteRule variable) Attribute.HeatCool where
-    from = from @(RulePattern _) . getRewriteRule
-
 instance TopBottom (RewriteRule variable) where
     isTop _ = False
     isBottom _ = False