From 3bdb527880bea77759a4cc720a2392fd8a78573a Mon Sep 17 00:00:00 2001 From: Nils Buchholz Date: Wed, 23 Oct 2024 11:23:19 +0200 Subject: [PATCH] add AbstractExternalSolverRuleApp to allow other external solvers to close goals --- .../main/java/de/uka/ilkd/key/proof/Goal.java | 3 +- .../rule/AbstractExternalSolverRuleApp.java | 178 ++++++++++++++++++ .../java/de/uka/ilkd/key/smt/SMTRuleApp.java | 54 ++---- 3 files changed, 195 insertions(+), 40 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java 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..f5c03dd030e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java @@ -0,0 +1,178 @@ +/* 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 java.util.ArrayList; +import java.util.List; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.logic.Name; +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 ExternalSolverRule rule; + 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.rule = rule.newRule(); + 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 BuiltInRule rule() { + return rule; + } + + @Override + public String displayName() { + return title; + } + + /** + * Interface for the rules of external solvers + */ + public interface ExternalSolverRule extends BuiltInRule { + Name name = new Name("ExternalSolverRule"); + + ExternalSolverRule newRule(); + + 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; + } + + + /** + * Create a new goal (to be closed in {@link Goal#apply(RuleApp)} directly afterwards) + * with the same sequent as the given one. + * + * @param goal the Goal on which to apply ruleApp + * @param services the Services with the necessary information about the java programs + * @param ruleApp the rule application to be executed + * @return a list with an identical goal as the given goal + */ + @Override + default ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) { + if (goal.proof().getInitConfig().getJustifInfo().getJustification(newRule()) == null) { + goal.proof().getInitConfig().registerRule(newRule(), () -> false); + } + return goal.split(1); + } + + @Override + default boolean isApplicableOnSubTerms() { + return false; + } + + @Override + default String displayName() { + return "ExternalSolver"; + } + + @Override + String toString(); + + @Override + default Name name() { + return name; + } + + } + + /** + * 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; + } + + /** + * Create a new RuleApp with the same pio (in this case, that will probably be null as the + * AbstractExternalSolver rule is applied to the complete sequent) as this one. + * Add all top level formulas of the goal + * to the RuleApp's ifInsts. + * + * @param goal the goal to instantiate the current RuleApp on + * @return a new RuleApp with the same pio and all top level formulas of the goal as ifInsts + */ + @Override + public AbstractExternalSolverRuleApp tryToInstantiate(Goal goal) { + AbstractExternalSolverRuleApp app = rule.createApp(pio, goal.proof().getServices()); + Sequent seq = goal.sequent(); + List ifInsts = new ArrayList<>(); + for (SequentFormula ante : seq.antecedent()) { + ifInsts.add(new PosInOccurrence(ante, PosInTerm.getTopLevel(), true)); + } + for (SequentFormula succ : seq.succedent()) { + ifInsts.add(new PosInOccurrence(succ, PosInTerm.getTopLevel(), false)); + } + return app.setIfInsts(ImmutableList.fromList(ifInsts)); + } + +} 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..ef4b9b38087 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,7 +9,7 @@ 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; @@ -17,14 +17,11 @@ 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 + * 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 +34,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 +45,20 @@ 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 ExternalSolverRule newRule() { + return new SMTRule(); + } + + @Override public SMTRuleApp createApp(String successfulSolverName) { return new SMTRuleApp(this, null, successfulSolverName); } @@ -81,6 +70,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 +81,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. @@ -115,16 +98,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 +112,9 @@ public String toString() { public Name name() { return name; } - } + @Override public SMTRuleApp setTitle(String title) { return new SMTRuleApp(RULE, pio, ifInsts, title); } @@ -168,5 +147,4 @@ public SMTRuleApp tryToInstantiate(Goal goal) { } return app.setIfInsts(ImmutableList.fromList(ifInsts)); } - }