lawref.evaluator.solver

Решатель: подстановка, свёртка термов и перебор — SPEC §103/§190/§204.

Модуль держит цикл взаимной рекурсии целиком, и разрывать его нельзя: solve → guard_value (гард §58) → resolve_aggregates (§59) → materialize_comprehension (§52.1) → solve. Агрегат в теле правила материализуется тем же перебором, который его и вызвал, поэтому четвёрка живёт в одном модуле.

Classes

Name	Description
NoBranchSelected	§56: опора условия NEITHER — ветвь не выбрана, значения у терма нет.
RangeRestrictionError	§190 нарушен САМОЙ программой: переменная головы не связана телом.

Functions

Name	Description
body_argument	§56/E-0180: select the branch before substituting a body argument.
body_literal	No description.
comprehension_branches	Ветви generator-а с проверкой §190 для КАЖДОЙ ветви (errata E-0219):
flatten_body	Body → список конъюнктов-пар (status, literal).
formula_support	Пара (t, f) формулы §62 под подстановкой — то, над чем §52 определяет
free_vars	Свободные переменные формулы/терма — список из кэша, НЕ мутировать.
generator_branches	Generator comprehension §52.1 → ветви ДНФ (errata E-0219).
generator_literals	Конъюнкты-листья generator-а в порядке узла, без повторов ДНФ: для
ground_or_witness	Ground-литерал посылки: подстановка, а у литерала с _ — свидетель
guard_value	Терм-гард §57/§58 в теле правила: агрегаты §59 сворачиваются по store
has_conditional	No description.
has_wildcard	E-0165 (§98): литерал с аргументом _ — «есть какое-либо значение».
materialize_comprehension	§52.1: материализация comprehension по established support — значения
merge_premises	Слияние посылок с дедупликацией по множеству; порядок вставки прежний —
quantified_support	§52: квантор над КОНЕЧНЫМ доменом.
quantified_value	Квантор как конъюнкт тела правила: rule-body default §66 требует
resolve_aggregates	§59: AggregateTerm → LiteralTerm до чистого eval_term. input —
rounding_support	§64.2 (errata E-0136): опора отношения округления над сертификатом.
select_conditionals	§56: выбор ветви IfTerm ДО свёртки агрегатов и вычисления подтермов.
solve	Детерминированный перебор подстановок (§103 naive fixpoint, §190 range
substitute	Подстановка §103 с рекурсией в вычислимые термы и их свёрткой.
substitute_head	Head правила под подстановкой: агрегаты §59 сворачиваются по store
substitute_literal	No description.
wildcard_witness	§98 (E-0165): свидетель существования — ground-атом, совпадающий с
within_effective	Rule temporal qualifier effective против context.legal_time (§87; T011).

NoBranchSelectedclass#

View source

class NoBranchSelected(where: str)

Bases: Exception

§56: опора условия NEITHER — ветвь не выбрана, значения у терма нет.

Не ошибка вычисления: причина (missing input §64.1, недостаточность границ §64.2) уже записана чтением опоры, и подменять её своей — значит потерять настоящую. Кандидат просто не даёт факта.

whereattributeinstance attribute#

View source

where = where

RangeRestrictionErrorclass#

View source

class RangeRestrictionError(code: str, message: str)

Bases: Exception

§190 нарушен САМОЙ программой: переменная головы не связана телом.

Отдельный класс, а не values.ValueError_: тот несёт ошибку ВЫЧИСЛЕНИЯ терма, и вызывающие превращают его в issue конкретного применения правила («деление на ноль в гарде»). Здесь дефектен не вход, а программа — правило, которое lawc check обязан был отвергнуть кодом LDC-E4101 ещё до lowering-а (§190: «head variables bound»). Слить их значило бы объявить непригодную программу невезучим делом.

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

codeattributeinstance attribute#

View source

code = code

messageattributeinstance attribute#

View source

message = message

body_argumentfunction#

View source

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/E-0180: select the branch before substituting a body argument.

body_literalfunction#

View source

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

comprehension_branchesfunction#

View source

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

Ветви generator-а с проверкой §190 для КАЖДОЙ ветви (errata E-0219): переменная comprehension и все binder-ы связаны позитивным литералом ветви. Для одной ветви проверки нет — прежнее поведение не меняется (несвязанную переменную там называет сам solve).

flatten_bodyfunction#

View source

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

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

status ∈ {“established”, “not_known”, “guard”}: Literal — implicit established §66, StatusFormula established — §204 canonical form, StatusFormula not_known — default negation §113 (истинен при NEITHER, проверяется после завершения producer stratum), ComparisonTerm §57/§58 — guard: терм-условие без опоры в store (у сравнения нет support-пары, оно проверяется на связанных переменных); StatusFormula supported — §65 (МОНОТОННЫЙ статус: истинен при любой positive-опоре, включая BOTH — T005; единственный вид, которому §103/§110 разрешают циклы). Прочие статусные виды — ValueError → правило пропускается с issue NON_EXECUTABLE.

formula_supportfunction#

View source

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 под подстановкой — то, над чем §52 определяет квантор. От flatten_body отличается уровнем: там конъюнкт тела правила уже свёрнут rule-body default §66 до «сработало/нет», здесь формула сохраняет все четыре значения, потому что один conflicted элемент обязан доехать до агрегированного BOTH.

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

free_varsfunction#

View source

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

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

generator_branchesfunction#

View source

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

Generator comprehension §52.1 → ветви ДНФ (errata E-0219).

Generator — Boolean-комбинация status tests (§207.1: голый литерал есть established(P)), поэтому or в нём исполняется ветвями: дистрибуция and над or слева направо, операнды — в порядке канонического узла §207.1. Лист, не являющийся связкой, разбирает flatten_body — его ValueError и есть отказ «вне подмножества». Формула без or даёт ровно одну ветвь, равную flatten_body (прежний путь байт в байт).

generator_literalsfunction#

View source

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

Конъюнкты-листья generator-а в порядке узла, без повторов ДНФ: для чтений §110/§111 развёртка не нужна, нужен состав листьев (E-0219).

ground_or_witnessfunction#

View source

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, E-0165); None — свидетеля нет.

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

