#!/usr/bin/env python3
"""Exact all-cut thinness for a bounded binary-multiplicity graph and tree.

Enumerates complement representatives of every nontrivial cut. This is an
exponential finite audit, not the paper's polynomial thin-tree constructor.
Tree edges select one copy of an original pair. No routing-load claim.
"""
import argparse
import json
from fractions import Fraction
from pathlib import Path

MAX_VERTICES=16
MAX_MULTIPLICITY_BITS=256
MAX_WORK=5_000_000


def audit(record, work_budget=MAX_WORK):
    if not isinstance(record,dict) or set(record)-{'vertices','edges','tree','target_alpha'}:
        raise ValueError('Provide vertices, edges, tree and optionally target_alpha')
    n=record.get('vertices')
    if isinstance(n,bool) or not isinstance(n,int) or not 2<=n<=MAX_VERTICES:
        raise ValueError(f'vertices must be from 2 to {MAX_VERTICES}')
    if isinstance(work_budget,bool) or not isinstance(work_budget,int) or not 1<=work_budget<=MAX_WORK:
        raise ValueError(f'work_budget must be from 1 to {MAX_WORK}')
    edges=record.get('edges')
    if not isinstance(edges,list) or len(edges)>n*(n-1)//2:
        raise ValueError('edges must be a bounded list of [u,v,multiplicity] triples')
    multiplicities={}
    for edge in edges:
        if not isinstance(edge,list) or len(edge)!=3 or any(isinstance(x,bool) or not isinstance(x,int) for x in edge):
            raise ValueError('Each edge must be an integer [u,v,multiplicity] triple')
        a,b=sorted(edge[:2]);multiplicity=edge[2]
        if not 0<=a<b<n or (a,b) in multiplicities or multiplicity<=0 or multiplicity.bit_length()>MAX_MULTIPLICITY_BITS:
            raise ValueError('Pairs must be distinct, loopless and in range; multiplicity must be positive with at most 256 bits')
        multiplicities[a,b]=multiplicity
    raw_tree=record.get('tree')
    if not isinstance(raw_tree,list) or len(raw_tree)>n*(n-1)//2:
        raise ValueError('tree must be a bounded edge-pair list')
    parent=list(range(n))
    def root(v):
        while parent[v]!=v:v=parent[v]
        return v
    tree=[];issues=[];used=set()
    for edge in raw_tree:
        if not isinstance(edge,list) or len(edge)!=2 or any(isinstance(x,bool) or not isinstance(x,int) for x in edge):
            raise ValueError('Tree edges must be integer pairs')
        a,b=sorted(edge)
        if not 0<=a<b<n:
            raise ValueError('Tree pair must be loopless and in range')
        if (a,b) not in multiplicities:issues.append('TREE_EDGE_NOT_IN_GRAPH')
        if (a,b) in used:issues.append('DUPLICATE_TREE_PAIR')
        used.add((a,b));tree.append((a,b))
        ra,rb=root(a),root(b)
        if ra==rb:issues.append('TREE_CYCLE')
        else:parent[ra]=rb
    if len(tree)!=n-1:issues.append('TREE_EDGE_COUNT')
    if len({root(v) for v in range(n)})!=1:issues.append('TREE_DISCONNECTED')
    target=None
    if 'target_alpha' in record:
        value=record['target_alpha']
        if not isinstance(value,str) or len(value)>160:raise ValueError('target_alpha must be a bounded rational string')
        try:target=Fraction(value)
        except (ValueError,ZeroDivisionError):raise ValueError('target_alpha must be a rational string')
        if target<0 or target.numerator.bit_length()>512 or target.denominator.bit_length()>512:
            raise ValueError('target_alpha must be nonnegative and have bounded numerator/denominator')
    result=dict(vertices=n,support_pairs=len(multiplicities),original_edge_copies=sum(multiplicities.values()),
        spanning_tree_valid=not issues,candidate_issues=sorted(set(issues)),target_alpha=str(target) if target is not None else None,
        source_connection=dict(family='174',source_commit='fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb',
            source_polynomial_constructor_implemented=False,source_proof_verification='not_run'),
        arithmetic='exact integers and fractions',formal_program_verification='not_run',
        limits=dict(vertices=MAX_VERTICES,multiplicity_bits=MAX_MULTIPLICITY_BITS,cut_edge_examinations=work_budget),
        work_unit_definition='Each original pair or tree edge examined at one cut; validation and fundamental-cut setup are additional bounded work.')
    if issues:return dict(result,status='invalid_tree',target_all_cut_bound_verified=False,exact_thinness=None)
    adjacency=[[] for _ in range(n)]
    for a,b in tree:adjacency[a].append(b);adjacency[b].append(a)
    fundamental=set()
    for removed in tree:
        reached={0};stack=[0]
        while stack:
            a=stack.pop()
            for b in adjacency[a]:
                if tuple(sorted((a,b)))==removed or b in reached:continue
                reached.add(b);stack.append(b)
        fundamental.add(sum(1<<v for v in reached))
    work=0;cuts=0;worst=Fraction(0);fundamental_worst=Fraction(0);witness=None;mincut=None;mincut_witness=None
    for mask in range(1,(1<<n)-1,2):
        # Odd masks contain vertex zero; complements cover the other half.
        graph_cut=0;tree_cut=0
        for (a,b),multiplicity in multiplicities.items():
            if work>=work_budget:
                return dict(result,status='budget_exceeded',cuts_completed=cuts,work_units=work,
                    exact_thinness=None,target_all_cut_bound_verified=False,
                    partial_max_ratio_lower_bound=str(worst),interpretation='Partial cut scan does not certify an all-cut bound or exact connectivity.')
            work+=1
            if bool(mask&(1<<a))!=bool(mask&(1<<b)):graph_cut+=multiplicity
        for a,b in tree:
            if work>=work_budget:
                return dict(result,status='budget_exceeded',cuts_completed=cuts,work_units=work,
                    exact_thinness=None,target_all_cut_bound_verified=False,
                    partial_max_ratio_lower_bound=str(worst),interpretation='Partial cut scan does not certify an all-cut bound or exact connectivity.')
            work+=1
            if bool(mask&(1<<a))!=bool(mask&(1<<b)):tree_cut+=1
        if graph_cut<=0:raise AssertionError('A valid supported spanning tree implies every nontrivial graph cut is positive')
        ratio=Fraction(tree_cut,graph_cut);cut=[v for v in range(n) if mask&(1<<v)]
        cuts+=1
        if ratio>worst:worst=ratio;witness=dict(vertices=cut,tree_edges=tree_cut,graph_edge_copies=graph_cut)
        if mask in fundamental:fundamental_worst=max(fundamental_worst,ratio)
        if mincut is None or graph_cut<mincut:mincut=graph_cut;mincut_witness=cut
    return dict(result,status='complete',cuts_completed=cuts,work_units=work,
        exact_thinness=str(worst),worst_cut=witness,exact_edge_connectivity=mincut,mincut_vertices=mincut_witness,
        achieved_C_for_k=str(mincut*worst),fundamental_tree_cut_max_ratio=str(fundamental_worst),
        target_all_cut_bound_verified=target is not None and worst<=target,
        interpretation='All cuts are exhausted for this bounded graph/tree. Binary multiplicities count distinct copies, not arbitrary real traffic capacities. Fundamental tree cuts alone can understate thinness. No polynomial source constructor, routing throughput, latency or failure-tolerant backbone is established.')


def main():
    parser=argparse.ArgumentParser(description=__doc__)
    parser.add_argument('input',type=Path)
    parser.add_argument('--output',type=Path)
    args=parser.parse_args()
    body=json.dumps(audit(json.loads(args.input.read_text())),indent=2,allow_nan=False)+'\n'
    if args.output:
        with args.output.open('x') as stream:stream.write(body)
    else:print(body,end='')


if __name__=='__main__':main()