Skip to content

Commit 8efd16c

Browse files
ana-pantilieana-pantilie
authored
SMT.Translate.translatePattern: add fallback for translateApplication (#2261)
1 parent 7579c77 commit 8efd16c

File tree

9 files changed

+123
-117
lines changed

9 files changed

+123
-117
lines changed

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

Lines changed: 26 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -210,9 +210,7 @@ translatePredicateWith translateTerm predicate =
210210
return $ SMT.int $ Builtin.Int.extractIntDomainValue
211211
"while translating dv to SMT.int" dv
212212
ApplySymbolF app ->
213-
(<|>)
214-
(translateApplication app)
215-
(translateUninterpreted SMT.tInt pat)
213+
translateApplication (Just SMT.tInt) pat app
216214
DefinedF (Defined child) -> translateInt child
217215
_ -> empty
218216

@@ -230,29 +228,39 @@ translatePredicateWith translateTerm predicate =
230228
-- will fail to translate.
231229
SMT.not <$> translateBool notChild
232230
ApplySymbolF app ->
233-
(<|>)
234-
(translateApplication app)
235-
(translateUninterpreted SMT.tBool pat)
231+
translateApplication (Just SMT.tBool) pat app
236232
DefinedF (Defined child) -> translateBool child
237233
_ -> empty
238234

239-
translateApplication :: Application Symbol p -> Translator m variable SExpr
235+
translateApplication :: Maybe SExpr -> p -> Application Symbol p -> Translator m variable SExpr
240236
translateApplication
237+
maybeSort
238+
original
241239
Application
242240
{ applicationSymbolOrAlias
243241
, applicationChildren
244242
}
245-
= do
246-
let translated = translateSymbol applicationSymbolOrAlias
247-
sexpr <- maybe empty return translated
248-
when (isNothing translated)
249-
$ warnSymbolSMTRepresentation applicationSymbolOrAlias
250-
children <- zipWithM translatePattern
251-
applicationChildrenSorts
252-
applicationChildren
253-
return $ shortenSExpr (applySExpr sexpr children)
243+
| isFunctionalPattern original =
244+
translateInterpretedApplication
245+
<|> translateUninterpreted'
246+
| otherwise =
247+
translateInterpretedApplication
254248
where
249+
translateInterpretedApplication = do
250+
let translated = translateSymbol applicationSymbolOrAlias
251+
sexpr <- maybe warnAndDiscard return translated
252+
children <- zipWithM translatePattern
253+
applicationChildrenSorts
254+
applicationChildren
255+
return $ shortenSExpr (applySExpr sexpr children)
255256
applicationChildrenSorts = termLikeSort <$> applicationChildren
257+
warnAndDiscard =
258+
warnSymbolSMTRepresentation applicationSymbolOrAlias
259+
>> empty
260+
translateUninterpreted' = do
261+
sort <- hoistMaybe maybeSort
262+
translateUninterpreted sort original
263+
256264

257265
translatePredicateExists
258266
:: Exists Sort variable p -> Translator m variable SExpr
@@ -300,7 +308,8 @@ translatePredicateWith translateTerm predicate =
300308
VariableF _ -> do
301309
smtSort <- hoistMaybe $ translateSort sort
302310
translateUninterpreted smtSort pat
303-
ApplySymbolF app -> translateApplication app
311+
ApplySymbolF app ->
312+
translateApplication (translateSort sort) pat app
304313
DefinedF (Defined child) -> translatePattern sort child
305314
_ -> empty
306315
where

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -262,6 +262,12 @@ dummyIntSymbol = unaryIntSymbol "f" & function
262262
dummyInt :: TermLike VariableName -> TermLike VariableName
263263
dummyInt x = mkApplySymbol dummyIntSymbol [x]
264264

265+
dummyFunctionalIntSymbol :: Internal.Symbol
266+
dummyFunctionalIntSymbol = unaryIntSymbol "ff" & function & functional
267+
268+
dummyFunctionalInt :: TermLike VariableName -> TermLike VariableName
269+
dummyFunctionalInt x = mkApplySymbol dummyFunctionalIntSymbol [x]
270+
265271
addInt, subInt, mulInt, divInt, tdivInt, tmodInt
266272
:: TermLike VariableName
267273
-> TermLike VariableName

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -616,7 +616,7 @@ positive :: TestTerm -> TestPredicate
616616
positive u' =
617617
makeEqualsPredicate Mock.testSort
618618
(Mock.lessInt
619-
(Mock.fTestInt u') -- wrap the given term for sort agreement
619+
(Mock.fTestFunctionalInt u') -- wrap the given term for sort agreement
620620
(Mock.builtinInt 0)
621621
)
622622
(Mock.builtinBool False)

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

Lines changed: 15 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -175,6 +175,8 @@ fIntId :: Id
175175
fIntId = testId "fInt"
176176
fTestIntId :: Id
177177
fTestIntId = testId "fTestInt"
178+
fTestFunctionalIntId :: Id
179+
fTestFunctionalIntId = testId "fTestFunctionalInt"
178180
plain00Id :: Id
179181
plain00Id = testId "plain00"
180182
plain00Sort0Id :: Id
@@ -374,6 +376,10 @@ fIntSymbol = symbol fIntId [intSort] intSort & function
374376
fTestIntSymbol :: Symbol
375377
fTestIntSymbol = symbol fTestIntId [testSort] intSort & function
376378

379+
fTestFunctionalIntSymbol :: Symbol
380+
fTestFunctionalIntSymbol =
381+
symbol fTestFunctionalIntId [testSort] intSort & function & functional
382+
377383
plain00Symbol :: Symbol
378384
plain00Symbol = symbol plain00Id [] testSort
379385

@@ -840,6 +846,14 @@ fTestInt
840846
-> TermLike variable
841847
fTestInt arg = Internal.mkApplySymbol fTestIntSymbol [arg]
842848

849+
fTestFunctionalInt
850+
:: InternalVariable variable
851+
=> HasCallStack
852+
=> TermLike variable
853+
-> TermLike variable
854+
fTestFunctionalInt arg =
855+
Internal.mkApplySymbol fTestFunctionalIntSymbol [arg]
856+
843857
fInt
844858
:: InternalVariable variable
845859
=> HasCallStack
@@ -1499,21 +1513,6 @@ builtinZeroarySmtSort sExpr =
14991513
, declaration = SMT.SortDeclaredIndirectly (SMT.AlreadyEncoded sExpr)
15001514
}
15011515

1502-
smtConstructor :: Id -> [Sort] -> Sort -> SMT.UnresolvedSymbol
1503-
smtConstructor symbolId argumentSorts resultSort =
1504-
SMT.Symbol
1505-
{ smtFromSortArgs = const (const (Just encodedId))
1506-
, declaration =
1507-
SMT.SymbolConstructor SMT.IndirectSymbolDeclaration
1508-
{ name = encodableId
1509-
, sortDependencies =
1510-
SMT.SortReference <$> resultSort : argumentSorts
1511-
}
1512-
}
1513-
where
1514-
encodableId = SMT.encodable symbolId
1515-
encodedId = SMT.encode encodableId
1516-
15171516
smtBuiltinSymbol
15181517
:: Text -> [Sort] -> Sort -> SMT.UnresolvedSymbol
15191518
smtBuiltinSymbol builtin argumentSorts resultSort =
@@ -1553,18 +1552,9 @@ smtUnresolvedDeclarations = SMT.Declarations
15531552
, (boolSortId, builtinZeroarySmtSort SMT.tBool)
15541553
]
15551554
, symbols = Map.fromList
1556-
[ ( aSort0Id, smtConstructor aSort0Id [] testSort1)
1557-
, ( aSort1Id, smtConstructor aSort1Id [] testSort1)
1558-
, ( aSubsortId, smtConstructor aSubsortId [] subSort)
1559-
, ( aSubOthersortId, smtConstructor aSubOthersortId [] subSubsort)
1560-
, ( aSubSubsortId, smtConstructor aSubSubsortId [] subSubsort)
1561-
, ( aTopSortId, smtConstructor aTopSortId [] topSort)
1562-
, ( aOtherSortId, smtConstructor aOtherSortId [] otherSort)
1563-
, ( bSort0Id, smtConstructor bSort0Id [] testSort0)
1564-
, ( lessIntId, smtBuiltinSymbol "<" [intSort, intSort] boolSort)
1555+
[ ( lessIntId, smtBuiltinSymbol "<" [intSort, intSort] boolSort)
15651556
, ( greaterEqIntId, smtBuiltinSymbol ">=" [intSort, intSort] boolSort)
15661557
, ( tdivIntId, smtBuiltinSymbol "div" [intSort, intSort] intSort)
1567-
, ( sigmaId, smtConstructor sigmaId [testSort, testSort] testSort)
15681558
]
15691559
}
15701560

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

Lines changed: 20 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -53,9 +53,6 @@ import Kore.Step.RulePattern
5353
import qualified Kore.Step.RulePattern as RulePattern
5454
( RulePattern (..)
5555
)
56-
import Kore.Step.Simplification.Data
57-
( runSimplifier
58-
)
5956
import Kore.Syntax.Variable
6057
import Kore.Unparser
6158
( unparseToString
@@ -65,9 +62,9 @@ import Test.Kore
6562
( testId
6663
)
6764
import qualified Test.Kore.Step.MockSymbols as Mock
68-
import Test.SMT
69-
( runNoSMT
70-
, runSMT
65+
import Test.Kore.Step.Simplification
66+
( runSimplifier
67+
, runSimplifierSMT
7168
)
7269
import Test.Tasty.HUnit.Ext
7370

@@ -235,13 +232,13 @@ test_combineRules =
235232
[ testCase "One rule" $ do
236233
let expected = [Mock.a `rewritesTo` Mock.cf]
237234

238-
actual <- runMergeRulesNoSMT [ Mock.a `rewritesTo` Mock.cf ]
235+
actual <- runMergeRules [ Mock.a `rewritesTo` Mock.cf ]
239236

240237
assertEqual "" expected actual
241238
, testCase "Two rules" $ do
242239
let expected = [Mock.a `rewritesTo` Mock.cf]
243240

244-
actual <- runMergeRulesNoSMT
241+
actual <- runMergeRules
245242
[ Mock.a `rewritesTo` Mock.b
246243
, Mock.b `rewritesTo` Mock.cf
247244
]
@@ -256,7 +253,7 @@ test_combineRules =
256253
`rewritesTo` Pair (Mock.cg, makeTruePredicate_)
257254
]
258255

259-
actual <- runMergeRules
256+
actual <- runMergeRulesSMT
260257
[ Mock.a `rewritesTo` Mock.functionalConstr10 Mock.cf
261258
, Mock.functionalConstr10 Mock.b `rewritesTo` Mock.cg
262259
]
@@ -268,7 +265,7 @@ test_combineRules =
268265
`rewritesTo` y
269266
]
270267

271-
actual <- runMergeRulesNoSMT
268+
actual <- runMergeRules
272269
[ Mock.functionalConstr10 x `rewritesTo` x
273270
, Mock.functionalConstr11 y `rewritesTo` y
274271
]
@@ -291,7 +288,7 @@ test_combineRules =
291288
`rewritesTo` Pair (y, makeTruePredicate_)
292289
]
293290

294-
actual <- runMergeRules
291+
actual <- runMergeRulesSMT
295292
[ Pair
296293
( Mock.functionalConstr10 x
297294
, makeEqualsPredicate_ (Mock.f x) (Mock.g x)
@@ -319,7 +316,7 @@ test_combineRules =
319316
`rewritesTo` x0
320317
]
321318

322-
actual <- runMergeRulesNoSMT
319+
actual <- runMergeRules
323320
[ Mock.functionalConstr10 x `rewritesTo` x
324321
, Mock.functionalConstr11 x `rewritesTo` x
325322
]
@@ -342,7 +339,7 @@ test_combineRulesGrouped =
342339
, testCase "Two rules" $ do
343340
let expected = [Mock.a `rewritesTo` Mock.cf]
344341

345-
actual <- runMergeRulesNoSMT
342+
actual <- runMergeRules
346343
[ Mock.a `rewritesTo` Mock.b
347344
, Mock.b `rewritesTo` Mock.cf
348345
]
@@ -355,7 +352,7 @@ test_combineRulesGrouped =
355352
`rewritesTo` z
356353
]
357354

358-
actual <- runMergeRulesNoSMT
355+
actual <- runMergeRules
359356
[ Mock.functionalConstr10 x `rewritesTo` x
360357
, Mock.functionalConstr11 y `rewritesTo` y
361358
, Mock.functionalConstr12 z `rewritesTo` z
@@ -380,29 +377,26 @@ applyAlias name aliasRight =
380377
}
381378
[]
382379

383-
runMergeRulesNoSMT
380+
runMergeRules
384381
:: [RewriteRule VariableName]
385382
-> IO [RewriteRule VariableName]
386-
runMergeRulesNoSMT (rule : rules) =
387-
runNoSMT
388-
$ runSimplifier Mock.env
383+
runMergeRules (rule : rules) =
384+
runSimplifier Mock.env
389385
$ mergeRules (rule :| rules)
390-
runMergeRulesNoSMT [] = error "Unexpected empty list of rules."
386+
runMergeRules [] = error "Unexpected empty list of rules."
391387

392-
runMergeRules
388+
runMergeRulesSMT
393389
:: [RewriteRule VariableName]
394390
-> IO [RewriteRule VariableName]
395-
runMergeRules (rule : rules) =
396-
runSMT (pure ())
397-
$ runSimplifier Mock.env
391+
runMergeRulesSMT (rule : rules) =
392+
runSimplifierSMT Mock.env
398393
$ mergeRules (rule :| rules)
399-
runMergeRules [] = error "Unexpected empty list of rules."
394+
runMergeRulesSMT [] = error "Unexpected empty list of rules."
400395

401396
runMergeRulesGrouped
402397
:: [RewriteRule VariableName]
403398
-> IO [RewriteRule VariableName]
404399
runMergeRulesGrouped (rule : rules) =
405-
runNoSMT
406-
$ runSimplifier Mock.env
400+
runSimplifier Mock.env
407401
$ mergeRulesConsecutiveBatches 2 (rule :| rules)
408402
runMergeRulesGrouped [] = error "Unexpected empty list of rules."

0 commit comments

Comments
 (0)