Skip to content

repair the axiom generation for adts defined in JavaDL#3556

Merged
wadoon merged 1 commit intoKeYProject:mainfrom
mattulbrich:adtAxiomRepair
Feb 20, 2025
Merged

repair the axiom generation for adts defined in JavaDL#3556
wadoon merged 1 commit intoKeYProject:mainfrom
mattulbrich:adtAxiomRepair

Conversation

@mattulbrich
Copy link
Copy Markdown
Member

Related Issue

This pull request addresses #3427, but does not solve it.

Intended Change

The axiom taclet created for adt was not applicable. It is applicable now.

Plan

  • remove the "notFreeIn" clause from the generated taclet
  • remove the find clause from the taclet.

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • There are changes to the (Java) code

Ensuring quality

  • I have tested the feature as follows: Looked at the translation of a few examples

It is a small change in the creation of a taclet.

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

@mattulbrich mattulbrich requested a review from wadoon February 19, 2025 15:26
@mattulbrich
Copy link
Copy Markdown
Member Author

Addressed during the 3rd HacKeYthon.

@codecov
Copy link
Copy Markdown

codecov Bot commented Feb 19, 2025

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 38.33%. Comparing base (a0c4f81) to head (46ef350).
Report is 13 commits behind head on main.

Additional details and impacted files
@@             Coverage Diff              @@
##               main    #3556      +/-   ##
============================================
- Coverage     38.33%   38.33%   -0.01%     
+ Complexity    17258    17257       -1     
============================================
  Files          2111     2111              
  Lines        127632   127630       -2     
  Branches      21461    21461              
============================================
- Hits          48926    48923       -3     
  Misses        72695    72695              
- Partials       6011     6012       +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

Comment thread key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java Outdated
@wadoon wadoon added this pull request to the merge queue Feb 20, 2025
Merged via the queue into KeYProject:main with commit 824af63 Feb 20, 2025
@WolframPfeifer WolframPfeifer moved this from In Progress to Done in 3rd HacKeYthon Feb 28, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

Status: Done

Development

Successfully merging this pull request may close these issues.

3 participants