"""Literal reversible networks and exact, budgeted productive-core detection."""
from dataclasses import dataclass
from itertools import combinations
from math import factorial,gcd
import sympy as sp
from check_certificate import check

@dataclass(frozen=True)
class LiteralSource:
    entities:tuple
    reactions:tuple
    left:tuple
    right:tuple
    def __post_init__(self):
        m,n=len(self.entities),len(self.reactions)
        if len(set(self.entities))!=m or len(set(self.reactions))!=n:raise ValueError('Labels must be unique.')
        for matrix in (self.left,self.right):
            if len(matrix)!=m or any(len(row)!=n for row in matrix) or any(type(v)is not int or v<0 for row in matrix for v in row):raise ValueError('Literal matrices must be rectangular nonnegative integers, including uncancelled catalysts.')
    @property
    def net(self):return tuple(tuple(p-l for p,l in zip(pr,lr)) for pr,lr in zip(self.right,self.left))
    def admissible(self,X,S):return bool(X and S) and all(any(self.left[x][r]>0 for x in X) and any(self.right[x][r]>0 for x in X) for r in S)
    def certificate(self,X,S):
        X,S=tuple(X),tuple(S)
        if len(X)!=len(S) or len(set(X))!=len(X) or len(set(S))!=len(S) or any(type(x)is not int or not 0<=x<len(self.entities) for x in X) or any(type(r)is not int or not 0<=r<len(self.reactions) for r in S) or not self.admissible(X,S):raise ValueError('Nonempty admissible square support required.')
        A=sp.Matrix([[self.net[x][r] for r in S] for x in X]);det=int(A.det(method='domain-ge'))
        if det==0:raise ValueError('Singular restriction.')
        v=A.inv(method='DM')*sp.ones(len(X),1);z=[int(abs(det)*a) for a in v];flow=[0]*len(self.reactions)
        for r,value in zip(S,z):flow[r]=value
        d=dict(left=list(map(list,self.left)),right=list(map(list,self.right)),entities=list(X),reactions=list(S),flow=flow)
        verified=check(d)
        if not verified['accepted']:raise ArithmeticError('Independent literal certificate verifier rejected the square witness.')
        H=max(1,max(abs(int(v)) for v in A));bound=factorial(len(X))*H**(len(X)-1)
        if max(map(abs,z))>bound:raise ArithmeticError('Adjugate coefficient bound failed.')
        return dict(certificate=d,verification=verified,determinant=det,integer_flow_bound=bound,max_flow_bits=max(abs(x).bit_length() for x in z),minimality='not checked by certificate verifier')

@dataclass(frozen=True)
class SquareSearch:
    candidate_budget:int=100000
    def search(self,source):
        if type(self.candidate_budget)is not int or self.candidate_budget<0:raise ValueError('Nonnegative integer candidate budget required.')
        attempted=admissible=0;m,n=len(source.entities),len(source.reactions)
        for q in range(1,min(m,n)+1):
            for X in combinations(range(m),q):
                for S in combinations(range(n),q):
                    if attempted>=self.candidate_budget:return dict(status='unknown_budget',attempted=attempted,admissible=admissible)
                    attempted+=1
                    if not source.admissible(X,S):continue
                    admissible+=1;A=sp.Matrix([[source.net[x][r] for r in S] for x in X])
                    if A.det(method='domain-ge'):
                        witness=source.certificate(X,S)
                        # A proper submotif would contain a strictly smaller
                        # square witness, all of which were already examined.
                        witness['minimality']='PAC certified by exhaustive exclusion of every smaller square witness'
                        return dict(status='yes',attempted=attempted,admissible=admissible,witness=witness)
        return dict(status='no_exhaustive',attempted=attempted,admissible=admissible,scope='Every square support was checked; this is exponential enumeration, not a polynomial-time solver.')

class BinarySourceCodec:
    """Paper Appendix B: canonical LSB-first binary natural fields; zero is empty.
    Each digit is prefixed by 1 and the field ends in 0. No implicit net matrix.
    """
    @staticmethod
    def encode(source):
        def field(n):
            bits=[]
            while n:bits.append('1'+str(n&1));n>>=1
            return ''.join(bits)+'0'
        m,n=len(source.entities),len(source.reactions);values=[m,n]+[matrix[x][r] for matrix in (source.left,source.right) for r in range(n) for x in range(m)]
        return ''.join(map(field,values))
    @staticmethod
    def decode(bits):
        if not isinstance(bits,str) or set(bits)-{'0','1'}:raise ValueError('A binary string is required.')
        values=[];i=0
        while i<len(bits):
            digits=[]
            while i<len(bits) and bits[i]=='1':
                if i+1>=len(bits):raise ValueError('Truncated digit.')
                digits.append(int(bits[i+1]));i+=2
            if i==len(bits):raise ValueError('Missing field terminator.')
            i+=1
            if digits and digits[-1]!=1:raise ValueError('Noncanonical natural-number field.')
            values.append(sum(d<<k for k,d in enumerate(digits)))
        if len(values)<2:raise ValueError('Missing dimensions.')
        m,n=values[:2]
        if len(values)!=2+2*m*n:raise ValueError('Incorrect field count.')
        # Shapes are bounded by encoded fields except for zero-dimensional data.
        if m*n==0:
            if m>len(bits) or n>len(bits):raise ValueError('Zero-dimensional allocation exceeds this decoder safety limit.')
        def matrix(start):return tuple(tuple(values[start+r*m+x] for r in range(n)) for x in range(m))
        return LiteralSource(tuple(f'e{i}' for i in range(m)),tuple(f'r{i}' for i in range(n)),matrix(2),matrix(2+m*n))