Skip to content

Recognise ==Int and ==K equations as substitutions when internalising #4061

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Oct 16, 2024
Merged

Recognise ==Int and ==K equations as substitutions when internalising #4061

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2dbac65
recognise ==Int and ==K equations as substitutions when internalising
jberthold Oct 16, 2024
0365bcd
changes to integration tests
jberthold Oct 16, 2024
a85ed55
mention substitution in test-vacuous in README.md
jberthold Oct 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 36 additions & 2 deletions booster/library/Booster/Syntax/Json/Internalise.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ module Booster.Syntax.Json.Internalise (
textToBS,
trm,
handleBS,
asEquations,
TermOrPredicates (..),
InternalisedPredicates (..),
PatternOrTopOrBottom (..),
Expand Down Expand Up @@ -481,6 +482,10 @@ mkEq x t = Internal.Predicate $ case sortOfTerm t of
Internal.SortBool -> Internal.EqualsBool (Internal.Var x) t
otherSort -> Internal.EqualsK (Internal.KSeq otherSort (Internal.Var x)) (Internal.KSeq otherSort t)

-- | turns a substitution into a list of equations
asEquations :: Map Internal.Variable Internal.Term -> [Internal.Predicate]
asEquations = map (uncurry mkEq) . Map.assocs

internalisePred ::
Flag "alias" ->
Flag "subsorts" ->
Expand Down Expand Up @@ -540,10 +545,12 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
ensureEqualSorts (sortOfTerm a) argS
ensureEqualSorts (sortOfTerm b) argS
case (argS, a, b) of
-- for "true" #Equals P, check whether P is in fact a substitution
(Internal.SortBool, Internal.TrueBool, x) ->
pure [BoolPred $ Internal.Predicate x]
mapM mbSubstitution [x]
(Internal.SortBool, x, Internal.TrueBool) ->
pure [BoolPred $ Internal.Predicate x]
mapM mbSubstitution [x]
-- we could also detect NotBool (NEquals _) in "false" #Equals P
(Internal.SortBool, Internal.FalseBool, x) ->
pure [BoolPred $ Internal.Predicate $ Internal.NotBool x]
(Internal.SortBool, x, Internal.FalseBool) ->
Expand Down Expand Up @@ -600,6 +607,33 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
throwE (IncompatibleSorts (map externaliseSort [s1, s2]))
zipWithM_ go args1 args2

mbSubstitution :: Internal.Term -> Except PatternError InternalisedPredicate
mbSubstitution = \case
eq@(Internal.EqualsInt (Internal.Var x) e)
| x `Set.member` freeVariables e -> pure $ boolPred eq
| otherwise -> pure $ SubstitutionPred x e
eq@(Internal.EqualsInt e (Internal.Var x))
| x `Set.member` freeVariables e -> pure $ boolPred eq
| otherwise -> pure $ SubstitutionPred x e
eq@(Internal.EqualsK (Internal.KSeq _sortL (Internal.Var x)) (Internal.KSeq _sortR e)) ->
do
-- NB sorts do not have to agree! (could be subsorts)
pure $
if (x `Set.member` freeVariables e)
then boolPred eq
else SubstitutionPred x e
eq@(Internal.EqualsK (Internal.KSeq _sortL e) (Internal.KSeq _sortR (Internal.Var x))) ->
do
-- NB sorts do not have to agree! (could be subsorts)
pure $
if (x `Set.member` freeVariables e)
then boolPred eq
else SubstitutionPred x e
other ->
pure $ boolPred other

boolPred = BoolPred . Internal.Predicate

----------------------------------------

-- for use with withAssoc
Expand Down
26 changes: 13 additions & 13 deletions booster/library/Booster/Syntax/ParsedKore/Internalise.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -765,6 +765,10 @@ internaliseAxiom (Partial partialDefinition) parsedAxiom =
sortVars
attribs

{- | internalises a pattern and turns its contained substitution into
equations (predicates). Errors if any ceil conditions or
unsupported predicates are found.
-}
internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported ::
KoreDefinition ->
SourceRef ->
Expand All @@ -776,16 +780,16 @@ internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref
(term, preds, ceilConditions, substitution, unsupported) <-
withExcept (DefinitionPatternError ref) $
internalisePattern AllowAlias IgnoreSubsorts maybeVars partialDefinition t
unless (null substitution) $
throwE $
DefinitionPatternError ref SubstitutionNotAllowed
unless (null ceilConditions) $
throwE $
DefinitionPatternError ref CeilNotAllowed
unless (null unsupported) $
throwE $
DefinitionPatternError ref (NotSupported (head unsupported))
pure (Util.modifyVariablesInT f term, map (Util.modifyVariablesInP f) preds)
pure
( Util.modifyVariablesInT f term
, map (Util.modifyVariablesInP f) (preds <> asEquations substitution)
)

internaliseRewriteRuleNoAlias ::
KoreDefinition ->
Expand Down Expand Up @@ -964,12 +968,10 @@ internaliseCeil partialDef left right sortVars attrs = do
internalPs <-
withExcept (DefinitionPatternError (sourceRef attrs)) $
internalisePredicates AllowAlias IgnoreSubsorts (Just sortVars) partialDef [p]
let constraints = internalPs.boolPredicates
substitutions = internalPs.substitution
let
-- turn substitution-like predicates back into equations
constraints = internalPs.boolPredicates <> asEquations internalPs.substitution
unsupported = internalPs.unsupported
unless (null substitutions) $
throwE $
DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed
unless (null unsupported) $
throwE $
DefinitionPatternError (sourceRef attrs) $
Expand Down Expand Up @@ -1005,9 +1007,6 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
withExcept (DefinitionPatternError (sourceRef attrs)) $
internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) partialDef $
Syntax.KJAnd leftTerm.sort [leftTerm, requires]
unless (null substitution) $
throwE $
DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed
unless (null ceils) $
throwE $
DefinitionPatternError (sourceRef attrs) CeilNotAllowed
Expand Down Expand Up @@ -1049,7 +1048,8 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
RewriteRule
{ lhs
, rhs
, requires = map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) preds
, requires =
map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) (preds <> asEquations substitution)
, ensures
, attributes
, computedAttributes
Expand Down
2 changes: 2 additions & 0 deletions booster/test/rpc-integration/test-vacuous/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ Rules `init` and `AC` introduce constraints on this variable:

