Skip to content

Purge sort depending functions in favor of parametric functions #3773

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Open
Drodt wants to merge 44 commits into
base: main
Choose a base branch
from
Open

Purge sort depending functions in favor of parametric functions #3773

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
44 commits
Select commit Hold shift + click to select a range
e83ca5e
Remove SortDependingFunction class
Drodt Mar 13, 2026
d5b5d48
Simplify parser
Drodt Mar 13, 2026
6d63c6e
Remove some sort depending fns
Drodt Mar 16, 2026
d0dff83
Merge branch 'main' into purge-sort-depending-fn
Drodt Mar 16, 2026
ec93a6f
Fix rewriting of .key files, field resolution, and grammar
Drodt Mar 16, 2026
5c07d77
Fix tests & pp
Drodt Mar 16, 2026
8e53992
Fix more .key files
Drodt Mar 16, 2026
3acacc7
Replace more sort dep fns
Drodt Mar 16, 2026
f50ce80
Fix more .key files, taclets.old.txt, and SMT files
Drodt Mar 17, 2026
7999173
Fix SMT translation
Drodt Mar 17, 2026
7a53e5d
Try to fix SMT lemma parsing
Drodt Mar 17, 2026
ebbd1d7
Fix LogicPrinter when services == null
Drodt Mar 17, 2026
70607d7
Fix oracle translation
Drodt Mar 17, 2026
46212b5
Fix some tests
Drodt Mar 17, 2026
1852859
Fix some tests
Drodt Mar 17, 2026
00accc7
Fix quicksort
Drodt Mar 17, 2026
3acb868
Fix BM
Drodt Mar 17, 2026
19daf1c
Fix Observer functions
Drodt Mar 17, 2026
b214f1e
Fix permission translation
Drodt Mar 17, 2026
03a4688
Fix proof
Drodt Mar 18, 2026
a7d24d2
Fix field name splitting
Drodt Mar 18, 2026
8c2b4e9
Fix rule
Drodt Mar 18, 2026
e9fc560
Fix same update level
Drodt Mar 18, 2026
abda47f
Fix taclet proofs
Drodt Mar 18, 2026
45fec3d
Update taclet oracle (same update level follow-up)
Drodt Mar 18, 2026
0e6cd44
Fix escaping in XML
Drodt Mar 18, 2026
46b2227
Merge branch 'main' into purge-sort-depending-fn
Drodt Mar 19, 2026
97e3166
Merge branch 'main' into purge-sort-depending-fn
Drodt Mar 20, 2026
355063b
Merge branch 'main' into purge-sort-depending-fn
Drodt Mar 20, 2026
7b25367
Merge branch 'main' into purge-sort-depending-fn
Drodt Mar 24, 2026
526d8fd
Merge branch 'main' into purge-sort-depending-fn
Drodt Mar 29, 2026
dc42f0e
Fix select w/ old syntax
Drodt Mar 29, 2026
7e4eff0
Fix field name splitting
Drodt Mar 29, 2026
2092755
Fix more .key and proof files
Drodt Mar 29, 2026
1be766d
Fix BM proof
Drodt Mar 30, 2026
e104444
Fix parser proof
Drodt Mar 30, 2026
6aa7f8f
Update taclet equality oracle
Drodt Mar 30, 2026
a11861c
Rename polymorphic implicit fields
Drodt Mar 30, 2026
6d182bd
Fix conversion of fields
Drodt Mar 31, 2026
e5307d3
Fix lookup for fields named instance
Drodt Mar 31, 2026
07ca9df
Merge branch 'main' into purge-sort-depending-fn
Drodt Apr 1, 2026
c13286c
Remove implicit idents from lexer
Drodt Apr 1, 2026
a0a4ce2
Improve comments and ncore lexer (thanks WP)
Drodt Apr 20, 2026
2e57948
Comment
Drodt Apr 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
6 changes: 3 additions & 3 deletions ...y/proof_references/testcase/analyst/TestClassAxiomAndInvariantProofReferencesAnalyst.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ public void testInvariantInOperationContractOfArgument() throws Exception {
new ClassAxiomAndInvariantProofReferencesAnalyst(),
element -> IProofReference.USE_INVARIANT.equals(element.getKind()),
new ExpectedProofReferences(IProofReference.USE_INVARIANT,
"and(geq(int::select(heap,self,Child::$x),Z(0(#))),leq(int::select(heap,self,Child::$x),Z(0(1(#)))))<<SC>>"));
"and(geq(select<[int]>(heap,self,Child::$x),Z(0(#))),leq(select<[int]>(heap,self,Child::$x),Z(0(1(#)))))<<SC>>"));
}

