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.

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

Jump to bottom

Ncore taclets #15

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

Ncore taclets #15

wants to merge 221 commits into from
+223,853 −17,914

Conversation

Drodt
Copy link
Owner

@Drodt Drodt commented Nov 13, 2024

Related Issue

This pull request addresses #.

Intended Change

Plan

  • Implement feature 1
  • Implement feature 2
  • Code cleanup
  • Document the changes

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • Refactoring (behaviour should not change or only minimally change)
  • 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
  • There are changes to the deployment/CI infrastructure (gradle, github, ...)
  • Other:

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: ...
  • I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

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

Drodt and others added 30 commits June 5, 2024 16:52
@Drodt
Add simplified Rust parser
b1bbfdf
@unp1
initial commit for generalizing data structures representing calculi
b0220bd
@unp1
more refactoring
704070f
@unp1
polish
9debf5e
@Drodt
Add AST classes
b99b975
@Drodt
Types, ops, and idents
5c6cbac
@Drodt
Convert to KeY AST
7bc8e41
@Drodt
Add ops and term
e02f171
@Drodt
TermFactory
adde184
@Drodt
Move Namespac
02bba08
@Drodt
Namespaces
f489dea
@Drodt
LDTs
a53a5d2
@Drodt
Spotless
76a08c4
@Drodt
Add taclet files
13414d8
@Drodt
Split grammars
e61c708
@Drodt
Merge branch 'main' into rusty-while
33201ff
@Drodt
TermBuilder and LDTs
d791592
@Drodt
Extend TermBuilder
5b7df1f
@Drodt
Basic KeY-File infrastructure
0d2996a
@Drodt
KeYUserProblemFile and friends
7077abe
@Drodt
Add SVs
39b1f4b
@Drodt
Spotless
fea930e
@Drodt
Make SimpleExpressionSort proper
f682fe1
@Drodt
Taclets
0d57115
@Drodt
Merge branch 'main' into rusty-while
e3a4ee7
@Drodt
Fix int literals and test
75b9809
@Drodt
Add more taclets
4f5b3f9
@Drodt
NoFindTaclet
bd87d2e
@Drodt
TacletBuilder
2b05b74
@Drodt
Printing + fix
30ef7f1
unp1 added 27 commits January 24, 2025 09:57
@unp1
Make proof listener list and its usage thread safe in ProofObject
f12da11 
The previous implementation synchronized on the listener list which was immutable. While this solved iterating over the listeners in a thread safe manner, the problem is when adding or removing the list is replaced while threads might synchronize on the old list.
@unp1
Minor code cleanup
d19468c 
- removed some warnings of unused annotations and similar
@unp1
Consistent and improved naming of method parameters and local variables
97c768d
@unp1
Fix JavaDoc warning in key.core
bc3855a
@unp1
Commented FormulaChangeInfo and removed unnecessary method
19da35d
@unp1
Improve comments in Semisequent, more consistent naming of method par…
36e2543 
…ameters and removal of private oneliner delegation methods
@unp1
Improved and completed API documentation of the Sequent class
9daa7bc
@unp1
Started to move prover main loop to ncore
0affcc9
@unp1
Moved termfeatures to ncore and replaced some term feature implementa…
2db8253 
…tions by combinations of existing ones
@unp1
Moved ApplyTFFeature to ncore
8b9b059
@unp1
Minor clean up
6bd1365
@unp1
Cleaned up strategy features
fd6cea7 
* Removed unused feature implementaiton
* Replaced feature Java implementation by termfeature combinations
@unp1
Generalized TermLabel feature to generic TermPredicateFeature.
18a1890 
- ConstantTermFeature now realized via TermPredicateFeature
@unp1
Minor cleanup
30c0b46 
* added missing Override annotations
* marked Feature and TermFeature as FunctionalInterface
@unp1
Moved more strategy features to ncore
bba2f81
@unp1
Moved several termgenerators to ncore
9aeec12
@unp1
Slight reorganisation of the package structure concerning the default…
8eb68ba 
… implementation of the main prover loop
@unp1
Fix introduce bug in AutomatedRuleFeature
8512d58
@unp1
Moved more rule filters to ncore
be12a5d
@unp1
Moved last remaining rule filter to ncore
ec648e3
@unp1
Progress on generalization of taclet application indices
0e74951 
- use as far as possible ncore term and operators
- removal of unnecessary casts
@unp1
Modernized Java used in TacletIndex
add6f70
@unp1
Minor clean up in AbstractProofReplayer
2eabcd6
@unp1
Fix SymbolicExecutionStrategy
233fdb5
@unp1
Added and improved comments
40ff7c6
@unp1
Remove generic from Feature class declarations
619275a
@unp1
Minor code cleanup
be361cb 
Add missing @OverRide annotations
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@Drodt @unp1 @tobias-rnh