Implement syntactic transitive closure routine

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/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}