# gta clzs.py
import gta
import enum

class SymbolType(enum.Enum):
  FuncSymbol = 1
  FreeVar = 2
  SkolemConst = 3

class Symbol:
  def __init__(self, name, symType):
    self.name = name
    self.symType = symType
  @classmethod
  def defaulFreeVar(cls):
    return cls('x', SymbolType.FreeVar)
  def __str__(self):
    return self.name
  def __eq__(self, other):
    return (self.name == other.name and self.symType == other.symType)
  def __hash__(self):
    return hash(self.name) + hash(self.symType)


class Node:
  def __init__(self, funSym, varSym):
    if (not isinstance(funSym, Symbol) or
        not isinstance(varSym, Symbol)): raise RuntimeError()
    self.funSym = funSym
    self.varSym = varSym
    self.arcs = []
  def addDes(self, node, weight):
    if not isinstance(node, Node): raise RuntimeError()
    self.arcs.append((node, weight))
  def removeDes(self, tup):
    if not isinstance(tup[0], Node): raise RuntimeError()
    self.arcs.remove(tup)
  def __str__(self):
    s = 'Node:' + str(self.funSym) + '(' + str(self.varSym) + ')'
    return s
  def __eq__(self, other):
    return (self.funSym == other.funSym and self.varSym == other.varSym)
  def __hash__(self):
    return hash(self.funSym) + hash(self.varSym)


class Cluster:
  def __init__(self, funSym):
    if not isinstance(funSym, Symbol): raise RuntimeError()
    self.funSym = funSym
    self.nodes = []
  def addNode(self, node):
    if not isinstance(node, Node): raise RuntimeError()
    if node not in self.nodes:
      self.nodes.append(node)
  def removeNode(self, node):
    if not isinstance(node, Node): raise RuntimeError()
    self.nodes.remove(node)
  def getNode(self, tupSym):
    if type(tupSym) is not tuple: raise RuntimeError()
    if self.funSym != tupSym[0]: raise RuntimeError()
    for node in self.nodes:
      if node.varSym == tupSym[1]: return node
    return None
  def __str__(self):
    return 'Cluster:' + str(self.funSym)


# Literal is an edge in the graph, will be extended as a path
class Literal:
  def __init__(self, src, des, weight):
    if not isinstance(src, Node) or not isinstance(des, Node):
      raise RuntimeError()
    self.src = src
    self.des = des
    self.weight = weight
    self.history = None   # tuple of the 2 constituition literals
  def contains(self, node):
    return self.src == node or self.des == node
  def __eq__(self, other):
    return (self.src == other.src and self.des == other.des
            and self.weight == other.weight)
  def __hash__(self):
    return hash(self.src) + hash(self.des) + self.weight
  def __str__(self):
    s = '['
    s += str(self.src) + "->" + str(self.des) + ":" + str(self.weight) + ']'
    return s


class Graph:
  def __init__(self):
    self.clusters = {}  # {funSym:cluster}
    self.literals = []
  def _addNode(self, node):
    if not isinstance(node, Node): raise RuntimeError()
    cluster = self.getCluster(node.funSym)
    if cluster is None: cluster = Cluster(node.funSym)
    cluster.addNode(node)
    self.clusters[node.funSym] = cluster
  def addLiteral(self, literal):
    if not isinstance(literal, Literal): raise RuntimeError()
    if not literal in self.literals:
      self._addNode(literal.src)
      self._addNode(literal.des)
      literal.src.addDes(literal.des, literal.weight)
      self.literals.append(literal)
  def removeLiteralKeepingNode(self, literal):
    if not isinstance(literal, Literal): raise RuntimeError()
    self.literals.remove(literal)
    literal.src.removeDes((literal.des, literal.weight))
  def removeIsolatedNode(self, node):
    if not self.isIsolatedNode(node): raise RuntimeError()
    self.getCluster(node.funSym).removeNode(node)
  def getCluster(self, funSym):
    if not isinstance(funSym, Symbol): raise RuntimeError()
    return self.clusters.get(funSym)
  def getNode(self, tupSym):
    if type(tupSym) is not tuple: raise RuntimeError()
    cluster = self.getCluster(tupSym[0])
    if cluster is None: return None
    return cluster.getNode(tupSym)
  def isIsolatedNode(self, node):
    if not isinstance(node, Node): raise RuntimeError()
    for literal in self.literals:
      if literal.contains(node):
        if not literal.isSelfArc(): return False
    return True
  def __str__(self):
    s = ''
    for funSym, cluster in self.clusters.items():
      s += str(cluster) + '\n'
      for node in cluster.nodes:
        s += ' ' + str(node)
      s += '\n'
    return s

