#!/usr/bin/env python3
"""Educational exact finite-model checker. No external solver or source parser.
Program semantics: pure total mathematical-integer expressions, finite acyclic
structured statements, all reads defined. Finite solver domain is explicit.
The CFG helper uses input node 0, exit node 10 and x/y input variables;
statement identifiers must be distinct and different from 0 and 10.
Finite-state examples use integer labels. These helpers are not source parsers
or validators for arbitrary language extensions.
Checks use exceptions and remain enabled under python -O.
"""
from itertools import product
from collections import deque
import json

def check(ok, message):
    if not ok: raise RuntimeError(message)

def ev(e, env):
    if type(e) is int: return e
    if isinstance(e, str): return env[e]
    op, a, b = e; a, b = ev(a, env), ev(b, env)
    return {'+':lambda:a+b, '-':lambda:a-b, '*':lambda:a*b,
            '>':lambda:a>b, '==':lambda:a==b, '!=':lambda:a!=b,
            '<=':lambda:a<=b}[op]()

def subst(e, env):
    if type(e) is int: return e
    if isinstance(e, str): return env[e]
    return (e[0], subst(e[1], env), subst(e[2], env))

def names(e):
    # Visit every expression occurrence once; never copy partial name sets.
    result=set(); pending=[e]
    while pending:
        term=pending.pop()
        if isinstance(term, str): result.add(term)
        elif type(term) is not int:
            pending.append(term[2]); pending.append(term[1])
    return result

# (id,kind,...) ; branch children are ordered tuples of statements.
PROGRAM=((1,'assign','a',('+','x',1)),(2,'assign','junk',('*','y','y')),
         (3,'assign','r',0),
         (4,'if',('>','x',0),((5,'if',('==','y','a'),
              ((6,'assign','r',1),),((7,'assign','r',2),)),),()),
         (8,'assign','junk',('+','junk',1)),(9,'return','r'))

def cfg(program):
    nodes={0:('input',('x','y')),10:('exit',)}; edges={10:[]}
    def seq(stmts, after):
        nxt=after
        for st in reversed(stmts):
            i,kind,*args=st
            check(i not in nodes,'duplicate node')
            if kind=='if':
                guard,yes,no=args; nodes[i]=(kind,guard)
                edges[i]=[(seq(yes,nxt),True),(seq(no,nxt),False)]
            else:
                nodes[i]=(kind,*args); edges[i]=[(nxt,None)]
            nxt=i
        return nxt
    edges[0]=[(seq(program,10),None)]
    return nodes,edges

def order(nodes,edges):
    indeg={v:0 for v in nodes}
    for outs in edges.values():
        for v,_ in outs: indeg[v]+=1
    q=deque(sorted(v for v in nodes if indeg[v]==0)); out=[]
    while q:
        u=q.popleft(); out.append(u)
        for v,_ in edges[u]:
            indeg[v]-=1
            if indeg[v]==0:q.append(v)
    check(len(out)==len(nodes),'model requires an acyclic CFG')
    return out

def dependence(program):
    nodes,edges=cfg(program); topo=order(nodes,edges); pd={}
    for u in reversed(topo):
        outs=edges[u]
        pd[u]={u} if not outs else {u}|set.intersection(*(pd[v] for v,_ in outs))
    control={(u,v,label) for u in nodes if nodes[u][0]=='if'
             for w,label in edges[u] for v in pd[w]-pd[u]}
    pred={u:[] for u in nodes}
    for u in nodes:
        for v,_ in edges[u]:pred[v].append(u)
    rd={}; data=set(); IN={}
    for u in topo:
        incoming=set().union(*(rd[p] for p in pred[u])); IN[u]=incoming
        kind,*a=nodes[u]
        reads=names(a[1]) if kind=='assign' else names(a[0]) if kind in ('if','return') else set()
        for x in reads:
            definitions={(d,x) for d,y in incoming if y==x}
            check(bool(definitions),'undefined read in example: '+x)
            data.update((d,u,x) for d,_ in definitions)
        writes={a[0]} if kind=='assign' else set(a[0]) if kind=='input' else set()
        rd[u]={(d,x) for d,x in incoming if x not in writes}|{(u,x) for x in writes}
    return pd,data,control

