import unittest
from itertools import combinations
from network import LiteralSource,SquareSearch,BinarySourceCodec
from linkage import CNF,DirectedLinkage,switch_check
from check_certificate import check
from example import examples

class ScientificChecks(unittest.TestCase):
    def test_literal_cancellation_and_signed_flow(self):
        e=examples();search=SquareSearch()
        self.assertEqual(search.search(e['literal_self_amplification'])['status'],'yes');self.assertEqual(search.search(e['net_only_cancellation_error'])['status'],'no_exhaustive')
        self.assertEqual(search.search(e['reverse_flow_needed'])['witness']['certificate']['flow'],[-1])
    def test_nontrivial_minimal_square_and_integer_witness(self):
        source=LiteralSource(('A','B','C'),('a','b','c'),((1,0,0),(0,1,0),(0,0,1)),((0,0,2),(2,0,0),(0,2,0)))
        result=SquareSearch().search(source);self.assertEqual(result['witness']['determinant'],7);self.assertEqual(result['witness']['certificate']['flow'],[7,7,7]);self.assertIn('PAC certified',result['witness']['minimality'])
        for q in [1,2]:
            for X in combinations(range(3),q):
                for S in combinations(range(3),q):
                    if source.admissible(X,S):
                        with self.assertRaises(ValueError):source.certificate(X,S)
        cert=result['witness']['certificate'];cert['flow'][0]=-100;self.assertFalse(check(cert)['accepted'])
    def test_no_and_unknown_and_external_resource(self):
        e=examples();self.assertEqual(SquareSearch().search(e['closed_conservative_cycle'])['status'],'no_exhaustive');self.assertEqual(SquareSearch(0).search(e['closed_conservative_cycle'])['status'],'unknown_budget');self.assertEqual(SquareSearch().search(e['external_resource'])['witness']['certificate']['entities'],[0])
    def test_binary_codec_and_invalid_inputs(self):
        s=examples()['external_resource'];bits=BinarySourceCodec.encode(s);other=BinarySourceCodec.decode(bits);self.assertEqual((other.left,other.right),(s.left,s.right));self.assertEqual(BinarySourceCodec.encode(other),bits)
        for bad in ['','1','100','110110','x01',bits+'0']:
            with self.assertRaises(ValueError):BinarySourceCodec.decode(bad)
        with self.assertRaises(ValueError):LiteralSource(('A',),('r',),((True,),),((1,),))
    def test_switch_all_simple_routes(self):self.assertTrue(switch_check()['all_three_properties'])
    def test_linkage_pairing_and_internal_cycle(self):
        vertices=('a0','a1','b0','b1','c','d');terms=vertices[:4]
        desired=DirectedLinkage(vertices,(('a0','c'),('c','b0'),('a1','b1')),terms);cert=desired.path_certificate((('a0','c','b0'),('a1','b1')));self.assertTrue(cert['verification']['accepted'])
        crossed=DirectedLinkage(vertices,(('a0','b1'),('a1','b0'),('c','d'),('d','c')),terms);self.assertEqual(SquareSearch().search(crossed.source())['status'],'no_exhaustive')
    def test_sat_wiring_boundaries_and_repeated_occurrences(self):
        for clauses,V in [((),0),(((1,1),),1),(((1,),(-1,2)),2)]:
            f=CNF(clauses,V);a=f.assignments();self.assertEqual(a['status'],'sat');g=f.compile();self.assertEqual(len(set(g.terminals)),4);self.assertTrue(g.path_certificate(f.satisfying_paths(a['assignment']))['verification']['accepted'])
        self.assertEqual(CNF(((),),0).assignments()['status'],'unsat_exhaustive');self.assertEqual(CNF(((1,),(-1,)),1).assignments()['status'],'unsat_exhaustive');self.assertEqual(CNF(((1,),),1).assignments(0)['status'],'unknown_budget')

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