#!/usr/bin/env python3
"""Propose a bounded unweighted matching with NetworkX, then audit it separately.

When the vertex/empty-subset bound is loose, vertex-deletion solves propose
D and S=N(D) minus D. The final certificate is checked independently of the solver.
This is an integration reference, not the collection's new matching backend.
"""
import argparse
import json
import platform
from pathlib import Path
from time import perf_counter

from audit_matching_certificate import audit

MAX_VERTICES = 256
MAX_SOLVER_CALLS = MAX_VERTICES + 1


def solve(record, max_solver_calls=MAX_SOLVER_CALLS):
    if not isinstance(record, dict):
        raise ValueError('Input must be an object')
    if set(record) != {'vertices', 'edges'}:
        raise ValueError('Provide only vertices and edges; weights and other objectives are unsupported')
    n = record.get('vertices')
    if isinstance(n, bool) or not isinstance(n, int) or not 1 <= n <= MAX_VERTICES:
        raise ValueError(f'vertices must be an integer from 1 to {MAX_VERTICES}')
    if (isinstance(max_solver_calls, bool) or not isinstance(max_solver_calls, int)
            or not 1 <= max_solver_calls <= MAX_SOLVER_CALLS):
        raise ValueError(f'max_solver_calls must be from 1 to {MAX_SOLVER_CALLS}')
    # Import is excluded from the stage timings and never touches SciPy.
    import networkx as nx

    started = perf_counter()
    audit(dict(record, matching=[]))  # Validate the graph before calling the solver.
    graph = nx.Graph()
    graph.add_nodes_from(range(n))
    graph.add_edges_from(record['edges'], unit_objective=1)
    graph_ready = perf_counter()

    primary = nx.max_weight_matching(graph, maxcardinality=True, weight='unit_objective')
    matching = sorted(sorted(edge) for edge in primary)
    primary_done = perf_counter()
    certificate = dict(record, matching=matching, barrier=[])
    initial = audit(certificate)
    first_audit_done = perf_counter()
    calls = 1
    d = set()
    deletion_complete = False
    attempted = False
    if not initial['maximum_cardinality_certificate_verified']:
        attempted = True
        for vertex in range(n):
            if calls >= max_solver_calls:
                break
            reduced = graph.copy()
            reduced.remove_node(vertex)
            size = len(nx.max_weight_matching(reduced, maxcardinality=True, weight='unit_objective'))
            calls += 1
            if size == len(matching):
                d.add(vertex)
        deletion_complete = calls == n + 1
        neighbors = {neighbor for vertex in d for neighbor in graph[vertex]}
        certificate['barrier'] = sorted(neighbors - d)
    subset_done = perf_counter()
    result = audit(certificate)
    finished = perf_counter()
    return dict(
        certificate=certificate,
        audit=result,
        proposal=dict(
            solver='NetworkX max_weight_matching', networkx_version=nx.__version__,
            objective='unweighted_maximum_cardinality', integer_edge_weight=1,
            solver_calls=calls, max_solver_calls=max_solver_calls,
            vertex_deletion_attempted=attempted, vertex_deletion_complete=deletion_complete,
            deletion_selected_vertices=sorted(d),
            subset_method='N(D) minus D, from deletion solves' if attempted else 'empty subset',
            constructor_guarantee='Only the final attaining-bound audit grants a certificate; incomplete deletion or a loose bound can return unknown.'),
        timings_seconds=dict(
            graph_validation_and_mapping=graph_ready-started,
            primary_solver=primary_done-graph_ready,
            initial_audit=first_audit_done-primary_done,
            subset_proposal=subset_done-first_audit_done,
            final_audit=finished-subset_done,
            measured_total=finished-started,
            excludes='Module imports, input file read, JSON serialization and output file write'),
        environment=dict(python=platform.python_version(), platform=platform.platform()),
        limits=dict(vertices=MAX_VERTICES, solver_calls=MAX_SOLVER_CALLS,
                    wall_time_deadline='none; call cap is not a runtime guarantee'),
        source_backend_implemented=False,
        interpretation='Finite existing-solver integration. Certificate scope is this supplied simple unweighted graph. No source-algorithm speed advantage, buyer workload, fairness, weighted-optimality or formal program verification is established.')


def main():
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument('input', type=Path)
    parser.add_argument('--max-solver-calls', type=int, default=MAX_SOLVER_CALLS)
    parser.add_argument('--output', type=Path)
    args = parser.parse_args()
    result = json.dumps(solve(json.loads(args.input.read_text()), args.max_solver_calls), indent=2, allow_nan=False) + '\n'
    if args.output:
        with args.output.open('x') as stream:
            stream.write(result)
    else:
        print(result, end='')


if __name__ == '__main__':
    main()