#!/usr/bin/python
# File:  aig2qbc
# Author:  mikolas
# Created on:  Thu Feb 28 16:20:35 WET 2013
# Copyright (C) 2013, Mikolas Janota
import re,sys
DBG=False

lc = 0

# read aig from [[input_stream]] and print QBC on [[out]]
def r(input_stream, out):
  global lc
  lc = 0
  phase = 0 # 0..header,1..inputs,2..outputs,3..ANDs
  inputs=[]
  outputs=[]
  print_qbc_header(out)
  false_used=False
  FALSE_ID=0 # ID of the variable representing the constant FALSE
             # used only when the constant is needed
  for line in input_stream:
    lc=lc+1
    if not line: continue
    if line[0]=='c': continue
    if phase==0: 
      # M = maximum variable index
      # I = number of inputs
      # L = number of latches
      # O = number of outputs
      # A = number of AND gates
      [ M, I, L, O, A ] = read_header(line)
      if L!=0: sorry('I do not know what latches are.')
      phase=1
      FALSE_ID=M+1
      continue
    if phase==1:
      if len(inputs)==I: phase=2 
      else: 
        il=int((line.split())[0])
        if (il&1)!=0: sorry('I am unable to encode negated inputs')
        inputs.append(il)
    if phase==2:
      if len(outputs)==O: phase=3 
      else:
        ol=int((line.split())[0])
        if (ol&1)!=0: sorry('I am unable to encode negated outputs')
        outputs.append(ol)
    if phase==3:
      if A<=0: phase=4
      ls = line.split()
      l0 = int(ls[0])
      l1 = int(ls[1])
      l2 = int(ls[2])
      fu = enc_andg(out,l0, l1, l2, FALSE_ID)
      false_used = false_used or fu
      A=A-1
  if false_used:
    print >>out, 'E', FALSE_ID+1, 'A 0' # TRUE constant
    print >>out, 'E', FALSE_ID, 'A', -(FALSE_ID+1), '0'
  print_qbc_concl(out)
  dbg("inputs", inputs)
  dbg("outputs", outputs)
      
def enc_andg(out,l0,l1,l2, FALSE_C):
  if (l0&1)!=0: sorry('I am unable to encode negated outputs of gates')
  ov = l0/2
  out.write('E ')
  out.write(str(ov))
  out.write(' A ')
  if (l1==0) or (l2==0):
    out.write(str(FALSE_C))
    out.write(' 0\n')
    return True
  if (l1!=1):
    if (l1&1)!=0: out.write('-')
    out.write(str(l1/2))
    out.write(' ')
  if (l2!=1):
    if (l2&1)!=0: out.write('-')
    out.write(str(l2/2))
  out.write(' 0\n')
  return False

def print_qbc_concl(out): out.write('CONCLUDE VALID\n')
def print_qbc_header(out): out.write('QBCertificate\n')

def dbg(s1,s2):
  if DBG: print >>sys.stderr, s1,":",s2

def warning (s) : 
  if lc>0: print 'warning:'+str(lc)+':',s
  else:  print 'warning',s

def error(s) : 
  if lc>0:  print 'error:'+str(lc)+':',s
  else:  print 'error:',s
  sys.exit(100) 

def sorry(s) : 
  if lc>0:  print 'sorry:'+str(lc)+':',s
  else:  print 'sorry:',s
  sys.exit(100) 

# read a header line of aig file, see [[r]] what meaning of numbers read
def read_header(line):
  m=re.match('^aag\s+([0-9]+)\s+([0-9]+)\s+([0-9]+)\s+([0-9]+)\s+([0-9]+)\s*$', line)
  if m:
    return map( lambda i: int(m.group(i)), range(1,6))
  else:
    error("failed to read header")

def main():
  r(sys.stdin, sys.stdout)

if __name__ == '__main__':
  main()