From d3be2883ad5112b7158ae0594e010b7cf76a20e3 Mon Sep 17 00:00:00 2001 From: Silvia Zoraqi Date: Tue, 19 Nov 2024 16:30:14 +0100 Subject: [PATCH 1/6] New files for multisets --- key.core/src/main/antlr4/JmlLexer.g4 | 1 + key.core/src/main/antlr4/JmlParser.g4 | 2 +- .../de/uka/ilkd/key/java/TypeConverter.java | 4 + .../java/ast/abstraction/PrimitiveType.java | 3 +- .../expression/literal/EmptyMSetLiteral.java | 43 ++ .../expression/literal/EmptySeqLiteral.java | 1 - .../java/ast/expression/literal/Literal.java | 6 +- .../ast/expression/operator/mst/MSetCard.java | 49 ++ .../ast/expression/operator/mst/MSetDiff.java | 38 ++ .../operator/mst/MSetIntersect.java | 39 ++ .../ast/expression/operator/mst/MSetMul.java | 50 ++ .../expression/operator/mst/MSetSingle.java | 43 ++ .../ast/expression/operator/mst/MSetSum.java | 38 ++ .../expression/operator/mst/MSetUnion.java | 36 ++ .../key/java/visitor/CreatingASTVisitor.java | 87 +++ .../ilkd/key/java/visitor/JavaASTVisitor.java | 28 + .../de/uka/ilkd/key/java/visitor/Visitor.java | 20 + .../main/java/de/uka/ilkd/key/ldt/LDT.java | 1 + .../java/de/uka/ilkd/key/ldt/MSetLDT.java | 150 +++++ .../uka/ilkd/key/logic/LexPathOrdering.java | 7 + .../de/uka/ilkd/key/logic/TermBuilder.java | 21 + .../nparser/builder/ExpressionBuilder.java | 124 ++-- .../de/uka/ilkd/key/pp/PrettyPrinter.java | 53 +- .../key/speclang/njml/JmlTermFactory.java | 78 +++ .../ilkd/key/speclang/njml/Translator.java | 4 + .../key/proof/rules/MSetRulesdefinition.key | 590 ++++++++++++++++++ .../de/uka/ilkd/key/proof/rules/ldt.key | 3 +- .../de/uka/ilkd/key/proof/rules/msetRules.key | 366 +++++++++++ 28 files changed, 1818 insertions(+), 67 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetCard.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetDiff.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetIntersect.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetMul.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSingle.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSum.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetUnion.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/proof/rules/MSetRulesdefinition.key create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index d90a738ff3d..92ff7ab68ad 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -275,6 +275,7 @@ MAP_UPDATE: '\\map_update'; //KeY extension, not official JML MAX: '\\max'; E_MEASURED_BY: '\\measured_by' -> type(MEASURED_BY); MIN: '\\min'; +MSET: '\\mset'; //KeY extension, not official JML NEWELEMSFRESH: '\\new_elems_fresh'; //KeY extension, not official JML NEW_OBJECTS: '\\new_objects'; //KeY extension, not official JML NONNULLELEMENTS: '\\nonnullelements'; diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index aed3866b353..e93126bf05d 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -417,7 +417,7 @@ sequence mapExpression: MAP_GET | MAP_OVERRIDE | MAP_UPDATE | MAP_REMOVE | IN_DOMAIN | DOMAIN_IMPLIES_CREATED | MAP_SIZE | MAP_SINGLETON | IS_FINITE; fpOperator: FP_ABS | FP_INFINITE | FP_NAN | FP_NEGATIVE | FP_NICE | FP_NORMAL | FP_POSITIVE | FP_SUBNORMAL; -quantifier: FORALL | EXISTS | MIN | MAX | NUM_OF | PRODUCT | SUM; +quantifier: FORALL | EXISTS | MIN | MAX | NUM_OF | PRODUCT | SUM | MSET; infinite_union_expr: LPAREN UNIONINF (boundvarmodifiers)? quantifiedvardecls SEMI (predicate SEMI)* storeref RPAREN; specquantifiedexpression: LPAREN quantifier (boundvarmodifiers)? quantifiedvardecls SEMI (expression SEMI)? expression RPAREN; oldexpression: (PRE LPAREN expression RPAREN | OLD LPAREN expression (COMMA IDENT)? RPAREN); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java index 6dfc71cd6e1..fa74ce98dc6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java @@ -116,6 +116,10 @@ public SeqLDT getSeqLDT() { return (SeqLDT) getLDT(SeqLDT.NAME); } + public MSetLDT getMSetLDT() { + return (MSetLDT) getLDT(MSetLDT.NAME); + } + public SortLDT getSortLDT() { return (SortLDT) getLDT(SortLDT.NAME); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java index 28cf6fe9942..25d3f7f8e34 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java @@ -9,7 +9,6 @@ import java.util.Map; import de.uka.ilkd.key.java.ast.expression.literal.*; -import de.uka.ilkd.key.java.ast.expression.literal.Literal; import de.uka.ilkd.key.ldt.*; import de.uka.ilkd.key.logic.ProgramElementName; @@ -59,6 +58,8 @@ public final class PrimitiveType implements Type { new PrimitiveType("\\map", EmptyMapLiteral.INSTANCE, MapLDT.NAME); public static final PrimitiveType JAVA_TYPE = new PrimitiveType("\\TYPE", NullLiteral.NULL, SortLDT.NAME); + public static final PrimitiveType JAVA_MSET = + new PrimitiveType("\\mset", EmptyMSetLiteral.INSTANCE, MSetLDT.NAME); public static final PrimitiveType PROGRAM_SV = new PrimitiveType("SV", null, null); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java new file mode 100644 index 00000000000..af03e8f328e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java @@ -0,0 +1,43 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.literal; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.ldt.MSetLDT; + +import org.key_project.logic.Name; + +public non-sealed class EmptyMSetLiteral extends Literal { + public static final EmptyMSetLiteral INSTANCE = new EmptyMSetLiteral(); + + private EmptyMSetLiteral() { + } + + @Override + public boolean equals(Object o) { + return o == this; + } + + @Override + protected int computeHashCode() { + return System.identityHashCode(this); + } + + public void visit(Visitor v) { + v.performActionOnEmptyMSetLiteral(this); + } + + + public KeYJavaType getKeYJavaType(Services javaServ) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET); + } + + @Override + public Name getLDTName() { + return MSetLDT.NAME; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java index 9045dd67f09..fbf8251356c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java @@ -33,7 +33,6 @@ public void visit(Visitor v) { v.performActionOnEmptySeqLiteral(this); } - public KeYJavaType getKeYJavaType(Services javaServ) { return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_SEQ); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java index b933c076c6e..13424e43a3f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java @@ -40,9 +40,9 @@ class Literal extends JavaProgramElement implements Expression, TerminalProgramElement - permits AbstractIntegerLiteral, BooleanLiteral, DoubleLiteral, EmptyMapLiteral, - EmptySeqLiteral, EmptySetLiteral, FloatLiteral, FreeLiteral, NullLiteral, RealLiteral, - StringLiteral { + permits AbstractIntegerLiteral, BooleanLiteral, DoubleLiteral, EmptyMSetLiteral, + EmptyMapLiteral, EmptySeqLiteral, EmptySetLiteral, FloatLiteral, FreeLiteral, NullLiteral, + RealLiteral, StringLiteral { public Literal(@Nullable PositionInfo pi, @Nullable List comments) { super(pi, comments); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetCard.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetCard.java new file mode 100644 index 00000000000..8caf741db18 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetCard.java @@ -0,0 +1,49 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetCard extends Operator { + + public MSetCard(ExtList children) { + super(children); + } + + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public void visit(Visitor v) { + v.performActionOnMSetCard(this); + } + + + @Override + public int getArity() { + return 1; + } + + + @Override + public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_INT); + } + + + @Override + public int getNotation() { + return Operator.PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetDiff.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetDiff.java new file mode 100644 index 00000000000..0de27b61292 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetDiff.java @@ -0,0 +1,38 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + + +public class MSetDiff extends BinaryOperator { + public MSetDiff(ExtList children) { + super(children); + } + + public MSetDiff(Expression msetA, Expression msetB) { + super(msetA, msetB); + } + + + + @Override + public void visit(Visitor v) { + v.performActionOnMSetDiff(this); + } + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public int getNotation() { + return PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetIntersect.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetIntersect.java new file mode 100644 index 00000000000..fa3d12c41d9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetIntersect.java @@ -0,0 +1,39 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetIntersect extends BinaryOperator { + + + public MSetIntersect(ExtList children) { + super(children); + } + + public MSetIntersect(Expression msetA, Expression msetB) { + super(msetA, msetB); + } + + + + @Override + public void visit(Visitor v) { + v.performActionOnMSetIntersect(this); + } + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public int getNotation() { + return PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetMul.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetMul.java new file mode 100644 index 00000000000..512eda0d16f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetMul.java @@ -0,0 +1,50 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + + +public class MSetMul extends Operator { + + public MSetMul(ExtList children) { + super(children); + } + + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public void visit(Visitor v) { + v.performActionOnMSetMul(this); + } + + @Override + public int getArity() { + return 1; + } + + + @Override + public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_INT); + } + + + @Override + public int getNotation() { + return Operator.PREFIX; + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSingle.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSingle.java new file mode 100644 index 00000000000..36872fcaba2 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSingle.java @@ -0,0 +1,43 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetSingle extends Operator { + + public MSetSingle(ExtList children) { super(children); } + + public MSetSingle(Expression child) { super(child); } + + public int getPrecedence() { + return 0; + } + + + public int getNotation() { + return PREFIX; + } + + + public void visit(Visitor v) { + v.performActionOnMSetSingle(this); + } + + public int getArity() { + return 1; + } + + public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec) { + return javaServ.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSum.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSum.java new file mode 100644 index 00000000000..78ec802d3c6 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetSum.java @@ -0,0 +1,38 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetSum extends BinaryOperator { + + public MSetSum(ExtList children) { + super(children); + } + + public MSetSum(Expression msetA, Expression msetB) { + super(msetA, msetB); + } + + + + @Override + public void visit(Visitor v) { + v.performActionOnMSetSum(this); + } + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public int getNotation() { + return PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetUnion.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetUnion.java new file mode 100644 index 00000000000..78fd39a7005 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/mst/MSetUnion.java @@ -0,0 +1,36 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.ast.expression.operator.mst; + +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.operator.BinaryOperator; +import de.uka.ilkd.key.java.visitor.Visitor; + +import org.key_project.util.ExtList; + +public class MSetUnion extends BinaryOperator { + public MSetUnion(ExtList children) { + super(children); + } + + public MSetUnion(Expression msetA, Expression msetB) { + super(msetA, msetB); + } + + + @Override + public void visit(Visitor v) { + v.performActionOnMSetUnion(this); + } + + @Override + public int getPrecedence() { + return 0; + } + + @Override + public int getNotation() { + return PREFIX; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java index de756e25907..bf544d4859d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -18,6 +18,7 @@ import de.uka.ilkd.key.java.ast.expression.PassiveExpression; import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.op.IProgramVariable; @@ -1479,6 +1480,92 @@ ProgramElement createNewElement(ExtList changeList) { def.doAction(x); } + public void performActionOnMSetUnion(MSetUnion x) { + + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + + return new MSetUnion(changeList); + } + + }; + + def.doAction(x); + + } + + @Override + public void performActionOnMSetIntersect(MSetIntersect x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetIntersect(changeList); + } + }; + def.doAction(x); + } + + @Override + public void performActionOnMSetSum(MSetSum x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetSum(changeList); + } + }; + def.doAction(x); + + } + + @Override + public void performActionOnMSetDiff(MSetDiff x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetDiff(changeList); + } + }; + def.doAction(x); + + + } + + @Override + public void performActionOnMSetSingle(MSetSingle x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetSingle(changeList); + } + }; + def.doAction(x); + } + + @Override + public void performActionOnMSetCard(MSetCard x) { + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetCard(changeList); + } + }; + def.doAction(x); + } + + @Override + public void performActionOnMSetMul(MSetMul x) { + + DefaultAction def = new DefaultAction(x) { + @Override + ProgramElement createNewElement(ExtList changeList) { + return new MSetMul(changeList); + } + }; + def.doAction(x); + } + + @Override public void performActionOnDLEmbeddedExpression(final DLEmbeddedExpression x) { DefaultAction def = new DefaultAction(x) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java index 91bd808e2f8..735dfb438c8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -11,9 +11,11 @@ import de.uka.ilkd.key.java.ast.expression.ParenthesizedExpression; import de.uka.ilkd.key.java.ast.expression.PassiveExpression; import de.uka.ilkd.key.java.ast.expression.literal.*; +import de.uka.ilkd.key.java.ast.expression.literal.EmptyMSetLiteral; import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.Subtype; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; @@ -190,6 +192,8 @@ public void performActionOnSetUnion(SetUnion x) { doDefaultAction(x); } + + @Override public void performActionOnIntersect(Intersect x) { doDefaultAction(x); @@ -240,6 +244,30 @@ public void performActionOnSeqPut(SeqPut x) { doDefaultAction(x); } + @Override + public void performActionOnEmptyMSetLiteral(EmptyMSetLiteral x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetUnion(MSetUnion x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetIntersect(MSetIntersect x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetSum(MSetSum x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetDiff(MSetDiff x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetSingle(MSetSingle x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetMul(MSetMul x) { doDefaultAction(x); } + + @Override + public void performActionOnMSetCard(MSetCard x) { doDefaultAction(x); } + @Override public void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x) { doDefaultAction(x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index e5299c49298..51b6c33d181 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -10,9 +10,11 @@ import de.uka.ilkd.key.java.ast.expression.ParenthesizedExpression; import de.uka.ilkd.key.java.ast.expression.PassiveExpression; import de.uka.ilkd.key.java.ast.expression.literal.*; +import de.uka.ilkd.key.java.ast.expression.literal.EmptyMSetLiteral; import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.Subtype; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; @@ -62,6 +64,8 @@ public interface Visitor { void performActionOnSetUnion(SetUnion x); + + void performActionOnIntersect(Intersect x); void performActionOnSetMinus(SetMinus x); @@ -84,6 +88,22 @@ public interface Visitor { void performActionOnSeqPut(SeqPut seqPut); + void performActionOnMSetUnion(MSetUnion x); + + void performActionOnMSetIntersect(MSetIntersect x); + + void performActionOnMSetSum(MSetSum x); + + void performActionOnMSetDiff(MSetDiff x); + + void performActionOnEmptyMSetLiteral(EmptyMSetLiteral x); + + void performActionOnMSetSingle(MSetSingle x); + + void performActionOnMSetMul(MSetMul x); + + void performActionOnMSetCard(MSetCard x); + void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x); void performActionOnStringLiteral(StringLiteral x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java index fe11de64b3b..98d33b14a78 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java @@ -154,6 +154,7 @@ public static Map getNewLDTInstances(Services s) { ret.put(DoubleLDT.NAME, new DoubleLDT(s)); ret.put(RealLDT.NAME, new RealLDT(s)); ret.put(CharListLDT.NAME, new CharListLDT(s)); + ret.put(MSetLDT.NAME, new MSetLDT(s)); return ret; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java new file mode 100644 index 00000000000..25cd59f92b3 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java @@ -0,0 +1,150 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.ldt; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.abstraction.Type; +import de.uka.ilkd.key.java.ast.expression.Expression; +import de.uka.ilkd.key.java.ast.expression.Operator; +import de.uka.ilkd.key.java.ast.expression.literal.*; +import de.uka.ilkd.key.java.ast.expression.operator.*; +import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; +import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.TermServices; +import de.uka.ilkd.key.logic.op.JFunction; + +import org.key_project.logic.Name; +import org.key_project.logic.op.Function; +import org.key_project.util.ExtList; + +public class MSetLDT extends LDT { + + public static final Name NAME = new Name("Mset"); + + private final JFunction msetRange; + private final JFunction msetMul; + private final JFunction msetEmpty; + private final JFunction msetSingle; + private final JFunction msetUnion; + private final JFunction msetIntersec; + private final JFunction msetSum; + private final JFunction msetDiff; + private final JFunction msetCard; + + public MSetLDT(TermServices services) { + super(NAME, services); + msetMul = addFunction(services, "msetMul"); + msetEmpty = addFunction(services, "msetEmpty"); + msetSingle = addFunction(services, "msetSingle"); + msetUnion = addFunction(services, "msetUnion"); + msetIntersec = addFunction(services, "msetIntersec"); + msetSum = addFunction(services, "msetSum"); + msetDiff = addFunction(services, "msetDiff"); + msetCard = addFunction(services, "msetCard"); + msetRange = addFunction(services, "msetRange"); + } + + + public JFunction getMsetRange() { return msetRange; } + + public JFunction getMsetMul() { + return msetMul; + } + + public JFunction getMsetEmpty() { + return msetEmpty; + } + + public JFunction getMsetSingle() { + return msetSingle; + } + + public JFunction getMsetUnion() { + return msetUnion; + } + + public JFunction getMsetIntersec() { + return msetIntersec; + } + + public JFunction getMsetAdd() { + return msetSum; + } + + public JFunction getMsetRemove() { + return msetDiff; + } + + @Override + public boolean isResponsible(Operator op, JTerm[] subs, Services services, + ExecutionContext ec) { + return op instanceof MSetCard || op instanceof MSetMul || op instanceof MSetSingle + || op instanceof MSetIntersect || + op instanceof MSetDiff || op instanceof MSetUnion || op instanceof MSetSum; + } + + @Override + public boolean isResponsible(Operator op, JTerm left, JTerm right, Services services, + ExecutionContext ec) { + return op instanceof MSetUnion || op instanceof MSetIntersect || op instanceof MSetSum + || op instanceof MSetDiff; + } + + @Override + public boolean isResponsible(Operator op, JTerm sub, TermServices services, + ExecutionContext ec) { + return op instanceof MSetSingle || op instanceof MSetMul || op instanceof MSetCard; + } + + @Override + public JTerm translateLiteral(Literal lit, Services services) { + assert lit instanceof EmptySeqLiteral; + return services.getTermBuilder().func(msetEmpty); + } + + @Override + public JFunction getFunctionFor(Operator op, Services services, ExecutionContext ec) { + if (op instanceof MSetSingle) { + return msetSingle; + } else if (op instanceof MSetCard) { + return msetCard; + } else if (op instanceof MSetUnion) { + return msetUnion; + } else if (op instanceof MSetDiff) { + return msetDiff; + } else if (op instanceof MSetSum) { + return msetSum; + } else if (op instanceof MSetIntersect) { + return msetIntersec; + } else if (op instanceof MSetMul) { + return msetMul; + } + + assert false; + return null; + + } + + @Override + public boolean hasLiteralFunction(Function f) { + return f.equals(msetEmpty); + } + + @Override + public Expression translateTerm(JTerm t, ExtList children, Services services) { + if (t.op().equals(msetEmpty)) { + return EmptyMSetLiteral.INSTANCE; + } + assert false; + return null; + } + + @Override + public Type getType(JTerm t) { + assert false; + return null; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java b/key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java index c6616c6edec..a7ca796a8ce 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/LexPathOrdering.java @@ -424,6 +424,13 @@ protected Integer getWeight(Operator p_op) { return 7; } + + if (opStr.equals("msetSingle")) { + return 6; + } + if (opStr.equals("msetSum")) { + return 7; + } return null; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java index 85e309de798..d171bddeddf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java @@ -2121,6 +2121,10 @@ public JTerm seqEmpty() { return func(services.getTypeConverter().getSeqLDT().getSeqEmpty()); } + public JTerm msetEmpty() { + return func(services.getTypeConverter().getMSetLDT().getMsetEmpty()); + } + public JTerm seqSingleton(JTerm x) { return func(services.getTypeConverter().getSeqLDT().getSeqSingleton(), x); } @@ -2245,6 +2249,23 @@ public JTerm seqDef(QuantifiableVariable qv, JTerm a, JTerm b, JTerm t) { new ImmutableArray<>(qv)); } + public JTerm mset(QuantifiableVariable qv, JTerm a, JTerm b, JTerm t) { + return func(services.getTypeConverter().getMSetLDT().getMsetRange(), + new JTerm[] { a, b, t }, + new ImmutableArray<>(qv)); + } + + public JTerm mset(ImmutableList qvs, JTerm range, JTerm t) { + final Function mset = services.getNamespaces().functions().lookup("mset"); + final Iterator it = qvs.iterator(); + JTerm res = func(mset, new JTerm[] { convertToBoolean(range), t }, + new ImmutableArray<>(it.next())); + while (it.hasNext()) { + res = func(mset, new JTerm[] { TRUE(), res }, new ImmutableArray<>(it.next())); + } + return res; + } + public JTerm values() { return func(services.getTypeConverter().getSeqLDT().getValues()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index 535d844ceaa..924642ed9f6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java @@ -56,7 +56,7 @@ /** * This visitor creates expression from {@link de.uka.ilkd.key.nparser.KeyAst.Term}. You should use - * the facade {@link de.uka.ilkd.key.nparser.KeyIO#parseExpression(String)} for term parsing. + * the facade {@link de.uka.ilkd.key.nparser.KeyIO#parseExpression(String)} for JTerm parsing. * * @author weigl */ @@ -64,7 +64,7 @@ public class ExpressionBuilder extends DefaultBuilder { public static final Logger LOGGER = LoggerFactory.getLogger(ExpressionBuilder.class); public static final String NO_HEAP_EXPRESSION_BEFORE_AT_EXCEPTION_MESSAGE = - "Expecting select term before '@', not: "; + "Expecting select JTerm before '@', not: "; /** * The current abbreviation used for resolving "@name" terms. @@ -175,9 +175,9 @@ public static String operatorOfJavaBlock(String raw) { return "n/a"; } - private static boolean isSelectTerm(JTerm term) { - return term.op() instanceof ParametricFunctionInstance pfi - && pfi.getBase().name().toString().equals("select") && term.arity() == 3; + private static boolean isSelectTerm(JTerm JTerm) { + return JTerm.op() instanceof ParametricFunctionInstance pfi + && pfi.getBase().name().toString().equals("select") && JTerm.arity() == 3; } @Override @@ -264,7 +264,7 @@ public JTerm visitConjunction_term(JavaKeYParser.Conjunction_termContext ctx) { t = binaryTerm(ctx, Junctor.AND, t, accept(c)); } return t; - // Term termR = accept(ctx.b); + // JTerm termR = accept(ctx.b); // return binaryTerm(ctx, Junctor.AND, termL, termR); } @@ -427,10 +427,10 @@ public Object visitStrong_arith_term_2(JavaKeYParser.Strong_arith_term_2Context // "mod" : // "div").collect(Collectors.toList()); - JTerm term = accept(ctx.a); - var sort = term.sort(); + JTerm JTerm = accept(ctx.a); + var sort = JTerm.sort(); if (sort == null) { - semanticError(ctx, "No sort for term '%s'", term); + semanticError(ctx, "No sort for JTerm '%s'", JTerm); } var ldt = services.getTypeConverter().getLDTFor(sort); @@ -449,9 +449,9 @@ public Object visitStrong_arith_term_2(JavaKeYParser.Strong_arith_term_2Context semanticError(ctx, "Could not find function symbol '%s' for sort '%s'.", opName, sort); } - term = binaryTerm(ctx, ctx.b.get(i), op, term, termL.get(i)); + JTerm = binaryTerm(ctx, ctx.b.get(i), op, JTerm, termL.get(i)); } - return term; + return JTerm; } protected JTerm capsulateTf(ParserRuleContext ctx, Supplier termSupplier) { @@ -459,8 +459,9 @@ protected JTerm capsulateTf(ParserRuleContext ctx, Supplier termSupplier) } /** - * Builds a term and, on failure, raises a {@link BuildingException} that describes the - * whole term {@code ctx} but is located at {@code locationCtx} (e.g. the offending + * Builds a JTerm and, on failure, raises a {@link BuildingException} that describes + * the + * whole JTerm {@code ctx} but is located at {@code locationCtx} (e.g. the offending * operand of a binary operation rather than the whole expression). */ protected JTerm capsulateTf(ParserRuleContext ctx, ParserRuleContext locationCtx, @@ -469,11 +470,11 @@ protected JTerm capsulateTf(ParserRuleContext ctx, ParserRuleContext locationCtx return termSupplier.get(); } catch (TermCreationException e) { // Surface the actual reason (usually an arity or sort/type mismatch) instead of the - // generic "Could not build term". The TermCreationException message lists the expected + // generic "Could not build JTerm". The TermCreationException message lists the expected // and actual argument sorts, including the sort hashes - these are kept on purpose: // they let one distinguish two different sort objects that share the same name. String reason = e.getMessage() == null ? "" : "\n" + e.getMessage(); - String msg = String.format("Could not type-check term '%s'.%s", ctx.getText(), reason); + String msg = String.format("Could not type-check JTerm '%s'.%s", ctx.getText(), reason); Token at = locationCtx != null ? locationCtx.start : (ctx != null ? ctx.start : null); throw new BuildingException(at, null, msg, e); } @@ -514,7 +515,7 @@ public Object visitBracket_term(JavaKeYParser.Bracket_termContext ctx) { // } /* - * @Override public Term + * @Override public JTerm * visitStatic_attribute_suffix(JavaKeYParser.Static_attribute_suffixContext * ctx) { Operator v = null; String attributeName = * accept(ctx.staticAttributeOrQueryReference()); String className; if @@ -954,16 +955,17 @@ private void markHeapAsExplicit(JTerm a) { } /* - * private Term createStaticAttributeOrMethod(JavaQuery jq, JavaKeYParser.AccesstermContext ctx) + * private JTerm createStaticAttributeOrMethod(JavaQuery jq, JavaKeYParser.AccesstermContext + * ctx) * { * final var kjt = jq.kjt; String mn = jq.attributeNames; if (jq.maybeAttr != null) { * ProgramVariable maybeAttr = getJavaInfo().getAttribute(mn, kjt); if (maybeAttr != null) { var * op = getAttributeInPrefixSort(kjt.getSort(), mn); return createAttributeTerm(null, op, ctx); * } } else { var suffix = ctx.atom_suffix(ctx.atom_suffix().size() - 1); for (IProgramMethod pm * : getJavaInfo().getAllProgramMethods(kjt)) { if (pm != null && pm.isStatic() && - * pm.name().toString().equals(kjt.getFullName() + "::" + mn)) { List arguments = - * mapOf(suffix.attribute_or_query_suffix().result.args.argument()); Term[] args = - * arguments.toArray(new Term[0]); return getJavaInfo().getStaticProgramMethodTerm(mn, args, + * pm.name().toString().equals(kjt.getFullName() + "::" + mn)) { List arguments = + * mapOf(suffix.attribute_or_query_suffix().result.args.argument()); JTerm[] args = + * arguments.toArray(new JTerm[0]); return getJavaInfo().getStaticProgramMethodTerm(mn, args, * kjt.getFullName()); } } } assert false; return null; } */ @@ -1015,10 +1017,10 @@ public Object visitBracket_access_star(JavaKeYParser.Bracket_access_starContext @Override public Object visitBracket_access_indexrange( JavaKeYParser.Bracket_access_indexrangeContext ctx) { - // | term LBRACKET indexTerm=term (DOTRANGE rangeTo=term)? RBRACKET + // | JTerm LBRACKET indexTerm=JTerm (DOTRANGE rangeTo=JTerm)? RBRACKET // #bracket_access_indexrange - JTerm term = pop(); - boolean sequenceAccess = term.sort().name().toString().equalsIgnoreCase("seq"); + JTerm JTerm = pop(); + boolean sequenceAccess = JTerm.sort().name().toString().equalsIgnoreCase("seq"); // boolean heapUpdate = reference.sort().name().toString().equalsIgnoreCase("Heap"); if (sequenceAccess) { @@ -1029,10 +1031,10 @@ public Object visitBracket_access_indexrange( assert indexTerm != null; if (!isIntTerm(indexTerm)) { semanticError(ctx, - "Expecting term of sort %s as index of sequence %s, but found: %s", - IntegerLDT.NAME, term, indexTerm); + "Expecting JTerm of sort %s as index of sequence %s, but found: %s", + IntegerLDT.NAME, JTerm, indexTerm); } - return getServices().getTermBuilder().seqGet(JavaDLTheory.ANY, term, indexTerm); + return getServices().getTermBuilder().seqGet(JavaDLTheory.ANY, JTerm, indexTerm); } if (ctx.rangeTo != null) { @@ -1060,7 +1062,7 @@ public Object visitBracket_access_indexrange( } } JTerm indexTerm = accept(ctx.indexTerm); - return capsulateTf(ctx, () -> getServices().getTermBuilder().dotArr(term, indexTerm)); + return capsulateTf(ctx, () -> getServices().getTermBuilder().dotArr(JTerm, indexTerm)); } @Override @@ -1134,7 +1136,7 @@ public Object visitAbbreviation(JavaKeYParser.AbbreviationContext ctx) { public JTerm visitIfThenElseTerm(JavaKeYParser.IfThenElseTermContext ctx) { JTerm condF = (JTerm) ctx.condF.accept(this); if (condF.sort() != JavaDLTheory.FORMULA) { - semanticError(ctx, "Condition of an \\if-then-else term has to be a formula."); + semanticError(ctx, "Condition of an \\if-then-else JTerm has to be a formula."); } JTerm thenT = (JTerm) ctx.thenT.accept(this); JTerm elseT = (JTerm) ctx.elseT.accept(this); @@ -1149,7 +1151,7 @@ public Object visitIfExThenElseTerm(JavaKeYParser.IfExThenElseTermContext ctx) { List exVars = accept(ctx.bound_variables()); JTerm condF = accept(ctx.condF); if (condF.sort() != JavaDLTheory.FORMULA) { - semanticError(ctx, "Condition of an \\ifEx-then-else term has to be a formula."); + semanticError(ctx, "Condition of an \\ifEx-then-else JTerm has to be a formula."); } JTerm thenT = accept(ctx.thenT); @@ -1325,7 +1327,7 @@ public boolean isClass(String p) { * Handles "[sort]::a.name.or.something.else" * * @param ctx - * @return a Term or an operator, depending on the referenced object. + * @return a JTerm or an operator, depending on the referenced object. */ @Override public Object visitFuncpred_name(JavaKeYParser.Funcpred_nameContext ctx) { @@ -1666,7 +1668,7 @@ public JTerm visitAccessterm(JavaKeYParser.AccesstermContext ctx) { for (QuantifiableVariable qv : args[i].freeVars()) { if (boundVars.contains(qv)) { semanticError(ctx, - "Building function term " + op + "Building function JTerm " + op + " with bound variables failed: " + "Variable " + qv + " must not occur free in subterm " + args[i]); } @@ -1674,7 +1676,7 @@ public JTerm visitAccessterm(JavaKeYParser.AccesstermContext ctx) { } } ImmutableArray finalBoundVars = boundVars; - // create term + // create JTerm JTerm[] finalArgs1 = args; current = capsulateTf(ctx, () -> getTermFactory().createTerm(finalOp, finalArgs1, finalBoundVars, null)); @@ -1773,7 +1775,7 @@ private JTerm toNum(String number) { } /* - * private Term makeBinaryTerm(String opName, Term a, Term a1) { LDT ldt = + * private JTerm makeBinaryTerm(String opName, JTerm a, JTerm a1) { LDT ldt = * services.getTypeConverter().getLDTFor(a.sort()); if (ldt != null) { Function op = * ldt.getFunctionFor(opName, services); if (op == null) { * semanticError("Cannot resolve symbol '" + opName + "' for sort " + a.sort()); } else { a = @@ -1856,15 +1858,19 @@ private boolean isPackage(String name) { } } - protected boolean isHeapTerm(JTerm term) { - return term != null - && term.sort() == getServices().getTypeConverter().getHeapLDT().targetSort(); + protected boolean isHeapTerm(JTerm JTerm) { + return JTerm != null + && JTerm.sort() == getServices().getTypeConverter().getHeapLDT().targetSort(); } private boolean isSequenceTerm(JTerm reference) { return reference != null && reference.sort().name().equals(SeqLDT.NAME); } + private boolean inMultisetTerm(JTerm reference) { + return reference != null && reference.sort().name().equals(MSetLDT.NAME); + } + private boolean isIntTerm(JTerm reference) { return reference.sort().name().equals(IntegerLDT.NAME); } @@ -1888,54 +1894,54 @@ private boolean isImplicitHeap(JTerm t) { * Guard for {@link #replaceHeap0(JTerm, JTerm, ParserRuleContext)} to protect the double * application of {@code @heap}. */ - private JTerm replaceHeap(JTerm term, JTerm heap, ParserRuleContext ctx) { - if (explicitHeap.contains(term)) { - return term; + private JTerm replaceHeap(JTerm JTerm, JTerm heap, ParserRuleContext ctx) { + if (explicitHeap.contains(JTerm)) { + return JTerm; } - JTerm t = replaceHeap0(term, heap, ctx); + JTerm t = replaceHeap0(JTerm, heap, ctx); markHeapAsExplicit(t); return t; } - private JTerm replaceHeap0(JTerm term, JTerm heap, ParserRuleContext ctx) { - if (isSelectTerm(term)) { - if (!isImplicitHeap(term.sub(0))) { + private JTerm replaceHeap0(JTerm JTerm, JTerm heap, ParserRuleContext ctx) { + if (isSelectTerm(JTerm)) { + if (!isImplicitHeap(JTerm.sub(0))) { // semanticError(null, "Expecting program variable heap as first argument of: %s", - // term); - return term; + // JTerm); + return JTerm; } - JTerm[] params = { heap, replaceHeap(term.sub(1), heap, ctx), term.sub(2) }; + JTerm[] params = { heap, replaceHeap(JTerm.sub(1), heap, ctx), JTerm.sub(2) }; return capsulateTf(ctx, - () -> getServices().getTermFactory().createTerm(term.op(), params)); - } else if (term.op() instanceof ObserverFunction) { - if (!isImplicitHeap(term.sub(0))) { + () -> getServices().getTermFactory().createTerm(JTerm.op(), params)); + } else if (JTerm.op() instanceof ObserverFunction) { + if (!isImplicitHeap(JTerm.sub(0))) { semanticError(null, "Expecting program variable heap as first argument of: %s", - term); + JTerm); } - JTerm[] params = new JTerm[term.arity()]; + JTerm[] params = new JTerm[JTerm.arity()]; params[0] = heap; - params[1] = replaceHeap(term.sub(1), heap, ctx); + params[1] = replaceHeap(JTerm.sub(1), heap, ctx); for (int i = 2; i < params.length; i++) { - params[i] = term.sub(i); + params[i] = JTerm.sub(i); } return capsulateTf(ctx, - () -> getServices().getTermFactory().createTerm(term.op(), params)); + () -> getServices().getTermFactory().createTerm(JTerm.op(), params)); } - return term; + return JTerm; } /** * Replace standard heap by another heap in an observer function. */ - protected JTerm heapSelectionSuffix(JTerm term, JTerm heap, ParserRuleContext ctx) { + protected JTerm heapSelectionSuffix(JTerm JTerm, JTerm heap, ParserRuleContext ctx) { if (!isHeapTerm(heap)) { - semanticError(null, "Expecting term of type Heap but sort is %s for term %s", - heap.sort(), term); + semanticError(null, "Expecting JTerm of type Heap but sort is %s for JTerm %s", + heap.sort(), JTerm); } - JTerm result = replaceHeap(term, heap, ctx); + JTerm result = replaceHeap(JTerm, heap, ctx); return result; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index 78818a43e31..a176c80c747 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -16,6 +16,7 @@ import de.uka.ilkd.key.java.ast.expression.literal.*; import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.java.visitor.Visitor; @@ -406,6 +407,55 @@ public void performActionOnSeqPut(SeqPut x) { printDLFunctionOperator("\\seq_upd", x); } + @Override + public void performActionOnEmptyMSetLiteral(EmptyMSetLiteral x) { + layouter.print("\\mset_empty"); + } + + + + @Override + public void performActionOnMSetUnion(MSetUnion x) { + printDLFunctionOperator("\\mset_union", x); + } + + @Override + public void performActionOnMSetIntersect( + MSetIntersect x) { + printDLFunctionOperator("\\mset_intersection", x); + } + + @Override + public void performActionOnMSetSum(MSetSum x) { + printDLFunctionOperator("\\mset_sum", x); + } + + @Override + public void performActionOnMSetDiff(MSetDiff x) { + printDLFunctionOperator("\\mset_diff", x); + } + + @Override + public void performActionOnMSetSingle( + MSetSingle x) { + printDLFunctionOperator("\\mset_single", x); + } + + @Override + public void performActionOnMSetMul(MSetMul x) { + x.getChildAt(0).visit(this); + layouter.print("["); + x.getChildAt(1).visit(this); + layouter.print("]"); + } + + @Override + public void performActionOnMSetCard(MSetCard x) { + x.getChildAt(0).visit(this); + layouter.print(".length"); + } + + @Override public void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x) { layouter.print("\\dl_" + x.getFunctionSymbol().name()); @@ -624,7 +674,8 @@ public void performActionOnTypeReference(TypeReference x, boolean fullTypeNames) } private void printTypeReference(ReferencePrefix prefix, @Nullable KeYJavaType type, - ProgramElementName name, boolean fullTypeNames) { + ProgramElementName name, + boolean fullTypeNames) { printReferencePrefix(prefix); if (fullTypeNames && type != null) { layouter.print(type.getFullName()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java index 390324347d4..45bf4acea81 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java @@ -275,6 +275,17 @@ public SLExpression quantifiedMax(JTerm _guard, JTerm body, KeYJavaType declsTyp return numeralQuantifier(javaType, nullable, qvs, t1, t2, resultType, unbounded, bounded); } + public @NonNull SLExpression quantifiedMset(KeYJavaType javaType, boolean nullable, + Iterable qvs, @Nullable JTerm t1, JTerm t2, KeYJavaType resultType) { + BoundedNumericalQuantifier bounded = tb::mset; + UnboundedNumericalQuantifier unbounded = (declsType, n, vars, range, body) -> { + final JTerm tr = typerestrict(declsType, n, vars); + return tb.mset(vars, tb.andSC(tr, range), body); + }; + return nonNumeralQuantifier(javaType, nullable, qvs, t1, t2, resultType, unbounded, + bounded); + } + public SLExpression forall(JTerm preTerm, JTerm bodyTerm, KeYJavaType declsType, ImmutableList declVars, boolean nullable, KeYJavaType resultType) { BiFunction quantify = tb::all; @@ -396,6 +407,33 @@ public JTerm upperBound(JTerm a, LogicVariable lv) { return buildBigintTruncationExpression(resultType, t); } + private @NonNull SLExpression nonNumeralQuantifier(KeYJavaType declsType, boolean nullable, + Iterable qvs, JTerm t1, JTerm t2, @Nullable KeYJavaType resultType, + UnboundedNumericalQuantifier unbounded, BoundedNumericalQuantifier bounded) { + Iterator it = qvs.iterator(); + LogicVariable lv = it.next(); + JTerm t; + if (it.hasNext() || !isBoundedNumerical(t1, lv)) { + // not interval range, create unbounded comprehension term + ImmutableList _qvs = + ImmutableSLList.nil().prepend(lv); + while (it.hasNext()) { + _qvs = _qvs.prepend(it.next()); + } + t = unbounded.apply(declsType, nullable, _qvs, t1, t2); + } else { + t = bounded.apply(lv, lowerBound(t1, lv), upperBound(t1, lv), t2); + } + + if (resultType == null) { + resultType = services.getTypeConverter().getKeYJavaType(t2); + } + + // cast to specific JML type (fixes bug #1347) + return new SLExpression(t, resultType); + } + + public ImmutableList infflowspeclist(ImmutableList result) { return result; } @@ -763,6 +801,19 @@ private SLExpression buildBigintTruncationExpression(KeYJavaType resultType, JTe } } + private SLExpression buildMSetTruncationExpression(KeYJavaType resultType, JTerm term) { + assert term.sort() == services.getTypeConverter().getIntegerLDT().targetSort(); + + SpecMathMode mode = this.overloadedFunctionHandler.getSpecMathMode(); + if (mode == SpecMathMode.JAVA) { + return buildIntCastExpression(resultType, term); + } else { + KeYJavaType mset = services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET); + return new SLExpression(term, mset); + } + } + + private SLExpression buildIntCastExpression(KeYJavaType resultType, JTerm term) { IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT(); try { @@ -879,6 +930,33 @@ public SLExpression createSeqDef(SLExpression a, SLExpression b, SLExpression t, return new SLExpression(resultTerm, seqtype); } + /* + * public SLExpression createMSet(SLExpression a, SLExpression b, SLExpression t, + * + * KeYJavaType declsType, ImmutableList declVars) { + * if (!(declsType.getJavaType().equals(PrimitiveType.JAVA_INT) + * || declsType.getJavaType().equals(PrimitiveType.JAVA_BIGINT))) { + * throw exc.createException0( + * "multiset definition variable must be of type int or \\bigint"); + * } else if (declVars.size() != 1) { + * throw exc.createException0("multiset definition must declare exactly one variable"); + * } + * QuantifiableVariable qv = declVars.head(); + * Term tt = t.getTerm(); + * if (tt.sort() == JavaDLTheory.FORMULA) { + * // bugfix (CS): t.getTerm() delivers a formula instead of a + * // boolean term; obviously the original boolean terms are + * // converted to formulas somewhere else; however, we need + * // boolean terms instead of formulas here + * tt = tb.convertToBoolean(t.getTerm()); + * } + * Term resultTerm = tb.mset(qv, a.getTerm(), b.getTerm(), tt); + * final KeYJavaType msettype = services.getJavaInfo().getPrimitiveKeYJavaType("\\mset"); + * return new SLExpression(resultTerm, msettype); + * } + * + */ + public SLExpression createUnionF(boolean nullable, Pair> declVars, JTerm expr, JTerm guard) { final JavaInfo javaInfo = services.getJavaInfo(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index 9d71c0b7b94..13cd41045d6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -1743,8 +1743,12 @@ public SLExpression visitSpecquantifiedexpression( expr.getType()); case JmlLexer.MAX -> termFactory.quantifiedMax(guard, body, declVars.first, nullable, declVars.second); + case JmlLexer.MIN -> termFactory.quantifiedMin(guard, body, declVars.first, nullable, declVars.second); + case JmlLexer.MSET -> + termFactory.quantifiedMset(declVars.first, nullable, declVars.second, guard, body, + services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET)); case JmlLexer.NUM_OF -> { KeYJavaType kjtInt = services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_BIGINT); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/MSetRulesdefinition.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/MSetRulesdefinition.key new file mode 100644 index 00000000000..2255cee5b91 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/MSetRulesdefinition.key @@ -0,0 +1,590 @@ + +\rules{ + + defOfMSetEmpty{ + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetEmpty) + + \varcond(\notFreeIn(x, msetEl)) + \replacewith(mset{x;}(0, 0, msetEl)) + }; + + defOfMSetSingle{ + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetSingle(msetEl)) + + \varcond(\notFreeIn(x, msetEl)) + \replacewith(mset{x;}(0, 1, msetEl)) + }; + + // defOfMSetMul{ + // \schemaVar \term Mset m; + // \schemaVar \term any msetEl; + // \schemaVar \variables int x; + + // \find(msetMul(m, msetEl)) + // \varcond(\notFreeIn(x, m) , + // \notFreeIn(x, msetEl)) + + + // ???????????????} + + + //defOfMSetCard{ + + //???????????????} + + + defOfMSetUnion{ + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetUnion(m, s)) + \varcond(\notFree(x, m), + \notFree(x, s), + \notFree(x, msetEl)) + + \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(s, msetEl) = 0)) + \then(msetSum(m, s)) + \else(msetSum(m , s) - msetIntersec(m , s)) + + }; + + defOfMSetIntersec{ + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetIntersec(m, s)) + \varcond(\notFree(x, m), + \notFree(x, s), + \notFree(x, msetEl)) + + \replacewith(msetSum(m , s) - msetUnion(m, s)) + + }; + + defOfMSetSum{ + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetIntersec(m, s)) + \varcond(\notFree(x, m), + \notFree(x, s), + \notFree(x, msetEl)) + + \replacewith( mset(m) + mset(s)) + }; + + + defOfMSetDiff{ + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + \schemaVar \variables int x; + + \find(msetIntersec(m, s)) + \varcond(\notFree(x, m), + \notFree(x, s), + \notFree(x, msetEl)) + + \replacewith( mset(m) - mset(s)) + }; + + + \lemma + msetUnionWithMSetEmpty1{ + + \find(msetUnion(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + + \heuristics(concrete) + \displayname "msetUnionWithEmpty" + }; + + \lemma + msetUnionWithMSetEmpty2{ + \schemaVar \term Mset m; + + \find(msetUnion(m, msetEmpty)) + \replacewith(m) + + \heuristics(concrete) + \displayname "msetUnionWithEmpty" + }; + + \lemma + msetUnionWithMSetEmpty3{ + \schemaVar \term any msetEl; + + \find(msetUnion(msetSingle(msetEl), msetEmpty)) + \replacewith(msetSingle(msetEl)) + + \heuristics(concrete) + \displayname "msetUnionWithEmpty" + }; + + \lemma + msetUnionWithMSetSingle1{ + \schemaVar \term any msetEl; + + \find(msetUnion(msetSingle(msetEl), msetSingle(msetEl))) + \replacewith(msetSingle(msetEl)) + + \heuristics(concrete) + \displayname "msetUnionWithSingle" + }; + + \lemma + msetUnionWithMSetSingle2{ + \schemaVar \term any msetEl1, msetEl2; + + \find(msetUnion(msetSingle(msetEl1), msetSingle(msetEl2)) + \replacewith(msetSum(msetSingle(msetEl1), msetSingle(msetEl2)) + + \heuristics(concrete) + \displayname "msetUnionWithSingle" + }; + + \lemma + msetUnionWithSameMSets{ + \schemaVar \term Mset m; + + \find(msetUnion(m , m)) + \replacewith(m) + \heuristics(concrete) + + }; + + \lemma + msetUnionCommutativity{ + \schemaVar \term Mset m, s; + + \find(msetUnion(m, s)) + \replacewith(msetUnion(s, m)) + \heuristics(concrete) + + }; + + \lemma + msetUnionAssociativity{ + \schemaVar \term Mset m, s, t; + + \find(msetUnion(m, msetUnion(s, t))) + \replacewith(msetUnion(msetUnion(m, s) , t)) + \heuristics(concrete) + + }; + + \lemma + msetUnionWithMSetIntersection{ + \schemaVar \term Mset m, s; + + \find(msetUnion(m, msetIntersec(m, s))) + \replacewith(m) + heuristics(concrete) + + }; + + \lemma + msetUnionSubset{ + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + + + \find(msetUnion(m, s)) + \varcond( + \notFreeIn(msetEl, m), + \notFreeIn(msetEl, s) + ) + \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(s, msetEl) > 0 && msetIntersec(m, s) == s) + \then(m) + \else(msetUnion(m, s))) + }; + + + \lemma + msetIntersectionWithMSetEmpty1{ + + \find(msetIntersec(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + + \heuristics(concrete) + \displayname "msetIntersecWithEmpty" + }; + + \lemma + msetIntersectionWithMSetEmpty2{ + \schemaVar \term Mset m; + + \find(msetIntersec(m, msetEmpty)) + \replacewith(msetEmpty) + + \heuristics(concrete) + \displayname "msetIntersecWithEmpty" + }; + + \lemma + msetIntersectionWithMSetEmpty3{ + \schemaVar \term any msetEl; + + \find(msetIntersec(msetSingle(msetEl), msetEmpty)) + \replacewith(msetEmpty) + + \heuristics(concrete) + \displayname "msetIntersecWithEmpty" + }; + + \lemma + msetIntersectionWithMSetSingle1{ + \schemaVar \term any msetEl; + + \find(msetIntersec(msetSingle(msetEl), msetSingle(msetEl))) + \replacewith(msetSingle(msetEl)) + \heuristics(concrete) + \displayname "msetIntersecWithSingle" + + }; + + \lemma + msetIntersectionWithMSetSingle2{ + \schemaVar \term any msetEl1 , msetEl2; + + \find(msetIntersec(msetSingle(msetEl1), msetSingle(msetEl2))) + \replacewith(msetEmpty) + \heuristics(concrete) + \displayname "msetIntersecWithSingle" + + }; + + \lemma + msetIntersecWithSameMSets{ + \schemaVar \term Mset m; + + \find(msetIntersec(m , m)) + \replacewith(m) + \heuristics(concrete) + + }; + + \lemma + msetIntersecCommutativity{ + \schemaVar \term Mset m, s; + + \find(msetIntersec(m, s)) + \replacewith(msetIntersec(s, m)) + \heuristics(concrete) + + }; + + + \lemma + msetIntersecDifferent{ + \schemaVar \term Mset m, s; + + \find(msetIntersec(m, s)) + \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(s, msetEl) = 0) + \than(msetEmpty) + \else(msetIntersec(m,s))) + + \heuristics(concrete) + + }; + + \lemma + msetIntersecSubset{ + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + + \find(msetIntersec(m, s)) + \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(s, msetEl) > 0 && msetUnion(m, s) == m) + \than(s) + \else(msetIntersec(m, s))) + + \heuristics(concrete) + + }; + + \lemma + msetIntersecWithMSetUnion{ + \schemaVar \term Mset m, s, t; + + \find(msetIntersec(m, msetUnion(s,t))) + \replacewith(msetUnion(msetIntersec(m,s), msetIntersec(m, t))) + \heuristics(concrete) + + }; + + + + \lemma + msetSumWithMSetEmpty1{ + + \find(msetSum(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + + \heuristics(concrete) + \displayname "msetSumWithEmpty" + }; + + \lemma + msetSumWithMSetEmpty2{ + \schemaVar \term Mset m; + + \find(msetSum(m, msetEmpty)) + \replacewith(m) + + \heuristics(concrete) + \displayname "msetSumWithEmpty" + }; + + \lemma + msetSumWithMSetEmpty3{ + \schemaVar \term any msetEl; + + \find(msetSum(msetSingle(msetEl), msetEmpty)) + \replacewith(msetSingle(msetEl)) + + \heuristics(concrete) + \displayname "msetSumWithEmpty" + }; + + \lemma + msetSumWithMSetSingle1{ + \schemaVar \term any msetEl; + + \find(msetSum(msetSingle(msetEl), msetSingle(msetEl))) + \replacewith(msetSingle(msetEl) + msetSingle(msetEL)) + \heuristics(concrete) + \displayname "msetSumWithSingle" + + }; + + \lemma + \msetSumWithMSetSingle2{ + \schemaVar \term Mset m; + \schemaVar \term any msetEl; + + \find(msetSum(m, msetSingle(msetEl))) + \replacewith(m + msetSingle(msetEl)) + \heuristics(concrete) + \displayname "msetSumWithSingle" + + }; + + + \lemma + msetSumCommutativity { + \schemaVar \term Mset m, s; + \find(msetSum(m, s)) + \replacewith(msetSum(s, m)) + \heuristics(concrete) + }; + + \lemma + msetSumAssociativity { + \schemaVar \term Mset m, s, t; + \find(msetSum(m, msetSum(s, t))) + \replacewith(msetSum(msetSum(m, s), t)) + }; + + + \lemma + msetSummWithSameMSets{ + \schemaVar \term Mset m; + \find(msetSum(m,m)) + \replace(m * 2) + \heuristics(concrete) + + }; + + + + + + + \lemma + msetDiffWithMSetEmpty1{ + + \find(msetDiff(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + + \heuristics(concrete) + \displayname "msetDiffWithEmpty" + }; + + \lemma + msetDiffWithMSetEmpty2{ + \schemaVar \term Mset m; + + \find(msetDiff(m, msetEmpty)) + \replacewith(m) + + \heuristics(concrete) + \displayname "msetDiffWithEmpty" + }; + + \lemma + msetDiffWithMSetEmpty3{ + \schemaVar \term any msetEl; + + \find(msetDiff(msetSingle(msetEl), msetEmpty)) + \replacewith(msetSingle(msetEl)) + + \heuristics(concrete) + \displayname "msetDiffWithEmpty" + }; + + + + \lemma + \msetDiffWithMSetSingle1{ + \schemaVar \term any msetEl; + + \find(msetDiff(msetSingle(msetEl), msetSingle(msetEl))) + \replacewith(msetEmpty) + \heuristics(concrete) + \displayname "msetDiffWithSingle" + + }; + + \lemma + \msetDiffWithMSetSingle2{ + \schemaVar \term any msetEl1, msetEl2; + + \find(msetDiff(msetSingle(msetEl1), msetSingle(msetEl2))) + \replace(msetSum(msetSingle(msetEl1), msetSingle(msetEl2))) + + \heuristics(concrete) + \displayname "msetDiffWithSingle" + + }; + + \lemma + msetDiffWithMSetSingle3{ + \schemaVar \term Mset m; + \schemaVar \term any msetEl; + + \find(msetDiff(m, msetSingle(msetEl))) + \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(msetSingle(msetEl), msetEl) == 1) + \than(m) + \else(msetSum(m, msetSingle(msetEl)))) + + \heuristics(concrete) + \displayname "msetDiffWithSingle" + + }; + + \lemma + msetDiffCommutativity{ + \schemaVar \term Mset m, s; + \find(msetDiff(m, s)) + \replacewith(msetDiff(s, m)) + \heuristics(concrete) + + }; + + +mset_split { + \schemaVar \term int low, high; + \schemaVar \term int middle; + \variables int uSub, uSub1, uSub2; + + + \find(mset{uSub;}(low, high, t)) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, middle), + \notFreeIn(uSub, high)) + \replacewith(\if(low <= middle & middle <= high) + \then(msetSum(mset{uSub;}(low, middle, t), mset{uSub;}(middle, high, t))) + \else(mset{uSub;}(low, high, t))) + + \heuristics(comprehension_split, triggered) + + \trigger {middle} mset{uSub;}(low, middle, t) \avoid middle <= low, middle >= high; + }; + +} + + + + mset_Single{ + \schemaVar \term int low, high; + \schemaVar \term any t; + \schemaVar \variables int uSub; + + \find(mset{uSub;}(low, high, t)) + + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high)) + + \replacewith(\if(high - low = 1) + \then(msetSingle(t)) + \else(mset{uSub;}(low, high, t))) + + } + + +mset_extract_triggered_back_2 { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(tempMset{uSub;}(low, high, beta :: select(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith( + \if(low = high) + \then(msetSingle(beta :: select(h, array, arr(high)))) + \else(msetSum(tempMset{uSub;}(low, high - 1, beta :: select(h, array, arr(uSub))), + msetSingle(beta :: select(h, array, arr(high))))) + ) + \heuristics(simplify_ENLARGING) +}; + + + mset_extract_triggered_front { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(tempMset{uSub;}(low, high, beta::select(h,array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith(msetSum(msetSingle(beta::select(h,array, arr(low))), + tempMset{uSub;}(low+1, high, beta :: select(h, array, arr(uSub))))) + + \heuristics(comprehension_split, triggered) + \trigger {low} msetSingle(beta::select(h,array, arr(low))) + \avoid low >= high, false; + }; + + mset_extract_triggered_back { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(tempMset{uSub;}(low, high, beta::select(h,array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith(msetSum(msetSingle(beta::select(h,array, arr(high))), + tempMset{uSub;}(low, high-1, beta :: select(h, array, arr(uSub))))) + + \heuristics(comprehension_split, triggered) + \trigger {high} msetSingle(beta::select(h,array, arr(high))) + \avoid high <= low, false; + }; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key index 381662fdc6a..e0d541ac494 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key @@ -31,4 +31,5 @@ freeADT, wellfound, "./string/charListHeader.key", - types; + types, + msetRules; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key new file mode 100644 index 00000000000..69ea1baa650 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key @@ -0,0 +1,366 @@ +\sorts { + Mset; + \generic alpha, beta; +} + +\functions { + // Getters + int msetMul(Mset, any); + int msetCard(Mset); + + // Constructors + Mset msetEmpty; + Mset msetSingle(any); + Mset msetUnion(Mset, Mset); + Mset msetIntersec(Mset, Mset); + Mset msetDiff(Mset, Mset); + Mset msetSum(Mset, Mset); + Mset msetRange {false, false, true}(int, int, any); +} + +\rules { + + + // Rule: mset_Empty + mset_Empty { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term beta t; + + \find(msetRange{uSub;}(left, right ,t)) + \varcond(\notFreeIn(uSub, left)) + \replacewith(\if(right < left) + \then(msetEmpty) + \else(msetRange{uSub;}(left, right, t))) + + \heuristics(out_of_bounds) + + }; + + + // Rule: mset_Single + mset_Single { + \schemaVar \term int left; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \find(msetRange{uSub;}(left, left, beta::select(h,array, arr(uSub)))) + \sameUpdateLevel + \varcond(\notFreeIn(uSub, left)) + \replacewith(msetSingle({\subst uSub; left}(beta::select(h,array, arr(uSub))))) + \heuristics(simplify) + }; + + // Union Rules + msetUnionWithMSetEmpty1 { + \find(msetUnion(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + \heuristics(simplify) + \displayname "msetUnionWithEmpty" + }; + + msetUnionWithMSetEmpty2 { + \schemaVar \term Mset m; + \find(msetUnion(m, msetEmpty)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetUnionWithEmpty" + }; + + msetUnionWithSameMSets { + \schemaVar \term Mset m; + \find(msetUnion(m, m)) + \replacewith(m) + \heuristics(simplify) + }; + + msetUnionCommutativity { + \schemaVar \term Mset commLeft, commRight; + \find(msetUnion(commLeft, commRight)) + \replacewith(msetUnion(commRight, commLeft)) + \heuristics(polySimp_expand, polySimp_addOrder) + }; + + msetUnionAssociativity { + \schemaVar \term Mset addAssocPoly0, addAssocPoly1, addAssocMono; + \find(msetUnion(addAssocPoly0, msetUnion(addAssocPoly1, addAssocMono))) + \replacewith(msetUnion(msetUnion(addAssocPoly0, addAssocPoly1), addAssocMono)) + \heuristics(polySimp_expand, polySimp_addAssoc) + }; + + msetUnionWithMSetIntersection { + \schemaVar \term Mset m, s; + \find(msetUnion(m, msetIntersec(m, s))) + \replacewith(m) + \heuristics(simplify) + }; + + msetUnionSubset { + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + + \find(msetUnion(m, s)) + \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) > 0 & msetIntersec(m, s) = s) + \then(m) + \else(msetUnion(m, s))) + \heuristics(simplify) + }; + + // Intersection Rules + msetIntersectionWithMSetEmpty1 { + \find(msetIntersec(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + \heuristics(simplify) + \displayname "msetIntersecWithEmpty" + }; + + msetIntersectionWithMSetEmpty2 { + \schemaVar \term Mset m; + \find(msetIntersec(m, msetEmpty)) + \replacewith(msetEmpty) + \heuristics(simplify) + \displayname "msetIntersecWithEmpty" + }; + + msetIntersecWithSameMSets { + \schemaVar \term Mset m; + \find(msetIntersec(m, m)) + \replacewith(m) + \heuristics(simplify) + }; + + msetIntersecCommutativity { + \schemaVar \term Mset commLeft, commRight; + \find(msetIntersec(commLeft, commRight)) + \replacewith(msetIntersec(commRight, commLeft)) + \heuristics(polySimp_expand, polySimp_addOrder) + }; + + msetIntersecDifferent { + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + + \find(msetIntersec(m, s)) + \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) = 0) + \then(msetEmpty) + \else(msetIntersec(m, s))) + \heuristics(simplify) + }; + + msetIntersecSubset { + \schemaVar \term Mset m, s; + \schemaVar \term any msetEl; + + \find(msetIntersec(m, s)) + \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) > 0 & msetUnion(m, s) = m) + \then(s) + \else(msetIntersec(m, s))) + \heuristics(simplify) + }; + + msetIntersecWithMSetUnion { + \schemaVar \term Mset m, s, t; + \find(msetIntersec(m, msetUnion(s, t))) + \replacewith(msetUnion(msetIntersec(m, s), msetIntersec(m, t))) + \heuristics(simplify) + }; + + // Sum Rules + msetSumWithMSetEmpty1 { + \schemaVar \term Mset m; + \find(msetSum(msetEmpty, m)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetSumWithEmpty" + }; + + msetSumWithMSetEmpty2 { + \schemaVar \term Mset m; + \find(msetSum(m, msetEmpty)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetSumWithEmpty" + }; + + msetSumCommutativity { + \schemaVar \term Mset commLeft, commRight; + \find(msetSum(commLeft, commRight)) + \replacewith(msetSum(commRight, commLeft)) + \heuristics(polySimp_expand, polySimp_addOrder) + }; + + msetSumAssociativity { + \schemaVar \term Mset addAssocPoly0, addAssocPoly1, addAssocMono; + \find(msetSum(addAssocPoly0, msetSum(addAssocPoly1, addAssocMono))) + \replacewith(msetSum(msetSum(addAssocPoly0, addAssocPoly1), addAssocMono)) + \heuristics(polySimp_expand, polySimp_addAssoc) + }; + + // Difference Rules + msetDiffWithMSetEmpty1 { + \find(msetDiff(msetEmpty, msetEmpty)) + \replacewith(msetEmpty) + \heuristics(simplify) + \displayname "msetDiffWithEmpty" + }; + + msetDiffWithMSetEmpty2 { + \schemaVar \term Mset m; + \find(msetDiff(m, msetEmpty)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetDiffWithEmpty" + }; + + msetDiffCommutativity { + \schemaVar \term Mset commLeft, commRight; + \find(msetDiff(commLeft, commRight)) + \replacewith(msetDiff(commRight, commLeft)) + \heuristics(polySimp_expand, polySimp_addOrder) + }; + + // Rule: mset_split + mset_split { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \variables int uSub; + \schemaVar \term beta t; + + \find(msetRange{uSub;}(left, right, t)) + \varcond(\notFreeIn(uSub, left), + \notFreeIn(uSub, middle), + \notFreeIn(uSub, right)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum(msetRange{uSub;}(left, middle-1, t), + msetRange{uSub;}(middle, right, t))) + \else(msetRange{uSub;}(left, right, t))) + }; + + + mset_extract_triggered { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange{uSub;}(left, right, beta::select(h,array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), + \notFreeIn(uSub, middle), + \notFreeIn(uSub, right), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta::select(h,array, arr(uSub))), + msetSingle(beta::select(h,array, arr(middle)))), + msetRange{uSub;}(middle+1, right, beta::select(h,array, arr(uSub))))) + \else(msetRange{uSub;}(left, right, beta::select(h,array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {middle} msetSingle(beta::select(h,array, arr(middle))) + \avoid middle <= -1 + left, right <= -1 + middle; + }; + + + + mset_extract_array { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \variables int uSub; + \schemaVar \term alpha x; + + \find(msetRange{uSub;}(left, right, beta :: select(store(h, array, arr(middle), x), array, arr(uSub)))) + + \varcond(\notFreeIn(uSub, left), + \notFreeIn(uSub, middle), + \notFreeIn(uSub, right)) + + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta :: select(h, array, arr(uSub))), + msetSingle({\subst uSub; middle}x)), + msetRange{uSub;}(middle+1, right, beta :: select(h, array, arr(uSub))))) + \else(msetRange{uSub;}(left, right, beta :: select(h, array, arr(uSub))))) + + \heuristics(simplify_ENLARGING) + }; + + mset_extract_array_front { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \term alpha x; + + \find(msetRange{uSub;}(left, right, beta :: select(store(h, array, arr(left), x), array, arr(uSub)))) + + \varcond(\notFreeIn(uSub, left), + \notFreeIn(uSub, right)) + + \replacewith(msetSum(msetSingle({\subst uSub; left}x), + msetRange{uSub;}(left+1, right, beta::select(h, array, arr(uSub))))) + + \heuristics(simplify_enlarging) + }; + + mset_extract_array_back { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \term alpha x; + + \find(msetRange{uSub;}(left, right, beta :: select(store(h, array, arr(right), x), array, arr(uSub)))) + + \varcond(\notFreeIn(uSub, left), + \notFreeIn(uSub, right)) + + + \replacewith(msetSum(msetRange{uSub;}(left, right-1, beta::select(h, array, arr(uSub))), + msetSingle({\subst uSub; right}x))) + + \heuristics(simplify_enlarging) + }; + + + mset_extract_triggered_front { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange{uSub;}(low, high, beta::select(h,array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith(msetSum(msetSingle(beta::select(h,array, arr(low))), + msetRange{uSub;}(low+1, high, beta :: select(h, array, arr(uSub))))) + + \heuristics(comprehension_split, triggered) + \trigger {low} msetSingle(beta::select(h,array, arr(low))) + \avoid low >= high, false; + }; + + mset_extract_triggered_back { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange{uSub;}(low, high, beta::select(h,array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), + \notFreeIn(uSub, high), + \notFreeIn(uSub, h), + \notFreeIn(uSub, array)) + \replacewith(msetSum(msetSingle(beta::select(h,array, arr(high))), + msetRange{uSub;}(low, high-1, beta :: select(h, array, arr(uSub))))) + + \heuristics(comprehension_split, triggered) + \trigger {high} msetSingle(beta::select(h,array, arr(high))) + \avoid high <= low, false; + }; + + + +} From 1029eba0e42820c0ea663c472227ee8026190ec7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Tue, 9 Dec 2025 16:27:16 +0100 Subject: [PATCH 2/6] refactoring mset files --- .../expression/literal/EmptyMSetLiteral.java | 3 +- .../key/java/visitor/CreatingASTVisitor.java | 3 +- .../ilkd/key/java/visitor/JavaASTVisitor.java | 15 +- .../de/uka/ilkd/key/java/visitor/Visitor.java | 1 - .../java/de/uka/ilkd/key/ldt/MSetLDT.java | 6 +- .../de/uka/ilkd/key/pp/PrettyPrinter.java | 6 +- .../de/uka/ilkd/key/proof/rules/msetRules.key | 268 ++++++++---------- 7 files changed, 129 insertions(+), 173 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java index af03e8f328e..6746a885cd3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMSetLiteral.java @@ -14,8 +14,7 @@ public non-sealed class EmptyMSetLiteral extends Literal { public static final EmptyMSetLiteral INSTANCE = new EmptyMSetLiteral(); - private EmptyMSetLiteral() { - } + private EmptyMSetLiteral() {} @Override public boolean equals(Object o) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java index bf544d4859d..a35e0b3e297 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -6,7 +6,7 @@ import java.util.ArrayDeque; import java.util.Deque; -import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.declaration.ClassInitializer; import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; @@ -19,6 +19,7 @@ import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; import de.uka.ilkd.key.java.ast.expression.operator.mst.*; +import de.uka.ilkd.key.java.ast.expression.operator.mst.MSetSum; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.op.IProgramVariable; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java index 735dfb438c8..8bd89a3122e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.visitor; -import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.ccatch.*; import de.uka.ilkd.key.java.ast.declaration.*; @@ -11,20 +11,13 @@ import de.uka.ilkd.key.java.ast.expression.ParenthesizedExpression; import de.uka.ilkd.key.java.ast.expression.PassiveExpression; import de.uka.ilkd.key.java.ast.expression.literal.*; -import de.uka.ilkd.key.java.ast.expression.literal.EmptyMSetLiteral; import de.uka.ilkd.key.java.ast.expression.operator.*; -import de.uka.ilkd.key.java.ast.expression.operator.Subtype; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.logic.op.IProgramMethod; -import de.uka.ilkd.key.logic.op.IProgramVariable; -import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.ProgramConstant; -import de.uka.ilkd.key.logic.op.ProgramSV; -import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.AbstractProgramElement; import de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer; import de.uka.ilkd.key.speclang.BlockContract; @@ -254,7 +247,9 @@ public void performActionOnSeqPut(SeqPut x) { public void performActionOnMSetIntersect(MSetIntersect x) { doDefaultAction(x); } @Override - public void performActionOnMSetSum(MSetSum x) { doDefaultAction(x); } + public void performActionOnMSetSum(MSetSum x) { + doDefaultAction(x); + } @Override public void performActionOnMSetDiff(MSetDiff x) { doDefaultAction(x); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index 51b6c33d181..7b61264883c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -10,7 +10,6 @@ import de.uka.ilkd.key.java.ast.expression.ParenthesizedExpression; import de.uka.ilkd.key.java.ast.expression.PassiveExpression; import de.uka.ilkd.key.java.ast.expression.literal.*; -import de.uka.ilkd.key.java.ast.expression.literal.EmptyMSetLiteral; import de.uka.ilkd.key.java.ast.expression.operator.*; import de.uka.ilkd.key.java.ast.expression.operator.Subtype; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java index 25cd59f92b3..7c8092b5c1b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java @@ -81,7 +81,8 @@ public JFunction getMsetRemove() { @Override public boolean isResponsible(Operator op, JTerm[] subs, Services services, ExecutionContext ec) { - return op instanceof MSetCard || op instanceof MSetMul || op instanceof MSetSingle + return op instanceof MSetCard || op instanceof MSetMul + || op instanceof de.uka.ilkd.key.java.ast.expression.operator.mst.MSetSingle || op instanceof MSetIntersect || op instanceof MSetDiff || op instanceof MSetUnion || op instanceof MSetSum; } @@ -89,7 +90,8 @@ public boolean isResponsible(Operator op, JTerm[] subs, Services services, @Override public boolean isResponsible(Operator op, JTerm left, JTerm right, Services services, ExecutionContext ec) { - return op instanceof MSetUnion || op instanceof MSetIntersect || op instanceof MSetSum + return op instanceof MSetUnion || op instanceof MSetIntersect + || op instanceof de.uka.ilkd.key.java.ast.expression.operator.mst.MSetSum || op instanceof MSetDiff; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index a176c80c747..74985d1ee89 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -7,6 +7,9 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; +import de.uka.ilkd.key.java.ast.Statement; +import de.uka.ilkd.key.java.ast.StatementBlock; +import de.uka.ilkd.key.java.ast.StatementContainer; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.abstraction.Type; import de.uka.ilkd.key.java.ast.ccatch.*; @@ -673,7 +676,8 @@ public void performActionOnTypeReference(TypeReference x, boolean fullTypeNames) } } - private void printTypeReference(ReferencePrefix prefix, @Nullable KeYJavaType type, + private void printTypeReference(ReferencePrefix prefix, + @Nullable KeYJavaType type, ProgramElementName name, boolean fullTypeNames) { printReferencePrefix(prefix); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key index 69ea1baa650..d3d6132f34c 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key @@ -20,38 +20,33 @@ \rules { + mset_Empty { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term beta t; - // Rule: mset_Empty - mset_Empty { - \schemaVar \term int left, right; - \schemaVar \variables int uSub; - \schemaVar \term beta t; - - \find(msetRange{uSub;}(left, right ,t)) - \varcond(\notFreeIn(uSub, left)) - \replacewith(\if(right < left) + \find(msetRange{uSub;}(left, right ,t)) + \varcond(\notFreeIn(uSub, left)) + \replacewith(\if(right < left) \then(msetEmpty) \else(msetRange{uSub;}(left, right, t))) - \heuristics(out_of_bounds) - - }; - + \heuristics(out_of_bounds) + }; - // Rule: mset_Single mset_Single { - \schemaVar \term int left; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; + \schemaVar \term int left; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \find(msetRange{uSub;}(left, left, beta::select(h,array, arr(uSub)))) \sameUpdateLevel - \varcond(\notFreeIn(uSub, left)) + \varcond(\notFreeIn(uSub, left)) \replacewith(msetSingle({\subst uSub; left}(beta::select(h,array, arr(uSub))))) \heuristics(simplify) }; - // Union Rules msetUnionWithMSetEmpty1 { \find(msetUnion(msetEmpty, msetEmpty)) \replacewith(msetEmpty) @@ -101,12 +96,11 @@ \find(msetUnion(m, s)) \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) > 0 & msetIntersec(m, s) = s) - \then(m) - \else(msetUnion(m, s))) + \then(m) + \else(msetUnion(m, s))) \heuristics(simplify) }; - // Intersection Rules msetIntersectionWithMSetEmpty1 { \find(msetIntersec(msetEmpty, msetEmpty)) \replacewith(msetEmpty) @@ -142,8 +136,8 @@ \find(msetIntersec(m, s)) \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) = 0) - \then(msetEmpty) - \else(msetIntersec(m, s))) + \then(msetEmpty) + \else(msetIntersec(m, s))) \heuristics(simplify) }; @@ -153,8 +147,8 @@ \find(msetIntersec(m, s)) \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) > 0 & msetUnion(m, s) = m) - \then(s) - \else(msetIntersec(m, s))) + \then(s) + \else(msetIntersec(m, s))) \heuristics(simplify) }; @@ -165,9 +159,8 @@ \heuristics(simplify) }; - // Sum Rules msetSumWithMSetEmpty1 { - \schemaVar \term Mset m; + \schemaVar \term Mset m; \find(msetSum(msetEmpty, m)) \replacewith(m) \heuristics(simplify) @@ -196,7 +189,6 @@ \heuristics(polySimp_expand, polySimp_addAssoc) }; - // Difference Rules msetDiffWithMSetEmpty1 { \find(msetDiff(msetEmpty, msetEmpty)) \replacewith(msetEmpty) @@ -219,7 +211,6 @@ \heuristics(polySimp_expand, polySimp_addOrder) }; - // Rule: mset_split mset_split { \schemaVar \term int left, right; \schemaVar \term int middle; @@ -227,140 +218,105 @@ \schemaVar \term beta t; \find(msetRange{uSub;}(left, right, t)) - \varcond(\notFreeIn(uSub, left), - \notFreeIn(uSub, middle), - \notFreeIn(uSub, right)) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) \replacewith(\if(left <= middle & middle <= right) \then(msetSum(msetRange{uSub;}(left, middle-1, t), msetRange{uSub;}(middle, right, t))) \else(msetRange{uSub;}(left, right, t))) }; + mset_extract_triggered { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; - mset_extract_triggered { - \schemaVar \term int left, right; - \schemaVar \term int middle; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - - \find(msetRange{uSub;}(left, right, beta::select(h,array, arr(uSub)))) - \varcond(\notFreeIn(uSub, left), - \notFreeIn(uSub, middle), - \notFreeIn(uSub, right), - \notFreeIn(uSub, h), - \notFreeIn(uSub, array)) - \replacewith(\if(left <= middle & middle <= right) - \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta::select(h,array, arr(uSub))), - msetSingle(beta::select(h,array, arr(middle)))), - msetRange{uSub;}(middle+1, right, beta::select(h,array, arr(uSub))))) - \else(msetRange{uSub;}(left, right, beta::select(h,array, arr(uSub))))) - \heuristics(comprehension_split, triggered) - \trigger {middle} msetSingle(beta::select(h,array, arr(middle))) - \avoid middle <= -1 + left, right <= -1 + middle; - }; - - - - mset_extract_array { - \schemaVar \term int left, right; - \schemaVar \term int middle; - \schemaVar \term Heap h; - \schemaVar \term Object array; - \schemaVar \variables int uSub; - \schemaVar \term alpha x; - - \find(msetRange{uSub;}(left, right, beta :: select(store(h, array, arr(middle), x), array, arr(uSub)))) - - \varcond(\notFreeIn(uSub, left), - \notFreeIn(uSub, middle), - \notFreeIn(uSub, right)) - - \replacewith(\if(left <= middle & middle <= right) - \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta :: select(h, array, arr(uSub))), - msetSingle({\subst uSub; middle}x)), - msetRange{uSub;}(middle+1, right, beta :: select(h, array, arr(uSub))))) - \else(msetRange{uSub;}(left, right, beta :: select(h, array, arr(uSub))))) - - \heuristics(simplify_ENLARGING) - }; - - mset_extract_array_front { - \schemaVar \term int left, right; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - \schemaVar \term alpha x; - - \find(msetRange{uSub;}(left, right, beta :: select(store(h, array, arr(left), x), array, arr(uSub)))) - - \varcond(\notFreeIn(uSub, left), - \notFreeIn(uSub, right)) - - \replacewith(msetSum(msetSingle({\subst uSub; left}x), - msetRange{uSub;}(left+1, right, beta::select(h, array, arr(uSub))))) - - \heuristics(simplify_enlarging) - }; - - mset_extract_array_back { - \schemaVar \term int left, right; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - \schemaVar \term alpha x; - - \find(msetRange{uSub;}(left, right, beta :: select(store(h, array, arr(right), x), array, arr(uSub)))) - - \varcond(\notFreeIn(uSub, left), - \notFreeIn(uSub, right)) - - - \replacewith(msetSum(msetRange{uSub;}(left, right-1, beta::select(h, array, arr(uSub))), - msetSingle({\subst uSub; right}x))) - - \heuristics(simplify_enlarging) - }; - - - mset_extract_triggered_front { - \schemaVar \term int low, high; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - - \find(msetRange{uSub;}(low, high, beta::select(h,array, arr(uSub)))) - \varcond(\notFreeIn(uSub, low), - \notFreeIn(uSub, high), - \notFreeIn(uSub, h), - \notFreeIn(uSub, array)) - \replacewith(msetSum(msetSingle(beta::select(h,array, arr(low))), - msetRange{uSub;}(low+1, high, beta :: select(h, array, arr(uSub))))) - - \heuristics(comprehension_split, triggered) - \trigger {low} msetSingle(beta::select(h,array, arr(low))) - \avoid low >= high, false; - }; - - mset_extract_triggered_back { - \schemaVar \term int low, high; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - - \find(msetRange{uSub;}(low, high, beta::select(h,array, arr(uSub)))) - \varcond(\notFreeIn(uSub, low), - \notFreeIn(uSub, high), - \notFreeIn(uSub, h), - \notFreeIn(uSub, array)) - \replacewith(msetSum(msetSingle(beta::select(h,array, arr(high))), - msetRange{uSub;}(low, high-1, beta :: select(h, array, arr(uSub))))) + \find(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta::select(h, array, arr(uSub))), + msetSingle(beta::select(h, array, arr(middle)))), + msetRange{uSub;}(middle+1, right, beta::select(h, array, arr(uSub))))) + \else(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {middle} msetSingle(beta::select(h, array, arr(middle))) + \avoid middle <= -1 + left, right <= -1 + middle; + }; - \heuristics(comprehension_split, triggered) - \trigger {high} msetSingle(beta::select(h,array, arr(high))) - \avoid high <= low, false; - }; + mset_extract_array { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \variables int uSub; + \schemaVar \term alpha x; + + \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(middle), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta::select(h, array, arr(uSub))), + msetSingle({\subst uSub; middle} x)), + msetRange{uSub;}(middle+1, right, beta::select(h, array, arr(uSub))))) + \else(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub))))) + \heuristics(simplify_ENLARGING) + }; + + mset_extract_array_front { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \term alpha x; + + \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(left), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) + \replacewith(msetSum(msetSingle({\subst uSub; left} x), + msetRange{uSub;}(left+1, right, beta::select(h, array, arr(uSub))))) + \heuristics(simplify_enlarging) + }; + mset_extract_array_back { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \term alpha x; + + \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(right), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) + \replacewith(msetSum(msetRange{uSub;}(left, right-1, beta::select(h, array, arr(uSub))), + msetSingle({\subst uSub; right} x))) + \heuristics(simplify_enlarging) + }; + mset_extract_triggered_front { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange{uSub;}(low, high, beta::select(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) + \replacewith(msetSum(msetSingle(beta::select(h, array, arr(low))), + msetRange{uSub;}(low+1, high, beta::select(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {low} msetSingle(beta::select(h, array, arr(low))) + \avoid low >= high, false; + }; + mset_extract_triggered_back { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange{uSub;}(low, high, beta::select(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) + \replacewith(msetSum(msetSingle(beta::select(h, array, arr(high))), + msetRange{uSub;}(low, high-1, beta::select(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {high} msetSingle(beta::select(h, array, arr(high))) + \avoid high <= low, false; + }; } From e5d82ea549bbc695ab979f785336a0e54d27b715 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Thu, 11 Dec 2025 17:23:06 +0100 Subject: [PATCH 3/6] MSetSingle also works for other terms --- .../de/uka/ilkd/key/proof/rules/msetRules.key | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key index d3d6132f34c..6375739a3cc 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key @@ -25,7 +25,7 @@ \schemaVar \variables int uSub; \schemaVar \term beta t; - \find(msetRange{uSub;}(left, right ,t)) + \find(msetRange{uSub;}(left, right, t)) \varcond(\notFreeIn(uSub, left)) \replacewith(\if(right < left) \then(msetEmpty) @@ -37,13 +37,11 @@ mset_Single { \schemaVar \term int left; \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; + \schemaVar \term beta t; - \find(msetRange{uSub;}(left, left, beta::select(h,array, arr(uSub)))) + \find(msetRange{uSub;}(left, left, t)) \sameUpdateLevel - \varcond(\notFreeIn(uSub, left)) - \replacewith(msetSingle({\subst uSub; left}(beta::select(h,array, arr(uSub))))) + \replacewith(msetSingle({\subst uSub; left}(t))) \heuristics(simplify) }; From 2505c67e31e228df5c008295cf949a20264a8660 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Thu, 11 Dec 2025 17:28:06 +0100 Subject: [PATCH 4/6] added quicksort example --- .../heap/quicksort_mset/Quicksort.java | 77 +++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 key.ui/examples/heap/quicksort_mset/Quicksort.java diff --git a/key.ui/examples/heap/quicksort_mset/Quicksort.java b/key.ui/examples/heap/quicksort_mset/Quicksort.java new file mode 100644 index 00000000000..a4c013082ac --- /dev/null +++ b/key.ui/examples/heap/quicksort_mset/Quicksort.java @@ -0,0 +1,77 @@ +/** + * This shows how MultiSets can be used to verify the permutation property + * of a sorting algorithm. + * FIXME: The sortedness property is NOT shown. + * The source code is the same as quicksort/QuickSort.java but the present + * specification is proven automatically, without proof scripts. + * + * @author Silvia Zoraqi, Lukas Grätz, 2025 + * + * based on: + * @author Mattias Ulbrich, 2015 + */ + +class Quicksort { + + /*@ public normal_behaviour + @ ensures (\mset int k; 0 <= k < array.length; array[k]) == \old((\mset int k; 0 <= k < array.length; array[k])); + @ assignable array[*]; + @*/ + public void sort(int[] array) { + if(array.length > 0) { + sort(array, 0, array.length-1); + } + } + + /*@ public normal_behaviour + @ requires 0 <= from; + @ requires to < array.length; + @ ensures (\mset int k; 0 <= k < array.length; array[k]) == \old((\mset int k; 0 <= k < array.length; array[k])); + @ assignable array[*]; + @ measured_by to - from + 1; + @*/ + private void sort(int[] array, int from, int to) { + if(from < to) { + int splitPoint = split(array, from, to); + sort(array, from, splitPoint-1); + sort(array, splitPoint+1, to); + } + } + + /*@ public normal_behaviour + @ requires 0 <= from && from < to && to <= array.length-1; + @ ensures (\mset int k; 0 <= k < array.length; array[k]) == \old((\mset int k; 0 <= k < array.length; array[k])); + @ ensures from <= \result && \result <= to; + @ assignable array[*]; + @*/ + private int split(int[] array, int from, int to) { + + int i = from; + int pivot = array[to]; + + /*@ + @ loop_invariant from <= i && i <= j; + @ loop_invariant from <= j && j <= to; + @ loop_invariant (\mset int k; 0 <= k < array.length; array[k]) == \old((\mset int k; 0 <= k < array.length; array[k])); + @ decreases to + to - j - i + 2; + @ assignable array[*]; + @*/ + for(int j = from; j < to; j++) { + if(array[j] <= pivot) { + int t = array[i]; + array[i] = array[j]; + array[j] = t; + i++; + } + } + + // FIXME: this assignment has no effect, it should be a loop invariant + pivot = array[to]; + + array[to] = array[i]; + array[i] = pivot; + + return i; + + } +} From 5e9aa6caa28653ffbc4659ee6748f3232975871d Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 28 Jun 2026 06:09:19 +0200 Subject: [PATCH 5/6] fix old syntax and wrong heuristic. --- .../de/uka/ilkd/key/proof/rules/msetRules.key | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key index 6375739a3cc..f96ab521602 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key @@ -31,7 +31,7 @@ \then(msetEmpty) \else(msetRange{uSub;}(left, right, t))) - \heuristics(out_of_bounds) + \heuristics(simplify) }; mset_Single { @@ -230,15 +230,15 @@ \schemaVar \term Heap h; \schemaVar \term Object array; - \find(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub)))) + \find(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub)))) \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) \replacewith(\if(left <= middle & middle <= right) - \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta::select(h, array, arr(uSub))), - msetSingle(beta::select(h, array, arr(middle)))), - msetRange{uSub;}(middle+1, right, beta::select(h, array, arr(uSub))))) - \else(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub))))) + \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, select<[beta]>(h, array, arr(uSub))), + msetSingle(select<[beta]>(h, array, arr(middle)))), + msetRange{uSub;}(middle+1, right, select<[beta]>(h, array, arr(uSub))))) + \else(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub))))) \heuristics(comprehension_split, triggered) - \trigger {middle} msetSingle(beta::select(h, array, arr(middle))) + \trigger {middle} msetSingle(select<[beta]>(h, array, arr(middle))) \avoid middle <= -1 + left, right <= -1 + middle; }; @@ -250,13 +250,13 @@ \schemaVar \variables int uSub; \schemaVar \term alpha x; - \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(middle), x), array, arr(uSub)))) + \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(middle), x), array, arr(uSub)))) \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) \replacewith(\if(left <= middle & middle <= right) - \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta::select(h, array, arr(uSub))), + \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, select<[beta]>(h, array, arr(uSub))), msetSingle({\subst uSub; middle} x)), - msetRange{uSub;}(middle+1, right, beta::select(h, array, arr(uSub))))) - \else(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub))))) + msetRange{uSub;}(middle+1, right, select<[beta]>(h, array, arr(uSub))))) + \else(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub))))) \heuristics(simplify_ENLARGING) }; @@ -267,10 +267,10 @@ \schemaVar \term Object array; \schemaVar \term alpha x; - \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(left), x), array, arr(uSub)))) + \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(left), x), array, arr(uSub)))) \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) \replacewith(msetSum(msetSingle({\subst uSub; left} x), - msetRange{uSub;}(left+1, right, beta::select(h, array, arr(uSub))))) + msetRange{uSub;}(left+1, right, select<[beta]>(h, array, arr(uSub))))) \heuristics(simplify_enlarging) }; @@ -281,9 +281,9 @@ \schemaVar \term Object array; \schemaVar \term alpha x; - \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(right), x), array, arr(uSub)))) + \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(right), x), array, arr(uSub)))) \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) - \replacewith(msetSum(msetRange{uSub;}(left, right-1, beta::select(h, array, arr(uSub))), + \replacewith(msetSum(msetRange{uSub;}(left, right-1, select<[beta]>(h, array, arr(uSub))), msetSingle({\subst uSub; right} x))) \heuristics(simplify_enlarging) }; @@ -294,12 +294,12 @@ \schemaVar \term Heap h; \schemaVar \term Object array; - \find(msetRange{uSub;}(low, high, beta::select(h, array, arr(uSub)))) + \find(msetRange{uSub;}(low, high, select<[beta]>(h, array, arr(uSub)))) \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) - \replacewith(msetSum(msetSingle(beta::select(h, array, arr(low))), - msetRange{uSub;}(low+1, high, beta::select(h, array, arr(uSub))))) + \replacewith(msetSum(msetSingle(select<[beta]>(h, array, arr(low))), + msetRange{uSub;}(low+1, high, select<[beta]>(h, array, arr(uSub))))) \heuristics(comprehension_split, triggered) - \trigger {low} msetSingle(beta::select(h, array, arr(low))) + \trigger {low} msetSingle(select<[beta]>(h, array, arr(low))) \avoid low >= high, false; }; @@ -309,12 +309,12 @@ \schemaVar \term Heap h; \schemaVar \term Object array; - \find(msetRange{uSub;}(low, high, beta::select(h, array, arr(uSub)))) + \find(msetRange{uSub;}(low, high, select<[beta]>(h, array, arr(uSub)))) \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) - \replacewith(msetSum(msetSingle(beta::select(h, array, arr(high))), - msetRange{uSub;}(low, high-1, beta::select(h, array, arr(uSub))))) + \replacewith(msetSum(msetSingle(select<[beta]>(h, array, arr(high))), + msetRange{uSub;}(low, high-1, select<[beta]>(h, array, arr(uSub))))) \heuristics(comprehension_split, triggered) - \trigger {high} msetSingle(beta::select(h, array, arr(high))) + \trigger {high} msetSingle(select<[beta]>(h, array, arr(high))) \avoid high <= low, false; }; } From 6d68f205ee9ea50c11d7312fd365729d1d53f2a9 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 19:33:34 +0200 Subject: [PATCH 6/6] Intermediate commit (compiles, but does not work yet) --- key.core/src/main/antlr4/JmlLexer.g4 | 2 +- key.core/src/main/antlr4/JmlParser.g4 | 4 +- .../java/de/uka/ilkd/key/ldt/MSetLDT.java | 139 +++++--- .../de/uka/ilkd/key/logic/TermBuilder.java | 31 +- .../key/speclang/njml/JmlTermFactory.java | 68 +--- .../ilkd/key/speclang/njml/Translator.java | 19 +- .../de/uka/ilkd/key/proof/rules/ldt.key | 2 +- .../msetAxioms.key} | 294 ---------------- .../ilkd/key/proof/rules/mset/msetHeader.key | 18 + .../ilkd/key/proof/rules/mset/msetRules.key | 210 ++++++++++++ .../de/uka/ilkd/key/proof/rules/msetRules.key | 320 ------------------ .../ilkd/key/proof/rules/standardRules.key | 1 + 12 files changed, 363 insertions(+), 745 deletions(-) rename key.core/src/main/resources/de/uka/ilkd/key/proof/rules/{MSetRulesdefinition.key => mset/msetAxioms.key} (56%) create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetHeader.key create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetRules.key delete mode 100644 key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key diff --git a/key.core/src/main/antlr4/JmlLexer.g4 b/key.core/src/main/antlr4/JmlLexer.g4 index 92ff7ab68ad..32c67b64e4b 100644 --- a/key.core/src/main/antlr4/JmlLexer.g4 +++ b/key.core/src/main/antlr4/JmlLexer.g4 @@ -275,7 +275,7 @@ MAP_UPDATE: '\\map_update'; //KeY extension, not official JML MAX: '\\max'; E_MEASURED_BY: '\\measured_by' -> type(MEASURED_BY); MIN: '\\min'; -MSET: '\\mset'; //KeY extension, not official JML +MSET: '\\msetRange'; //KeY extension, not official JML NEWELEMSFRESH: '\\new_elems_fresh'; //KeY extension, not official JML NEW_OBJECTS: '\\new_objects'; //KeY extension, not official JML NONNULLELEMENTS: '\\nonnullelements'; diff --git a/key.core/src/main/antlr4/JmlParser.g4 b/key.core/src/main/antlr4/JmlParser.g4 index e93126bf05d..275820bd243 100644 --- a/key.core/src/main/antlr4/JmlParser.g4 +++ b/key.core/src/main/antlr4/JmlParser.g4 @@ -356,6 +356,7 @@ jmlprimary | java_math_expression #primaryJavaMathExpression | beforeexpression #pignore6 | transactionUpdated #pignore7 + | msetrangeterm #pignore8 | BACKUP LPAREN expression RPAREN #primaryBackup | PERMISSION LPAREN expression RPAREN #primaryPermission | NONNULLELEMENTS LPAREN expression RPAREN #primaryNNE @@ -417,7 +418,7 @@ sequence mapExpression: MAP_GET | MAP_OVERRIDE | MAP_UPDATE | MAP_REMOVE | IN_DOMAIN | DOMAIN_IMPLIES_CREATED | MAP_SIZE | MAP_SINGLETON | IS_FINITE; fpOperator: FP_ABS | FP_INFINITE | FP_NAN | FP_NEGATIVE | FP_NICE | FP_NORMAL | FP_POSITIVE | FP_SUBNORMAL; -quantifier: FORALL | EXISTS | MIN | MAX | NUM_OF | PRODUCT | SUM | MSET; +quantifier: FORALL | EXISTS | MIN | MAX | NUM_OF | PRODUCT | SUM; infinite_union_expr: LPAREN UNIONINF (boundvarmodifiers)? quantifiedvardecls SEMI (predicate SEMI)* storeref RPAREN; specquantifiedexpression: LPAREN quantifier (boundvarmodifiers)? quantifiedvardecls SEMI (expression SEMI)? expression RPAREN; oldexpression: (PRE LPAREN expression RPAREN | OLD LPAREN expression (COMMA IDENT)? RPAREN); @@ -426,6 +427,7 @@ safe_math_expression: (SAFE_MATH LPAREN expression RPAREN); bigint_math_expression: (BIGINT_MATH LPAREN expression RPAREN); beforeexpression: (BEFORE LPAREN expression RPAREN); bsumterm: LPAREN BSUM quantifiedvardecls SEMI (expression SEMI expression SEMI expression) RPAREN; +msetrangeterm: LPAREN MSET quantifiedvardecls SEMI (expression SEMI expression SEMI expression) RPAREN; seqdefterm: LPAREN SEQDEF quantifiedvardecls SEMI (expression SEMI expression SEMI expression) RPAREN; quantifiedvardecls: typespec quantifiedvariabledeclarator (COMMA quantifiedvariabledeclarator)*; boundvarmodifiers: (NON_NULL | NULLABLE); diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java index 7c8092b5c1b..0ef9fdae04e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/MSetLDT.java @@ -8,76 +8,110 @@ import de.uka.ilkd.key.java.ast.expression.Expression; import de.uka.ilkd.key.java.ast.expression.Operator; import de.uka.ilkd.key.java.ast.expression.literal.*; -import de.uka.ilkd.key.java.ast.expression.operator.*; -import de.uka.ilkd.key.java.ast.expression.operator.adt.*; import de.uka.ilkd.key.java.ast.expression.operator.mst.*; import de.uka.ilkd.key.java.ast.reference.ExecutionContext; +import de.uka.ilkd.key.logic.GenericArgument; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermServices; -import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.logic.op.ParametricFunctionDecl; +import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; import org.key_project.logic.Name; import org.key_project.logic.op.Function; +import org.key_project.logic.sort.Sort; import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableList; public class MSetLDT extends LDT { public static final Name NAME = new Name("Mset"); - private final JFunction msetRange; - private final JFunction msetMul; - private final JFunction msetEmpty; - private final JFunction msetSingle; - private final JFunction msetUnion; - private final JFunction msetIntersec; - private final JFunction msetSum; - private final JFunction msetDiff; - private final JFunction msetCard; + private final ParametricFunctionDecl msetRange; + private final ParametricFunctionDecl msetEmpty; + private final ParametricFunctionDecl msetSingle; + private final ParametricFunctionDecl msetSum; + private final ParametricFunctionDecl msetDiff; + private final Function msetCard; + private final Function msetMul; public MSetLDT(TermServices services) { super(NAME, services); msetMul = addFunction(services, "msetMul"); - msetEmpty = addFunction(services, "msetEmpty"); - msetSingle = addFunction(services, "msetSingle"); - msetUnion = addFunction(services, "msetUnion"); - msetIntersec = addFunction(services, "msetIntersec"); - msetSum = addFunction(services, "msetSum"); - msetDiff = addFunction(services, "msetDiff"); + msetEmpty = addParametricFunction(services, "msetEmpty"); + msetSingle = addParametricFunction(services, "msetSingle"); + msetSum = addParametricFunction(services, "msetSum"); + msetDiff = addParametricFunction(services, "msetDiff"); msetCard = addFunction(services, "msetCard"); - msetRange = addFunction(services, "msetRange"); + msetRange = addParametricFunction(services, "msetRange"); } - public JFunction getMsetRange() { return msetRange; } + public ParametricFunctionDecl getMsetRange() { return msetRange; } - public JFunction getMsetMul() { + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetRange(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetRange, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); + } + + + public Function getMsetMul() { return msetMul; } - public JFunction getMsetEmpty() { + public ParametricFunctionDecl getMsetEmpty() { return msetEmpty; } - public JFunction getMsetSingle() { - return msetSingle; + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetEmpty(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetEmpty, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); } - public JFunction getMsetUnion() { - return msetUnion; + + public ParametricFunctionDecl getMsetSingle() { + return msetSingle; } - public JFunction getMsetIntersec() { - return msetIntersec; + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetSingle(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetSingle, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); } - public JFunction getMsetAdd() { + public ParametricFunctionDecl getMsetSum() { return msetSum; } - public JFunction getMsetRemove() { + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetSum(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetSum, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); + } + + + + public ParametricFunctionDecl getMsetDiff() { return msetDiff; } + /** + * Returns the select function for the given sort. + */ + public ParametricFunctionInstance getMsetDiff(Sort instanceSort, TermServices services) { + return ParametricFunctionInstance.get(msetDiff, + ImmutableList.of(new GenericArgument(instanceSort)), (Services) services); + } + @Override public boolean isResponsible(Operator op, JTerm[] subs, Services services, ExecutionContext ec) { @@ -103,31 +137,32 @@ public boolean isResponsible(Operator op, JTerm sub, TermServices services, @Override public JTerm translateLiteral(Literal lit, Services services) { - assert lit instanceof EmptySeqLiteral; - return services.getTermBuilder().func(msetEmpty); + throw new RuntimeException("Not implemented yet"); +// assert lit instanceof EmptyMSetLiteral; +// return services.getTermBuilder().func(msetEmpty, lit.g); } @Override - public JFunction getFunctionFor(Operator op, Services services, ExecutionContext ec) { - if (op instanceof MSetSingle) { - return msetSingle; - } else if (op instanceof MSetCard) { - return msetCard; - } else if (op instanceof MSetUnion) { - return msetUnion; - } else if (op instanceof MSetDiff) { - return msetDiff; - } else if (op instanceof MSetSum) { - return msetSum; - } else if (op instanceof MSetIntersect) { - return msetIntersec; - } else if (op instanceof MSetMul) { - return msetMul; - } - - assert false; - return null; - + public Function getFunctionFor(Operator op, Services services, ExecutionContext ec) { + throw new RuntimeException("Not implemented yet"); + // if (op instanceof MSetSingle) { +// return msetSingle; +// } else if (op instanceof MSetCard) { +// return msetCard; +// } else if (op instanceof MSetUnion) { +// return msetUnion; +// } else if (op instanceof MSetDiff) { +// return msetDiff; +// } else if (op instanceof MSetSum) { +// return msetSum; +// } else if (op instanceof MSetIntersect) { +// return msetIntersec; +// } else if (op instanceof MSetMul) { +// return msetMul; +// } +// +// assert false; +// return null; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java index d171bddeddf..2aec9cc3e47 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java @@ -2121,10 +2121,6 @@ public JTerm seqEmpty() { return func(services.getTypeConverter().getSeqLDT().getSeqEmpty()); } - public JTerm msetEmpty() { - return func(services.getTypeConverter().getMSetLDT().getMsetEmpty()); - } - public JTerm seqSingleton(JTerm x) { return func(services.getTypeConverter().getSeqLDT().getSeqSingleton(), x); } @@ -2168,6 +2164,16 @@ public JTerm seqReverse(JTerm s) { return func(services.getTypeConverter().getSeqLDT().getSeqReverse(), s); } + public JTerm msetEmpty(Sort instanceSort) { + return func(services.getTypeConverter().getMSetLDT().getMsetEmpty(instanceSort, services)); + } + + public JTerm msetRange(QuantifiableVariable qv, JTerm left, JTerm right, JTerm supplier, Sort instanceSort) { + return func(services.getTypeConverter().getMSetLDT().getMsetRange(instanceSort, services), + new JTerm[] { left, right, supplier }, + new ImmutableArray<>(qv)); + } + // ------------------------------------------------------------------------- // misc (moved from key.util.MiscTools) // ------------------------------------------------------------------------- @@ -2249,23 +2255,6 @@ public JTerm seqDef(QuantifiableVariable qv, JTerm a, JTerm b, JTerm t) { new ImmutableArray<>(qv)); } - public JTerm mset(QuantifiableVariable qv, JTerm a, JTerm b, JTerm t) { - return func(services.getTypeConverter().getMSetLDT().getMsetRange(), - new JTerm[] { a, b, t }, - new ImmutableArray<>(qv)); - } - - public JTerm mset(ImmutableList qvs, JTerm range, JTerm t) { - final Function mset = services.getNamespaces().functions().lookup("mset"); - final Iterator it = qvs.iterator(); - JTerm res = func(mset, new JTerm[] { convertToBoolean(range), t }, - new ImmutableArray<>(it.next())); - while (it.hasNext()) { - res = func(mset, new JTerm[] { TRUE(), res }, new ImmutableArray<>(it.next())); - } - return res; - } - public JTerm values() { return func(services.getTypeConverter().getSeqLDT().getValues()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java index 45bf4acea81..9a8b11c2696 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java @@ -275,17 +275,6 @@ public SLExpression quantifiedMax(JTerm _guard, JTerm body, KeYJavaType declsTyp return numeralQuantifier(javaType, nullable, qvs, t1, t2, resultType, unbounded, bounded); } - public @NonNull SLExpression quantifiedMset(KeYJavaType javaType, boolean nullable, - Iterable qvs, @Nullable JTerm t1, JTerm t2, KeYJavaType resultType) { - BoundedNumericalQuantifier bounded = tb::mset; - UnboundedNumericalQuantifier unbounded = (declsType, n, vars, range, body) -> { - final JTerm tr = typerestrict(declsType, n, vars); - return tb.mset(vars, tb.andSC(tr, range), body); - }; - return nonNumeralQuantifier(javaType, nullable, qvs, t1, t2, resultType, unbounded, - bounded); - } - public SLExpression forall(JTerm preTerm, JTerm bodyTerm, KeYJavaType declsType, ImmutableList declVars, boolean nullable, KeYJavaType resultType) { BiFunction quantify = tb::all; @@ -416,7 +405,7 @@ public JTerm upperBound(JTerm a, LogicVariable lv) { if (it.hasNext() || !isBoundedNumerical(t1, lv)) { // not interval range, create unbounded comprehension term ImmutableList _qvs = - ImmutableSLList.nil().prepend(lv); + ImmutableList.of().prepend(lv); while (it.hasNext()) { _qvs = _qvs.prepend(it.next()); } @@ -801,19 +790,6 @@ private SLExpression buildBigintTruncationExpression(KeYJavaType resultType, JTe } } - private SLExpression buildMSetTruncationExpression(KeYJavaType resultType, JTerm term) { - assert term.sort() == services.getTypeConverter().getIntegerLDT().targetSort(); - - SpecMathMode mode = this.overloadedFunctionHandler.getSpecMathMode(); - if (mode == SpecMathMode.JAVA) { - return buildIntCastExpression(resultType, term); - } else { - KeYJavaType mset = services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET); - return new SLExpression(term, mset); - } - } - - private SLExpression buildIntCastExpression(KeYJavaType resultType, JTerm term) { IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT(); try { @@ -930,32 +906,21 @@ public SLExpression createSeqDef(SLExpression a, SLExpression b, SLExpression t, return new SLExpression(resultTerm, seqtype); } - /* - * public SLExpression createMSet(SLExpression a, SLExpression b, SLExpression t, - * - * KeYJavaType declsType, ImmutableList declVars) { - * if (!(declsType.getJavaType().equals(PrimitiveType.JAVA_INT) - * || declsType.getJavaType().equals(PrimitiveType.JAVA_BIGINT))) { - * throw exc.createException0( - * "multiset definition variable must be of type int or \\bigint"); - * } else if (declVars.size() != 1) { - * throw exc.createException0("multiset definition must declare exactly one variable"); - * } - * QuantifiableVariable qv = declVars.head(); - * Term tt = t.getTerm(); - * if (tt.sort() == JavaDLTheory.FORMULA) { - * // bugfix (CS): t.getTerm() delivers a formula instead of a - * // boolean term; obviously the original boolean terms are - * // converted to formulas somewhere else; however, we need - * // boolean terms instead of formulas here - * tt = tb.convertToBoolean(t.getTerm()); - * } - * Term resultTerm = tb.mset(qv, a.getTerm(), b.getTerm(), tt); - * final KeYJavaType msettype = services.getJavaInfo().getPrimitiveKeYJavaType("\\mset"); - * return new SLExpression(resultTerm, msettype); - * } - * - */ + public SLExpression createMsetRange(SLExpression left, SLExpression right, SLExpression supplier, + KeYJavaType declsType, ImmutableList declVars) { + if (!(declsType.getJavaType().equals(PrimitiveType.JAVA_INT) + || declsType.getJavaType().equals(PrimitiveType.JAVA_BIGINT))) { + throw exc.createException0( + "msetRange definition variable must be of type int or \\bigint"); + } else if (declVars.size() != 1) { + throw exc.createException0("msetRange definition must declare exactly one variable"); + } + QuantifiableVariable qv = declVars.head(); + JTerm supplierTerm = ensureTerm(supplier.getTerm()); + JTerm resultTerm = tb.msetRange(qv, left.getTerm(), right.getTerm(), supplierTerm, supplierTerm.sort()); + final KeYJavaType msetType = services.getJavaInfo().getPrimitiveKeYJavaType("\\mSet"); + return new SLExpression(resultTerm, msetType); + } public SLExpression createUnionF(boolean nullable, Pair> declVars, JTerm expr, JTerm guard) { @@ -1291,7 +1256,6 @@ public SLExpression skolemExprHelper(String jmlKeyWord, KeYJavaType type, return skolemExprHelper(type, services, jmlKeyWord); } - public @NonNull SLExpression skolemExprHelper(@NonNull KeYJavaType type, @NonNull TermServices services, @NonNull String shortName) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index 13cd41045d6..357acf2a256 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -1746,9 +1746,7 @@ public SLExpression visitSpecquantifiedexpression( case JmlLexer.MIN -> termFactory.quantifiedMin(guard, body, declVars.first, nullable, declVars.second); - case JmlLexer.MSET -> - termFactory.quantifiedMset(declVars.first, nullable, declVars.second, guard, body, - services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_MSET)); + case JmlLexer.NUM_OF -> { KeYJavaType kjtInt = services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_BIGINT); @@ -1865,6 +1863,21 @@ public Object visitSeqdefterm(JmlParser.SeqdeftermContext ctx) { return result; } + @Override + public Object visitMsetrangeterm(JmlParser.MsetrangetermContext ctx) { + Pair> decls = accept(ctx.quantifiedvardecls()); + resolverManager.pushLocalVariablesNamespace(); + assert decls != null; + resolverManager.putIntoTopLocalVariablesNamespace(decls.second, decls.first); + SLExpression left = accept(ctx.expression(0)); + SLExpression right = accept(ctx.expression(1)); + SLExpression supplier = accept(ctx.expression(2)); + assert supplier != null; + SLExpression result = termFactory.createMsetRange(left, right, supplier, decls.first, decls.second); + resolverManager.popLocalVariablesNamespace(); + return result; + } + @Override public Pair> visitQuantifiedvardecls( JmlParser.QuantifiedvardeclsContext ctx) { diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key index e0d541ac494..99253bf46b0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key @@ -32,4 +32,4 @@ wellfound, "./string/charListHeader.key", types, - msetRules; + "./mset/msetHeader.key"; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/MSetRulesdefinition.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetAxioms.key similarity index 56% rename from key.core/src/main/resources/de/uka/ilkd/key/proof/rules/MSetRulesdefinition.key rename to key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetAxioms.key index 2255cee5b91..62aaf9ce9b5 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/MSetRulesdefinition.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetAxioms.key @@ -21,54 +21,6 @@ \replacewith(mset{x;}(0, 1, msetEl)) }; - // defOfMSetMul{ - // \schemaVar \term Mset m; - // \schemaVar \term any msetEl; - // \schemaVar \variables int x; - - // \find(msetMul(m, msetEl)) - // \varcond(\notFreeIn(x, m) , - // \notFreeIn(x, msetEl)) - - - // ???????????????} - - - //defOfMSetCard{ - - //???????????????} - - - defOfMSetUnion{ - \schemaVar \term Mset m, s; - \schemaVar \term any msetEl; - \schemaVar \variables int x; - - \find(msetUnion(m, s)) - \varcond(\notFree(x, m), - \notFree(x, s), - \notFree(x, msetEl)) - - \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(s, msetEl) = 0)) - \then(msetSum(m, s)) - \else(msetSum(m , s) - msetIntersec(m , s)) - - }; - - defOfMSetIntersec{ - \schemaVar \term Mset m, s; - \schemaVar \term any msetEl; - \schemaVar \variables int x; - - \find(msetIntersec(m, s)) - \varcond(\notFree(x, m), - \notFree(x, s), - \notFree(x, msetEl)) - - \replacewith(msetSum(m , s) - msetUnion(m, s)) - - }; - defOfMSetSum{ \schemaVar \term Mset m, s; \schemaVar \term any msetEl; @@ -81,247 +33,6 @@ \replacewith( mset(m) + mset(s)) }; - - - defOfMSetDiff{ - \schemaVar \term Mset m, s; - \schemaVar \term any msetEl; - \schemaVar \variables int x; - - \find(msetIntersec(m, s)) - \varcond(\notFree(x, m), - \notFree(x, s), - \notFree(x, msetEl)) - - \replacewith( mset(m) - mset(s)) - }; - - - \lemma - msetUnionWithMSetEmpty1{ - - \find(msetUnion(msetEmpty, msetEmpty)) - \replacewith(msetEmpty) - - \heuristics(concrete) - \displayname "msetUnionWithEmpty" - }; - - \lemma - msetUnionWithMSetEmpty2{ - \schemaVar \term Mset m; - - \find(msetUnion(m, msetEmpty)) - \replacewith(m) - - \heuristics(concrete) - \displayname "msetUnionWithEmpty" - }; - - \lemma - msetUnionWithMSetEmpty3{ - \schemaVar \term any msetEl; - - \find(msetUnion(msetSingle(msetEl), msetEmpty)) - \replacewith(msetSingle(msetEl)) - - \heuristics(concrete) - \displayname "msetUnionWithEmpty" - }; - - \lemma - msetUnionWithMSetSingle1{ - \schemaVar \term any msetEl; - - \find(msetUnion(msetSingle(msetEl), msetSingle(msetEl))) - \replacewith(msetSingle(msetEl)) - - \heuristics(concrete) - \displayname "msetUnionWithSingle" - }; - - \lemma - msetUnionWithMSetSingle2{ - \schemaVar \term any msetEl1, msetEl2; - - \find(msetUnion(msetSingle(msetEl1), msetSingle(msetEl2)) - \replacewith(msetSum(msetSingle(msetEl1), msetSingle(msetEl2)) - - \heuristics(concrete) - \displayname "msetUnionWithSingle" - }; - - \lemma - msetUnionWithSameMSets{ - \schemaVar \term Mset m; - - \find(msetUnion(m , m)) - \replacewith(m) - \heuristics(concrete) - - }; - - \lemma - msetUnionCommutativity{ - \schemaVar \term Mset m, s; - - \find(msetUnion(m, s)) - \replacewith(msetUnion(s, m)) - \heuristics(concrete) - - }; - - \lemma - msetUnionAssociativity{ - \schemaVar \term Mset m, s, t; - - \find(msetUnion(m, msetUnion(s, t))) - \replacewith(msetUnion(msetUnion(m, s) , t)) - \heuristics(concrete) - - }; - - \lemma - msetUnionWithMSetIntersection{ - \schemaVar \term Mset m, s; - - \find(msetUnion(m, msetIntersec(m, s))) - \replacewith(m) - heuristics(concrete) - - }; - - \lemma - msetUnionSubset{ - \schemaVar \term Mset m, s; - \schemaVar \term any msetEl; - - - \find(msetUnion(m, s)) - \varcond( - \notFreeIn(msetEl, m), - \notFreeIn(msetEl, s) - ) - \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(s, msetEl) > 0 && msetIntersec(m, s) == s) - \then(m) - \else(msetUnion(m, s))) - }; - - - \lemma - msetIntersectionWithMSetEmpty1{ - - \find(msetIntersec(msetEmpty, msetEmpty)) - \replacewith(msetEmpty) - - \heuristics(concrete) - \displayname "msetIntersecWithEmpty" - }; - - \lemma - msetIntersectionWithMSetEmpty2{ - \schemaVar \term Mset m; - - \find(msetIntersec(m, msetEmpty)) - \replacewith(msetEmpty) - - \heuristics(concrete) - \displayname "msetIntersecWithEmpty" - }; - - \lemma - msetIntersectionWithMSetEmpty3{ - \schemaVar \term any msetEl; - - \find(msetIntersec(msetSingle(msetEl), msetEmpty)) - \replacewith(msetEmpty) - - \heuristics(concrete) - \displayname "msetIntersecWithEmpty" - }; - - \lemma - msetIntersectionWithMSetSingle1{ - \schemaVar \term any msetEl; - - \find(msetIntersec(msetSingle(msetEl), msetSingle(msetEl))) - \replacewith(msetSingle(msetEl)) - \heuristics(concrete) - \displayname "msetIntersecWithSingle" - - }; - - \lemma - msetIntersectionWithMSetSingle2{ - \schemaVar \term any msetEl1 , msetEl2; - - \find(msetIntersec(msetSingle(msetEl1), msetSingle(msetEl2))) - \replacewith(msetEmpty) - \heuristics(concrete) - \displayname "msetIntersecWithSingle" - - }; - - \lemma - msetIntersecWithSameMSets{ - \schemaVar \term Mset m; - - \find(msetIntersec(m , m)) - \replacewith(m) - \heuristics(concrete) - - }; - - \lemma - msetIntersecCommutativity{ - \schemaVar \term Mset m, s; - - \find(msetIntersec(m, s)) - \replacewith(msetIntersec(s, m)) - \heuristics(concrete) - - }; - - - \lemma - msetIntersecDifferent{ - \schemaVar \term Mset m, s; - - \find(msetIntersec(m, s)) - \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(s, msetEl) = 0) - \than(msetEmpty) - \else(msetIntersec(m,s))) - - \heuristics(concrete) - - }; - - \lemma - msetIntersecSubset{ - \schemaVar \term Mset m, s; - \schemaVar \term any msetEl; - - \find(msetIntersec(m, s)) - \replacewith(\if(msetMul(m, msetEl) > 0 && msetMul(s, msetEl) > 0 && msetUnion(m, s) == m) - \than(s) - \else(msetIntersec(m, s))) - - \heuristics(concrete) - - }; - - \lemma - msetIntersecWithMSetUnion{ - \schemaVar \term Mset m, s, t; - - \find(msetIntersec(m, msetUnion(s,t))) - \replacewith(msetUnion(msetIntersec(m,s), msetIntersec(m, t))) - \heuristics(concrete) - - }; - - - \lemma msetSumWithMSetEmpty1{ @@ -403,11 +114,6 @@ }; - - - - - \lemma msetDiffWithMSetEmpty1{ diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetHeader.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetHeader.key new file mode 100644 index 00000000000..e3c3003b4bd --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetHeader.key @@ -0,0 +1,18 @@ +\sorts { + \generic El; + \generic SubEl \extends El; + Mset<[El]>; +} + +\functions { + // Getters + int msetMul(Mset<[El]>, El); + int msetCard(Mset<[El]>); + + // Constructors + Mset<[El]> msetEmpty<[El]>; + Mset<[El]> msetSingle<[El]>(El); + Mset<[El]> msetDiff<[El]>(Mset<[El]>, Mset<[El]>); + Mset<[El]> msetSum<[El]>(Mset<[El]>, Mset<[El]>); + Mset<[El]> msetRange<[El]> {false, false, true}(int, int, El); +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetRules.key new file mode 100644 index 00000000000..4bb9ea9f684 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mset/msetRules.key @@ -0,0 +1,210 @@ + +\rules { + + mset_Empty { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term SubEl t; + + \find(msetRange<[El]>{uSub;}(left, right, t)) + \varcond(\notFreeIn(uSub, left)) + \replacewith(\if(right < left) + \then(msetEmpty<[El]>) + \else(msetRange<[El]>{uSub;}(left, right, t))) + + \heuristics(simplify) + }; + + mset_Single { + \schemaVar \term int left; + \schemaVar \variables int uSub; + \schemaVar \term SubEl t; + + \find(msetRange<[El]>{uSub;}(left, left, t)) + \sameUpdateLevel + \replacewith(msetSingle({\subst uSub; left}(t))) + \heuristics(simplify) + }; + + msetSumWithMsetEmpty1 { + \schemaVar \term Mset m; + \find(msetSum<[El]>(msetEmpty<[El]>, m)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetSumWithEmpty" + }; + + msetSumWithmsetEmpty2 { + \schemaVar \term Mset m; + \find(msetSum<[El]>(m, msetEmpty<[El]>)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetSumWithEmpty" + }; + + msetSumCommutativity { + \schemaVar \term Mset commLeft, commRight; + \find(msetSum<[El]>(commLeft, commRight)) + \replacewith(msetSum<[El]>(commRight, commLeft)) + \heuristics(polySimp_expand, polySimp_addOrder) + }; + + msetSumAssociativity { + \schemaVar \term Mset addAssocPoly0, addAssocPoly1, addAssocMono; + \find(msetSum<[El]>(addAssocPoly0, msetSum<[El]>(addAssocPoly1, addAssocMono))) + \replacewith(msetSum<[El]>(msetSum<[El]>(addAssocPoly0, addAssocPoly1), addAssocMono)) + \heuristics(polySimp_expand, polySimp_addAssoc) + }; + + msetDiffWithMsetEmpty1 { + \find(msetDiff<[El]>(msetEmpty<[El]>, msetEmpty<[El]>)) + \replacewith(msetEmpty<[El]>) + \heuristics(simplify) + \displayname "msetDiffWithEmpty" + }; + + msetDiffWithMsetEmpty2 { + \schemaVar \term Mset m; + \find(msetDiff<[El]>(m, msetEmpty<[El]>)) + \replacewith(m) + \heuristics(simplify) + \displayname "msetDiffWithEmpty" + }; + + msetDiffCommutativity { + \schemaVar \term Mset commLeft, commRight; + \find(msetDiff<[El]>(commLeft, commRight)) + \replacewith(msetDiff<[El]>(commRight, commLeft)) + \heuristics(order_terms) + }; + + mset_split { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \variables int uSub; + \schemaVar \term SubEl t; + + \find(msetRange<[El]>{uSub;}(left, right, t)) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum<[El]>( + msetRange<[El]>{uSub;}(left, middle-1, t), + msetRange<[El]>{uSub;}(middle, right, t))) + \else(msetRange<[El]>{uSub;}(left, right, t))) + }; + + mset_extract_triggered { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left, middle, right, h, array)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum<[El]>(msetSum<[El]>(msetRange<[El]>{uSub;}(left, middle-1, select<[SubEl]>(h, array, arr(uSub))), + msetSingle<[El]>(select<[SubEl]>(h, array, arr(middle)))), + msetRange<[El]>{uSub;}(middle+1, right, select<[SubEl]>(h, array, arr(uSub))))) + \else(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {middle} msetSingle<[El]>(select<[SubEl]>(h, array, arr(middle))) + \avoid middle <= -1 + left, right <= -1 + middle; + }; + + // that rule seems not to be correct middle -1 can be < left, how is range for an empty negative interval defined? + mset_extract_array { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \variables int uSub; + \schemaVar \term SubEl x; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(store(h, array, arr(middle), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum<[El]>(msetSum<[El]>(msetRange<[El]>{uSub;}(left, middle-1, select<[SubEl]>(h, array, arr(uSub))), + msetSingle<[El]>({\subst uSub; middle} x)), + msetRange<[El]>{uSub;}(middle+1, right, select<[SubEl]>(h, array, arr(uSub))))) + \else(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(simplify_ENLARGING) + }; + + mset_extract_array { + \schemaVar \term int left, right; + \schemaVar \term int middle; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \variables int uSub; + \schemaVar \term SubEl x; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(store(h, array, arr(middle), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) + \replacewith(\if(left <= middle & middle <= right) + \then(msetSum<[El]>(msetSum<[El]>(msetRange<[El]>{uSub;}(left, middle-1, select<[SubEl]>(h, array, arr(uSub))), + msetSingle<[El]>({\subst uSub; middle} x)), + msetRange<[El]>{uSub;}(middle+1, right, select<[SubEl]>(h, array, arr(uSub))))) + \else(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(simplify_ENLARGING) + }; + + mset_extract_array_front { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \term SubEl x; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(store(h, array, arr(left), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) + \replacewith(msetSum<[El]>(msetSingle<[El]>({\subst uSub; left} x), + msetRange<[El]>{uSub;}(left+1, right, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(simplify_enlarging) + }; + + mset_extract_array_back { + \schemaVar \term int left, right; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + \schemaVar \term SubEl x; + + \find(msetRange<[El]>{uSub;}(left, right, select<[SubEl]>(store(h, array, arr(right), x), array, arr(uSub)))) + \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) + \replacewith(msetSum<[El]>(msetRange<[El]>{uSub;}(left, right-1, + select<[SubEl]>(h, array, arr(uSub))), + msetSingle<[El]>({\subst uSub; right} x))) + \heuristics(simplify_enlarging) + }; + + mset_extract_triggered_front { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange<[El]>{uSub;}(low, high, select<[SubEl]>(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) + \replacewith(msetSum<[El]>(msetSingle<[El]>(select<[SubEl]>(h, array, arr(low))), + msetRange<[El]>{uSub;}(low+1, high, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {low} msetSingle<[El]>(select<[SubEl]>(h, array, arr(low))) + \avoid low >= high, false; + }; + + mset_extract_triggered_back { + \schemaVar \term int low, high; + \schemaVar \variables int uSub; + \schemaVar \term Heap h; + \schemaVar \term Object array; + + \find(msetRange<[El]>{uSub;}(low, high, select<[SubEl]>(h, array, arr(uSub)))) + \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) + \replacewith(msetSum<[El]>(msetSingle<[El]>(select<[SubEl]>(h, array, arr(high))), + msetRange<[El]>{uSub;}(low, high-1, select<[SubEl]>(h, array, arr(uSub))))) + \heuristics(comprehension_split, triggered) + \trigger {high} msetSingle<[El]>(select<[SubEl]>(h, array, arr(high))) + \avoid high <= low, false; + }; +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key deleted file mode 100644 index f96ab521602..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key +++ /dev/null @@ -1,320 +0,0 @@ -\sorts { - Mset; - \generic alpha, beta; -} - -\functions { - // Getters - int msetMul(Mset, any); - int msetCard(Mset); - - // Constructors - Mset msetEmpty; - Mset msetSingle(any); - Mset msetUnion(Mset, Mset); - Mset msetIntersec(Mset, Mset); - Mset msetDiff(Mset, Mset); - Mset msetSum(Mset, Mset); - Mset msetRange {false, false, true}(int, int, any); -} - -\rules { - - mset_Empty { - \schemaVar \term int left, right; - \schemaVar \variables int uSub; - \schemaVar \term beta t; - - \find(msetRange{uSub;}(left, right, t)) - \varcond(\notFreeIn(uSub, left)) - \replacewith(\if(right < left) - \then(msetEmpty) - \else(msetRange{uSub;}(left, right, t))) - - \heuristics(simplify) - }; - - mset_Single { - \schemaVar \term int left; - \schemaVar \variables int uSub; - \schemaVar \term beta t; - - \find(msetRange{uSub;}(left, left, t)) - \sameUpdateLevel - \replacewith(msetSingle({\subst uSub; left}(t))) - \heuristics(simplify) - }; - - msetUnionWithMSetEmpty1 { - \find(msetUnion(msetEmpty, msetEmpty)) - \replacewith(msetEmpty) - \heuristics(simplify) - \displayname "msetUnionWithEmpty" - }; - - msetUnionWithMSetEmpty2 { - \schemaVar \term Mset m; - \find(msetUnion(m, msetEmpty)) - \replacewith(m) - \heuristics(simplify) - \displayname "msetUnionWithEmpty" - }; - - msetUnionWithSameMSets { - \schemaVar \term Mset m; - \find(msetUnion(m, m)) - \replacewith(m) - \heuristics(simplify) - }; - - msetUnionCommutativity { - \schemaVar \term Mset commLeft, commRight; - \find(msetUnion(commLeft, commRight)) - \replacewith(msetUnion(commRight, commLeft)) - \heuristics(polySimp_expand, polySimp_addOrder) - }; - - msetUnionAssociativity { - \schemaVar \term Mset addAssocPoly0, addAssocPoly1, addAssocMono; - \find(msetUnion(addAssocPoly0, msetUnion(addAssocPoly1, addAssocMono))) - \replacewith(msetUnion(msetUnion(addAssocPoly0, addAssocPoly1), addAssocMono)) - \heuristics(polySimp_expand, polySimp_addAssoc) - }; - - msetUnionWithMSetIntersection { - \schemaVar \term Mset m, s; - \find(msetUnion(m, msetIntersec(m, s))) - \replacewith(m) - \heuristics(simplify) - }; - - msetUnionSubset { - \schemaVar \term Mset m, s; - \schemaVar \term any msetEl; - - \find(msetUnion(m, s)) - \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) > 0 & msetIntersec(m, s) = s) - \then(m) - \else(msetUnion(m, s))) - \heuristics(simplify) - }; - - msetIntersectionWithMSetEmpty1 { - \find(msetIntersec(msetEmpty, msetEmpty)) - \replacewith(msetEmpty) - \heuristics(simplify) - \displayname "msetIntersecWithEmpty" - }; - - msetIntersectionWithMSetEmpty2 { - \schemaVar \term Mset m; - \find(msetIntersec(m, msetEmpty)) - \replacewith(msetEmpty) - \heuristics(simplify) - \displayname "msetIntersecWithEmpty" - }; - - msetIntersecWithSameMSets { - \schemaVar \term Mset m; - \find(msetIntersec(m, m)) - \replacewith(m) - \heuristics(simplify) - }; - - msetIntersecCommutativity { - \schemaVar \term Mset commLeft, commRight; - \find(msetIntersec(commLeft, commRight)) - \replacewith(msetIntersec(commRight, commLeft)) - \heuristics(polySimp_expand, polySimp_addOrder) - }; - - msetIntersecDifferent { - \schemaVar \term Mset m, s; - \schemaVar \term any msetEl; - - \find(msetIntersec(m, s)) - \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) = 0) - \then(msetEmpty) - \else(msetIntersec(m, s))) - \heuristics(simplify) - }; - - msetIntersecSubset { - \schemaVar \term Mset m, s; - \schemaVar \term any msetEl; - - \find(msetIntersec(m, s)) - \replacewith(\if(msetMul(m, msetEl) > 0 & msetMul(s, msetEl) > 0 & msetUnion(m, s) = m) - \then(s) - \else(msetIntersec(m, s))) - \heuristics(simplify) - }; - - msetIntersecWithMSetUnion { - \schemaVar \term Mset m, s, t; - \find(msetIntersec(m, msetUnion(s, t))) - \replacewith(msetUnion(msetIntersec(m, s), msetIntersec(m, t))) - \heuristics(simplify) - }; - - msetSumWithMSetEmpty1 { - \schemaVar \term Mset m; - \find(msetSum(msetEmpty, m)) - \replacewith(m) - \heuristics(simplify) - \displayname "msetSumWithEmpty" - }; - - msetSumWithMSetEmpty2 { - \schemaVar \term Mset m; - \find(msetSum(m, msetEmpty)) - \replacewith(m) - \heuristics(simplify) - \displayname "msetSumWithEmpty" - }; - - msetSumCommutativity { - \schemaVar \term Mset commLeft, commRight; - \find(msetSum(commLeft, commRight)) - \replacewith(msetSum(commRight, commLeft)) - \heuristics(polySimp_expand, polySimp_addOrder) - }; - - msetSumAssociativity { - \schemaVar \term Mset addAssocPoly0, addAssocPoly1, addAssocMono; - \find(msetSum(addAssocPoly0, msetSum(addAssocPoly1, addAssocMono))) - \replacewith(msetSum(msetSum(addAssocPoly0, addAssocPoly1), addAssocMono)) - \heuristics(polySimp_expand, polySimp_addAssoc) - }; - - msetDiffWithMSetEmpty1 { - \find(msetDiff(msetEmpty, msetEmpty)) - \replacewith(msetEmpty) - \heuristics(simplify) - \displayname "msetDiffWithEmpty" - }; - - msetDiffWithMSetEmpty2 { - \schemaVar \term Mset m; - \find(msetDiff(m, msetEmpty)) - \replacewith(m) - \heuristics(simplify) - \displayname "msetDiffWithEmpty" - }; - - msetDiffCommutativity { - \schemaVar \term Mset commLeft, commRight; - \find(msetDiff(commLeft, commRight)) - \replacewith(msetDiff(commRight, commLeft)) - \heuristics(polySimp_expand, polySimp_addOrder) - }; - - mset_split { - \schemaVar \term int left, right; - \schemaVar \term int middle; - \schemaVar \variables int uSub; - \schemaVar \term beta t; - - \find(msetRange{uSub;}(left, right, t)) - \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) - \replacewith(\if(left <= middle & middle <= right) - \then(msetSum(msetRange{uSub;}(left, middle-1, t), - msetRange{uSub;}(middle, right, t))) - \else(msetRange{uSub;}(left, right, t))) - }; - - mset_extract_triggered { - \schemaVar \term int left, right; - \schemaVar \term int middle; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - - \find(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub)))) - \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) - \replacewith(\if(left <= middle & middle <= right) - \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, select<[beta]>(h, array, arr(uSub))), - msetSingle(select<[beta]>(h, array, arr(middle)))), - msetRange{uSub;}(middle+1, right, select<[beta]>(h, array, arr(uSub))))) - \else(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub))))) - \heuristics(comprehension_split, triggered) - \trigger {middle} msetSingle(select<[beta]>(h, array, arr(middle))) - \avoid middle <= -1 + left, right <= -1 + middle; - }; - - mset_extract_array { - \schemaVar \term int left, right; - \schemaVar \term int middle; - \schemaVar \term Heap h; - \schemaVar \term Object array; - \schemaVar \variables int uSub; - \schemaVar \term alpha x; - - \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(middle), x), array, arr(uSub)))) - \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right)) - \replacewith(\if(left <= middle & middle <= right) - \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, select<[beta]>(h, array, arr(uSub))), - msetSingle({\subst uSub; middle} x)), - msetRange{uSub;}(middle+1, right, select<[beta]>(h, array, arr(uSub))))) - \else(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub))))) - \heuristics(simplify_ENLARGING) - }; - - mset_extract_array_front { - \schemaVar \term int left, right; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - \schemaVar \term alpha x; - - \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(left), x), array, arr(uSub)))) - \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) - \replacewith(msetSum(msetSingle({\subst uSub; left} x), - msetRange{uSub;}(left+1, right, select<[beta]>(h, array, arr(uSub))))) - \heuristics(simplify_enlarging) - }; - - mset_extract_array_back { - \schemaVar \term int left, right; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - \schemaVar \term alpha x; - - \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(right), x), array, arr(uSub)))) - \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right)) - \replacewith(msetSum(msetRange{uSub;}(left, right-1, select<[beta]>(h, array, arr(uSub))), - msetSingle({\subst uSub; right} x))) - \heuristics(simplify_enlarging) - }; - - mset_extract_triggered_front { - \schemaVar \term int low, high; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - - \find(msetRange{uSub;}(low, high, select<[beta]>(h, array, arr(uSub)))) - \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) - \replacewith(msetSum(msetSingle(select<[beta]>(h, array, arr(low))), - msetRange{uSub;}(low+1, high, select<[beta]>(h, array, arr(uSub))))) - \heuristics(comprehension_split, triggered) - \trigger {low} msetSingle(select<[beta]>(h, array, arr(low))) - \avoid low >= high, false; - }; - - mset_extract_triggered_back { - \schemaVar \term int low, high; - \schemaVar \variables int uSub; - \schemaVar \term Heap h; - \schemaVar \term Object array; - - \find(msetRange{uSub;}(low, high, select<[beta]>(h, array, arr(uSub)))) - \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array)) - \replacewith(msetSum(msetSingle(select<[beta]>(h, array, arr(high))), - msetRange{uSub;}(low, high-1, select<[beta]>(h, array, arr(uSub))))) - \heuristics(comprehension_split, triggered) - \trigger {high} msetSingle(select<[beta]>(h, array, arr(high))) - \avoid high <= low, false; - }; -} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key index ebbbb59ad82..4a5b0d307c0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key @@ -48,6 +48,7 @@ \include "./sequence/seqPerm.key"; \include "./sequence/seqPerm2.key"; \include "./set/setRules.key"; +\include "./mset/msetRules.key"; // rules for Java (order does not matter, since not provable anyway) \include javaRules;