Skip to content
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.

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

Remove SequentFormula class #3478

Draft
wants to merge 17 commits into
base: main
Choose a base branch
from
Draft

Conversation

unp1
Copy link
Member

@unp1 unp1 commented Jun 13, 2024

Intended Change

This PR prepares the ground for generalizing proof and calculus structures.
It removes the superfluous SequentFormula class, which is only a behaviorless
container for a term. The class is a left-over from times when we had formulas with
constraints on the sequent level

It depends on PR #3472 to be merged first as it is based on that branch

Plan

  • Pass tests
  • Code cleanup

Type of pull request

  • Refactoring (behaviour should not change or only minimally change)

Ensuring quality

  • I have tested the feature as follows: tests
  • I have checked that runtime performance has not deteriorated.

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

@unp1 unp1 marked this pull request as draft June 13, 2024 07:56
@unp1 unp1 force-pushed the removeSequentFormula branch 2 times, most recently from 19f4f15 to 9debf5e Compare June 13, 2024 08:09
The class is a left-over from previous times when a formula in the sequent could have a constraint attached. This commit works towards generalizing proof structures
@unp1 unp1 force-pushed the removeSequentFormula branch 2 times, most recently from 2e72f76 to 16f0da5 Compare June 13, 2024 09:06
@unp1 unp1 self-assigned this Jun 13, 2024
@unp1 unp1 added the RFC "Request for comments" is the appeal for making and expressing your opinion on a topic. label Jun 13, 2024
Copy link

codecov bot commented Jun 13, 2024

Codecov Report

Attention: Patch coverage is 52.52918% with 366 lines in your changes missing coverage. Please review.

Project coverage is 38.03%. Comparing base (345c9c6) to head (fca7bd8).
Report is 46 commits behind head on main.

Files Patch % Lines
...java/de/uka/ilkd/key/proof/join/JoinProcessor.java 0.00% 16 Missing ⚠️
...ore/src/main/java/de/uka/ilkd/key/rule/Taclet.java 30.43% 13 Missing and 3 partials ⚠️
...ka/ilkd/key/macros/scripts/InstantiateCommand.java 0.00% 12 Missing ⚠️
.../de/uka/ilkd/key/macros/AbstractBlastingMacro.java 0.00% 11 Missing ⚠️
...core/src/main/java/org/key_project/logic/Term.java 0.00% 11 Missing ⚠️
.../src/main/java/de/uka/ilkd/key/smt/SMTProblem.java 0.00% 8 Missing ⚠️
...ey/strategy/feature/InfFlowContractAppFeature.java 0.00% 8 Missing ⚠️
...de/uka/ilkd/key/macros/scripts/RewriteCommand.java 41.66% 5 Missing and 2 partials ⚠️
...e/uka/ilkd/key/rule/UseDependencyContractRule.java 22.22% 7 Missing ⚠️
...src/main/java/de/uka/ilkd/key/logic/JavaBlock.java 0.00% 6 Missing ⚠️
... and 112 more
Additional details and impacted files
@@             Coverage Diff              @@
##               main    #3478      +/-   ##
============================================
- Coverage     38.03%   38.03%   -0.01%     
- Complexity    17084    17099      +15     
============================================
  Files          2099     2105       +6     
  Lines        127194   127378     +184     
  Branches      21368    21389      +21     
============================================
+ Hits          48375    48443      +68     
- Misses        72856    72972     +116     
  Partials       5963     5963              

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

@WolframPfeifer WolframPfeifer changed the title Remove sequent formula Remove SequentFormula class Oct 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
RFC "Request for comments" is the appeal for making and expressing your opinion on a topic.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants