Existential matching of simplification side conditions

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/ApplyEquations.hs

@@ -26,6 +26,7 @@ module Booster.Pattern.ApplyEquations (
     evaluateConstraints,
 ) where
 
+import Booster.Pattern.Existential (instantiateExistentialsMany)
 import Control.Exception qualified as Exception (throw)
 import Control.Monad
 import Control.Monad.Extra (fromMaybeM, whenJust)
@@ -39,7 +40,7 @@ import Data.Bifunctor (bimap)
 import Data.ByteString.Char8 qualified as BS
 import Data.Coerce (coerce)
 import Data.Data (Data, Proxy)
-import Data.Foldable (toList, traverse_)
+import Data.Foldable (foldl', toList, traverse_)
 import Data.List (foldl1', intersperse, partition)
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map (Map)
@@ -726,6 +727,7 @@ applyEquation term rule =
         getPrettyModifiers >>= \case
             ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do
                 -- ensured by internalisation: no existentials in equations
+                -- TODO allow existentials, but only in the requires clause
                 unless (null rule.existentials) $ do
                     withContext CtxAbort $
                         logMessage ("Equation with existentials" :: Text)
@@ -804,7 +806,55 @@ applyEquation term rule =
                         -- If the required condition is _syntactically_ present in
                         -- the prior (known constraints), we don't check it.
                         knownPredicates <- (.predicates) <$> lift getState
-                        toCheck <- lift $ filterOutKnownConstraints knownPredicates required
+
+                        let partitionExistentialRequires :: [Predicate] -> ([Predicate], [Predicate])
+                            partitionExistentialRequires = foldl' decide ([], [])
+                              where
+                                decide (hasEx, noHasEx) p
+                                    | hasExistentials p = (p : hasEx, noHasEx)
+                                    | otherwise = (hasEx, p : noHasEx)
+
+                            hasExistentials :: Predicate -> Bool
+                            hasExistentials (Predicate t) = any (isExVar . (.variableName)) (freeVariables t)
+
+                            listExistentials :: Predicate -> Set VarName
+                            listExistentials (Predicate t) = Set.filter isExVar . Set.map (.variableName) . freeVariables $ t
+
+                        -- If we get an equation with existentials in the requires clause, we must have them all instantiated
+                        let (predicateWithEx, predicatesWithNoEx) = partitionExistentialRequires required
+                            instantiatedExistentialPredicates = instantiateExistentialsMany knownPredicates predicateWithEx
+
+                        -- detect if any existentials still remain
+                        when (any hasExistentials instantiatedExistentialPredicates) $ do
+                            -- what to do here? Abort equation or simply throw away the clauses with existentials?
+                            -- Let's abort for now.
+                            let remainingExistentials =
+                                    Set.toList . Set.map Text.decodeLatin1 . Set.unions . map listExistentials $
+                                        instantiatedExistentialPredicates
+
+                            withContext CtxAbort $
+                                logMessage $
+                                    "Could not instantiate existentials: " <> (Text.intercalate "," remainingExistentials)
+
+                        -- all existentials are instantiated: assemble the requires clause again
+                        let requiredWithInstantiatedExistentials = predicatesWithNoEx <> instantiatedExistentialPredicates
+
+                        -- TODO these logs need to either go or be assigned a more specific context
+                        withContext CtxConstraint . withContext CtxDetail $ do
+                            logMessage $
+                                renderOneLineText $
+                                    "Requires clause after substitution:"
+                                        <+> hsep (intersperse "," $ map (pretty' @mods) required)
+                            logMessage $
+                                renderOneLineText $
+                                    "Known predicates:"
+                                        <+> hsep (intersperse "," $ map (pretty' @mods) (Set.toList knownPredicates))
+                            logMessage $
+                                renderOneLineText $
+                                    "Requires clause predicate after instantiating existential:"
+                                        <+> hsep (intersperse "," $ map (pretty' @mods) requiredWithInstantiatedExistentials)
+
+                        toCheck <- lift $ filterOutKnownConstraints knownPredicates requiredWithInstantiatedExistentials
 
                         -- check the filtered requires clause conditions
                         unclearConditions <-

booster/library/Booster/Pattern/Bool.hs

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

booster/library/Booster/Pattern/Existential.hs

@@ -0,0 +1,74 @@
+{- |
+Copyright   : (c) Runtime Verification, 2024
+License     : BSD-3-Clause
+-}
+module Booster.Pattern.Existential (matchExistential, instantiateExistentials, instantiateExistentialsMany) where
+
+import Control.Monad (guard, when)
+import Control.Monad.Trans.Class (lift)
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.State.Strict
+import Data.Coerce (coerce)
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
+import Data.Maybe (fromJust)
+import Data.Set (Set)
+import Data.Set qualified as Set
+
+import Booster.Pattern.Base
+import Booster.Pattern.Util
+
+{- | Given a set of @known@ predicates, which must not contains any existential variables,
+     attempt to instantiate the existential in the @target@ predicate using the following method:
+     * generate a list of candidate substitutions by matching with every known predicate individually
+     * collapse all substitutions into one, resolving any conflicts left-to-right, i.e. if a variable
+       is bound, it is /not/ updated
+-}
+instantiateExistentials :: Set Predicate -> Predicate -> (Predicate, Substitution)
+instantiateExistentials known target@(Predicate targetTerm) =
+    let candidates = map (matchExistential target) (Set.toList known)
+        combinedSubst = Map.unions candidates
+     in (Predicate $ substituteInTerm combinedSubst targetTerm, combinedSubst)
+
+type Substitution = Map Variable Term
+
+{- | Apply @instantiateExistentials@ to a list of predicates:
+     - apply to the head to instantiate existentials and get the substitution
+     - apply the substitution to the tail and call recursively
+-}
+instantiateExistentialsMany :: Set Predicate -> [Predicate] -> [Predicate]
+instantiateExistentialsMany known = reverse . go []
+  where
+    go :: [Predicate] -> [Predicate] -> [Predicate]
+    go acc = \case
+        [] -> acc
+        (p : ps) ->
+            let (p', subst) = instantiateExistentials known p
+             in go (p' : acc) (map (coerce . substituteInTerm subst . coerce) ps)
+
+{- | Given a @target@ predicate, which may contain existential variables,
+  and a @known@ predicate, which must not, attempt to instantiate the first with the second
+-}
+matchExistential :: Predicate -> Predicate -> Substitution
+matchExistential target known =
+    flip execState Map.empty . runMaybeT $ matchExistentialImpl target known
+
+matchExistentialImpl :: Predicate -> Predicate -> MaybeT (State Substitution) ()
+matchExistentialImpl (Predicate target) (Predicate known) =
+    case (target, known) of
+        (SymbolApplication symbol1 _ [a, b], SymbolApplication symbol2 _ [c, d]) -> do
+            guard (symbol1 == symbol2)
+            tryBindExVar a c
+            tryBindExVar b d
+        _ -> fail "Not a symbol application"
+  where
+    tryBindExVar :: Term -> Term -> MaybeT (State Substitution) ()
+    tryBindExVar variable term = do
+        when (isExistentialVariable variable) $ do
+            let variableVar = fromJust . retractVariable $ variable
+            lift $ modify (Map.insert variableVar term)
+
+isExistentialVariable :: Term -> Bool
+isExistentialVariable = \case
+    Var v -> isExVar v.variableName
+    _ -> False

booster/library/Booster/Pattern/Util.hs

@@ -13,6 +13,7 @@ module Booster.Pattern.Util (
     modifyVarName,
     modifyVarNameConcreteness,
     freeVariables,
+    retractVariable,
     isConstructorSymbol,
     isFunctionSymbol,
     isDefinedSymbol,
@@ -30,6 +31,7 @@ module Booster.Pattern.Util (
     cellVariableStats,
     stripMarker,
     markAsExVar,
+    isExVar,
     markAsRuleVar,
     incrementNameCounter,
 ) where
@@ -125,6 +127,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"
 -}
@@ -200,6 +205,11 @@ modifyVarNameConcreteness f = \case
 freeVariables :: Term -> Set Variable
 freeVariables (Term attributes _) = attributes.variables
 
+retractVariable :: Term -> Maybe Variable
+retractVariable = \case
+    (Var v) -> Just v
+    _ -> Nothing
+
 isConcrete :: Term -> Bool
 isConcrete = Set.null . freeVariables