SMT.Translate.translatePattern: add fallback for translateApplication

kore/src/Kore/Step/SMT/Translate.hs

@@ -210,9 +210,7 @@ translatePredicateWith translateTerm predicate =
                 return $ SMT.int $ Builtin.Int.extractIntDomainValue
                     "while translating dv to SMT.int" dv
             ApplySymbolF app ->
-                (<|>)
-                    (translateApplication app)
-                    (translateUninterpreted SMT.tInt pat)
+                translateApplication (Just SMT.tInt) pat app
             DefinedF (Defined child) -> translateInt child
             _ -> empty
 
@@ -230,29 +228,39 @@ translatePredicateWith translateTerm predicate =
                 -- will fail to translate.
                 SMT.not <$> translateBool notChild
             ApplySymbolF app ->
-                (<|>)
-                    (translateApplication app)
-                    (translateUninterpreted SMT.tBool pat)
+                translateApplication (Just SMT.tBool) pat app
             DefinedF (Defined child) -> translateBool child
             _ -> empty
 
-    translateApplication :: Application Symbol p -> Translator m variable SExpr
+    translateApplication :: Maybe SExpr -> p -> Application Symbol p -> Translator m variable SExpr
     translateApplication
+        maybeSort
+        original
         Application
             { applicationSymbolOrAlias
             , applicationChildren
             }
-      = do
-        let translated = translateSymbol applicationSymbolOrAlias
-        sexpr <- maybe empty return translated
-        when (isNothing translated)
-            $ warnSymbolSMTRepresentation applicationSymbolOrAlias
-        children <- zipWithM translatePattern
-            applicationChildrenSorts
-            applicationChildren
-        return $ shortenSExpr (applySExpr sexpr children)
+      | isFunctionalPattern original =
+        translateInterpretedApplication
+        <|> translateUninterpreted'
+      | otherwise =
+        translateInterpretedApplication
       where
+        translateInterpretedApplication = do
+            let translated = translateSymbol applicationSymbolOrAlias
+            sexpr <- maybe warnAndDiscard return translated
+            children <- zipWithM translatePattern
+                applicationChildrenSorts
+                applicationChildren
+            return $ shortenSExpr (applySExpr sexpr children)
         applicationChildrenSorts = termLikeSort <$> applicationChildren
+        warnAndDiscard =
+            warnSymbolSMTRepresentation applicationSymbolOrAlias
+            >> empty
+        translateUninterpreted' = do
+            sort <- hoistMaybe maybeSort
+            translateUninterpreted sort original
+
 
     translatePredicateExists
         :: Exists Sort variable p -> Translator m variable SExpr
@@ -300,7 +308,8 @@ translatePredicateWith translateTerm predicate =
                     VariableF _ -> do
                         smtSort <- hoistMaybe $ translateSort sort
                         translateUninterpreted smtSort pat
-                    ApplySymbolF app -> translateApplication app
+                    ApplySymbolF app ->
+                        translateApplication (translateSort sort) pat app
                     DefinedF (Defined child) -> translatePattern sort child
                     _ -> empty
       where

kore/test/Test/Kore/Builtin/Definition.hs

@@ -262,6 +262,12 @@ dummyIntSymbol = unaryIntSymbol "f" & function
 dummyInt :: TermLike VariableName -> TermLike VariableName
 dummyInt x = mkApplySymbol dummyIntSymbol [x]
 
+dummyFunctionalIntSymbol :: Internal.Symbol
+dummyFunctionalIntSymbol = unaryIntSymbol "ff" & function & functional
+
+dummyFunctionalInt :: TermLike VariableName -> TermLike VariableName
+dummyFunctionalInt x = mkApplySymbol dummyFunctionalIntSymbol [x]
+
 addInt, subInt, mulInt, divInt, tdivInt, tmodInt
     :: TermLike VariableName
     -> TermLike VariableName

kore/test/Test/Kore/Equation/Application.hs

