Proof slicing extension

.gitignore

@@ -60,7 +60,7 @@ key.core/src/main/gen
 key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.preamble.xml
 
 # this file is automatically generated by gradle task :key.core:generateSolverPropsList
-key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes
+key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/solvers.txt
 
 key/key.ui/examples/**/**.proof
 **/testresults/**

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java

@@ -2,8 +2,7 @@
 
 import java.util.Collection;
 import java.util.LinkedHashSet;
-
-import org.key_project.util.java.ObjectUtil;
+import java.util.Objects;
 
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
@@ -95,9 +94,9 @@ public Proof getSource() {
     public boolean equals(Object obj) {
         if (obj instanceof IProofReference<?>) {
             IProofReference<?> other = (IProofReference<?>) obj;
-            return ObjectUtil.equals(getKind(), other.getKind())
-                    && ObjectUtil.equals(getSource(), other.getSource())
-                    && ObjectUtil.equals(getTarget(), other.getTarget());
+            return Objects.equals(getKind(), other.getKind())
+                    && Objects.equals(getSource(), other.getSource())
+                    && Objects.equals(getTarget(), other.getTarget());
         } else {
             return false;
         }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java

@@ -10,13 +10,13 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Map.Entry;
+import java.util.Objects;
 import java.util.Set;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.java.CollectionUtil;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.ldt.HeapLDT;
@@ -1069,10 +1069,10 @@ public String toString() {
         public boolean equals(Object obj) {
             if (obj instanceof ExtractLocationParameter) {
                 ExtractLocationParameter other = (ExtractLocationParameter) obj;
-                return ObjectUtil.equals(arrayIndex, other.arrayIndex)
+                return Objects.equals(arrayIndex, other.arrayIndex)
                         && stateMember == other.stateMember
-                        && ObjectUtil.equals(parentTerm, other.parentTerm)
-                        && ObjectUtil.equals(programVariable, other.programVariable);
+                        && Objects.equals(parentTerm, other.parentTerm)
+                        && Objects.equals(programVariable, other.programVariable);
             } else {
                 return false;
             }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionVariableExtractor.java

@@ -6,11 +6,11 @@
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Set;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.PosInOccurrence;
@@ -352,8 +352,8 @@ public ParentDef(Term parent, Node goalNode) {
         public boolean equals(Object obj) {
             if (obj instanceof ParentDef) {
                 ParentDef other = (ParentDef) obj;
-                return ObjectUtil.equals(parent, other.parent)
-                        && ObjectUtil.equals(goalNode, other.goalNode);
+                return Objects.equals(parent, other.parent)
+                        && Objects.equals(goalNode, other.goalNode);
             } else {
                 return false;
             }
@@ -408,7 +408,7 @@ public boolean equals(Object obj) {
             if (obj instanceof LocationDef) {
                 LocationDef other = (LocationDef) obj;
                 return programVariable == other.programVariable
-                        && ObjectUtil.equals(arrayIndex, other.arrayIndex);
+                        && Objects.equals(arrayIndex, other.arrayIndex);
             } else {
                 return false;
             }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java

@@ -9,6 +9,7 @@
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Set;
 
 import org.key_project.util.collection.DefaultImmutableSet;
@@ -17,7 +18,6 @@
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.java.CollectionUtil;
 import org.key_project.util.java.IFilter;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.logic.DefaultVisitor;
 import de.uka.ilkd.key.logic.Name;
@@ -901,7 +901,7 @@ protected ISymbolicLayout createLayoutFromExecutionVariableValuePairs(
                         container.addAssociation(association);
                     } else {
                         // Make sure that target is the same
-                        if (!ObjectUtil.equals(association.getTarget(),
+                        if (!Objects.equals(association.getTarget(),
                             existingAssociation.getTarget())) {
                             throw new ProofInputException("Multiple association targets found: "
                                 + association + " and " + existingAssociation + ".");
@@ -928,7 +928,7 @@ protected ISymbolicLayout createLayoutFromExecutionVariableValuePairs(
                         container.addValue(value);
                     } else {
                         // Make sure that the value is the same
-                        if (!ObjectUtil.equals(value.getValue(), existingValue.getValue())) {
+                        if (!Objects.equals(value.getValue(), existingValue.getValue())) {
                             throw new ProofInputException(
                                 "Multiple values found: " + value + " and " + existingValue + ".");
                         }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/object_model/impl/AbstractSymbolicAssociationValueContainer.java

@@ -4,7 +4,6 @@
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.java.CollectionUtil;
 import org.key_project.util.java.IFilter;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
@@ -13,6 +12,8 @@
 import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicAssociationValueContainer;
 import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicValue;
 
+import java.util.Objects;
+
 /**
  * Default implementation of {@link ISymbolicAssociationValueContainer}.
  *
@@ -67,8 +68,8 @@ public ISymbolicAssociation getAssociation(final IProgramVariable programVariabl
             public boolean select(ISymbolicAssociation element) {
                 return element.getProgramVariable() == programVariable
                         && element.isArrayIndex() == isArrayIndex
-                        && ObjectUtil.equals(element.getArrayIndex(), arrayIndex)
-                        && ObjectUtil.equals(element.getCondition(), condition);
+                        && Objects.equals(element.getArrayIndex(), arrayIndex)
+                        && Objects.equals(element.getCondition(), condition);
             }
         });
     }
@@ -101,8 +102,8 @@ public ISymbolicValue getValue(final IProgramVariable programVariable,
             public boolean select(ISymbolicValue element) {
                 return element.getProgramVariable() == programVariable
                         && element.isArrayIndex() == isArrayIndex
-                        && ObjectUtil.equals(element.getArrayIndex(), arrayIndex)
-                        && ObjectUtil.equals(element.getCondition(), condition);
+                        && Objects.equals(element.getArrayIndex(), arrayIndex)
+                        && Objects.equals(element.getCondition(), condition);
             }
         });
     }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java

@@ -4,14 +4,14 @@
 import java.io.StringWriter;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Properties;
 
 import de.uka.ilkd.key.speclang.jml.translation.Context;
 import de.uka.ilkd.key.speclang.njml.JmlIO;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.java.Expression;
 import de.uka.ilkd.key.java.JavaInfo;
@@ -238,8 +238,8 @@ public int hashCode() {
     public boolean equals(Object obj) {
         if (obj instanceof ProgramMethodPO) {
             ProgramMethodPO other = (ProgramMethodPO) obj;
-            return ObjectUtil.equals(pm, other.getProgramMethod())
-                    && ObjectUtil.equals(precondition, other.getPrecondition());
+            return Objects.equals(pm, other.getProgramMethod())
+                    && Objects.equals(precondition, other.getPrecondition());
         } else {
             return false;
         }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java

@@ -5,12 +5,12 @@
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Properties;
 import java.util.Set;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.java.Services;
@@ -276,8 +276,8 @@ public boolean equals(Object obj) {
         if (obj instanceof ProgramMethodSubsetPO) {
             ProgramMethodSubsetPO other = (ProgramMethodSubsetPO) obj;
             return super.equals(obj)
-                    && ObjectUtil.equals(getStartPosition(), other.getStartPosition())
-                    && ObjectUtil.equals(getEndPosition(), other.getEndPosition());
+                    && Objects.equals(getStartPosition(), other.getStartPosition())
+                    && Objects.equals(getEndPosition(), other.getEndPosition());
         } else {
             return false;
         }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractSlicer.java

@@ -6,6 +6,7 @@
 import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Set;
 import java.util.SortedSet;
 import java.util.TreeSet;
@@ -15,7 +16,6 @@
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.java.CollectionUtil;
 import org.key_project.util.java.IFilter;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.java.Expression;
 import de.uka.ilkd.key.java.JavaTools;
@@ -1081,7 +1081,7 @@ public static <T> boolean startsWith(ImmutableList<T> list, ImmutableList<T> pre
             while (same && prefixIter.hasNext()) {
                 T listNext = listIter.next();
                 T prefixNext = prefixIter.next();
-                if (!ObjectUtil.equals(listNext, prefixNext)) {
+                if (!Objects.equals(listNext, prefixNext)) {
                     same = false;
                 }
             }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Access.java

@@ -1,11 +1,12 @@
 package de.uka.ilkd.key.symbolic_execution.slicing;
 
 import org.key_project.util.collection.ImmutableArray;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
 
+import java.util.Objects;
+
 public class Access {
     /**
      * The {@link ProgramVariable} or {@code null} if an array index is accessed.
@@ -96,8 +97,8 @@ public int hashCode() {
     public boolean equals(Object obj) {
         if (obj instanceof Access) {
             Access other = (Access) obj;
-            return ObjectUtil.equals(programVariable, other.getProgramVariable())
-                    && ObjectUtil.equals(dimensionExpressions, other.getDimensionExpressions());
+            return Objects.equals(programVariable, other.getProgramVariable())
+                    && Objects.equals(dimensionExpressions, other.getDimensionExpressions());
         } else {
             return false;
         }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/Location.java

@@ -2,14 +2,15 @@
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.Function;
 import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import java.util.Objects;
+
 /**
  * Represents a location like a local variable, method parameter, static field or an instance field
  * on a specified object.
@@ -77,7 +78,7 @@ public int hashCode() {
     public boolean equals(Object obj) {
         if (obj instanceof Location) {
             Location other = (Location) obj;
-            return ObjectUtil.equals(accesses, other.getAccesses());
+            return Objects.equals(accesses, other.getAccesses());
         } else {
             return false;
         }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/MethodBreakpoint.java

@@ -1,7 +1,5 @@
 package de.uka.ilkd.key.symbolic_execution.strategy.breakpoint;
 
-import org.key_project.util.java.ObjectUtil;
-
 import de.uka.ilkd.key.java.JavaTools;
 import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.java.SourceElement;
@@ -23,6 +21,8 @@
 import de.uka.ilkd.key.speclang.translation.SLTranslationException;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import java.util.Objects;
+
 public class MethodBreakpoint extends AbstractConditionalBreakpoint {
     /**
      * flag to tell whether to stop on method entry
@@ -148,7 +148,7 @@ private boolean isCorrectMethodReturn(Node node, RuleApp ruleApp) {
         term = TermBuilder.goBelowUpdates(term);
         MethodFrame mf =
             JavaTools.getInnermostMethodFrame(term.javaBlock(), node.proof().getServices());
-        return ObjectUtil.equals(getPm(), mf.getProgramMethod());
+        return Objects.equals(getPm(), mf.getProgramMethod());
     }
 
     @Override

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java

@@ -5,14 +5,14 @@
 import java.util.LinkedHashSet;
 import java.util.LinkedList;
 import java.util.List;
+import java.util.Objects;
 import java.util.Set;
 
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.java.CollectionUtil;
 import org.key_project.util.java.IFilter;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
@@ -723,7 +723,7 @@ public static Term extractOperatorTerm(Node node, final Operator operator) {
             public boolean select(SequentFormula element) {
                 Term term = element.formula();
                 term = TermBuilder.goBelowUpdates(term);
-                return ObjectUtil.equals(term.op(), operator);
+                return Objects.equals(term.op(), operator);
             }
         });
         if (sf != null) {

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -13,15 +13,14 @@
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.Set;
 
-import de.uka.ilkd.key.nparser.DebugKeyLexer;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.java.CollectionUtil;
 import org.key_project.util.java.IFilter;
-import org.key_project.util.java.ObjectUtil;
 
 import de.uka.ilkd.key.java.Expression;
 import de.uka.ilkd.key.java.JavaProgramElement;
@@ -4087,7 +4086,7 @@ public static boolean equalsWithPosition(SourceElement first, SourceElement seco
             } else {
                 // Compare all source elements including ints position info
                 return first.equals(second)
-                        && ObjectUtil.equals(first.getPositionInfo(), second.getPositionInfo());
+                        && Objects.equals(first.getPositionInfo(), second.getPositionInfo());
             }
         } else {
             return first == null && second == null;
@@ -4332,7 +4331,7 @@ protected static ImmutableArray<Term> extractValueFromUpdate(Term term,
         ImmutableArray<Term> result = null;
         if (term.op() instanceof ElementaryUpdate) {
             ElementaryUpdate update = (ElementaryUpdate) term.op();
-            if (ObjectUtil.equals(variable, update.lhs())) {
+            if (Objects.equals(variable, update.lhs())) {
                 result = term.subs();
             }
         } else if (term.op() instanceof UpdateJunctor) {