Add RewriteRule "ExistentialSimplifications"

runtimeverification · Jun 14, 2024 · 2a3cbad · 2a3cbad
1 parent a96eba0
commit 2a3cbad
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 0 deletions.
diff --git a/booster/library/Booster/Definition/Base.hs b/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
         }
 

diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/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

diff --git a/booster/unit-tests/Test/Booster/Fixture.hs b/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