def backward_slice(data,control,criterion):
    rev={}
    for a,b,_ in data|control: rev.setdefault(b,set()).add(a)
    keep=set(criterion); todo=list(criterion)
    while todo:
        v=todo.pop()
        for u in rev.get(v,set()):
            if u not in keep: keep.add(u);todo.append(u)
    return keep

def prune(program,keep):
    out=[]
    for st in program:
        i,kind,*a=st
        if kind=='if':
            yes,no=prune(a[1],keep),prune(a[2],keep)
            check(i in keep or not(yes or no),'missing enclosing control predicate')
            if i in keep:out.append((i,kind,a[0],yes,no))
        elif i in keep:out.append(st)
    return tuple(out)

def concrete(program,x,y):
    env={'x':x,'y':y}; trace=[]
    def go(stmts):
        for i,kind,*a in stmts:
            trace.append(i)
            if kind=='assign':env[a[0]]=ev(a[1],env)
            elif kind=='if':go(a[1] if ev(a[0],env) else a[2])
            elif kind=='return':env['_return']=ev(a[0],env)
    go(program);return env['_return'],trace

DOMAIN=tuple(product(range(-2,3),repeat=2))
def satisfies(path,xy):
    env=dict(zip(('X','Y'),xy))
    return all(bool(ev(expr,env))==truth for _,expr,truth in path)

def solve(path,domain=DOMAIN):
    # Exact SAT/UNSAT only over domain; never an unbounded-integer SMT result.
    return next((xy for xy in domain if satisfies(path,xy)),None)

def symbolic(program,domain=DOMAIN):
    nodes,edges=cfg(program); todo=[(edges[0][0][0],{'x':'X','y':'Y'},())]; leaves=[]
    while todo:
        pc,env,path=todo.pop(); kind,*a=nodes[pc]
        if kind=='assign':
            env=dict(env);env[a[0]]=subst(a[1],env);todo.append((edges[pc][0][0],env,path))
        elif kind=='if':
            e=subst(a[0],env)
            for nxt,truth in reversed(edges[pc]):
                p=path+((pc,e,truth),)
                if solve(p,domain) is not None:todo.append((nxt,dict(env),p))
        elif kind=='return':leaves.append((path,subst(a[0],env)))
        else:raise ValueError('unexpected reachable node')
    return leaves

def concolic_run(program,xy):
    nodes,edges=cfg(program); pc=edges[0][0][0]
    concrete_env=dict(zip(('x','y'),xy)); symbolic_env={'x':'X','y':'Y'}; path=[]
    while True:
        kind,*a=nodes[pc]
        if kind=='assign':
            symbolic_env[a[0]]=subst(a[1],symbolic_env)
            concrete_env[a[0]]=ev(a[1],concrete_env)
            pc=edges[pc][0][0]
        elif kind=='if':
            e=subst(a[0],symbolic_env); truth=bool(ev(a[0],concrete_env))
            check(bool(ev(e,dict(zip(('X','Y'),xy))))==truth,'dual-state mismatch')
            path.append((pc,e,truth));pc=next(v for v,b in edges[pc] if b==truth)
        else:
            check(kind=='return','unexpected node')
            return tuple(path),ev(a[0],concrete_env)

def path_key(p):return tuple((i,b) for i,_,b in p)

def concolic(program,seed=(0,0),domain=DOMAIN):
    check(seed in domain,'seed outside domain'); pending=deque([seed]); covered=set();attempted=set();runs=[]
    while pending:
        xy=pending.popleft();p,value=concolic_run(program,xy)
        runs.append({'input':list(xy),'path':[[i,b] for i,_,b in p],'return':value})
        for j in range(1,len(p)+1):covered.add(path_key(p[:j]))
        for j in reversed(range(len(p))):
            i,e,b=p[j]; target=p[:j]+((i,e,not b),);key=path_key(target)
            if key in covered or key in attempted:continue
            attempted.add(key);model=solve(target,domain)
            if model is not None:
                actual,_=concolic_run(program,model)
                check(path_key(actual[:j+1])==key,'new input failed replay')
                pending.append(model)
    return runs

