iscas2symcnf

#!/usr/bin/python
class parser(): # takes the ISCAS 89 file as input and finds all input output pairs
    def __init__(self, ISCAS_filename):
        self.filename = ISCAS_filename
        self.gate_dict = {}
        self.output_set = []
        self.input_set = []

    def get_circuit_output(self, line):
        self.output_set.append(str(re.search('\((.+?)\)', line).group(1))) # add each output to the output set.

    def get_circuit_input(self, line):
        if "INPUT" in line:
            self.input_set.append(str(re.search('\((.+?)\)', line).group(1))) # add each output to the output set.

    def get_init_cond(self, line):
        if "INIT" in line:
            found = str(re.search('\((.*)\)', line).group(1)).strip()
            init_conditions = str(found).split(",") # split into a list of inputs [x1, ... xn]
            for i, input in enumerate(init_conditions):
                init_conditions[i] = input.strip()
            return init_conditions


    def get_output(self, line):
        return str(re.search('(.+?) =', line).group(1)).strip() # save outputs as strings to a variable


    def get_gate_type(self,line):
            try: # find each gate bounded by "= ... ("
                return str(re.search('= (.+?)\(', line).group(1)).strip()  # find each gate bounded by "= ... ("
            except:
                return None

    def get_input_set(self, line):
        if self.get_gate_type(line) == None:
            found = str(re.search('= (.*)', line).group(1)).strip()
            return [found] # Really hate this, but works for now. Standardizes inputs to set types
        else:
            found = re.search('\((.+?)\)', line).group(1) # find each input set inside brackets (x1 ... xn)
            input_set = str(found).split(",") # split into a list of inputs [x1, ... xn]
            for i, input in enumerate(input_set):
                input_set[i] = input.strip()
            return input_set

    def parse(self):
        init_cond_set = []
        file_id = open(self.filename, "r")
        lines = file_id.readlines()
        for line in lines:
            if "#" in line: # handle comments
                line = line[:line.index("#")]
            if "INIT" in line:
                init_cond_set = self.get_init_cond(line)

            if "OUTPUT" in line:
                self.get_circuit_output(line)

            if "=" in line: # find all lines with logic gates/circuits
                output = self.get_output(line)

                gate_type = self.get_gate_type(line)


                input_set = self.get_input_set(line)

                self.gate_dict[output] = [gate_type, input_set] # save the output: {gate_Type, input_set} pair to a dict

        return self.gate_dict, init_cond_set #self.output_set



