Skip to content

Commit 9247a96

Browse files
dopamanegithub-actionsttuegelrv-jenkins
authored
Prune unsatisfiable state with unifyStringEq (#2647)
* add unifyStringEq to maybeTermAnd * add unifyIntEq to maybeTermAnd * drafting And term simplification ==String test * Format with fourmolu * revert incorrect test draft * modify test_unifyStringEq * Format with fourmolu * add unifyIntEq integration test * Format with fourmolu * Format with fourmolu * trigger tests with empty commit * Add failing test for \and(_, ==String(_, _)) * draft cleanup of maybeTermEquals and maybeTermAnd with respect to unifyStringEq * add failing test for \and(_, ==Int(_,_)) * save bool term then re-add after scatter * Format with fourmolu * add in predicate test, fix unifyStringEq unit tests * add boolTerm back after scatter for unifyIntEq, update unifyIntEq tests * matchUnifyStringEq and matchUnifyEq handle matching their arguments both ways Co-authored-by: Thomas Tuegel <[email protected]> * matchUnifyKequalsEq handles matching arguments both ways * save only bool term in UnifyIntEq data type, cleanup unifyIntEq function body * save only bool term in UnifyStringEq data type, cleanup unifyStringEq function body * unifyStringEq use InternalBool * unifyIntEq use InternalBool * unifyKequalsEq use InternalBool * update KEqual and AndTerms simplification tests Co-authored-by: github-actions <[email protected]> Co-authored-by: Thomas Tuegel <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent c0d7174 commit 9247a96

File tree

8 files changed

+174
-46
lines changed

8 files changed

+174
-46
lines changed

‎kore/src/Kore/Builtin/Int.hs

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,10 @@ import Kore.Builtin.EqTerm
110110
import Kore.Builtin.Int.Int
111111
import qualified Kore.Error
112112
import qualified Kore.Internal.Condition as Condition
113+
import Kore.Internal.Conditional (
114+
term,
115+
)
116+
import Kore.Internal.InternalBool
113117
import Kore.Internal.InternalInt
114118
import qualified Kore.Internal.MultiOr as MultiOr
115119
import qualified Kore.Internal.OrPattern as OrPattern
@@ -477,7 +481,7 @@ unifyInt term1 term2 unifyData =
477481

478482
data UnifyIntEq = UnifyIntEq
479483
{ eqTerm :: !(EqTerm (TermLike RewritingVariableName))
480-
, value :: !Bool
484+
, internalBool :: !InternalBool
481485
}
482486

483487
{- | Matches
@@ -492,8 +496,8 @@ matchUnifyIntEq ::
492496
matchUnifyIntEq first second
493497
| Just eqTerm <- matchIntEqual first
494498
, isFunctionPattern first
495-
, Just value <- Bool.matchBool second =
496-
Just UnifyIntEq{eqTerm, value}
499+
, InternalBool_ internalBool <- second =
500+
Just UnifyIntEq{eqTerm, internalBool}
497501
| otherwise = Nothing
498502
{-# INLINE matchUnifyIntEq #-}
499503

@@ -510,11 +514,15 @@ unifyIntEq ::
510514
unifier (Pattern RewritingVariableName)
511515
unifyIntEq unifyChildren (NotSimplifier notSimplifier) unifyData =
512516
do
513-
solution <- unifyChildren operand1 operand2 & OrPattern.gather
514-
let solution' = MultiOr.map eraseTerm solution
515-
(if value then pure else notSimplifier SideCondition.top) solution'
516-
>>= Unify.scatter
517+
solution <- OrPattern.gather $ unifyChildren operand1 operand2
518+
solution' <-
519+
MultiOr.map eraseTerm solution
520+
& if internalBoolValue internalBool
521+
then pure
522+
else notSimplifier SideCondition.top
523+
scattered <- Unify.scatter solution'
524+
return scattered{term = mkInternalBool internalBool}
517525
where
518-
UnifyIntEq{eqTerm, value} = unifyData
526+
UnifyIntEq{eqTerm, internalBool} = unifyData
519527
EqTerm{operand1, operand2} = eqTerm
520528
eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm

‎kore/src/Kore/Builtin/KEqual.hs

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,10 @@ import qualified Kore.Builtin.Builtin as Builtin
5353
import Kore.Builtin.EqTerm
5454
import qualified Kore.Error
5555
import qualified Kore.Internal.Condition as Condition
56+
import Kore.Internal.Conditional (
57+
term,
58+
)
59+
import Kore.Internal.InternalBool
5660
import qualified Kore.Internal.MultiOr as MultiOr
5761
import qualified Kore.Internal.OrPattern as OrPattern
5862
import Kore.Internal.Pattern (
@@ -224,7 +228,7 @@ matchKequalEq =
224228

225229
data UnifyKequalsEq = UnifyKequalsEq
226230
{ eqTerm :: !(EqTerm (TermLike RewritingVariableName))
227-
, value :: !Bool
231+
, internalBool :: !InternalBool
228232
}
229233

230234
{- | Matches two terms when second is a bool term
@@ -251,8 +255,8 @@ matchUnifyKequalsEq ::
251255
matchUnifyKequalsEq first second
252256
| Just eqTerm <- matchKequalEq first
253257
, isFunctionPattern first
254-
, Just value <- Bool.matchBool second =
255-
Just UnifyKequalsEq{eqTerm, value}
258+
, InternalBool_ internalBool <- second =
259+
Just UnifyKequalsEq{eqTerm, internalBool}
256260
| otherwise = Nothing
257261
{-# INLINE matchUnifyKequalsEq #-}
258262

@@ -265,12 +269,16 @@ unifyKequalsEq ::
265269
unifier (Pattern RewritingVariableName)
266270
unifyKequalsEq unifyChildren (NotSimplifier notSimplifier) unifyData =
267271
do
268-
solution <- unifyChildren operand1 operand2 & OrPattern.gather
269-
let solution' = MultiOr.map eraseTerm solution
270-
(if value then pure else notSimplifier SideCondition.top) solution'
271-
>>= Unify.scatter
272+
solution <- OrPattern.gather $ unifyChildren operand1 operand2
273+
solution' <-
274+
MultiOr.map eraseTerm solution
275+
& if internalBoolValue internalBool
276+
then pure
277+
else notSimplifier SideCondition.top
278+
scattered <- Unify.scatter solution'
279+
return scattered{term = mkInternalBool internalBool}
272280
where
273-
UnifyKequalsEq{eqTerm, value} = unifyData
281+
UnifyKequalsEq{eqTerm, internalBool} = unifyData
274282
EqTerm{operand1, operand2} = eqTerm
275283
eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm
276284

‎kore/src/Kore/Builtin/String.hs

Lines changed: 40 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ module Kore.Builtin.String (
2727
unifyString,
2828
unifyStringEq,
2929
matchString,
30+
matchUnifyStringEq,
3031

3132
-- * keys
3233
ltKey,
@@ -77,11 +78,18 @@ import qualified Kore.Error
7778
import Kore.Internal.ApplicationSorts (
7879
applicationSortsResult,
7980
)
81+
import Kore.Internal.Conditional (
82+
term,
83+
)
84+
import Kore.Internal.InternalBool
8085
import Kore.Internal.InternalString
86+
import qualified Kore.Internal.MultiOr as MultiOr
87+
import qualified Kore.Internal.OrPattern as OrPattern
8188
import Kore.Internal.Pattern (
8289
Pattern,
8390
)
8491
import qualified Kore.Internal.Pattern as Pattern
92+
import qualified Kore.Internal.SideCondition as SideCondition
8593
import Kore.Internal.Symbol (
8694
symbolHook,
8795
)
@@ -521,6 +529,23 @@ unifyString term1 term2 unifyData =
521529
debugUnifyBottomAndReturnBottom "distinct strings" term1 term2
522530
UnifyString{string1, string2} = unifyData
523531

532+
data UnifyStringEq = UnifyStringEq
533+
{ eqTerm :: !(EqTerm (TermLike RewritingVariableName))
534+
, internalBool :: !InternalBool
535+
}
536+
537+
matchUnifyStringEq ::
538+
TermLike RewritingVariableName ->
539+
TermLike RewritingVariableName ->
540+
Maybe UnifyStringEq
541+
matchUnifyStringEq first second
542+
| Just eqTerm <- matchStringEqual first
543+
, isFunctionPattern first
544+
, InternalBool_ internalBool <- second =
545+
Just UnifyStringEq{eqTerm, internalBool}
546+
| otherwise = Nothing
547+
{-# INLINE matchUnifyStringEq #-}
548+
524549
{- | Unification of the @STRING.eq@ symbol
525550
526551
This function is suitable only for equality simplification.
@@ -530,14 +555,19 @@ unifyStringEq ::
530555
MonadUnify unifier =>
531556
TermSimplifier RewritingVariableName unifier ->
532557
NotSimplifier unifier ->
533-
TermLike RewritingVariableName ->
534-
TermLike RewritingVariableName ->
535-
MaybeT unifier (Pattern RewritingVariableName)
536-
unifyStringEq unifyChildren notSimplifier a b =
537-
worker a b <|> worker b a
558+
UnifyStringEq ->
559+
unifier (Pattern RewritingVariableName)
560+
unifyStringEq unifyChildren (NotSimplifier notSimplifier) unifyData =
561+
do
562+
solution <- OrPattern.gather $ unifyChildren operand1 operand2
563+
solution' <-
564+
MultiOr.map eraseTerm solution
565+
& if internalBoolValue internalBool
566+
then pure
567+
else notSimplifier SideCondition.top
568+
scattered <- Unify.scatter solution'
569+
return scattered{term = mkInternalBool internalBool}
538570
where
539-
worker termLike1 termLike2
540-
| Just eqTerm <- matchStringEqual termLike1
541-
, isFunctionPattern termLike1 =
542-
unifyEqTerm unifyChildren notSimplifier eqTerm termLike2
543-
| otherwise = empty
571+
UnifyStringEq{eqTerm, internalBool} = unifyData
572+
EqTerm{operand1, operand2} = eqTerm
573+
eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm

‎kore/src/Kore/Step/Simplification/AndTerms.hs

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -194,14 +194,11 @@ maybeTermEquals notSimplifier childTransformers first second = do
194194
lift $ Builtin.Int.unifyIntEq childTransformers notSimplifier unifyData
195195
| Just unifyData <- Builtin.Int.matchUnifyIntEq second first =
196196
lift $ Builtin.Int.unifyIntEq childTransformers notSimplifier unifyData
197+
| Just unifyData <- Builtin.String.matchUnifyStringEq first second = lift $ Builtin.String.unifyStringEq childTransformers notSimplifier unifyData
198+
| Just unifyData <- Builtin.String.matchUnifyStringEq second first = lift $ Builtin.String.unifyStringEq childTransformers notSimplifier unifyData
197199
| otherwise =
198200
asum
199-
[ Builtin.String.unifyStringEq
200-
childTransformers
201-
notSimplifier
202-
first
203-
second
204-
, do
201+
[ do
205202
unifyData <- Error.hoistMaybe $ Builtin.KEqual.matchUnifyKequalsEq first second
206203
lift $ Builtin.KEqual.unifyKequalsEq childTransformers notSimplifier unifyData
207204
, do
@@ -287,8 +284,9 @@ maybeTermAnd notSimplifier childTransformers first second = do
287284
lift $ Builtin.Bool.unifyBoolNot childTransformers first boolNotData
288285
| Just unifyData <- Builtin.KEqual.matchUnifyKequalsEq first second =
289286
lift $ Builtin.KEqual.unifyKequalsEq childTransformers notSimplifier unifyData
290-
| Just unifyData <- Builtin.KEqual.matchUnifyKequalsEq second first =
291-
lift $ Builtin.KEqual.unifyKequalsEq childTransformers notSimplifier unifyData
287+
| Just unifyData <- Builtin.Int.matchUnifyIntEq first second =
288+
lift $ Builtin.Int.unifyIntEq childTransformers notSimplifier unifyData
289+
| Just unifyData <- Builtin.String.matchUnifyStringEq first second = lift $ Builtin.String.unifyStringEq childTransformers notSimplifier unifyData
292290
| otherwise =
293291
asum
294292
[ Builtin.KEqual.unifyIfThenElse childTransformers first second

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

Lines changed: 42 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -102,10 +102,12 @@ import Kore.Step.Simplification.AndTerms (
102102
termUnification,
103103
)
104104
import Kore.Step.Simplification.Data (
105+
runSimplifier,
105106
runSimplifierBranch,
106107
simplifyCondition,
107108
)
108109
import qualified Kore.Step.Simplification.Not as Not
110+
import qualified Kore.Step.Simplification.Pattern as Pattern
109111
import Kore.Unification.UnifierT (
110112
evalEnvUnifierT,
111113
)
@@ -578,14 +580,28 @@ test_unifyIntEq =
578580
-- unit test
579581
do
580582
actual <- unifyIntEq term1 term2
581-
assertEqual "" [Just expect] actual
583+
let expect' = expect{term = term1}
584+
assertEqual "" [Just expect'] actual
582585
-- integration test
583586
do
584587
actual <-
585588
makeEqualsPredicate term1 term2
586589
& Condition.fromPredicate
587590
& simplifyCondition'
588591
assertEqual "" [expect{term = ()}] actual
592+
-- integration test (see #2586)
593+
do
594+
actual <-
595+
makeInPredicate term1 term2
596+
& Condition.fromPredicate
597+
& simplifyCondition'
598+
assertEqual "" [expect{term = ()}] actual
599+
do
600+
actual <-
601+
mkAnd term1 term2
602+
& Pattern.fromTermLike
603+
& simplifyPattern
604+
assertEqual "" [expect{term = term1}] actual
589605
, testCase "\\equals(true, X ==Int Y)" $ do
590606
let term1 = Test.Bool.asInternal True
591607
term2 = eqInt (mkElemVar x) (mkElemVar y)
@@ -597,7 +613,7 @@ test_unifyIntEq =
597613
actual <- unifyIntEq term1 term2
598614
-- TODO (thomas.tuegel): Remove predicate sorts to eliminate this
599615
-- inconsistency.
600-
let expect' = expect{predicate = makeTruePredicate}
616+
let expect' = expect{term = term1}
601617
assertEqual "" [Just expect'] actual
602618
-- integration test
603619
do
@@ -606,6 +622,19 @@ test_unifyIntEq =
606622
& Condition.fromPredicate
607623
& simplifyCondition'
608624
assertEqual "" [expect{term = ()}] actual
625+
-- integration test (see #2586)
626+
do
627+
actual <-
628+
makeInPredicate term1 term2
629+
& Condition.fromPredicate
630+
& simplifyCondition'
631+
assertEqual "" [expect{term = ()}] actual
632+
do
633+
actual <-
634+
mkAnd term1 term2
635+
& Pattern.fromTermLike
636+
& simplifyPattern
637+
assertEqual "" [expect{term = term1}] actual
609638
, testCase "\\equals(X +Int 1 ==Int Y +Int 1, false)" $ do
610639
let term1 =
611640
eqInt
@@ -622,7 +651,8 @@ test_unifyIntEq =
622651
-- unit test
623652
do
624653
actual <- unifyIntEq term1 term2
625-
assertEqual "" [Just expect] actual
654+
let expect' = expect{term = term2}
655+
assertEqual "" [Just expect'] actual
626656
-- integration test
627657
do
628658
actual <-
@@ -667,6 +697,15 @@ test_unifyIntEq =
667697
& runSimplifierBranch testEnv
668698
& runNoSMT
669699

700+
simplifyPattern ::
701+
Pattern RewritingVariableName ->
702+
IO [Pattern RewritingVariableName]
703+
simplifyPattern pattern1 =
704+
Pattern.simplify pattern1
705+
& runSimplifier testEnv
706+
& runNoSMT
707+
& fmap OrPattern.toPatterns
708+
670709
test_contradiction :: TestTree
671710
test_contradiction =
672711
testCase "x + y = 0 ∧ x + y = 1" $ do

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -192,7 +192,7 @@ test_KEqualSimplification =
192192
keqBool
193193
(kseq (inj kItemSort dvX) dotk)
194194
(kseq (inj kItemSort dvT) dotk)
195-
expect = [Just Pattern.top]
195+
expect = [Just (Pattern.fromTermLike term1)]
196196
actual <- runKEqualSimplification term1 term2
197197
assertEqual' "" expect actual
198198
]

0 commit comments

Comments
 (0)