-
Notifications
You must be signed in to change notification settings - Fork 27
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge remote-tracking branch 'origin/main' into mulbrichPolymorphic
* origin/main: (46 commits) spotless update removed default implementations for AbstractExternalSolverRuleApp around RULE field small formatting change Bump the gradle-deps group with 6 updates Bump JetBrains/qodana-action in the github-actions-deps group set version to 2.12.4-dev increase java version to 21 added missing conversion rules from javaUnaryMinusFloat/Double to negFloat/Double add AbstractExternalSolverRuleApp to allow other external solvers to close goals fixes NullPointerException, when using compareTo with locations that dont have a URI or position Bump the github-actions-deps group with 2 updates Bump the gradle-deps group with 5 updates formatting Bump the github-actions-deps group with 2 updates Bump the gradle-deps group with 8 updates spotless generating ProofTree tooltips lazily, options to disable them completely fix for visual bug with overlapping/unreadable text in color settings Fox copyright year Bump the gradle-deps group with 6 updates ...
- Loading branch information
Showing
55 changed files
with
1,186 additions
and
614 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
112 changes: 112 additions & 0 deletions
112
key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,112 @@ | ||
| /* This file is part of KeY - https://key-project.org | ||
| * KeY is licensed under the GNU General Public License Version 2 | ||
| * SPDX-License-Identifier: GPL-2.0-only */ | ||
| package de.uka.ilkd.key.rule; | ||
|
|
||
| import de.uka.ilkd.key.logic.*; | ||
| import de.uka.ilkd.key.proof.Goal; | ||
|
|
||
| import org.key_project.util.collection.ImmutableList; | ||
|
|
||
| /** | ||
| * The rule application that is used when a goal is closed by means of an external solver. So far it | ||
| * stores the rule that that has been used and a title containing some information for the user. | ||
| * <p> | ||
| * {@link de.uka.ilkd.key.smt.SMTRuleApp} | ||
| */ | ||
| public abstract class AbstractExternalSolverRuleApp extends AbstractBuiltInRuleApp { | ||
| protected final String title; | ||
| protected final String successfulSolverName; | ||
|
|
||
| /** | ||
| * Creates a new AbstractExternalSolverRuleApp, | ||
| * | ||
| * @param rule the ExternalSolverRule to apply | ||
| * @param pio the position in the term to apply the rule to | ||
| * @param unsatCore an unsat core consisting of the formulas that are needed to prove the goal | ||
| * (optional null) | ||
| * @param successfulSolverName the name of the solver used to find the proof | ||
| * @param title the title of this rule app | ||
| */ | ||
| protected AbstractExternalSolverRuleApp(ExternalSolverRule rule, PosInOccurrence pio, | ||
| ImmutableList<PosInOccurrence> unsatCore, | ||
| String successfulSolverName, String title) { | ||
| super(rule, pio, unsatCore); | ||
| this.title = title; | ||
| this.successfulSolverName = successfulSolverName; | ||
| } | ||
|
|
||
| /** | ||
| * Gets the title of this rule application | ||
| * | ||
| * @return title of this application | ||
| */ | ||
| public String getTitle() { | ||
| return title; | ||
| } | ||
|
|
||
| /** | ||
| * Gets the name of the successful solver | ||
| * | ||
| * @return name of the successful solver | ||
| */ | ||
| public String getSuccessfulSolverName() { | ||
| return successfulSolverName; | ||
| } | ||
|
|
||
| @Override | ||
| public String displayName() { | ||
| return title; | ||
| } | ||
|
|
||
| /** | ||
| * Interface for the rules of external solvers | ||
| */ | ||
| public interface ExternalSolverRule extends BuiltInRule { | ||
| AbstractExternalSolverRuleApp createApp(String successfulSolverName); | ||
|
|
||
| /** | ||
| * Create a new rule application with the given solver name and unsat core. | ||
| * | ||
| * @param successfulSolverName solver that produced this result | ||
| * @param unsatCore formulas required to prove the result | ||
| * @return rule application instance | ||
| */ | ||
| AbstractExternalSolverRuleApp createApp(String successfulSolverName, | ||
| ImmutableList<PosInOccurrence> unsatCore); | ||
|
|
||
| @Override | ||
| AbstractExternalSolverRuleApp createApp(PosInOccurrence pos, TermServices services); | ||
|
|
||
|
|
||
| @Override | ||
| default boolean isApplicable(Goal goal, PosInOccurrence pio) { | ||
| return false; | ||
| } | ||
|
|
||
| @Override | ||
| default boolean isApplicableOnSubTerms() { | ||
| return false; | ||
| } | ||
|
|
||
| @Override | ||
| String displayName(); | ||
|
|
||
| @Override | ||
| String toString(); | ||
| } | ||
|
|
||
| /** | ||
| * Sets the title (needs to create a new instance for this) | ||
| * | ||
| * @param title new title for rule app | ||
| * @return copy of this with the new title | ||
| */ | ||
| public abstract AbstractExternalSolverRuleApp setTitle(String title); | ||
|
|
||
| @Override | ||
| public AbstractExternalSolverRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts) { | ||
| setMutable(ifInsts); | ||
| return this; | ||
| } | ||
| } |
Oops, something went wrong.