Skip to content
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

Use preconditions from the init model in eq. lemmas #1499

Merged
merged 3 commits into from
Feb 15, 2024
Merged

Use preconditions from the init model in eq. lemmas #1499

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9b3fe89
typo?
drganam Aug 21, 2023
50c80e1
Merge branch 'epfl-lara:main' into master
drganam Feb 11, 2024
9fa109a
equivalence is not transitive when there are requires
drganam Feb 11, 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
7 changes: 4 additions & 3 deletions core/src/main/scala/stainless/equivchk/EquivalenceChecker.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -566,6 +566,7 @@ class EquivalenceChecker(override val trees: Trees,
val newParamTps = eqLemma0.tparams.map { tparam => tparam.tp }
val newParamVars = eqLemma0.params.map { param => param.toVariable }

val specsModel = if conf.topLevel then symbols.functions(allModels.head) else conf.model
val subst = {
val nweParamVarsPermuted = conf.strat.order match {
case EquivCheckOrder.ModelFirst =>
Expand All @@ -575,12 +576,12 @@ class EquivalenceChecker(override val trees: Trees,
// f1 = candidate, f2 = model: we need to "undo" the ordering
perm.m2c.map(newParamVars)
}
(conf.model.params.map(_.id) zip nweParamVarsPermuted).toMap
(specsModel.params.map(_.id) zip nweParamVarsPermuted).toMap
}
val tsubst = (conf.model.tparams zip newParamTps).map { case (tparam, targ) => tparam.tp.id -> targ }.toMap
val tsubst = (specsModel.tparams zip newParamTps).map { case (tparam, targ) => tparam.tp.id -> targ }.toMap
val specializer = new Specializer(eqLemma0, eqLemma0.id, tsubst, subst, Map())

val specs = BodyWithSpecs(conf.model.fullBody).specs.filter(s => s.kind == LetKind || s.kind == PreconditionKind)
val specs = BodyWithSpecs(specsModel.fullBody).specs.filter(s => s.kind == LetKind || s.kind == PreconditionKind)
val pre = specs.map {
case Precondition(cond) => Precondition(specializer.transform(cond))
case LetInSpec(vd, expr) => LetInSpec(vd, specializer.transform(expr))
Expand Down