4118 better indexing for rewrite rules

booster/library/Booster/Definition/Util.hs

@@ -30,7 +30,7 @@ import Booster.Definition.Attributes.Base
 import Booster.Definition.Base
 import Booster.Definition.Ceil (ComputeCeilSummary (..))
 import Booster.Pattern.Base
-import Booster.Pattern.Index (CellIndex (..), TermIndex (..))
+import Booster.Pattern.Index (TermIndex (..))
 import Booster.Pattern.Pretty
 import Booster.Prettyprinter
 import Booster.Util
@@ -111,16 +111,16 @@ instance Pretty Summary where
                         : tableView prettyLabel prettyLabel summary.subSorts
                    )
                 <> ( "Rewrite rules by term index:"
-                        : tableView prettyTermIndex pretty summary.rewriteRules
+                        : tableView pretty pretty summary.rewriteRules
                    )
                 <> ( "Function equations by term index:"
-                        : tableView prettyTermIndex pretty summary.functionRules
+                        : tableView pretty pretty summary.functionRules
                    )
                 <> ( "Simplifications by term index:"
-                        : tableView prettyTermIndex pretty summary.simplifications
+                        : tableView pretty pretty summary.simplifications
                    )
                 <> ( "Ceils:"
-                        : tableView prettyTermIndex prettyCeilRule summary.ceils
+                        : tableView pretty prettyCeilRule summary.ceils
                    )
                 <> [mempty]
       where
@@ -140,13 +140,6 @@ instance Pretty Summary where
 
         prettyLabel = either error (pretty . BS.unpack) . decodeLabel
 
-        prettyTermIndex :: TermIndex -> Doc a
-        prettyTermIndex (TermIndex ixs) = Pretty.sep $ map prettyCellIndex ixs
-
-        prettyCellIndex Anything = "Anything"
-        prettyCellIndex (TopSymbol sym) = prettyLabel sym
-        prettyCellIndex None = "None"
-
         prettyCeilRule :: RewriteRule r -> Doc a
         prettyCeilRule RewriteRule{lhs, rhs} =
             "#Ceil(" <+> pretty' @['Decoded, 'Truncated] lhs <+> ") =>" <+> pretty' @['Decoded, 'Truncated] rhs

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -802,7 +802,7 @@ applyEquations theory handler term = do
         withContext CtxAbort $ logMessage ("Index 'None'" :: Text)
         throw (IndexIsNone term)
     let
-        indexes = Set.toList $ Idx.coveringIndexes index
+        indexes = Set.toList $ Map.keysSet theory `Idx.covering` index
         equationsFor i = fromMaybe Map.empty $ Map.lookup i theory
         -- neither simplification nor function equations should need groups,
         -- since simplification priority is just a suggestion and function equations
@@ -1172,7 +1172,9 @@ simplifyConstraint' :: LoggerMIO io => Bool -> Term -> EquationT io Term
 -- 'true \equals P' using simplifyBool if they are concrete, or using
 -- evaluateTerm.
 simplifyConstraint' recurseIntoEvalBool = \case
-    t@(Term TermAttributes{canBeEvaluated} _)
+    t@(Term TermAttributes{isEvaluated, canBeEvaluated} _)
+        | isEvaluated ->
+            pure t
         | isConcrete t && canBeEvaluated -> do
             mbApi <- (.llvmApi) <$> getConfig
             case mbApi of

booster/library/Booster/Pattern/Index.hs

@@ -7,22 +7,32 @@ Everything to do with term indexing.
 module Booster.Pattern.Index (
     CellIndex (..),
     TermIndex (..),
+    -- Flat lattice
+    (^<=^),
+    invert,
+    -- compute index cover for rule selection
+    covering,
+    -- indexing
     compositeTermIndex,
     kCellTermIndex,
     termTopIndex,
-    coveringIndexes,
+    -- helpers
     hasNone,
+    noFunctions,
 ) where
 
 import Control.Applicative (Alternative (..), asum)
 import Control.DeepSeq (NFData)
+import Data.ByteString.Char8 (ByteString, unpack)
 import Data.Functor.Foldable (embed, para)
 import Data.Maybe (fromMaybe)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import GHC.Generics (Generic)
+import Prettyprinter (Doc, Pretty, pretty, sep)
 
 import Booster.Pattern.Base
