NOT READY Compute syntactic transitive closure for select relational symbols

booster/library/Booster/Definition/Base.hs

@@ -47,6 +47,7 @@ data KoreDefinition = KoreDefinition
     , rewriteTheory :: Theory (RewriteRule "Rewrite")
     , functionEquations :: Theory (RewriteRule "Function")
     , simplifications :: Theory (RewriteRule "Simplification")
+    , existentialSimplifications :: Theory (RewriteRule "ExistentialSimplification")
     , ceils :: Theory (RewriteRule "Ceil")
     }
     deriving stock (Eq, Show, GHC.Generic)
@@ -67,6 +68,7 @@ emptyKoreDefinition attributes =
         , rewriteTheory = Map.empty
         , functionEquations = Map.empty
         , simplifications = Map.empty
+        , existentialSimplifications = Map.empty
         , ceils = Map.empty
         }
 

booster/library/Booster/Pattern/Bool.hs

@@ -17,6 +17,7 @@ module Booster.Pattern.Bool (
     pattern AndBool,
     pattern EqualsInt,
     pattern EqualsBool,
+    pattern LtInt,
     pattern NEqualsInt,
     pattern EqualsK,
     pattern NEqualsK,
@@ -102,7 +103,15 @@ pattern NotBool t =
         []
         [t]
 
-pattern EqualsInt, EqualsBool, NEqualsInt, EqualsK, NEqualsK, SetIn :: Term -> Term -> Term
+pattern
+    EqualsInt
+    , EqualsBool
+    , LtInt
+    , NEqualsInt
+    , EqualsK
+    , NEqualsK
+    , SetIn ::
+        Term -> Term -> Term
 pattern EqualsInt a b =
     SymbolApplication
         ( Symbol
@@ -114,6 +123,17 @@ pattern EqualsInt a b =
             )
         []
         [a, b]
+pattern LtInt a b =
+    SymbolApplication
+        ( Symbol
+                "Lbl'Unds-LT-'Int'Unds'"
+                []
+                [SortInt, SortInt]
+                SortBool
+                (HookedTotalFunctionWithSMT "INT.lt" "<")
+            )
+        []
+        [a, b]
 pattern EqualsBool a b =
     SymbolApplication
         ( Symbol

booster/library/Booster/Pattern/PartialOrder.hs

@@ -0,0 +1,61 @@
+{-# LANGUAGE PatternSynonyms #-}
+
+{- |
+Copyright   : (c) Runtime Verification, 2024
+License     : BSD-3-Clause
+-}
+module Booster.Pattern.PartialOrder (transitiveClosure) where
+
+import Control.Monad (guard)
+import Data.Maybe (mapMaybe)
+import Data.Set (Set)
+import Data.Set qualified as Set
+
+import Booster.Pattern.Base
+
+{- | Given a set of predicates @ps@, construct a syntactic transitive closure of relative to the symbol @sym@.
+
+     This function only returns new predicates (if any).
+
+     If the @ps@ contains application of symbols other than @sym@, they are ignored.
+-}
+transitiveClosure :: Symbol -> Set Predicate -> Set Predicate
+transitiveClosure sym ps =
+    let attempts = map (\target -> Attempt target (Set.toList (Set.delete target ps))) . Set.toList $ ps
+     in (Set.fromList . concatMap (makeTransitiveStep sym) $ attempts)
+
+-- | An @Attempt@ is a target clause and a list of assumption clauses
+data Attempt = Attempt
+    { target :: !Predicate
+    -- ^ target predicate to eliminate, contains an existential variable
+    , assumptions :: ![Predicate]
+    -- ^ predicates that are assume "known", must contain the same existential that the target
+    }
+
+{- | Validate a predicate clause. Checks:
+     * the clause is a symbol application of @sym@
+     * the variables have distinct names, i.e. @sym@ is irreflexive
+-}
+validateClause :: Symbol -> Predicate -> Bool
+validateClause sym (Predicate p) = case p of
+    (SymbolApplication clauseSym _ [(Var Variable{variableName = a}), (Var Variable{variableName = b})]) -> clauseSym == sym && a /= b
+    _ -> False
+
+-- | Try solving, return an instantiated target if successful
+makeTransitiveStep :: Symbol -> Attempt -> [Predicate]
+makeTransitiveStep sym Attempt{target, assumptions} = do
+    guard (all (validateClause sym) (target : assumptions))
+    mapMaybe (matchAndTransit sym target) assumptions
+
+{- | Try to make strengthen the @left@ predicate using the @right@ predicate,
+  assuming both are the same *transitive* symbol
+-}
+matchAndTransit :: Symbol -> Predicate -> Predicate -> Maybe Predicate
+matchAndTransit sym (Predicate current) (Predicate next) =
+    case (current, next) of
+        (SymbolApplication symbol1 sorts [a, b], SymbolApplication symbol2 _ [c, d]) -> do
+            guard (symbol1 == symbol2 && b == c)
+            let newClause = Predicate $ SymbolApplication symbol1 sorts [a, d]
+            guard (validateClause sym newClause)
+            pure newClause
+        _ -> Nothing

booster/library/Booster/Pattern/Util.hs

@@ -30,6 +30,7 @@ module Booster.Pattern.Util (
     cellVariableStats,
     stripMarker,
     markAsExVar,
+    isExVar,
     markAsRuleVar,
     incrementNameCounter,
 ) where
@@ -125,6 +126,9 @@ markAsRuleVar = ("Rule#" <>)
 markAsExVar :: VarName -> VarName
 markAsExVar = ("Ex#" <>)
 
+isExVar :: VarName -> Bool
+isExVar = BS.isPrefixOf "Ex#"
+
 {- | Strip variable provenance prefixes introduced using "markAsRuleVar" and "markAsExVar"
 in "Syntax.ParsedKore.Internalize"
 -}

booster/library/Booster/Syntax/ParsedKore/Internalise.hs

@@ -181,6 +181,7 @@ mergeDefs k1 k2
                 <*> pure (mergeTheories rewriteTheory k1 k2)
                 <*> pure (mergeTheories functionEquations k1 k2)
                 <*> pure (mergeTheories simplifications k1 k2)
+                <*> pure (mergeTheories existentialSimplifications k1 k2)
                 <*> pure (mergeTheories ceils k1 k2)
   where
     mergeTheories ::
@@ -235,6 +236,7 @@ addModule
                     , rewriteTheory = currentRewriteTheory
                     , functionEquations = currentFctEqs
                     , simplifications = currentSimpls
+                    , existentialSimplifications = currentExistentialSimplifications
                     , ceils = currentCeils
                     }
                 )
@@ -296,6 +298,7 @@ addModule
                             , rewriteTheory = currentRewriteTheory -- no rules yet
                             , functionEquations = Map.empty
                             , simplifications = Map.empty
+                            , existentialSimplifications = Map.empty
                             , ceils = Map.empty
                             }
 