guard_valuefunction#

View source

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

Терм-гард §57/§58 в теле правила: агрегаты §59 сворачиваются по store (свободные переменные comprehension приходят из subst — §52.1 внутри правила), затем терм вычисляется. Возвращает (значение, premise-узлы агрегатов): у сравнения нет support-пары, но у посчитанных им фактов — есть.

has_conditionalfunction#

View source

def has_conditional(term: Any) -> bool

has_wildcardfunction#

View source

def has_wildcard(literal: Any) -> bool

E-0165 (§98): литерал с аргументом _ — «есть какое-либо значение».

materialize_comprehensionfunction#

View source

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: материализация comprehension по established support — значения element + premise-узлы proof. Порядок детерминирован каноническими байтами значений (§51: итерация, влияющая на результат, обязана быть упорядочена).

distinct (§51, errata E-0012) выбирает коллекцию, а не оптимизацию: true — Set<T>, различные ground-значения (collect); false — List<T>, по элементу на КАЖДУЮ solution substitution (collect all). Свод числового поля по множеству сущностей выразим только вторым: над множеством две равные позиции неотличимы от одной, и sum §59 молча недосчитывает. Поле обязательно — умолчания у кратности нет.

outer — подстановка охватывающего правила: comprehension в теле правила параметризуется его переменными («взносы ЭТОГО плательщика»), свободные переменные при этом обязаны быть range-restricted позитивным конъюнктом правила (§190).

merge_premisesfunction#

View source

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

Слияние посылок с дедупликацией по множеству; порядок вставки прежний — список остаётся источником порядка. incoming бывает N-размерным (посылки comprehension §52.1), и линейный not in premises давал O(N·M).

quantified_supportfunction#

View source

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

§52: квантор над КОНЕЧНЫМ доменом.

forall — паранепротиворечивая конъюнкция инстанцированных тел, exists — дизъюнкция. Пустой домен даёт нормативные значения прямо из §52 (forall … == true, exists … == false) — они выпадают из тех же формул как нейтральные элементы. Один conflicted элемент делает агрегат BOTH, и rule-body default §66 такой конъюнкт не считает сработавшим.

