"""Exact excluded-region checks used by the AP-deficient comparison."""
from verify_ab_cover import F,Path,json,N,add,outer,sy,vs,pd,ell,q,d,r,z,base,K,fR,fT
H0=add((1,base),(1,K));HR=add((1,base),(-1,fR));HT=add((1,base),(-1,fT),(-1,K))
def verify(case_names=None):
 data=json.loads(Path(__file__).with_name('ab-good-domains-certificate.json').read_text())
 for row in data['cases']:
  if case_names is not None and row['name'] not in case_names:continue
  b,c,mu,kl,ku=map(F,row['parameters']);p=1-b-c;G=F(row['gamma'])
  assert min(p,b,c,mu,kl,ku)>=0 and p>=8*c
  H=add((1,H0),(b,add((1,HR),(-1,H0))),(c,add((1,HT),(-1,H0))))
  if row['name']=='Z_le_3r2':
   assert F(5,8)*b-2*c>=mu
   H=add((1,H),(mu,sy(r,vs((1,z),(F(-3,2),r)))),(-kl,sy(ell,vs((1,q),(-1,r)))),(-ku,sy(ell,vs((1,r),(F(-4,5),q)))))
  elif row['name']=='d_ge_23Z20':
   assert F(5,8)*b-2*c>=mu
   H=add((1,H),(mu,sy(r,vs((1,z),(F(-20,23),d)))),(-kl,sy(ell,vs((1,q),(-1,r)))),(-ku,sy(ell,vs((1,r),(F(-4,5),q)))))
  else:
   assert row['name']=='r_le_7q8' and F(5,8)*b>=2*c
   H=add((1,H),(-mu,sy(ell,vs((F(7,8),q),(-1,r)))),(-kl,sy(ell,vs((1,r),(F(-4,5),q)))),(-ku,sy(ell,vs((1,q),(-1,r)))))
  pd(add((1,H),(-(1-2*G),outer(ell,ell))))
  print('PASS good-P domain exclusion',row['name'],G,float(G))
 assert F(23,20)<F(7,6)
 return True
if __name__=='__main__':verify()