Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/reasonsmith/adapters/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@
from reasonsmith.adapters.rules import RulesAdapter, RulesSUT

__all__ = [
"JSONLAdapter",
"JsonlSUT",
"CallableAdapter",
"CallableSUT",
"JSONLAdapter",
"JsonlSUT",
"RulesAdapter",
"RulesSUT",
]
6 changes: 3 additions & 3 deletions src/reasonsmith/adapters/callable.py
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
from __future__ import annotations

from collections.abc import Iterable, Mapping
from typing import Any, Optional
from typing import Any

from reasonsmith.neural import DeclaredInputSpace
from reasonsmith.sut import BaseSUT
Expand All @@ -32,8 +32,8 @@ def __init__(
self,
target: Any,
declared_capabilities: set[str] | Iterable[str],
test_inputs: Optional[Iterable[Any]] = None,
decisions: Optional[Iterable[dict[str, Any]]] = None,
test_inputs: Iterable[Any] | None = None,
decisions: Iterable[dict[str, Any]] | None = None,
input_space: DeclaredInputSpace | Mapping[str, Any] | None = None,
frontier_ai_status: str | None = None,
):
Expand Down
14 changes: 7 additions & 7 deletions src/reasonsmith/adapters/rules.py
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@

import ast
from collections.abc import Iterable
from typing import Any, Optional
from typing import Any

