"""

This function wraps the construction of an SMV netlist from a Verilog design via EBMC,
optionally injects an LTL assertion, then uses ABC to perform liveness checking on the result.

Function:
  runABC(name, module_name, nuXmvSpec, idtext, SVSpec=None)

Workflow:
 1. Record start time.
 2. Read original Verilog from `Benchmarks/{name}.sv`.
 3. If `SVSpec` is provided:
    - Inject `assert property ({SVSpec});` before `endmodule`.
    - Write modified SV to `Tools/abc_mc/SMV/{name}.sv`.
    - Call EBMC with `--smv-netlist` to produce `Tools/abc_mc/SMV/{name}.smv`.
    - Remove temporary `.sv` file.
 4. If no `SVSpec`, call EBMC directly on the original SV.
 5. Post-process the SMV file:
    - Keep content from the EBMC header onward.
    - Append `nuXmvSpec` if no SVSpec was injected.
    - Overwrite the SMV file.
 6. Convert SMV to AIG using ABC tools (`smvtoaig`, `ltl2smv`).
 7. Run `simple_liveness.sh` on the AIG.
 8. Measure and print total elapsed time.

Returns:
    abcT (float):     Execution time in seconds for the ABC-based liveness check.
"""

import os
import time
import re

def runABC(name, module_name, nuXmvSpec, idtext, SVSpec = None):
	begin = time.time()
	#os.system(f"rm ../../Tools/abc_mc/SMV/{name}.smv")
	with open(f"../../Benchmarks/{name}.sv", 'r') as file:
	    data = file.read()
	if SVSpec is not None:
		prop = f"\tp1: assert property  ({SVSpec}) ;\nendmodule"
		data = re.sub("endmodule", prop, data)
		with open(f"../../Tools/abc_mc/SMV/{name}.sv", "w") as file:
			file.write(data)
		print(data)
		os.system(f"ebmc ../../Tools/abc_mc/SMV/{name}.sv --smv-netlist > ../../Tools/abc_mc/SMV/{name}.smv")
		os.system(f"rm ../../Tools/abc_mc/SMV/{name}.sv")
	else:
		os.system(f"ebmc ../../Benchmarks/{name}.sv --smv-netlist > ../../Tools/abc_mc/SMV/{name}.smv")
	
	data = ""
	with open(f"../../Tools/abc_mc/SMV/{name}.smv", 'r') as file:
		data = file.read()
	data = data[data.find('-- Generated by EBMC') :]
	if SVSpec is None:
		data += "\n\n"+ nuXmvSpec
	with open(f"../../Tools/abc_mc/SMV/{name}.smv", "w") as file:
		file.write(data)
	os.system(f"../../Tools/abc_mc/smvtoaig -L ../../Tools/abc_mc/ltl2smv ../../Tools/abc_mc/SMV/{name}.smv ../../Tools/abc_mc/AIG/{name}.aig")
	print(f"\n\nABC LIVE evaluating {name}.aig\n")
	os.system(f"../../super-prove-build/build/super_prove/bin/simple_liveness.sh ../../Tools/abc_mc/AIG/{name}.aig")
	end = time.time()
	abcT = end - begin
	print(f"\n\nABC TIME: {abcT}\n")
	return abcT

