RelationalSymbolicValue extends BinarySymbolicValue { @VisibleForTesting Set<RelationalSymbolicValue> transitiveRelations(Set<RelationalSymbolicValue> knownRelations) { Set<RelationalSymbolicValue> newRelations = new HashSet<>(); Deque<RelationalSymbolicValue> workList = new ArrayDeque<>(); int iterations = 0; workList.add(this); while (!workList.isEmpty()) { int relationSize = newRelations.size() * knownRelations.size(); if (relationSize > MAX_DEDUCED_RELATIONS || iterations > MAX_ITERATIONS) { throw new RelationalSymbolicValue.TransitiveRelationExceededException("Used relations: " + relationSize + ". Iterations " + iterations); } iterations++; RelationalSymbolicValue relation = workList.pop(); for (RelationalSymbolicValue knownRelation : knownRelations) { RelationalSymbolicValue r = relation.deduceTransitiveOrSimplified(knownRelation); if (r != null && !knownRelations.contains(r) && newRelations.add(r)) { workList.add(r); } } } return newRelations; } RelationalSymbolicValue(Kind kind); @VisibleForTesting  RelationalSymbolicValue(Kind kind, SymbolicValue leftOp, SymbolicValue rightOp); @Override List<ProgramState> setConstraint(ProgramState initialProgramState, BooleanConstraint booleanConstraint); @Override boolean equals(Object o); boolean isEquality(); @Override int hashCode(); @Override String toString(); @VisibleForTesting Kind kind();  }
@Test void test_all_transitive_relations_are_computed() throws Exception { RelationalSymbolicValue ab = relationalSV(Tree.Kind.EQUAL_TO, a, b); RelationalSymbolicValue bc = relationalSV(Tree.Kind.EQUAL_TO, b, c); RelationalSymbolicValue cd = relationalSV(Tree.Kind.EQUAL_TO, c, d); Set<RelationalSymbolicValue> transitive = ab.transitiveRelations(ImmutableSet.of(ab, bc, cd)); assertThat(transitive).containsOnly(relationalSV(Tree.Kind.EQUAL_TO, a, c), relationalSV(Tree.Kind.EQUAL_TO, b, d), relationalSV(Tree.Kind.EQUAL_TO, a, d)); }