/**
Expand Down Expand Up @@ -69,7 +69,7 @@ false, new ClassAxiomAndInvariantProofReferencesAnalyst(),
new ExpectedProofReferences(IProofReference.USE_AXIOM,
"equiv(java.lang.Object::$inv(heap,self),true)"),
new ExpectedProofReferences(IProofReference.USE_AXIOM,
"equals(test.ModelFieldTest::$f(heap,self),mul(Z(2(#)),int::select(heap,self,test.ModelFieldTest::$x)))"));
"equals(test.ModelFieldTest::$f(heap,self),mul(Z(2(#)),select<[int]>(heap,self,test.ModelFieldTest::$x)))"));
}

/**
Expand All @@ -83,7 +83,7 @@ public void testModelFieldTest_f() throws Exception {
new ExpectedProofReferences(IProofReference.USE_AXIOM,
"equiv(java.lang.Object::$inv(heap,self),true)"),
new ExpectedProofReferences(IProofReference.USE_AXIOM,
"equals(test.ModelFieldTest::$f(heap,self),mul(Z(2(#)),int::select(heap,self,test.ModelFieldTest::$x)))"));
"equals(test.ModelFieldTest::$f(heap,self),mul(Z(2(#)),select<[int]>(heap,self,test.ModelFieldTest::$x)))"));
}

/**
Expand Down
10 changes: 5 additions & 5 deletions ...n/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestConditionalVariables.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ protected IExecutionVariable[] createExpectedEqualCaseVariables() {
ExecutionNodeReader.KeYlessVariable selfContentVar =
new ExecutionNodeReader.KeYlessVariable(selfValue, false, null, "content");
selfContentVar.addValue(new ExecutionNodeReader.KeYlessValue(selfContentVar, "int",
"int::select(heap,n,Number::$content)", "content {true}", false, false, "true"));
"select<[int]>(heap,n,Number::$content)", "content {true}", false, false, "true"));
selfValue.addChildVariable(selfContentVar);
// n
result[1] = new ExecutionNodeReader.KeYlessVariable(null, false, null, "n");
Expand All @@ -111,7 +111,7 @@ protected IExecutionVariable[] createExpectedEqualCaseVariables() {
ExecutionNodeReader.KeYlessVariable nContentVar =
new ExecutionNodeReader.KeYlessVariable(nValue, false, null, "content");
nContentVar.addValue(new ExecutionNodeReader.KeYlessValue(nContentVar, "int",
"int::select(heap,n,Number::$content)", "content {true}", false, false, "true"));
"select<[int]>(heap,n,Number::$content)", "content {true}", false, false, "true"));
nValue.addChildVariable(nContentVar);
// exc
result[2] = new ExecutionNodeReader.KeYlessVariable(null, false, null, "exc");
Expand All @@ -135,7 +135,7 @@ protected IExecutionVariable[] createExpectedNotEqualCaseVariables() {
ExecutionNodeReader.KeYlessVariable selfContentVar =
new ExecutionNodeReader.KeYlessVariable(selfValue, false, null, "content");
selfContentVar.addValue(new ExecutionNodeReader.KeYlessValue(selfContentVar, "int",
"int::select(heap,self,Number::$content)", "content {true}", false, false, "true"));
"select<[int]>(heap,self,Number::$content)", "content {true}", false, false, "true"));
selfValue.addChildVariable(selfContentVar);
// n
result[1] = new ExecutionNodeReader.KeYlessVariable(null, false, null, "n");
Expand All @@ -145,7 +145,7 @@ protected IExecutionVariable[] createExpectedNotEqualCaseVariables() {
ExecutionNodeReader.KeYlessVariable nContentVar =
new ExecutionNodeReader.KeYlessVariable(nValue, false, null, "content");
nContentVar.addValue(new ExecutionNodeReader.KeYlessValue(nContentVar, "int",
"int::select(heap,n,Number::$content)", "content {true}", false, false, "true"));
"select<[int]>(heap,n,Number::$content)", "content {true}", false, false, "true"));
nValue.addChildVariable(nContentVar);
// exc
result[2] = new ExecutionNodeReader.KeYlessVariable(null, false, null, "exc");
Expand All @@ -169,7 +169,7 @@ protected IExecutionVariable[] createExpectedNullCaseVariables() {
ExecutionNodeReader.KeYlessVariable selfContentVar =
new ExecutionNodeReader.KeYlessVariable(selfValue, false, null, "content");
selfContentVar.addValue(new ExecutionNodeReader.KeYlessValue(selfContentVar, "int",
"int::select(heap,self,Number::$content)", "content {true}", false, false, "true"));
"select<[int]>(heap,self,Number::$content)", "content {true}", false, false, "true"));
selfValue.addChildVariable(selfContentVar);
// n
result[1] = new ExecutionNodeReader.KeYlessVariable(null, false, null, "n");
Expand Down
14 changes: 7 additions & 7 deletions ...execution/src/test/resources/testcase/set/aliasTest/oracle/AliasTest_main_immediately.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,15 @@
<variable name="a" isArrayIndex="false">
<value name="a {true}" typeString="AliasTest.IntWrapper" valueString="a" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
</variable>
<variable name="b" isArrayIndex="false">
<value name="b {true}" typeString="AliasTest.IntWrapper" valueString="b" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
Expand All @@ -52,7 +52,7 @@
<variable name="value" isArrayIndex="false">
<value name="value {equals(b,a)}" typeString="int" valueString="Z(2(#))" isValueAnObject="false" isValueUnknown="false" conditionString="equals(b,a)">
</value>
<value name="value {not(equals(b,a))}" typeString="int" valueString="int::select(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="not(equals(b,a))">
<value name="value {not(equals(b,a))}" typeString="int" valueString="select<[int]>(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="not(equals(b,a))">
</value>
</variable>
</value>
Expand Down Expand Up @@ -151,15 +151,15 @@
<callStateVariable name="a" isArrayIndex="false">
<value name="a {true}" typeString="AliasTest.IntWrapper" valueString="a" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
</callStateVariable>
<callStateVariable name="b" isArrayIndex="false">
<value name="b {true}" typeString="AliasTest.IntWrapper" valueString="b" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
Expand Down Expand Up @@ -269,15 +269,15 @@
<callStateVariable name="a" isArrayIndex="false">
<value name="a {true}" typeString="AliasTest.IntWrapper" valueString="a" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
</callStateVariable>
<callStateVariable name="b" isArrayIndex="false">
<value name="b {true}" typeString="AliasTest.IntWrapper" valueString="a" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
Expand Down
10 changes: 5 additions & 5 deletions ...bolic_execution/src/test/resources/testcase/set/aliasTest/oracle/AliasTest_main_never.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,15 @@
<variable name="a" isArrayIndex="false">
<value name="a {true}" typeString="AliasTest.IntWrapper" valueString="a" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
</variable>
<variable name="b" isArrayIndex="false">
<value name="b {true}" typeString="AliasTest.IntWrapper" valueString="b" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
Expand All @@ -52,7 +52,7 @@
<variable name="value" isArrayIndex="false">
<value name="value {equals(b,a)}" typeString="int" valueString="Z(2(#))" isValueAnObject="false" isValueUnknown="false" conditionString="equals(b,a)">
</value>
<value name="value {not(equals(b,a))}" typeString="int" valueString="int::select(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="not(equals(b,a))">
<value name="value {not(equals(b,a))}" typeString="int" valueString="select<[int]>(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="not(equals(b,a))">
</value>
</variable>
</value>
Expand Down Expand Up @@ -138,15 +138,15 @@ as result of self.main(a, b)&gt;" isReturnValueComputed="true" methodReturnCondi
<callStateVariable name="a" isArrayIndex="false">
<value name="a {true}" typeString="AliasTest.IntWrapper" valueString="a" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,a,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
</callStateVariable>
<callStateVariable name="b" isArrayIndex="false">
<value name="b {true}" typeString="AliasTest.IntWrapper" valueString="b" isValueAnObject="true" isValueUnknown="false" conditionString="true">
<variable name="value" isArrayIndex="false">
<value name="value {true}" typeString="int" valueString="int::select(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
<value name="value {true}" typeString="int" valueString="select<[int]>(heap,b,AliasTest.IntWrapper::$value)" isValueAnObject="false" isValueUnknown="false" conditionString="true">
</value>
</variable>
</value>
Expand Down
Loading
Loading