@@ -616,7 +616,7 @@ positive :: TestTerm -> TestPredicate
 positive u' =
     makeEqualsPredicate Mock.testSort
         (Mock.lessInt
-            (Mock.fTestInt u')  -- wrap the given term for sort agreement
+            (Mock.fTestFunctionalInt u')  -- wrap the given term for sort agreement
             (Mock.builtinInt 0)
         )
         (Mock.builtinBool False)

kore/test/Test/Kore/Step/MockSymbols.hs

@@ -175,6 +175,8 @@ fIntId :: Id
 fIntId = testId "fInt"
 fTestIntId :: Id
 fTestIntId = testId "fTestInt"
+fTestFunctionalIntId :: Id
+fTestFunctionalIntId = testId "fTestFunctionalInt"
 plain00Id :: Id
 plain00Id = testId "plain00"
 plain00Sort0Id :: Id
@@ -374,6 +376,10 @@ fIntSymbol = symbol fIntId [intSort] intSort & function
 fTestIntSymbol :: Symbol
 fTestIntSymbol = symbol fTestIntId [testSort] intSort & function
 
+fTestFunctionalIntSymbol :: Symbol
+fTestFunctionalIntSymbol =
+    symbol fTestFunctionalIntId [testSort] intSort & function & functional
+
 plain00Symbol :: Symbol
 plain00Symbol = symbol plain00Id [] testSort
 
@@ -840,6 +846,14 @@ fTestInt
     -> TermLike variable
 fTestInt arg = Internal.mkApplySymbol fTestIntSymbol [arg]
 
+fTestFunctionalInt
+    :: InternalVariable variable
+    => HasCallStack
+    => TermLike variable
+    -> TermLike variable
+fTestFunctionalInt arg =
+    Internal.mkApplySymbol fTestFunctionalIntSymbol [arg]
+
 fInt
     :: InternalVariable variable
     => HasCallStack
@@ -1499,21 +1513,6 @@ builtinZeroarySmtSort sExpr =
         , declaration = SMT.SortDeclaredIndirectly (SMT.AlreadyEncoded sExpr)
         }
 
-smtConstructor :: Id -> [Sort] -> Sort -> SMT.UnresolvedSymbol
-smtConstructor symbolId argumentSorts resultSort =
-    SMT.Symbol
-        { smtFromSortArgs = const (const (Just encodedId))
-        , declaration =
-            SMT.SymbolConstructor SMT.IndirectSymbolDeclaration
-                { name = encodableId
-                , sortDependencies =
-                    SMT.SortReference <$> resultSort : argumentSorts
-                }
-        }
-  where
-    encodableId = SMT.encodable symbolId
-    encodedId = SMT.encode encodableId
-
 smtBuiltinSymbol
     :: Text -> [Sort] -> Sort -> SMT.UnresolvedSymbol
 smtBuiltinSymbol builtin argumentSorts resultSort =
@@ -1553,18 +1552,9 @@ smtUnresolvedDeclarations = SMT.Declarations
         , (boolSortId, builtinZeroarySmtSort SMT.tBool)
         ]
     , symbols = Map.fromList
-        [ ( aSort0Id, smtConstructor aSort0Id [] testSort1)
-        , ( aSort1Id, smtConstructor aSort1Id [] testSort1)
-        , ( aSubsortId, smtConstructor aSubsortId [] subSort)
-        , ( aSubOthersortId, smtConstructor aSubOthersortId [] subSubsort)
-        , ( aSubSubsortId, smtConstructor aSubSubsortId [] subSubsort)
-        , ( aTopSortId, smtConstructor aTopSortId [] topSort)
-        , ( aOtherSortId, smtConstructor aOtherSortId [] otherSort)
-        , ( bSort0Id, smtConstructor bSort0Id [] testSort0)
-        , ( lessIntId, smtBuiltinSymbol "<" [intSort, intSort] boolSort)
+        [ ( lessIntId, smtBuiltinSymbol "<" [intSort, intSort] boolSort)
         , ( greaterEqIntId, smtBuiltinSymbol ">=" [intSort, intSort] boolSort)
         , ( tdivIntId, smtBuiltinSymbol "div" [intSort, intSort] intSort)
-        , ( sigmaId, smtConstructor sigmaId [testSort, testSort] testSort)
         ]
     }
 

kore/test/Test/Kore/Step/Rule/Combine.hs

@@ -53,9 +53,6 @@ import Kore.Step.RulePattern
 import qualified Kore.Step.RulePattern as RulePattern
     ( RulePattern (..)
     )
