it;
if (antec != null) {
// Result has already been computed. No need to recompute.
@@ -53,7 +53,7 @@ protected void filterSequent() {
antec = ImmutableSLList.nil();
it = originalSequent.antecedent().iterator();
while (it.hasNext()) {
- SequentFormula sf = it.next();
+ Term sf = it.next();
lp.reset();
lp.printConstrainedFormula(sf);
String formString = lp.result();
@@ -66,7 +66,7 @@ protected void filterSequent() {
succ = ImmutableSLList.nil();
it = originalSequent.succedent().iterator();
while (it.hasNext()) {
- SequentFormula sf = it.next();
+ Term sf = it.next();
lp.reset();
lp.printConstrainedFormula(sf);
String formString = lp.result();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/IdentitySequentPrintFilter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/IdentitySequentPrintFilter.java
index ae73d537ebb..6230c2ea20b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/IdentitySequentPrintFilter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/IdentitySequentPrintFilter.java
@@ -3,7 +3,7 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.pp;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import org.key_project.util.collection.ImmutableList;
@@ -24,11 +24,11 @@ protected void filterSequent() {
/**
*
- * @param sequentFormula the formula to filter
+ * @param fml the formula to filter
* @return the FilterEntry from the formula
*/
- protected SequentPrintFilterEntry filterFormula(SequentFormula sequentFormula) {
- return new IdentityFilterEntry(sequentFormula);
+ protected SequentPrintFilterEntry filterFormula(Term fml) {
+ return new IdentityFilterEntry(fml);
}
/**
@@ -60,14 +60,14 @@ public static class IdentityFilterEntry implements SequentPrintFilterEntry {
/**
* the original Formula being filtered
*/
- final SequentFormula originalFormula;
+ final Term originalFormula;
/**
* constructor
*
* @param originalFormula the original formula to be filtered
*/
- IdentityFilterEntry(SequentFormula originalFormula) {
+ IdentityFilterEntry(Term originalFormula) {
this.originalFormula = originalFormula;
}
@@ -76,7 +76,7 @@ public static class IdentityFilterEntry implements SequentPrintFilterEntry {
*
* @return the original formula
*/
- public SequentFormula getFilteredFormula() {
+ public Term getFilteredFormula() {
return originalFormula;
}
@@ -85,7 +85,7 @@ public SequentFormula getFilteredFormula() {
*
* @return the original formula
*/
- public SequentFormula getOriginalFormula() {
+ public Term getOriginalFormula() {
return originalFormula;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/InitialPositionTable.java b/key.core/src/main/java/de/uka/ilkd/key/pp/InitialPositionTable.java
index 33a568bcc7b..854726f7709 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/InitialPositionTable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/InitialPositionTable.java
@@ -5,7 +5,7 @@
import de.uka.ilkd.key.logic.IntIterator;
import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
@@ -13,7 +13,7 @@
/**
* An InitialPositionTable is a PositionTable that describes the beginning of the element/subelement
* relationship. Thus, an InitialPositionTable describes the information on where the
- * {@link SequentFormula}e of a sequent are located. It is the root of the tree of PositionTables
+ * {@link Term}e of a sequent are located. It is the root of the tree of PositionTables
* and may be asked for a PosInSequent for a given index position and a given Sequent.
*
*
@@ -80,7 +80,7 @@ private PosInSequent getTopPIS(ImmutableList posList, SequentPrintFilte
/**
* Returns the path for a given PosInOccurrence. This is built up from the initial 0, the number
- * of the SequentFormula in the sequent, the position in the constrained formula, and possibly
+ * of the Term in the sequent, the position in the constrained formula, and possibly
* inside a Metavariable instantiation.
*
* @param pio the given PosInOccurrence
@@ -90,7 +90,7 @@ private PosInSequent getTopPIS(ImmutableList posList, SequentPrintFilte
public ImmutableList pathForPosition(PosInOccurrence pio, SequentPrintFilter filter) {
ImmutableList p = ImmutableSLList.nil();
p = prependPathInFormula(p, pio);
- int index = indexOfCfma(pio.sequentFormula(), filter);
+ int index = indexOfCfma(pio.sequentLevelFormula(), filter);
if (index == -1) {
return null;
}
@@ -116,7 +116,7 @@ private ImmutableList prependPathInFormula(ImmutableList p,
* @param filter the current filter
* @return the index of the given formula in the sequent as printed
*/
- private int indexOfCfma(SequentFormula cfma, SequentPrintFilter filter) {
+ private int indexOfCfma(Term cfma, SequentPrintFilter filter) {
ImmutableList list =
filter.getFilteredAntec().append(filter.getFilteredSucc());
int k;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
index 409c6dd32cd..0ab328fcaf8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
@@ -751,8 +751,8 @@ public void printSemisequent(ImmutableList formulas) {
*
* @param cfma the constrained formula to be printed
*/
- public void printConstrainedFormula(SequentFormula cfma) {
- printTerm(cfma.formula());
+ public void printConstrainedFormula(Term cfma) {
+ printTerm(cfma);
}
/**
@@ -816,11 +816,11 @@ void printLabels(Term t, String left, String right) {
afterFirst = true;
}
layouter.print(l.name().toString());
- if (l.getChildCount() > 0) {
+ if (l.getTLChildCount() > 0) {
layouter.print("(").beginC();
- for (int i = 0; i < l.getChildCount(); i++) {
- layouter.print("\"" + l.getChild(i).toString() + "\"");
- if (i < l.getChildCount() - 1) {
+ for (int i = 0; i < l.getTLChildCount(); i++) {
+ layouter.print("\"" + l.getTLChild(i).toString() + "\"");
+ if (i < l.getTLChildCount() - 1) {
layouter.print(",").ind(1, 2);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PosInSequent.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PosInSequent.java
index ce8f82b1e2a..93a17a13cc6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/PosInSequent.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PosInSequent.java
@@ -31,11 +31,11 @@ public static PosInSequent createSequentPos() {
}
/**
- * creates a PosInSequent that points to a SequentFormula described by a PosInOccurrence.
- * Additionally a boolean indicates whether the the whole SequentFormula or just the formula is
+ * creates a PosInSequent that points to a Term described by a PosInOccurrence.
+ * Additionally a boolean indicates whether the the whole Term or just the formula is
* meant.
*
- * @param posInOcc the PositionInOccurrence describing the SequentFormula and maybe a subterm of
+ * @param posInOcc the PositionInOccurrence describing the Term and maybe a subterm of
* its formula.
*/
public static PosInSequent createCfmaPos(PosInOccurrence posInOcc) {
@@ -92,7 +92,7 @@ public Range getFirstJavaStatementRange() {
/**
- * returns the PosInOccurrence if the PosInSequent marks a SequentFormula or parts of it, null
+ * returns the PosInOccurrence if the PosInSequent marks a Term or parts of it, null
* otherwise.
*/
public PosInOccurrence getPosInOccurrence() {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PositionTable.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PositionTable.java
index 1ffebb4e6d7..1ba59a1e63e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/PositionTable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PositionTable.java
@@ -5,7 +5,7 @@
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.PosInTerm;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
@@ -44,7 +44,7 @@ public class PositionTable {
private final int rows;
/**
- * creates a new PositionTable with the number of subterms (or number of SequentFormula in a
+ * creates a new PositionTable with the number of subterms (or number of Term in a
* Semisequent, or the number of Semisequents in a Sequent, etc.)
*
* @param rows the number of direct sub-elements in the term whose position information is
@@ -243,7 +243,7 @@ protected PosInSequent getSequentPIS(ImmutableList posList,
// This can raise a NPE sporadically. (MU 19)
// This raises an NPE repeatably (JS/MU 21) #1650
- SequentFormula cfma = filterEntry.getOriginalFormula();
+ Term cfma = filterEntry.getOriginalFormula();
PosInOccurrence currentPos = new PosInOccurrence(cfma, PosInTerm.getTopLevel(),
filter.getOriginalSequent().antecedent().contains(cfma));
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/RegroupSequentPrintFilter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/RegroupSequentPrintFilter.java
index b2ec7475952..85ad34827a4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/RegroupSequentPrintFilter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/RegroupSequentPrintFilter.java
@@ -7,7 +7,7 @@
import java.util.regex.Matcher;
import java.util.regex.Pattern;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.pp.IdentitySequentPrintFilter.IdentityFilterEntry;
import org.key_project.util.collection.ImmutableSLList;
@@ -33,7 +33,7 @@ public RegroupSequentPrintFilter(SequentViewLogicPrinter lp, boolean regex) {
@Override
protected void filterSequent() {
- Iterator it;
+ Iterator it;
if (searchString == null || searchString.length() < 3) {
filterIdentity();
@@ -48,7 +48,7 @@ protected void filterSequent() {
antec = ImmutableSLList.nil();
it = originalSequent.antecedent().iterator();
while (it.hasNext()) {
- SequentFormula sf = it.next();
+ Term sf = it.next();
lp.reset();
lp.printConstrainedFormula(sf);
String formString = lp.result();
@@ -63,7 +63,7 @@ protected void filterSequent() {
succ = ImmutableSLList.nil();
it = originalSequent.succedent().iterator();
while (it.hasNext()) {
- SequentFormula sf = it.next();
+ Term sf = it.next();
lp.reset();
lp.printConstrainedFormula(sf);
String formString = lp.result();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilter.java
index 0018fe2a215..4d54c77793a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilter.java
@@ -6,7 +6,7 @@
import java.util.Iterator;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.pp.IdentitySequentPrintFilter.IdentityFilterEntry;
import org.key_project.util.collection.ImmutableList;
@@ -83,7 +83,7 @@ public ImmutableList getFilteredSucc() {
*/
protected void filterIdentity() {
antec = ImmutableSLList.nil();
- Iterator it = originalSequent.antecedent().iterator();
+ Iterator it = originalSequent.antecedent().iterator();
while (it.hasNext()) {
antec = antec.append(new IdentityFilterEntry(it.next()));
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilterEntry.java b/key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilterEntry.java
index dd1e2b42fad..91129b4dc5f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilterEntry.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/SequentPrintFilterEntry.java
@@ -3,7 +3,7 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.pp;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
/**
@@ -15,11 +15,11 @@ public interface SequentPrintFilterEntry {
/**
* Formula to display
*/
- SequentFormula getFilteredFormula();
+ Term getFilteredFormula();
/**
* Original formula from sequent
*/
- SequentFormula getOriginalFormula();
+ Term getOriginalFormula();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/ShowSelectedSequentPrintFilter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/ShowSelectedSequentPrintFilter.java
index 9ac6e9acc4b..ac229e5c847 100755
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/ShowSelectedSequentPrintFilter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/ShowSelectedSequentPrintFilter.java
@@ -4,7 +4,7 @@
package de.uka.ilkd.key.pp;
import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
@@ -65,25 +65,26 @@ public static final class Entry implements SequentPrintFilterEntry {
/**
* The filtered formula, i.e., the formula at {@code pos}.
*/
- private final SequentFormula filtered;
+ private final Term filtered;
/**
* The origin formula, i.e., the formula at {@code pos.getTopLevel()}.
*/
- private final SequentFormula original;
+ private final Term original;
private Entry(PosInOccurrence pos) {
- filtered = new SequentFormula(pos.subTerm());
- original = pos.sequentFormula();
+ Term uAssumptions = pos.subTerm();
+ filtered = uAssumptions;
+ original = pos.sequentLevelFormula();
}
@Override
- public SequentFormula getFilteredFormula() {
+ public Term getFilteredFormula() {
return filtered;
}
@Override
- public SequentFormula getOriginalFormula() {
+ public Term getOriginalFormula() {
return original;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java
index 350d9f0d849..4b65c4f88f9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/BuiltInRuleAppIndex.java
@@ -87,13 +87,13 @@ private void scanSimplificationRule(ImmutableList rules, Goal goal,
final Node node = goal.node();
final Sequent seq = node.sequent();
- for (final SequentFormula sf : (antec ? seq.antecedent() : seq.succedent())) {
+ for (final Term sf : (antec ? seq.antecedent() : seq.succedent())) {
scanSimplificationRule(rules, goal, antec, sf, listener);
}
}
private void scanSimplificationRule(ImmutableList rules, Goal goal, boolean antec,
- SequentFormula cfma, NewRuleListener listener) {
+ Term cfma, NewRuleListener listener) {
final PosInOccurrence pos = new PosInOccurrence(cfma, PosInTerm.getTopLevel(), antec);
ImmutableList subrules = ImmutableSLList.nil();
while (!rules.isEmpty()) {
@@ -145,9 +145,9 @@ public void sequentChanged(Goal goal, SequentChangeInfo sci, NewRuleListener lis
private void scanAddedFormulas(Goal goal, boolean antec, SequentChangeInfo sci,
NewRuleListener listener) {
- ImmutableList cfmas = sci.addedFormulas(antec);
+ ImmutableList cfmas = sci.addedFormulas(antec);
while (!cfmas.isEmpty()) {
- final SequentFormula cfma = cfmas.head();
+ final Term cfma = cfmas.head();
scanSimplificationRule(index.rules(), goal, antec, cfma, listener);
cfmas = cfmas.tail();
}
@@ -160,7 +160,7 @@ private void scanModifiedFormulas(Goal goal, boolean antec, SequentChangeInfo sc
while (!fcis.isEmpty()) {
final FormulaChangeInfo fci = fcis.head();
- final SequentFormula cfma = fci.newFormula();
+ final Term cfma = fci.newFormula();
scanSimplificationRule(index.rules(), goal, antec, cfma, listener);
fcis = fcis.tail();
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/FormulaTagManager.java b/key.core/src/main/java/de/uka/ilkd/key/proof/FormulaTagManager.java
index b71df3fa24a..415d2d1869c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/FormulaTagManager.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/FormulaTagManager.java
@@ -102,7 +102,7 @@ private void updateTags(SequentChangeInfo sci, boolean p_antec, Goal p_goal) {
}
private void addTags(SequentChangeInfo sci, boolean p_antec, Goal p_goal) {
- for (SequentFormula constrainedFormula : sci.addedFormulas(p_antec)) {
+ for (Term constrainedFormula : sci.addedFormulas(p_antec)) {
final PosInOccurrence pio =
new PosInOccurrence(constrainedFormula, PosInTerm.getTopLevel(), p_antec);
createNewTag(pio, p_goal);
@@ -110,7 +110,7 @@ private void addTags(SequentChangeInfo sci, boolean p_antec, Goal p_goal) {
}
private void removeTags(SequentChangeInfo sci, boolean p_antec, Goal p_goal) {
- for (SequentFormula constrainedFormula : sci.removedFormulas(p_antec)) {
+ for (Term constrainedFormula : sci.removedFormulas(p_antec)) {
final PosInOccurrence pio =
new PosInOccurrence(constrainedFormula, PosInTerm.getTopLevel(), p_antec);
removeTag(pio);
@@ -148,7 +148,7 @@ private void createNewTags(Goal p_goal, boolean p_antec) {
final Sequent seq = p_goal.sequent();
final Semisequent ss = p_antec ? seq.antecedent() : seq.succedent();
- for (SequentFormula s : ss) {
+ for (Term s : ss) {
final PosInOccurrence pio = new PosInOccurrence(s, PosInTerm.getTopLevel(), p_antec);
createNewTag(pio, p_goal);
}
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..48e08240c3b 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
@@ -379,10 +379,10 @@ public void setSequent(SequentChangeInfo sci) {
* adds a formula to the sequent before the given position and informs the rule application
* index about this change
*
- * @param cf the SequentFormula to be added
+ * @param cf the Term to be added
* @param p PosInOccurrence encodes the position
*/
- public void addFormula(SequentFormula cf, PosInOccurrence p) {
+ public void addFormula(Term cf, PosInOccurrence p) {
setSequent(sequent().addFormula(cf, p));
}
@@ -390,12 +390,12 @@ public void addFormula(SequentFormula cf, PosInOccurrence p) {
* adds a formula to the antecedent or succedent of a sequent. Either at its front or back and
* informs the rule application index about this change
*
- * @param cf the SequentFormula to be added
- * @param inAntec boolean true(false) if SequentFormula has to be added to antecedent
+ * @param cf the Term to be added
+ * @param inAntec boolean true(false) if Term has to be added to antecedent
* (succedent)
* @param first boolean true if at the front, if false then cf is added at the back
*/
- public void addFormula(SequentFormula cf, boolean inAntec, boolean first) {
+ public void addFormula(Term cf, boolean inAntec, boolean first) {
setSequent(sequent().addFormula(cf, inAntec, first));
}
@@ -403,10 +403,10 @@ public void addFormula(SequentFormula cf, boolean inAntec, boolean first) {
* replaces a formula at the given position and informs the rule application index about this
* change
*
- * @param cf the SequentFormula replacing the old one
+ * @param cf the Term replacing the old one
* @param p the PosInOccurrence encoding the position
*/
- public void changeFormula(SequentFormula cf, PosInOccurrence p) {
+ public void changeFormula(Term cf, PosInOccurrence p) {
setSequent(sequent().changeFormula(cf, p));
}
@@ -607,10 +607,10 @@ public ImmutableList apply(final RuleApp ruleApp) {
* caught.
*/
NamespaceSet originalNamespaces = getLocalNamespaces();
- Services overlayServices = proof.getServices().getOverlay(originalNamespaces);
final ImmutableList goalList;
var time = System.nanoTime();
try {
+ Services overlayServices = proof.getServices().getOverlay(originalNamespaces);
goalList = ruleApp.execute(this, overlayServices);
} finally {
PERF_APP_EXECUTE.getAndAdd(System.nanoTime() - time);
@@ -702,12 +702,12 @@ public void makeLocalNamespacesFrom(NamespaceSet ns) {
public List getAllBuiltInRuleApps() {
final BuiltInRuleAppIndex index = ruleAppIndex().builtInRuleAppIndex();
LinkedList ruleApps = new LinkedList<>();
- for (SequentFormula sf : node().sequent().antecedent()) {
+ for (Term sf : node().sequent().antecedent()) {
ImmutableList t =
index.getBuiltInRule(this, new PosInOccurrence(sf, PosInTerm.getTopLevel(), true));
t.forEach(ruleApps::add);
}
- for (SequentFormula sf : node().sequent().succedent()) {
+ for (Term sf : node().sequent().succedent()) {
ImmutableList t =
index.getBuiltInRule(this, new PosInOccurrence(sf, PosInTerm.getTopLevel(), false));
t.forEach(ruleApps::add);
@@ -725,13 +725,13 @@ protected boolean filter(Taclet taclet) {
return true;
}
};
- for (SequentFormula sf : node().sequent().antecedent()) {
+ for (Term sf : node().sequent().antecedent()) {
ImmutableList tacletAppAtAndBelow = index.getTacletAppAtAndBelow(filter,
new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services);
tacletAppAtAndBelow.forEach(allApps::add);
}
- for (SequentFormula sf : node().sequent().succedent()) {
+ for (Term sf : node().sequent().succedent()) {
ImmutableList tacletAppAtAndBelow = index.getTacletAppAtAndBelow(filter,
new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services);
tacletAppAtAndBelow.forEach(allApps::add);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java
index 55a54a489f3..a50e7a424b1 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java
@@ -10,9 +10,9 @@
import de.uka.ilkd.key.logic.TermFactory;
import de.uka.ilkd.key.logic.op.Operator;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
import de.uka.ilkd.key.util.InfFlowSpec;
+import org.key_project.logic.SyntaxElement;
import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
@@ -36,7 +36,7 @@ public class OpReplacer {
/**
* The replacement map.
*/
- private final ReplacementMap extends SVSubstitute, ? extends SVSubstitute> map;
+ private final ReplacementMap extends SyntaxElement, ? extends SyntaxElement> map;
/**
*
@@ -53,7 +53,7 @@ public class OpReplacer {
* with
* @param tf a term factory.
*/
- public OpReplacer(Map extends SVSubstitute, ? extends SVSubstitute> map, TermFactory tf) {
+ public OpReplacer(Map extends SyntaxElement, ? extends SyntaxElement> map, TermFactory tf) {
this(map, tf, null);
}
@@ -65,12 +65,12 @@ public OpReplacer(Map extends SVSubstitute, ? extends SVSubstitute> map, TermF
* @param tf a term factory.
* @param proof the currently loaded proof
*/
- public OpReplacer(Map extends SVSubstitute, ? extends SVSubstitute> map, TermFactory tf,
+ public OpReplacer(Map extends SyntaxElement, ? extends SyntaxElement> map, TermFactory tf,
Proof proof) {
assert map != null;
this.map = map instanceof ReplacementMap
- ? (ReplacementMap extends SVSubstitute, ? extends SVSubstitute>) map
+ ? (ReplacementMap extends SyntaxElement, ? extends SyntaxElement>) map
: ReplacementMap.create(tf, proof, map);
this.tf = tf;
@@ -234,7 +234,7 @@ public Term replace(Term term) {
return newTerm;
}
- for (SVSubstitute svs : map.keySet()) {
+ for (SyntaxElement svs : map.keySet()) {
if (term.equalsModProperty(svs, TERM_LABELS_PROPERTY)) {
return (Term) map.get(svs);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
index 730707056a3..bbf6a42dad3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
@@ -144,9 +144,8 @@ public SVInstantiations replace(SVInstantiations insts) {
result = result.replace(sv, newA, services);
}
} else if (ie instanceof TermInstantiation) {
- Term t = (Term) inst;
- Term newT = replace(t);
- if (newT != t) {
+ Term newT = replace((Term) inst);
+ if (newT != inst) {
result = result.replace(sv, newT, services);
}
} else {
@@ -183,11 +182,11 @@ public SemisequentChangeInfo replace(Semisequent s) {
SemisequentChangeInfo result = new SemisequentChangeInfo();
result.setFormulaList(s.asList());
- final Iterator it = s.iterator();
+ final Iterator it = s.iterator();
for (int formulaNumber = 0; it.hasNext(); formulaNumber++) {
- final SequentFormula oldcf = it.next();
- final SequentFormula newcf = replace(oldcf);
+ final Term oldcf = it.next();
+ final Term newcf = replace(oldcf);
if (newcf != oldcf) {
result.combine(result.semisequent().replace(formulaNumber, newcf));
@@ -197,22 +196,6 @@ public SemisequentChangeInfo replace(Semisequent s) {
return result;
}
-
- /**
- * replaces in a constrained formula
- */
- public SequentFormula replace(SequentFormula cf) {
- SequentFormula result = cf;
-
- final Term newFormula = replace(cf.formula());
-
- if (newFormula != cf.formula()) {
- result = new SequentFormula(newFormula);
- }
- return result;
- }
-
-
private Term replaceProgramVariable(Term t) {
final ProgramVariable pv = (ProgramVariable) t.op();
ProgramVariable o = map.get(pv);
@@ -222,7 +205,6 @@ private Term replaceProgramVariable(Term t) {
return t;
}
-
private Term standardReplace(Term t) {
Term result = t;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
index 1fb6157a6c0..e8121005091 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
@@ -242,7 +242,7 @@ public Proof(String name, Sequent problem, String header, InitConfig initConfig,
public Proof(String name, Term problem, String header, InitConfig initConfig) {
this(name,
Sequent.createSuccSequent(
- Semisequent.EMPTY_SEMISEQUENT.insert(0, new SequentFormula(problem)).semisequent()),
+ Semisequent.EMPTY_SEMISEQUENT.insert(0, problem).semisequent()),
initConfig.createTacletIndex(), initConfig.createBuiltInRuleIndex(), initConfig);
problemHeader = header;
}
@@ -490,7 +490,6 @@ public ImmutableList openEnabledGoals() {
return filterEnabledGoals(openGoals);
}
-
/**
* filter those goals from a list which are enabled
*
@@ -509,15 +508,14 @@ private ImmutableList filterEnabledGoals(ImmutableList goals) {
return enabledGoals;
}
-
/**
* removes the given goal and adds the new goals in list
*
* @param oldGoal the old goal that has to be removed from list
- * @param newGoals the IList with the new goals that were result of a rule application on
- * goal
+ * @param newGoals the Iterable with the new goals that were result of a rule application
+ * on goal
*/
- public void replace(Goal oldGoal, ImmutableList newGoals) {
+ public void replace(Goal oldGoal, Iterable newGoals) {
openGoals = openGoals.removeAll(oldGoal);
if (closed()) {
@@ -632,6 +630,21 @@ public void add(ImmutableList goals) {
fireProofGoalsAdded(goals);
}
+ /**
+ * adds a list with new goals to the list of open goals
+ *
+ * @param goals the Iterable to be prepended
+ */
+ public void add(Iterable goals) {
+ ImmutableList addGoals;
+ if (goals instanceof ImmutableList asList) {
+ addGoals = asList;
+ } else {
+ addGoals = ImmutableList.fromList(goals);
+ }
+ add(addGoals);
+ }
+
/**
* returns true if the root node is marked as closed and all goals have been removed
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java
index 88fe0af0499..a6df47649fb 100755
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java
@@ -11,11 +11,12 @@
import de.uka.ilkd.key.logic.TermFactory;
import de.uka.ilkd.key.logic.label.OriginTermLabel;
import de.uka.ilkd.key.logic.label.TermLabelManager;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
import de.uka.ilkd.key.settings.ProofSettings;
import de.uka.ilkd.key.settings.TermLabelSettings;
import de.uka.ilkd.key.util.LinkedHashMap;
+import org.key_project.logic.SyntaxElement;
+
/**
* A map to be used in an {@link OpReplacer}. It maps operators that should be replaced to their
* replacements.
@@ -25,7 +26,7 @@
* @param the type of the elements to replace.
* @param the type of the replacements.
*/
-public interface ReplacementMap extends Map {
+public interface ReplacementMap extends Map {
/**
* Creates a new replacement map.
@@ -36,7 +37,7 @@ public interface ReplacementMap extends Map {
* @param proof the currently loaded proof, or {@code null} if no proof is loaded.
* @return a new replacement map.
*/
- static ReplacementMap create(TermFactory tf,
+ static ReplacementMap create(TermFactory tf,
Proof proof) {
var noIrrelevantTermLabelsMap = proof == null
? ProofSettings.DEFAULT_SETTINGS.getTermLabelSettings().getUseOriginLabels()
@@ -58,7 +59,7 @@ static ReplacementMap create(TermFactory tf,
* @param initialMappings a map whose mapping should be added to the new replacement map.
* @return a new replacement map.
*/
- static ReplacementMap create(TermFactory tf,
+ static ReplacementMap create(TermFactory tf,
Proof proof, Map initialMappings) {
ReplacementMap result = create(tf, proof);
result.putAll(initialMappings);
@@ -77,7 +78,7 @@ static ReplacementMap create(TermFactory tf,
* @param the type of the operators to replace.
* @param the type of the replacements.
*/
- class DefaultReplacementMap extends LinkedHashMap
+ class DefaultReplacementMap extends LinkedHashMap
implements ReplacementMap {
private static final long serialVersionUID = 6223486569442129676L;
}
@@ -98,7 +99,7 @@ class DefaultReplacementMap extends LinkedHashMap
+ class NoIrrelevantLabelsReplacementMap
implements ReplacementMap {
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/SemisequentTacletAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/SemisequentTacletAppIndex.java
index f70243418f7..4a8c236ee6b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/SemisequentTacletAppIndex.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/SemisequentTacletAppIndex.java
@@ -24,7 +24,7 @@ public class SemisequentTacletAppIndex {
public static final AtomicLong PERF_ADD = new AtomicLong();
public static final AtomicLong PERF_REMOVE = new AtomicLong();
- private ImmutableMap termIndices =
+ private ImmutableMap termIndices =
DefaultImmutableMap.nilMap();
private TermTacletAppIndexCacheSet indexCaches;
@@ -38,10 +38,10 @@ public class SemisequentTacletAppIndex {
* Add indices for the given formulas to the map termIndices
. Existing entries are
* replaced with the new indices. Note: destructive, use only when constructing new index
*/
- private void addTermIndices(ImmutableList cfmas, Services services,
+ private void addTermIndices(ImmutableList cfmas, Services services,
TacletIndex tacletIndex, NewRuleListener listener) {
while (!cfmas.isEmpty()) {
- final SequentFormula cfma = cfmas.head();
+ final Term cfma = cfmas.head();
cfmas = cfmas.tail();
addTermIndex(cfma, services, tacletIndex, listener);
}
@@ -51,7 +51,7 @@ private void addTermIndices(ImmutableList cfmas, Services servic
* Add an index for the given formula to the map termIndices
. An existing entry is
* replaced with the new one. Note: destructive, use only when constructing new index
*/
- private void addTermIndex(SequentFormula cfma, Services services,
+ private void addTermIndex(Term cfma, Services services,
TacletIndex tacletIndex, NewRuleListener listener) {
final PosInOccurrence pos = new PosInOccurrence(cfma, PosInTerm.getTopLevel(), antec);
termIndices = termIndices.put(cfma, TermTacletAppIndex.create(pos, services, tacletIndex,
@@ -63,7 +63,7 @@ private void addTermIndex(SequentFormula cfma, Services services,
* termIndices
, by adding the taclets that are selected by filter
* Note: destructive, use only when constructing new index
*/
- private void addTaclets(RuleFilter filter, SequentFormula cfma, Services services,
+ private void addTaclets(RuleFilter filter, Term cfma, Services services,
TacletIndex tacletIndex, NewRuleListener listener) {
final TermTacletAppIndex oldIndex = termIndices.get(cfma);
assert oldIndex != null : "Term index that is supposed to be updated " + "does not exist";
@@ -78,8 +78,8 @@ private void addTaclets(RuleFilter filter, SequentFormula cfma, Services service
* Remove the indices for the given formulas from the map termIndices
. Note:
* destructive, use only when constructing new index
*/
- private void removeTermIndices(ImmutableList cfmas) {
- for (SequentFormula cfma : cfmas) {
+ private void removeTermIndices(ImmutableList cfmas) {
+ for (Term cfma : cfmas) {
removeTermIndex(cfma);
}
}
@@ -88,7 +88,7 @@ private void removeTermIndices(ImmutableList cfmas) {
* Remove the index for the given formula from the map termIndices
. Note:
* destructive, use only when constructing new index
*/
- private void removeTermIndex(SequentFormula cfma) {
+ private void removeTermIndex(Term cfma) {
termIndices = termIndices.remove(cfma);
}
@@ -102,7 +102,7 @@ private List removeFormulas(ImmutableList
var oldIndices = new ArrayList(infos.size());
for (FormulaChangeInfo info : infos) {
- final SequentFormula oldFor = info.getOriginalFormula();
+ final Term oldFor = info.getOriginalFormula();
oldIndices.add(termIndices.get(oldFor));
removeTermIndex(oldFor);
@@ -125,7 +125,7 @@ private void updateTermIndices(List oldIndices,
while (infoIt.hasNext()) {
final FormulaChangeInfo info = infoIt.next();
- final SequentFormula newFor = info.newFormula();
+ final Term newFor = info.newFormula();
final TermTacletAppIndex oldIndex = oldIndexIt.next();
if (oldIndex == null)
@@ -184,7 +184,7 @@ public SemisequentTacletAppIndex copy() {
* Get term index for the formula to which position pos
points
*/
private TermTacletAppIndex getTermIndex(PosInOccurrence pos) {
- return termIndices.get(pos.sequentFormula());
+ return termIndices.get(pos.sequentLevelFormula());
}
/**
@@ -240,7 +240,7 @@ public SemisequentTacletAppIndex sequentChanged(SequentChangeInfo sci, Services
public SemisequentTacletAppIndex addTaclets(RuleFilter filter, Services services,
TacletIndex tacletIndex, NewRuleListener listener) {
final SemisequentTacletAppIndex result = copy();
- final Iterator it = termIndices.keyIterator();
+ final Iterator it = termIndices.keyIterator();
while (it.hasNext()) {
result.addTaclets(filter, it.next(), services, tacletIndex, listener);
@@ -254,8 +254,8 @@ public SemisequentTacletAppIndex addTaclets(RuleFilter filter, Services services
* taclet app.
*/
void reportRuleApps(NewRuleListener l) {
- for (final ImmutableMapEntry entry : termIndices) {
- final SequentFormula cfma = entry.key();
+ for (final ImmutableMapEntry entry : termIndices) {
+ final Term cfma = entry.key();
final TermTacletAppIndex index = entry.value();
final PosInOccurrence pio = new PosInOccurrence(cfma, PosInTerm.getTopLevel(), antec);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TermTacletAppIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TermTacletAppIndex.java
index 1af43522d9f..5b044a194db 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/TermTacletAppIndex.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TermTacletAppIndex.java
@@ -91,9 +91,9 @@ private static ImmutableList getFindTaclet(PosInOccurrence pos,
/**
- * collects all AntecedentTaclet instantiations for the given heuristics and SequentFormula
+ * collects all AntecedentTaclet instantiations for the given heuristics and Term
*
- * @param pos the PosInOccurrence of the SequentFormula the taclets have to be connected to (pos
+ * @param pos the PosInOccurrence of the Term the taclets have to be connected to (pos
* must point to the top level formula, i.e. pos.isTopLevel() must be true)
* @param services the Services object encapsulating information about the java datastructures
* like (static)types etc.
@@ -105,9 +105,9 @@ private static ImmutableList antecTaclet(PosInOccurrence pos, Ru
}
/**
- * collects all SuccedentTaclet instantiations for the given heuristics and SequentFormula
+ * collects all SuccedentTaclet instantiations for the given heuristics and Term
*
- * @param pos the PosInOccurrence of the SequentFormula the taclets have to be connected to (pos
+ * @param pos the PosInOccurrence of the Term the taclets have to be connected to (pos
* must point to the top level formula, i.e. pos.isTopLevel() must be true)
* @param services the Services object encapsulating information about the java datastructures
* like (static)types etc.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/delayedcut/DelayedCutProcessor.java b/key.core/src/main/java/de/uka/ilkd/key/proof/delayedcut/DelayedCutProcessor.java
index cd0b76007b2..ee89b1abafc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/delayedcut/DelayedCutProcessor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/delayedcut/DelayedCutProcessor.java
@@ -186,7 +186,7 @@ protected boolean filter(Taclet taclet) {
*/
private ImmutableList hide(DelayedCut cut, Goal goal) {
- SequentFormula sf = getSequentFormula(goal, cut.isDecisionPredicateInAntecendet());
+ Term sf = getTerm(goal, cut.isDecisionPredicateInAntecendet());
PosInOccurrence pio =
new PosInOccurrence(sf, PosInTerm.getTopLevel(), cut.isDecisionPredicateInAntecendet());
@@ -208,9 +208,9 @@ private int getGoalForHiding(ImmutableList goals, DelayedCut cut) {
String side = cut.isDecisionPredicateInAntecendet() ? "TRUE" : "FALSE";
if (goal[i].node().getNodeInfo().getBranchLabel().endsWith(side)) {
- SequentFormula formula =
- getSequentFormula(goal[i], cut.isDecisionPredicateInAntecendet());
- if (formula.formula() == cut.getFormula()) {
+ Term formula =
+ getTerm(goal[i], cut.isDecisionPredicateInAntecendet());
+ if (formula == cut.getFormula()) {
return i;
}
}
@@ -223,7 +223,7 @@ private String getHideTacletName(DelayedCut cut) {
return cut.isDecisionPredicateInAntecendet() ? HIDE_LEFT_TACLET : HIDE_RIGHT_TACLET;
}
- private SequentFormula getSequentFormula(Goal goal, boolean decPredInAnte) {
+ private Term getTerm(Goal goal, boolean decPredInAnte) {
return decPredInAnte ? goal.sequent().antecedent().get(DEC_PRED_INDEX)
: goal.sequent().succedent().get(DEC_PRED_INDEX);
@@ -390,7 +390,7 @@ private PosInOccurrence translate(NodeGoalPair pair, TermServices services) {
}
int formulaNumber =
pair.node.sequent().formulaNumberInSequent(oldRuleApp.posInOccurrence().isInAntec(),
- oldRuleApp.posInOccurrence().sequentFormula());
+ oldRuleApp.posInOccurrence().sequentLevelFormula());
return PosInOccurrence.findInSequent(pair.goal.sequent(), formulaNumber,
oldRuleApp.posInOccurrence().posInTerm());
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
index 4c089e3a4b5..0b2c712662f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
@@ -17,7 +17,6 @@
import de.uka.ilkd.key.ldt.HeapLDT;
import de.uka.ilkd.key.logic.Namespace;
import de.uka.ilkd.key.logic.NamespaceSet;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.label.OriginTermLabelFactory;
import de.uka.ilkd.key.logic.op.*;
@@ -377,8 +376,8 @@ private void populateNamespaces(Term term, NamespaceSet namespaces, Goal rootGoa
private void populateNamespaces(Proof proof) {
final NamespaceSet namespaces = proof.getNamespaces();
final Goal rootGoal = proof.openGoals().head();
- for (SequentFormula cf : proof.root().sequent()) {
- populateNamespaces(cf.formula(), namespaces, rootGoal);
+ for (Term cf : proof.root().sequent()) {
+ populateNamespaces(cf, namespaces, rootGoal);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
index b40ef0409c1..7992e507085 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
@@ -495,7 +495,7 @@ private TacletApp constructTacletApp(TacletAppIntermediate currInterm, Goal curr
NamespaceSet nss = currGoal.getLocalNamespaces();
Term term = parseTerm(ifFormulaStr, proof, nss.variables(), nss.programVariables(),
nss.functions());
- ifFormulaList = ifFormulaList.append(new IfFormulaInstDirect(new SequentFormula(term)));
+ ifFormulaList = ifFormulaList.append(new IfFormulaInstDirect(term));
}
if (!ourApp.ifInstsCorrectSize(ifFormulaList)) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
index 9bfd785e9e4..cf4e70129e7 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
@@ -172,8 +172,8 @@ public void save(OutputStream out) throws IOException {
strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY,
StrategyProperties.INF_FLOW_CHECK_TRUE);
strategySettings.setActiveStrategyProperties(strategyProperties);
- for (final SequentFormula s : proof.root().sequent().succedent().asList()) {
- ((InfFlowProof) proof).addLabeledTotalTerm(s.formula());
+ for (final Term s : proof.root().sequent().succedent().asList()) {
+ ((InfFlowProof) proof).addLabeledTotalTerm(s);
}
} else {
strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY,
@@ -694,7 +694,8 @@ public static String posInOccurrence2Proof(Sequent seq, PosInOccurrence pos) {
if (pos == null) {
return "";
}
- return " (formula \"" + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentFormula())
+ return " (formula \""
+ + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentLevelFormula())
+ "\")" + posInTerm2Proof(pos.posInTerm());
}
@@ -754,15 +755,16 @@ public String ifFormulaInsts(Node node, ImmutableList l)
StringBuilder s = new StringBuilder();
for (final IfFormulaInstantiation aL : l) {
if (aL instanceof IfFormulaInstSeq) {
- final SequentFormula f = aL.getConstrainedFormula();
+ final Term f = aL.getConstrainedFormula();
s.append(" (ifseqformula \"")
.append(node.sequent()
.formulaNumberInSequent(((IfFormulaInstSeq) aL).inAntec(), f))
.append("\")");
} else if (aL instanceof IfFormulaInstDirect) {
+ Term fml = aL.getConstrainedFormula();
final String directInstantiation =
- printTerm(aL.getConstrainedFormula().formula(), node.proof().getServices());
+ printTerm(fml, node.proof().getServices());
s.append(" (ifdirectformula \"").append(escapeCharacters(directInstantiation))
.append("\")");
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java b/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java
index 2568f3fe8cd..072a2aa0474 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java
@@ -7,7 +7,6 @@
import java.util.List;
import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.op.UpdateApplication;
@@ -87,8 +86,8 @@ private ProspectivePartner areProspectivePartners(Goal g1, PosInOccurrence pio,
referenceFormula.op() instanceof UpdateApplication ? referenceFormula.sub(1)
: referenceFormula;
- for (SequentFormula sf : g2.sequent().succedent()) {
- Term formula = sf.formula();
+ for (Term sf : g2.sequent().succedent()) {
+ Term formula = sf;
Term update2 = tb.skip();
if (formula.op() instanceof UpdateApplication
&& !formula.equalsModProperty(referenceFormula, RENAMING_PROPERTY)) {
@@ -98,7 +97,8 @@ private ProspectivePartner areProspectivePartners(Goal g1, PosInOccurrence pio,
}
if (formula.equalsModProperty(referenceFormula, RENAMING_PROPERTY)) {
- return new ProspectivePartner(referenceFormula, g1.node(), pio.sequentFormula(),
+ return new ProspectivePartner(referenceFormula, g1.node(),
+ pio.sequentLevelFormula(),
update1, g2.node(), sf, update2);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java b/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java
index 48bf81f8d66..8f8429f1d06 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java
@@ -115,15 +115,15 @@ private void processJoin() {
}
private void orRight(Goal goal) {
- SequentFormula sf = goal.sequent().succedent().get(0);
+ Term sf = goal.sequent().succedent().get(0);
PosInOccurrence pio = new PosInOccurrence(sf, PosInTerm.getTopLevel(), false);
apply(new String[] { OR_RIGHT_TACLET }, goal, pio);
}
- private SequentFormula findFormula(Sequent sequent, Term content, boolean antecedent) {
- for (SequentFormula sf : (antecedent ? sequent.antecedent() : sequent.succedent())) {
- if (sf.formula().equals(content)) {
+ private Term findFormula(Sequent sequent, Term content, boolean antecedent) {
+ for (Term sf : (antecedent ? sequent.antecedent() : sequent.succedent())) {
+ if (sf.equals(content)) {
return sf;
}
}
@@ -132,7 +132,7 @@ private SequentFormula findFormula(Sequent sequent, Term content, boolean antece
private Goal simplifyUpdate(Goal goal, DelayedCut cut) {
- SequentFormula sf = findFormula(goal.sequent(), cut.getFormula(), false);
+ Term sf = findFormula(goal.sequent(), cut.getFormula(), false);
PosInOccurrence pio = new PosInOccurrence(sf, PosInTerm.getTopLevel().down(0), false);
Goal result = apply(SIMPLIFY_UPDATE, goal, pio).head();
@@ -203,10 +203,12 @@ private Term createPhi() {
partner.getSequent(1).succedent(), partner.getCommonFormula());
Collection commonGamma = computeCommonFormulas(partner.getSequent(0).antecedent(),
partner.getSequent(1).antecedent(), partner.getCommonFormula());
+ Term partnerFormula = partner.getFormula(0);
Collection delta1 = computeDifference(partner.getSequent(0).succedent(), commonDelta,
- partner.getFormula(0).formula());
+ partnerFormula);
+ Term formula = partner.getFormula(1);
Collection delta2 = computeDifference(partner.getSequent(1).succedent(), commonDelta,
- partner.getFormula(1).formula());
+ formula);
Collection gamma1 =
computeDifference(partner.getSequent(0).antecedent(), commonGamma, null);
@@ -262,9 +264,9 @@ private Collection createConstrainedTerms(Collection terms, Term pre
private Collection computeCommonFormulas(Semisequent s1, Semisequent s2, Term exclude) {
TreeSet formulas1 = createTree(s1, exclude);
TreeSet result = createTree();
- for (SequentFormula sf : s2) {
- if (formulas1.contains(sf.formula())) {
- result.add(sf.formula());
+ for (Term sf : s2) {
+ if (formulas1.contains(sf)) {
+ result.add(sf);
}
}
return result;
@@ -273,9 +275,11 @@ private Collection computeCommonFormulas(Semisequent s1, Semisequent s2, T
private Collection computeDifference(Semisequent s, Collection excludeSet,
Term exclude) {
LinkedList result = new LinkedList<>();
- for (SequentFormula sf : s) {
- if (sf.formula() != exclude && !excludeSet.contains(sf.formula())) {
- result.add(sf.formula());
+ for (Term sf : s) {
+ if (sf != exclude) {
+ if (!excludeSet.contains(sf)) {
+ result.add(sf);
+ }
}
}
return result;
@@ -283,9 +287,9 @@ private Collection computeDifference(Semisequent s, Collection exclu
private TreeSet createTree(Semisequent semisequent, Term exclude) {
TreeSet set = createTree();
- for (SequentFormula sf : semisequent) {
- if (sf.formula() != exclude) {
- set.add(sf.formula());
+ for (Term sf : semisequent) {
+ if (sf != exclude) {
+ set.add(sf);
}
}
return set;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/join/LateApplicationCheck.java b/key.core/src/main/java/de/uka/ilkd/key/proof/join/LateApplicationCheck.java
index 1b9db61523b..076c8782067 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/join/LateApplicationCheck.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/join/LateApplicationCheck.java
@@ -7,7 +7,7 @@
import java.util.List;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.delayedcut.ApplicationCheck;
@@ -27,8 +27,8 @@ public List check(Node node, Node cutNode, ApplicationCheck check) {
private List check(ApplicationCheck check, Sequent sequent, Node cutNode) {
List conflicts = new LinkedList<>();
- for (SequentFormula sf : sequent) {
- String result = check.check(cutNode, sf.formula());
+ for (Term sf : sequent) {
+ String result = check.check(cutNode, sf);
if (result != null) {
conflicts.add(result);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/join/ProspectivePartner.java b/key.core/src/main/java/de/uka/ilkd/key/proof/join/ProspectivePartner.java
index f7a26bc2dce..4d54f573f9f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/join/ProspectivePartner.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/join/ProspectivePartner.java
@@ -4,7 +4,6 @@
package de.uka.ilkd.key.proof.join;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.proof.Node;
@@ -16,11 +15,11 @@
public class ProspectivePartner {
private final Term[] updates = new Term[2];
private final Term commonFormula;
- private final SequentFormula[] formula = new SequentFormula[2];
+ private final Term[] formula = new Term[2];
private final Node[] nodes = new Node[2];
private Term commonPredicate = null;
private Node commonParent = null;
- private SequentFormula formulaForHiding = null;
+ private Term formulaForHiding = null;
/**
* Constructs a new prospective partner object, i.e. a structure comprising the information
@@ -35,8 +34,8 @@ public class ProspectivePartner {
* @param formula2 The second join formula.
* @param update2 The second symbolic state.
*/
- public ProspectivePartner(Term commonFormula, Node node1, SequentFormula formula1, Term update1,
- Node node2, SequentFormula formula2, Term update2) {
+ public ProspectivePartner(Term commonFormula, Node node1, Term formula1, Term update1,
+ Node node2, Term formula2, Term update2) {
super();
this.commonFormula = commonFormula;
formula[0] = formula1;
@@ -72,15 +71,15 @@ public void setCommonParent(Node commonParent) {
if (commonParent.getAppliedRuleApp() != null
&& commonParent.getAppliedRuleApp().posInOccurrence() != null) {
setFormulaForHiding(
- commonParent.getAppliedRuleApp().posInOccurrence().sequentFormula());
+ commonParent.getAppliedRuleApp().posInOccurrence().sequentLevelFormula());
}
}
- private void setFormulaForHiding(SequentFormula formulaForHiding) {
+ private void setFormulaForHiding(Term formulaForHiding) {
this.formulaForHiding = formulaForHiding;
}
- public SequentFormula getFormulaForHiding() {
+ public Term getFormulaForHiding() {
return formulaForHiding;
}
@@ -92,7 +91,7 @@ public Sequent getSequent(int index) {
return getNode(index).sequent();
}
- public SequentFormula getFormula(int i) {
+ public Term getFormula(int i) {
return formula[i];
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
index ac8404f0b4e..ef826a9216e 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
@@ -189,7 +189,8 @@ private static Taclet getUnlimitedToLimitedTaclet(IObserverFunction limited,
// create taclet
final RewriteTacletBuilder tacletBuilder = new RewriteTacletBuilder<>();
tacletBuilder.setFind(tb.func(unlimited, subs));
- final SequentFormula cf = new SequentFormula(tb.equals(limitedTerm, unlimitedTerm));
+ Term uAssumptions = tb.equals(limitedTerm, unlimitedTerm);
+ final Term cf = uAssumptions;
final Sequent addedSeq =
Sequent.createAnteSequent(Semisequent.EMPTY_SEMISEQUENT.insertFirst(cf).semisequent());
tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(addedSeq,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/proofevent/NodeReplacement.java b/key.core/src/main/java/de/uka/ilkd/key/proof/proofevent/NodeReplacement.java
index 46f9447818b..6d1c9f0b213 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/proofevent/NodeReplacement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/proofevent/NodeReplacement.java
@@ -12,7 +12,7 @@
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.SequentChangeInfo;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.proof.Node;
import org.key_project.util.collection.ImmutableList;
@@ -55,7 +55,7 @@ private void addNodeChanges() {
}
private void addNodeChange(SequentChangeInfo p_sci) {
- Iterator it;
+ Iterator it;
Iterator it2;
// ---
@@ -72,13 +72,13 @@ private void addNodeChange(SequentChangeInfo p_sci) {
// Information about modified formulas is currently not used
it2 = p_sci.modifiedFormulas(true).iterator();
while (it2.hasNext()) {
- addRemovedChange(it2.next().positionOfModification().sequentFormula(), true);
+ addRemovedChange(it2.next().positionOfModification().sequentLevelFormula(), true);
}
// Information about modified formulas is currently not used
it2 = p_sci.modifiedFormulas(false).iterator();
while (it2.hasNext()) {
- addRemovedChange(it2.next().positionOfModification().sequentFormula(), false);
+ addRemovedChange(it2.next().positionOfModification().sequentLevelFormula(), false);
}
it = p_sci.addedFormulas(true).iterator();
@@ -119,7 +119,7 @@ private void addNodeChange(SequentChangeInfo p_sci) {
}
- private void addAddedChange(SequentFormula p_cf, boolean p_inAntec) {
+ private void addAddedChange(Term p_cf, boolean p_inAntec) {
Sequent oldS = parent.sequent();
Semisequent oldSS = (p_inAntec ? oldS.antecedent() : oldS.succedent());
Sequent newS = node.sequent();
@@ -140,7 +140,7 @@ private void addAddedChange(SequentFormula p_cf, boolean p_inAntec) {
* @param p_cf
* @param p_inAntec
*/
- private void addAddedRedundantChange(SequentFormula p_cf, boolean p_inAntec) {
+ private void addAddedRedundantChange(Term p_cf, boolean p_inAntec) {
final PosInOccurrence pio = new PosInOccurrence(p_cf, PosInTerm.getTopLevel(), p_inAntec);
addNodeChange(new NodeRedundantAddChange(pio));
@@ -149,7 +149,7 @@ private void addAddedRedundantChange(SequentFormula p_cf, boolean p_inAntec) {
- private void addRemovedChange(SequentFormula p_cf, boolean p_inAntec) {
+ private void addRemovedChange(Term p_cf, boolean p_inAntec) {
Sequent oldS = parent.sequent();
Semisequent oldSS = (p_inAntec ? oldS.antecedent() : oldS.succedent());
@@ -165,7 +165,7 @@ private void addNodeChange(NodeChange p_nc) {
changes = changes.prepend(p_nc);
}
- private void removeNodeChanges(SequentFormula p_cf, boolean p_inAntec) {
+ private void removeNodeChanges(Term p_cf, boolean p_inAntec) {
Iterator it = changes.iterator();
changes = ImmutableSLList.nil();
NodeChange oldNC;
@@ -176,7 +176,7 @@ private void removeNodeChanges(SequentFormula p_cf, boolean p_inAntec) {
if (oldNC instanceof NodeChangeARFormula) {
oldPio = oldNC.getPos();
- if (oldPio.isInAntec() == p_inAntec && oldPio.sequentFormula().equals(p_cf)) {
+ if (oldPio.isInAntec() == p_inAntec && oldPio.sequentLevelFormula().equals(p_cf)) {
continue;
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java
index 48538a003f3..278b897a38b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java
@@ -14,8 +14,8 @@
import de.uka.ilkd.key.logic.PosInTerm;
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
@@ -304,10 +304,10 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
if (oldFormulaPioSpec.second) {
ifFormulaList = ifFormulaList.append(
new IfFormulaInstSeq(currGoal.sequent(), oldFormulaPio.isInAntec(),
- newPio.sequentFormula()));
+ newPio.sequentLevelFormula()));
} else {
ifFormulaList = ifFormulaList.append(
- new IfFormulaInstDirect(newPio.sequentFormula()));
+ new IfFormulaInstDirect(newPio.sequentLevelFormula()));
}
}
@@ -333,11 +333,12 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
* @return the formula in the sequent, or null if not found
*/
private PosInOccurrence findInNewSequent(PosInOccurrence oldPos, Sequent newSequent) {
- SequentFormula oldFormula = oldPos.sequentFormula();
+ Term oldFormula = oldPos.sequentLevelFormula();
Semisequent semiSeq = oldPos.isInAntec() ? newSequent.antecedent()
: newSequent.succedent();
- for (SequentFormula newFormula : semiSeq.asList()) {
- if (newFormula.equalsModProofIrrelevancy(oldFormula)) {
+ for (Term newFormula : semiSeq.asList()) {
+ if (newFormula.equalsModProperty(oldFormula,
+ ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY)) {
return oldPos.replaceConstrainedFormula(newFormula);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java
index 05b6f74d9dd..5d69be261c3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java
@@ -267,9 +267,9 @@ private ProofTreeListener prepareStrategy(Proof proof, ImmutableList goals
ProofTreeListener treeListener = new ProofTreeAdapter() {
@Override
public void proofGoalsAdded(ProofTreeEvent e) {
- ImmutableList newGoals = e.getGoals();
+ Iterable newGoals = e.getGoals();
// Check for a closed goal ...
- if (newGoals.size() == 0) {
+ if (!newGoals.iterator().hasNext()) {
// No new goals have been generated ...
closedGoals++;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
index dfae6550d37..8e118b9ebd3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
@@ -24,7 +24,6 @@
import de.uka.ilkd.key.java.statement.JavaStatement;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.ProgramElementName;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.TermServices;
@@ -294,7 +293,7 @@ protected static Term buildInfFlowPostAssumption(ProofObligationVars instVars,
return afterAssumptions;
}
- static SequentFormula buildBodyPreservesSequent(InfFlowPOSnippetFactory f, InfFlowProof proof) {
+ static Term buildBodyPreservesSequent(InfFlowPOSnippetFactory f, InfFlowProof proof) {
Term selfComposedExec =
f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_BLOCK_WITH_PRE_RELATION);
Term post = f.create(InfFlowPOSnippetFactory.Snippet.INF_FLOW_INPUT_OUTPUT_RELATION);
@@ -304,7 +303,7 @@ static SequentFormula buildBodyPreservesSequent(InfFlowPOSnippetFactory f, InfFl
tb.imp(tb.label(selfComposedExec, ParameterlessTermLabel.SELF_COMPOSITION_LABEL), post);
proof.addLabeledIFSymbol(selfComposedExec);
- return new SequentFormula(finalTerm);
+ return finalTerm;
}
private static ProofObligationVars generateProofObligationVariables(
@@ -347,7 +346,7 @@ private static void addProofObligation(final Goal infFlowGoal, final InfFlowProo
InfFlowPOSnippetFactory infFlowFactory =
POSnippetFactory.getInfFlowFactory(contract, ifVars.c1, ifVars.c2, ec, services);
- final SequentFormula poFormula = buildBodyPreservesSequent(infFlowFactory, proof);
+ final Term poFormula = buildBodyPreservesSequent(infFlowFactory, proof);
// add proof obligation to goal
infFlowGoal.addFormula(poFormula, false, true);
@@ -399,7 +398,7 @@ protected void setUpInfFlowPartOfUsageGoal(final Goal usageGoal,
tb.applySequential(new Term[] { contextUpdate, remembranceUpdate },
tb.and(infFlowValitidyData.preAssumption,
tb.apply(anonymisationUpdate, infFlowValitidyData.postAssumption)));
- usageGoal.addFormula(new SequentFormula(uAssumptions), true, false);
+ usageGoal.addFormula(uAssumptions, true, false);
}
protected InfFlowValidityData setUpInfFlowValidityGoal(final Goal infFlowGoal,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java
index cc0f21552f8..7b58514ee7b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java
@@ -9,6 +9,7 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.PosInOccurrence;
+import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty;
import de.uka.ilkd.key.logic.op.LocationVariable;
import de.uka.ilkd.key.proof.Goal;
@@ -55,7 +56,7 @@ public BuiltInRule rule() {
}
/**
- * returns the PositionInOccurrence (representing a SequentFormula and a position in the
+ * returns the PositionInOccurrence (representing a Term and a position in the
* corresponding formula) of this rule application
*/
@Override
@@ -171,7 +172,8 @@ public boolean equalsModProofIrrelevancy(Object obj) {
@Override
public int hashCodeModProofIrrelevancy() {
return Objects.hash(rule(), getHeapContext(),
- posInOccurrence().sequentFormula().hashCodeModProofIrrelevancy(),
+ ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY
+ .hashCodeModThisProperty(posInOccurrence().sequentLevelFormula()),
posInOccurrence().posInTerm());
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java
index 4991bac41dc..4edccc048ef 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java
@@ -1355,7 +1355,7 @@ public Term setUpWdGoal(final Goal goal, final BlockContract contract, final Ter
services.getSpecificationRepository().addWdStatement(bwd);
final LocationVariable heapAtPre = variables.remembranceHeaps.get(heap);
final Term anon = anonHeap != null ? services.getTermBuilder().func(anonHeap) : null;
- final SequentFormula wdBlock = bwd.generateSequent(variables.self, variables.exception,
+ final Term wdBlock = bwd.generateSequent(variables.self, variables.exception,
variables.result, heap, heapAtPre, anon, localIns, update, anonUpdate, services);
if (goal != null) {
@@ -1363,7 +1363,7 @@ public Term setUpWdGoal(final Goal goal, final BlockContract contract, final Ter
goal.changeFormula(wdBlock, occurrence);
}
- return wdBlock.formula();
+ return wdBlock;
}
/**
@@ -1394,8 +1394,9 @@ public Term setUpValidityGoal(final Goal goal, final Term[] updates,
Term term;
if (goal != null) {
+ Term uAssumptions = tb.applySequential(updates, tb.and(assumptions));
goal.addFormula(
- new SequentFormula(tb.applySequential(updates, tb.and(assumptions))), true,
+ uAssumptions, true,
false);
ImmutableArray labels = TermLabelManager.instantiateLabels(
@@ -1408,7 +1409,7 @@ public Term setUpValidityGoal(final Goal goal, final Term[] updates,
term = tb.applySequential(updates,
tb.prog(instantiation.modality().kind(), newJavaBlock, newPost, labels));
- goal.changeFormula(new SequentFormula(term), occurrence);
+ goal.changeFormula(term, occurrence);
TermLabelManager.refactorGoal(termLabelState, services, occurrence,
application.rule(), goal, null, null);
addInfFlow(goal);
@@ -1512,7 +1513,7 @@ public Term setUpLoopValidityGoal(final Goal goal, final LoopContract contract,
if (goal != null) {
goal.setBranchLabel("Validity");
addInfFlow(goal);
- goal.changeFormula(new SequentFormula(term), occurrence);
+ goal.changeFormula(term, occurrence);
}
return term;
}
@@ -1532,7 +1533,7 @@ public void setUpPreconditionGoal(final Goal goal, final Term update,
fullPrecondition =
TermLabelManager.refactorTerm(termLabelState, services, null, fullPrecondition,
rule, goal, BlockContractInternalRule.FULL_PRECONDITION_TERM_HINT, null);
- goal.changeFormula(new SequentFormula(fullPrecondition), occurrence);
+ goal.changeFormula(fullPrecondition, occurrence);
TermLabelManager.refactorGoal(termLabelState, services, occurrence, application.rule(),
goal, null, null);
}
@@ -1549,9 +1550,10 @@ public void setUpUsageGoal(final Goal goal, final Term[] updates,
final TermBuilder tb = services.getTermBuilder();
goal.setBranchLabel("Usage");
Term uAssumptions = tb.applySequential(updates, tb.and(assumptions));
- goal.addFormula(new SequentFormula(uAssumptions), true, false);
+ goal.addFormula(uAssumptions, true, false);
+ Term uAssumptions1 = tb.applySequential(updates, buildUsageFormula(goal));
goal.changeFormula(
- new SequentFormula(tb.applySequential(updates, buildUsageFormula(goal))),
+ uAssumptions1,
occurrence);
TermLabelManager.refactorGoal(termLabelState, services, occurrence, application.rule(),
goal, null, null);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java
index 50f3a0ec633..5b57624c749 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java
@@ -10,7 +10,6 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.TermServices;
@@ -355,7 +354,8 @@ private void setUpValidityGoal(final ImmutableList result, final boolean i
updates[1], updates[2], tb);
} else {
// nothing to prove -> set up trivial goal
- validityGoal.addFormula(new SequentFormula(tb.tt()), false, true);
+ Term uAssumptions = tb.tt();
+ validityGoal.addFormula(uAssumptions, false, true);
}
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/BoundUniquenessChecker.java b/key.core/src/main/java/de/uka/ilkd/key/rule/BoundUniquenessChecker.java
index 5b20688062a..d25d73c54c2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/BoundUniquenessChecker.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/BoundUniquenessChecker.java
@@ -7,7 +7,6 @@
import java.util.LinkedHashSet;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
@@ -52,8 +51,8 @@ public void addTerm(Term term) {
* @param seq the Sequent with the formulas to add
*/
public void addAll(Sequent seq) {
- for (final SequentFormula cf : seq) {
- terms = terms.prepend(cf.formula());
+ for (final Term cf : seq) {
+ terms = terms.prepend(cf);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstDirect.java b/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstDirect.java
index 710c9da1949..dc9fcca4607 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstDirect.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstDirect.java
@@ -4,7 +4,7 @@
package de.uka.ilkd.key.rule;
import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.proof.io.ProofSaver;
@@ -17,16 +17,16 @@ public class IfFormulaInstDirect implements IfFormulaInstantiation {
/**
* Simply the formula
*/
- private final SequentFormula cf;
+ private final Term cf;
- public IfFormulaInstDirect(SequentFormula p_cf) {
+ public IfFormulaInstDirect(Term p_cf) {
cf = p_cf;
}
/**
* @return the cf this is pointing to
*/
- public SequentFormula getConstrainedFormula() {
+ public Term getConstrainedFormula() {
return cf;
}
@@ -48,6 +48,6 @@ public int hashCode() {
}
public String toString(Services services) {
- return ProofSaver.printAnything(cf.formula(), services);
+ return ProofSaver.printAnything(cf, services);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstSeq.java b/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstSeq.java
index d70b9e1a529..c082aa270b2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstSeq.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstSeq.java
@@ -4,11 +4,7 @@
package de.uka.ilkd.key.rule;
import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.PosInTerm;
-import de.uka.ilkd.key.logic.Semisequent;
-import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.proof.io.OutputStreamProofSaver;
import org.key_project.util.collection.ImmutableArray;
@@ -25,9 +21,9 @@ public class IfFormulaInstSeq implements IfFormulaInstantiation {
*/
private final Sequent seq;
private final boolean antec; // formula is in antecedent?
- private final SequentFormula cf;
+ private final Term cf;
- public IfFormulaInstSeq(Sequent p_seq, boolean antec, SequentFormula p_cf) {
+ public IfFormulaInstSeq(Sequent p_seq, boolean antec, Term p_cf) {
seq = p_seq;
this.antec = antec;
cf = p_cf;
@@ -43,7 +39,7 @@ public IfFormulaInstSeq(Sequent seq, int formulaNr) {
* @return the cf this is pointing to
*/
@Override
- public SequentFormula getConstrainedFormula() {
+ public Term getConstrainedFormula() {
return cf;
}
@@ -93,7 +89,7 @@ public String toString() {
@Override
public String toString(Services services) {
- return OutputStreamProofSaver.printAnything(cf.formula(), services);
+ return OutputStreamProofSaver.printAnything(cf, services);
}
@Override
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java
index 9abb3fc3b5a..a7ab7433c88 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiation.java
@@ -4,7 +4,8 @@
package de.uka.ilkd.key.rule;
import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.SequentFormula;
+import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty;
import org.key_project.util.EqualsModProofIrrelevancy;
@@ -18,7 +19,7 @@ public interface IfFormulaInstantiation extends EqualsModProofIrrelevancy {
/**
* @return the cf this is pointing to
*/
- SequentFormula getConstrainedFormula();
+ Term getConstrainedFormula();
String toString(Services services);
@@ -27,11 +28,13 @@ default boolean equalsModProofIrrelevancy(Object obj) {
if (!(obj instanceof IfFormulaInstantiation that)) {
return false;
}
- return getConstrainedFormula().equalsModProofIrrelevancy(that.getConstrainedFormula());
+ return getConstrainedFormula().equalsModProperty(that.getConstrainedFormula(),
+ ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY);
}
@Override
default int hashCodeModProofIrrelevancy() {
- return getConstrainedFormula().hashCodeModProofIrrelevancy();
+ return getConstrainedFormula()
+ .hashCodeModProperty(ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java
index 87b9131b154..b3f641c0a87 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java
@@ -158,7 +158,8 @@ public IBuiltInRuleApp createApp(PosInOccurrence occurrence, TermServices servic
private void setUpValidityRule(Goal goal, PosInOccurrence occurrence, Term update,
Term condition, TermBuilder tb) {
goal.setBranchLabel("Validity");
- goal.changeFormula(new SequentFormula(tb.apply(update, condition)), occurrence);
+ Term uAssumptions = tb.apply(update, condition);
+ goal.changeFormula(uAssumptions, occurrence);
}
private void setUpUsageGoal(Goal goal, PosInOccurrence occurrence, Term update, Term target,
@@ -169,7 +170,7 @@ private void setUpUsageGoal(Goal goal, PosInOccurrence occurrence, Term update,
tb.imp(condition,
tb.prog(((Modality) target.op()).kind(), javaBlock, target.sub(0), null)));
- goal.changeFormula(new SequentFormula(newTerm), occurrence);
+ goal.changeFormula(newTerm, occurrence);
}
@Override
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java
index c2ed88a8cde..728bb34a756 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java
@@ -9,7 +9,6 @@
import de.uka.ilkd.key.java.visitor.ProgramElementReplacer;
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.TermServices;
@@ -96,9 +95,9 @@ public class LoopApplyHeadRule implements BuiltInRule {
}
Goal result = goal.split(1).head();
+ Term uAssumptions = tb.apply(update, tb.prog(modality.kind(), newJavaBlock, target.sub(0)));
result.changeFormula(
- new SequentFormula(
- tb.apply(update, tb.prog(modality.kind(), newJavaBlock, target.sub(0)))),
+ uAssumptions,
ruleApp.pio);
return ImmutableSLList.nil().append(goal);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java
index 3ae2aaed6cb..1e35409edc0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java
@@ -21,7 +21,6 @@
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.ProgramPrefix;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.label.ParameterlessTermLabel;
@@ -240,9 +239,9 @@ private void constructPresrvAndUCGoal(Services services, RuleApp ruleApp, Goal p
uBeforeLoopDefAnonVariant, invTerm);
presrvAndUCGoal.setBranchLabel("Invariant Preserved and Used");
- presrvAndUCGoal.addFormula(new SequentFormula(uAnonInv), true, false);
- presrvAndUCGoal.addFormula(new SequentFormula(wellFormedAnon), true, false);
- presrvAndUCGoal.changeFormula(new SequentFormula(newFormula), ruleApp.posInOccurrence());
+ presrvAndUCGoal.addFormula(uAnonInv, true, false);
+ presrvAndUCGoal.addFormula(wellFormedAnon, true, false);
+ presrvAndUCGoal.changeFormula(newFormula, ruleApp.posInOccurrence());
}
// -------------------------------------------------------------------------
@@ -323,7 +322,7 @@ private ProgramElement newProgram(Services services, final While loop,
}
/**
- * Creates the {@link SequentFormula} for the "initially valid" goal.
+ * Creates the {@link Term} for the "initially valid" goal.
*
* @param termLabelState The {@link TermLabelState}.
* @param inst The {@link Instantiation} for this rule application.
@@ -331,9 +330,9 @@ private ProgramElement newProgram(Services services, final While loop,
* @param reachableState The reachable state formula.
* @param services The {@link Services} object.
* @param initGoal The goal containing the "initially valid" PO.
- * @return The {@link SequentFormula} for the "initially valid" goal.
+ * @return The {@link Term} for the "initially valid" goal.
*/
- private SequentFormula initFormula(TermLabelState termLabelState, Instantiation inst,
+ private Term initFormula(TermLabelState termLabelState, Instantiation inst,
final Term invTerm, Term reachableState, Services services, Goal initGoal) {
final TermBuilder tb = services.getTermBuilder();
@@ -341,7 +340,7 @@ private SequentFormula initFormula(TermLabelState termLabelState, Instantiation
sfTerm = TermLabelManager.refactorTerm(termLabelState, services, null, sfTerm, this,
initGoal, INITIAL_INVARIANT_ONLY_HINT, null);
- return new SequentFormula(sfTerm);
+ return sfTerm;
}
/**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java
index 2b6434e380e..df86c6ca0c0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java
@@ -282,7 +282,7 @@ protected ImmutableSet contextVars(SchemaVariable sv) {
/**
- * returns the PositionInOccurrence (representing a SequentFormula and a position in the
+ * returns the PositionInOccurrence (representing a Term and a position in the
* corresponding formula)
*
* @return the PosInOccurrence
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java
index 000bd93dc5f..e48fde9cd4d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java
@@ -18,7 +18,6 @@
import de.uka.ilkd.key.java.reference.TypeReference;
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermBuilder;
import de.uka.ilkd.key.logic.TermServices;
@@ -194,8 +193,9 @@ private ImmutableList applyForModelFields(Goal goal, ModelFieldInstantiati
// ---- create "Null Reference" branch
if (nullGoal != null) {
final Term actualSelfNotNull = tb.not(tb.equals(inst.receiver, tb.NULL()));
+ Term uAssumptions = tb.apply(inst.update, actualSelfNotNull, null);
nullGoal.changeFormula(
- new SequentFormula(tb.apply(inst.update, actualSelfNotNull, null)),
+ uAssumptions,
ruleApp.posInOccurrence());
}
@@ -216,7 +216,7 @@ private ImmutableList applyForModelFields(Goal goal, ModelFieldInstantiati
Term update = tb.elementary(lhs,
makeCall(services, inst.observerSymbol, inst.receiver, ImmutableList.of()));
Term normalPost = tb.apply(update, modalityTerm);
- contGoal.changeFormula(new SequentFormula(tb.apply(inst.update, normalPost, null)),
+ contGoal.changeFormula(tb.apply(inst.update, normalPost, null),
ruleApp.posInOccurrence());
TermLabelManager.refactorGoal(termLabelState, services, ruleApp.posInOccurrence(), this,
@@ -256,7 +256,8 @@ private ImmutableList applyForMethods(Goal goal, Instantiation inst, Servi
// ---- create "Null Reference" branch
if (nullGoal != null) {
final Term actualSelfNotNull = tb.not(tb.equals(inst.actualSelf, tb.NULL()));
- nullGoal.changeFormula(new SequentFormula(tb.apply(inst.u, actualSelfNotNull, null)),
+ Term uAssumptions = tb.apply(inst.u, actualSelfNotNull, null);
+ nullGoal.changeFormula(uAssumptions,
ruleApp.posInOccurrence());
}
@@ -274,7 +275,7 @@ private ImmutableList applyForMethods(Goal goal, Instantiation inst, Servi
Term update =
tb.elementary(lhs, makeCall(services, inst.pm, inst.actualSelf, inst.actualParams));
Term normalPost = tb.apply(update, modalityTerm);
- contGoal.changeFormula(new SequentFormula(tb.apply(inst.u, normalPost, null)),
+ contGoal.changeFormula(tb.apply(inst.u, normalPost, null),
ruleApp.posInOccurrence());
TermLabelManager.refactorGoal(termLabelState, services, ruleApp.posInOccurrence(), this,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java
index feec9a03cae..19d726d810b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java
@@ -15,7 +15,6 @@
import de.uka.ilkd.key.logic.PosInTerm;
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.TermServices;
import de.uka.ilkd.key.logic.label.TermLabel;
@@ -83,7 +82,7 @@ public static final class Protocol extends ArrayList {
.append("update_apply").append("update_join").append("elimQuantifier");
private static final boolean[] bottomUp = { false, false, true, true, true, false };
- private final Map applicabilityCache =
+ private final Map applicabilityCache =
new LRUCache<>(APPLICABILITY_CACHE_SIZE);
private Proof lastProof;
@@ -241,7 +240,7 @@ public boolean isShutdown() {
*
* @param protocol
*/
- private SequentFormula simplifyPos(Goal goal, Services services, PosInOccurrence pos,
+ private Term simplifyPos(Goal goal, Services services, PosInOccurrence pos,
int indexNr, Protocol protocol) {
final ImmutableList apps =
indices[indexNr].getRewriteTaclet(pos, TacletFilter.TRUE, services);
@@ -257,13 +256,13 @@ private SequentFormula simplifyPos(Goal goal, Services services, PosInOccurrence
}
}
RewriteTaclet taclet = (RewriteTaclet) app.rule();
- SequentFormula result =
+ Term result =
taclet.getRewriteResult(goal, new TermLabelState(), services, app);
if (protocol != null) {
protocol.add(app);
}
return result;
- // TODO Idea: return new Pair(null, null);
+ // TODO Idea: return new Pair(null, null);
}
return null;
}
@@ -275,10 +274,10 @@ private SequentFormula simplifyPos(Goal goal, Services services, PosInOccurrence
*
* @param protocol
*/
- private SequentFormula simplifySub(Goal goal, Services services, PosInOccurrence pos,
+ private Term simplifySub(Goal goal, Services services, PosInOccurrence pos,
int indexNr, Protocol protocol) {
for (int i = 0, n = pos.subTerm().arity(); i < n; i++) {
- SequentFormula result =
+ Term result =
simplifyPosOrSub(goal, services, pos.down(i), indexNr, protocol);
if (result != null) {
return result;
@@ -294,14 +293,14 @@ private SequentFormula simplifySub(Goal goal, Services services, PosInOccurrence
*
* @param protocol
*/
- private SequentFormula simplifyPosOrSub(Goal goal, Services services, PosInOccurrence pos,
+ private Term simplifyPosOrSub(Goal goal, Services services, PosInOccurrence pos,
int indexNr, Protocol protocol) {
final Term term = pos.subTerm();
if (notSimplifiableCaches[indexNr].get(term) != null) {
return null;
}
- SequentFormula result;
+ Term result;
if (bottomUp[indexNr]) {
result = simplifySub(goal, services, pos, indexNr, protocol);
if (result == null) {
@@ -376,20 +375,20 @@ private Term replaceKnownHelper(Map map, Te
* (hardcoded here). The context formulas available for replace-known are passed in as
* "context". The positions of the actually used context formulas are passed out as "ifInsts".
*/
- private SequentFormula replaceKnown(Services services, SequentFormula cf, boolean inAntecedent,
+ private Term replaceKnown(Services services, Term cf, boolean inAntecedent,
Map context,
/* out */ List ifInsts, Protocol protocol, Goal goal,
RuleApp ruleApp) {
if (context == null) {
return null;
}
- final Term formula = cf.formula();
+ final Term formula = cf;
final Term simplifiedFormula = replaceKnownHelper(context, formula, inAntecedent, ifInsts,
protocol, services, goal, ruleApp);
if (simplifiedFormula.equals(formula)) {
return null;
} else {
- return new SequentFormula(simplifiedFormula);
+ return simplifiedFormula;
}
}
@@ -406,18 +405,18 @@ private RuleApp makeReplaceKnownTacletApp(Term formula, boolean inAntecedent,
SVInstantiations svi = SVInstantiations.EMPTY_SVINSTANTIATIONS;
FormulaSV sv = SchemaVariableFactory.createFormulaSV(new Name("b"));
- svi.add(sv, pio.sequentFormula().formula(), lastProof.getServices());
+ svi.add(sv, pio.sequentLevelFormula(), lastProof.getServices());
PosInOccurrence applicatinPIO =
- new PosInOccurrence(new SequentFormula(formula), PosInTerm.getTopLevel(), // TODO: This
- // should be
- // the precise
- // sub term
+ new PosInOccurrence(formula, PosInTerm.getTopLevel(), // TODO: This
+ // should be
+ // the precise
+ // sub term
inAntecedent); // It is required to create a new PosInOccurrence because formula and
// pio.constrainedFormula().formula() are only equals module
// renamings and term labels
ImmutableList ifInst = ImmutableSLList.nil();
- ifInst = ifInst.append(new IfFormulaInstDirect(pio.sequentFormula()));
+ ifInst = ifInst.append(new IfFormulaInstDirect(pio.sequentLevelFormula()));
TacletApp ta = PosTacletApp.createPosTacletApp(taclet, svi, ifInst, applicatinPIO,
lastProof.getServices());
return ta;
@@ -429,11 +428,11 @@ private RuleApp makeReplaceKnownTacletApp(Term formula, boolean inAntecedent,
*
* @param protocol
*/
- private SequentFormula simplifyConstrainedFormula(Services services, SequentFormula cf,
+ private Term simplifyConstrainedFormula(Services services, Term cf,
boolean inAntecedent, Map context,
/* out */ List ifInsts, Protocol protocol, Goal goal,
RuleApp ruleApp) {
- SequentFormula result =
+ Term result =
replaceKnown(services, cf, inAntecedent, context, ifInsts, protocol, goal, ruleApp);
if (result != null) {
return result;
@@ -461,24 +460,28 @@ private Instantiation computeInstantiation(Services services, PosInOccurrence os
// collect context formulas (potential if-insts for replace-known)
final Map context =
new LinkedHashMap<>();
- final SequentFormula cf = ossPIO.sequentFormula();
- for (SequentFormula ante : seq.antecedent()) {
- if (!ante.equals(cf) && ante.formula().op() != Junctor.TRUE) {
- context.put(new TermReplacementKey(ante.formula()),
- new PosInOccurrence(ante, PosInTerm.getTopLevel(), true));
+ final Term cf = ossPIO.sequentLevelFormula();
+ for (Term ante : seq.antecedent()) {
+ if (!ante.equals(cf)) {
+ if (ante.op() != Junctor.TRUE) {
+ context.put(new TermReplacementKey(ante),
+ new PosInOccurrence(ante, PosInTerm.getTopLevel(), true));
+ }
}
}
- for (SequentFormula succ : seq.succedent()) {
- if (!succ.equals(cf) && succ.formula().op() != Junctor.FALSE) {
- context.put(new TermReplacementKey(succ.formula()),
- new PosInOccurrence(succ, PosInTerm.getTopLevel(), false));
+ for (Term succ : seq.succedent()) {
+ if (!succ.equals(cf)) {
+ if (succ.op() != Junctor.FALSE) {
+ context.put(new TermReplacementKey(succ),
+ new PosInOccurrence(succ, PosInTerm.getTopLevel(), false));
+ }
}
}
final List ifInsts = new ArrayList<>(seq.size());
// simplify as long as possible
- ImmutableList list = ImmutableSLList.nil();
- SequentFormula simplifiedCf = cf;
+ ImmutableList list = ImmutableSLList.nil();
+ Term simplifiedCf = cf;
while (true) {
simplifiedCf = simplifyConstrainedFormula(services, simplifiedCf, ossPIO.isInAntec(),
context, ifInsts, protocol, goal, ruleApp);
@@ -500,14 +503,14 @@ private Instantiation computeInstantiation(Services services, PosInOccurrence os
/**
* Tells whether the passed formula can be simplified
*/
- private synchronized boolean applicableTo(Services services, SequentFormula cf,
+ private synchronized boolean applicableTo(Services services, Term cf,
boolean inAntecedent, Goal goal, RuleApp ruleApp) {
final Boolean b = applicabilityCache.get(cf);
if (b != null) {
return b;
} else {
// try one simplification step without replace-known
- final SequentFormula simplifiedCf = simplifyConstrainedFormula(services, cf,
+ final Term simplifiedCf = simplifyConstrainedFormula(services, cf,
inAntecedent, null, null, null, goal, ruleApp);
final boolean result = simplifiedCf != null && !simplifiedCf.equals(cf);
applicabilityCache.put(cf, result);
@@ -572,7 +575,8 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
}
// applicable to the formula?
- return applicableTo(goal.proof().getServices(), pio.sequentFormula(), pio.isInAntec(), goal,
+ return applicableTo(goal.proof().getServices(), pio.sequentLevelFormula(), pio.isInAntec(),
+ goal,
null);
}
@@ -594,21 +598,21 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
if (((OneStepSimplifierRuleApp) ruleApp).shouldRestrictAssumeInsts()
&& !disableOSSRestriction) {
ImmutableList ifInsts = ((OneStepSimplifierRuleApp) ruleApp).ifInsts();
- ImmutableList anteFormulas = ImmutableSLList.nil();
- ImmutableList succFormulas = ImmutableSLList.nil();
+ ImmutableList anteFormulas = ImmutableSLList.nil();
+ ImmutableList succFormulas = ImmutableSLList.nil();
if (ifInsts != null) {
for (PosInOccurrence it : ifInsts) {
if (it.isInAntec()) {
- anteFormulas = anteFormulas.prepend(it.sequentFormula());
+ anteFormulas = anteFormulas.prepend(it.sequentLevelFormula());
} else {
- succFormulas = succFormulas.prepend(it.sequentFormula());
+ succFormulas = succFormulas.prepend(it.sequentLevelFormula());
}
}
}
if (pos.isInAntec()) {
- anteFormulas = anteFormulas.prepend(pos.sequentFormula());
+ anteFormulas = anteFormulas.prepend(pos.sequentLevelFormula());
} else {
- succFormulas = succFormulas.prepend(pos.sequentFormula());
+ succFormulas = succFormulas.prepend(pos.sequentLevelFormula());
}
Semisequent antecedent = anteFormulas.isEmpty() ? Semisequent.EMPTY_SEMISEQUENT
: new Semisequent(anteFormulas);
@@ -673,11 +677,11 @@ public Set getCapturedTaclets() {
// -------------------------------------------------------------------------
private static final class Instantiation {
- private final SequentFormula cf;
+ private final Term cf;
private final int numAppliedRules;
private final ImmutableList ifInsts;
- public Instantiation(SequentFormula cf, int numAppliedRules,
+ public Instantiation(Term cf, int numAppliedRules,
ImmutableList ifInsts) {
assert numAppliedRules >= 0;
this.cf = cf;
@@ -685,7 +689,7 @@ public Instantiation(SequentFormula cf, int numAppliedRules,
this.ifInsts = ifInsts;
}
- public SequentFormula getCf() {
+ public Term getCf() {
return cf;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java
index 6c5d92442ad..0baf6550866 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java
@@ -10,6 +10,7 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
@@ -277,7 +278,7 @@ public boolean complete() {
}
/**
- * returns the PositionInOccurrence (representing a SequentFormula and a position in the
+ * returns the PositionInOccurrence (representing a Term and a position in the
* corresponding formula)
*
* @return the PosInOccurrence
@@ -319,7 +320,8 @@ public boolean equalsModProofIrrelevancy(Object o) {
@Override
public int hashCodeModProofIrrelevancy() {
return Objects.hash(super.hashCodeModProofIrrelevancy(),
- pos.sequentFormula().hashCodeModProofIrrelevancy(),
+ ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY
+ .hashCodeModThisProperty(pos.sequentLevelFormula()),
pos.posInTerm());
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java
index 492c155c269..3ffe39389eb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java
@@ -88,7 +88,7 @@ public class QueryExpand implements BuiltInRule {
tb.addRuleSet(new RuleSet(new Name("concrete")));
// move the query call directly to the succedent. Use box instead of diamond?
- g.addFormula(new SequentFormula(queryEval.first), true, true);
+ g.addFormula(queryEval.first, true, true);
g.addTaclet(tb.getTaclet(), SVInstantiations.EMPTY_SVINSTANTIATIONS, true);
return newGoal;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java
index 6e506a3f31b..696e7405cf2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java
@@ -258,7 +258,7 @@ public RewriteTacletExecutor extends RewriteTaclet> getExecutor() {
return (RewriteTacletExecutor extends RewriteTaclet>) executor;
}
- public SequentFormula getRewriteResult(Goal goal, TermLabelState termLabelState,
+ public Term getRewriteResult(Goal goal, TermLabelState termLabelState,
Services services, TacletApp app) {
return getExecutor().getRewriteResult(goal, termLabelState, services, app);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java
index af71ed4c8ec..09f069deb69 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java
@@ -39,5 +39,7 @@ ImmutableList apply(Goal goal, Services services, RuleApp ruleApp)
/**
* returns the display name of the rule
*/
- String displayName();
+ default String displayName() {
+ return name().toString();
+ }
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAbortException.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAbortException.java
index 96e67cb4ea9..e10f101bd10 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAbortException.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAbortException.java
@@ -10,9 +10,7 @@
* This Exception signals the abort of a rule Application
*
*/
-
-
-public class RuleAbortException extends Exception {
+public class RuleAbortException extends RuntimeException {
private static final long serialVersionUID = -645034125571021135L;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java
index 8c505c74360..c55bd34bd9a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java
@@ -23,7 +23,7 @@ public interface RuleApp extends EqualsModProofIrrelevancy {
Rule rule();
/**
- * returns the PositionInOccurrence (representing a SequentFormula and a position in the
+ * returns the PositionInOccurrence (representing a Term and a position in the
* corresponding formula) of this rule application
*/
PosInOccurrence posInOccurrence();
@@ -33,11 +33,10 @@ public interface RuleApp extends EqualsModProofIrrelevancy {
* instantiated
*
* @param goal the Goal where to apply the rule
- * @param services the Services encapsulating all java information
* @return list of new created goals
*/
- @Nullable
- ImmutableList execute(Goal goal, Services services);
+ // @Nullable
+ // ImmutableList execute(G goal);
/**
* returns true if all variables are instantiated
@@ -46,6 +45,17 @@ public interface RuleApp extends EqualsModProofIrrelevancy {
*/
boolean complete();
+ /**
+ * applies the specified rule at the specified position if all schema variables have been
+ * instantiated
+ *
+ * @param goal the Goal where to apply the rule
+ * @param services the Services encapsulating all java information
+ * @return list of new created goals
+ */
+ @Nullable
+ ImmutableList execute(Goal goal, Services services);
+
/**
* @return user-friendly name for this rule-application
*/
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SVNameCorrespondenceCollector.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SVNameCorrespondenceCollector.java
index b86aa18d2bf..dfe05eb9e5a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/SVNameCorrespondenceCollector.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/SVNameCorrespondenceCollector.java
@@ -7,7 +7,6 @@
import de.uka.ilkd.key.logic.DefaultVisitor;
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.JFunction;
import de.uka.ilkd.key.logic.op.SchemaVariable;
@@ -84,8 +83,8 @@ public ImmutableMap getCorrespondences() {
* @param semiseq the Semisequent to visit
*/
private void visit(Semisequent semiseq) {
- for (SequentFormula cf : semiseq) {
- cf.formula().execPostOrder(this);
+ for (Term cf : semiseq) {
+ cf.execPostOrder(this);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java
index 6e29239f3eb..94082faab59 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java
@@ -113,7 +113,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence occurrence, TermServices servic
Term newTerm = tb.apply(update, tb.apply(newUpdate, term));
ImmutableList result = goal.split(1);
- result.head().changeFormula(new SequentFormula(newTerm), occurrence);
+ result.head().changeFormula(newTerm, occurrence);
return result;
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java
index 5f61d57f92b..c1adfe7c326 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java
@@ -7,6 +7,7 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
+import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty;
import de.uka.ilkd.key.logic.label.TermLabel;
import de.uka.ilkd.key.logic.op.Operator;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
@@ -491,17 +492,19 @@ public boolean equalsModProofIrrelevancy(Object o) {
if ((ifSequent == null && t2.ifSequent != null)
|| (ifSequent != null && t2.ifSequent == null)) {
return false;
+ } else if (ifSequent.size() != t2.ifSequent.size()) {
+ return false;
} else {
- ImmutableList if1 = ifSequent.asList();
- ImmutableList if2 = t2.ifSequent.asList();
- while (!if1.isEmpty() && !if2.isEmpty()
- && if1.head().equalsModProofIrrelevancy(if2.head())) {
+ ImmutableList if1 = ifSequent.asList();
+ ImmutableList if2 = t2.ifSequent.asList();
+ while (!if1.isEmpty()) {
+ if (!ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY
+ .equalsModThisProperty(if1.head(), if2.head())) {
+ return false;
+ }
if1 = if1.tail();
if2 = if2.tail();
}
- if (!if1.isEmpty() || !if2.isEmpty()) {
- return false;
- }
}
if (!choices.equals(t2.choices)) {
@@ -529,7 +532,9 @@ public int hashCode() {
@Override
public int hashCodeModProofIrrelevancy() {
if (hashcode2 == 0) {
- hashcode2 = ifSequent.getFormulabyNr(1).hashCodeModProofIrrelevancy();
+ Term term = ifSequent.getFormulabyNr(1);
+ hashcode2 =
+ ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(term);
if (hashcode2 == 0) {
hashcode2 = -1;
}
@@ -740,8 +745,8 @@ public Set collectSchemaVars() {
private void collectSchemaVarsHelper(Sequent s, OpCollector oc) {
- for (SequentFormula cf : s) {
- cf.formula().execPostOrder(oc);
+ for (Term cf : s) {
+ cf.execPostOrder(oc);
}
}
@@ -762,9 +767,9 @@ public static class TacletLabelHint {
private final Sequent sequent;
/**
- * The optional {@link SequentFormula} contained in {@link #getSequent()}.
+ * The optional {@link Term} contained in {@link #getSequent()}.
*/
- private final SequentFormula sequentFormula;
+ private final Term seqFormula;
/**
* The optional replace {@link Term} of the taclet.
@@ -788,7 +793,7 @@ public TacletLabelHint(TacletOperation tacletOperation, Sequent sequent) {
assert sequent != null;
this.tacletOperation = tacletOperation;
this.sequent = sequent;
- this.sequentFormula = null;
+ this.seqFormula = null;
this.term = null;
}
@@ -796,30 +801,30 @@ public TacletLabelHint(TacletOperation tacletOperation, Sequent sequent) {
* Constructor creating a hint indicating
* {@link TacletOperation#REPLACE_TERM} as the currently performed operation.
*
- * @param term The optional replace {@link Term} of the taclet.
+ * @param replaceTerm The optional replace {@link Term} of the taclet.
*/
- public TacletLabelHint(Term term) {
- assert term != null;
+ public TacletLabelHint(Term replaceTerm) {
+ assert replaceTerm != null;
this.tacletOperation = TacletOperation.REPLACE_TERM;
this.sequent = null;
- this.sequentFormula = null;
- this.term = term;
+ this.seqFormula = null;
+ this.term = seqFormula;
}
/**
* Constructor.
*
* @param labelHint The previous {@link TacletLabelHint} which is now specialised.
- * @param sequentFormula The optional {@link SequentFormula} contained in
+ * @param formula The optional {@link Term} contained in
* {@link #getSequent()}.
*/
- public TacletLabelHint(TacletLabelHint labelHint, SequentFormula sequentFormula) {
+ public TacletLabelHint(TacletLabelHint labelHint, Term formula) {
assert labelHint != null;
assert !TacletOperation.REPLACE_TERM.equals(labelHint.getTacletOperation());
- assert sequentFormula != null;
+ assert formula != null;
this.tacletOperation = labelHint.getTacletOperation();
this.sequent = labelHint.getSequent();
- this.sequentFormula = sequentFormula;
+ this.seqFormula = formula;
this.term = labelHint.getTerm();
}
@@ -842,12 +847,12 @@ public Sequent getSequent() {
}
/**
- * Returns the optional {@link SequentFormula} contained in {@link #getSequent()}.
+ * Returns the optional {@link Term} contained in {@link #getSequent()}.
*
- * @return The optional {@link SequentFormula} contained in {@link #getSequent()}.
+ * @return The optional {@link Term} contained in {@link #getSequent()}.
*/
- public SequentFormula getSequentFormula() {
- return sequentFormula;
+ public Term getSeqFormula() {
+ return seqFormula;
}
/**
@@ -883,7 +888,7 @@ public Term getTerm() {
@Override
public String toString() {
return tacletOperation + ", sequent = " + sequent + ", sequent formula = "
- + sequentFormula + ", term = " + term;
+ + seqFormula + ", term = " + term;
}
/**
@@ -894,20 +899,20 @@ public String toString() {
public enum TacletOperation {
/**
* Add clause of a {@link Taclet} applied to the antecedent. Available information are
- * {@link TacletLabelHint#getSequent()} and {@link TacletLabelHint#getSequentFormula()}.
+ * {@link TacletLabelHint#getSequent()} and {@link TacletLabelHint#getSeqFormula()}.
*/
ADD_ANTECEDENT,
/**
* Add clause of a {@link Taclet} applied to the succedent. Available information are
- * {@link TacletLabelHint#getSequent()} and {@link TacletLabelHint#getSequentFormula()}.
+ * {@link TacletLabelHint#getSequent()} and {@link TacletLabelHint#getSeqFormula()}.
*/
ADD_SUCCEDENT,
/**
* Replace clause of a {@link Taclet} provides a {@link Sequent} and currently
* additional adds to the antecedent are performed. Available information are
- * {@link TacletLabelHint#getSequent()} and {@link TacletLabelHint#getSequentFormula()}.
+ * {@link TacletLabelHint#getSequent()} and {@link TacletLabelHint#getSeqFormula()}.
*/
REPLACE_TO_ANTECEDENT,
@@ -915,7 +920,7 @@ public enum TacletOperation {
* Replace clause of a {@link Taclet} provides a {@link Sequent} and currently the
* current {@link PosInOccurrence} on the succedent is modified. Available information
* are {@link TacletLabelHint#getSequent()} and
- * {@link TacletLabelHint#getSequentFormula()}.
+ * {@link TacletLabelHint#getSeqFormula()}.
*/
REPLACE_AT_SUCCEDENT,
@@ -923,21 +928,21 @@ public enum TacletOperation {
* Replace clause of a {@link Taclet} provides a {@link Sequent} and currently the
* current {@link PosInOccurrence} on the antecedent is modified. Available information
* are {@link TacletLabelHint#getSequent()} and
- * {@link TacletLabelHint#getSequentFormula()}.
+ * {@link TacletLabelHint#getSeqFormula()}.
*/
REPLACE_AT_ANTECEDENT,
/**
* Replace clause of a {@link Taclet} provides a {@link Sequent} and currently
* additional adds to the succedent are performed. Available information are
- * {@link TacletLabelHint#getSequent()} and {@link TacletLabelHint#getSequentFormula()}.
+ * {@link TacletLabelHint#getSequent()} and {@link TacletLabelHint#getSeqFormula()}.
*/
REPLACE_TO_SUCCEDENT,
/**
* Replace clause of a {@link Taclet} provides a {@link Term} which is currently used to
* modify the {@link PosInOccurrence}. Available information are
- * {@link TacletLabelHint#getTerm()}.
+ * {@link TacletLabelHint#getSeqFormula()}.
*/
REPLACE_TERM
}
@@ -955,7 +960,7 @@ public enum TacletOperation {
*/
@Override
public @NonNull ImmutableList apply(Goal goal, Services services, RuleApp tacletApp) {
- return getExecutor().apply(goal, services, tacletApp);
+ return getExecutor().apply((Goal) goal, services, tacletApp);
}
public TacletExecutor extends Taclet> getExecutor() {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java
index a98632eb8ef..feecc41cc5d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java
@@ -236,8 +236,8 @@ private static Term getTermBelowQuantifier(SchemaVariable varSV, Term term) {
* @return the term below the given quantifier in the find and if-parts of the Taclet
*/
private static Term getTermBelowQuantifier(Taclet taclet, SchemaVariable varSV) {
- for (SequentFormula sequentFormula : taclet.ifSequent()) {
- Term result = getTermBelowQuantifier(varSV, sequentFormula.formula());
+ for (Term assumesFml : taclet.ifSequent()) {
+ Term result = getTermBelowQuantifier(varSV, assumesFml);
if (result != null) {
return result;
}
@@ -895,7 +895,7 @@ public ImmutableList findIfFormulaInstantiations(Sequent seq, Service
* @return a list of tacletapps with the found if formula instantiations
*/
private ImmutableList findIfFormulaInstantiationsHelp(
- ImmutableList ruleSuccTail, ImmutableList ruleAntecTail,
+ ImmutableList ruleSuccTail, ImmutableList ruleAntecTail,
ImmutableArray instSucc,
ImmutableArray instAntec,
ImmutableList instAlreadyMatched, MatchConditions matchCond,
@@ -918,8 +918,8 @@ private ImmutableList findIfFormulaInstantiationsHelp(
}
// Match the current formula
- IfMatchResult mr = taclet().getMatcher().matchIf(instSucc, ruleSuccTail.head().formula(),
- matchCond, services);
+ Term fml = ruleSuccTail.head();
+ IfMatchResult mr = taclet().getMatcher().matchIf(instSucc, fml, matchCond, services);
// For each matching formula call the method again to match
// the remaining terms
@@ -935,10 +935,10 @@ private ImmutableList findIfFormulaInstantiationsHelp(
return res;
}
- private ImmutableList createSemisequentList(Semisequent p_ss) {
- ImmutableList res = ImmutableSLList.nil();
+ private ImmutableList createSemisequentList(Semisequent p_ss) {
+ ImmutableList res = ImmutableSLList.nil();
- for (SequentFormula p_s : p_ss) {
+ for (Term p_s : p_ss) {
res = res.prepend(p_s);
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java
index 567b38b68f1..9ca5be95b01 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletMatcher.java
@@ -6,9 +6,10 @@
import de.uka.ilkd.key.java.ProgramElement;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
import de.uka.ilkd.key.logic.op.SchemaVariable;
+import org.key_project.logic.SyntaxElement;
+
public interface TacletMatcher {
/**
@@ -69,7 +70,7 @@ MatchConditions checkConditions(MatchConditions p_matchconditions,
* instantiationCandidate
or null
if a match was not possible
*/
MatchConditions checkVariableConditions(SchemaVariable var,
- SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services);
+ SyntaxElement instantiationCandidate, MatchConditions matchCond, Services services);
/**
* matches the given term against the taclet's find term if the taclet has no find term or the
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java
index 04d610c2326..60356bf5e21 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletSchemaVariableCollector.java
@@ -10,7 +10,6 @@
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.label.TermLabel;
import de.uka.ilkd.key.logic.op.*;
@@ -159,8 +158,8 @@ public boolean contains(SchemaVariable var) {
* @param semiseq the Semisequent to visit
*/
private void visit(Semisequent semiseq) {
- for (SequentFormula aSemiseq : semiseq) {
- aSemiseq.formula().execPostOrder(this);
+ for (Term aSemiseq : semiseq) {
+ aSemiseq.execPostOrder(this);
}
}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java
index 6b9fe73e9e1..9e3dd9ac82c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java
@@ -56,8 +56,8 @@ private UseDependencyContractRule() {
private static List getEqualityDefs(Term term, Sequent seq) {
final List result = new LinkedList<>();
- for (SequentFormula cf : seq.antecedent()) {
- final Term formula = cf.formula();
+ for (Term cf : seq.antecedent()) {
+ final Term formula = cf;
if (formula.op() instanceof Equality && formula.sub(1).equals(term)) {
result.add(formula.sub(0));
}
@@ -69,8 +69,8 @@ private static List getEqualityDefs(Term term, Sequent seq) {
private static List> getEqualityDefsAndPos(Term term, Sequent seq) {
final List> result =
new LinkedList<>();
- for (SequentFormula cf : seq.antecedent()) {
- final Term formula = cf.formula();
+ for (Term cf : seq.antecedent()) {
+ final Term formula = cf;
if (formula.op() instanceof Equality && formula.sub(1).equals(term)) {
final PosInOccurrence pos = new PosInOccurrence(cf, PosInTerm.getTopLevel(), true);
result.add(new Pair<>(formula.sub(0), pos));
@@ -83,8 +83,8 @@ private static List