def houdini(states,initial,edges,candidates):
    active=set(candidates);log=[]
    candidate_order=tuple(candidates); initial_order=tuple(initial); edge_order=tuple(edges)
    while True:
        # All obligations in this round use the SAME current conjunction.
        invalid={};allowed={s for s in states if all(candidates[q](s) for q in active)}
        for q in candidate_order:
            if q not in active:continue
            init_bad=next((s for s in initial_order if not candidates[q](s)),None)
            step_bad=next(((s,t) for s,t in edge_order if s in allowed and not candidates[q](t)),None)
            if init_bad is not None:invalid[q]={'initial':init_bad}
            elif step_bad is not None:invalid[q]={'step':list(step_bad)}
        log.append({'active':[q for q in candidate_order if q in active],'removed':invalid})
        if not invalid:return active,log
        active-=set(invalid)

def paths(starts,edges,length):
    front=[(s,) for s in sorted(starts)]
    for _ in range(length):front=[p+(t,) for p in front for s,t in sorted(edges) if s==p[-1]]
    return front

def kinduction(states,initial,edges,P,k):
    check(type(k) is int and k>=1,'k must be positive')
    base=next((p for j in range(k) for p in paths(initial,edges,j) if not P(p[-1])),None)
    step=next((p for p in paths(states,edges,k) if all(P(s) for s in p[:-1]) and not P(p[-1])),None)
    return {'k':k,'base_counterexample':base,'step_counterexample':step,'proved':base is None and step is None}