class CNF_conversion(): # used to generate a Symbolic CNF file. An IR for use in a solver
    def __init__(self, CNF_filename, gate_dict, init_cond_set):
        self.gate_dict = gate_dict
        self.input_set = []
        self.gate_type = ""
        self.file_name = CNF_filename
        self.output = ''
        self.file_ID = open(CNF_filename, "w")
        self.not_gate_dict = {}
        self.init_cond_set = init_cond_set

    def AND(self):
        self.file_ID = open(self.file_name, "a")
        self.file_ID.write( "# "+ self.output + " = " + self.gate_type +  str(self.input_set) + "\n") # set comments

        all_variable_forumula = ""
        for input in self.input_set:
        # CNF formula representing: (!f + a) * (!f + b) ...
            self.file_ID.write("(" + input + " + " + self.negate(self.output) + ")\n")
            # DIMACS string representing (f + ~a + ~b ... )
            all_variable_forumula += " + " + self.negate(input)
        self.file_ID.write("(" + self.output + all_variable_forumula + ")\n")

    def OR(self):
        self.file_ID = open(self.file_name, "a")
        self.file_ID.write( "# "+ self.output + " = " + self.gate_type +  str(self.input_set) + "\n") # set comments

        all_variable_forumula = ""
        for input in self.input_set:
        # CNF formula representing: (~a + f) *(~b + f) ...
            self.file_ID.write("(" + self.negate(input) + " + " + self.output + ")\n")
            # DIMACS string representing (~f + a + b ... )
            all_variable_forumula += " + " + input
        self.file_ID.write("(" + self.negate(self.output) + all_variable_forumula + ")\n")


    def XOR(self):
        self.file_ID = open(self.file_name, "a")
        self.file_ID.write( "# "+ self.output + " = " + self.gate_type +  str(self.input_set) + "\n") # set comments
        all_variable_forumula = ""
        variable_set = []
        for input in self.input_set:
            variable_set.append(input)
        variable_set.append(self.output)

        for var_1 in variable_set: # this loop creates the (!f + a + b) (f + !a + b) (f + a + !b) terms
            formula_str = "("
            formula_str += self.negate(var_1)
            for var_2 in variable_set:
                if var_1 == var_2:
                    continue
                formula_str += " + " + var_2
            self.file_ID.write(formula_str + ")\n")

        formula_str = "("
        for input in self.input_set:
            formula_str += self.negate(input) + " + "

        self.file_ID.write(formula_str + self.negate(self.output) + ")\n")

            # for input_pos in self.input_set:
            #
            #     self.file_ID.write("(" + self.negate(input) + " + " + self.output + ")\n")
            #     # DIMACS string representing (~f + a + b ... )
            #     all_variable_forumula_neg += " + " + self.negate(input)
            # self.file_ID.write("(" + self.negate(self.output) + all_variable_forumula + ")\n")
    def XNOR(self):
        self.file_ID = open(self.file_name, "a")
        self.file_ID.write( "# "+ self.output + " = " + self.gate_type +  str(self.input_set) + "\n") # set comments
        all_variable_forumula = ""
        variable_set = []
        for input in self.input_set:
            variable_set.append(input)
        variable_set.append(self.output)

        for var_1 in variable_set: # this loop creates the (!f + !a + b) (f + !a + !b) (!f + a + !b) terms
            formula_str = "("
            formula_str += var_1
            for var_2 in variable_set:
                if var_1 == var_2:
                    continue
                formula_str += " + " + self.negate(var_2)
            self.file_ID.write(formula_str + ")\n")

        formula_str = "("
        for input in self.input_set:
            formula_str += input + " + "

        self.file_ID.write(formula_str + self.output + ")\n")

    def NAND(self):
        self.file_ID = open(self.file_name, "a")
        self.file_ID.write( "# "+ self.output + " = " + self.gate_type +  str(self.input_set) + "\n") # set comments
        all_variable_forumula = ""
        for input in self.input_set:
        # CNF formula representing: (f + a) * (f + b) ...
            self.file_ID.write("(" + input + " + " + self.output + ")\n")
            # DIMACS string representing (~f + ~a + ~b ... )
            all_variable_forumula += " + " + self.negate(input)
        self.file_ID.write("(" + self.negate(self.output) + all_variable_forumula + ")\n")



    def NOR(self):
        self.file_ID = open(self.file_name, "a")
        all_variable_forumula = ""
        self.file_ID.write( "# "+ self.output + " = " + self.gate_type +  str(self.input_set) + "\n") # set comments
        for input in self.input_set:
        # CNF formula representing: (~a + ~f) *(~b + ~f) ...
            self.file_ID.write("(" + self.negate(input) + " + " + self.negate(self.output) + ")\n")
            # DIMACS string representing (f + a + b ... )
            all_variable_forumula += " + " + input
        self.file_ID.write("(" + self.output + all_variable_forumula + ")\n")



    def NOT(self):
        self.file_ID = open(self.file_name, "a")
        self.file_ID.write( "# "+ self.output + " = " + self.gate_type +  str(self.input_set) + "\n") # set comments

        for input in self.input_set:
            # DIMACS string representing (~f + ~a)
            self.file_ID.write("(" + self.negate(input) + " + " + self.negate(self.output) + ")\n")
            # DIMACS string representing (f + a)
            self.file_ID.write("(" + input + " + " + self.output + ")\n")



    def negate(self, variable):
        if "!" in variable:
            variable = variable[1:]
        else:
            variable = "!" + variable
        return variable

    def DFF(self):
        return 0
        # self.file_ID = open(self.file_name, "a")
        #
        # for input in self.input_set:
        #     if input in self.not_gate_dict:
        #         input = self.not_gate_dict[input]
        #     self.file_ID.write( self.output+ " = DFF(" + input + ")" + "\n")

    def EQ(self):
        self.file_ID = open(self.file_name, "a")
        self.file_ID.write( "# "+ self.output + " = " +  str(self.input_set) + "\n") # set comments

        for input in self.input_set:
            # DIMACS string representing (~f + a)
            self.file_ID.write("(" + input + " + " + self.negate(self.output) + ")\n")
            # DIMACS string representing (f + ~a)
            self.file_ID.write("(" + self.negate(input) + " + " + self.output + ")\n")



    def get_cnf_from_gate(self):
        if self.gate_type == "AND":
            self.AND()
        elif self.gate_type == "OR":
            self.OR()
        elif self.gate_type == "XOR":
            self.XOR()
        elif self.gate_type == "NAND":
            self.NAND()
        elif self.gate_type == "NOR":
            self.NOR()
        elif self.gate_type == "NOT":
            self.NOT()
        elif self.gate_type == "DFF":
            self.DFF()
        elif self.gate_type == "XNOR":
            self.XNOR()
        elif self.gate_type == None:
            self.EQ()

        else:
            print("This gate type is unsupported: " + self.gate_type)


    def gate_dict_to_cnf(self):
        with open(self.file_name) as self.file_ID:
            for init_cond in self.init_cond_set:
                # Unit clauses for each init cond
                self.file_ID = open(self.file_name, "a")
                self.file_ID.write("(" + init_cond + ")\n")

            for self.output in self.gate_dict:
                self.gate_type = self.gate_dict[self.output][0] # Dict of the form gate_type[output] = [gate_type, input_set]
                self.input_set = self.gate_dict[self.output][1]
                self.get_cnf_from_gate()



def main():

    ###############################
    INPUT_FILE = str(sys.argv[1]) # "s27.isc"
    ###############################


    ###############################
    OUTPUT_FILE = str(sys.argv[2]) # "output_test.scnf"
    ###############################

    gate_dict, init_cond_set = parser(INPUT_FILE).parse()
    file_ID = open(OUTPUT_FILE , "w")

    CNF_conversion(OUTPUT_FILE , gate_dict, init_cond_set).gate_dict_to_cnf()

    return 0

if __name__ == '__main__':
    import re # used for parsing
    import sys # used for everything
    main()
    quit()


"""
 TODO:
 Add all logic functions
"""