import sys
import getopt
import warnings
from smt.z3solver import *
from smt.cvc5solver import *
from pycvc5 import Solver as CVCSolver
import json

from dds.read import read_dds, read_dpn_pnml, read_properties_pnml
from ltl.property import LTLProperty, CTLStarProperty
from dds.dds import DDS
from dds.dpn import DPN
from verification.constraint_graph import ConstraintGraph
from verification.product_construction import ProductConstruction
from verification.abstraction_equivalence import Equivalence
from verification.ctlstar import check_CTLstar
from verification.ltl import check_LTL
from verification.monitor import Trace, Monitor

### printing
def spaces(n):
  return "" if n <= 0 else " " + spaces(n-1) 


def fill_to(s, n):
  return s + spaces(n - len(s)) if len(s) < n else s[:n]

def read_input_file(model_file):
  is_pnml = "<pnml>" in open(model_file, "r").read()
  ltl_string = None
  if not is_pnml:
    dds_array = read_dds(model_file)
    dds = DDS(dds_array)
    ltl_string = dds_array["property"] if "property" in dds_array else None
  else:
    dpn = DPN(read_dpn_pnml(model_file))
    dds = dpn.to_DDS()
  return (dds, ltl_string)

def visualize_graphs(dds, cg, suffix):
  # ignore warnings that graph output was scaled
  warnings.filterwarnings("ignore", message = ".*graph is too large.*Scaling.*")
  outdir = "out"
  dds.show(outdir + "/ddsa" + ("_" + suffix if suffix else "") + ".png")
  cg.show(outdir + "/cg" + ("_" + suffix if suffix else "") + ".png")


def determine_finite_summary(dds, constraints, solver, verbose):
  (fin_summ, equiv) = dds.check_finite_summary(constraints, solver, verbose)
  if not fin_summ:
    print("Finite summary was not detected.")
    exit(0)

  if not (isinstance(equiv, Equivalence)):
    solver.destroy()
    del solver
    solver = Z3Solver(mode="qe")
    (fin_summ, equiv) = dds.check_finite_summary(constraints, solver, False)
  return (fin_summ, equiv, solver)


def cvc5_has_qe():
  solver = CVCSolver()
  qe = "getQuantifierElimination" # only available by hack
  return hasattr(solver, qe) #and callable(getattr(solver, qe))

### monitoring routine
def monitor(property_str, trace_param, suffix = "", verbose=True):
  # read trace
  if isinstance(trace_param, str) and os.path.exists(trace_param):
    tfile = open(trace_param, "r")
    trace = Trace(json.loads(tfile.read()))
  else:
    trace = Trace(trace_param)

  property = LTLProperty(property_str, trace.get_variables(), [])
  solver =  Z3Solver(mode="qe")  #CVC5Solver() if cvc5_has_qe() else Z3Solver(mode="qe") 
  monitor = Monitor(property, solver, suffix, verbose = verbose)
  return monitor.monitoring_state(trace, verbose = verbose)

def process_args(argv):
  usage = "arithmonitor.py -m <model_file> [-p <property_string> | -s] [-x]"
  dds_file = None
  property = None
  soundness = False
  trace = None
  suffix = ""
  try:
    opts, args = getopt.getopt(argv,"hsm:p:t:x:")
  except getopt.GetoptError:
    print(usage)
    sys.exit(2)
  for (opt, arg) in opts:
    if opt == '-h':
      print(usage)
      sys.exit()
    elif opt == "-m":
      dds_file = arg
    elif opt == "-p":
      property = arg
    elif opt == "-s":
      soundness = True
    elif opt == "-t":
      trace = arg
    elif opt == "-x":
      suffix = arg
  return (dds_file, property, soundness, trace, suffix)

if __name__ == "__main__":
  # parse command line arguments
  (dds_file, the_property, soundness, trace, ext) = process_args(sys.argv[1:])
  monitor(the_property, trace, suffix=ext)
  