Fixed operator replacements in WD taclets after changes in PR #3436 (#3484)

Author: WolframPfeifer

key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java

@@ -669,11 +669,10 @@ static RewriteTaclet createTaclet(String name, Term find1, Term find2, Term goal
         assert find1.sub(0).op().name().equals(find2.sub(0).op().name());
         assert find1.sub(0).arity() == find2.sub(0).arity();
 
-        Map<ProgramVariable, ProgramVariable> map =
-            new LinkedHashMap<>();
+        Map<Operator, Operator> map = new LinkedHashMap<>();
         int i = 0;
         for (Term sub : find1.sub(0).subs()) {
-            map.put((ProgramVariable) find2.sub(0).sub(i).op(), (ProgramVariable) sub.op());
+            map.put(find2.sub(0).sub(i).op(), sub.op());
             i++;
         }
         final OpReplacer or = new OpReplacer(map, services.getTermFactory());

key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt

@@ -5400,7 +5400,7 @@ Choices: sequences:on}
 defOfSeqUpd {
 \find(seqUpd(seq,idx,value))
 \varcond(\notFreeIn(uSub (variable), seq (Seq term)), \notFreeIn(uSub (variable), value (any term)), \notFreeIn(uSub (variable), idx (int term)))
-\replacewith(seqDef{uSub (variable)}(Z(0(#)),seqLen(seq),if-then-else(equals(uSub,idx),value,any::seqGet(seq,uSub)))) 
+\replacewith(seqDef{uSub (variable)}(Z(0(#)),seqLen(seq),if-then-else(equals(uSub,idx),value,any::seqGet(seq,uSub))))
 
 Choices: sequences:on}
 -----------------------------------------------------
@@ -9697,7 +9697,7 @@ Choices: sequences:on}
 == getOfSeqUpd (getOfSeqUpd) =========================================
 getOfSeqUpd {
 \find(alpha::seqGet(seqUpd(seq,idx,value),jdx))
-\replacewith(if-then-else(and(and(leq(Z(0(#)),jdx),lt(jdx,seqLen(seq))),equals(idx,jdx)),alpha::cast(value),alpha::seqGet(seq,jdx))) 
+\replacewith(if-then-else(and(and(leq(Z(0(#)),jdx),lt(jdx,seqLen(seq))),equals(idx,jdx)),alpha::cast(value),alpha::seqGet(seq,jdx)))
 \heuristics(simplify_enlarging)
 Choices: sequences:on}
 -----------------------------------------------------
@@ -12135,7 +12135,7 @@ Choices: sequences:on}
 == lenOfSeqUpd (lenOfSeqUpd) =========================================
 lenOfSeqUpd {
 \find(seqLen(seqUpd(seq,idx,value)))
-\replacewith(seqLen(seq)) 
+\replacewith(seqLen(seq))
 \heuristics(simplify)
 Choices: sequences:on}
 -----------------------------------------------------
@@ -16555,22 +16555,22 @@ Choices: true}
 == ssubsortDirect (ssubsortDirect) =========================================
 ssubsortDirect {
 \find(ssubsort(alphSub::ssort,alph::ssort))
-\replacewith(true) 
+\replacewith(true)
 \heuristics(simplify)
 Choices: true}
 -----------------------------------------------------
 == ssubsortSup (ssubsortSup) =========================================
 ssubsortSup {
 \find(ssubsort(alph::ssort,alphSub::ssort))
 \varcond(\not\same(alphSub, alph))
-\replacewith(false) 
+\replacewith(false)
 \heuristics(simplify)
 Choices: true}
 -----------------------------------------------------
 == ssubsortTop (ssubsortTop) =========================================
 ssubsortTop {
 \find(ssubsort(s,anySORT))
-\replacewith(true) 
+\replacewith(true)
 \heuristics(simplify)
 Choices: true}
 -----------------------------------------------------
@@ -17071,8 +17071,8 @@ Choices: programRules:Java}
 -----------------------------------------------------
 == subsortTrans (subsortTrans) =========================================
 subsortTrans {
-\assumes ([ssubsort(s1,s2),ssubsort(s2,s3)]==>[]) 
-\add [ssubsort(s1,s3)]==>[] 
+\assumes ([ssubsort(s1,s2),ssubsort(s2,s3)]==>[])
+\add [ssubsort(s1,s3)]==>[]
 \heuristics(simplify_enlarging)
 Choices: true}
 -----------------------------------------------------

key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPerm.proof

@@ -1,8 +1,8 @@
 \profile "Java Profile";
 
 \settings // Proof-Settings-Config-File
-{ 
-    "Choice" : { 
+{
+    "Choice" : {
         "JavaCard" : "JavaCard:off",
         "Strings" : "Strings:on",
         "assertions" : "assertions:safe",
@@ -24,10 +24,10 @@
         "wdChecks" : "wdChecks:off",
         "wdOperator" : "wdOperator:L"
      }
- } 
+ }
 
 \proofObligation // Proof-Obligation settings
-{ 
+{
     "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput",
     "name" : "seqSwapPreservesSeqPerm"
  }

key.core/tacletProofs/seqPerm/Taclet_seqSwapPreservesSeqPermEQ.proof

@@ -1,8 +1,8 @@
 \profile "Java Profile";
 
 \settings // Proof-Settings-Config-File
-{ 
-    "Choice" : { 
+{
+    "Choice" : {
         "JavaCard" : "JavaCard:off",
         "Strings" : "Strings:on",
         "assertions" : "assertions:safe",
@@ -24,10 +24,10 @@
         "wdChecks" : "wdChecks:off",
         "wdOperator" : "wdOperator:L"
      }
- } 
+ }
 
 \proofObligation // Proof-Obligation settings
-{ 
+{
     "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput",
     "name" : "seqSwapPreservesSeqPermEQ"
  }