Домен v1 — comprehension §52.1: только он несёт тип элемента и доказуемо конечен. Домен-провайдер (функция, внешняя коллекция) вне среза — правило честно пропускается как NON_EXECUTABLE, а не считается по домену, полноты которого никто не показал. Незакреплённый домен §52 (NEITHER + MISSING_INPUT) в v1 не возникает: comprehension всегда материализуется, а пустой результат — это пустой домен, а не отсутствующий.

quantified_valuefunction#

View source

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 требует TRUE_ONLY, поэтому BOTH (конфликт внутри домена) правило НЕ активирует. Возвращает (сработал ли конъюнкт, посылки прочитанных фактов).

resolve_aggregatesfunction#

View source

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: AggregateTerm → LiteralTerm до чистого eval_term. input — ComprehensionTerm (материализуется по established, как collect §52.1), элементы сворачиваются values.aggregate; прочие термы — рекурсивный обход.

rounding_supportfunction#

View source

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 (errata E-0136): опора отношения округления над сертификатом.

Единственная формула Core, чья пара берётся из ДОКАЗАТЕЛЬСТВА, а не из store §61 и не из lifting Boolean §64.1. NEITHER здесь означает недостаточность границ: интервал задел две ячейки, и ответа нет ни положительного, ни отрицательного.

Решение принимается на КОНЦАХ отрезка — все семь режимов §50 монотонно неубывающие, — и считается ТЕМ ЖЕ кодом, что round §50: второе определение режима разошлось бы с первым на точной половине.

select_conditionalsfunction#

View source

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: выбор ветви IfTerm ДО свёртки агрегатов и вычисления подтермов.

Порядок здесь — не оптимизация, а само содержание §56: НЕВЫБРАННАЯ ветвь не обязана быть вычислимой. resolve_aggregates обходит дерево целиком, поэтому пустая коллекция §59 в мёртвой ветви уронила бы правило, а её опоры попали бы в proof-граф вопреки тому, что норма эту ветвь не выбрала. То же и с делением на ноль: ленивость обязана начинаться ЗДЕСЬ, а не в eval_term, до которого дерево уже не доедет целым.

Условие со status-тестом §65 читается из store. Без store терм остаётся целым: значение такого условия живёт в опоре, а не только в данных.

solvefunction#

View source

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 naive fixpoint, §190 range restriction). Селекция конъюнкта: сначала любой полностью связанный (литерал — фильтр по TRUE_ONLY, гард §58 — вычисление терма), иначе первый позитивный с несвязанными переменными (перечисление established-атомов); если остались только негативные/гарды с несвязанными переменными — нарушение range restriction.

Semi-naive §103 (17.09.2026): delta = (литерал, штамп) ограничивает перечисление ЭТОГО литерала (по тождеству объекта) атомами, получившими опору позже штампа; greedy меняет выбор перечисляемого литерала на «наибольшее число связанных позиций» (дельта-литерал — первым). Оба ключа меняют лишь порядок и объём перебора, но не множество подстановок: перечисление исчерпывающее, фильтры коммутируют. Вызывающий (strict.strict_closure) восстанавливает наивный порядок сортировкой.

substitutefunction#

View source

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

Подстановка §103 с рекурсией в вычислимые термы и их свёрткой.

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

env — окружение evaluation (§85/§86) для календарных термов; чистым термам не нужно, поэтому по умолчанию отсутствует.

substitute_headfunction#

View source

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 сворачиваются по store (comprehension параметризована переменными правила), затем вычисляются термы §58/§50. Возвращает (ground-литерал, premise-узлы агрегатов).

Агрегат в head нужен нормам вида «объект исчисления считается по СУММЕ всех видов начисленных доходов» — сумма там и есть содержание вывода, а не условие. Барьер полноты §111 проверяется на фильтре правил, как и для гардов: источник агрегата обязан быть невыводимым.

substitute_literalfunction#

View source

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

wildcard_witnessfunction#

View source

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 (E-0165): свидетель существования — ground-атом, совпадающий с литералом по всем позициям, кроме _, со статусом TRUE_ONLY (established) либо TRUE_ONLY|BOTH (supported/monotone). При нескольких — НАИМЕНЬШИЙ по каноническому ключу: один и тот же в обеих реализациях и в повторе. None — ни одного значения нет.

within_effectivefunction#

View source

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

Rule temporal qualifier effective против context.legal_time (§87; T011). Сравнение ISO-дат лексикографично; instants v1 не смешиваются с датами (§2.15).