@@ -352,6 +355,7 @@ addModule
                 subsortPairs = mapMaybe retractSubsortRule newAxioms
                 newFunctionEquations = mapMaybe retractFunctionRule newAxioms
                 newSimplifications = mapMaybe retractSimplificationRule newAxioms
+                newExistentialSimplifications = mapMaybe retractExistentialSimplificationRule newAxioms
                 newCeils = mapMaybe retractCeilRule newAxioms
             let rewriteIndex =
                     if null defAttributes.indexCells
@@ -363,6 +367,11 @@ addModule
                     addToTheoryWith (Idx.termTopIndex . (.lhs)) newFunctionEquations currentFctEqs
                 simplifications =
                     addToTheoryWith (Idx.termTopIndex . (.lhs)) newSimplifications currentSimpls
+                existentialSimplifications =
+                    addToTheoryWith
+                        (Idx.termTopIndex . (.lhs))
+                        newExistentialSimplifications
+                        currentExistentialSimplifications
                 ceils =
                     addToTheoryWith (Idx.termTopIndex . (.lhs)) newCeils currentCeils
                 sorts =
@@ -374,6 +383,7 @@ addModule
                     , rewriteTheory
                     , functionEquations
                     , simplifications
+                    , existentialSimplifications
                     , ceils
                     }
       where
