Automatically Generate EQ Taclets

[Drodt]

Related Issue

This idea was mentioned in #3945 by @unp1.

Intended Change

We have many "EQ taclets" in our taclet base that all follow exactly the same schema. However, as they represent essentially a duplication of logic, it is easy for the "normal" taclets and its EQ version to go out of sync. In #3945 this was observed w.r.t. variable conditions.

This PR makes all of that superfluous, as EQ taclets are generated automatically.

To generate an EQ taclet, add the \generateEQ modifier to it. It takes a term---the term to be put into the \assumes part. Let's look at two examples:

\lemma
lenOfSeqEmpty {
    \find(seqLen(seqEmpty))
    \replacewith(0)
    \heuristics(concrete)
    \generateEQ(seqEmpty)
}

generates the EQ taclet

\lemma
lenOfSeqEmptyEQ {
    \schemaVar \term Seq EQ;
    \assumes(seqEmpty = EQ)
    \find(seqLen(EQ))
    \replacewith(0)
    \heuristics(concrete)
}

Note that all properties of the taclet (annotations, rule sets, etc.) are copied over. The name is automatically extended with "EQ", an \assumes part is added, and seqEmpty is replaced with EQ in the \find and (original) \assumes parts. (Also for the \find of added rules).

You can override the rule sets of the taclet as follows:

\lemma
getOfSeqSingleton {
    \schemaVar \term any x;
    \schemaVar \term int idx;
    \find(seqGet<[alpha]>(seqSingleton(x), idx))
    \replacewith(\if(idx = 0)
            \then((alpha)x)
            \else((alpha)seqGetOutside))
    \heuristics(simplify)
    \generateEQ(seqSingleton(x) : no_self_application, simplify_enlarging)
}

which generates

\lemma
getOfSeqSingletonEQ {
    \schemaVar \term any x;
    \schemaVar \term int idx;
    \schemaVar \term Seq EQ;
    \find(seqGet<[alpha]>(EQ, idx))
    \replacewith(\if(idx = 0)
            \then((alpha)x)
            \else((alpha)seqGetOutside))
    \heuristics(no_self_application, simplify_enlarging)
}

One side effect of all this: Some taclets change names, as the EQ was not at the end of its name previously. Personally, I prefer the consistency.

Plan

• Document code in TacletPBuilder
• Discuss syntax
• Once approved: Document in KeY Docs

Type of pull request

• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: Examined generated taclets.old.txt

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[unp1]

HeapSimplificationMacro and SupportedTaclets use the old names of subsetOf... and reach... that did not follow the normal naming approach

Same for saved SMT settings in:
key.ui/examples/completionscopes/ and key.core/src/test/resources/testcase/merge/

[unp1]

Thanks a lot! Only smaller changes.

One general comment:
Should we check whether the term given in generateEQ occurs in the find term, otherwise a wrong taclet might be easily generated (or is that done and I overlooked it)

[Drodt]

Should we check whether the term given in generateEQ occurs in the find term, otherwise a wrong taclet might be easily generated (or is that done and I overlooked it)

That's not done. I can add it.

[Drodt]

subsetOf

Done

[unp1]

Thanks!