"""Exact next-map demonstration and exact finite-grid specialization of elimination.

The finite-grid result concerns that rational grid, not the full real projection.
In particular, grid infeasibility never certifies real infeasibility.
"""
from dataclasses import dataclass
from fractions import Fraction as F


@dataclass(frozen=True)
class ClosedUnionNext:
    intervals: tuple

    def __post_init__(self):
        intervals=tuple((F(a),F(b)) for a,b in self.intervals)
        if any(a<0 or a>b for a,b in intervals) or any(intervals[i][1]>=intervals[i+1][0] for i in range(len(intervals)-1)):
            raise ValueError('nonnegative ordered disjoint closed intervals required')
        object.__setattr__(self,'intervals',intervals)

    def value(self,lower):
        lower=F(lower)
        for a,b in self.intervals:
            if lower<=b:return max(lower,a)
        return None  # +infinity, never a guessed endpoint


class GridElimination:
    def __init__(self,problem,margin,denominator=256):
        self.problem=problem;self.margin=F(margin);self.N=denominator
        if self.margin<0 or type(denominator) is not int or denominator<1:raise ValueError('invalid margin or grid')

    def solve(self):
        p=self.problem;N=self.N;infinity=N+1;vertices=list(p.boxes);adj={v:[] for v in vertices}
        maps={}
        def ceilgrid(x):return min(infinity,max(0,-((-x*N).__floor__())))
        for e in p.cores:
            adj[e.tail].append(e.head);adj[e.head].append(e.tail)
            maps[e.tail,e.head]=[ceilgrid(e.lower(F(i,N))+self.margin*e.lower_weight) for i in range(N+1)]+[infinity]
            inverse=[]
            for i in range(N+1):
                target=F(i,N)+self.margin*e.upper_weight;lo,hi=-1,infinity
                while hi-lo>1:
                    mid=(lo+hi)//2
                    if e.upper(F(mid,N))>=target:hi=mid
                    else:lo=mid
                inverse.append(hi)
            maps[e.head,e.tail]=inverse+[infinity]
        parent={};order=[]
        def dfs(v,previous):
            parent[v]=previous
            for w in sorted(adj[v]):
                if w not in parent:dfs(w,v)
            order.append(v)
        for v in vertices:
            if v not in parent:dfs(v,None)
        lows={v:ceilgrid(b.lower) for v,b in p.boxes.items()};highs={v:(b.upper*N).__floor__() for v,b in p.boxes.items()}
        selfmaps={v:[0]*(N+1)+[infinity] for v in vertices};saved={};trace=[]
        for w in order:
            anc=[];v=parent[w]
            while v is not None:anc.append(v);v=parent[v]
            admissible=[lows[w]<=i<=highs[w] and selfmaps[w][i]<=i for i in range(N+1)]
            nxt=[infinity]*(N+2)
            for i in range(N,-1,-1):nxt[i]=i if admissible[i] else nxt[i+1]
            incoming={v:maps[v,w][:] for v in anc if (v,w) in maps};saved[w]=(nxt,incoming,lows[w])
            trace.append(dict(vertex=w,admissible_grid_points=sum(admissible),ancestors=anc))
            if not any(admissible):return dict(status='grid_infeasible',trace=trace,scope='No point on this grid; continuous feasibility is undecided by this result.')
            for j in anc:
                if (w,j) not in maps:continue
                outgoing=maps[w,j];lows[j]=max(lows[j],outgoing[nxt[lows[w]]])
                for i,inmap in incoming.items():
                    composed=[outgoing[nxt[k]] for k in inmap]
                    if i==j:selfmaps[i]=[max(a,b) for a,b in zip(selfmaps[i],composed)]
                    else:maps[i,j]=[max(a,b) for a,b in zip(maps.get((i,j),[0]*(N+1)+[infinity]),composed)]
        indices={}
        for w in reversed(order):
            nxt,incoming,lower=saved[w];a=max([lower]+[m[indices[i]] for i,m in incoming.items()]);k=nxt[a]
            if k==infinity:return dict(status='grid_infeasible',trace=trace,scope='No point on this grid; no real infeasibility claim.')
            indices[w]=k
        state={v:F(indices[v],N) for v in vertices}
        assert p.check_rational(state,self.margin)
        return dict(status='grid_feasible',state=state,trace=trace,denominator=N,scope='Exact least solution on a finite rational grid. Its witness is feasible over the reals, but need not be the real least state. No FPT runtime claim.')