class Clause:
  def __init__(self):
    self.literals = []
  def addLiteral(self, literal):
    if not isinstance(literal, Literal): raise RuntimeError()
    self.literals.append(literal)
  def __str__(self):
    s = ''
    for literal in self.literals:
      s += str(literal)
    return s

class ClauseSet:
  def __init__(self):
    self.clauses = []
    self.literalDict = {}   # {literal:[clause]}
  def addClause(self, clause):
    if not isinstance(clause, Clause): raise RuntimeError()
    self.clauses.append(clause)
    for literal in clause.literals:
      assocClause = self.literalDict.get(literal)
      if assocClause is None: assocClause = []
      assocClause.append(clause)
      self.literalDict[literal] = assocClause
  def isUnsatistifiedWith(self, literals):
    literalsSet = set(literals)
    Debug.trace('compare:', *literalsSet)
    for c in self.clauses:
      found = True
      Debug.trace('with ', *c.literals)
      for lit in c.literals:
        if lit not in literalsSet:
          found = False
          break
      if found:
        Debug.trace('found unsatisfied clause!')
        return True
    Debug.trace('end-compare')
    return False
  def __str__(self):
    s = 'Begin ClauseSet\n'
    s += ' ' + 'All clauses:\n'
    for clause in self.clauses:
      s += '  ' + str(clause) + '\n'
    s += ' ' + 'Litearl and associative clauses:\n'
    for lit, clauses in self.literalDict.items():
      s += '  ' + str(lit) + ': ' + str(len(clauses)) + ' clauses\n'
    s += 'End ClauseSet'
    return s

class Cycle(Clause):
  def __init__(self, *arcs):
    super(Cycle, self).__init__()
    self.weight = 0
    self.positive = False
    self.negatePositive = False
    for arc in arcs:
      self.addLiteral(arc)
      self.weight += arc.weight
    if self.weight > 0:
      self.positive = True
    if len(self.literals) - self.weight > 0:
      self.negatePositive = True
  def __str__(self):
    s = ''
    if self.positive: s += 'positive cycle '
    if self.negatePositive: s += 'positive negated cycle '
    s += super(Cycle, self).__str__()
    return s

class Checker:
  def __init__(self, clauseSet, cycles):
    self.clauseSet = clauseSet
    self.positiveCycles = []
    for cycle in cycles:
      if cycle.positive:
        self.positiveCycles.append(cycle)
      if cycle.negatePositive:
        self.clauseSet.addClause(cycle)
  def check(self):
    def rec(clauseSet, cycleIndex, numCycles, literals):
      if cycleIndex == numCycles: return False
      for literal in self.positiveCycles[cycleIndex].literals:
        literals.append(literal)
        subUnsatisfied = False
        if clauseSet.isUnsatistifiedWith(literals):
          subUnsatisfied = True
        else:
          subUnsatisfied = rec(clauseSet, cycleIndex+1, numCycles, literals)
        del(literals[-1])
        if subUnsatisfied: return True
      return False

    numCycles = len(self.positiveCycles)
    return rec(self.clauseSet, 0, numCycles, [])


class Debug:
  debug = True
  @classmethod
  def trace(self, *args):
    if Debug.debug:
      s = 'Debug: '
      for a in args: s += str(a) + ' '
      print(s)
