diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java index 8a13a566d5..dc1e89ee63 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java @@ -21,7 +21,7 @@ import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil; import org.key_project.logic.Name; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.Rule; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java index fc7de40232..ffcd3f49bb 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java @@ -37,8 +37,8 @@ import org.key_project.logic.Name; import org.key_project.logic.op.SortedOperator; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate; import org.key_project.prover.sequent.PosInOccurrence; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java index 5d23a22e56..23dfbe8f77 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java @@ -13,7 +13,7 @@ import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; import org.key_project.logic.Name; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; /** * {@link Strategy} used to simplify {@link Term}s in side proofs. diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java b/key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java index 22990771ad..6ce125be55 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java @@ -13,10 +13,10 @@ import de.uka.ilkd.key.rule.match.vm.VMTacletMatcher; import org.key_project.logic.Name; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; -import org.key_project.prover.rules.AssumesMatchResult; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesMatchResult; +import org.key_project.prover.rules.instantiation.SVInstantiations; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java b/key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java index 14bd5b1ca2..2b2f0a08fb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java +++ b/key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java @@ -5,8 +5,8 @@ import de.uka.ilkd.key.logic.Term; -import org.key_project.prover.rules.MatchConditions; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.MatchConditions; +import org.key_project.prover.rules.instantiation.SVInstantiations; import org.key_project.prover.sequent.SequentFormula; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java index 4ac6489976..a097aa4472 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java @@ -22,8 +22,8 @@ import de.uka.ilkd.key.strategy.FocussedBreakpointRuleApplicationManager; import de.uka.ilkd.key.strategy.FocussedRuleApplicationManager; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java index da4fcea8db..bbee30b668 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java @@ -22,8 +22,8 @@ import de.uka.ilkd.key.util.RecognitionException; import org.key_project.logic.LogicServices; -import org.key_project.prover.rules.AssumesFormulaInstDirect; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java index 2dc1b575e5..e16d32fa21 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java @@ -16,8 +16,8 @@ import de.uka.ilkd.key.rule.inst.SortException; import org.key_project.logic.Namespace; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.Sequent; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java index e0c266a21d..eeb7e4d1d6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java @@ -13,7 +13,7 @@ import de.uka.ilkd.key.util.properties.Properties; import org.key_project.logic.LogicServices; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Semisequent; import org.key_project.prover.sequent.SequentChangeInfo; 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 b9528d97dc..150dc75ca4 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 @@ -17,8 +17,8 @@ import de.uka.ilkd.key.rule.inst.*; import org.key_project.logic.PosInTerm; -import org.key_project.prover.rules.inst.InstantiationEntry; -import org.key_project.prover.rules.inst.ListInstantiation; +import org.key_project.prover.rules.instantiation.InstantiationEntry; +import org.key_project.prover.rules.instantiation.ListInstantiation; import org.key_project.prover.sequent.*; import org.key_project.util.collection.*; 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 ea0ac3c559..2f3f6fd2bf 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 @@ -57,9 +57,9 @@ import org.key_project.logic.op.Function; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.AssumesFormulaInstDirect; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; 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 cda65ce87d..cdf77453a4 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 @@ -48,11 +48,11 @@ import org.key_project.logic.PosInTerm; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.AssumesFormulaInstDirect; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; 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 93a61470d8..b3035332d0 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 @@ -26,9 +26,9 @@ import org.key_project.logic.Name; import org.key_project.logic.PosInTerm; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstDirect; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Semisequent; import org.key_project.prover.sequent.Sequent; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AssumesFormulaInstantiationCache.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AssumesFormulaInstantiationCache.java index 7243c283e6..3ea91cc66d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AssumesFormulaInstantiationCache.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AssumesFormulaInstantiationCache.java @@ -7,7 +7,7 @@ import java.util.concurrent.locks.ReentrantReadWriteLock.ReadLock; import java.util.concurrent.locks.ReentrantReadWriteLock.WriteLock; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.Semisequent; import org.key_project.util.LRUCache; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java index 31b0894822..b75f7af886 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java @@ -16,7 +16,7 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.EqualsModProofIrrelevancyUtil; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/IfMatchResult.java b/key.core/src/main/java/de/uka/ilkd/key/rule/IfMatchResult.java index d3cd47832b..4b51f9dde1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/IfMatchResult.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/IfMatchResult.java @@ -6,7 +6,7 @@ import de.uka.ilkd.key.util.Debug; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/MatchConditions.java b/key.core/src/main/java/de/uka/ilkd/key/rule/MatchConditions.java index 72bb714436..bd0272e8fd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/MatchConditions.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/MatchConditions.java @@ -13,7 +13,7 @@ /** * Simple container class containing the information resulting from a Taclet.match-call */ -public class MatchConditions extends org.key_project.prover.rules.MatchConditions { +public class MatchConditions extends org.key_project.prover.rules.instantiation.MatchConditions { public static final MatchConditions EMPTY_MATCHCONDITIONS = new MatchConditions(SVInstantiations.EMPTY_SVINSTANTIATIONS, RenameTable.EMPTY_TABLE); @@ -40,7 +40,7 @@ public SVInstantiations getInstantiations() { @Override public MatchConditions setInstantiations( - org.key_project.prover.rules.inst.SVInstantiations p_instantiations) { + org.key_project.prover.rules.instantiation.SVInstantiations p_instantiations) { if (instantiations == p_instantiations) { return this; } else { 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 046a27cf5a..6ea806b200 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 @@ -13,9 +13,9 @@ import de.uka.ilkd.key.util.Debug; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstantiation; -import org.key_project.prover.rules.MatchConditions; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.MatchConditions; +import org.key_project.prover.rules.instantiation.SVInstantiations; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; @@ -245,8 +245,8 @@ public TacletApp setMatchConditions(MatchConditions mc, Services services) { * metavariables and if formula instantiations given and forget the old ones */ @Override - protected TacletApp setAllInstantiations(org.key_project.prover.rules.MatchConditions mc, - ImmutableList assumesInstantiations, Services services) { + protected TacletApp setAllInstantiations(MatchConditions mc, + ImmutableList assumesInstantiations, Services services) { return createNoPosTacletApp(taclet(), mc.getInstantiations(), assumesInstantiations, services); } 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 12b66a64a2..f77c48044c 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 @@ -35,8 +35,8 @@ import org.key_project.logic.Name; import org.key_project.logic.PosInTerm; -import org.key_project.prover.rules.AssumesFormulaInstDirect; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleSet; import org.key_project.prover.sequent.*; 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 4004023765..c8d4670029 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 @@ -12,9 +12,9 @@ import de.uka.ilkd.key.util.Debug; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstantiation; -import org.key_project.prover.rules.MatchConditions; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.MatchConditions; +import org.key_project.prover.rules.instantiation.SVInstantiations; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; @@ -231,9 +231,9 @@ public TacletApp setMatchConditions(MatchConditions mc, Services services) { * metavariables and if formula instantiations given and forget the old ones */ @Override - protected TacletApp setAllInstantiations(org.key_project.prover.rules.MatchConditions mc, - ImmutableList assumesInstantiations, - Services services) { + protected TacletApp setAllInstantiations(MatchConditions mc, + ImmutableList assumesInstantiations, + Services services) { return createPosTacletApp((FindTaclet) taclet(), mc.getInstantiations(), assumesInstantiations, posInOccurrence(), services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAppUtil.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAppUtil.java index 638e473cfc..c8c24b1bd0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAppUtil.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAppUtil.java @@ -12,8 +12,8 @@ import de.uka.ilkd.key.smt.SMTRuleApp; import org.key_project.logic.PosInTerm; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; 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 e4ab1e22c4..a29c744013 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 @@ -27,8 +27,8 @@ import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.*; -import org.key_project.prover.rules.MatchConditions; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.*; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.sequent.*; import org.key_project.util.collection.*; @@ -816,7 +816,7 @@ public TacletApp addInstantiation(SchemaVariable sv, Name name, Services service * metavariables and if formula instantiations given and forget the old ones */ protected abstract TacletApp setAllInstantiations( - org.key_project.prover.rules.MatchConditions mc, + MatchConditions mc, ImmutableList ifInstantiations, Services services); /** @@ -894,7 +894,7 @@ private ImmutableList findIfFormulaInstantiationsHelp( ImmutableArray instSucc, ImmutableArray instAntec, ImmutableList instAlreadyMatched, - org.key_project.prover.rules.MatchConditions matchCond, + MatchConditions matchCond, Services services) { while (ruleSuccTail.isEmpty()) { @@ -921,7 +921,7 @@ private ImmutableList findIfFormulaInstantiationsHelp( // For each matching formula call the method again to match // the remaining terms ImmutableList res = ImmutableSLList.nil(); - Iterator itMC = + Iterator itMC = mr.matchConditions().iterator(); ruleSuccTail = ruleSuccTail.tail(); for (final AssumesFormulaInstantiation instantiationCandidate : mr.candidates()) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java index 35de237fec..dd8b71736f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java @@ -9,7 +9,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java index 267f953518..a478b056d3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java @@ -14,7 +14,7 @@ import org.key_project.logic.Name; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableSet; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java index 178ab74710..b6f9a8f2a4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java @@ -18,7 +18,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java index e907b73eef..07e75d2aa3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java @@ -13,7 +13,7 @@ import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.Function; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java index 95ecfda746..840ced5512 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java @@ -13,7 +13,7 @@ import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.Function; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java index b3bd8823c3..bab9857b5c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java @@ -15,7 +15,7 @@ import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java index e8801aa885..768557598b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java @@ -21,7 +21,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java index 76b4532b67..290e99999d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java @@ -14,7 +14,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java index ad47fde98a..90adc4b100 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java @@ -19,7 +19,7 @@ import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java index 80665d3014..a01b792571 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java @@ -22,7 +22,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java index 49c0262b05..fd344a6231 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java @@ -22,7 +22,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java index 932c036cb2..e8a86e8998 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java @@ -12,7 +12,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java index 0a3affe4f3..422fa94d48 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java @@ -40,8 +40,8 @@ public NewJumpLabelCondition(SchemaVariable sv) { @Override public MatchConditions check(SchemaVariable var, - SyntaxElement instCandidate, - org.key_project.prover.rules.MatchConditions matchCond, LogicServices services) { + SyntaxElement instCandidate, + org.key_project.prover.rules.instantiation.MatchConditions matchCond, LogicServices services) { SVInstantiations instantiations = (SVInstantiations) matchCond.getInstantiations(); if (var != labelSV && instantiations.isInstantiated(labelSV)) { var = labelSV; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java index eea656ae22..017efd5e97 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java @@ -11,9 +11,9 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.SVInstantiations; public final class ObserverCondition implements VariableCondition { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java index c3d435e734..c43d006f8b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SameObserverCondition.java @@ -15,7 +15,7 @@ import org.key_project.logic.ParsableVariable; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; import org.key_project.util.collection.ImmutableSet; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java index c36214a9f7..3d19826740 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java @@ -17,9 +17,9 @@ import org.key_project.logic.Named; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.SVInstantiations; public class SimplifyIfThenElseUpdateCondition implements VariableCondition { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java index 62f057cd68..13e648661a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java @@ -14,9 +14,9 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.SVInstantiations; /** * Stores the given {@link Statement}, after substitution of {@link SchemaVariable}s, into the given diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java index 01c853daf0..1cfe990c7b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java @@ -10,7 +10,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.rules.VariableCondition; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/TacletExecutor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/TacletExecutor.java index 9dcd0e6958..9080b10475 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/TacletExecutor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/TacletExecutor.java @@ -85,11 +85,11 @@ protected Term and(Term t1, Term t2, Goal goal) { */ @Override protected Term syntacticalReplace(Term term, - PosInOccurrence applicationPosInOccurrence, - org.key_project.prover.rules.MatchConditions mc, Goal goal, - RuleApp ruleApp, - LogicServices services, - Object... /* TermLabelState, TacletLabelHint */ instantiationInfo) { + PosInOccurrence applicationPosInOccurrence, + org.key_project.prover.rules.instantiation.MatchConditions mc, Goal goal, + RuleApp ruleApp, + LogicServices services, + Object... /* TermLabelState, TacletLabelHint */ instantiationInfo) { final SyntacticalReplaceVisitor srVisitor = new SyntacticalReplaceVisitor((TermLabelState) instantiationInfo[0], (TacletLabelHint) instantiationInfo[1], applicationPosInOccurrence, @@ -99,7 +99,7 @@ protected Term syntacticalReplace(Term term, return srVisitor.getTerm(); } - protected Term applyContextUpdate(org.key_project.prover.rules.inst.SVInstantiations p_svInst, + protected Term applyContextUpdate(org.key_project.prover.rules.instantiation.SVInstantiations p_svInst, Term formula, Goal goal) { // var instantiatedFormula = (de.uka.ilkd.key.logic.Term) formula; final SVInstantiations svInst = (SVInstantiations) p_svInst; @@ -131,7 +131,7 @@ protected Term applyContextUpdate(org.key_project.prover.rules.inst.SVInstantiat protected ImmutableList instantiateSemisequent( Semisequent semi, PosInOccurrence applicationPosInOccurrence, - org.key_project.prover.rules.MatchConditions matchCond, Goal goal, + org.key_project.prover.rules.instantiation.MatchConditions matchCond, Goal goal, RuleApp tacletApp, LogicServices services, Object... instantiationInfo) { // TermLabelState termLabelState, TacletLabelHint // labelHint) { @@ -161,7 +161,7 @@ protected ImmutableList instantiateSemisequent( protected void applyAddrule(ImmutableList rules, Goal goal, LogicServices services, - org.key_project.prover.rules.MatchConditions p_matchCond) { + org.key_project.prover.rules.instantiation.MatchConditions p_matchCond) { var matchCond = (MatchConditions) p_matchCond; for (var tacletToAdd : rules) { final Node n = goal.node(); @@ -208,7 +208,7 @@ protected void applyAddProgVars(ImmutableSet renamings = ImmutableSLList.nil(); for (final SchemaVariable sv : pvs) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java index 9573c92d4a..9c3a23c3ea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java @@ -12,7 +12,7 @@ import org.key_project.logic.Term; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java index 939f9ad9b2..95b959f419 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java @@ -16,7 +16,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.op.sv.OperatorSV; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; import org.key_project.util.collection.DefaultImmutableMap; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableMap; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java index d268ed7300..f0e5ce2569 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java @@ -20,8 +20,8 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.Name; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.inst.InstantiationEntry; -import org.key_project.prover.rules.inst.ListInstantiation; +import org.key_project.prover.rules.instantiation.InstantiationEntry; +import org.key_project.prover.rules.instantiation.ListInstantiation; import org.key_project.util.collection.DefaultImmutableMap; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -37,7 +37,7 @@ * and is used to store instantiations of schemavariables. The class is immutable, * this means changing its content results in creating a new object. */ -public class SVInstantiations implements org.key_project.prover.rules.inst.SVInstantiations { +public class SVInstantiations implements org.key_project.prover.rules.instantiation.SVInstantiations { /** the empty instantiation */ public static final SVInstantiations EMPTY_SVINSTANTIATIONS = new SVInstantiations(); @@ -596,7 +596,7 @@ public int hashCode() { return result; } - public SVInstantiations union(org.key_project.prover.rules.inst.SVInstantiations p_other, + public SVInstantiations union(org.key_project.prover.rules.instantiation.SVInstantiations p_other, LogicServices services) { final var other = (SVInstantiations) p_other; ImmutableMap> result = map; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java index a735321c85..88bdca24bd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java @@ -24,6 +24,9 @@ import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.prover.rules.*; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesMatchResult; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableList; @@ -111,15 +114,15 @@ public VMTacletMatcher(Taclet taclet) { */ @Override public final AssumesMatchResult matchAssumes(Iterable p_toMatch, - org.key_project.logic.Term p_template, - org.key_project.prover.rules.MatchConditions p_matchCond, - LogicServices p_services) { + org.key_project.logic.Term p_template, + org.key_project.prover.rules.instantiation.MatchConditions p_matchCond, + LogicServices p_services) { TacletMatchProgram prg = assumesMatchPrograms.get(p_template); MatchConditions mc = (MatchConditions) p_matchCond; ImmutableList resFormulas = ImmutableSLList.nil(); - ImmutableList resMC = ImmutableSLList.nil(); + ImmutableList resMC = ImmutableSLList.nil(); final boolean updateContextPresent = !mc.getInstantiations().getUpdateContext().isEmpty(); ImmutableList context = ImmutableSLList.nil(); @@ -185,7 +188,7 @@ private Term matchUpdateContext(ImmutableList context, Term for @Override public final MatchConditions matchAssumes( Iterable p_toMatch, - org.key_project.prover.rules.MatchConditions p_matchCond, + org.key_project.prover.rules.instantiation.MatchConditions p_matchCond, LogicServices p_services) { final Iterator anteIterator = @@ -193,7 +196,7 @@ public final MatchConditions matchAssumes( final Iterator succIterator = assumesSequent.succedent().iterator(); - ImmutableList newMC; + ImmutableList newMC; for (final AssumesFormulaInstantiation candidateInst : p_toMatch) { // Part of fix for #1716: match antecedent with antecedent, succ with succ @@ -230,8 +233,8 @@ public final MatchConditions matchAssumes( * {@inheritDoc} */ @Override - public final MatchConditions checkConditions(org.key_project.prover.rules.MatchConditions cond, - LogicServices services) { + public final MatchConditions checkConditions(org.key_project.prover.rules.instantiation.MatchConditions cond, + LogicServices services) { MatchConditions result = (MatchConditions) cond; if (result != null) { final var svIterator = result.getInstantiations().svIterator(); @@ -283,8 +286,8 @@ private boolean varIsBound(SchemaVariable v) { */ @Override public final MatchConditions checkVariableConditions(SchemaVariable var, - SyntaxElement instantiationCandidate, - org.key_project.prover.rules.MatchConditions matchCond, LogicServices services) { + SyntaxElement instantiationCandidate, + org.key_project.prover.rules.instantiation.MatchConditions matchCond, LogicServices services) { if (matchCond != null) { if (instantiationCandidate instanceof Term term) { if (!(term.op() instanceof QuantifiableVariable)) { @@ -337,9 +340,9 @@ private Pair matchAndIgnoreUpdatePrefix( * {@inheritDoc} */ @Override - public final org.key_project.prover.rules.MatchConditions matchFind( + public final org.key_project.prover.rules.instantiation.MatchConditions matchFind( org.key_project.logic.Term term, - org.key_project.prover.rules.MatchConditions p_matchCond, + org.key_project.prover.rules.instantiation.MatchConditions p_matchCond, LogicServices services) { if (findMatchProgram == TacletMatchProgram.EMPTY_PROGRAM) { return null; @@ -362,7 +365,7 @@ public final org.key_project.prover.rules.MatchConditions matchFind( @Override public MatchConditions matchSV(SchemaVariable sv, SyntaxElement syntaxElement, - org.key_project.prover.rules.MatchConditions matchCond, + org.key_project.prover.rules.instantiation.MatchConditions matchCond, LogicServices services) { final MatchSchemaVariableInstruction instr = diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/AssumesInstantiator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/AssumesInstantiator.java index 6b23c2b16e..02d3b8bb8f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/AssumesInstantiator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/AssumesInstantiator.java @@ -16,9 +16,9 @@ import de.uka.ilkd.key.util.Debug; import org.key_project.logic.PosInTerm; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; -import org.key_project.prover.rules.AssumesMatchResult; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesMatchResult; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; @@ -231,7 +231,7 @@ private void findIfFormulaInstantiationsHelp( // For each matching formula call the method again to match // the remaining terms - Iterator itMC = + Iterator itMC = mr.matchConditions().iterator(); p_ifSeqTail = p_ifSeqTail.tail(); for (final AssumesFormulaInstantiation ifInstantiation : mr.candidates()) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java index 7d44617084..17292718ae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java @@ -11,7 +11,7 @@ import de.uka.ilkd.key.proof.Node; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.util.LRUCache; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java index ab4f6f7153..2188da4c72 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java @@ -13,8 +13,8 @@ import de.uka.ilkd.key.util.Debug; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractNonDuplicateAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractNonDuplicateAppFeature.java index 1385bf8b8a..a712eb8051 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractNonDuplicateAppFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractNonDuplicateAppFeature.java @@ -14,9 +14,9 @@ import de.uka.ilkd.key.rule.inst.SVInstantiations; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableMap; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java index 16108799a1..bd4878a888 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java @@ -9,8 +9,8 @@ import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.util.Debug; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PIOPathIterator; import org.key_project.prover.sequent.PosInOccurrence; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndIfFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndIfFeature.java index 3ac4fdc610..5c98742662 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndIfFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndIfFeature.java @@ -6,8 +6,8 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.TacletApp; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java index f7f2f6c8e1..b88055f029 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java @@ -24,9 +24,9 @@ import de.uka.ilkd.key.strategy.TopRuleAppCost; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Semisequent; import org.key_project.prover.sequent.Sequent; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java index 06521f20e0..ab12bcb3f7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java @@ -7,7 +7,7 @@ import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.util.Debug; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java b/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java index 3a1900dd78..33281994f2 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java @@ -19,8 +19,8 @@ import org.key_project.logic.Name; import org.key_project.logic.PosInTerm; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstDirect; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.*; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/TestMatchTaclet.java b/key.core/src/test/java/de/uka/ilkd/key/rule/TestMatchTaclet.java index 10482b7314..a67606d6e7 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/TestMatchTaclet.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/TestMatchTaclet.java @@ -25,7 +25,7 @@ import org.key_project.logic.PosInTerm; import org.key_project.logic.op.Function; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.sequent.*; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSLList; diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/TestSchemaModalOperators.java b/key.core/src/test/java/de/uka/ilkd/key/rule/TestSchemaModalOperators.java index 860a8171b2..f1a7e8bf6a 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/TestSchemaModalOperators.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/TestSchemaModalOperators.java @@ -20,7 +20,7 @@ import org.key_project.logic.Name; import org.key_project.logic.PosInTerm; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.prover.sequent.*; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java index 2f52eacacf..f6532d87a5 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java @@ -14,7 +14,7 @@ import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.junit.jupiter.api.Test; diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcherTest.java b/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcherTest.java index f6ff530610..2bef9e1289 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcherTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcherTest.java @@ -14,7 +14,7 @@ import de.uka.ilkd.key.util.HelperClassForTests; import org.key_project.logic.Name; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.junit.jupiter.api.BeforeAll; import org.junit.jupiter.api.Test; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletExecutor.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletExecutor.java index 8c7321e8eb..7685d5bf40 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletExecutor.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletExecutor.java @@ -9,7 +9,10 @@ import org.key_project.logic.Term; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.prover.proof.ProofGoal; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.MatchConditions; +import org.key_project.prover.rules.instantiation.SVInstantiations; import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate; import org.key_project.prover.sequent.*; import org.key_project.util.collection.ImmutableList; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletMatcher.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletMatcher.java index cb2367da88..952ddc4eee 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletMatcher.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/TacletMatcher.java @@ -7,6 +7,9 @@ import org.key_project.logic.SyntaxElement; import org.key_project.logic.Term; import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesMatchResult; +import org.key_project.prover.rules.instantiation.MatchConditions; public interface TacletMatcher { /** @@ -26,7 +29,7 @@ public interface TacletMatcher { * @return the found schema variable mapping or null if the matching failed */ MatchConditions matchFind(Term term, MatchConditions matchCond, - LogicServices services); + LogicServices services); /** * checks if the conditions for a correct instantiation are satisfied @@ -73,7 +76,7 @@ MatchConditions checkVariableConditions(org.key_project.logic.op.sv.SchemaVariab * MatchConditions. */ AssumesMatchResult matchAssumes(Iterable toMatch, Term template, - MatchConditions matchCond, LogicServices services); + MatchConditions matchCond, LogicServices services); /** * Match the whole if sequent using the given list of instantiations of all assumes-sequent diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/VariableCondition.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/VariableCondition.java index e6d89ac43a..7a2e894a74 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/VariableCondition.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/VariableCondition.java @@ -6,6 +6,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.instantiation.MatchConditions; /** * The instantiations of a schemavariable can be restricted on rule scope by attaching conditions on @@ -29,5 +30,5 @@ public interface VariableCondition { * otherwise */ MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, - MatchConditions matchCond, LogicServices services); + MatchConditions matchCond, LogicServices services); } diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstDirect.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstDirect.java similarity index 97% rename from key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstDirect.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstDirect.java index 45bd721f0e..7c67e06845 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstDirect.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstDirect.java @@ -1,7 +1,7 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package org.key_project.prover.rules; +package org.key_project.prover.rules.instantiation; import org.key_project.logic.LogicServices; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstSeq.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstSeq.java similarity index 98% rename from key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstSeq.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstSeq.java index 66d017bda9..0e0c8742ad 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstSeq.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstSeq.java @@ -1,7 +1,7 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package org.key_project.prover.rules; +package org.key_project.prover.rules.instantiation; import org.key_project.logic.LogicServices; import org.key_project.logic.PosInTerm; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstantiation.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstantiation.java similarity index 92% rename from key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstantiation.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstantiation.java index e3c082cddd..b6a7330033 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesFormulaInstantiation.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstantiation.java @@ -1,7 +1,7 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package org.key_project.prover.rules; +package org.key_project.prover.rules.instantiation; import org.key_project.logic.LogicServices; import org.key_project.prover.sequent.SequentFormula; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesMatchResult.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesMatchResult.java similarity index 96% rename from key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesMatchResult.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesMatchResult.java index 498e30411a..980172589d 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/AssumesMatchResult.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesMatchResult.java @@ -1,7 +1,7 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package org.key_project.prover.rules; +package org.key_project.prover.rules.instantiation; import org.key_project.util.collection.ImmutableList; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/InstantiationEntry.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/InstantiationEntry.java similarity index 97% rename from key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/InstantiationEntry.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/InstantiationEntry.java index 1201307028..f50bdb43c7 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/InstantiationEntry.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/InstantiationEntry.java @@ -1,7 +1,7 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package org.key_project.prover.rules.inst; +package org.key_project.prover.rules.instantiation; import org.jspecify.annotations.NonNull; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/ListInstantiation.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/ListInstantiation.java similarity index 95% rename from key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/ListInstantiation.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/ListInstantiation.java index 6d9e9eddcd..c234602413 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/ListInstantiation.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/ListInstantiation.java @@ -1,7 +1,7 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package org.key_project.prover.rules.inst; +package org.key_project.prover.rules.instantiation; import org.key_project.util.collection.ImmutableArray; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/MatchConditions.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/MatchConditions.java similarity index 85% rename from key.ncore.calculus/src/main/java/org/key_project/prover/rules/MatchConditions.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/MatchConditions.java index aa5551d9a3..69e7ef2a9c 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/MatchConditions.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/MatchConditions.java @@ -1,11 +1,9 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package org.key_project.prover.rules; +package org.key_project.prover.rules.instantiation; -import org.key_project.prover.rules.inst.SVInstantiations; - public abstract class MatchConditions { protected final SVInstantiations instantiations; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/SVInstantiations.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/SVInstantiations.java similarity index 98% rename from key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/SVInstantiations.java rename to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/SVInstantiations.java index a2126283c2..ace047e504 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/inst/SVInstantiations.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/SVInstantiations.java @@ -1,7 +1,7 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package org.key_project.prover.rules.inst; +package org.key_project.prover.rules.instantiation; import org.key_project.logic.LogicServices; import org.key_project.logic.Name; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletIfSelectionDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletIfSelectionDialog.java index 938815ee5a..e0a5842de9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletIfSelectionDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletIfSelectionDialog.java @@ -14,7 +14,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.io.ProofSaver; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java index fd0147e0db..c07c7b9209 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java @@ -28,8 +28,8 @@ import org.key_project.logic.PosInTerm; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java index 69f14d5105..64c7f8ce78 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java @@ -24,8 +24,8 @@ import de.uka.ilkd.key.smt.SMTRuleApp; import org.key_project.logic.PosInTerm; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/IntermediateProofReplayer.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/IntermediateProofReplayer.java index 2f3deb5500..b55fc5d39a 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/IntermediateProofReplayer.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/IntermediateProofReplayer.java @@ -15,9 +15,9 @@ import org.key_project.logic.op.Function; import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstDirect; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java index 8f24ee61bb..826eb584ae 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/proof/io/OutputStreamProofSaver.java @@ -12,8 +12,8 @@ import org.key_project.logic.Name; import org.key_project.logic.PosInTerm; import org.key_project.logic.Term; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; import org.key_project.rusty.Services; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/IfMatchResult.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/IfMatchResult.java index 8269badd03..eadd4de1b5 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/IfMatchResult.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/IfMatchResult.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.rule; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.util.collection.ImmutableList; public class IfMatchResult { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/MatchConditions.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/MatchConditions.java index d357557bc4..08f4e6507a 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/MatchConditions.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/MatchConditions.java @@ -5,7 +5,7 @@ import org.key_project.rusty.rule.inst.SVInstantiations; -public class MatchConditions extends org.key_project.prover.rules.MatchConditions { +public class MatchConditions extends org.key_project.prover.rules.instantiation.MatchConditions { public static final MatchConditions EMPTY_MATCHCONDITIONS = new MatchConditions(SVInstantiations.EMPTY_SVINSTANTIATIONS); @@ -22,7 +22,7 @@ public SVInstantiations getInstantiations() { } public MatchConditions setInstantiations( - org.key_project.prover.rules.inst.SVInstantiations p_instantiations) { + org.key_project.prover.rules.instantiation.SVInstantiations p_instantiations) { if (instantiations == p_instantiations) { return this; } else { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/NoPosTacletApp.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/NoPosTacletApp.java index 33ea8ad185..4e0bed9b86 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/NoPosTacletApp.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/NoPosTacletApp.java @@ -7,9 +7,9 @@ import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstantiation; -import org.key_project.prover.rules.MatchConditions; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.MatchConditions; +import org.key_project.prover.rules.instantiation.SVInstantiations; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.rusty.Services; import org.key_project.util.collection.DefaultImmutableSet; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/PosTacletApp.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/PosTacletApp.java index b902352694..1f826d64b0 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/PosTacletApp.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/PosTacletApp.java @@ -8,9 +8,9 @@ import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstantiation; -import org.key_project.prover.rules.MatchConditions; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.MatchConditions; +import org.key_project.prover.rules.instantiation.SVInstantiations; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.rusty.Services; import org.key_project.util.collection.DefaultImmutableSet; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletApp.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletApp.java index 4e22b21900..585aec5b27 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletApp.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletApp.java @@ -13,11 +13,11 @@ import org.key_project.logic.op.sv.OperatorSV; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.AssumesFormulaInstSeq; -import org.key_project.prover.rules.AssumesFormulaInstantiation; -import org.key_project.prover.rules.AssumesMatchResult; -import org.key_project.prover.rules.MatchConditions; -import org.key_project.prover.rules.inst.SVInstantiations; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesMatchResult; +import org.key_project.prover.rules.instantiation.MatchConditions; +import org.key_project.prover.rules.instantiation.SVInstantiations; import org.key_project.prover.sequent.*; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java index e48d489ce7..9b3a54b5ed 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletExecutor.java @@ -58,8 +58,8 @@ protected Term syntacticalReplace(Term term, PosInOccurrence applicationPosInOcc @Override protected Term syntacticalReplace(Term term, PosInOccurrence applicationPosInOccurrence, - org.key_project.prover.rules.MatchConditions mc, @NonNull Goal goal, - @NonNull RuleApp ruleApp, LogicServices services, Object... instantiationInfo) { + org.key_project.prover.rules.instantiation.MatchConditions mc, @NonNull Goal goal, + @NonNull RuleApp ruleApp, LogicServices services, Object... instantiationInfo) { return syntacticalReplace(term, applicationPosInOccurrence, (MatchConditions) mc, goal, ruleApp, (Services) services); } @@ -77,7 +77,7 @@ protected Term syntacticalReplace(Term term, PosInOccurrence applicationPosInOcc @Override protected void applyAddrule(ImmutableList rules, @NonNull Goal goal, LogicServices p_services, - org.key_project.prover.rules.MatchConditions p_matchCond) { + org.key_project.prover.rules.instantiation.MatchConditions p_matchCond) { var services = (Services) p_services; var matchCond = (MatchConditions) p_matchCond; for (var rule : rules) { @@ -124,7 +124,7 @@ protected void applyAddrule(ImmutableList> { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramInstantiation.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramInstantiation.java index 47dd02030f..4f89628417 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramInstantiation.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramInstantiation.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.rule.inst; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; import org.key_project.rusty.ast.RustyProgramElement; /** diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramListInstantiation.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramListInstantiation.java index d85e5674d0..a1f46295d9 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramListInstantiation.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/ProgramListInstantiation.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.rule.inst; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.util.collection.ImmutableArray; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java index 6748a416bd..efbb98bef9 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java @@ -10,7 +10,7 @@ import org.key_project.logic.Term; import org.key_project.logic.op.sv.OperatorSV; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.logic.PosInProgram; @@ -22,7 +22,7 @@ import static org.key_project.rusty.rule.match.instructions.MatchProgramSVInstruction.convertToLogicElement; -public class SVInstantiations implements org.key_project.prover.rules.inst.SVInstantiations { +public class SVInstantiations implements org.key_project.prover.rules.instantiation.SVInstantiations { /** the empty instantiation */ public static final SVInstantiations EMPTY_SVINSTANTIATIONS = new SVInstantiations(); /** @@ -341,7 +341,7 @@ public boolean isEmpty() { && genericSortConditions.isEmpty() && genericSortInstantiations.isEmpty()); } - public SVInstantiations union(org.key_project.prover.rules.inst.SVInstantiations p_other, + public SVInstantiations union(org.key_project.prover.rules.instantiation.SVInstantiations p_other, LogicServices services) { final var other = (SVInstantiations) p_other; ImmutableMap> result = map; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/TermInstantiation.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/TermInstantiation.java index adc83e6ace..9a98b3308d 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/TermInstantiation.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/TermInstantiation.java @@ -5,7 +5,7 @@ import org.key_project.logic.Term; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.inst.InstantiationEntry; +import org.key_project.prover.rules.instantiation.InstantiationEntry; import org.key_project.rusty.logic.op.sv.OperatorSV; public class TermInstantiation extends InstantiationEntry { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/TacletMatchProgram.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/TacletMatchProgram.java index 37b9c2dc91..b9c3755453 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/TacletMatchProgram.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/TacletMatchProgram.java @@ -11,7 +11,7 @@ import org.key_project.logic.op.Operator; import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.logic.op.ElementaryUpdate; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/VMTacletMatcher.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/VMTacletMatcher.java index 36e5dd5c68..7595642b7e 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/VMTacletMatcher.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/VMTacletMatcher.java @@ -12,6 +12,9 @@ import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.prover.rules.*; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesMatchResult; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.logic.op.UpdateApplication; import org.key_project.rusty.rule.*; @@ -81,9 +84,9 @@ public VMTacletMatcher(Taclet taclet) { } @Override - public org.key_project.prover.rules.MatchConditions matchFind( + public org.key_project.prover.rules.instantiation.MatchConditions matchFind( Term term, - org.key_project.prover.rules.MatchConditions matchCond, + org.key_project.prover.rules.instantiation.MatchConditions matchCond, LogicServices services) { if (findMatchProgram == TacletMatchProgram.EMPTY_PROGRAM) { return null; @@ -101,8 +104,8 @@ public org.key_project.prover.rules.MatchConditions matchFind( * {@inheritDoc} */ @Override - public final MatchConditions checkConditions(org.key_project.prover.rules.MatchConditions cond, - LogicServices services) { + public final MatchConditions checkConditions(org.key_project.prover.rules.instantiation.MatchConditions cond, + LogicServices services) { MatchConditions result = (MatchConditions) cond; if (result != null) { final var svIterator = result.getInstantiations().svIterator(); @@ -154,7 +157,7 @@ private boolean varDeclaredNotFree(SchemaVariable var) { @Override public final MatchConditions checkVariableConditions(SchemaVariable var, SyntaxElement instantiationCandidate, - org.key_project.prover.rules.MatchConditions matchCond, + org.key_project.prover.rules.instantiation.MatchConditions matchCond, LogicServices services) { if (matchCond != null) { if (instantiationCandidate instanceof Term term) { @@ -205,15 +208,15 @@ private Pair matchAndIgnoreUpdatePrefix(final Term term, @Override public final AssumesMatchResult matchAssumes(Iterable toMatch, - org.key_project.logic.Term p_template, - org.key_project.prover.rules.MatchConditions p_matchCond, - LogicServices p_services) { + org.key_project.logic.Term p_template, + org.key_project.prover.rules.instantiation.MatchConditions p_matchCond, + LogicServices p_services) { TacletMatchProgram prg = assumesMatchPrograms.get(p_template); MatchConditions matchCond = (MatchConditions) p_matchCond; ImmutableList resFormulas = ImmutableSLList.nil(); - ImmutableList resMC = ImmutableSLList.nil(); + ImmutableList resMC = ImmutableSLList.nil(); final boolean updateContextPresent = !matchCond.getInstantiations().getUpdateContext().isEmpty(); @@ -278,12 +281,12 @@ private Term matchUpdateContext(ImmutableList context, Term formula) { @Override public final MatchConditions matchAssumes( Iterable p_toMatch, - org.key_project.prover.rules.MatchConditions p_matchCond, LogicServices p_services) { + org.key_project.prover.rules.instantiation.MatchConditions p_matchCond, LogicServices p_services) { final var anteIterator = assumesSequent.antecedent().iterator(); final var succIterator = assumesSequent.succedent().iterator(); - ImmutableList newMC; + ImmutableList newMC; for (final AssumesFormulaInstantiation candidateInst : p_toMatch) { // Part of fix for #1716: match antecedent with antecedent, succ with succ @@ -322,7 +325,7 @@ public final MatchConditions matchAssumes( @Override public MatchConditions matchSV(SchemaVariable sv, SyntaxElement syntaxElement, - org.key_project.prover.rules.MatchConditions matchCond, + org.key_project.prover.rules.instantiation.MatchConditions matchCond, LogicServices services) { final MatchSchemaVariableInstruction instr = diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/BindVariablesInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/BindVariablesInstruction.java index 04961fe22b..910b74691a 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/BindVariablesInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/BindVariablesInstruction.java @@ -7,7 +7,7 @@ import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.Services; import org.key_project.rusty.logic.op.BoundVariable; import org.key_project.rusty.logic.op.sv.VariableSV; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/Instruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/Instruction.java index d2cc88f9e4..bcec43300a 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/Instruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/Instruction.java @@ -7,7 +7,7 @@ import org.key_project.logic.Term; import org.key_project.logic.op.Operator; import org.key_project.logic.op.QuantifiableVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.logic.op.ElementaryUpdate; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchElementaryUpdateInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchElementaryUpdateInstruction.java index 57c4f4baef..34d284266d 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchElementaryUpdateInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchElementaryUpdateInstruction.java @@ -6,7 +6,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.logic.op.ElementaryUpdate; import org.key_project.rusty.logic.op.ProgramVariable; import org.key_project.rusty.logic.op.sv.ProgramSV; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchFormulaSVInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchFormulaSVInstruction.java index 2ebf818143..3effa909cd 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchFormulaSVInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchFormulaSVInstruction.java @@ -6,7 +6,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.logic.RustyDLTheory; import org.key_project.rusty.logic.op.sv.FormulaSV; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchInstruction.java index 217eca3860..3ed39037c2 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchInstruction.java @@ -5,7 +5,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElementCursor; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; /** * Interface that has to be implemented by instructions for the matching virtual machine diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchModalOperatorSVInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchModalOperatorSVInstruction.java index f88b083a14..73856f03e8 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchModalOperatorSVInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchModalOperatorSVInstruction.java @@ -5,7 +5,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElementCursor; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.logic.op.Modality; import org.key_project.rusty.logic.op.sv.ModalOperatorSV; import org.key_project.rusty.rule.inst.SVInstantiations; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchModalityInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchModalityInstruction.java index 77e9a1b5bc..086e6070d6 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchModalityInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchModalityInstruction.java @@ -7,7 +7,7 @@ import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; import org.key_project.logic.op.Operator; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.logic.op.Modality; import org.jspecify.annotations.NonNull; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchOpIdentityInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchOpIdentityInstruction.java index 4ac652e14c..480cc6153a 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchOpIdentityInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchOpIdentityInstruction.java @@ -7,7 +7,7 @@ import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; import org.key_project.logic.op.Operator; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; /** * The match instruction reports a success if the top level operator of the term to be matched is diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchOperatorInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchOperatorInstruction.java index 623cc9cd88..33941b10bc 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchOperatorInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchOperatorInstruction.java @@ -5,7 +5,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.op.Operator; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; public interface MatchOperatorInstruction extends MatchInstruction { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramInstruction.java index 4cbf900948..2e529777bf 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramInstruction.java @@ -5,7 +5,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElementCursor; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.ast.SourceData; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramSVInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramSVInstruction.java index 9093c20e2d..ce76f1657c 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramSVInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramSVInstruction.java @@ -7,7 +7,7 @@ import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; import org.key_project.logic.op.Operator; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.ast.expr.ArithLogicalExpression; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java index f5138e4c6e..6ae79fa24f 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java @@ -7,7 +7,7 @@ import org.key_project.logic.Term; import org.key_project.logic.op.sv.OperatorSV; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.Services; import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.rule.inst.IllegalInstantiationException; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchTermSVInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchTermSVInstruction.java index 8c1428b661..05d378a650 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchTermSVInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchTermSVInstruction.java @@ -6,7 +6,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.logic.op.sv.TermSV; import org.jspecify.annotations.NonNull; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchUpdateSVInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchUpdateSVInstruction.java index 47e3fe7e76..299c3f2513 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchUpdateSVInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchUpdateSVInstruction.java @@ -6,7 +6,7 @@ import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.logic.op.sv.UpdateSV; import org.jspecify.annotations.NonNull; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchVariableSVInstruction.java b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchVariableSVInstruction.java index d2524682c6..c8a2d5e50d 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchVariableSVInstruction.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchVariableSVInstruction.java @@ -7,7 +7,7 @@ import org.key_project.logic.SyntaxElementCursor; import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; -import org.key_project.prover.rules.MatchConditions; +import org.key_project.prover.rules.instantiation.MatchConditions; import org.key_project.rusty.logic.op.sv.VariableSV; import org.jspecify.annotations.NonNull; diff --git a/keyext.rusty/src/test/java/org/key_project/rusty/rule/TestApplyTaclet.java b/keyext.rusty/src/test/java/org/key_project/rusty/rule/TestApplyTaclet.java index 8d0b627d54..437e5e4ae1 100644 --- a/keyext.rusty/src/test/java/org/key_project/rusty/rule/TestApplyTaclet.java +++ b/keyext.rusty/src/test/java/org/key_project/rusty/rule/TestApplyTaclet.java @@ -9,8 +9,8 @@ import org.key_project.logic.PosInTerm; import org.key_project.logic.Term; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.AssumesFormulaInstDirect; -import org.key_project.prover.rules.AssumesFormulaInstantiation; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect; +import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula;