|
| 1 | +package de.uka.ilkd.key.macros.scripts; |
| 2 | + |
| 3 | +import de.uka.ilkd.key.logic.*; |
| 4 | +import de.uka.ilkd.key.logic.op.SchemaVariable; |
| 5 | +import de.uka.ilkd.key.macros.scripts.meta.Option; |
| 6 | +import de.uka.ilkd.key.proof.Goal; |
| 7 | +import de.uka.ilkd.key.rule.FindTaclet; |
| 8 | +import de.uka.ilkd.key.rule.PosTacletApp; |
| 9 | +import de.uka.ilkd.key.rule.Taclet; |
| 10 | +import de.uka.ilkd.key.rule.TacletApp; |
| 11 | +import de.uka.ilkd.key.rule.inst.SVInstantiations; |
| 12 | +import org.key_project.util.collection.ImmutableList; |
| 13 | + |
| 14 | +import java.util.Iterator; |
| 15 | +import java.util.Set; |
| 16 | + |
| 17 | +/** |
| 18 | + * The command "focus" allows you to select formulas from the current sequent |
| 19 | + * to focus verification on. This means that all other formulas are discarded |
| 20 | + * (i.e. hidden using hide_right, hide_left). |
| 21 | + * |
| 22 | + * Benefits are: The automation is guided into focussing on a relevant set of |
| 23 | + * formulas. |
| 24 | + * |
| 25 | + * The selected set of sequent formulas can be regarded as an equivalent to an |
| 26 | + * unsat core. |
| 27 | + * |
| 28 | + * @author Created by sarah on 1/12/17. |
| 29 | + * @author Mattias Ulbrich, 2023 |
| 30 | + */ |
| 31 | +public class FocusCommand extends AbstractCommand<FocusCommand.Parameters> { |
| 32 | + |
| 33 | + public FocusCommand() { |
| 34 | + super(Parameters.class); |
| 35 | + } |
| 36 | + |
| 37 | + static class Parameters { |
| 38 | + @Option("#2") |
| 39 | + public Sequent toKeep; |
| 40 | + } |
| 41 | + |
| 42 | + @Override |
| 43 | + public void execute(Parameters s) throws ScriptException, InterruptedException { |
| 44 | + if (s == null) { |
| 45 | + throw new ScriptException("Missing 'sequent' argument for focus"); |
| 46 | + } |
| 47 | + |
| 48 | + Sequent toKeep = s.toKeep; |
| 49 | + |
| 50 | + hideAll(toKeep); |
| 51 | + } |
| 52 | + |
| 53 | + @Override |
| 54 | + public String getName() { |
| 55 | + return "focus"; |
| 56 | + } |
| 57 | + |
| 58 | + /** |
| 59 | + * Hide all formulas of the sequent that are not on focus sequent |
| 60 | + * |
| 61 | + * @param toKeep sequent containing formulas to keep |
| 62 | + * @throws ScriptException if no goal is currently open |
| 63 | + */ |
| 64 | + private void hideAll(Sequent toKeep) throws ScriptException { |
| 65 | + Goal goal = state.getFirstOpenAutomaticGoal(); |
| 66 | + assert goal != null : "not null by contract of the method"; |
| 67 | + |
| 68 | + // The formulas to keep in the antecedent |
| 69 | + ImmutableList<Term> keepAnte = toKeep.antecedent().asList().map(SequentFormula::formula); |
| 70 | + ImmutableList<SequentFormula> ante = goal.sequent().antecedent().asList(); |
| 71 | + |
| 72 | + for (SequentFormula seqFormula : ante) { |
| 73 | + // This means "!keepAnte.contains(seqFormula.formula)" but with equality mod renaming! |
| 74 | + if (!keepAnte.exists(it -> it.equalsModRenaming(seqFormula.formula()))) { |
| 75 | + Taclet tac = getHideTaclet("left"); |
| 76 | + makeTacletApp(goal, seqFormula, tac, true); |
| 77 | + } |
| 78 | + } |
| 79 | + |
| 80 | + ImmutableList<Term> keepSucc = toKeep.succedent().asList().map(SequentFormula::formula); |
| 81 | + ImmutableList<SequentFormula> succ = goal.sequent().succedent().asList(); |
| 82 | + for (SequentFormula seqFormula : succ) { |
| 83 | + if (!keepSucc.exists(it -> it.equalsModRenaming(seqFormula.formula()))) { |
| 84 | + Taclet tac = getHideTaclet("right"); |
| 85 | + makeTacletApp(goal, seqFormula, tac, false); |
| 86 | + } |
| 87 | + } |
| 88 | + } |
| 89 | + |
| 90 | + // determine where formula in sequent and apply either hide_left or hide_right |
| 91 | + private Taclet getHideTaclet(String pos) { |
| 92 | + String ruleName = "hide_" + pos; |
| 93 | + return proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(ruleName)); |
| 94 | + } |
| 95 | + |
| 96 | + /** |
| 97 | + * Make tacletApp for one sequent formula to hide on the sequent |
| 98 | + * |
| 99 | + * @param g the goal on which this hide rule should be applied to |
| 100 | + * @param toHide the sequent formula to hide |
| 101 | + * @param tac the taclet top apply (either hide_left or hide_right) |
| 102 | + * @param antec whether the formula is in the antecedent |
| 103 | + */ |
| 104 | + private void makeTacletApp(Goal g, SequentFormula toHide, Taclet tac, boolean antec) { |
| 105 | + |
| 106 | + // hide rules only applicable to top-level terms/sequent formulas |
| 107 | + PosInTerm pit = PosInTerm.getTopLevel(); |
| 108 | + |
| 109 | + PosInOccurrence pio = new PosInOccurrence(toHide, pit, antec); |
| 110 | + |
| 111 | + Set<SchemaVariable> svs = tac.collectSchemaVars(); |
| 112 | + assert svs.size() == 1; |
| 113 | + Iterator<SchemaVariable> iter = svs.iterator(); |
| 114 | + SchemaVariable sv = (SchemaVariable) iter.next(); |
| 115 | + |
| 116 | + SVInstantiations inst = SVInstantiations.EMPTY_SVINSTANTIATIONS; |
| 117 | + |
| 118 | + TacletApp app = |
| 119 | + PosTacletApp.createPosTacletApp((FindTaclet) tac, inst, pio, proof.getServices()); |
| 120 | + app = app.addCheckedInstantiation(sv, toHide.formula(), proof.getServices(), true); |
| 121 | + g.apply(app); |
| 122 | + |
| 123 | + } |
| 124 | + |
| 125 | +} |
| 126 | + |
0 commit comments