# lawref.evaluator.solver

*module*

Решатель: подстановка, свёртка термов и перебор — SPEC [§103](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#103-strict-closure)/[§190](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/27-part-xxvi-static-semantics-and-diagnostics.ru.md#190-rule-safety)/[§204](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/28-part-xxvii-canonical-legal-ir.ru.md#204-canonical-rule).

Модуль держит цикл взаимной рекурсии целиком, и разрывать его нельзя:
`solve` → `guard_value` (гард [§58](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#58-arithmetic)) → `resolve_aggregates` ([§59](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#59-aggregates)) →
`materialize_comprehension` ([§52.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#521-finite-relation-comprehensions)) → `solve`. Агрегат в теле правила
материализуется тем же перебором, который его и вызвал, поэтому четвёрка
живёт в одном модуле.

## lawref.evaluator.solver.NoBranchSelected

*class*

```python
class NoBranchSelected(Exception)
```

Bases: `Exception`

[§56](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#56-conditional-expression): опора условия NEITHER — ветвь не выбрана, значения у терма нет.

Не ошибка вычисления: причина (missing input [§64.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#641-lifting-data-boolean-в-formula), недостаточность границ
[§64.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#642-отношение-округления-над-сертифицированными-границами-errata-e-0136)) уже записана чтением опоры, и подменять её своей — значит потерять
настоящую. Кандидат просто не даёт факта.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L1112-L1121)

### lawref.evaluator.solver.NoBranchSelected.where

*attribute* · *instance attribute*

```python
where = where
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L1121-L1121)

## lawref.evaluator.solver.RangeRestrictionError

*class*

```python
class RangeRestrictionError(Exception)
```

Bases: `Exception`

[§190](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/27-part-xxvi-static-semantics-and-diagnostics.ru.md#190-rule-safety) нарушен САМОЙ программой: переменная головы не связана телом.

Отдельный класс, а не `values.ValueError_`: тот несёт ошибку ВЫЧИСЛЕНИЯ
терма, и вызывающие превращают его в issue конкретного применения правила
(«деление на ноль в гарде»). Здесь дефектен не вход, а программа —
правило, которое `lawc check` обязан был отвергнуть кодом LDC-E4101 ещё до
lowering-а ([§190](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/27-part-xxvi-static-semantics-and-diagnostics.ru.md#190-rule-safety): «head variables bound»). Слить их значило бы объявить
непригодную программу невезучим делом.

До 02.09.2026 своего класса не было, и такая программа роняла оракул
голым `KeyError: 'v0'` из `substitute` — сообщением, не называющим ни
правила, ни §-ссылки, ни того, что дефект статический. Падение уносило
ВЕСЬ прогон (`run_kz_regression.py`), а не один сценарий. Класс ловится
статикой с той же даты (T168/T169, errata E-0099); диагностика здесь —
вторая линия для CLIR, собранного до ужесточения либо написанного руками.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L21-L42)

### lawref.evaluator.solver.RangeRestrictionError.code

*attribute* · *instance attribute*

```python
code = code
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L41-L41)

### lawref.evaluator.solver.RangeRestrictionError.message

*attribute* · *instance attribute*

```python
message = message
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L42-L42)

## lawref.evaluator.solver.body_argument

*function*

```python
def body_argument(term: dict, subst: dict[str, dict], where: str, env: Any, store: 'SupportStore', registry: Any = None, premises: list[str] | None = None) -> dict
```

[§56](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#56-conditional-expression)/E-0180: select the branch before substituting a body argument.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L285-L291)

## lawref.evaluator.solver.body_literal

*function*

```python
def body_literal(literal: dict, subst: dict[str, dict], store: 'SupportStore', env: Any = None, registry: Any = None, premises: list[str] | None = None) -> dict
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L294-L299)

## lawref.evaluator.solver.comprehension_branches

*function*

```python
def comprehension_branches(comp: dict) -> list[list[tuple[str, dict]]]
```

Ветви generator-а с проверкой [§190](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/27-part-xxvi-static-semantics-and-diagnostics.ru.md#190-rule-safety) для КАЖДОЙ ветви (errata E-0219):
переменная comprehension и все binder-ы связаны позитивным литералом
ветви. Для одной ветви проверки нет — прежнее поведение не меняется
(несвязанную переменную там называет сам `solve`).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L454-L475)

## lawref.evaluator.solver.flatten_body

*function*

```python
def flatten_body(formula: dict) -> list[tuple[str, dict]]
```

Body → список конъюнктов-пар (status, literal).

status ∈ {"established", "not_known", "guard"}: Literal — implicit
established [§66](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#66-rule-body-default), StatusFormula established — [§204](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/28-part-xxvii-canonical-legal-ir.ru.md#204-canonical-rule) canonical form,
StatusFormula not_known — default negation [§113](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#113-default-negation) (истинен при NEITHER,
проверяется после завершения producer stratum), ComparisonTerm [§57](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#57-equality)/[§58](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#58-arithmetic) —
guard: терм-условие без опоры в store (у сравнения нет support-пары, оно
проверяется на связанных переменных); StatusFormula supported — [§65](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#65-status-tests)
(МОНОТОННЫЙ статус: истинен при любой positive-опоре, включая BOTH — T005;
единственный вид, которому [§103](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#103-strict-closure)/[§110](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#110-stratification) разрешают циклы). Прочие статусные
виды — ValueError → правило пропускается с issue NON_EXECUTABLE.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L360-L410)

## lawref.evaluator.solver.formula_support

*function*

```python
def formula_support(formula: dict, subst: dict[str, dict], store: SupportStore, registry: 'ProofRegistry | None', premises: list[str], env: Any = None) -> tuple[bool, bool]
```

Пара (t, f) формулы [§62](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#62-support-pair) под подстановкой — то, над чем [§52](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#52-finite-domains) определяет
квантор. От `flatten_body` отличается уровнем: там конъюнкт тела правила
уже свёрнут rule-body default [§66](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#66-rule-body-default) до «сработало/нет», здесь формула
сохраняет все четыре значения, потому что один conflicted элемент обязан
доехать до агрегированного BOTH.

Опоры прочитанных литералов копятся в `premises`: у квантора своей
support-пары в store нет, но факты, по которым он вычислен, — законные
посылки доказательства.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L664-L738)

## lawref.evaluator.solver.free_vars

*function*

```python
def free_vars(item: Any) -> list[str]
```

Свободные переменные формулы/терма — список из кэша, НЕ мутировать.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L504-L514)

## lawref.evaluator.solver.generator_branches

*function*

```python
def generator_branches(formula: dict) -> list[list[tuple[str, dict]]]
```

Generator comprehension [§52.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#521-finite-relation-comprehensions) → ветви ДНФ (errata E-0219).

Generator — Boolean-комбинация status tests ([§207.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/28-part-xxvii-canonical-legal-ir.ru.md#2071-formula-normalization): голый литерал есть
`established(P)`), поэтому `or` в нём исполняется ветвями: дистрибуция
`and` над `or` слева направо, операнды — в порядке канонического узла
[§207.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/28-part-xxvii-canonical-legal-ir.ru.md#2071-formula-normalization). Лист, не являющийся связкой, разбирает `flatten_body` — его
ValueError и есть отказ «вне подмножества». Формула без `or` даёт ровно
одну ветвь, равную `flatten_body` (прежний путь байт в байт).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L413-L435)

## lawref.evaluator.solver.generator_literals

*function*

```python
def generator_literals(formula: dict) -> list[tuple[str, dict]]
```

Конъюнкты-листья generator-а в порядке узла, без повторов ДНФ: для
чтений [§110](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#110-stratification)/[§111](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#111-порядок-evaluation-strata) развёртка не нужна, нужен состав листьев (E-0219).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L438-L447)

## lawref.evaluator.solver.ground_or_witness

*function*

```python
def ground_or_witness(literal: dict, subst: dict[str, dict], store: 'SupportStore', env: Any = None, registry: Any = None, premises: list[str] | None = None, status: str = 'established') -> dict | None
```

Ground-литерал посылки: подстановка, а у литерала с `_` — свидетель
существования ([§98](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/15-part-xiv-rules.ru.md#98-body), E-0165); `None` — свидетеля нет.

`status` — статус-тест КОНЪЮНКТА (errata E-0193): свидетель посылки обязан
быть тем же атомом, на котором конъюнкт выполнен в `solve`. Без него
свидетель `supported`/`monotone` искался среди TRUE_ONLY-атомов, при паре
BOTH не находился, и применение выходило БЕЗ посылок — доказательство, не
называющее ни одного прочитанного факта.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L342-L357)

## lawref.evaluator.solver.guard_value

*function*

```python
def guard_value(term: dict, subst: dict[str, dict], store: SupportStore, registry: 'ProofRegistry | None', env: Any = None) -> tuple[bool, list[str]]
```

Терм-гард [§57](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#57-equality)/[§58](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#58-arithmetic) в теле правила: агрегаты [§59](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#59-aggregates) сворачиваются по store
(свободные переменные comprehension приходят из subst — [§52.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#521-finite-relation-comprehensions) внутри
правила), затем терм вычисляется. Возвращает (значение, premise-узлы
агрегатов): у сравнения нет support-пары, но у посчитанных им фактов — есть.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L621-L654)

## lawref.evaluator.solver.has_conditional

*function*

```python
def has_conditional(term: Any) -> bool
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L279-L282)

## lawref.evaluator.solver.has_wildcard

*function*

```python
def has_wildcard(literal: Any) -> bool
```

E-0165 ([§98](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/15-part-xiv-rules.ru.md#98-body)): литерал с аргументом `_` — «есть какое-либо значение».

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L302-L306)

## lawref.evaluator.solver.materialize_comprehension

*function*

```python
def materialize_comprehension(comp: dict, store: 'SupportStore', registry: 'ProofRegistry', outer: dict[str, dict] | None = None, env: Any = None) -> tuple[list[dict], list[str]]
```

[§52.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#521-finite-relation-comprehensions): материализация comprehension по established support — значения
element + premise-узлы proof. Порядок детерминирован каноническими байтами
значений ([§51](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#51-collections): итерация, влияющая на результат, обязана быть упорядочена).

`distinct` ([§51](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#51-collections), errata E-0012) выбирает коллекцию, а не оптимизацию:
`true` — `Set<T>`, различные ground-значения (`collect`); `false` —
`List<T>`, по элементу на КАЖДУЮ solution substitution (`collect all`).
Свод числового поля по множеству сущностей выразим только вторым: над
множеством две равные позиции неотличимы от одной, и `sum` [§59](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#59-aggregates) молча
недосчитывает. Поле обязательно — умолчания у кратности нет.

`outer` — подстановка охватывающего правила: comprehension в теле правила
параметризуется его переменными («взносы ЭТОГО плательщика»), свободные
переменные при этом обязаны быть range-restricted позитивным конъюнктом
правила ([§190](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/27-part-xxvi-static-semantics-and-diagnostics.ru.md#190-rule-safety)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L1025-L1109)

## lawref.evaluator.solver.merge_premises

*function*

```python
def merge_premises(premises: list[str], incoming: list[str]) -> None
```

Слияние посылок с дедупликацией по множеству; порядок вставки прежний —
список остаётся источником порядка. `incoming` бывает N-размерным
(посылки comprehension [§52.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#521-finite-relation-comprehensions)), и линейный `not in premises` давал O(N·M).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L1006-L1014)

## lawref.evaluator.solver.quantified_support

*function*

```python
def quantified_support(formula: dict, subst: dict[str, dict], store: SupportStore, registry: 'ProofRegistry | None', premises: list[str], env: Any = None) -> tuple[bool, bool]
```

[§52](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#52-finite-domains): квантор над КОНЕЧНЫМ доменом.

`forall` — паранепротиворечивая конъюнкция инстанцированных тел, `exists`
— дизъюнкция. Пустой домен даёт нормативные значения прямо из [§52](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#52-finite-domains)
(`forall … == true`, `exists … == false`) — они выпадают из тех же
формул как нейтральные элементы. Один conflicted элемент делает агрегат
BOTH, и rule-body default [§66](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#66-rule-body-default) такой конъюнкт не считает сработавшим.

Домен v1 — comprehension [§52.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#521-finite-relation-comprehensions): только он несёт тип элемента и доказуемо
конечен. Домен-провайдер (функция, внешняя коллекция) вне среза — правило
честно пропускается как NON_EXECUTABLE, а не считается по домену,
полноты которого никто не показал. Незакреплённый домен [§52](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#52-finite-domains) (`NEITHER +
MISSING_INPUT`) в v1 не возникает: comprehension всегда материализуется,
а пустой результат — это пустой домен, а не отсутствующий.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L741-L782)

## lawref.evaluator.solver.quantified_value

*function*

```python
def quantified_value(formula: dict, subst: dict[str, dict], store: SupportStore, registry: 'ProofRegistry | None', env: Any = None) -> tuple[bool, list[str]]
```

Квантор как конъюнкт тела правила: rule-body default [§66](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#66-rule-body-default) требует
TRUE_ONLY, поэтому BOTH (конфликт внутри домена) правило НЕ активирует.
Возвращает (сработал ли конъюнкт, посылки прочитанных фактов).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L785-L793)

## lawref.evaluator.solver.resolve_aggregates

*function*

```python
def resolve_aggregates(term: dict, store: 'SupportStore', registry: 'ProofRegistry', stats: list[dict], premises: list[str], outer: dict[str, dict] | None = None, env: Any = None) -> dict
```

[§59](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#59-aggregates): AggregateTerm → LiteralTerm до чистого eval_term. input —
ComprehensionTerm (материализуется по established, как collect [§52.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#521-finite-relation-comprehensions)),
элементы сворачиваются values.aggregate; прочие термы — рекурсивный обход.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L1227-L1263)

## lawref.evaluator.solver.rounding_support

*function*

```python
def rounding_support(formula: dict, subst: dict[str, dict], store: SupportStore, registry: 'ProofRegistry | None', env: Any = None) -> tuple[tuple[bool, bool], list[str]]
```

[§64.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#642-отношение-округления-над-сертифицированными-границами-errata-e-0136) (errata E-0136): опора отношения округления над сертификатом.

Единственная формула Core, чья пара берётся из ДОКАЗАТЕЛЬСТВА, а не из
store [§61](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#61-literal) и не из lifting Boolean [§64.1](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#641-lifting-data-boolean-в-formula). `NEITHER` здесь означает
недостаточность границ: интервал задел две ячейки, и ответа нет ни
положительного, ни отрицательного.

Решение принимается на КОНЦАХ отрезка — все семь режимов [§50](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#50-money) монотонно
неубывающие, — и считается ТЕМ ЖЕ кодом, что `round` [§50](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#50-money): второе
определение режима разошлось бы с первым на точной половине.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L522-L594)

## lawref.evaluator.solver.select_conditionals

*function*

```python
def select_conditionals(term: Any, subst: dict[str, dict], where: str = 'term', env: Any = None, store: Any = None, registry: Any = None, premises: list[str] | None = None) -> Any
```

[§56](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#56-conditional-expression): выбор ветви `IfTerm` ДО свёртки агрегатов и вычисления подтермов.

Порядок здесь — не оптимизация, а само содержание [§56](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#56-conditional-expression): НЕВЫБРАННАЯ ветвь
не обязана быть вычислимой. `resolve_aggregates` обходит дерево целиком,
поэтому пустая коллекция [§59](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#59-aggregates) в мёртвой ветви уронила бы правило, а её
опоры попали бы в proof-граф вопреки тому, что норма эту ветвь не выбрала.
То же и с делением на ноль: ленивость обязана начинаться ЗДЕСЬ, а не в
`eval_term`, до которого дерево уже не доедет целым.

Условие со status-тестом [§65](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#65-status-tests) читается из store. Без store терм остаётся
целым: значение такого условия живёт в опоре, а не только в данных.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L1124-L1224)

## lawref.evaluator.solver.solve

*function*

```python
def solve(conjuncts: list[dict], subst: dict[str, dict], store: SupportStore, registry: 'ProofRegistry | None' = None, env: Any = None, delta: 'tuple[dict, int] | None' = None, greedy: bool = False)
```

Детерминированный перебор подстановок ([§103](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#103-strict-closure) naive fixpoint, [§190](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/27-part-xxvi-static-semantics-and-diagnostics.ru.md#190-rule-safety) range
restriction). Селекция конъюнкта: сначала любой полностью связанный
(литерал — фильтр по TRUE_ONLY, гард [§58](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#58-arithmetic) — вычисление терма), иначе первый
позитивный с несвязанными переменными (перечисление established-атомов);
если остались только негативные/гарды с несвязанными переменными —
нарушение range restriction.

Semi-naive [§103](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#103-strict-closure) (17.09.2026): `delta = (литерал, штамп)` ограничивает
перечисление ЭТОГО литерала (по тождеству объекта) атомами, получившими
опору позже штампа; `greedy` меняет выбор перечисляемого литерала на
«наибольшее число связанных позиций» (дельта-литерал — первым). Оба
ключа меняют лишь порядок и объём перебора, но не множество подстановок:
перечисление исчерпывающее, фильтры коммутируют. Вызывающий
(strict.strict_closure) восстанавливает наивный порядок сортировкой.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L829-L1003)

## lawref.evaluator.solver.substitute

*function*

```python
def substitute(term: dict, subst: dict[str, dict], where: str = 'term', env: Any = None) -> dict
```

Подстановка [§103](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#103-strict-closure) с рекурсией в вычислимые термы и их свёрткой.

Плоская версия (только `kind == "var"` верхнего уровня) публиковала
`p(x, y * 0.02)` с несвязанной переменной внутри терма — ground-инвариант
store нарушался молча.

`env` — окружение evaluation ([§85](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/12-part-xii-events-actions-temporal-model.ru.md#85-calendar-snapshot)/[§86](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/12-part-xii-events-actions-temporal-model.ru.md#86-deadline-policy)) для календарных термов; чистым
термам не нужно, поэтому по умолчанию отсутствует.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L205-L269)

## lawref.evaluator.solver.substitute_head

*function*

```python
def substitute_head(head: dict, subst: dict[str, dict], store: SupportStore, registry: 'ProofRegistry', env: Any = None, rule_id: str | None = None) -> tuple[dict, list[str]]
```

Head правила под подстановкой: агрегаты [§59](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#59-aggregates) сворачиваются по store
(comprehension параметризована переменными правила), затем вычисляются
термы [§58](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/09-part-ix-values-terms-expressions.ru.md#58-arithmetic)/[§50](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#50-money). Возвращает (ground-литерал, premise-узлы агрегатов).

Агрегат в head нужен нормам вида «объект исчисления считается по СУММЕ
всех видов начисленных доходов» — сумма там и есть содержание вывода,
а не условие. Барьер полноты [§111](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#111-порядок-evaluation-strata) проверяется на фильтре правил, как и
для гардов: источник агрегата обязан быть невыводимым.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L796-L826)

## lawref.evaluator.solver.substitute_literal

*function*

```python
def substitute_literal(literal: dict, subst: dict[str, dict], env: Any = None) -> dict
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L272-L276)

## lawref.evaluator.solver.wildcard_witness

*function*

```python
def wildcard_witness(literal: dict, subst: dict[str, dict], store: 'SupportStore', env: Any = None, status: str = 'established', registry: Any = None, premises: list[str] | None = None) -> dict | None
```

[§98](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/15-part-xiv-rules.ru.md#98-body) (E-0165): свидетель существования — ground-атом, совпадающий с
литералом по всем позициям, кроме `_`, со статусом TRUE_ONLY (established)
либо TRUE_ONLY|BOTH (supported/monotone). При нескольких — НАИМЕНЬШИЙ по
каноническому ключу: один и тот же в обеих реализациях и в повторе.
`None` — ни одного значения нет.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L309-L339)

## lawref.evaluator.solver.within_effective

*function*

```python
def within_effective(interval: dict | None, legal_time: str) -> bool
```

Rule temporal qualifier `effective` против context.legal_time ([§87](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/12-part-xii-events-actions-temporal-model.ru.md#87-rule-temporal-qualifiers); T011).
Сравнение ISO-дат лексикографично; instants v1 не смешиваются с датами ([§2.15](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/01-part-i-audit.ru.md#215-legal_time-date-было-слишком-узким)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/evaluator/solver.py#L478-L490)