diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index 9885acd6145..5f9bc869cdb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -22,7 +22,6 @@ import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.rule.merge.MergeRule; -import de.uka.ilkd.key.smt.SMTRuleApp; import de.uka.ilkd.key.strategy.AutomatedRuleApplicationManager; import de.uka.ilkd.key.strategy.QueueRuleApplicationManager; import de.uka.ilkd.key.strategy.Strategy; @@ -627,7 +626,7 @@ public ImmutableList apply(final RuleApp ruleApp) { } else { proof.replace(this, goalList); if (ruleApp instanceof TacletApp tacletApp && tacletApp.taclet().closeGoal() - || ruleApp instanceof SMTRuleApp) { + || ruleApp instanceof AbstractExternalSolverRuleApp) { // the first new goal is the one to be closed proof.closeGoal(goalList.head()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java new file mode 100644 index 00000000000..1e61eff79db --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java @@ -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. + *

+ * {@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 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 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 ifInsts) { + setMutable(ifInsts); + return this; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java index 9674a9ed1b8..b7254570b20 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java @@ -9,22 +9,21 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.rule.AbstractBuiltInRuleApp; +import de.uka.ilkd.key.rule.AbstractExternalSolverRuleApp; import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.RuleApp; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.NonNull; + /** - * The rule application that is used when a goal is closed by means of an external solver. So far it + * The rule application that is used when a goal is closed by means of an SMT solver. So far it * stores the rule that that has been used and a title containing some information for the user. */ -public class SMTRuleApp extends AbstractBuiltInRuleApp { - +public class SMTRuleApp extends AbstractExternalSolverRuleApp { public static final SMTRule RULE = new SMTRule(); - private final String title; - private final String successfulSolverName; /** * Create a new rule app without ifInsts (will be null). @@ -37,11 +36,10 @@ public class SMTRuleApp extends AbstractBuiltInRuleApp { this(rule, pio, null, successfulSolverName); } - SMTRuleApp(SMTRule rule, PosInOccurrence pio, ImmutableList unsatCore, + SMTRuleApp(ExternalSolverRule rule, PosInOccurrence pio, + ImmutableList unsatCore, String successfulSolverName) { - super(rule, pio, unsatCore); - this.title = "SMT: " + successfulSolverName; - this.successfulSolverName = successfulSolverName; + super(rule, pio, unsatCore, successfulSolverName, "SMT: " + successfulSolverName); } @Override @@ -49,27 +47,15 @@ public SMTRuleApp replacePos(PosInOccurrence newPos) { return new SMTRuleApp(RULE, newPos, ifInsts, successfulSolverName); } - public String getTitle() { - return title; - } - - public String getSuccessfulSolverName() { - return successfulSolverName; - } - @Override public BuiltInRule rule() { return RULE; } - @Override - public String displayName() { - return title; - } - - public static class SMTRule implements BuiltInRule { + public static class SMTRule implements ExternalSolverRule { public static final Name name = new Name("SMTRule"); + @Override public SMTRuleApp createApp(String successfulSolverName) { return new SMTRuleApp(this, null, successfulSolverName); } @@ -81,6 +67,7 @@ public SMTRuleApp createApp(String successfulSolverName) { * @param unsatCore formulas required to prove the result * @return rule application instance */ + @Override public SMTRuleApp createApp(String successfulSolverName, ImmutableList unsatCore) { return new SMTRuleApp(this, null, unsatCore, successfulSolverName); @@ -91,13 +78,6 @@ public SMTRuleApp createApp(PosInOccurrence pos, TermServices services) { return new SMTRuleApp(this, null, ""); } - - @Override - public boolean isApplicable(Goal goal, PosInOccurrence pio) { - return false; - } - - /** * Create a new goal (to be closed in {@link Goal#apply(RuleApp)} directly afterwards) * with the same sequent as the given one. @@ -108,6 +88,7 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) { * @return a list with an identical goal as the given goal */ @Override + @NonNull public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) { if (goal.proof().getInitConfig().getJustifInfo().getJustification(RULE) == null) { goal.proof().getInitConfig().registerRule(RULE, () -> false); @@ -115,16 +96,12 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) return goal.split(1); } - @Override - public boolean isApplicableOnSubTerms() { - return false; - } - @Override public String displayName() { return "SMT"; } + @Override public String toString() { return displayName(); } @@ -133,9 +110,9 @@ public String toString() { public Name name() { return name; } - } + @Override public SMTRuleApp setTitle(String title) { return new SMTRuleApp(RULE, pio, ifInsts, title); } @@ -168,5 +145,4 @@ public SMTRuleApp tryToInstantiate(Goal goal) { } return app.setIfInsts(ImmutableList.fromList(ifInsts)); } - }