diff --git a/docs/about/limits.md b/docs/about/limits.md index 776cddf3..c5742346 100644 --- a/docs/about/limits.md +++ b/docs/about/limits.md @@ -154,17 +154,17 @@ lets an engine build the model one chunk of rows at a time. What has been asked for and refused, with the reason and what to write instead. That another tool has a feature is not by itself a reason to add it. -| Request | Why refused | Instead | -| ------------------------------------------------------------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| Resampling, clustering, file IO, unit conversion | not math | do it in data preparation, and pass a parameter | -| Unit checking at load | a `unit: MW` on a parameter is a claim that nothing checks against the column. A clean pass would only mean that no two annotated operands disagreed. It would also need a grammar of units that the language then has to maintain ([#125](https://github.com/fluxopt/lpspec/issues/125)) | convert to one unit system in data preparation, and name it in the `description:` | -| Array operations such as `merge` and `reindex` | there is no end to them | data preparation | -| Helpers for one domain, such as `reduce_carrier_dim` | writes one field's vocabulary into the language | a component library of macros over the operators that exist | -| A vocabulary for tracked metrics: `impacts:`, `effects:`, a `costs` axis | a named expression already does this | an `impact` dimension and one named expression. Cap it with a constraint, whose dual is the shadow price; weight it in the objective; read it back after the solve ([#124](https://github.com/fluxopt/lpspec/issues/124)) | -| `**` with a variable in the base or the exponent | the exponent would decide the degree, and `to_spec` reads no data. `p ** n` is linear at `n = 1`, quadratic at `n = 2`, and refused at `n = 3` | `x * x` for a square. `**` over parameters and numbers is allowed ([#1175](https://github.com/fluxopt/lpspec/issues/1175)) | -| Normalisation, `x / sum(x)` | dividing by a variable is not a polynomial, and no solver takes it | write the ratio as a constraint, or fix the denominator | -| An `if`, a loop, or declarations that depend on the data | `to_spec` could no longer read the file without the data | `where:` masks and `dims:` dimensions. A tool may loop over models | -| A Python API for building models | the model is the file you review and diff | YAML, or a `dict` with the same keys ([below](#composition-component-libraries)) | +| Request | Why refused | Instead | +| ------------------------------------------------------------------------ | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Resampling, clustering, file IO, unit conversion | not math | do it in data preparation, and pass a parameter | +| Unit checking at load | a `unit: MW` on a parameter is a claim that nothing checks against the column. A clean pass would only mean that no two annotated operands disagreed. It would also need a grammar of units that the language then has to maintain ([#125](https://github.com/fluxopt/lpspec/issues/125)). A range is different: `assumptions:` states one, and the engine checks it against every row | convert to one unit system in data preparation, and name it in the `description:` | +| Array operations such as `merge` and `reindex` | there is no end to them | data preparation | +| Helpers for one domain, such as `reduce_carrier_dim` | writes one field's vocabulary into the language | a component library of macros over the operators that exist | +| A vocabulary for tracked metrics: `impacts:`, `effects:`, a `costs` axis | a named expression already does this | an `impact` dimension and one named expression. Cap it with a constraint, whose dual is the shadow price; weight it in the objective; read it back after the solve ([#124](https://github.com/fluxopt/lpspec/issues/124)) | +| `**` with a variable in the base or the exponent | the exponent would decide the degree, and `to_spec` reads no data. `p ** n` is linear at `n = 1`, quadratic at `n = 2`, and refused at `n = 3` | `x * x` for a square. `**` over parameters and numbers is allowed ([#1175](https://github.com/fluxopt/lpspec/issues/1175)) | +| Normalisation, `x / sum(x)` | dividing by a variable is not a polynomial, and no solver takes it | write the ratio as a constraint, or fix the denominator | +| An `if`, a loop, or declarations that depend on the data | `to_spec` could no longer read the file without the data | `where:` masks and `dims:` dimensions. A tool may loop over models | +| A Python API for building models | the model is the file you review and diff | YAML, or a `dict` with the same keys ([below](#composition-component-libraries)) | ## Composition (component libraries) diff --git a/docs/examples/commitment.md b/docs/examples/commitment.md index 915ad9c2..244c31bb 100644 --- a/docs/examples/commitment.md +++ b/docs/examples/commitment.md @@ -83,6 +83,11 @@ constraints: dispatch - shift(dispatch, along=snapshot, offset=1, edge=0) <= ramp_limit * previous_status + start_up_limit * (1 - previous_status) +assumptions: + floor_below_capacity: + description: a floor above the capacity leaves `upper` and `lower` no output to agree on + holds: "min_output <= capacity" + objective: sense: minimize expression: sum(dispatch * cost) @@ -182,6 +187,14 @@ $`\mathrm{pos}(t)`$ denotes where index $`t`$ sits along its dimension's own ord ```math \mathit{status}_{t,g} \in \{0, 1\} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} ``` + +#### Assumptions + +**`floor_below_capacity`** + +```math +\mathrm{min\_output}_{g} \le \mathrm{capacity}_{g} \qquad \forall\, g \in \mathcal{G} +``` Regenerate with `pixi run python -m tools.gallery`. diff --git a/docs/reference/language/declarations.md b/docs/reference/language/declarations.md index 9b604b55..cf7ca1d9 100644 --- a/docs/reference/language/declarations.md +++ b/docs/reference/language/declarations.md @@ -5,7 +5,8 @@ SPDX-License-Identifier: CC-BY-4.0 # Parameters, variables, constraints and the objective -These four blocks carry the math. Each takes an optional `description:`. +These four blocks carry the math, and a fifth, `assumptions`, says what the +math takes for granted about its data. Each takes an optional `description:`. A description is free text with no length limit. The parser throws a `#` comment away, but keeps a description, so a renderer or a checker can print it. The @@ -210,3 +211,68 @@ different models. A second objective cannot be written, because the schema holds one block. To pursue several goals, weight them into one expression. + +## `assumptions` + +An assumption is a claim about the data: a predicate that every coordinate +has to satisfy before the model is built. The language decides nothing about +the numbers, so the tool that binds the data checks each assumption and refuses +the data where one does not hold. The [typeset](../typeset.md) document prints +every assumption under its own heading, so the math a reader checks carries what +the model assumes of its inputs. + +```yaml +dimensions: + generator: { dtype: str } +parameters: + p_min: { dims: [generator] } + p_max: { dims: [generator] } + efficiency: { dims: [generator] } +variables: + p: { dims: [generator], bounds: { lower: p_min, upper: p_max } } +assumptions: + efficiency_is_a_fraction: "efficiency > 0 AND efficiency <= 1" + bounds_do_not_cross: + holds: "p_min <= p_max" + where: "p_min" + description: a unit with no minimum is unconstrained below +``` + +```math +\mathrm{efficiency}_{g} > 0 \wedge \mathrm{efficiency}_{g} \le 1 \qquad \forall\, g \in \mathcal{G} +``` + +```math +\mathrm{p}^{\mathrm{min}}_{g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} \,:\, \mathrm{p}^{\mathrm{min}}_{g} \text{ is defined} +``` + +| Field | | | +| ------------- | ------------------------------------------------------------------------------------------------------------------------------------ | -------------- | +| `holds` | required. A [`where` string](expressions.md#where-strings) over parameters, dimensions and lookups. A bare string is read as `holds` | | +| `where` | which coordinates are checked, in the same grammar | default `null` | +| `description` | free text | default `null` | + +Three rules say what an assumption means: + +- **It holds at every coordinate of its frame.** The frame is the product of + every dimension that `holds` and `where` name, so `p_min <= p_max` over one + dimension is checked once per generator, and `budget > 0` over none is + checked once. There is no `dims:` to declare, because a predicate widens + nothing. +- **A missing row reads as false**, as it does in every `where` + ([absence](absence.md#what-creates-absence)). So `efficiency > 0` refuses a + generator whose row is missing. Where a parameter is supplied only for the + units it applies to, say so in `where:`, as `bounds_do_not_cross` does: the + assumption is checked where `p_min` is defined and nowhere else. +- **Two parameters may be compared.** `p_min <= p_max` reads the two coordinate + by coordinate, the narrower one at every coordinate of the wider. Both are + numbers, or both share a dtype. A number against a label is refused. + +A predicate that names a variable is refused, because an assumption is about +the data and a variable is what the solver decides from it. State a rule about +a decision as a constraint. A predicate that folds to `True` or `False` is +refused too: the first assumes nothing, and the second admits no data. + +A `piecewise:` block assumes things of its breakpoints that no file writes, +such as a strictly increasing x-axis. Those print under the same heading, +labelled by the block ([what a curve assumes](piecewise.md#what-a-curve-assumes)). diff --git a/docs/reference/language/expressions.md b/docs/reference/language/expressions.md index d68f0b1e..ccfe2c60 100644 --- a/docs/reference/language/expressions.md +++ b/docs/reference/language/expressions.md @@ -175,6 +175,7 @@ QUOTED ::= "'" chars "'" | '"' chars '"' | `name OP value` | parameter | Element-wise, and a null compares false. The right-hand side is a literal, or a bare name read as a string label | | `name OP value` | dimension | A filter on the frame's own coordinate column | | `name OP value`, `name.col OP value` | relation | A filter on a value column of a keyed relation, read at its key, so the key's dimensions have to be in the frame. Name the column where the key determines several. A null compares false | +| `name OP name` | two parameters | Coordinate by coordinate, the narrower one read at every coordinate of the wider. Both are numbers, or both share a dtype. A null on either side compares false | | `name OP name`, `name.a OP name.b` | two relation columns | Legal only where both relations are keyed over the same dimensions and both columns are over one dimension. `ends.bus0 != ends.bus1` excludes a self-loop | | `expression OP expression` | arithmetic over parameters | Coordinate by coordinate, over every dimension either side carries. A macro and a named expression expand as in an expression, and every operator keeps its rule, so a `shift` names its `edge=`. A side with no value at a coordinate compares false | | `position(name) OP i` | dimension | Where the row sits along the dimension's own order. `0` is first, and a negative number counts from the end | @@ -213,12 +214,13 @@ so `node >= 'b'` means the same however the nodes were listed. A label the dimension does not carry compares equal to nothing, so the mask is false there rather than an error. -Comparing two parameters, or two dimensions, is not in the language. Precompute a -boolean parameter instead. Two relation columns are the exception, where the two -relations are keyed over the same dimensions and the two columns are over one -dimension. Keyed alike, they are two columns of one key table, so the comparison -filters that table rather than joining two. Over one dimension they draw from one -label set, so a match is possible at all. +Two parameters compare coordinate by coordinate, as `p_min <= p_max` does. +Two relation columns compare where the two relations are keyed over the same +dimensions and the two columns are over one dimension. Keyed alike, they are +two columns of one key table, so the comparison filters that table rather than +joining two. Over one dimension they draw from one label set, so a match is +possible at all. Comparing two dimensions is not in the language. Precompute a +boolean parameter instead. ### Arithmetic in a comparison diff --git a/docs/reference/language/file.md b/docs/reference/language/file.md index 68b3aec9..c8057578 100644 --- a/docs/reference/language/file.md +++ b/docs/reference/language/file.md @@ -5,8 +5,8 @@ SPDX-License-Identifier: CC-BY-4.0 # File shape -A model file is a YAML mapping with **ten declaration keys**, plus `version` -and `description`. Any subset of the ten is accepted. +A model file is a YAML mapping with **eleven declaration keys**, plus `version` +and `description`. Any subset of the eleven is accepted. | Key | | | ------------- | ------------------------------------------------------------------------------------------------------------------- | @@ -20,6 +20,7 @@ and `description`. Any subset of the ten is accepted. | `macros` | templates that take arguments ([macros](expressions.md#macros)) | | `piecewise` | piecewise-linear curves ([piecewise](piecewise.md)) | | `sos` | special-ordered sets ([sos](piecewise.md#sos)) | +| `assumptions` | what the model assumes of its data ([assumptions](declarations.md#assumptions)) | A file with no `objective` is a **feasibility problem**: it asks whether the constraints can all be met. It loads and solves like any other model, and the diff --git a/docs/reference/language/index.md b/docs/reference/language/index.md index c081f237..e93795ce 100644 --- a/docs/reference/language/index.md +++ b/docs/reference/language/index.md @@ -46,7 +46,7 @@ message that names the fix. These ten rules are what it checks. | # | Rule | | | --- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------- | -| 1 | A file has ten declaration keys, plus `version` and `description`. A key the schema does not know is refused, with the nearest valid key named: `boundz` → `bounds`. | [File shape](file.md) | +| 1 | A file has eleven declaration keys, plus `version` and `description`. A key the schema does not know is refused, with the nearest valid key named: `boundz` → `bounds`. | [File shape](file.md) | | 2 | Everything that can be checked without data is checked when the file loads. | [Errors](errors.md) | | 3 | Every name is declared once. A parameter and a dimension both called `snapshot` is refused, and the message names both lines. | [Names](expressions.md#name-resolution) | | 4 | Where a name may stand depends on what it is. A dimension may follow `over=` or `along=`, and may not be multiplied: `dispatch * snapshot` is refused, because `snapshot` is an axis and not a column of numbers. | [Names](expressions.md#name-resolution) | @@ -63,7 +63,7 @@ message that names the fix. These ten rules are what it checks. | ----------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------- | | [File shape](file.md) | the ten keys, `version`, `description`, and how the YAML is read | | [Dimensions and relations](dimensions.md) | the axes, and the maps from one axis onto another | -| [Parameters, variables, constraints and the objective](declarations.md) | the four blocks that carry the math | +| [Parameters, variables, constraints and the objective](declarations.md) | the four blocks that carry the math, and the assumptions the data is held to | | [Expressions](expressions.md) | the arithmetic grammar and the `where` grammar, where each kind of name may stand, and how dimensions combine | | [Reported expressions](reported.md) | named quantities that no constraint or objective uses, which you read back after a solve | | [Operators](operators.md) | `sum`, `sum_back`, `at` and `shift` | diff --git a/docs/reference/language/piecewise.md b/docs/reference/language/piecewise.md index 305e15e8..2e652402 100644 --- a/docs/reference/language/piecewise.md +++ b/docs/reference/language/piecewise.md @@ -183,6 +183,25 @@ stating lines rather than weights: along the end segments. They are the same rows that `linopy`'s own `lp` method emits. +### What a curve assumes + +A method assumes things of the breakpoints that no file writes. `convex` and +`lp` sort by the first link's values, so those have to increase along `over` +within each curve, and each method is exact only for the shape named above. +`lp` needs at least two breakpoints per curve, and a `points:` mask has to +admit one consecutive run. The engine checks each of these when the data +binds. The [typeset](../typeset.md) document prints them under the +[assumptions](declarations.md#assumptions), labelled by the block, beside the +assumptions the file writes itself: + +```math +\mathrm{bp\_x}_{g,b - 1} < \mathrm{bp\_x}_{g,b} \qquad \forall\, g \in \mathcal{G},\ b \in \mathcal{B} +``` + +```math +\mathrm{bp\_y}_{g,b} \text{ is a convex function of } \mathrm{bp\_x}_{g,b} \text{ along } b \qquad \forall\, g \in \mathcal{G} +``` + ### Writing the curve out by hand `links:` is a list, so the number of expressions a block ties is written in the diff --git a/docs/reference/language/reading.md b/docs/reference/language/reading.md index dd213065..cc61a10f 100644 --- a/docs/reference/language/reading.md +++ b/docs/reference/language/reading.md @@ -94,6 +94,11 @@ parameters it is about. The engine, which has the numbers, runs the check, and says how a parameter is filled, and `None` means the engine binds it from its data. +`program.assumptions` keeps each `assumptions:` entry as two masks, `holds` and +`where`, under the name the file wrote. The engine checks `holds` at every +coordinate of the product of the dimensions the two masks name that `where` +admits, and `assumption_message` gives it the sentence to raise. + ## Nodes and masks You never build a node yourself. The node classes are exported so that you can diff --git a/docs/reference/notation.md b/docs/reference/notation.md index b59c3708..42b64155 100644 --- a/docs/reference/notation.md +++ b/docs/reference/notation.md @@ -5,30 +5,27 @@ SPDX-License-Identifier: CC-BY-4.0 # Every construct, as math -[Typesetting](typeset.md) prints a model the way a paper prints it. This page -prints _all_ of it: every construct the language has, beside the math the -typesetter gives it, so the notation can be read as the one system it has to -be — two constructs that mean different things looking different, a symbol -introduced where it is defined and used where it is meant. - -It is generated by `pixi run python -m tools.notation`, almost all of it from one -model: -[`tests/typesetting/golden/model.yaml`](https://github.com/energy-models/math-spec/blob/main/tests/typesetting/golden/model.yaml), -which is not a sensible optimisation problem and is not trying to be: it is the -one file that carries every construct at once, and three checks in -`tests/typesetting/test_typeset.py` hold it to the language — every operator a format -spells, every node kind the parsers produce, every line of the walk. So _every_ -here is asserted rather than promised, and a construct added to the language -arrives on this page or CI goes red. The curves are the exception, one real -model per `method:`, for the reason the section gives. - -Two things this page is not. It is not the operator reference — what each -operator _does_ is [Operators](language/operators.md), which renders the same -math one row per call shape. And it is not a tutorial: the models under -`examples/` are the ones written to be read. +Every construct the language has is printed here, beside the math the +typesetter gives it. Look up the notation for one construct, or read the whole +notation at once: two constructs that mean different things print differently, +and every symbol below appears first in the legend that defines it. + +The page is generated by `pixi run python -m tools.notation`, almost all of it +from one model, +[`tests/typesetting/golden/model.yaml`](https://github.com/energy-models/math-spec/blob/main/tests/typesetting/golden/model.yaml). +That model is not a sensible optimisation problem. It is the one file that +carries every construct at once, and tests in `tests/typesetting/` hold it to +the language: every operator a format spells, every kind of node the parsers +produce, and every line of the code that walks them. So a construct added to the +language either arrives on this page, or CI fails. The curves are the exception, +and use one real model per `method:`. + +For what an operator _does_, read [Operators](language/operators.md), which +prints the same math with one row per call. For models written to be read, start +with the [examples](../examples/index.md). The symbols below are **derived** from the names in the file, which is what a -model prints with no setup, so you see $\mathrm{load}_{t}$ rather than $\ell_t$. +model prints with no setup, so you see $\mathit{load}_{t}$ rather than $\ell_t$. A [symbol table](typeset.md#symbol-tables) replaces every symbol, and changes nothing else on this page. @@ -45,6 +42,7 @@ dimensions: zone: { dtype: str } season: { dtype: str } technology: { dtype: str } + bp: { dtype: int } relations: gen_bus: { columns: [generator, bus], key: generator } @@ -70,6 +68,10 @@ parameters: lead: { dims: [generator], dtype: int } budget: { dims: [] } # scalar: the legend says so rather than printing an empty product growth: { dims: [] } # the base of a power; the exponent is `lead`, a column + bp_x: { dims: [generator, bp] } # a curve's breakpoints, one curve per generator + bp_y: { dims: [generator, bp] } + fuel_bp: { dims: [bp] } # a second curve's breakpoints, one curve for every generator + heat_bp: { dims: [bp] } ``` #### Sets @@ -82,6 +84,7 @@ parameters: | $`\mathcal{Z}`$ | index $`z`$ — `zone` with $`\mathrm{zone\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{area\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{gen\_zone}: \mathcal{G} \times \mathcal{T} \to \mathcal{Z}`$ | | $`\mathcal{S}`$ | index $`s`$ — `season` with $`\mathrm{season\_of}: \mathcal{T} \to \mathcal{S}`$ | | $`\mathcal{E}`$ | index $`e`$ — `technology` with $`\mathrm{gen\_tech}: \mathcal{G} \to \mathcal{E},\ \mathrm{gen\_bt}: \mathcal{G} \to \mathcal{B} \times \mathcal{E}`$ | +| $`\mathcal{A}`$ | index $`a`$ — `bp` | #### Parameters @@ -99,6 +102,13 @@ parameters: | $`\mathrm{lead}`$ | `lead` over $`\mathcal{G}`$ | | $`\mathrm{budget}`$ | `budget` (scalar) | | $`\mathrm{growth}`$ | `growth` (scalar) | +| $`\mathrm{bp\_x}`$ | `bp_x` over $`\mathcal{G} \times \mathcal{A}`$ | +| $`\mathrm{bp\_y}`$ | `bp_y` over $`\mathcal{G} \times \mathcal{A}`$ | +| $`\mathrm{fuel\_bp}`$ | `fuel_bp` over $`\mathcal{A}`$ | +| $`\mathrm{heat}^{\mathrm{bp}}`$ | `heat_bp` over $`\mathcal{A}`$ | +| $`\mathrm{cost}^{\mathrm{curve,points}}`$ | `cost_curve_points` over $`\mathcal{G} \times \mathcal{A}`$ — where 'bp\_x' has a row, and so where the curve runs | +| $`\mathrm{cost}^{\mathrm{curve,starts}}`$ | `cost_curve_starts` over $`\mathcal{G} \times \mathcal{A}`$ — the first breakpoint of each curve | +| $`\mathrm{cost}^{\mathrm{curve,ends}}`$ | `cost_curve_ends` over $`\mathcal{G} \times \mathcal{A}`$ — the last breakpoint of each curve | #### Variables @@ -114,6 +124,8 @@ parameters: | $`\mathit{reserve}`$ | `reserve` (scalar) | | $`\mathit{headroom}`$ | `headroom` (scalar) | | $`\mathit{weight}`$ | `weight` over $`\mathcal{T} \times \mathcal{G}`$ | +| $`\mathit{op\_cost}`$ | `op_cost` over $`\mathcal{T} \times \mathcal{G}`$ | +| $`\mathit{heat}`$ | `heat` over $`\mathcal{T} \times \mathcal{G}`$ | #### Definitions @@ -989,6 +1001,136 @@ weight: 0 \le \mathit{weight}_{t,g} \le 1 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} ``` +#### `op_cost` + +what a curve bounds below + +```yaml +op_cost: + dims: [snapshot, generator] + bounds: { lower: 0 } +``` + +```math +\mathit{op\_cost}_{t,g} \ge 0 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} +``` + +#### `heat` + +what a second curve bounds above + +```yaml +heat: + dims: [snapshot, generator] + bounds: { lower: 0 } +``` + +```math +\mathit{heat}_{t,g} \ge 0 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} +``` + +### Assumptions + +#### `capacity_is_nonnegative` + +one comparison, so the line aligns on its relation + +```yaml +capacity_is_nonnegative: p_max >= 0 +``` + +```math +\mathrm{p}^{\mathrm{max}}_{g} \ge 0 \qquad \forall\, g \in \mathcal{G} +``` + +#### `bounds_are_ordered` + +two parameters compared coordinate by coordinate, checked where the narrower one is defined + +```yaml +bounds_are_ordered: + holds: "p_min <= p_max" + where: "p_min" +``` + +```math +\mathrm{p}^{\mathrm{min}}_{g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} \,:\, \mathrm{p}^{\mathrm{min}}_{g} \text{ is defined} +``` + +#### `budget_is_positive` + +a scalar, so no quantifier + +```yaml +budget_is_positive: budget > 0 +``` + +```math +\mathrm{budget} > 0 +``` + +#### `flexible_units_are_cheap` + +a compound predicate, which no one relation aligns + +```yaml +flexible_units_are_cheap: "NOT is_flexible OR cost <= budget" +``` + +```math +\neg \mathrm{is\_flexible}_{g} \vee \mathrm{cost}_{g} \le \mathrm{budget} \qquad \forall\, g \in \mathcal{G} +``` + +#### `floor_is_half_the_capacity` + +arithmetic on a side, which reads as an expression does + +```yaml +floor_is_half_the_capacity: "p_min <= 0.5 * p_max" +``` + +```math +\mathrm{p}^{\mathrm{min}}_{g} \le 0.5 \cdot \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} +``` + +#### `load_ramps_within_the_zone_cap` + +a translation under a comparison names its edge, and the where keeps the vacated row out + +```yaml +load_ramps_within_the_zone_cap: + holds: "load - shift(load, along=snapshot, offset=1, edge=0) <= at(zone_cap, by=zone_of)" + where: "position(snapshot) > 0" +``` + +```math +\mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} \le \mathrm{zone\_cap}_{\mathrm{zone\_of}(b)} \qquad \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{pos}(t) > 0 +``` + +#### `fleet_covers_the_budget` + +a reduction on a side, so the frame is what is left + +```yaml +fleet_covers_the_budget: "sum(p_max, over=generator) >= budget" +``` + +```math +\sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} \ge \mathrm{budget} +``` + +#### `cheap_when_spent` + +an expressions: entry on a side, read by the name the file gave it + +```yaml +cheap_when_spent: "spend_cap > 0 OR NOT is_flexible" +``` + +```math +\mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} \qquad \forall\, g \in \mathcal{G} +``` + ### Curves, as what they expand to A curve is sugar: what prints is the formulation it expands to, which is the math the solver receives. One row per `method:`, each from the model named under it, so the symbols in this section are that model's. @@ -1129,6 +1271,14 @@ cost_curve: 0 \le \lambda_{t,g,b} \le 1 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ b \in \mathcal{B} ``` +```math +\mathrm{x}_{g,b - 1} < \mathrm{x}_{g,b} \qquad \forall\, g \in \mathcal{G},\ b \in \mathcal{B} +``` + +```math +\mathrm{y}_{g,b} \text{ is a convex or concave function of } \mathrm{x}_{g,b} \text{ along } b \qquad \forall\, g \in \mathcal{G} +``` + #### `cost_curve` **`method: lp`** — no weights at all — one row per segment line, plus the two rows holding the domain, in `examples/piecewise_lp.yaml`. @@ -1164,6 +1314,18 @@ cost_curve: \mathit{dispatch}_{t,g} \le \mathrm{x}_{g,b} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ b \in \mathcal{B} \,:\, \mathrm{pos}(b) = \lvert \mathcal{B} \rvert - 1 ``` +```math +\mathrm{x}_{g,b - 1} < \mathrm{x}_{g,b} \qquad \forall\, g \in \mathcal{G},\ b \in \mathcal{B} +``` + +```math +\mathrm{y}_{g,b} \text{ is a convex function of } \mathrm{x}_{g,b} \text{ along } b \qquad \forall\, g \in \mathcal{G} +``` + +```math +\lvert \mathcal{B} \rvert \ge 2 +``` + ### Sets carried to the solver #### `adjacent` diff --git a/docs/reference/typeset.md b/docs/reference/typeset.md index 41f2047b..43e168c7 100644 --- a/docs/reference/typeset.md +++ b/docs/reference/typeset.md @@ -74,6 +74,9 @@ a flag. symbol table touches it. - A `piecewise:` block prints as the variables and constraints it expands into, because the expansion is the math the solver receives. +- An `assumptions:` block prints under its own heading, after the variable + domains, and so does what each `piecewise:` block assumes of its breakpoints + ([assumptions](language/declarations.md#assumptions)). - Inlining reaches only an expression that the math reads. A `cases:` block has no single body to substitute, and a [reported entry](language/reported.md) is read by nothing, so both keep their definition line under either setting. @@ -86,7 +89,7 @@ a flag. ## Printing one declaration on its own `typeset_declaration` returns the line the document prints for one named -expression, constraint or variable, with its quantifier and without a document, +expression, constraint, assumption or variable, with its quantifier and without a document, a label, a number or math delimiters. Use it for a docstring, a table cell or a comment beside the value it computes: @@ -114,7 +117,7 @@ A line on its own has no _Definitions_ section beside it, so the plain named expressions it uses are substituted unless you say otherwise. A cased expression prints by symbol, and a second call with its name prints its block. -A name that is none of the three kinds is refused with the near miss. A name that +A name that is none of the four kinds is refused with the near miss. A name that is both a constraint and a variable is refused too, because one line can print only one of them. Constraints sit outside the [flat namespace](language/expressions.md#name-resolution), so a model may use one diff --git a/examples/commitment.yaml b/examples/commitment.yaml index 770ba19e..ed805d9d 100644 --- a/examples/commitment.yaml +++ b/examples/commitment.yaml @@ -67,6 +67,11 @@ constraints: dispatch - shift(dispatch, along=snapshot, offset=1, edge=0) <= ramp_limit * previous_status + start_up_limit * (1 - previous_status) +assumptions: + floor_below_capacity: + description: a floor above the capacity leaves `upper` and `lower` no output to agree on + holds: "min_output <= capacity" + objective: sense: minimize expression: sum(dispatch * cost) diff --git a/schema/math-spec.schema.json b/schema/math-spec.schema.json index ae5c8378..0cbf8b1a 100644 --- a/schema/math-spec.schema.json +++ b/schema/math-spec.schema.json @@ -1,5 +1,51 @@ { "$defs": { + "AssumptionBlock": { + "anyOf": [ + { + "additionalProperties": false, + "description": "What the model assumes of its data: a predicate every coordinate has to satisfy.\n\nWritten in YAML as a bare where string, or as a mapping once it carries a\n``where:`` or a ``description:``, and serialised back to whichever form it\nwas written in::\n\n assumptions:\n efficiency_is_a_fraction: \"efficiency > 0 AND efficiency <= 1\"\n bounds_do_not_cross:\n holds: \"p_min <= p_max\"\n where: \"p_min\"\n description: a unit with no minimum is unconstrained below\n\nThe language decides nothing about the numbers, so the consumer binding\nthe data checks it, and refuses the data where it does not hold.", + "properties": { + "description": { + "anyOf": [ + { + "type": "string" + }, + { + "type": "null" + } + ], + "default": null, + "title": "Description" + }, + "holds": { + "title": "Holds", + "type": "string" + }, + "where": { + "anyOf": [ + { + "type": "string" + }, + { + "type": "null" + } + ], + "default": null, + "title": "Where" + } + }, + "required": [ + "holds" + ], + "title": "AssumptionBlock", + "type": "object" + }, + { + "type": "string" + } + ] + }, "BoundsBlock": { "additionalProperties": false, "description": "Variable bounds \u2014 each side is a number or parameter name.\n\nAn omitted bound leaves the variable unbounded on that side, not\nimplicitly non-negative.", @@ -630,8 +676,16 @@ }, "$schema": "https://json-schema.org/draft/2020-12/schema", "additionalProperties": false, - "description": "The declared math \u2014 one YAML file, or one dict, validated. Nothing here has seen data.\n\nA ``Spec`` that exists has passed the whole language: constructing one by\nany route \u2014 ``to_spec``, :meth:`model_validate`, the constructor \u2014 runs\nevery load-time check, expansion and expression pass included, and raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\nHolding one is the proof, so nothing downstream checks it again.\n\nThe API is the ten declaration sections plus ``version`` and\n``description``, and two ways back out: :meth:`to_dict` for the model as\ndata, :meth:`to_yaml` for the file a reviewer reads. Everything else on\nthis class is pydantic's, not a contract this package keeps.", + "description": "The declared math \u2014 one YAML file, or one dict, validated. Nothing here has seen data.\n\nA ``Spec`` that exists has passed the whole language: constructing one by\nany route \u2014 ``to_spec``, :meth:`model_validate`, the constructor \u2014 runs\nevery load-time check, expansion and expression pass included, and raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\nHolding one is the proof, so nothing downstream checks it again.\n\nThe API is the eleven declaration sections plus ``version`` and\n``description``, and two ways back out: :meth:`to_dict` for the model as\ndata, :meth:`to_yaml` for the file a reviewer reads. Everything else on\nthis class is pydantic's, not a contract this package keeps.", "properties": { + "assumptions": { + "additionalProperties": { + "$ref": "#/$defs/AssumptionBlock" + }, + "default": {}, + "title": "Assumptions", + "type": "object" + }, "constraints": { "additionalProperties": { "$ref": "#/$defs/ConstraintBlock" diff --git a/src/math_spec/dimensions.py b/src/math_spec/dimensions.py index ea7e4701..301450b8 100644 --- a/src/math_spec/dimensions.py +++ b/src/math_spec/dimensions.py @@ -47,6 +47,7 @@ Mask, ParameterComparisonNode, ParameterDefinedNode, + ParameterPairComparisonNode, RelationComparisonNode, RelationDefinedNode, RelationPairComparisonNode, @@ -522,7 +523,7 @@ def _check_where_dims( if not (outside := sorted(Mask(atom).dims - frame)): continue match atom: - case ParameterDefinedNode() | ParameterComparisonNode(): + case ParameterDefinedNode() | ParameterComparisonNode() | ParameterPairComparisonNode(): leaf = f"where-parameter '{atom.name}'" case VariableDefinedNode(): leaf = f"where-variable '{atom.name}'" diff --git a/src/math_spec/exclusivity.py b/src/math_spec/exclusivity.py index 6ee9a7eb..73ef34c7 100644 --- a/src/math_spec/exclusivity.py +++ b/src/math_spec/exclusivity.py @@ -33,6 +33,7 @@ OrNode, ParameterComparisonNode, ParameterDefinedNode, + ParameterPairComparisonNode, RelationComparisonNode, RelationDefinedNode, RelationPairComparisonNode, @@ -138,7 +139,7 @@ class Subject: a rank is further split by the ``by=`` relation it is counted within. """ - kind: Literal['param', 'expression', 'dim', 'rank', 'relation', 'relation_pair', 'variable'] + kind: Literal['param', 'param_pair', '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. @@ -148,7 +149,7 @@ def __str__(self) -> str: if self.kind == 'rank': within = f' within {self.qualifier}' if self.qualifier else '' return f'the position of {self.name}{within}' - if self.kind == 'relation_pair': + if self.kind in ('relation_pair', 'param_pair'): return f'{self.name} vs {self.qualifier}' return self.name @@ -191,12 +192,16 @@ def _observe(node: TypedPredicateNode, subject: Subject, values: set[Any], dtype """Record what *node* says about its subject: a position, or a literal. ``position()`` converts the dimension to an integer, so an ordering over a - rank is an ordering of integers and every comparator is admitted there. + rank is an ordering of integers and every comparator is admitted there. A + parameter pair names no literal: its subject is the order between the two + columns, whose cells :func:`_cells_for` fixes. """ + if isinstance(node, ParameterPairComparisonNode): + return if isinstance(node, ArithmeticComparisonNode | ExpressionComparisonNode): msg = ( 'it compares expressions, whose values only the data decides — compare one parameter against a ' - 'literal, or precompute the test as a boolean parameter and test that' + 'literal or another parameter, or precompute the test as a boolean parameter and test that' ) raise Undecidable(msg) if isinstance(node, DimensionPositionNode): @@ -228,6 +233,8 @@ def _subject_of(node: TypedPredicateNode) -> Subject: return Subject('variable', name) case DimensionComparisonNode(name=name): return Subject('dim', name) + case ParameterPairComparisonNode(name=name, other=other): + return Subject('param_pair', name, other) case DimensionPositionNode(name=name, partition=partition): if partition is None: return Subject('rank', name) @@ -252,6 +259,8 @@ def _cells_for(subject: Subject, values: set[Any], dtypes: Mapping[str, Declared return _rank_cells(subject, cast('set[int]', values)) if subject.kind in ('relation_pair', 'variable'): return [True, False] + if subject.kind == 'param_pair': + return [*_PAIR_ORDERS, Special.NULL] dtype = dtypes.get(subject.name) if dtype == 'bool': if values: @@ -373,11 +382,18 @@ def _rank_cells(subject: Subject, positions_seen: set[int]) -> list[Cell]: return cells +#: The order the left side of a parameter pair stands in to the right: the sign +#: of their difference, which every comparator reads against ``0``. +_PAIR_ORDERS: tuple[int, ...] = (-1, 0, 1) + + def _shown(subject: Subject, value: Cell) -> str: if subject.kind == 'rank': return str(value) if subject.kind == 'relation_pair': return 'equal' if value else 'different' + if subject.kind == 'param_pair' and isinstance(value, int): + return {-1: 'less', 0: 'equal', 1: 'greater'}[value] if isinstance(value, Special): return {Special.NULL: 'absent', Special.OTHER: 'anything else'}.get(value, value.value) if isinstance(value, bool): @@ -419,6 +435,10 @@ def _atom(node: TypedPredicateNode, cell: dict[Subject, Cell], grid: _Grid) -> b return bool(value) case RelationPairComparisonNode(op=op): return bool(value) if op == '==' else not value + case ParameterPairComparisonNode(op=op): + if value is Special.NULL: + return False + return _compare(value, op, 0) case ArithmeticComparisonNode() | ExpressionComparisonNode(): msg = 'a comparison of expressions is refused as undecidable before any cell is read' raise AssertionError(msg) diff --git a/src/math_spec/lowering.py b/src/math_spec/lowering.py index 3388d5dd..bb275852 100644 --- a/src/math_spec/lowering.py +++ b/src/math_spec/lowering.py @@ -173,6 +173,13 @@ def lower_program(expanded: _ExpandedSpec) -> program.Program: dimensions=dimensions, sos=sos, piecewise={name: declaration_of(ex) for name, ex in expanded.expanded_piecewise.items()}, + assumptions={ + name: program.AssumptionDeclaration( + _Lowering(expanded, f"assumption '{name}'").mask(holds) or holds, + _Lowering(expanded, f"assumption '{name}'").mask(where), + ) + for name, (holds, where) in resolved.assumptions.items() + }, named_expressions=expressions, ) diff --git a/src/math_spec/model.py b/src/math_spec/model.py index 0ce239d2..ecff0ec5 100644 --- a/src/math_spec/model.py +++ b/src/math_spec/model.py @@ -466,6 +466,56 @@ def _as_written(self) -> str | dict[str, Any]: return {'expression': self.expression, 'description': self.description} +class AssumptionBlock(_StrictBlock): + """What the model assumes of its data: a predicate every coordinate has to satisfy. + + Written in YAML as a bare where string, or as a mapping once it carries a + ``where:`` or a ``description:``, and serialised back to whichever form it + was written in:: + + assumptions: + efficiency_is_a_fraction: "efficiency > 0 AND efficiency <= 1" + bounds_do_not_cross: + holds: "p_min <= p_max" + where: "p_min" + description: a unit with no minimum is unconstrained below + + The language decides nothing about the numbers, so the consumer binding + the data checks it, and refuses the data where it does not hold. + """ + + _label: ClassVar[str] = 'an assumption declaration' + + #: The predicate, in the where grammar. It holds at every coordinate of + #: its own frame that ``where`` admits. + holds: str + #: Which coordinates are checked, in the same grammar; absent means every one. + where: str | None = None + description: str | None = None + + @model_validator(mode='before') + @classmethod + def _from_string(cls, data: Any) -> Any: + return {'holds': data} if isinstance(data, str) else data + + @classmethod + @override + def __get_pydantic_json_schema__(cls, core_schema: CoreSchema, handler: GetJsonSchemaHandler) -> JsonSchemaValue: + """The published schema admits the bare string the one-line form is written as.""" + return _also_written_as(core_schema, handler, {'type': 'string'}) + + @model_serializer + def _as_written(self) -> str | dict[str, Any]: + if self.where is None and self.description is None: + return self.holds + written: dict[str, Any] = {'holds': self.holds} + if self.where is not None: + written['where'] = self.where + if self.description is not None: + written['description'] = self.description + return written + + class PiecewiseLink(_StrictBlock): """One link of a piecewise block: an expression pinned to a values curve. @@ -683,7 +733,7 @@ class Spec(_StrictBlock): :class:`~math_spec.errors.LanguageError` on a model the language refuses. Holding one is the proof, so nothing downstream checks it again. - The API is the ten declaration sections plus ``version`` and + The API is the eleven declaration sections plus ``version`` and ``description``, and two ways back out: :meth:`to_dict` for the model as data, :meth:`to_yaml` for the file a reviewer reads. Everything else on this class is pydantic's, not a contract this package keeps. @@ -714,6 +764,7 @@ class Spec(_StrictBlock): macros: dict[str, MacroBlock] = {} piecewise: dict[str, PiecewiseBlock] = {} sos: dict[str, SosBlock] = {} + assumptions: dict[str, AssumptionBlock] = {} def relations_of(self, dimension: str) -> dict[str, RelationBlock]: """The relations with a column over *dimension*, by name.""" diff --git a/src/math_spec/program.py b/src/math_spec/program.py index ce8947f4..04f6aaf6 100644 --- a/src/math_spec/program.py +++ b/src/math_spec/program.py @@ -42,6 +42,7 @@ 'Add', 'AndNode', 'ArithmeticComparisonNode', + 'AssumptionDeclaration', 'At', 'AtLeastTwo', 'BooleanLiteralNode', @@ -83,6 +84,7 @@ 'ParameterDeclaration', 'ParameterDefinedNode', 'ParameterDtype', + 'ParameterPairComparisonNode', 'PiecewiseDeclaration', 'Power', 'PredicateOperator', @@ -107,6 +109,7 @@ 'Walk', 'WhereNode', 'Window', + 'assumption_message', 'carries_variable', 'check_message', 'children', @@ -754,6 +757,32 @@ class ConstraintDeclaration: where: Mask | None = None +@dataclass(frozen=True) +class AssumptionDeclaration: + """An ``assumptions:`` entry: what the file assumes of its data, kept for the consumer holding it to check. + + ``holds`` is true at every coordinate of its frame — the product of every + dim the two masks name — that ``where`` admits, a missing row reading as + false as it does in any mask. The language decides nothing about the + numbers, so a consumer binding data checks, and refuses the data with + :func:`assumption_message` at the first coordinate where ``holds`` is + false. + """ + + holds: Mask + where: Mask | None = None + + +def assumption_message(name: str, assumption: AssumptionDeclaration) -> str: + """The sentence a consumer raises when the data bound to *assumption*, called *name*, fails it. + + The language's own wording, so every consumer refuses in the same words; + a consumer appends the coordinates it saw. + """ + read = ', '.join(f"'{n}'" for n in sorted(assumption.holds.names_read)) + return f"assumption '{name}' does not hold for the data bound to {read}" + + @dataclass(frozen=True) class SosDeclaration: """One special-ordered set per coordinate of the variable's ``dims`` minus ``over``. @@ -948,6 +977,9 @@ class Program: #: Each ``piecewise:`` block the file wrote, as facts — see #: :class:`PiecewiseDeclaration`. piecewise: Mapping[str, PiecewiseDeclaration] = Sealed({}) + #: What the file assumes of its data, by the name it wrote — see + #: :class:`AssumptionDeclaration`. A consumer binding data checks each. + assumptions: Mapping[str, AssumptionDeclaration] = Sealed({}) #: Declared ``expressions:``, lowered, each saying whether the math reads #: it. None builds a row of its own — one the math reads is inlined where #: it is read — but all are lowered with the program, so a file whose @@ -1140,6 +1172,20 @@ class ParameterComparisonNode: dims: tuple[str, ...] +@dataclass(frozen=True) +class ParameterPairComparisonNode: + """Compare two parameters, coordinate by coordinate — ``p_min <= p_max``. + + ``dims`` is the union of both parameters' dims: the narrower one is read + at every coordinate of the wider, as a product of the two would be. + """ + + name: str + other: str + op: PredicateOperator + dims: tuple[str, ...] + + @dataclass(frozen=True) class ExpressionComparisonNode: """Compare two variable-free expressions, coordinate by coordinate — ``p_min <= 0.5 * p_max``. @@ -1269,6 +1315,7 @@ class OrNode: | ParameterDefinedNode | VariableDefinedNode | ParameterComparisonNode + | ParameterPairComparisonNode | ExpressionComparisonNode | ArithmeticComparisonNode | DimensionComparisonNode @@ -1285,6 +1332,7 @@ class OrNode: #: decide about them. TypedPredicateNode = ( ParameterComparisonNode + | ParameterPairComparisonNode | ExpressionComparisonNode | ArithmeticComparisonNode | ParameterDefinedNode @@ -1350,6 +1398,7 @@ def _atom_dims(atom: TypedPredicateNode) -> frozenset[str]: match atom: case ( ParameterComparisonNode() + | ParameterPairComparisonNode() | ExpressionComparisonNode() | ArithmeticComparisonNode() | ParameterDefinedNode() @@ -1370,8 +1419,9 @@ def _atom_names(atom: TypedPredicateNode) -> frozenset[str]: """One leaf's declarations, its dimension apart — the rule :attr:`Mask.names_read` is the union of. A comparison on a dimension names no declaration — a coordinate is not - data to feed — a relation pair names both maps it compares, and a comparison - of expressions names every parameter and relation its sides read. + data to feed — a relation pair and a parameter pair each name both sides + they compare, and a comparison of expressions names every parameter and + relation its sides read. ``assert_never``-closed for the reason :func:`_atom_dims` is: a predicate node added without a reading is a type error at this one branch rather than a name silently dropped at the first model to use it. @@ -1385,7 +1435,7 @@ def _atom_names(atom: TypedPredicateNode) -> frozenset[str]: | RelationDefinedNode() ): return frozenset({atom.name}) - case RelationPairComparisonNode(): + case RelationPairComparisonNode() | ParameterPairComparisonNode(): return frozenset({atom.name, atom.other}) case ExpressionComparisonNode(): return _names_under(atom.left, atom.right) diff --git a/src/math_spec/resolution.py b/src/math_spec/resolution.py index aebbb98d..f2deccef 100644 --- a/src/math_spec/resolution.py +++ b/src/math_spec/resolution.py @@ -13,7 +13,7 @@ import datetime import re -from dataclasses import dataclass, replace +from dataclasses import dataclass, field, replace from functools import cached_property from typing import TYPE_CHECKING, Literal, NamedTuple, assert_never, cast @@ -74,6 +74,7 @@ OrNode, ParameterComparisonNode, ParameterDefinedNode, + ParameterPairComparisonNode, PredicateOperator, RelationComparisonNode, RelationDeclaration, @@ -211,6 +212,13 @@ class ResolvedConstraint(NamedTuple): where: Mask | None +class Assumption(NamedTuple): + """One assumption's typed halves: what holds, and where it is checked.""" + + holds: Mask + where: Mask | None + + @dataclass(frozen=True) class Resolved: """Every expression and where string of one schema, typed once at load. @@ -232,12 +240,15 @@ class Resolved: constraints: Each constraint's comparison and ``where``. objective: The objective's expression, ``None`` where the file declares none. + assumptions: Each assumption's predicate and the mask it is checked + under. """ expressions: dict[str, CasesNode | DefinitionNode] variables: dict[str, Mask | None] constraints: dict[str, ResolvedConstraint] objective: ArithmeticNode | None + assumptions: dict[str, Assumption] = field(default_factory=dict) @cached_property def read_by_the_math(self) -> frozenset[str]: @@ -921,7 +932,7 @@ def _position(self, node: UnresolvedPositionNode) -> DimensionPositionNode | Unr return DimensionPositionNode(node.dimension, node.op, node.position, walk) def _comparison(self, node: UnresolvedComparisonNode) -> WhereNode | UnresolvedWhereNode: - """``name literal``, or the one structural form ``relation relation``. + """``name literal``, or the two pair forms: ``relation relation`` and ``parameter parameter``. A side that names an ``expressions:`` entry is arithmetic, whatever the grammar first read it as, and takes the expression path. @@ -945,7 +956,16 @@ def _comparison(self, node: UnresolvedComparisonNode) -> WhereNode | UnresolvedW return node dims = tuple(ns.shape_of(left_name).dim(k) for k in ns.shape_of(left_name).key) return RelationPairComparisonNode(left_name, left, right_name, right, node.op, dims) - self.errors.append(_declared_rhs_error(context, node, value, rhs_kind)) + if rhs_kind == 'parameter' and ns.kind(left_name) == 'parameter' and not (left_column or right_column): + if (refusal := _parameter_pair_error(context, node, value, ns)) is not None: + self.errors.append(refusal) + return node + dims = ( + *ns.leaf_dims[node.name], + *(d for d in ns.leaf_dims[value] if d not in ns.leaf_dims[node.name]), + ) + return ParameterPairComparisonNode(node.name, value, node.op, dims) + self.errors.append(_declared_rhs_error(context, node, value, rhs_kind, ns)) return node kind = ns.kind(left_name) @@ -1181,15 +1201,14 @@ def _literal(value: ArithmeticNode) -> NumberNode | None: return None -def _declared_rhs_error(context: str, node: UnresolvedComparisonNode, value: str, kind: str) -> str: +def _declared_rhs_error(context: str, node: UnresolvedComparisonNode, value: str, kind: str, ns: Namespace) -> str: """Why the right-hand side of a where-comparison may not name a declaration.""" comparison = f"'{node.name} {node.op} {value}'" if kind == 'parameter': return ( - f'{context}: {comparison} compares two parameters, which is not in the ' - f'language — a where-comparison tests one parameter or dimension against ' - f'a literal. Precompute the comparison as a boolean parameter in data ' - f'prep and test that.' + f'{context}: {comparison} compares {node.name!r}, which is {_declared_as(ns, node.name)}, against ' + f'parameter {value!r}. Two parameters may be compared, and nothing else may be compared against ' + f'one — test a parameter, or a literal.' ) if kind == 'variable': return ( @@ -1211,6 +1230,23 @@ def _declared_rhs_error(context: str, node: UnresolvedComparisonNode, value: str ) +def _parameter_pair_error(context: str, node: UnresolvedComparisonNode, other: str, ns: Namespace) -> str | None: + """Why two parameters may not be compared, or ``None`` where they may. + + Two numbers compare, as do two labels and two flags; a number against a + label or a flag compares nothing, silently, whatever the data library + makes of it. + """ + left, right = ns.dtypes[node.name], ns.dtypes[other] + if left == right or {left, right} <= NUMERIC_DTYPES: + return None + return ( + f"{context}: '{node.name} {node.op} {other}' compares a {left} parameter against a {right} one, " + f'and the two have no value in common to compare. Declare both as numbers, or both as the same ' + f'dtype, or precompute the test as a boolean parameter.' + ) + + def _relation_pair_error( context: str, node: UnresolvedComparisonNode, other: str, ns: Namespace, left: str, right: str ) -> str | None: diff --git a/src/math_spec/typesetting/__init__.py b/src/math_spec/typesetting/__init__.py index 0575fe39..0b186589 100644 --- a/src/math_spec/typesetting/__init__.py +++ b/src/math_spec/typesetting/__init__.py @@ -158,7 +158,7 @@ def typeset_declaration( """Render one declaration as the bare line the document prints for it. The line the whole-model render prints for it — a named expression's - definition, a constraint, or a variable's domain, quantifier included — + definition, a constraint, an assumption, or a variable's domain, quantifier included — with no document, label, equation number or math delimiters around it, for a math context the caller lays out: a docstring, a table cell. A line on its own has no Definitions section beside it, so the plain named @@ -167,7 +167,7 @@ def typeset_declaration( Args: model: Anything :func:`math_spec.to_spec` accepts. - name: A named expression, constraint or variable the model declares. + name: A named expression, constraint, assumption or variable the model declares. fmt: What spells the math — a key of :data:`FORMATS`. symbols: How names print; see :func:`typeset`. inline_expressions: Substitute the plain named expressions the line uses, so it @@ -181,17 +181,24 @@ def typeset_declaration( Raises: ValueError: *fmt* names no format. LanguageError: A model that does not compile; it does not print. - SchemaError: *name* is declared as none of the three, or as two — a + SchemaError: *name* is declared as none of the four, or as two — a constraint may share a variable's name; or a symbol table entry names nothing in the model. """ walk = _walk(model, fmt, symbols, inline_expressions=inline_expressions) schema = walk.schema - kinds = {'named expression': schema.expressions, 'constraint': schema.constraints, 'variable': schema.variables} + kinds = { + 'named expression': schema.expressions, + 'constraint': schema.constraints, + 'assumption': schema.assumptions, + 'variable': schema.variables, + } found = [kind for kind, group in kinds.items() if name in group] if not found: everything = {n for group in kinds.values() for n in group} - msg = f"'{name}' is not a named expression, constraint or variable. {did_you_mean(name, everything)}" + msg = ( + f"'{name}' is not a named expression, constraint, assumption or variable. {did_you_mean(name, everything)}" + ) raise SchemaError(msg) if len(found) > 1: msg = f"'{name}' is both a {found[0]} and a {found[1]}, and one line prints one of them — rename one." diff --git a/src/math_spec/typesetting/format.py b/src/math_spec/typesetting/format.py index a0bedfb5..80612b69 100644 --- a/src/math_spec/typesetting/format.py +++ b/src/math_spec/typesetting/format.py @@ -223,6 +223,10 @@ def cardinality(self, inner: str) -> str: def fraction(self, numerator: str, denominator: str) -> str: ... + def set_of(self, members: str, condition: str) -> str: + """A set by comprehension: ``{ k ∈ K : condition }``.""" + ... + def summation(self, domain: str, body: str) -> str: ... def cases(self, arms: list[tuple[str, str]]) -> str: diff --git a/src/math_spec/typesetting/latex.py b/src/math_spec/typesetting/latex.py index d09c3ff2..3e3296f5 100644 --- a/src/math_spec/typesetting/latex.py +++ b/src/math_spec/typesetting/latex.py @@ -98,6 +98,9 @@ def cardinality(self, inner: str) -> str: def fraction(self, numerator: str, denominator: str) -> str: return rf'\frac{{{numerator}}}{{{denominator}}}' + def set_of(self, members: str, condition: str) -> str: + return rf'\{{ {members} {self.operators["such_that"]} {condition} \}}' + def cases(self, arms: list[tuple[str, str]]) -> str: rows = self.cases_row.join(f'{value} & {condition}' for value, condition in arms) return rf'\begin{{cases}} {rows} \end{{cases}}' diff --git a/src/math_spec/typesetting/typst.py b/src/math_spec/typesetting/typst.py index 55c34c7f..d83a1aeb 100644 --- a/src/math_spec/typesetting/typst.py +++ b/src/math_spec/typesetting/typst.py @@ -106,6 +106,9 @@ def cardinality(self, inner: str) -> str: def fraction(self, numerator: str, denominator: str) -> str: return f'frac({numerator}, {denominator})' + def set_of(self, members: str, condition: str) -> str: + return f'{{{members} {self.operators["such_that"]} {condition}}}' + def cases(self, arms: list[tuple[str, str]]) -> str: return 'cases({})'.format(self.cases_row.join(f'{value} & {condition}' for value, condition in arms)) diff --git a/src/math_spec/typesetting/walk.py b/src/math_spec/typesetting/walk.py index c6f5b5fc..e447ab94 100644 --- a/src/math_spec/typesetting/walk.py +++ b/src/math_spec/typesetting/walk.py @@ -34,18 +34,25 @@ VariableNode, ) from math_spec.dimensions import dims_of +from math_spec.piecewise import declaration_of from math_spec.program import ( AndNode, ArithmeticComparisonNode, + AtLeastTwo, BooleanLiteralNode, + Check, + Contiguous, + Curved, DimensionComparisonNode, DimensionPositionNode, ExpressionComparisonNode, + Increasing, Mask, NotNode, OrNode, ParameterComparisonNode, ParameterDefinedNode, + ParameterPairComparisonNode, PredicateOperator, RelationComparisonNode, RelationDefinedNode, @@ -59,7 +66,7 @@ import datetime from collections.abc import Iterable, Mapping - from math_spec.model import RelationBlock, SosBlock, _ExpandedSpec + from math_spec.model import ExpandedPiecewise, RelationBlock, SosBlock, _ExpandedSpec from math_spec.program import Walk as RelationWalk from math_spec.typesetting.format import Format from math_spec.typesetting.symbols import Symbols @@ -74,6 +81,18 @@ #: a comparison sits above the connectives and is bracketed under none. _WHERE_PRECEDENCE = {'or': 0, 'and': 1, 'comparison': 2, 'not': 3} +#: The predicates that are one relation between two sides, which a line may +#: align on the way it aligns a constraint. +AlignedComparison = ( + ParameterComparisonNode + | ParameterPairComparisonNode + | ArithmeticComparisonNode + | DimensionComparisonNode + | DimensionPositionNode + | RelationComparisonNode + | RelationPairComparisonNode +) + _PREDICATES: dict[PredicateOperator, OperatorName] = { '==': 'equal', '!=': 'ne', @@ -379,6 +398,10 @@ def _arithmetic(self, node: ArithmeticNode, ctx: _Context) -> tuple[str, int]: assert_never(node) + def _parameter(self, name: str, ctx: _Context) -> str: + """A parameter's symbol, indexed by its own dims.""" + return ctx.indexed(self.symbols.name[name], list(self.schema.parameters[name].dims)) + def _dual(self, node: DualNode, ctx: _Context) -> str: """λ subscripted by the constraint's symbol, then the indices of the constraint's own frame.""" frame = self._sorted(dims_of(node, self.schema, 'a dual')) @@ -577,41 +600,14 @@ def _where(self, node: WhereNode, ctx: _Context) -> tuple[str, int]: comparison, ) - if isinstance(node, ParameterComparisonNode): - left = ctx.indexed(self.symbols.name[node.name], list(node.dims)) - return f'{left} {self._op(_PREDICATES[node.op])} {self._literal(node.value)}', comparison - - if isinstance(node, ArithmeticComparisonNode): - left, right = self._expression(node.left, ctx), self._expression(node.right, ctx) - return f'{left} {self._op(_PREDICATES[node.op])} {right}', comparison + if isinstance(node, AlignedComparison): + left, right = self._relation(node, ctx) + return f'{left} {right}', comparison if isinstance(node, ExpressionComparisonNode): msg = 'a lowered comparison reached the typesetter; it prints the resolved tree, which lowering rebuilds.' raise AssertionError(msg) - if isinstance(node, DimensionComparisonNode): - if isinstance(node.value, int | float): - self.noticed.numeric_coordinates.add(node.name) - return ( - f'{ctx.subscript(node.name)} {self._op(_PREDICATES[node.op])} {self._literal(node.value)}', - comparison, - ) - - if isinstance(node, DimensionPositionNode): - grouping = None if node.partition is None else self._position_group(node, ctx) - place = self._position(ctx.subscript(node.name), grouping) - ordinal = self._ordinal(node.name, node.position, grouping) - return f'{place} {self._op(_PREDICATES[node.op])} {ordinal}', comparison - - if isinstance(node, RelationComparisonNode): - applied = self._value_read(node.name, node.column, ctx) - return f'{applied} {self._op(_PREDICATES[node.op])} {self._literal(node.value)}', comparison - - if isinstance(node, RelationPairComparisonNode): - left = self._value_read(node.name, node.column, ctx) - right = self._value_read(node.other, node.other_column, ctx) - return f'{left} {self._op(_PREDICATES[node.op])} {right}', comparison - if isinstance(node, RelationDefinedNode): lk = self.schema.relations[node.name] if lk.keys: @@ -639,6 +635,35 @@ def _where(self, node: WhereNode, ctx: _Context) -> tuple[str, int]: assert_never(node) + def _relation(self, node: AlignedComparison, ctx: _Context) -> tuple[str, str]: + """A comparison as its two sides, the relation symbol leading the right. + + Split so that a line whose whole predicate is one comparison aligns + on the relation as a constraint does. + """ + if isinstance(node, ParameterComparisonNode): + left, right = self._parameter(node.name, ctx), self._literal(node.value) + elif isinstance(node, ParameterPairComparisonNode): + left, right = self._parameter(node.name, ctx), self._parameter(node.other, ctx) + elif isinstance(node, ArithmeticComparisonNode): + left, right = self._expression(node.left, ctx), self._expression(node.right, ctx) + elif isinstance(node, DimensionComparisonNode): + if isinstance(node.value, int | float): + self.noticed.numeric_coordinates.add(node.name) + left, right = ctx.subscript(node.name), self._literal(node.value) + elif isinstance(node, DimensionPositionNode): + grouping = None if node.partition is None else self._position_group(node, ctx) + left = self._position(ctx.subscript(node.name), grouping) + right = self._ordinal(node.name, node.position, grouping) + elif isinstance(node, RelationComparisonNode): + left, right = self._value_read(node.name, node.column, ctx), self._literal(node.value) + elif isinstance(node, RelationPairComparisonNode): + left = self._value_read(node.name, node.column, ctx) + right = self._value_read(node.other, node.other_column, ctx) + else: + assert_never(node) + return left, f'{self._op(_PREDICATES[node.op])} {right}' + def _literal(self, value: float | str | datetime.date) -> str: return self._number(value) if isinstance(value, int | float) else self.format.quoted(str(value)) @@ -688,6 +713,7 @@ def equations(self) -> tuple[list[tuple[str, list[Line]]], Noticed]: ('Subject to', self._constraints()), ('Definitions', self._definitions()), ('Variable domains', self._variables()), + ('Assumptions', self._assumptions()), ] return sections, self.noticed @@ -762,15 +788,17 @@ def definition(self, name: str) -> Line: ) def line(self, name: str) -> Line: - """The one line *name* prints as: a named expression's definition, a constraint, or a variable's domain. + """The one line *name* prints as: a named expression's definition, a constraint, an assumption, or a variable's domain. - *name* is one of the three; :func:`~math_spec.typesetting.typeset_declaration` + *name* is one of the four; :func:`~math_spec.typesetting.typeset_declaration` refuses the rest, and a constraint sharing a variable's name. """ if name in self.schema.expressions: return self.definition(name) if name in self.schema.constraints: return self._constraint(name) + if name in self.schema.assumptions: + return self._assumption(name) return self._variable(name) def _arms(self, node: CasesNode, ctx: _Context) -> list[tuple[str, str]]: @@ -842,6 +870,102 @@ def _sos(self, name: str, block: SosBlock, ctx: _Context) -> Line: condition=self._quantifier([d for d in dims if d != block.over], ''), ) + # -- assumptions ------------------------------------------------------- + + def _assumptions(self) -> list[Line]: + """What the model assumes of its data: every ``assumptions:`` entry, then what each curve assumes of its breakpoints. + + A ``piecewise:`` block's checks are the language's own + (:func:`~math_spec.piecewise.declaration_of`), so they print here + beside the author's, under the block's name: the reader sees every + condition the data is held to, whether the file wrote it or a method + implied it. + """ + lines = [self._assumption(name) for name in self.schema.assumptions] + for name, expanded in self.schema.expanded_piecewise.items(): + lines += [self._check(name, expanded, check) for check in declaration_of(expanded).checks] + return lines + + def _assumption(self, name: str) -> Line: + """One declared assumption: the predicate, quantified over the frame both its masks name, under its ``where``.""" + holds, where = self.schema.resolved.assumptions[name] + frame = self._sorted(holds.dims | (where.dims if where is not None else frozenset())) + ctx = self._context(frame) + if isinstance(holds.root, AlignedComparison): + left, right = self._relation(holds.root, ctx) + else: + left, right = self._predicate(holds.root, ctx), '' + return Line(label=name, left=left, right=right, condition=self._quantifier(frame, self._condition(ctx, where))) + + def _check(self, block: str, expanded: ExpandedPiecewise, check: Check) -> Line: + """One condition a curve puts on its breakpoints, as the line a reader checks the data against. + + The strictly increasing x-axis is an inequality between neighbours, + printed with the plain translation whose vacated first row is absent. + The shape a method is exact for is prose, as a paper writes it, since + "convex or concave" is no one inequality. The two conditions on a + ``points:`` mask are stated of the set the mask admits. + """ + over = expanded.block.over + match check: + case Increasing(parameter, _): + frame = self._sorted(frozenset(self.schema.parameters[parameter].dims)) + ctx = self._context(frame) + previous = ctx.translated(over, _Step(1, 'plain')) + condition = '' + if (mask := expanded.points) is not None: + admitted = ParameterDefinedNode(mask, tuple(self.schema.parameters[mask].dims)) + condition = self.format.joined( + [self._predicate(admitted, ctx), self._predicate(admitted, previous)], self._op('and') + ) + return Line( + label=f'{block} increasing', + left=self._parameter(parameter, previous), + right=f'{self._op("lt")} {self._parameter(parameter, ctx)}', + condition=self._quantifier(frame, condition), + ) + case Curved(x, y, _, curvature): + dims = frozenset(self.schema.parameters[x].dims) | frozenset(self.schema.parameters[y].dims) + ctx = self._context(self._sorted(dims)) + shape = 'convex or concave' if curvature == 'either' else curvature + return Line( + label=f'{block} curvature', + left=self._parameter(y, ctx), + right=( + f'{self.format.prose(f" is a {shape} function of ")} {self._parameter(x, ctx)} ' + f'{self.format.prose(" along ")} {self.symbols.index[over]}' + ), + condition=self._quantifier(self._sorted(dims - {over}), ''), + ) + case AtLeastTwo(_, mask): + members, frame = self.symbols.set[over], self._sorted(frozenset()) + if mask is not None: + members, frame = self._admitted(mask, over) + return Line( + label=f'{block} breakpoints', + left=self.format.cardinality(members), + right=f'{self._op("ge")} {self._number(2)}', + condition=self._quantifier(frame, ''), + ) + case Contiguous(mask, _): + members, frame = self._admitted(mask, over) + return Line( + label=f'{block} points', + left=members, + right=self.format.prose(' is one run of consecutive breakpoints'), + condition=self._quantifier(frame, ''), + ) + case _: + assert_never(check) + + def _admitted(self, mask: str, over: str) -> tuple[str, list[str]]: + """The breakpoints *mask* admits along *over* as a set, and the frame that set is one of per curve.""" + dims = frozenset(self.schema.parameters[mask].dims) + frame = self._sorted(dims - {over}) + ctx = self._context([*frame, over]) + admitted = self._predicate(ParameterDefinedNode(mask, tuple(self.schema.parameters[mask].dims)), ctx) + return self.format.set_of(self._membership(over), admitted), frame + def _bound(self, ctx: _Context, value: float | str) -> str: if isinstance(value, str): return ctx.indexed(self.symbols.name[value], list(self.schema.parameters[value].dims)) diff --git a/src/math_spec/validation.py b/src/math_spec/validation.py index e4017957..2531c8bf 100644 --- a/src/math_spec/validation.py +++ b/src/math_spec/validation.py @@ -37,8 +37,9 @@ from math_spec.expansion import expand, parse_and_expand, parse_template from math_spec.model import Spec from math_spec.operators import BUILTINS, unknown_operator_message -from math_spec.program import BooleanLiteralNode +from math_spec.program import BooleanLiteralNode, Mask, VariableDefinedNode from math_spec.resolution import ( + Assumption, Namespace, Resolved, ResolvedConstraint, @@ -51,7 +52,7 @@ if TYPE_CHECKING: from pathlib import Path - from math_spec.model import ExpressionBlock + from math_spec.model import AssumptionBlock, ExpressionBlock from math_spec.program import WhereNode @@ -161,10 +162,15 @@ def validate_expressions(schema: Spec) -> Resolved: schema.objective.expression, schema, ns, 'The objective', errors, comparison=False, ceiling=2 ) + assumptions: dict[str, Assumption] = {} + for aname, adef in schema.assumptions.items(): + if (assumption := _assumption(aname, adef, ns, errors)) is not None: + assumptions[aname] = assumption + if errors: raise SchemaError(_once(errors)) - resolved = Resolved(expressions, variables, constraints, objective) + resolved = Resolved(expressions, variables, constraints, objective, assumptions) check_schema(schema, resolved) return resolved @@ -206,6 +212,43 @@ def _named( return CasesNode(name, (*arms, CaseArm('otherwise', None, fallback))) +def _assumption(name: str, block: AssumptionBlock, ns: Namespace, errors: list[str]) -> Assumption | None: + """One ``assumptions:`` entry typed, or ``None`` once anything in it failed. + + A predicate the connectives decide is refused: one that folds to true + assumes nothing, and one that folds to false refuses every dataset. A + variable is refused too, since an assumption is about the data and a + variable is what the solver decides from it. + """ + context = f"Assumption '{name}'" + found = len(errors) + holds = resolve_where_text(block.holds, ns, context, errors) + where = resolve_where_text(block.where, ns, f'{context}, where', errors) + if isinstance(holds, BooleanLiteralNode): + errors.append( + f'{context}: the predicate {block.holds!r} folds to {holds.value}, so it ' + + ( + 'assumes nothing of the data. Delete it, or name a parameter it constrains.' + if holds.value + else 'holds on no data at all. Delete it, or write the predicate the data can satisfy.' + ) + ) + for mask, part in ((holds, 'assumes'), (where, 'is checked where')): + if mask is None or isinstance(mask, BooleanLiteralNode): + continue + errors.extend( + f"{context}: variable '{atom.name}' stands in what the assumption {part}, and an assumption is " + f'about the data — a variable is what the solver decides from it. Name a parameter, or state the ' + f'rule as a constraint.' + for atom in Mask(mask).atoms + if isinstance(atom, VariableDefinedNode) + ) + if len(errors) > found: + return None + assert holds is not None, 'a where string that read to nothing appended an error' + return Assumption(Mask(holds), mask_of(where)) + + def _prefixed(context: str, e: ValueError) -> str: """*e* under *context*, once — expansion errors already carry it.""" return str(e) if str(e).startswith(context) else f'{context}: {e}' @@ -299,7 +342,7 @@ def _check_expression( f'Got: {expression!r}\n' f'A constraint is a claim about a decision, and a comparison of numbers and parameters ' f'is settled before the solve — no consumer builds a row for it. Name the variable it should ' - f'bound, or drop the declaration and check the fact where the data is prepared.' + f'bound, or state the fact under `assumptions:`, where the consumer binding the data checks it.' ) return None return resolved diff --git a/tests/test_exclusivity.py b/tests/test_exclusivity.py index 3b62be64..c3f225d1 100644 --- a/tests/test_exclusivity.py +++ b/tests/test_exclusivity.py @@ -60,6 +60,27 @@ def refusals(schema: Spec, cases: dict[str, str]) -> list[str]: return list(overlapping({name: _mask(when, namespace, name) for name, when in cases.items()}, namespace.dtypes)) +def test_two_parameters_compared_are_one_subject_ordered_three_ways(schema): + """The order between two columns is less, equal or greater, so `<` and `>=` are apart and `<=` meets `>=` at equality.""" + assert refusals(schema, {'below': 'soc_initial < capacity', 'above': 'soc_initial >= capacity'}) == [], ( + 'the two orders share no cell' + ) + [refusal] = refusals(schema, {'below': 'soc_initial <= capacity', 'above': 'soc_initial >= capacity'}) + assert 'soc_initial vs capacity is equal' in refusal, 'the witness names the order both cases claim' + + +def test_a_parameter_pair_with_a_row_missing_compares_false_under_every_comparator(schema): + """`NOT (a < b)` and `NOT (a >= b)` are apart wherever both rows exist, and both claim a coordinate where one is missing. + + A missing row read as the smallest value instead would put the two apart + everywhere, and the data would then give one coordinate two values. + """ + [refusal] = refusals( + schema, {'not_below': 'NOT (soc_initial < capacity)', 'not_above': 'NOT (soc_initial >= capacity)'} + ) + assert 'soc_initial vs capacity is absent' in refusal, 'the one cell both claim is the missing row' + + def _mask(text: str, namespace: Namespace, name: str) -> WhereNode: """Resolved but not folded, which is the shape a case's `when` reaches the prover in.""" errors: list[str] = [] diff --git a/tests/test_lowering.py b/tests/test_lowering.py index 384f89ed..59d33260 100644 --- a/tests/test_lowering.py +++ b/tests/test_lowering.py @@ -25,6 +25,7 @@ QUADRATIC_POSITIONS, Add, AndNode, + AssumptionDeclaration, At, BooleanLiteralNode, Cases, @@ -45,6 +46,7 @@ Parameter, ParameterComparisonNode, ParameterDefinedNode, + ParameterPairComparisonNode, Power, Program, Region, @@ -54,6 +56,7 @@ Variable, Walk, Window, + assumption_message, children, divisor_parameters, fan_in, @@ -401,7 +404,45 @@ def test_a_constraint_where_is_a_mask_like_a_variable_s(): assert c.where == Mask(ParameterComparisonNode('load', '>', 0.0, ('snapshot',))) -def test_a_comparison_of_expressions_lowers_to_program_expressions_on_both_sides(): +def test_an_assumption_lowers_to_its_predicate_and_the_mask_it_is_checked_under(): + """What the file assumes of its data reaches the consumer as two masks under the name the file wrote.""" + program = to_program( + override( + DISPATCH_MODEL, + assumptions={'capacity': 'p_max >= 0', 'ordered': {'holds': 'cost <= p_max', 'where': 'cost'}}, + ) + ) + + assert program.assumptions['capacity'] == AssumptionDeclaration( + Mask(ParameterComparisonNode('p_max', '>=', 0.0, ('generator',))) + ), 'an assumption without a where is checked at every coordinate its predicate names' + assert program.assumptions['ordered'] == AssumptionDeclaration( + Mask(ParameterPairComparisonNode('cost', 'p_max', '<=', ('generator',))), + Mask(ParameterDefinedNode('cost', ('generator',))), + ) + assert assumption_message('ordered', program.assumptions['ordered']) == ( + "assumption 'ordered' does not hold for the data bound to 'cost', 'p_max'" + ), 'the sentence names every parameter the predicate reads, sorted, for the consumer to append what it saw' + + +def test_a_parameter_pair_carries_the_union_of_both_dims_left_first(): + """`p_max <= floor` over `[generator]` and `[snapshot, generator]` is read at every coordinate of both.""" + program = to_program( + override( + DISPATCH_MODEL, + **{'parameters.floor': {'dims': ['snapshot', 'generator']}, 'assumptions': {'a': 'p_max <= floor'}}, + ) + ) + holds = program.assumptions['a'].holds + + assert holds.root == ParameterPairComparisonNode('p_max', 'floor', '<=', ('generator', 'snapshot')), ( + "the left parameter's dims first, then what the right one adds" + ) + assert holds.dims == frozenset({'generator', 'snapshot'}) + assert holds.names_read == frozenset({'p_max', 'floor'}), 'a pair names both sides it compares' + + +def test_a_comparison_of_expressions_lowers_to_program_expressions_on_both_sides(shapes_schema): """The resolved tree holds the core syntax tree; the program holds the vocabulary a consumer reads, and every mask is rebuilt so.""" program = to_program( override( @@ -409,11 +450,7 @@ def test_a_comparison_of_expressions_lowers_to_program_expressions_on_both_sides **{ 'parameters.zc': {'dims': ['z']}, 'variables.p.where': 'c <= 0.5 * k', - 'constraints.w': { - 'dims': ['g'], - 'where': 'c <= at(zc, by=lk2) + sum_back(c, along=g, window=2, by=lk2)', - 'expression': 'p <= c', - }, + 'assumptions': {'a': 'c <= at(zc, by=lk2) + sum_back(c, along=g, window=2, by=lk2)'}, }, ) ) @@ -422,10 +459,10 @@ def test_a_comparison_of_expressions_lowers_to_program_expressions_on_both_sides assert where.root == ExpressionComparisonNode( Parameter('c'), '<=', Multiply(Constant(0.5), Parameter('k')), ('g',) ), 'the sides are lowered as a constraint side is, and the dims are what either side carries' - mask = program.constraints['w'].where - assert mask is not None and isinstance(mask.root, ExpressionComparisonNode) - assert isinstance(mask.root.right, Add) and isinstance(mask.root.right.left, At) - assert mask.names_read == frozenset({'c', 'zc', 'lk2'}), ( + holds = program.assumptions['a'].holds + assert isinstance(holds.root, ExpressionComparisonNode) + assert isinstance(holds.root.right, Add) and isinstance(holds.root.right.left, At) + assert holds.names_read == frozenset({'c', 'zc', 'lk2'}), ( 'the relation a pullback and a partition read through is data the consumer binds too' ) diff --git a/tests/test_validation.py b/tests/test_validation.py index 96226223..77607e57 100644 --- a/tests/test_validation.py +++ b/tests/test_validation.py @@ -893,7 +893,9 @@ class TestRulesDecidedWithoutData: id='where-two-relations-with-different-keys', ), pytest.param( - {'variables.p.where': 'c > flag'}, ('compares two parameters',), id='where-against-a-parameter' + {'variables.p.where': 'c > flag'}, + ('compares a float parameter against a bool one', 'Declare both as numbers'), + id='where-against-a-parameter-of-another-dtype', ), pytest.param( {'variables.p.where': 'c > q'}, @@ -923,6 +925,153 @@ def test_a_rule_decided_without_data(self, patch, fragments): assert fragment in message +class TestAssumptions: + """What an `assumptions:` entry may say, decided with no data bound.""" + + @pytest.mark.parametrize( + ('patch', 'fragments'), + [ + pytest.param( + {'assumptions': {'a': 'True'}}, + ("Assumption 'a'", 'folds to True', 'assumes nothing of the data'), + id='a-predicate-that-is-always-true', + ), + pytest.param( + {'assumptions': {'a': 'c > 0 AND False'}}, + ('folds to False', 'holds on no data at all'), + id='a-predicate-that-is-always-false', + ), + pytest.param( + {'assumptions': {'a': 'p'}}, + ("variable 'p' stands in what the assumption assumes", 'an assumption is about the data'), + id='a-variable-in-the-predicate', + ), + pytest.param( + {'assumptions': {'a': {'holds': 'c > 0', 'where': 'q'}}}, + ("variable 'q' stands in what the assumption is checked where",), + id='a-variable-in-the-where', + ), + pytest.param({'assumptions': {'a': 'nope > 0'}}, ("'nope' not found",), id='an-unknown-name'), + pytest.param({'assumptions': {'a': 'c >'}}, ('Failed to parse where string',), id='a-malformed-predicate'), + pytest.param( + {'assumptions': {'a': 'c > tag'}}, + ('compares a float parameter against a str one', 'Declare both as numbers'), + id='two-parameters-of-different-dtypes', + ), + pytest.param( + {'assumptions': {'a': 'c > p'}}, ('compares against variable',), id='a-parameter-against-a-variable' + ), + pytest.param( + {'assumptions': {'a': {'holds': 'c > 0', 'wher': 'flag'}}}, + ("unknown key 'wher' in an assumption declaration", "Did you mean 'where'?"), + id='a-misspelt-key', + ), + pytest.param( + {'assumptions': {'a': 'c > 2 * p'}}, + ('one side names a variable', 'built before variables exist'), + id='a-variable-inside-arithmetic', + ), + pytest.param( + { + 'constraints': {'x': {'dims': ['g'], 'expression': 'p <= c'}}, + 'assumptions': {'a': 'dual(x) * 2 > 0'}, + }, + ('one side reads a dual', 'test the data instead'), + id='a-dual-inside-arithmetic', + ), + pytest.param( + {'assumptions': {'a': 'tag * 2 > 0'}}, + ("'tag' is declared dtype: str, and an expression is arithmetic",), + id='a-label-inside-arithmetic', + ), + pytest.param( + {'assumptions': {'a': 'c / (k + 1) > 0'}}, + ('a divisor must be a single Constant/Parameter factor',), + id='a-divisor-that-adds', + ), + pytest.param( + {'assumptions': {'a': 'shift(c, along=g, offset=1) <= k'}}, + ('shift() over a variable-free expression leaves vacated positions with no value',), + id='a-translation-with-no-edge', + ), + pytest.param( + {'assumptions': {'a': 'c * nope > 0'}}, + ("'nope' not found",), + id='an-unknown-name-inside-arithmetic', + ), + ], + ) + def test_a_bad_assumption_is_refused_at_load(self, patch, fragments): + message = _refusal(**patch) + for fragment in fragments: + assert fragment in message + + @pytest.mark.parametrize( + ('patch', 'holds'), + [ + pytest.param({}, 'c >= 0', id='one-parameter-against-a-number'), + pytest.param({}, 'c <= k', id='two-numbers-of-different-dims'), + pytest.param({'parameters.n': {'dims': ['g'], 'dtype': 'int'}}, 'n < c', id='an-int-against-a-float'), + pytest.param({'parameters.tag2': {'dims': ['g'], 'dtype': 'str'}}, 'tag != tag2', id='two-labels'), + pytest.param({'parameters.flag2': {'dims': ['g'], 'dtype': 'bool'}}, 'flag == flag2', id='two-flags'), + pytest.param({}, "tag == 'gas'", id='a-label-against-a-literal'), + pytest.param({}, 'NOT flag OR c > 0', id='a-compound-predicate'), + pytest.param({}, 'k > 0', id='a-scalar'), + pytest.param({}, 'c <= 0.5 * k', id='arithmetic-on-a-side'), + pytest.param({'macros.half': {'args': ['x'], 'template': 'x / 2'}}, 'c <= half(k)', id='a-macro'), + pytest.param({'expressions.e': 'c * 2'}, 'e > 0', id='a-named-expression-on-the-left'), + pytest.param({'expressions.e': 'c * 2'}, 'k < e', id='a-named-expression-on-the-right'), + pytest.param({}, 'sum(c, over=g) >= k', id='a-reduction'), + pytest.param({'parameters.d': {'dims': ['h']}}, 'c <= at(d, by=lk)', id='a-pullback-through-a-lookup'), + pytest.param( + {}, + {'holds': 'c - shift(c, along=g, offset=1, edge=0) <= k', 'where': 'position(g) > 0'}, + id='a-translation', + ), + ], + ) + def test_an_assumption_about_the_data_loads(self, patch, holds): + spec = _schema(**patch, assumptions={'a': holds}) + assert list(spec.assumptions) == ['a'] + + def test_a_comparison_of_expressions_is_held_to_the_frame_it_sits_in(self): + message = _refusal( + **{ + 'parameters.d': {'dims': ['h']}, + 'constraints': {'cap': {'dims': ['g'], 'where': 'c > d * 2', 'expression': 'p <= c'}}, + } + ) + assert "a where-comparison of expressions reads dims ['h'] outside the frame ['g']" in message + + def test_a_case_comparing_expressions_is_refused_as_undecidable(self): + """Two cases split by arithmetic cannot be proved apart without the numbers, and the rewrite is named.""" + message = _refusal( + expressions={ + 'e': { + 'dims': ['g'], + 'cases': { + 'wide': {'when': 'c > 2 * k', 'expression': 'c'}, + 'narrow': {'when': 'c <= 2 * k', 'expression': 'k'}, + }, + 'otherwise': 0, + } + } + ) + assert 'cannot be told apart before the data arrives: it compares expressions' in message + assert 'precompute the test as a boolean parameter' in message + + def test_an_assumption_round_trips_in_the_form_it_was_written(self): + """A bare string stays a bare string, and a mapping stays a mapping, so `to_yaml` reproduces the file.""" + spec = _schema( + assumptions={'bare': 'c > 0', 'masked': {'holds': 'c <= k', 'where': 'flag', 'description': 'why'}} + ) + assert to_spec(spec.to_dict()) == spec + assert spec.to_dict()['assumptions'] == { + 'bare': 'c > 0', + 'masked': {'holds': 'c <= k', 'where': 'flag', 'description': 'why'}, + }, 'each entry is written back in the form it arrived in' + + class TestArithmeticInAWhere: """What a comparison of expressions may say in a where, decided with no data bound.""" @@ -994,23 +1143,6 @@ def test_a_bad_comparison_of_expressions_is_refused_at_load(self, patch, fragmen for fragment in fragments: assert fragment in message - def test_a_case_comparing_expressions_is_refused_as_undecidable(self): - """Two cases split by arithmetic cannot be proved apart without the numbers, and the rewrite is named.""" - message = _refusal( - expressions={ - 'e': { - 'dims': ['g'], - 'cases': { - 'wide': {'when': 'c > 2 * k', 'expression': 'c'}, - 'narrow': {'when': 'c <= 2 * k', 'expression': 'k'}, - }, - 'otherwise': 0, - } - } - ) - assert 'cannot be told apart before the data arrives: it compares expressions' in message - assert 'precompute the test as a boolean parameter' in message - class TestTheFrontDoor: def test_a_list_of_models_is_not_a_model(self): diff --git a/tests/typesetting/golden/latex.out b/tests/typesetting/golden/latex.out index d94a1940..40f527c6 100644 --- a/tests/typesetting/golden/latex.out +++ b/tests/typesetting/golden/latex.out @@ -15,6 +15,7 @@ \item[{$\mathcal{Z}$}] index $z$ --- \texttt{zone} with $\mathrm{zone\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{area\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{gen\_zone}: \mathcal{G} \times \mathcal{T} \to \mathcal{Z}$ \item[{$\mathcal{S}$}] index $s$ --- \texttt{season} with $\mathrm{season\_of}: \mathcal{T} \to \mathcal{S}$ \item[{$\mathcal{E}$}] index $e$ --- \texttt{technology} with $\mathrm{gen\_tech}: \mathcal{G} \to \mathcal{E},\ \mathrm{gen\_bt}: \mathcal{G} \to \mathcal{B} \times \mathcal{E}$ +\item[{$\mathcal{A}$}] index $a$ --- \texttt{bp} \end{description} \paragraph{Parameters} @@ -31,6 +32,13 @@ \item[{$\mathrm{lead}$}] \texttt{lead} over $\mathcal{G}$ \item[{$\mathrm{budget}$}] \texttt{budget} (scalar) \item[{$\mathrm{growth}$}] \texttt{growth} (scalar) +\item[{$\mathrm{bp\_x}$}] \texttt{bp\_x} over $\mathcal{G} \times \mathcal{A}$ +\item[{$\mathrm{bp\_y}$}] \texttt{bp\_y} over $\mathcal{G} \times \mathcal{A}$ +\item[{$\mathrm{fuel\_bp}$}] \texttt{fuel\_bp} over $\mathcal{A}$ +\item[{$\mathrm{heat}^{\mathrm{bp}}$}] \texttt{heat\_bp} over $\mathcal{A}$ +\item[{$\mathrm{cost}^{\mathrm{curve,points}}$}] \texttt{cost\_curve\_points} over $\mathcal{G} \times \mathcal{A}$ --- where 'bp\_x' has a row, and so where the curve runs +\item[{$\mathrm{cost}^{\mathrm{curve,starts}}$}] \texttt{cost\_curve\_starts} over $\mathcal{G} \times \mathcal{A}$ --- the first breakpoint of each curve +\item[{$\mathrm{cost}^{\mathrm{curve,ends}}$}] \texttt{cost\_curve\_ends} over $\mathcal{G} \times \mathcal{A}$ --- the last breakpoint of each curve \end{description} \paragraph{Variables} @@ -45,6 +53,8 @@ \item[{$\mathit{reserve}$}] \texttt{reserve} (scalar) \item[{$\mathit{headroom}$}] \texttt{headroom} (scalar) \item[{$\mathit{weight}$}] \texttt{weight} over $\mathcal{T} \times \mathcal{G}$ +\item[{$\mathit{op\_cost}$}] \texttt{op\_cost} over $\mathcal{T} \times \mathcal{G}$ +\item[{$\mathit{heat}$}] \texttt{heat} over $\mathcal{T} \times \mathcal{G}$ \end{description} \paragraph{Definitions} @@ -119,7 +129,13 @@ \text{margin} && p_{t,g} & \le \mathrm{p}^{\mathrm{max}}_{g} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{p}^{\mathrm{max}}_{g} - \mathrm{p}^{\mathrm{min}}_{g} > \frac{\mathrm{cost}_{g}}{2} \\ \text{ramped} && \mathit{slack}_{t} & \le \mathrm{load}_{t,b} && \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} \le \mathrm{zone\_cap}_{\mathrm{zone\_of}(b)} \wedge \mathrm{pos}(t) > 0 \\ \text{covered} && \sum_{t \in \mathcal{T},\ g \in \mathcal{G}} p_{t,g} & \le \mathrm{budget} && \text{where } \sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} \ge \mathrm{budget} \\ -\text{capped} && p_{t,g} & \le \mathrm{p}^{\mathrm{max}}_{g} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} +\text{capped} && p_{t,g} & \le \mathrm{p}^{\mathrm{max}}_{g} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} \\ +\text{cost\_curve\_chord} && \mathit{op\_cost}_{t,g} \cdot \left( \mathrm{bp\_x}_{g,a} - \mathrm{bp\_x}_{g,a \boxminus_{0} 1} \right) & \ge \left( \mathrm{bp\_y}_{g,a} - \mathrm{bp\_y}_{g,a \boxminus_{0} 1} \right) \cdot \left( p_{t,g} - \mathrm{bp\_x}_{g,a} \right) + \mathrm{bp\_y}_{g,a} \cdot \left( \mathrm{bp\_x}_{g,a} - \mathrm{bp\_x}_{g,a \boxminus_{0} 1} \right) && \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,points}}_{g,a} \wedge \neg \mathrm{cost}^{\mathrm{curve,starts}}_{g,a} \\ +\text{cost\_curve\_domain\_lo} && p_{t,g} & \ge \mathrm{bp\_x}_{g,a} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,starts}}_{g,a} \\ +\text{cost\_curve\_domain\_hi} && p_{t,g} & \le \mathrm{bp\_x}_{g,a} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,ends}}_{g,a} \\ +\text{heat\_curve\_chord} && \mathit{heat}_{t,g} \cdot \left( \mathrm{fuel\_bp}_{a} - \mathrm{fuel\_bp}_{a \boxminus_{0} 1} \right) & \le \left( \mathrm{heat}^{\mathrm{bp}}_{a} - \mathrm{heat}^{\mathrm{bp}}_{a \boxminus_{0} 1} \right) \cdot \left( p_{t,g} - \mathrm{fuel\_bp}_{a} \right) + \mathrm{heat}^{\mathrm{bp}}_{a} \cdot \left( \mathrm{fuel\_bp}_{a} - \mathrm{fuel\_bp}_{a \boxminus_{0} 1} \right) && \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) \neq 0 \\ +\text{heat\_curve\_domain\_lo} && p_{t,g} & \ge \mathrm{fuel\_bp}_{a} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) = 0 \\ +\text{heat\_curve\_domain\_hi} && p_{t,g} & \le \mathrm{fuel\_bp}_{a} && \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) = \lvert \mathcal{A} \rvert - 1 \end{align} \paragraph{Definitions} @@ -143,7 +159,28 @@ \text{reserve} && \mathit{reserve} & \ge 0 \\ \text{headroom} && \mathit{headroom} & \ge 0 && \text{where } \mathrm{budget} \text{ is defined} \\ \text{weight} && 0 \le \mathit{weight}_{t,g} & \le 1 && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \\ -\text{weight sos} && \left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} & \in \mathrm{SOS}2 && \forall\, t \in \mathcal{T} +\text{weight sos} && \left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} & \in \mathrm{SOS}2 && \forall\, t \in \mathcal{T} \\ +\text{op\_cost} && \mathit{op\_cost}_{t,g} & \ge 0 && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \\ +\text{heat} && \mathit{heat}_{t,g} & \ge 0 && \forall\, t \in \mathcal{T},\ g \in \mathcal{G} +\end{align} + +\paragraph{Assumptions} +\begin{align} +\text{capacity\_is\_nonnegative} && \mathrm{p}^{\mathrm{max}}_{g} & \ge 0 && \forall\, g \in \mathcal{G} \\ +\text{bounds\_are\_ordered} && \mathrm{p}^{\mathrm{min}}_{g} & \le \mathrm{p}^{\mathrm{max}}_{g} && \forall\, g \in \mathcal{G} \,:\, \mathrm{p}^{\mathrm{min}}_{g} \text{ is defined} \\ +\text{budget\_is\_positive} && \mathrm{budget} & > 0 \\ +\text{flexible\_units\_are\_cheap} && \neg \mathrm{is\_flexible}_{g} \vee \mathrm{cost}_{g} \le \mathrm{budget} & && \forall\, g \in \mathcal{G} \\ +\text{floor\_is\_half\_the\_capacity} && \mathrm{p}^{\mathrm{min}}_{g} & \le 0.5 \cdot \mathrm{p}^{\mathrm{max}}_{g} && \forall\, g \in \mathcal{G} \\ +\text{load\_ramps\_within\_the\_zone\_cap} && \mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} & \le \mathrm{zone\_cap}_{\mathrm{zone\_of}(b)} && \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{pos}(t) > 0 \\ +\text{fleet\_covers\_the\_budget} && \sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} & \ge \mathrm{budget} \\ +\text{cheap\_when\_spent} && \mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} & && \forall\, g \in \mathcal{G} \\ +\text{cost\_curve increasing} && \mathrm{bp\_x}_{g,a - 1} & < \mathrm{bp\_x}_{g,a} && \forall\, g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,points}}_{g,a} \wedge \mathrm{cost}^{\mathrm{curve,points}}_{g,a - 1} \\ +\text{cost\_curve curvature} && \mathrm{bp\_y}_{g,a} & \text{ is a convex function of } \mathrm{bp\_x}_{g,a} \text{ along } a && \forall\, g \in \mathcal{G} \\ +\text{cost\_curve breakpoints} && \lvert \{ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,points}}_{g,a} \} \rvert & \ge 2 && \forall\, g \in \mathcal{G} \\ +\text{cost\_curve points} && \{ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,points}}_{g,a} \} & \text{ is one run of consecutive breakpoints} && \forall\, g \in \mathcal{G} \\ +\text{heat\_curve increasing} && \mathrm{fuel\_bp}_{a - 1} & < \mathrm{fuel\_bp}_{a} && \forall\, a \in \mathcal{A} \\ +\text{heat\_curve curvature} && \mathrm{heat}^{\mathrm{bp}}_{a} & \text{ is a concave function of } \mathrm{fuel\_bp}_{a} \text{ along } a \\ +\text{heat\_curve breakpoints} && \lvert \mathcal{A} \rvert & \ge 2 \end{align} \end{document} diff --git a/tests/typesetting/golden/markdown.out b/tests/typesetting/golden/markdown.out index 80ad5e1a..d993a136 100644 --- a/tests/typesetting/golden/markdown.out +++ b/tests/typesetting/golden/markdown.out @@ -12,6 +12,7 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 | $`\mathcal{Z}`$ | index $`z`$ — `zone` with $`\mathrm{zone\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{area\_of}: \mathcal{B} \to \mathcal{Z},\ \mathrm{gen\_zone}: \mathcal{G} \times \mathcal{T} \to \mathcal{Z}`$ | | $`\mathcal{S}`$ | index $`s`$ — `season` with $`\mathrm{season\_of}: \mathcal{T} \to \mathcal{S}`$ | | $`\mathcal{E}`$ | index $`e`$ — `technology` with $`\mathrm{gen\_tech}: \mathcal{G} \to \mathcal{E},\ \mathrm{gen\_bt}: \mathcal{G} \to \mathcal{B} \times \mathcal{E}`$ | +| $`\mathcal{A}`$ | index $`a`$ — `bp` | #### Parameters @@ -29,6 +30,13 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 | $`\mathrm{lead}`$ | `lead` over $`\mathcal{G}`$ | | $`\mathrm{budget}`$ | `budget` (scalar) | | $`\mathrm{growth}`$ | `growth` (scalar) | +| $`\mathrm{bp\_x}`$ | `bp_x` over $`\mathcal{G} \times \mathcal{A}`$ | +| $`\mathrm{bp\_y}`$ | `bp_y` over $`\mathcal{G} \times \mathcal{A}`$ | +| $`\mathrm{fuel\_bp}`$ | `fuel_bp` over $`\mathcal{A}`$ | +| $`\mathrm{heat}^{\mathrm{bp}}`$ | `heat_bp` over $`\mathcal{A}`$ | +| $`\mathrm{cost}^{\mathrm{curve,points}}`$ | `cost_curve_points` over $`\mathcal{G} \times \mathcal{A}`$ — where 'bp\_x' has a row, and so where the curve runs | +| $`\mathrm{cost}^{\mathrm{curve,starts}}`$ | `cost_curve_starts` over $`\mathcal{G} \times \mathcal{A}`$ — the first breakpoint of each curve | +| $`\mathrm{cost}^{\mathrm{curve,ends}}`$ | `cost_curve_ends` over $`\mathcal{G} \times \mathcal{A}`$ — the last breakpoint of each curve | #### Variables @@ -44,6 +52,8 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 | $`\mathit{reserve}`$ | `reserve` (scalar) | | $`\mathit{headroom}`$ | `headroom` (scalar) | | $`\mathit{weight}`$ | `weight` over $`\mathcal{T} \times \mathcal{G}`$ | +| $`\mathit{op\_cost}`$ | `op_cost` over $`\mathcal{T} \times \mathcal{G}`$ | +| $`\mathit{heat}`$ | `heat` over $`\mathcal{T} \times \mathcal{G}`$ | #### Definitions @@ -335,6 +345,42 @@ p_{t,g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, t \in \mathcal{T},\ g p_{t,g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} ``` +**`cost_curve_chord`** + +```math +\mathit{op\_cost}_{t,g} \cdot \left( \mathrm{bp\_x}_{g,a} - \mathrm{bp\_x}_{g,a \boxminus_{0} 1} \right) \ge \left( \mathrm{bp\_y}_{g,a} - \mathrm{bp\_y}_{g,a \boxminus_{0} 1} \right) \cdot \left( p_{t,g} - \mathrm{bp\_x}_{g,a} \right) + \mathrm{bp\_y}_{g,a} \cdot \left( \mathrm{bp\_x}_{g,a} - \mathrm{bp\_x}_{g,a \boxminus_{0} 1} \right) \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,points}}_{g,a} \wedge \neg \mathrm{cost}^{\mathrm{curve,starts}}_{g,a} +``` + +**`cost_curve_domain_lo`** + +```math +p_{t,g} \ge \mathrm{bp\_x}_{g,a} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,starts}}_{g,a} +``` + +**`cost_curve_domain_hi`** + +```math +p_{t,g} \le \mathrm{bp\_x}_{g,a} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,ends}}_{g,a} +``` + +**`heat_curve_chord`** + +```math +\mathit{heat}_{t,g} \cdot \left( \mathrm{fuel\_bp}_{a} - \mathrm{fuel\_bp}_{a \boxminus_{0} 1} \right) \le \left( \mathrm{heat}^{\mathrm{bp}}_{a} - \mathrm{heat}^{\mathrm{bp}}_{a \boxminus_{0} 1} \right) \cdot \left( p_{t,g} - \mathrm{fuel\_bp}_{a} \right) + \mathrm{heat}^{\mathrm{bp}}_{a} \cdot \left( \mathrm{fuel\_bp}_{a} - \mathrm{fuel\_bp}_{a \boxminus_{0} 1} \right) \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) \neq 0 +``` + +**`heat_curve_domain_lo`** + +```math +p_{t,g} \ge \mathrm{fuel\_bp}_{a} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) = 0 +``` + +**`heat_curve_domain_hi`** + +```math +p_{t,g} \le \mathrm{fuel\_bp}_{a} \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{pos}(a) = \lvert \mathcal{A} \rvert - 1 +``` + #### Definitions **`spend_cap`** @@ -434,3 +480,107 @@ p_{t,g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, t \in \mathcal{T},\ g ```math \left( \mathit{weight}_{t,g} \right)_{g \in \mathcal{G}} \in \mathrm{SOS}2 \qquad \forall\, t \in \mathcal{T} ``` + +**`op_cost`** + +```math +\mathit{op\_cost}_{t,g} \ge 0 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} +``` + +**`heat`** + +```math +\mathit{heat}_{t,g} \ge 0 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} +``` + +#### Assumptions + +**`capacity_is_nonnegative`** + +```math +\mathrm{p}^{\mathrm{max}}_{g} \ge 0 \qquad \forall\, g \in \mathcal{G} +``` + +**`bounds_are_ordered`** + +```math +\mathrm{p}^{\mathrm{min}}_{g} \le \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} \,:\, \mathrm{p}^{\mathrm{min}}_{g} \text{ is defined} +``` + +**`budget_is_positive`** + +```math +\mathrm{budget} > 0 +``` + +**`flexible_units_are_cheap`** + +```math +\neg \mathrm{is\_flexible}_{g} \vee \mathrm{cost}_{g} \le \mathrm{budget} \qquad \forall\, g \in \mathcal{G} +``` + +**`floor_is_half_the_capacity`** + +```math +\mathrm{p}^{\mathrm{min}}_{g} \le 0.5 \cdot \mathrm{p}^{\mathrm{max}}_{g} \qquad \forall\, g \in \mathcal{G} +``` + +**`load_ramps_within_the_zone_cap`** + +```math +\mathrm{load}_{t,b} - \mathrm{load}_{t \boxminus_{0} 1,b} \le \mathrm{zone\_cap}_{\mathrm{zone\_of}(b)} \qquad \forall\, t \in \mathcal{T},\ b \in \mathcal{B} \,:\, \mathrm{pos}(t) > 0 +``` + +**`fleet_covers_the_budget`** + +```math +\sum_{g \in \mathcal{G}} \mathrm{p}^{\mathrm{max}}_{g} \ge \mathrm{budget} +``` + +**`cheap_when_spent`** + +```math +\mathrm{spend}^{\mathrm{cap}}_{g} > 0 \vee \neg \mathrm{is\_flexible}_{g} \qquad \forall\, g \in \mathcal{G} +``` + +**`cost_curve increasing`** + +```math +\mathrm{bp\_x}_{g,a - 1} < \mathrm{bp\_x}_{g,a} \qquad \forall\, g \in \mathcal{G},\ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,points}}_{g,a} \wedge \mathrm{cost}^{\mathrm{curve,points}}_{g,a - 1} +``` + +**`cost_curve curvature`** + +```math +\mathrm{bp\_y}_{g,a} \text{ is a convex function of } \mathrm{bp\_x}_{g,a} \text{ along } a \qquad \forall\, g \in \mathcal{G} +``` + +**`cost_curve breakpoints`** + +```math +\lvert \{ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,points}}_{g,a} \} \rvert \ge 2 \qquad \forall\, g \in \mathcal{G} +``` + +**`cost_curve points`** + +```math +\{ a \in \mathcal{A} \,:\, \mathrm{cost}^{\mathrm{curve,points}}_{g,a} \} \text{ is one run of consecutive breakpoints} \qquad \forall\, g \in \mathcal{G} +``` + +**`heat_curve increasing`** + +```math +\mathrm{fuel\_bp}_{a - 1} < \mathrm{fuel\_bp}_{a} \qquad \forall\, a \in \mathcal{A} +``` + +**`heat_curve curvature`** + +```math +\mathrm{heat}^{\mathrm{bp}}_{a} \text{ is a concave function of } \mathrm{fuel\_bp}_{a} \text{ along } a +``` + +**`heat_curve breakpoints`** + +```math +\lvert \mathcal{A} \rvert \ge 2 +``` diff --git a/tests/typesetting/golden/model.yaml b/tests/typesetting/golden/model.yaml index 13a88b31..0786d31a 100644 --- a/tests/typesetting/golden/model.yaml +++ b/tests/typesetting/golden/model.yaml @@ -19,6 +19,7 @@ dimensions: zone: { dtype: str } season: { dtype: str } technology: { dtype: str } + bp: { dtype: int } relations: gen_bus: { columns: [generator, bus], key: generator } @@ -44,6 +45,10 @@ parameters: lead: { dims: [generator], dtype: int } budget: { dims: [] } # scalar: the legend says so rather than printing an empty product growth: { dims: [] } # the base of a power; the exponent is `lead`, a column + bp_x: { dims: [generator, bp] } # a curve's breakpoints, one curve per generator + bp_y: { dims: [generator, bp] } + fuel_bp: { dims: [bp] } # a second curve's breakpoints, one curve for every generator + heat_bp: { dims: [bp] } variables: p: # both bounds, and a where with all three connectives @@ -78,6 +83,27 @@ variables: weight: # the family a sos runs along dims: [snapshot, generator] bounds: { lower: 0, upper: 1 } + op_cost: # what a curve bounds below + dims: [snapshot, generator] + bounds: { lower: 0 } + heat: # what a second curve bounds above + dims: [snapshot, generator] + bounds: { lower: 0 } + +piecewise: + cost_curve: # a curve as its segment lines, masked by its own breakpoints: every check a curve can carry prints under Assumptions + over: bp + points: bp_x + method: lp + links: + - [p, bp_x] + - [op_cost, bp_y, ">="] + heat_curve: # the same method over every breakpoint, so the count is the set's own size and the curve bends the other way + over: bp + method: lp + links: + - [p, fuel_bp] + - [heat, heat_bp, "<="] sos: adjacent: # at most two adjacent members nonzero, one set per snapshot @@ -250,6 +276,20 @@ constraints: where: "spend_cap > 0 OR NOT is_flexible" expression: p <= p_max +assumptions: + capacity_is_nonnegative: p_max >= 0 # one comparison, so the line aligns on its relation + bounds_are_ordered: # two parameters compared coordinate by coordinate, checked where the narrower one is defined + holds: "p_min <= p_max" + where: "p_min" + budget_is_positive: budget > 0 # a scalar, so no quantifier + flexible_units_are_cheap: "NOT is_flexible OR cost <= budget" # a compound predicate, which no one relation aligns + floor_is_half_the_capacity: "p_min <= 0.5 * p_max" # arithmetic on a side, which reads as an expression does + load_ramps_within_the_zone_cap: # a translation under a comparison names its edge, and the where keeps the vacated row out + holds: "load - shift(load, along=snapshot, offset=1, edge=0) <= at(zone_cap, by=zone_of)" + where: "position(snapshot) > 0" + fleet_covers_the_budget: "sum(p_max, over=generator) >= budget" # a reduction on a side, so the frame is what is left + cheap_when_spent: "spend_cap > 0 OR NOT is_flexible" # an expressions: entry on a side, read by the name the file gave it + objective: # a sense, a product of two variables, a power over two parameters, a power of one of those, and the summations a scalar objective spells out beside two scalar terms sense: maximize expression: sum(p * cost) + sum(p * p * cost) + sum(p * cost * growth ** lead) + sum(p * (growth ** lead) ** 2) + sum(p * p_max) - reserve + -headroom diff --git a/tests/typesetting/golden/typst.out b/tests/typesetting/golden/typst.out index 4ff580d9..6b45f56a 100644 --- a/tests/typesetting/golden/typst.out +++ b/tests/typesetting/golden/typst.out @@ -10,6 +10,7 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 / $cal(Z)$: index $z$ --- `zone` with $upright("zone_of"): cal(B) arrow.r cal(Z), upright("area_of"): cal(B) arrow.r cal(Z), upright("gen_zone"): cal(G) times cal(T) arrow.r cal(Z)$ / $cal(S)$: index $s$ --- `season` with $upright("season_of"): cal(T) arrow.r cal(S)$ / $cal(E)$: index $e$ --- `technology` with $upright("gen_tech"): cal(G) arrow.r cal(E), upright("gen_bt"): cal(G) arrow.r cal(B) times cal(E)$ +/ $cal(A)$: index $a$ --- `bp` == Parameters / $upright("p")^(upright("max"))$: `p_max` over $cal(G)$ @@ -24,6 +25,13 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 / $upright("lead")$: `lead` over $cal(G)$ / $upright("budget")$: `budget` (scalar) / $upright("growth")$: `growth` (scalar) +/ $upright("bp_x")$: `bp_x` over $cal(G) times cal(A)$ +/ $upright("bp_y")$: `bp_y` over $cal(G) times cal(A)$ +/ $upright("fuel_bp")$: `fuel_bp` over $cal(A)$ +/ $upright("heat")^(upright("bp"))$: `heat_bp` over $cal(A)$ +/ $upright("cost")^(upright("curve,points"))$: `cost_curve_points` over $cal(G) times cal(A)$ --- where 'bp\_x' has a row, and so where the curve runs +/ $upright("cost")^(upright("curve,starts"))$: `cost_curve_starts` over $cal(G) times cal(A)$ --- the first breakpoint of each curve +/ $upright("cost")^(upright("curve,ends"))$: `cost_curve_ends` over $cal(G) times cal(A)$ --- the last breakpoint of each curve == Variables / $p$: `p` over $cal(T) times cal(G)$ @@ -36,6 +44,8 @@ every character a notation escapes, set as text: link\_to, 100% & \#1 costs \$5 / $italic("reserve")$: `reserve` (scalar) / $italic("headroom")$: `headroom` (scalar) / $italic("weight")$: `weight` over $cal(T) times cal(G)$ +/ $italic("op_cost")$: `op_cost` over $cal(T) times cal(G)$ +/ $italic("heat")$: `heat` over $cal(T) times cal(G)$ == Definitions / $upright("spend")^(upright("cap"))$: `spend_cap` over $cal(G)$ @@ -106,7 +116,13 @@ $ upright("budgeted") & italic("spend")_(t) & <= upright("budget") & forall t in upright("margin") & p_(t,g) & <= upright("p")^(upright("max"))_(g) & forall t in cal(T), g in cal(G) colon upright("p")^(upright("max"))_(g) - upright("p")^(upright("min"))_(g) > frac(upright("cost")_(g), 2) \ upright("ramped") & italic("slack")_(t) & <= upright("load")_(t,b) & forall t in cal(T), b in cal(B) colon upright("load")_(t,b) - upright("load")_(t minus.square_(0) 1,b) <= upright("zone_cap")_(upright("zone_of")(b)) and upright("pos")(t) > 0 \ upright("covered") & sum_(t in cal(T), g in cal(G)) p_(t,g) & <= upright("budget") & upright("where ") sum_(g in cal(G)) upright("p")^(upright("max"))_(g) >= upright("budget") \ - upright("capped") & p_(t,g) & <= upright("p")^(upright("max"))_(g) & forall t in cal(T), g in cal(G) colon upright("spend")^(upright("cap"))_(g) > 0 or not upright("is_flexible")_(g) $ + upright("capped") & p_(t,g) & <= upright("p")^(upright("max"))_(g) & forall t in cal(T), g in cal(G) colon upright("spend")^(upright("cap"))_(g) > 0 or not upright("is_flexible")_(g) \ + upright("cost_curve_chord") & italic("op_cost")_(t,g) dot (upright("bp_x")_(g,a) - upright("bp_x")_(g,a minus.square_(0) 1)) & >= (upright("bp_y")_(g,a) - upright("bp_y")_(g,a minus.square_(0) 1)) dot (p_(t,g) - upright("bp_x")_(g,a)) + upright("bp_y")_(g,a) dot (upright("bp_x")_(g,a) - upright("bp_x")_(g,a minus.square_(0) 1)) & forall t in cal(T), g in cal(G), a in cal(A) colon upright("cost")^(upright("curve,points"))_(g,a) and not upright("cost")^(upright("curve,starts"))_(g,a) \ + upright("cost_curve_domain_lo") & p_(t,g) & >= upright("bp_x")_(g,a) & forall t in cal(T), g in cal(G), a in cal(A) colon upright("cost")^(upright("curve,starts"))_(g,a) \ + upright("cost_curve_domain_hi") & p_(t,g) & <= upright("bp_x")_(g,a) & forall t in cal(T), g in cal(G), a in cal(A) colon upright("cost")^(upright("curve,ends"))_(g,a) \ + upright("heat_curve_chord") & italic("heat")_(t,g) dot (upright("fuel_bp")_(a) - upright("fuel_bp")_(a minus.square_(0) 1)) & <= (upright("heat")^(upright("bp"))_(a) - upright("heat")^(upright("bp"))_(a minus.square_(0) 1)) dot (p_(t,g) - upright("fuel_bp")_(a)) + upright("heat")^(upright("bp"))_(a) dot (upright("fuel_bp")_(a) - upright("fuel_bp")_(a minus.square_(0) 1)) & forall t in cal(T), g in cal(G), a in cal(A) colon upright("pos")(a) != 0 \ + upright("heat_curve_domain_lo") & p_(t,g) & >= upright("fuel_bp")_(a) & forall t in cal(T), g in cal(G), a in cal(A) colon upright("pos")(a) = 0 \ + upright("heat_curve_domain_hi") & p_(t,g) & <= upright("fuel_bp")_(a) & forall t in cal(T), g in cal(G), a in cal(A) colon upright("pos")(a) = abs(cal(A)) - 1 $ == Definitions #set math.equation(numbering: "(1)") @@ -128,4 +144,24 @@ $ upright("p") & upright("p")^(upright("min"))_(g) <= p_(t,g) & <= upright("p")^ upright("reserve") & italic("reserve") & >= 0 \ upright("headroom") & italic("headroom") & >= 0 & upright("where ") upright("budget") upright(" is defined") \ upright("weight") & 0 <= italic("weight")_(t,g) & <= 1 & forall t in cal(T), g in cal(G) \ - upright("weight sos") & (italic("weight")_(t,g))_(g in cal(G)) & in upright("SOS")2 & forall t in cal(T) $ + upright("weight sos") & (italic("weight")_(t,g))_(g in cal(G)) & in upright("SOS")2 & forall t in cal(T) \ + upright("op_cost") & italic("op_cost")_(t,g) & >= 0 & forall t in cal(T), g in cal(G) \ + upright("heat") & italic("heat")_(t,g) & >= 0 & forall t in cal(T), g in cal(G) $ + +== Assumptions +#set math.equation(numbering: "(1)") +$ upright("capacity_is_nonnegative") & upright("p")^(upright("max"))_(g) & >= 0 & forall g in cal(G) \ + upright("bounds_are_ordered") & upright("p")^(upright("min"))_(g) & <= upright("p")^(upright("max"))_(g) & forall g in cal(G) colon upright("p")^(upright("min"))_(g) upright(" is defined") \ + upright("budget_is_positive") & upright("budget") & > 0 \ + upright("flexible_units_are_cheap") & not upright("is_flexible")_(g) or upright("cost")_(g) <= upright("budget") & & forall g in cal(G) \ + upright("floor_is_half_the_capacity") & upright("p")^(upright("min"))_(g) & <= 0.5 dot upright("p")^(upright("max"))_(g) & forall g in cal(G) \ + upright("load_ramps_within_the_zone_cap") & upright("load")_(t,b) - upright("load")_(t minus.square_(0) 1,b) & <= upright("zone_cap")_(upright("zone_of")(b)) & forall t in cal(T), b in cal(B) colon upright("pos")(t) > 0 \ + upright("fleet_covers_the_budget") & sum_(g in cal(G)) upright("p")^(upright("max"))_(g) & >= upright("budget") \ + upright("cheap_when_spent") & upright("spend")^(upright("cap"))_(g) > 0 or not upright("is_flexible")_(g) & & forall g in cal(G) \ + upright("cost_curve increasing") & upright("bp_x")_(g,a - 1) & < upright("bp_x")_(g,a) & forall g in cal(G), a in cal(A) colon upright("cost")^(upright("curve,points"))_(g,a) and upright("cost")^(upright("curve,points"))_(g,a - 1) \ + upright("cost_curve curvature") & upright("bp_y")_(g,a) & upright(" is a convex function of ") upright("bp_x")_(g,a) upright(" along ") a & forall g in cal(G) \ + upright("cost_curve breakpoints") & abs({a in cal(A) colon upright("cost")^(upright("curve,points"))_(g,a)}) & >= 2 & forall g in cal(G) \ + upright("cost_curve points") & {a in cal(A) colon upright("cost")^(upright("curve,points"))_(g,a)} & upright(" is one run of consecutive breakpoints") & forall g in cal(G) \ + upright("heat_curve increasing") & upright("fuel_bp")_(a - 1) & < upright("fuel_bp")_(a) & forall a in cal(A) \ + upright("heat_curve curvature") & upright("heat")^(upright("bp"))_(a) & upright(" is a concave function of ") upright("fuel_bp")_(a) upright(" along ") a \ + upright("heat_curve breakpoints") & abs(cal(A)) & >= 2 $ diff --git a/tests/typesetting/test_declaration.py b/tests/typesetting/test_declaration.py index d1872884..908a19e7 100644 --- a/tests/typesetting/test_declaration.py +++ b/tests/typesetting/test_declaration.py @@ -127,15 +127,25 @@ def test_a_body_naming_another_expression_inlines_it_on_its_own_and_names_it_in_ @pytest.mark.parametrize( ('name', 'match'), [ - pytest.param('spent', r"'spent' is not a named expression, constraint or variable.*spend", id='a-near-miss'), + pytest.param( + 'spent', r"'spent' is not a named expression, constraint, assumption or variable.*spend", id='a-near-miss' + ), pytest.param('objective', r"'objective' is not a named expression", id='the-objective-has-no-name'), ], ) -def test_a_name_declared_as_none_of_the_three_is_refused(name: str, match: str): +def test_a_name_declared_as_none_of_the_four_is_refused(name: str, match: str): with pytest.raises(SchemaError, match=match): typeset_declaration(PLAIN, name, 'latex') +def test_an_assumption_prints_as_the_line_the_document_prints_for_it(): + """The frame is every dim either mask names, so a `where` over another dim widens the quantifier.""" + model = override(PLAIN, assumptions={'affordable': {'holds': 'cost <= 10', 'where': 'load > 0'}}) + assert typeset_declaration(model, 'affordable', 'latex') == ( + r'\mathrm{cost}_{g} \le 10 \qquad \forall\, t \in \mathcal{T},\ g \in \mathcal{G} \,:\, \mathrm{load}_{t} > 0' + ) + + def test_a_name_shared_by_a_constraint_and_a_variable_is_refused_rather_than_guessed(): """Constraints sit outside the flat namespace, so the model admits the pair; one line prints one of them.""" model = override(PLAIN, **{'constraints.p': {'dims': ['snapshot', 'generator'], 'expression': 'p <= 1'}}) diff --git a/tests/typesetting/test_golden.py b/tests/typesetting/test_golden.py index c40e8af1..4a8c0194 100644 --- a/tests/typesetting/test_golden.py +++ b/tests/typesetting/test_golden.py @@ -129,6 +129,10 @@ def _rendered_trees() -> Iterator[object]: for mask in resolved.variables.values(): if mask is not None: yield mask.root + for holds, where in resolved.assumptions.values(): + yield holds.root + if where is not None: + yield where.root yield from resolved.expressions.values() @@ -189,7 +193,8 @@ def test_the_golden_model_calls_every_operator_in_the_language(): #: What the fixture cannot reach, by the source text of the line. The guards #: are what the walk raises when resolution hands it something it types away, -#: so a model reaching one is a bug upstream. The absent objective is the arm a +#: so a model reaching one is a bug upstream; the closing arm over a curve's +#: checks is the same guard on the closed ``Check`` union. The absent objective is the arm a #: *different* model takes — a file declares at most one — and #: `test_a_model_with_no_objective_prints_the_rest` covers it. UNREACHABLE = { @@ -201,6 +206,8 @@ def test_the_golden_model_calls_every_operator_in_the_language(): "msg = f'{context}: expected a comparison, got {type(node).__name__}'", 'raise AssertionError(msg)', 'assert_never(node)', + 'case _:', + 'assert_never(check)', 'if block is None:', 'return []', } @@ -226,7 +233,7 @@ def test_the_golden_model_reaches_every_line_of_the_walk(tmp_path: Path): 'to_latex(model)\n' 'to_latex(model, inline_expressions=True)\n' 'spec = to_spec(model)\n' - 'for name in (*spec.expressions, *spec.constraints, *spec.variables):\n' + 'for name in (*spec.expressions, *spec.constraints, *spec.assumptions, *spec.variables):\n' " typeset_declaration(model, name, 'latex')\n" ) subprocess.run( diff --git a/tests/typesetting/test_walk.py b/tests/typesetting/test_walk.py index 57aac9b8..40effda5 100644 --- a/tests/typesetting/test_walk.py +++ b/tests/typesetting/test_walk.py @@ -18,6 +18,7 @@ from math_spec.typesetting.symbols import Symbols, _derive_name_symbol, chosen_expressions from math_spec.validation import to_spec from tests.fixtures import DISPATCH_MODEL, OPERATOR_PROBES, override +from tests.test_piecewise import LP, LP_MASKED from tests.typesetting import golden from tests.typesetting.fixtures import EVERY_FORMAT, LATEX @@ -761,11 +762,58 @@ def test_a_string_value_in_a_where_prints_as_a_quoted_label(name: FormatName, fm assert fmt.prose('gas_ccgt') not in unquoted, 'a string value is data, never words inside math' +@EVERY_FORMAT +def test_an_assumption_prints_under_its_own_heading_quantified_over_its_frame(name: FormatName, fmt: Format): + """What the data is held to prints last, after what the solver decides, one line per entry. + + A predicate that is one comparison splits on its relation as a constraint + does; its `where` sits on the quantifier as a constraint's does. + """ + model = override( + DISPATCH_MODEL, + assumptions={'ordered': {'holds': 'cost <= p_max', 'where': 'cost'}, 'positive': 'cost > 0'}, + ) + text = typeset(model, name, legend=False) + assert text.index('Variable domains') < text.index('Assumptions'), 'the section comes after the domains' + cost = fmt.subscript(fmt.upright('cost'), ['g']) + p_max = fmt.subscript(fmt.superscript(fmt.upright('p'), fmt.upright('max')), ['g']) + section = text[text.index('Assumptions') :] + [ordered] = [line for line in section.splitlines() if f'{fmt.operators["le"]} {p_max}' in line] + assert cost in ordered and ordered.index(cost) < ordered.index(fmt.operators['le']), 'the relation splits the line' + assert fmt.operators['such_that'] in ordered and fmt.prose(' is defined') in ordered, ( + 'the where is the condition on the quantifier' + ) + assert f'{fmt.operators["gt"]} 0' in section + + +@EVERY_FORMAT +def test_a_curve_prints_what_it_assumes_of_its_breakpoints(name: FormatName, fmt: Format): + """The checks a `piecewise:` block carries print beside the author's, under the block's name.""" + text = typeset(LP_MASKED, name, legend=False) + section = text[text.index('Assumptions') :] + for kind in ('increasing', 'curvature', 'breakpoints', 'points'): + assert f'curve {kind}' in section, 'every check the block carries prints as a line labelled by the block' + bp_x = fmt.upright('bp_x') + [increasing] = [line for line in section.splitlines() if fmt.subscript(bp_x, ['b - 1']) in line] + assert f'{fmt.operators["lt"]} {fmt.subscript(bp_x, ["b"])}' in increasing, ( + 'strictly increasing breakpoints are an inequality between neighbours' + ) + assert fmt.prose(' is a convex function of ') in section, 'the shape lp is exact for, as a paper writes it' + assert f'{fmt.operators["ge"]} 2' in section + + unmasked = typeset(LP, name, legend=False) + unmasked = unmasked[unmasked.index('Assumptions') :] + assert fmt.cardinality(fmt.script('B')) in unmasked and f'{fmt.operators["ge"]} 2' in unmasked, ( + 'with no mask the count is the size of the breakpoint set itself' + ) + assert 'curve points' not in unmasked, 'nothing to be contiguous without a mask' + + @EVERY_FORMAT def test_a_comparison_of_expressions_prints_as_the_arithmetic_it_is(name: FormatName, fmt: Format): - """`cost <= p_max / 2` on a quantifier renders each side as an expression, around the relation.""" - model = override(DISPATCH_MODEL, **{'variables.p.where': 'cost <= p_max / 2'}) + """`p_min <= 0.5 * p_max` aligns on its relation like any comparison, each side rendered as an expression.""" + model = override(DISPATCH_MODEL, assumptions={'half': 'cost <= p_max / 2'}) text = typeset(model, name, legend=False) + section = text[text.index('Assumptions') :] p_max = fmt.subscript(fmt.superscript(fmt.upright('p'), fmt.upright('max')), ['g']) - cost = fmt.subscript(fmt.upright('cost'), ['g']) - assert f'{cost} {fmt.operators["le"]} {fmt.fraction(p_max, "2")}' in text + assert f'{fmt.operators["le"]} {fmt.fraction(p_max, "2")}' in section diff --git a/tools/gallery.py b/tools/gallery.py index 14a4a1ec..fc376145 100644 --- a/tools/gallery.py +++ b/tools/gallery.py @@ -111,6 +111,7 @@ def declared_block(path: Path) -> str: equation = equations(_section(page, 'Subject to')) definition = equations(_section(page[page.index('#### Objective') :], 'Definitions')) if model.expressions else {} domains = _section(page, 'Variable domains').strip() + assumption = equations(_section(page, 'Assumptions')) if model.assumptions else {} parts = [legend, f'### Objective\n\n```yaml\n{declaration(text, "objective")}\n```\n\n{objective}'] for name, block in model.constraints.items(): parts.append( @@ -124,6 +125,13 @@ def declared_block(path: Path) -> str: for name in model.expressions ) parts.append(domains) + parts.extend( + f'### `{_stands_for(name, block.description)}`\n\n' + f'`{name}`\n\n' + f'```yaml\n{declaration(text, "assumptions", name)}\n```\n\n' + f'{assumption[name]}' + for name, block in model.assumptions.items() + ) return '\n\n'.join(parts) diff --git a/tools/notation.py b/tools/notation.py index affe89ef..62002c68 100644 --- a/tools/notation.py +++ b/tools/notation.py @@ -55,6 +55,7 @@ 'constraints': 'Constraints', 'expressions': 'Definitions', 'variables': 'Variable domains', + 'assumptions': 'Assumptions', 'piecewise': 'Curves, as what they expand to', 'sos': 'Sets carried to the solver', } @@ -262,15 +263,16 @@ def _labels(declaration: Declaration, printed: dict[str, str]) -> list[str]: Two blocks do not print under their own name. A ``sos:`` block restricts a variable, so its line sits with that variable; a ``piecewise:`` block is sugar, and what prints is the rows and columns it expands to — every one of - which the expander names after the block. A declaration printing nothing is - an error rather than an empty row: it means the walk stopped rendering - something the file still declares. + which the expander names after the block — and, under Assumptions, what + the block assumes of its breakpoints, labelled `` ``. A + declaration printing nothing is an error rather than an empty row: it + means the walk stopped rendering something the file still declares. """ if declaration.name in printed: return [declaration.name] if (variable := declaration.field('variable')) and f'{variable} sos' in printed: return [f'{variable} sos'] - expanded = [label for label in printed if label.startswith(f'{declaration.name}_')] + expanded = [label for label in printed if label.startswith((f'{declaration.name}_', f'{declaration.name} '))] assert expanded, f'{declaration.name} declares math and the walk printed none of it' return expanded