diff --git a/CHANGELOG.md b/CHANGELOG.md index 312daff5..61a6935c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,7 @@ it releases that version ([RELEASING.md](https://github.com/energy-models/mathsp ## Upcoming version - fix(language): the case check reads a comparison on a relation as false where the relation has no row ([#949](https://github.com/energy-models/mathspec/pull/949)) +- fix(language): the case check reads each pair of relation columns as its own fact ([#950](https://github.com/energy-models/mathspec/pull/950)) - docs(language): a comparison on a relation is false where the relation has no row, whatever its operator ([#947](https://github.com/energy-models/mathspec/pull/947)) - docs(language): the relations page shows a variable masked by a bare relation, so it exists only at the pairs the relation lists ([#946](https://github.com/energy-models/mathspec/pull/946)) diff --git a/src/mathspec/_exclusivity.py b/src/mathspec/_exclusivity.py index efadad01..c822d09b 100644 --- a/src/mathspec/_exclusivity.py +++ b/src/mathspec/_exclusivity.py @@ -150,12 +150,14 @@ class Subject: A comparison on a relation is split by the column it reads, because two columns of one row hold two values. The relation's own subject, with no column, is whether it has a row, and every comparison on it reads that too. + A comparison of two columns is keyed by both relations and both columns, + in one order whichever side each is written on. """ kind: Literal['param', 'expression', 'dim', 'rank', 'relation', 'relation_pair', 'variable'] name: str qualifier: str | None = None - #: A rank's group columns: two positions by one relation into different columns are two subjects. + #: A rank's group columns, or a pair's two columns: a different column is a different subject. group: tuple[str, ...] = () def __str__(self) -> str: @@ -163,7 +165,8 @@ def __str__(self) -> str: within = f' within {self.qualifier}' if self.qualifier else '' return f'the position of {self.name}{within}' if self.kind == 'relation_pair': - return f'{self.name} vs {self.qualifier}' + column, other_column = self.group + return f'{self.name}[{column}] vs {self.qualifier}[{other_column}]' if self.kind == 'relation' and self.qualifier: return f'{self.name}[{self.qualifier}]' return self.name @@ -338,8 +341,9 @@ def _subject_of(node: TypedCondition) -> Subject: return Subject('relation', name) case RelationComparison(name=name, column=column): return Subject('relation', name, column) - case RelationPairComparison(name=name, other=other): - return Subject('relation_pair', name, other) + case RelationPairComparison(name=name, column=column, other=other, other_column=other_column): + (name, column), (other, other_column) = sorted([(name, column), (other, other_column)]) + return Subject('relation_pair', name, other, (column, other_column)) case ExpressionComparison(): return Subject('expression', 'a comparison of expressions') case CountComparison(): diff --git a/tests/test_exclusivity.py b/tests/test_exclusivity.py index 74360fcd..11c6af02 100644 --- a/tests/test_exclusivity.py +++ b/tests/test_exclusivity.py @@ -365,7 +365,7 @@ def test_a_relation_proved_apart_stays_apart_on_every_row(self, seed: int): Subject('relation', 'ends', 'bus0'), Subject('relation', 'ends', 'bus1'), ) - pair = Subject('relation_pair', 'ends', 'ends') + pair = Subject('relation_pair', 'ends', 'ends', ('bus0', 'bus1')) labels = ['north', 'south', 'east', 'west'] grid = [{row: Special.NULL, bus0: 'north', bus1: 'north', pair: True}] + [ {row: True, bus0: first, bus1: second, pair: first == second} @@ -457,7 +457,7 @@ def test_a_comparison_and_the_missing_row_are_apart(self, cases: dict[str, str], [ pytest.param( {'loop': 'ends[bus0] == ends[bus1]', 'north': "ends[bus0] == 'north'"}, - "where ends vs ends is equal, ends[bus0] is 'north'.", + "where ends[bus0] vs ends[bus1] is equal, ends[bus0] is 'north'.", id='a-column-value-says-the-row-exists', ), pytest.param({'listed': 'ends', 'again': 'ends'}, 'where ends has a row.', id='the-bare-name-says-it'), @@ -467,3 +467,27 @@ def test_a_row_both_cases_read_is_still_found(self, cases: dict[str, str], witne """The mirror: the row is there for both cases, and the witness says so once.""" [refusal] = refusals(to_spec(NETWORK), cases) assert witness in refusal + + +class TestAPairOfColumns: + """A comparison of two columns is one fact per pair of columns, whichever side each is written on.""" + + #: `ends` with a third column, so one relation offers more than one pair of columns. + THREE_ENDS: ClassVar[dict[str, Any]] = varied(NETWORK, **{'relations.ends.values.bus2': 'bus'}) + + def test_two_pairs_of_columns_are_two_facts(self): + """Both cases claim a line whose `bus0` and `bus1` are equal and whose `bus2` is another bus. + + The prover keyed a comparison of two columns by the two relation names + only. `ends[bus0] == ends[bus1]` and `ends[bus0] != ends[bus2]` read one + fact, so it proved the two cases apart. + """ + [refusal] = refusals( + to_spec(self.THREE_ENDS), {'a': 'ends[bus0] == ends[bus1]', 'b': 'ends[bus0] != ends[bus2]'} + ) + assert 'where ends[bus0] vs ends[bus1] is equal, ends[bus0] vs ends[bus2] is different.' in refusal + + def test_one_pair_written_both_ways_is_one_fact(self): + assert refusals(to_spec(NETWORK), {'a': 'ends[bus0] == ends[bus1]', 'b': 'ends[bus1] != ends[bus0]'}) == [], ( + 'a pair of columns with its sides swapped is the same pair' + )