def main():
    pd,data,control=dependence(PROGRAM);keep=backward_slice(data,control,{9}); sliced=prune(PROGRAM,keep)
    check(keep=={0,1,3,4,5,6,7,9},'slice nodes')
    check(control=={(4,5,True),(5,6,True),(5,7,False)},'control direction')
    for xy in DOMAIN:check(concrete(PROGRAM,*xy)[0]==concrete(sliced,*xy)[0],'slice changed return')
    leaves=symbolic(PROGRAM);counts=[];failures=[]
    for p,e in leaves:
        inputs=[xy for xy in DOMAIN if satisfies(p,xy)];counts.append({'path':[[i,b] for i,_,b in p],'inputs':len(inputs),'return':e})
        for xy in inputs:
            val=ev(e,dict(zip(('X','Y'),xy)))
            check(val==concrete(PROGRAM,*xy)[0],'symbolic/concrete mismatch')
            if val==1:failures.append(xy)
    check(sum(c['inputs'] for c in counts)==25 and failures==[(1,2)],'path partition')
    runs=concolic(sliced);check([r['input'] for r in runs]==[[0,0],[1,-2],[1,2]],'concolic schedule')
    S=set(range(5));I={0};T={(0,1),(1,2),(2,2),(3,4),(4,4)}
    C={'p0':lambda s:s>0,'p1':lambda s:s!=1,'p2':lambda s:s!=2,'p3':lambda s:s<=2,'p4':lambda s:s!=4}
    active,log=houdini(S,I,T,C);check(active=={'p3','p4'},'Houdini result')
    check([sorted(x['removed']) for x in log]==[['p0'],['p1'],['p2'],[]],'cascading rounds')
    final={s for s in S if all(C[q](s) for q in active)}
    check(I<=final and all(t in final for s,t in T if s in final) and all(s!=4 for s in final),'final certificate')
    # Exhaustively compare every inductive candidate subset against the survivor set.
    for mask in range(1<<len(C)):
        subset={q for j,q in enumerate(C) if mask>>j&1}; allowed={s for s in S if all(C[q](s) for q in subset)}
        if I<=allowed and all(t in allowed for s,t in T if s in allowed):check(subset<=active,'maximum-subset theorem')
    S4=set(range(4));T4={(0,1),(1,1),(2,3),(3,3)};P=lambda s:s!=3
    one=kinduction(S4,{0},T4,P,1);two=kinduction(S4,{0},T4,P,2)
    check(one['step_counterexample']==(2,3) and not one['proved'] and two['proved'],'k=1/2')
    cyclic=T4|{(2,2)};cycle_checks=[kinduction(S4,{0},cyclic,P,k) for k in range(1,9)]
    check(all(not r['proved'] and r['base_counterexample'] is None for r in cycle_checks),'unreachable safe cycle')
    strengthened=kinduction(S4,{0},cyclic,lambda s:s<=1,1);check(strengthened['proved'],'strengthened invariant')
    # Dead ends: base must inspect shorter paths rather than requiring k-step extension.
    dead=kinduction({0},{0},set(),lambda s:False,3);check(dead['base_counterexample']==(0,),'dead-end initial bug')
    # k-step UNSAT alone cannot excuse a bad initial state.
    initbad=kinduction({0},{0},{(0,0)},lambda s:False,1);check(initbad['step_counterexample'] is None and not initbad['proved'],'base cannot be skipped')
    # Nonempty candidate conjunctions may support one another.
    mutual,_=houdini(set(range(4)),{0},{(0,0),(1,2),(2,1),(3,3)},
                     {'x0':lambda s:s<2,'y0':lambda s:s%2==0})
    check(mutual=={'x0','y0'},'mutual support')
    # Transfer tasks: recompute after program/domain/model changes.
    changed=PROGRAM[:-2]+((8,'assign','r','junk'),PROGRAM[-1])
    _,dd,cc=dependence(changed); kk=backward_slice(dd,cc,{9})
    check(kk=={0,2,8,9},'changed return slice')
    for xy in DOMAIN:check(concrete(prune(changed,kk),*xy)[0]==xy[1]**2,'changed slice replay')
    repaired=PROGRAM[:3]+((4,'if',('>','x',0),((5,'if',('==','y','a'),
               ((6,'assign','r',('-','a','y')),),((7,'assign','r',2),)),),()),)+PROGRAM[4:]
    check(all(concrete(repaired,*xy)[0]!=1 for xy in DOMAIN),'repair finite-domain check')
    small=tuple(product(range(-1,2),repeat=2)); small_paths=symbolic(PROGRAM,small)
    check(len(small_paths)==2 and all(concrete(PROGRAM,*xy)[0]!=1 for xy in small),'restricted domain')
    broken_active,broken_log=houdini(S,I,T|{(2,3)},C)
    check(not broken_active and [sorted(r['removed']) for r in broken_log]==[['p0'],['p1'],['p2'],['p3'],['p4'],[]],'Houdini migration')
    moved_initial=kinduction(S4,{2},T4,P,2)
    check(moved_initial['base_counterexample']==(2,3) and moved_initial['step_counterexample'] is None and not moved_initial['proved'],'initial condition migration')
    result={'model':'Mathematical integers, pure total acyclic structured program; finite input solver domain [-2,2]^2 only.',
       'pdg':{'postdominators':{str(k):sorted(v) for k,v in sorted(pd.items())},'data_edges':sorted(data),'control_edges':sorted(control)},
       'slice':{'kept':sorted(keep),'removed':[2,8],'checked_inputs':25},
       'symbolic_paths':counts,'assert_r_not_1_counterexamples':failures,'concolic_runs':runs,
       'houdini':{'rounds':log,'survivors':sorted(active),'certificate_states':sorted(final),'candidate_subsets_checked':32},
       'kinduction':{'depth1':one,'depth2':two,'cycle_depths_checked':8,'cycle_counterexample_pattern':'2 repeated k times, then 3; unreachable from initial 0','strengthened':strengthened},
       'transfer_checks':{'changed_slice':sorted(kk),'restricted_domain_paths':len(small_paths),'repair_checked_inputs':25,'added_edge_houdini_survivors':sorted(broken_active),'new_initial_k2':moved_initial},
       'regressions':['dead-end bad initial state','base omitted would be unsound','mutually supporting candidates','python -O retains explicit checks']}
    print(json.dumps(result,ensure_ascii=False,indent=2))

if __name__=='__main__':main()