diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs
index e5db8e344f..dbca5fb972 100644
--- a/booster/library/Booster/Syntax/Json/Internalise.hs
+++ b/booster/library/Booster/Syntax/Json/Internalise.hs
@@ -24,6 +24,7 @@ module Booster.Syntax.Json.Internalise (
textToBS,
trm,
handleBS,
+ asEquations,
TermOrPredicates (..),
InternalisedPredicates (..),
PatternOrTopOrBottom (..),
@@ -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" ->
@@ -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) ->
@@ -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
diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs
index 6a1acbd6f5..5c258cba73 100644
--- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs
+++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs
@@ -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 ->
@@ -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 ->
@@ -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) $
@@ -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
@@ -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
diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md
index 00c6823dc4..80b71a94c7 100644
--- a/booster/test/rpc-integration/test-vacuous/README.md
+++ b/booster/test/rpc-integration/test-vacuous/README.md
@@ -37,6 +37,7 @@ Rules `init` and `AC` introduce constraints on this variable:
_Expected:_
- The rewrite is stuck with `dN \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_
@@ -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 `dN \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
diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json
index b7cf387833..c604e9284f 100644
--- a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json
+++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json
@@ -66,13 +66,13 @@
"sorts": [],
"args": [
{
- "tag": "EVar",
- "name": "N",
+ "tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
- }
+ },
+ "value": "0"
}
]
},
@@ -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"
+ }
}
}
}
diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json
index d3b14044a8..9bb9e7c837 100644
--- a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json
+++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json
@@ -66,13 +66,13 @@
"sorts": [],
"args": [
{
- "tag": "EVar",
- "name": "N",
+ "tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
- }
+ },
+ "value": "0"
}
]
},
@@ -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"
+ }
}
}
}