from profiler import *

#from PropertyVerification.v2.disambiguate import Disambiguator
from core.himesis_utils import graph_to_dot, expand_graph

import multiprocessing
from multiprocessing import Manager

from PropertyVerification.v2.prover_worker import prover_worker

from util.progress import ProgressBar

import time
from time import sleep

class ContractProver:

    def __init__(self):
        #self.disambig = Disambiguator(0)

        self.verbosity = 2

        self.pathCondGen = None

        #super slow
        self.draw_success_failed = False

    def find_smallest_pc(self, pc_names):
        smallest = []
        smallestSize = 0

        for pc_name in pc_names:
            sizeCounter = len(pc_name.split("_"))
            if smallestSize == 0:
                smallest.append(pc_name)
                smallestSize = sizeCounter
            else:
                if sizeCounter < smallestSize:
                    smallest = [pc_name]
                    smallestSize = sizeCounter
                elif sizeCounter == smallestSize:
                    smallest.append(pc_name)

        return smallest


    #@do_cprofile
    #@profile
    def prove_contracts(self, pathCondGen, atomic_contracts, if_then_contracts):

        self.verbosity = pathCondGen.verbosity
        self.pathCondGen = pathCondGen

        print("\nStarting to prove contracts:")
        start_time = time.time()

        contract_failed_pcs = {}
        contract_succeeded_pcs = {}
        for contract_name, atomic_contract in atomic_contracts + if_then_contracts:
            print("Proving: " + atomic_contract.to_string())
            contract_failed_pcs[contract_name] = []
            contract_succeeded_pcs[contract_name] = []

        manager = Manager()
        cpu_count = multiprocessing.cpu_count()
        print("CPU Count: " + str(cpu_count))

        pc_queue = manager.Queue()
        results_queue = manager.Queue()

        workers = []

        for i in range(cpu_count):
            new_worker = prover_worker(i, self.verbosity, pc_queue, results_queue, atomic_contracts, if_then_contracts)
            new_worker.start()
            workers.append(new_worker)

        for pc, pc_name in pathCondGen.get_path_conditions(expand=False):
            pc_queue.put(pc)

        for i in range(cpu_count):
            pc_queue.put(None)

        #start a progress bar
        pc_set_length = pathCondGen.num_path_conditions
        progress_bar = ProgressBar(pc_set_length)

        len_pc_queue = pc_queue.qsize()
        while len_pc_queue > 0:
            progress_bar.update_progress(pc_set_length - len_pc_queue)
            sleep(1)
            len_pc_queue = pc_queue.qsize()

        for worker in workers:
            worker.join()

        for worker in workers:
            [fail, succeed] = results_queue.get()

            print("Thread finished at time: " + str(time.time() - start_time))

            for contract_name in fail.keys():
                contract_failed_pcs[contract_name] += fail[contract_name]
            for contract_name in succeed.keys():
                contract_succeeded_pcs[contract_name] += succeed[contract_name]



        proof_time = time.time() - start_time


        print("")
        for contract_name, atomic_contract in atomic_contracts + if_then_contracts:

            self.report_success_fail("Succeeded", contract_succeeded_pcs, contract_name)

            self.report_success_fail("Failed", contract_failed_pcs, contract_name)

            if self.draw_success_failed:
                atomic_contract.draw()

        print("Summary:")
        for contract_name, atomic_contract in atomic_contracts + if_then_contracts:
            print("Name:" + contract_name)
            print("\tNum Succeeded Contracts: " + str(len(contract_succeeded_pcs[contract_name])))
            print("\tNum Failed Contracts: " + str(len(contract_failed_pcs[contract_name])))

        print("Took " + str(proof_time) + " seconds to prove " + str(len(atomic_contracts + if_then_contracts)) + " contracts\n")

    def report_success_fail(self, status, list_of_pcs, contract_name):
        num_contracts_to_print = 20

        print("\n" + str(len(list_of_pcs[contract_name])) + " " + status + " PCs for " + contract_name + ":")

        if len(list_of_pcs[contract_name]) < num_contracts_to_print:
            for pc_name in sorted(list_of_pcs[contract_name]):
                self.print_name(pc_name)
        else:
            print("More than " + str(num_contracts_to_print) + " contracts")

        print ('\nSmallest Path Conditions where the contract ' + status + ':')
        success_smallest_pc_set = self.find_smallest_pc(list_of_pcs[contract_name])
        for pc_name in success_smallest_pc_set:
            self.print_name(pc_name)

        print('\n')

        if self.draw_success_failed:
            for pc, pc_name in self.pathCondGen.get_path_conditions(expand = False, get_pretty_name = False):
                if pc_name in list_of_pcs[contract_name]:
                    pc = expand_graph(pc)
                    graph_to_dot(contract_name + "_" + status + "_" + pc.name, pc)

    def print_name(self, name):

        contract_name_max_size = 300

        name = name[:contract_name_max_size]
        real_name_list = self.pathCondGen.rules_in_pc_real_name(name)
        print("_".join(real_name_list))
@@ -495,28 +495,8 @@
 ne%0A%0A
-        #super slow%0A
     
@@ -526,20 +526,19 @@
 ailed = 
-Fals
+Tru
 e%0A%0A    d
@@ -4594,24 +4594,16 @@
         
-success_
 smallest
@@ -4685,24 +4685,16 @@
 name in 
-success_
 smallest
@@ -4748,25 +4748,8 @@
     
-    print('%5Cn')%0A%0A
     
@@ -4797,168 +4797,58 @@
     
-for pc, pc_name in self.pathCondGen.get_path_conditions(expand = False, get_pretty_name = False):%0A                if pc_name in list_of_pcs%5Bcontract_name%5D:%0A    
+    shrunk_pc = self.pathCondGen.pc_dict%5Bpc_name%5D%0A
     
@@ -4881,16 +4881,19 @@
 aph(
+shrunk_
 pc)%0A
-    
     
@@ -4964,24 +4964,45 @@
 .name, pc)%0A%0A
+        print('%5Cn')%0A%0A
     def prin

Make drawing of succeeded slash failed pcs much faster.