-import Kore.Step.Simplification.Data
-    ( runSimplifier
-    )
 import Kore.Syntax.Variable
 import Kore.Unparser
     ( unparseToString
@@ -65,9 +62,9 @@ import Test.Kore
     ( testId
     )
 import qualified Test.Kore.Step.MockSymbols as Mock
-import Test.SMT
-    ( runNoSMT
-    , runSMT
+import Test.Kore.Step.Simplification
+    ( runSimplifier
+    , runSimplifierSMT
     )
 import Test.Tasty.HUnit.Ext
 
@@ -235,13 +232,13 @@ test_combineRules =
     [ testCase "One rule" $ do
         let expected = [Mock.a `rewritesTo` Mock.cf]
 
-        actual <- runMergeRulesNoSMT [ Mock.a `rewritesTo` Mock.cf ]
+        actual <- runMergeRules [ Mock.a `rewritesTo` Mock.cf ]
 
         assertEqual "" expected actual
     , testCase "Two rules" $ do
         let expected = [Mock.a `rewritesTo` Mock.cf]
 
-        actual <- runMergeRulesNoSMT
+        actual <- runMergeRules
             [ Mock.a `rewritesTo` Mock.b
             , Mock.b `rewritesTo` Mock.cf
             ]
@@ -256,7 +253,7 @@ test_combineRules =
                     `rewritesTo` Pair (Mock.cg, makeTruePredicate_)
                 ]
 
-        actual <- runMergeRules
+        actual <- runMergeRulesSMT
             [ Mock.a `rewritesTo` Mock.functionalConstr10 Mock.cf
             , Mock.functionalConstr10 Mock.b `rewritesTo` Mock.cg
             ]
@@ -268,7 +265,7 @@ test_combineRules =
                     `rewritesTo` y
                 ]
 
-        actual <- runMergeRulesNoSMT
+        actual <- runMergeRules
             [ Mock.functionalConstr10 x `rewritesTo` x
             , Mock.functionalConstr11 y `rewritesTo` y
             ]
@@ -291,7 +288,7 @@ test_combineRules =
                     `rewritesTo` Pair (y, makeTruePredicate_)
                 ]
 
-        actual <- runMergeRules
+        actual <- runMergeRulesSMT
             [   Pair
                     ( Mock.functionalConstr10 x
                     , makeEqualsPredicate_ (Mock.f x) (Mock.g x)
@@ -319,7 +316,7 @@ test_combineRules =
                     `rewritesTo` x0
                 ]
 
-        actual <- runMergeRulesNoSMT
+        actual <- runMergeRules
             [ Mock.functionalConstr10 x `rewritesTo` x
             , Mock.functionalConstr11 x `rewritesTo` x
             ]
@@ -342,7 +339,7 @@ test_combineRulesGrouped =
     , testCase "Two rules" $ do
         let expected = [Mock.a `rewritesTo` Mock.cf]
 
-        actual <- runMergeRulesNoSMT
+        actual <- runMergeRules
             [ Mock.a `rewritesTo` Mock.b
             , Mock.b `rewritesTo` Mock.cf
             ]
@@ -355,7 +352,7 @@ test_combineRulesGrouped =
                     `rewritesTo` z
                 ]
 
-        actual <- runMergeRulesNoSMT
+        actual <- runMergeRules
             [ Mock.functionalConstr10 x `rewritesTo` x
             , Mock.functionalConstr11 y `rewritesTo` y
             , Mock.functionalConstr12 z `rewritesTo` z
@@ -380,29 +377,26 @@ applyAlias name aliasRight =
             }
         []
 
-runMergeRulesNoSMT
+runMergeRules
     :: [RewriteRule VariableName]
     -> IO [RewriteRule VariableName]
-runMergeRulesNoSMT (rule : rules) =
-    runNoSMT
-    $ runSimplifier Mock.env
+runMergeRules (rule : rules) =
+    runSimplifier Mock.env
     $ mergeRules (rule :| rules)
-runMergeRulesNoSMT [] = error "Unexpected empty list of rules."
+runMergeRules [] = error "Unexpected empty list of rules."
 
-runMergeRules
+runMergeRulesSMT
     :: [RewriteRule VariableName]
     -> IO [RewriteRule VariableName]
-runMergeRules (rule : rules) =
-    runSMT (pure ())
-    $ runSimplifier Mock.env
+runMergeRulesSMT (rule : rules) =
+    runSimplifierSMT Mock.env
     $ mergeRules (rule :| rules)
-runMergeRules [] = error "Unexpected empty list of rules."
+runMergeRulesSMT [] = error "Unexpected empty list of rules."
 
 runMergeRulesGrouped
     :: [RewriteRule VariableName]
     -> IO [RewriteRule VariableName]
 runMergeRulesGrouped (rule : rules) =
-    runNoSMT
-    $ runSimplifier Mock.env
+    runSimplifier Mock.env
     $ mergeRulesConsecutiveBatches 2 (rule :| rules)
 runMergeRulesGrouped [] = error "Unexpected empty list of rules."