text: import sys
  from sympy import *
  from typing import Any, List
  from multiprocessing import *
  import os 
  
  # Parse input string into a list of all parentheses and atoms (int or str),
  # exclude whitespaces.
  def normalize_str(string: str) -> List[str]:
      str_norm = []
      last_c = None
      for c in string:
          if c.isalnum():
              if last_c.isalnum():
                  str_norm[-1] += c
              else:
                  str_norm.append(c)
          elif not c.isspace():
              str_norm.append(c)
          last_c = c
      return str_norm
  
  # Generate abstract syntax tree from normalized input.
  def get_ast(input_norm: List[str]) -> List[Any]:
      ast = []
      # Go through each element in the input:
      # - if it is an open parenthesis, find matching parenthesis and make recursive
      #   call for content in-between. Add the result as an element to the current list.
      # - if it is an atom, just add it to the current list.
      i = 0
      while i < len(input_norm):
          symbol = input_norm[i]
          if symbol == '(':
              list_content = []
              match_ctr = 1 # If 0, parenthesis has been matched.
              while match_ctr != 0:
                  i += 1
                  if i >= len(input_norm):
                      raise ValueError("Invalid input: Unmatched open parenthesis.")
                  symbol = input_norm[i]
                  if symbol == '(':
                      match_ctr += 1
                  elif symbol == ')':
                      match_ctr -= 1
                  if match_ctr != 0:
                      list_content.append(symbol)             
              ast.append(get_ast(list_content))
          elif symbol == ')':
                  raise ValueError("Invalid input: Unmatched close parenthesis.")
          else:
              try:
                  ast.append(int(symbol))
              except ValueError:
                  ast.append(symbol)
          i += 1
      return ast
  
  
  translate = {}
  names = 0
  
  def parse_equal(s):
      global names
      string = ""
      if type(s[1]) is list :
          string += to_string(s[1])
      else :
          string += s[1]
      string += '='
      if type(s[2]) is list :
          string += to_string(s[2])
      else :
          string += s[2]
      names += 1
      translate['A' + str(names)]=string
      return 'A' + str(names)
  
  def parse_nequal(s):
      global names
      string = ""
      s = s[1]
      if type(s[1]) is list :
          string += to_string(s[1])
      else :
          string += s[1]
      string += '!='
      if type(s[2]) is list :
          string += to_string(s[2])
      else :
          string += s[2]
      names += 1
      translate['A' + str(names)]=string
      return 'A' + str(names)
  
  
  def parse_function(s):
      string = ""
      string += s[0] + "("
      for i in range(len(s)):
          if i is len(s)-1:
              string += to_string(s[i])
          elif i is not 0:
              string += s[i] + ","
      string += ")"
      return string
  
  def to_string(s):
      string = ""
      # Case: string
      if type(s) is not list:
          return s
      if(s[0] == '='):
          string += "("
          string += parse_equal(s)
          string += ")"
      elif(s[0] == 'not'):
          string += "("
          string += parse_nequal(s)
          string += ")"
      elif(s[0] == 'and'):
          string += "("
          for i in range(1,len(s)):
              string += to_string(s[i])
              if i != len(s)-1:
                  string += "&"
          string += ")"
      elif(s[0] == 'or'):
          string += "("        
          for i in range(1,len(s)):
              string += to_string(s[i])
              if i != len(s)-1:
                  string += "|"
          string += ")"
      # Function
      else:
          print("Function")
          string += "("
          string += parse_function(s)
          string += ")"
      return string
  
  def dnf(s):
      input_norm = normalize_str(s)
      ast = get_ast(input_norm)
      ast = ast[0]
      string = to_string(ast[1])
      to_replace =  str(to_dnf(string,simplify=False))
      to_replace = to_replace.replace('(','( ')
      to_replace = to_replace.replace(')',' )')
      array = to_replace.split()
      for i in range(len(array)):
          if array[i] != '&' and array[i] != '|' and array[i] != '(' and array[i] != ')':
              array[i] = translate[array[i]]
      result = ""
      for i in range(len(array)):
          result+=array[i]
      return result
  
  sat = []
  info = []
  
  def thread(i,l):
      x = []
      file = open("../benchmarks/eq_diamond/eq_diamond" + str(i) + ".smt2", "r")
      for f in file:
          x.append(f)
      file.close()
      print("Thread " + str(i) + " finished")
      l.acquire()
      try:
          sat.append(dnf(x[len(x)-3]))
          info.append(x[9])
          out = open("benchmarks_info.txt",'a')
          for i in range(len(info)):
              out.write(info[i]+'\n')
          out.close()
          out = open("benchmarks_formula.txt",'a')
          for i in range(len(sat)):
              out.write(sat[i]+'\n')
          out.close()
      finally:
          l.release()
  
  def multi_parser(m,n):
      threads=[]
      for i in range(1,n):
          lock = Lock()
          threads.append(Process(target=thread,args=(i,lock)))
      for t in threads:    
          t.start()
      for t in threads:
          t.join()
  
  
  def single_parser(i):
      x = []
      file = open("../benchmarks/eq_diamond/eq_diamond" + str(i) + ".smt2", "r")
      for f in file:
          x.append(f)
      file.close()
      sat.append(dnf(x[len(x)-3]))
      info.append(x[9])
      out = open("benchmarks_info.txt",'a')
      for i in range(len(info)):
          out.write(info[i]+'\n')
      out.close()
      out = open("benchmarks_formula.txt",'a')
      for i in range(len(sat)):
          out.write(sat[i]+'\n')
      out.close()
  
  
  def main():
      multi_parser(14,17)
      #single_parser(14)
  
      
  
  
  if __name__ == '__main__':
      main()