Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

NOT READY Compute syntactic transitive closure for select relational symbols #3940

Closed
wants to merge 2 commits into from
Closed
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Implement syntactic transitive closure routine
geo2a committed Jun 14, 2024
commit c81d5e811f209f04f111055b105c8d9d92316829
22 changes: 21 additions & 1 deletion booster/library/Booster/Pattern/Bool.hs
Original file line number Diff line number Diff line change
@@ -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
61 changes: 61 additions & 0 deletions booster/library/Booster/Pattern/PartialOrder.hs
Original file line number Diff line number Diff line change
@@ -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
4 changes: 4 additions & 0 deletions booster/library/Booster/Pattern/Util.hs
Original file line number Diff line number Diff line change
@@ -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"
-}
77 changes: 77 additions & 0 deletions booster/unit-tests/Test/Booster/Pattern/PartialOrder.hs
Original file line number Diff line number Diff line change
@@ -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}