import unittest
import copy
from example import *


class ScientificChecks(unittest.TestCase):
    def test_literal_current_response_identities_and_scaling(self):
        e=Core('A','B',F(9),F(1));x,y=F(99,100),F(593,600);p,q,ru,rv=e.currents(x,y)
        self.assertEqual(ru,(e.a+2*e.b)*(y-e.lower(x)));self.assertEqual(rv,(e.a+e.b)*(e.upper(x)-y));self.assertGreater(min(ru,rv),0)
        scaled=Core('A','B',90,10);self.assertEqual(scaled.lower(x),e.lower(x));self.assertEqual(scaled.currents(x,y),tuple(10*v for v in (p,q,ru,rv)))
        food=F(3,2);transformed=Core('A','B',e.a,e.b*food)
        self.assertEqual(e.currents(x,y,food),tuple(food*v for v in transformed.currents(x/food,y/food)))
        # Unit shortcut obstruction is a polynomial identity, not failed search.
        unit=Core('A','B',1,1);path=DirectedPath((unit,unit));G=DirectedPath((unit,)).polynomial(2);FF=path.polynomial(1)
        coefficients=[F(G.coefficients[i],G.denominator) if i<len(G.coefficients) else F(0) for i in range(5)]
        coefficients=[v-F(FF.coefficients[i],FF.denominator) for i,v in enumerate(coefficients)]
        self.assertEqual(coefficients,[F(0),F(1,12),F(7,24),-F(1,4),-F(1,8)])

    def test_rational_reconstruction_near_both_boundaries(self):
        for r in (2,3,5):
            path=DirectedPath(tuple(Core(str(i),str(i+1),F(2*i+3,3*i+1),F(5*i+2,7*i+3)) for i in range(r)))
            for x in (F(9,10),F(99,100)):
                lo,hi=path.response(x,2),path.response(x,1)
                for position in (F(1,10000),F(1,2),F(9999,10000)):
                    y=lo+position*(hi-lo);ell=min(y/2,F(1,10));state,stats=path.reconstruct(x,y,ell)
                    self.assertEqual(state[0],x);self.assertEqual(state[-1],y);self.assertLessEqual(stats['iterations'],stats['proved_budget'])
                    self.assertTrue(all(min(e.currents(u,v)[2:])>0 for e,u,v in zip(path.cores,state,state[1:])))
                with self.assertRaises(ValueError):path.reconstruct(x,lo,min(lo/2,F(1,10)))

    def test_decomposition_validation_and_limits(self):
        data=shortcut_data();data['paths']=[[1,0],[2]]
        with self.assertRaises(ValueError):Assembly(data)
        data=shortcut_data();data['boxes']={'B':['9/10','1']}
        with self.assertRaises(ValueError):Assembly(data)
        data=shortcut_data();data['boxes']={'A':['1','9/10']}
        with self.assertRaises(ValueError):Assembly(data)
        data=shortcut_data();data['paths']=[[0,1],[0]]
        with self.assertRaises(ValueError):Assembly(data)
        data=shortcut_data();data['edges'][0]['a']=9.0
        with self.assertRaises(ValueError):Assembly(data)
        self.assertEqual(BoundarySolver(max_junctions=1).solve(Assembly(shortcut_data()))['status'],'OUTSIDE_IMPLEMENTATION_LIMITS')

    def test_backend_witnesses_obstructions_and_unknown(self):
        for private,singleton in ((True,False),(False,False),(True,True),(False,True)):
            a=Assembly(shortcut_data(private,singleton=singleton));result=BoundarySolver().solve(a)
            self.assertEqual(result['status'],'SAT');a.check(result['activities'])
            if singleton:
                for s in a.junctions:self.assertEqual(F(result['activities'][s]),F(REFERENCE_ACTIVITIES[s]))
        self.assertEqual(BoundarySolver().solve(Assembly(shortcut_data(unit=True)))['status'],'UNSAT')
        data={'species':['A','B','C'],'junctions':['A','B','C'],'ell':'1/10','edges':[dict(u=u,v=v,a=1,b=1) for u,v in [('A','B'),('B','C'),('C','A')]],'paths':[[0],[1],[2]]}
        self.assertEqual(BoundarySolver().solve(Assembly(data))['status'],'UNSAT')
        self.assertEqual(BoundarySolver(max_queries=0).solve(Assembly(shortcut_data()))['status'],'UNKNOWN')
        empty=Assembly({'species':['isolated'],'junctions':[],'ell':'1/10','edges':[],'paths':[]});self.assertEqual(BoundarySolver().solve(empty)['activities'],{'isolated':'1/10'})

    def test_operating_certificates_and_strict_endpoints(self):
        a=Assembly(shortcut_data());x={s:F(v) for s,v in REFERENCE_ACTIVITIES.items()};c=OperatingCertificate(a,x)
        self.assertEqual(c.relative_radius(),(F(43,943),[F(11,236),F(43,943),F(21,304)]))
        self.assertEqual(c.relative_margin(F(1,25)),F(77,375000));self.assertEqual(c.relative_margin(F(43,943)),0)
        box={s:(v-F(1,10**6),v+F(1,10**6)) for s,v in x.items()};factors=[((e.a*F(24,25),e.a*F(26,25)),(e.b*F(24,25),e.b*F(26,25))) for e in a.cores]
        joint=c.joint_rectangle(box,factors);self.assertTrue(joint['productive_throughout']);self.assertEqual(F(joint['minimum_residual']),F(847959991,4687500000000));self.assertEqual(len(joint['corners']),24)
        food=c.food_window();self.assertEqual(food,(F(14814,14825),F(88859,88775)))
        for f in food:self.assertEqual(min(min(e.currents(x[e.source],x[e.target],f)[2:]) for e in a.cores),0)
        budget=c.instantaneous_budget();self.assertEqual(F(budget['strict_dilution_upper']),F(307,44550));self.assertEqual(sum(map(F,budget['production'].values())),F(budget['food_consumption']));self.assertEqual(F(budget['food_consumption']),F(2893,120000))

    def test_nongraded_linear_sufficient_construction(self):
        data,d=nongraded_data();a=Assembly(data);result=DeficitConstruction.from_deficits(a,d,F(1,10000))
        self.assertEqual(result['status'],'SAT');self.assertEqual(F(result['minimum_residual']),F(21,100000000));self.assertEqual([len(p.cores) for p in a.paths],[4,5])
        lp=DeficitConstruction.linear_program(a);self.assertEqual(lp['status'],'SAT');a.check(lp['activities'])
        failed=DeficitConstruction.linear_program(Assembly(shortcut_data(unit=True)));self.assertEqual(failed['status'],'NO_SUFFICIENT_CERTIFICATE')
        self.assertEqual(DeficitConstruction.from_deficits(a,d,F(1,2))['status'],'NO_SUFFICIENT_CERTIFICATE')

    def test_positive_polynomial_representation(self):
        for h in (1,2,4,8):
            path=DirectedPath(tuple(Core(str(i),str(i+1),1,1) for i in range(h)))
            for c in (1,2):
                p=path.polynomial(c);self.assertEqual(len(p.coefficients)-1,2**h);self.assertEqual(sum(p.coefficients),p.denominator);self.assertEqual(p.evaluate(F(9,10)),path.response(F(9,10),c))
            p=path.polynomial(1);self.assertEqual(F(p.coefficients[-1],p.denominator),F(1,2**(2**h-1)))


if __name__=='__main__':unittest.main()