@@ -534,6 +544,8 @@ data AxiomResult
       FunctionAxiom (RewriteRule "Function")
     | -- | Simplification
       SimplificationAxiom (RewriteRule "Simplification")
+    | -- | Existential simplification
+      ExistentialSimplificationAxiom (RewriteRule "ExistentialSimplification")
     | -- | Ceil rule
       CeilAxiom (RewriteRule "Ceil")
 
@@ -554,6 +566,11 @@ retractSimplificationRule :: AxiomResult -> Maybe (RewriteRule "Simplification")
 retractSimplificationRule (SimplificationAxiom r) = Just r
 retractSimplificationRule _ = Nothing
 
+retractExistentialSimplificationRule ::
+    AxiomResult -> Maybe (RewriteRule "ExistentialSimplification")
+retractExistentialSimplificationRule (ExistentialSimplificationAxiom r) = Just r
+retractExistentialSimplificationRule _ = Nothing
+
 retractCeilRule :: AxiomResult -> Maybe (RewriteRule "Ceil")
 retractCeilRule (CeilAxiom r) = Just r
 retractCeilRule _ = Nothing

booster/unit-tests/Test/Booster/Fixture.hs

@@ -67,6 +67,7 @@ testDefinition =
         , rewriteTheory = Map.empty
         , functionEquations = Map.empty
         , simplifications = Map.empty
+        , existentialSimplifications = Map.empty
         , ceils = Map.empty
         }
   where

booster/unit-tests/Test/Booster/Pattern/PartialOrder.hs

@@ -0,0 +1,77 @@
+module Test.Booster.Pattern.PartialOrder (
+    test_transitiveClosure,
+) where
+
+import Data.Set qualified as Set
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Booster.Pattern.Base
+import Booster.Pattern.Bool
+import Booster.Pattern.PartialOrder
+
+test_transitiveClosure :: TestTree
+test_transitiveClosure =
+    testGroup
+        "<Int --- strict partial order"
+        [ test
+            "No new items"
+            ltIntSymbol
+            ( [ LtInt (var "A") (var "B")
+              , LtInt (var "C") (var "D")
+              ]
+            )
+            ( []
+            )
+        , test
+            "One new item"
+            ltIntSymbol
+            ( [ LtInt (var "A") (var "B")
+              , LtInt (var "B") (var "C")
+              ]
+            )
+            ( [ LtInt (var "A") (var "C")
+              ]
+            )
+        , test
+            "Two new items"
+            ltIntSymbol
+            ( [ LtInt (var "A") (var "B")
+              , LtInt (var "B") (var "C")
+              , LtInt (var "B") (var "D")
+              ]
+            )
+            ( [ LtInt (var "A") (var "C")
+              , LtInt (var "A") (var "D")
+              ]
+            )
+        , test
+            "Cycle, no new items"
+            ltIntSymbol
+            ( [ LtInt (var "A") (var "B")
+              , LtInt (var "B") (var "A")
+              ]
+            )
+            ( []
+            )
+        ]
+
+----------------------------------------
+-- Test fixture
+test :: String -> Symbol -> [Term] -> [Term] -> TestTree
+test name sym input expected =
+    testCase name $
+        transitiveClosure sym (Set.fromList $ map Predicate input)
+            @?= (Set.fromList $ map Predicate expected)
+
+ltIntSymbol :: Symbol
+ltIntSymbol =
+    case LtInt (var "DUMMY") (var "DUMMY") of
+        SymbolApplication ltInt _ _ -> ltInt
+        _ -> error "Impossible"
+
+someSort :: Sort
+someSort = SortApp "SomeSort" []
+
+var :: VarName -> Term
+var variableName = Var $ Variable{variableSort = someSort, variableName}