from reasonsmith.rulelang import (
UnsupportedConstructError,
Expand Down Expand Up @@ -92,11 +92,11 @@ class RulesAdapter(BaseSUT):
def __init__(
self,
rules: list[str] | str,
variables: Optional[dict[str, str]] = None,
constraints: Optional[list[str] | str] = None,
declared_capabilities: Optional[set[str] | Iterable[str]] = None,
test_inputs: Optional[Iterable[dict[str, Any]]] = None,
computes: Optional[Iterable[str]] = None,
variables: dict[str, str] | None = None,
constraints: list[str] | str | None = None,
declared_capabilities: set[str] | Iterable[str] | None = None,
test_inputs: Iterable[dict[str, Any]] | None = None,
computes: Iterable[str] | None = None,
frontier_ai_status: str | None = None,
):
if isinstance(rules, str):
Expand Down Expand Up @@ -126,7 +126,7 @@ def __init__(
if variables is not None:
self._variables = dict(variables)
else:
self._variables = {v: "real" for v in sorted(discovered_vars)}
self._variables = dict.fromkeys(sorted(discovered_vars), "real")

if isinstance(computes, (str, bytes)):
raise ValueError(
Expand Down
36 changes: 18 additions & 18 deletions src/reasonsmith/analysis.py
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@
import ast
import copy
from dataclasses import dataclass, field
from typing import Any, Optional
from typing import Any

import z3

Expand Down Expand Up @@ -173,7 +173,7 @@ class PackAnalysis:
"""What the four questions answered, and every one skipped rather than answered."""

pack_id: str
satisfiable: Optional[bool]
satisfiable: bool | None
unsatisfiable_core: tuple[str, ...] = ()
relations: tuple[Relation, ...] = ()
vacuities: tuple[VacuityFinding, ...] = ()
Expand All @@ -183,7 +183,7 @@ class PackAnalysis:
notes: tuple[str, ...] = field(default_factory=tuple)
#: `None` when the optional decision procedure is not installed, which is not the same fact as
#: "it was installed and found nothing" and must not render as it.
temporal: Optional[TemporalAnalysis] = None
temporal: TemporalAnalysis | None = None


class _PackScope(_Scope):
Expand Down Expand Up @@ -223,7 +223,7 @@ def contains(self, signal: str, phrase: str) -> Any:
return atom


def _state_property(req: Requirement) -> tuple[Optional[ast.Expression], str]:
def _state_property(req: Requirement) -> tuple[ast.Expression | None, str]:
"""The state property this analysis encodes for a requirement, or a reason it encodes none."""
if req.formalism == "counterfactual":
return None, (
Expand Down Expand Up @@ -273,7 +273,7 @@ def _encoded(node: ast.AST, scope: _Scope, what: str) -> Any:
return _as_bool(_ast_to_z3(node, scope), what)


def _valid(assertions: list[Any], formula: Any, timeout_ms: int) -> Optional[bool]:
def _valid(assertions: list[Any], formula: Any, timeout_ms: int) -> bool | None:
"""Whether `formula` holds everywhere the assertions admit; `None` if the solver cannot say."""
solver = z3.Solver()
solver.set("timeout", timeout_ms)
Expand All @@ -287,8 +287,8 @@ def _valid(assertions: list[Any], formula: Any, timeout_ms: int) -> Optional[boo
return None


def _parents(tree: ast.AST) -> dict[int, tuple[ast.AST, str, Optional[int]]]:
parents: dict[int, tuple[ast.AST, str, Optional[int]]] = {}
def _parents(tree: ast.AST) -> dict[int, tuple[ast.AST, str, int | None]]:
parents: dict[int, tuple[ast.AST, str, int | None]] = {}
for node in ast.walk(tree):
for name, value in ast.iter_fields(node):
if isinstance(value, list):
Expand Down Expand Up @@ -392,7 +392,7 @@ def vacuous_subformulas(

def _has_reported_ancestor(
node: ast.AST,
parents: dict[int, tuple[ast.AST, str, Optional[int]]],
parents: dict[int, tuple[ast.AST, str, int | None]],
reported: set[int],
) -> bool:
current = node
Expand All @@ -405,7 +405,7 @@ def _has_reported_ancestor(

def _satisfiability_and_relations(
pack: Pack, timeout_ms: int
) -> tuple[Optional[bool], tuple[str, ...], tuple[Relation, ...], list[str], list[str]]:
) -> tuple[bool | None, tuple[str, ...], tuple[Relation, ...], list[str], list[str]]:
"""Encode every encodable requirement of a pack once, then ask the two formula questions."""
skipped: list[str] = []
encoded: list[tuple[str, ast.Expression]] = []
Expand Down Expand Up @@ -435,7 +435,7 @@ def _satisfiability_and_relations(
for req_id, formula in formulas.items():
solver.assert_and_track(formula, req_id)
outcome = solver.check()
satisfiable: Optional[bool] = None
satisfiable: bool | None = None
core: tuple[str, ...] = ()
if outcome == z3.sat:
satisfiable = True
Expand Down Expand Up @@ -463,7 +463,7 @@ def _satisfiability_and_relations(
return satisfiable, core, tuple(relations), skipped, notes


def _temporal_analysis(pack: Pack) -> tuple[Optional[TemporalAnalysis], list[str], list[str]]:
def _temporal_analysis(pack: Pack) -> tuple[TemporalAnalysis | None, list[str], list[str]]:
"""Decide the pack's temporal duties as finite-trace formulas, or say why one was not.

The whole fragment reaches this, not only the shapes the Z3 reduction misses: an entailment
Expand Down Expand Up @@ -608,7 +608,7 @@ def _mutation_coverage(
pack: Pack,
sut: SystemUnderTest,
system_domains: tuple[str, ...],
system_scope: Optional[str],
system_scope: str | None,
) -> tuple[tuple[MutationScore, ...], str, list[str]]:
"""Re-run the pack against every mutant of the system's declared rules.

Expand Down Expand Up @@ -640,7 +640,7 @@ def _mutation_coverage(
domains = system_domains or tuple(getattr(sut, "system_domains", ()) or ())
scope = system_scope or getattr(sut, "system_scope", getattr(sut, "declared_scope", None))

def build(mutated: list[str]) -> Optional[RulesAdapter]:
def build(mutated: list[str]) -> RulesAdapter | None:
try:
adapter = RulesAdapter(
rules=mutated,
Expand Down Expand Up @@ -692,9 +692,9 @@ def build(mutated: list[str]) -> Optional[RulesAdapter]:
def _verdict_map(
pack: Pack,
sut: SystemUnderTest,
system_scope: Optional[str],
system_scope: str | None,
system_domains: tuple[str, ...],
) -> dict[str, tuple[str, Optional[str]]]:
) -> dict[str, tuple[str, str | None]]:
report = check_conformance(
sut, pack, system_scope=system_scope, system_domains=system_domains or None
)
Expand All @@ -709,9 +709,9 @@ def _verdict_map(

def analyse_pack(
pack: Pack,
sut: Optional[SystemUnderTest] = None,
sut: SystemUnderTest | None = None,
*,
system_scope: Optional[str] = None,
system_scope: str | None = None,
system_domains: tuple[str, ...] = (),
timeout_ms: int = 5000,
) -> PackAnalysis:
Expand All @@ -734,7 +734,7 @@ def analyse_pack(

vacuities: list[VacuityFinding] = []
domain_label = "every assignment to the signals the properties read"
logic_scope: Optional[_Scope] = None
logic_scope: _Scope | None = None
logic_assertions: list[Any] = []
declared_computes: Any = None
if sut is not None:
Expand Down
6 changes: 3 additions & 3 deletions src/reasonsmith/artifacts/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -97,23 +97,23 @@
from reasonsmith.spec import normalize_claimed_semantics

__all__ = [
"DECISION_THRESHOLD_KEY",
"DECLARATION_REFUTED",
"DECLARED_NON_MONOTONE",
"EXACT_REASONS_KEY",
"EXACT_SEMANTICS_KEY",
"DECISION_THRESHOLD_KEY",
"MONOTONE_KEY",
"NO_INTERPRETATION",
"NO_SEMANTICS_REFERENCE",
"RECOUNTED_REASONS",
"UNDECLARED_MONOTONICITY",
"InferenceArtifact",
"DeclaredInputSpace",
"InferenceArtifact",
"OnnxArtifact",
"admits_interpretation",
"decision_threshold",
"default_label",
"deletion_semantics_refusal",
"decision_threshold",
"reason_set_is_exact",
"reference_semantics",
"semantics_reference_refusal",
Expand Down
4 changes: 2 additions & 2 deletions src/reasonsmith/artifacts/ground_program.py
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ def probability(self, fact: Atom) -> float:
"""This fact's probability under the base interpretation — half of the wider surface."""
return float(self.base[fact])

def at(self, fact: Atom, probability: float) -> "GroundProgramArtifact":
def at(self, fact: Atom, probability: float) -> GroundProgramArtifact:
"""The same inference at `probability` for `fact`, and the same reason set to score it over.

The widened perturbation. It re-scores what the base enumeration found and never
Expand All @@ -151,6 +151,6 @@ def at(self, fact: Atom, probability: float) -> "GroundProgramArtifact":
decision_threshold=self.decision_threshold,
)

def without(self, fact: Atom) -> "GroundProgramArtifact":
def without(self, fact: Atom) -> GroundProgramArtifact:
"""The same inference with `fact` at probability zero — the deletion probe's one call."""
return self.at(fact, 0.0)
2 changes: 1 addition & 1 deletion src/reasonsmith/artifacts/reason_trace.py
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ def engine_value(self) -> float:
"""The system's own answer, re-run with the suppressed facts withheld."""
return float(self._answer(self._suppressed))

def without(self, fact: Any) -> "ReasonTraceArtifact":
def without(self, fact: Any) -> ReasonTraceArtifact:
return ReasonTraceArtifact(
self.query,
self._reasons,
Expand Down
8 changes: 4 additions & 4 deletions src/reasonsmith/autoformalize.py
Original file line number Diff line number Diff line change
Expand Up @@ -487,8 +487,8 @@ def _challenge_result(candidate: str, case: ChallengeCase, requirement: Requirem
raise ValueError("counterfactual case pairs do not have one expected classification")
return results[0]

var_types: dict[str, str] = {name: "bool" for name in bare_boolean_names(node)}
var_types.update({name: "real" for name in measured_magnitude_names(node)})
var_types: dict[str, str] = dict.fromkeys(bare_boolean_names(node), "bool")
var_types.update(dict.fromkeys(measured_magnitude_names(node), "real"))
scope = _ChallengeScope(var_types, case.signals)
value = _formula(scope, node)
solver = z3.Solver()
Expand Down Expand Up @@ -674,12 +674,12 @@ def candidate_acceptable(
"ChallengeSet",
"RoundTripCheck",
"SignOff",
"candidate_ready",
"candidate_acceptable",
"verify_candidate",
"candidate_ready",
"challenge_requirements",
"check_challenges",
"load_challenge_sets",
"round_trip_check",
"signoff",
"verify_candidate",
]
2 changes: 1 addition & 1 deletion src/reasonsmith/demo.py
Original file line number Diff line number Diff line change
Expand Up @@ -1153,7 +1153,7 @@ def decisions(self) -> list[dict]:

def logic(self):
"""No rule set to reason over: the deployed engine is proof search over a ground program."""
return None
return

def artifact(self, decision: dict) -> dict | None:
"""The inference this decision came from, as the keyword arguments of `certify`."""
Expand Down
7 changes: 4 additions & 3 deletions src/reasonsmith/drift.py
Original file line number Diff line number Diff line change
Expand Up @@ -48,11 +48,12 @@
import re
import sys
import urllib.request
from collections.abc import Callable, Iterable
from dataclasses import dataclass
from datetime import datetime, timezone
from datetime import UTC, datetime
from html.parser import HTMLParser
from pathlib import Path
from typing import Callable, Iterable, Literal, cast
from typing import Literal, cast

from reasonsmith.spec import load_pack

Expand Down Expand Up @@ -792,7 +793,7 @@ def check_statute_drift(
)
return DriftReport(
results=tuple(results),
checked_at=now if now is not None else datetime.now(timezone.utc),
checked_at=now if now is not None else datetime.now(UTC),
)


Expand Down
4 changes: 2 additions & 2 deletions src/reasonsmith/engines/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -26,10 +26,10 @@
from reasonsmith.engines.temporal import TemporalProofEngine

__all__ = [
"RecordEngine",
"CertificateEngine",
"ObservedEngine",
"ProbedEngine",
"ProvedEngine",
"CertificateEngine",
"RecordEngine",
"TemporalProofEngine",
]
6 changes: 3 additions & 3 deletions src/reasonsmith/engines/counterfactual.py
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@
import ast
from collections.abc import Callable, Iterable, Mapping
from dataclasses import replace
from typing import Any, Optional
from typing import Any

import z3

Expand Down Expand Up @@ -370,7 +370,7 @@ class CounterfactualProofEngine:
def evaluate(
req: Requirement,
sut: SystemUnderTest,
records: Optional[list[dict[str, Any]]] = None,
records: list[dict[str, Any]] | None = None,
timeout_ms: int = 5000,
*,
logic_data: Any = _UNSET_LOGIC,
Expand Down Expand Up @@ -868,7 +868,7 @@ class PairedReplayEngine:
def evaluate(
req: Requirement,
sut: SystemUnderTest,
records: Optional[list[dict[str, Any]]] = None,
records: list[dict[str, Any]] | None = None,
*,
trace_provider: Callable[[], Iterable[dict[str, Any]]] | None = None,
max_values: int = DEFAULT_MAX_VALUES,
Expand Down
6 changes: 3 additions & 3 deletions src/reasonsmith/engines/probed.py
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@
import copy
import random
from collections.abc import Callable, Iterable, Mapping
from typing import Any, Optional
from typing import Any

from reasonsmith.report import (
PROBE_BUDGET_KEY,
Expand Down Expand Up @@ -292,7 +292,7 @@ def _shared_mutable_path(
original: Any,
cloned: Any,
path: str = "input",
seen: Optional[set[tuple[int, int]]] = None,
seen: set[tuple[int, int]] | None = None,
) -> str | None:
if isinstance(original, (type(None), bool, int, float, complex, str, bytes)):
return None
Expand Down Expand Up @@ -477,7 +477,7 @@ class ProbedEngine:
def evaluate(
req: Requirement,
sut: SystemUnderTest,
records: Optional[list[dict[str, Any]]] = None,
records: list[dict[str, Any]] | None = None,
trials: int = DEFAULT_TRIALS,
seed: int = DEFAULT_SEED,
*,
Expand Down
Loading
Loading