Moving Strategies to NCore

[unp1]

• Modularize Feature strategies
• Cleanup of IntegerStrategy
• Factor out reasoning about strings in own strategy
• Moves FormulaTag manager to ncore (start of generalizing the indexing structures)
• Move RuleIndex to ncore
• Cleanup TacletApp implementations
• Minor cleanup and nullness annotations
• Simplify "union" logic in SVInstantiations
• Nullness and cleanup of code
• Renaming from ifInstantiation to assumesFormulaInstantiation
• Avoid duplicate check of equal sv instantiations
• Rewrite recursion to iterative solution (in this case the intend is clearer in the iterative one) and nullness annotations
• Nullness fixes and removal of unnecessary casts
• Nullness annotations
• Added and updated comments
• Cleanup TacletApp (and subclasses)
• Move RuleIndex to ncore
• Try to distribute responsibilities for features; this commit has errors
• Added javadoc
• Intermediate commit: Move common features to modular strat; fix: instApp method for instApp
• Clean up
• Modular UI Strategy panel
• Add responsibilities to StringStrategy
• Rename UI text
• Add SymEx strat
• Finish SymExStrategy
• Split program rules from normal rule sets
• Simplify
• Modularize int assign rules
• Conflict resolution
• Spotless
• Add conflict resolution for int
• Add FOL Strat
• Nullability
• Remove LocSet handling from FOLStrat
• Add JFOLStrat
• Split up int rules; fix relative paths in JARs
• Split sequence
• Make paths relative by default; split more rules and headers
• Documentation
• Add proof settings to float files; use correct strategy factory for macros
• Remove printing
• Spotless
• Add .key file ending to relative paths
• Slight performance improvement
• Simplify
• Fix OSS
• Simplify conflict resolution
• Handle built-in rules
• Fix ExprTests (relative paths)
• Regenerate taclet oracle
• Fix OSS
• Add missing Builtin rule to JavaDL strat
• Strategy Dispatcher API refactoring (work-in-progress; does not yet compile)
• Fix reworked dispatch seprataion
• Fix performance regression (add fail fast in approval logic)
• Minor cleanup and correction (approval feature and cost feature were out-of-sync)
• added some comments
• Remove erroneous(?) third slash in URI
• Refactor ModularStrat; add Documentation
• Experiment w/ windows URIs
• Add third slash to URI again
• make Metal the default LaF, create checkbox for defaultLaFDecorated
• Make Metal default when creating new config
• Fix formatting
• Bump the gradle-deps group with 4 updates
• fix KeY does not accept local files KeYProject/key#3721, getParent().toUri() requires absolute paths
• explicit types as requested
• Fixes unbalanced block exception when pretty printing anon heap terms. (+1 squashed commit)
• Ensure opening block before printTerm
• Bump the gradle-deps group with 7 updates
• Start extracting InfFlow and modularization of some rules.
• move RunAllProofsInfFlow.java
• set profile in infflow files + spotless
• fixing separation issues
• fix proof storage, UseOperationContractRule.java
• old proof was not reloadable.
• fix proof
• rip out of WD intro extra module
• i do not understand these assertion in the test case
• fix services and classpath
• fix tests
• fix bug in WhileInvariantRule
• fixing justification problem
• working on WD
• fixing InfFlowWhileInvariantRule and App
• IDX_GOAL_WD constant
• disable functional tests in infflow
• formatting
• activate WD proofs
• loading options improvements, renaming of Profile methods
• fix ProofReplayer
• fix Taclet generation
• using getUseDependencyContractRule in replay
• fix IntermediateProofReplayer
• fix cost computation
• replace identify with sub-class for cost computation
• further fixes on WD profile
• clean-up Proof Replayer
• change Taclet base to list of RuleSource
• externalize wd rules
• fixes Information Flow proofs are not re-loadable KeYProject/key#3714 -- maybe
• Don't check VarCondNotFreeIn for TermLabelSVs
• Remove pointless error logging; cast instead
• fix naming problems
• Making the specification of an example well-defined
• solve not findable WD contracts
• disable unprovable and out-dated test cases
• fix test case, wrong contract name
• add a script for reformatting a stack of commits
• prepare master merge
• clean build.gradle
• configure new respositories/plugin for nexus
• clean up github actions, more deployment into build.gradle
• minor javadoc corrections
• add deployment to our gitlab server
• Fix nullchecker
• fix windows path
• Moved ComponentStrategy to ncore

Related Issue

This pull request resolves #.

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.
• For new Gradle modules: I added the Gradle module to the test matrix in
  .github/workflows/tests.yml

Additional information and contact(s)

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

[Drodt]

No.