Skip to content

Commit 20b86e1

Browse files
denis-bogdanasdenis-bogdanas
authored
Java Backend: Minor refactorings (runtimeverification#434)
* Java Backend refactorings 1. Removed var `guarded` in proveRule 2. removed and old comment that essentially attempted to implement present --boundary-cells functionality. 3. renamed ConjunctiveFormula.removeBindings to ConjunctiveFormula.removeSubstitutionVars for clarity. * Java Backend refactoring: Replaced one instance of removeSubstitution() with retainSubstitutionVars() for clarity.
1 parent 0b7464e commit 20b86e1

4 files changed

Lines changed: 35 additions & 33 deletions

File tree

‎java-backend/src/main/java/org/kframework/backend/java/kil/ConstrainedTerm.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -199,7 +199,7 @@ public ConjunctiveFormula matchImplies(ConstrainedTerm matchRHSTerm, boolean exp
199199
constraint = constraint.orientSubstitution(matchRHSOnlyVars);
200200

201201
ConjunctiveFormula implicationLHS = data.constraint;
202-
ConjunctiveFormula implicationRHS = constraint.removeBindings(matchRHSOnlyVars);
202+
ConjunctiveFormula implicationRHS = constraint.removeSubstitutionVars(matchRHSOnlyVars);
203203
implicationRHS = (ConjunctiveFormula) implicationRHS.substituteAndEvaluate(implicationLHS.substitution(), context);
204204

205205
boolean implies = implicationLHS.implies(implicationRHS, matchRHSOnlyVars, formulaContext);

‎java-backend/src/main/java/org/kframework/backend/java/symbolic/ConjunctiveFormula.java‎

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -355,20 +355,34 @@ public boolean isUnknown() {
355355
}
356356

357357
/**
358-
* Removes specified variable bindings from this constraint.
358+
* Builds a new ConjunctiveFormula with the same content as original, but without the substitutions given as
359+
* argument.
359360
* <p>
360361
* Note: this method should only be used to garbage collect useless
361362
* bindings. It is called to remove all bindings of the rewrite rule
362363
* variables after building the rewrite result.
363364
*/
364-
public ConjunctiveFormula removeBindings(Set<Variable> variablesToRemove) {
365+
public ConjunctiveFormula removeSubstitutionVars(Set<Variable> variablesToRemove) {
365366
return ConjunctiveFormula.of(
366367
substitution.minusAll(variablesToRemove),
367368
equalities,
368369
disjunctions,
369370
global);
370371
}
371372

373+
/**
374+
* Builds a new ConjunctiveFormula with the same content as original, but retaining only the substitutions given as
375+
* argument.
376+
* <p>
377+
* E.g. new substitution = this substitution intersected with variablesToRetain.
378+
*/
379+
public ConjunctiveFormula retainSubstitutionVars(Set<Variable> variablesToRetain) {
380+
return ConjunctiveFormula.of(
381+
substitution.retainAll(variablesToRetain),
382+
equalities,
383+
disjunctions,
384+
global);
385+
}
372386

373387
public ConjunctiveFormula simplify() {
374388
return simplify(false, true, TermContext.builder(global).build(), false);
@@ -837,7 +851,7 @@ public boolean smartImplies(ConjunctiveFormula constraint) {
837851
constraint = constraint.orientSubstitution(rightOnlyVariables);
838852
839853
ConjunctiveFormula leftHandSide = data.constraint;
840-
ConjunctiveFormula rightHandSide = constraint.removeBindings(rightOnlyVariables);
854+
ConjunctiveFormula rightHandSide = constraint.removeSubstitutionVars(rightOnlyVariables);
841855
rightHandSide = (ConjunctiveFormula) rightHandSide.substitute(leftHandSide.substitution());
842856
if (!leftHandSide.implies(rightHandSide, rightOnlyVariables)) {
843857
return null;

‎java-backend/src/main/java/org/kframework/backend/java/symbolic/Substitution.java‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@
99
import java.util.Collection;
1010
import java.util.List;
1111
import java.util.Map;
12+
import java.util.Set;
13+
import java.util.stream.Collectors;
1214

1315

1416
public interface Substitution<K extends Term, V extends Term> extends Map<K, V> {
@@ -26,6 +28,14 @@ default Substitution<K, V> plusAll(Map<? extends K, ? extends V> substitution) {
2628
return result;
2729
}
2830

31+
/**
32+
* @return Intersection of this substitution and parameter substitution.
33+
*/
34+
default Substitution<K, V> retainAll(Set<? extends K> keysToRetain) {
35+
return ImmutableMapSubstitution.from(
36+
keySet().stream().filter(keysToRetain::contains).collect(Collectors.toMap(key -> key, this::get)));
37+
}
38+
2939
Substitution<K, V> minus(K key);
3040

3141
Substitution<K, V> minusAll(Collection<? extends K> keys);

‎java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java‎

Lines changed: 7 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -227,7 +227,7 @@ public List<ConstrainedTerm> fastComputeRewriteStep(ConstrainedTerm subject, boo
227227
}
228228
/* eliminate bindings of the substituted variables */
229229
ConjunctiveFormula constraint = matchResult.constraint;
230-
constraint = constraint.removeBindings(rule.variableSet());
230+
constraint = constraint.removeSubstitutionVars(rule.variableSet());
231231

232232
/* get fresh substitutions of rule variables */
233233
Map<Variable, Variable> renameSubst = Variable.rename(rule.variableSet());
@@ -433,7 +433,7 @@ public static ConstrainedTerm buildResult(
433433
Term term = rule.rightHandSide().substituteAndEvaluate(constraint.substitution(), context);
434434

435435
/* eliminate bindings of the substituted variables */
436-
constraint = constraint.removeBindings(substitutedVars);
436+
constraint = constraint.removeSubstitutionVars(substitutedVars);
437437

438438
/* get fresh substitutions of rule variables */
439439
Map<Variable, Variable> renameSubst = Variable.rename(rule.variableSet());
@@ -640,7 +640,6 @@ public List<ConstrainedTerm> proveRule(
640640

641641
visited.add(initialTerm);
642642
queue.add(initialTerm);
643-
boolean guarded = false;
644643
int step = 0;
645644

646645
if (prettyInitTerm != null) {
@@ -704,27 +703,8 @@ public List<ConstrainedTerm> proveRule(
704703
// Disabling on step 1 is useful for specs that match 1 full loop iteration.
705704
}
706705

707-
/* TODO(AndreiS): terminate the proof with failure based on the klabel _~>_
708-
List<Term> leftKContents = term.term().getCellContentsByName("<k>");
709-
List<Term> rightKContents = targetTerm.term().getCellContentsByName("<k>");
710-
// TODO(YilongL): the `get(0)` seems hacky
711-
if (leftKContents.size() == 1 && rightKContents.size() == 1) {
712-
Pair<Term, Variable> leftKPattern = KSequence.splitContentAndFrame(leftKContents.get(0));
713-
Pair<Term, Variable> rightKPattern = KSequence.splitContentAndFrame(rightKContents.get(0));
714-
if (leftKPattern.getRight() != null && rightKPattern.getRight() != null
715-
&& leftKPattern.getRight().equals(rightKPattern.getRight())) {
716-
BoolToken matchable = MetaK.matchable(
717-
leftKPattern.getLeft(),
718-
rightKPattern.getLeft(),
719-
term.termContext());
720-
if (matchable != null && matchable.booleanValue()) {
721-
proofResults.add(term);
722-
continue;
723-
}
724-
}
725-
}*/
726-
727-
if (guarded) {
706+
//Attempt to apply a spec rule, except on first step.
707+
if (step > 1) {
728708
ConstrainedTerm result = applySpecRules(term, specRules);
729709
if (result != null) {
730710
nextStepLogEnabled = true;
@@ -745,6 +725,7 @@ public List<ConstrainedTerm> proveRule(
745725
}
746726
}
747727

728+
//Apply a regular rule
748729
List<ConstrainedTerm> results = fastComputeRewriteStep(term, false, true, true, step,
749730
initialTerm);
750731
if (results.isEmpty()) {
@@ -775,13 +756,11 @@ public List<ConstrainedTerm> proveRule(
775756
}
776757
}
777758
}
759+
//Build results of regular rule application
778760
for (ConstrainedTerm cterm : results) {
779761
ConstrainedTerm result = new ConstrainedTerm(
780762
cterm.term(),
781-
cterm.constraint().removeBindings(
782-
Sets.difference(
783-
cterm.constraint().substitution().keySet(),
784-
initialTerm.variableSet())),
763+
cterm.constraint().retainSubstitutionVars(initialTerm.variableSet()),
785764
cterm.termContext());
786765
if (visited.add(result)) {
787766
nextQueue.add(result);
@@ -817,7 +796,6 @@ public List<ConstrainedTerm> proveRule(
817796
queue = nextQueue;
818797
nextQueue = temp;
819798
nextQueue.clear();
820-
guarded = true;
821799

822800
global.javaExecutionOptions.log = originalLog;
823801
}

0 commit comments

Comments
 (0)