RelationalSymbolicValue extends BinarySymbolicValue { RelationalSymbolicValue inverse() { return new RelationalSymbolicValue(kind.inverse(), leftOp, rightOp); } 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_direct_deduction() throws Exception { List<String> actual = new ArrayList<>(); for (Tree.Kind operator : operators) { actual.addAll(resolveRelationStateForAllKinds(relationalSV(operator, b, a), () -> relationToString(operator, a, b))); actual.addAll(resolveRelationStateForAllKinds(relationalSV(operator, a, b), () -> relationToString(operator, b, a))); } RelationalSymbolicValue eqAB = new RelationalSymbolicValue(RelationalSymbolicValue.Kind.METHOD_EQUALS, a, b); RelationalSymbolicValue eqBA = new RelationalSymbolicValue(RelationalSymbolicValue.Kind.METHOD_EQUALS, b, a); Stream.of(eqAB, eqBA, eqAB.inverse(), eqBA.inverse()).forEach(rel -> actual.addAll(resolveRelationStateForAllKinds(rel, rel::toString))); List<String> expected = IOUtils.readLines(getClass().getResourceAsStream("/relations/direct.txt")); assertThat(actual).isEqualTo(expected); }
@Test void test_transitive_deduction() throws Exception { List<String> actual = new ArrayList<>(); for (Tree.Kind r : operators) { RelationalSymbolicValue first = relationalSV(r, b, a); actual.addAll(combineWithAll(first, () -> relationToString(r, a, b))); } RelationalSymbolicValue eqAB = new RelationalSymbolicValue(RelationalSymbolicValue.Kind.METHOD_EQUALS, a, b); actual.addAll(combineWithAll(eqAB, eqAB::toString)); RelationalSymbolicValue neqAB = eqAB.inverse(); actual.addAll(combineWithAll(neqAB, neqAB::toString)); List<String> expected = IOUtils.readLines(getClass().getResourceAsStream("/relations/transitive.txt")); assertThat(actual).isEqualTo(expected); }