_Expected:_
- The rewrite is stuck with `<k>d</k><int>N</int> \and...(contradiction)`
- The `N` is substituted by value `1` in the final result (booster).
- The result is simplified and discovered to be `vacuous` (with state `d`).
1) _vacuous-but-rewritten_

Expand All @@ -47,6 +48,7 @@ Rules `init` and `AC` introduce constraints on this variable:
_Expected:_
- Rewrite with `BD` (despite the contradiction)
- The rewrite is stuck with `<k>d</k><int>N</int> \and...(contradiction)`
- The `N` is substituted by value `1` in the final result (booster).
- The result is simplified and discovered to be `vacuous` (with state `d`).

With `kore-rpc-dev`, some contradictions will be discovered before or while
Expand Down
167 changes: 61 additions & 106 deletions booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,13 +66,13 @@
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"value": "0"
}
]
},
Expand All @@ -95,119 +95,74 @@
]
}
},
"substitution": {
"format": "KORE",
"version": 1,
"term": {
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
}
},
"predicate": {
"format": "KORE",
"version": 1,
"term": {
"tag": "And",
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"patterns": [
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "true"
},
"second": {
"tag": "App",
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
{
"tag": "Equals",
"argSort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"sort": {
"tag": "SortApp",
"name": "SortGeneratedTopCell",
"args": []
},
"first": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "true"
},
"second": {
"tag": "App",
"name": "LblnotBool'Unds'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "EVar",
"name": "N",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
}
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
}
]
"value": "true"
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "false"
}
}
}
}
Expand Down
Loading
Loading