+import Booster.Util (decodeLabel)
 
 {- | Index data allowing for a quick lookup of potential axioms.
 
@@ -48,12 +58,54 @@ newtype TermIndex = TermIndex [CellIndex]
 
 data CellIndex
     = None -- bottom element
-    | TopSymbol SymbolName
+    | TopCons SymbolName
+    | TopFun SymbolName
+    | TopVal ByteString
+    | TopMap
+    | TopList
+    | TopSet
     | Anything -- top element
-    -- should we have  | Value Sort ?? (see Term type)
     deriving stock (Eq, Ord, Show, Generic)
     deriving anyclass (NFData)
 
+{- | Index lattice class. This is mostly just a _flat lattice_ but also
+  needs to support a special 'invert' method for the subject term index.
+-}
+class IndexLattice a where
+    (^<=^) :: a -> a -> Bool
+
+    invert :: a -> a
+
+ifGreater :: IndexLattice a => Set a -> a -> Set a
+ifGreater base x = Set.filter (x ^<=^) base
+
+{- | Partial less-or-equal for CellIndex (implies partial order)
+
+                Anything
+   ____________/   |  \_______________________________________...
+  /          /     |            |           \             \
+TopList ..TopSet  TopVal "x"..TopVal "y"  TopCons "A"..  TopFun "f"..
+  \__________|__   |  _________|____________|____________/____...
+                \  | /
+                 None
+-}
+instance IndexLattice CellIndex where
+    None ^<=^ _ = True
+    a ^<=^ None = a == None
+    _ ^<=^ Anything = True
+    Anything ^<=^ a = a == Anything
+    a ^<=^ b = a == b
+
+    invert None = Anything
+    invert Anything = None
+    invert a = a
+
+-- | Partial less-or-equal for TermIndex (product lattice)
+instance IndexLattice TermIndex where
+    TermIndex idxs1 ^<=^ TermIndex idxs2 = and $ zipWith (^<=^) idxs1 idxs2
+
+    invert (TermIndex idxs) = TermIndex (map invert idxs)
+
 {- | Combines two indexes (an "infimum" function on the index lattice).
 
   This is useful for terms containing an 'AndTerm': Any term that
@@ -65,35 +117,61 @@ instance Semigroup CellIndex where
     _ <> None = None
     x <> Anything = x
     Anything <> x = x
-    s@(TopSymbol s1) <> TopSymbol s2
-        | s1 == s2 = s
-        | otherwise = None -- incompatible indexes
+    idx1 <> idx2
+        | idx1 == idx2 = idx1
+        | otherwise = None
 
-{- | Compute all indexes that cover the given index, for rule lookup.
+-- | Pretty instances
+instance Pretty TermIndex where
+    pretty (TermIndex ixs) = sep $ map pretty ixs
 
-  An index B is said to "cover" another index A if all parts of B are
-  either equal to the respective parts of A, or 'Anything'.
+instance Pretty CellIndex where
+    pretty None = "_|_"
+    pretty Anything = "***"
+    pretty (TopCons sym) = "C--" <> prettyLabel sym
+    pretty (TopFun sym) = "F--" <> prettyLabel sym
+    pretty (TopVal sym) = "V--" <> prettyLabel sym
+    pretty TopMap = "Map"
+    pretty TopList = "List"
+    pretty TopSet = "Set"
 
-  When selecting candidate rules for a term, we must consider all
-  rules whose index has either the exact same @CellIndex@ or
-  @Anything@ at every position of their @TermIndex@.
--}
-coveringIndexes :: TermIndex -> Set TermIndex
-coveringIndexes (TermIndex ixs) =
-    Set.fromList . map TermIndex $ orAnything ixs
-  where
-    orAnything :: [CellIndex] -> [[CellIndex]]
-    orAnything [] = [[]]
-    orAnything (i : is) =
-        let rest = orAnything is
-         in map (i :) rest <> map (Anything :) rest
+prettyLabel :: ByteString -> Doc a
+prettyLabel = either error (pretty . unpack) . decodeLabel
 
 {- | Check whether a @TermIndex@ has @None@ in any position (this
 means no match will be possible).
 -}
 hasNone :: TermIndex -> Bool
 hasNone (TermIndex ixs) = None `elem` ixs
 
+-- | turns TopFun _ into Anything (for rewrite rule selection)
+noFunctions :: TermIndex -> TermIndex
+noFunctions (TermIndex ixs) = TermIndex (map funsAnything ixs)
+  where
+    funsAnything TopFun{} = Anything
+    funsAnything other = other
+
+{- | Computes all indexes that "cover" the given index, for rule lookup.
+
+  An index B is said to "cover" an index A if all components of B are
+  greater or equal to those of the respective component of A inverted.
+
+  * For components of A that are distinct from @Anything@, this means
+    the component of B is equal to that of A or @Anything@.
+  * For components of A that are @None@, the respective component of B
+    _must_ be @Anything@. However, if A contains @None@ no match is
+    possible anyway.
+  * For components of A that are @Anything@, B can contain an
+    arbitrary index (@None@ will again have no chance of a match,
+    though).
+
+  When selecting candidate rules for a term, we must consider all
+  rules whose index has either the exact same @CellIndex@ or
+  @Anything@ at every position of their @TermIndex@.
+-}
+covering :: Set TermIndex -> TermIndex -> Set TermIndex
+covering prior ix = prior `ifGreater` invert ix
+
 -- | Indexes a term by the heads of K sequences in given cells.
 compositeTermIndex :: [SymbolName] -> Term -> TermIndex
 compositeTermIndex cells t = TermIndex [kCellIndexFor c t | c <- cells]
@@ -162,11 +240,25 @@ stripSortInjections = \case
 termTopIndex :: Term -> TermIndex
 termTopIndex = TermIndex . (: []) . cellTopIndex
 
+-- | Cell top indexes form a lattice with a flat partial ordering
 cellTopIndex :: Term -> CellIndex
 cellTopIndex = \case
-    SymbolApplication symbol _ _ ->
-        TopSymbol symbol.name
+    ConsApplication symbol _ _ ->
+        TopCons symbol.name
+    FunctionApplication symbol _ _ ->
+        TopFun symbol.name
+    DomainValue _ v ->
+        TopVal v
+    Var{} ->
+        Anything
+    KMap{} ->
+        TopMap
+    KList{} ->
+        TopList
+    KSet{} ->
+        TopSet
+    -- look-through
+    Injection _ _ t ->
+        cellTopIndex t
     AndTerm t1 t2 ->
         cellTopIndex t1 <> cellTopIndex t2
-    _other ->
-        Anything

booster/library/Booster/Pattern/Rewrite.hs

@@ -179,7 +179,13 @@ rewriteStep cutLabels terminalLabels pat = do
         termIdx = getIndex pat.term
     when (Idx.hasNone termIdx) $ throw (TermIndexIsNone pat.term)
     let
-        indexes = Set.toList $ Idx.coveringIndexes termIdx
+        indexes =
+            Set.toList $ Map.keysSet def.rewriteTheory `Idx.covering` Idx.noFunctions termIdx
+        -- Function calls in the index have to be generalised to
+        -- `Anything` for rewriting because they may evaluate to any
+        -- category of terms. If there are any function calls in the
+        -- subject, the rewrite can only succeed if the function call
+        -- is matched to a variable.
         rulesFor i = fromMaybe Map.empty $ Map.lookup i def.rewriteTheory
         rules =
             map snd . Map.toAscList . Map.unionsWith (<>) $ map rulesFor indexes

booster/test/internalisation/bool.kore.report

@@ -18,37 +18,37 @@ Subsorts:
 - SortBool: SortBool
 Rewrite rules by term index:
 Function equations by term index:
-- Lbl_=/=Bool_: /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (960, 8)
-- Lbl_andBool_: 4
+- F--Lbl_=/=Bool_: /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (960, 8)
+- F--Lbl_andBool_: 4
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (933, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (932, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (934, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (931, 8)
-- Lbl_andThenBool_: 4
+- F--Lbl_andThenBool_: 4
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (938, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (937, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (939, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (936, 8)
-- Lbl_impliesBool_: 4
+- F--Lbl_impliesBool_: 4
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (958, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (957, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (956, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (955, 8)
-- Lbl_orBool_: 4
+- F--Lbl_orBool_: 4
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (948, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (946, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (947, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (945, 8)
-- Lbl_orElseBool_: 4
+- F--Lbl_orElseBool_: 4
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (953, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (951, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (952, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (950, 8)
-- Lbl_xorBool_: 3
+- F--Lbl_xorBool_: 3
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (943, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (942, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (941, 8)
-- LblnotBool_: 2
+- F--LblnotBool_: 2
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (929, 8)
   - /nix/store/08jyy9cx4xp32ca29lfsa1k4mbvw6kwv-k-5.5.140-dirty-maven/include/kframework/builtin/domains.md :  (928, 8)
 Simplifications by term index: