#!/usr/bin/python
# File:  qcnf2z3
# Author:  mikolas
# Created on:  Sat Nov 19 06:43:23 CAST 2011
# Copyright (C) 2011, Mikolas Janota
#
# USAGE: Accepts qdimacs on standard input and outputs smt2 

import string, sys, re, os 

# reading ----------------------------------- 
lc=0 # line counter

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) 


# input_stream where to get the formula
# quantifier   dictionary from levels to Boolean, where true means exists
# level        dictionary from variable to level
# clauses      list of clauses
# variables    set of variables
def read_formula(input_stream, quantifier, level, clauses, 
                 variables, free_vars):
  global lc
  lc=0
  current_level = 0
  last_q = '-'
  for line in input_stream:
    lc=lc+1
    line=line.strip()
    if len(line)==0: continue
    c=line[0]
    clause = []
    if   c=='c': continue
    elif c=='p':
      m=re.match('p\s+cnf\s+([0-9]+)\s+([0-9]+)\s*', line)
      if m:
        vs=int(m.group(1))
        cs=int(m.group(2))
      else:
        warning('error parsing p line')
    elif c=='a' or c=='e': 
      qvariables=map(int, line[1:].split())
      if len(qvariables)==0: warning('skipping empty quantifier',lc)
      else:
        if last_q != c:     # increase levels upon alternations
          last_q=c
          current_level=current_level + 1
          quantifier[current_level]=(c=='e') 
        zc=0 # zero counter
        for il in qvariables:
          if il < 0: warning('skipping negative variable')
          elif (il!=0): 
              variables.add(il)
              level[il]=current_level
          else: zc=zc+1
        if zc!=1: warning('there are no or  more than one zeros')
    else:
      for l in line.split():
         il=int(l)
         if il==0: # end of clause
           clauses.append(clause)
           clause = []
         else: 
           v=abs(il)
           if v not in variables: free_vars.add(v) 
           clause.append(il)   

def varn(vid): return 'x'+str(vid) # var name

#### main ####
formula_stream = sys.stdin
quantifier  = dict()
level       = dict()
clauses     = []
variables   = set()
free_vars   = set()

read_formula(formula_stream,quantifier, level, clauses, variables, free_vars)
if variables and free_vars: 
  error('formula contains both free and nonfree vars')

levels = 0 if not variables else max(map(lambda x: level[x], variables ))
print '(set-option :smt.relevancy 0)'
print '(set-option :smt.mbqi.max_iterations 1000000)'
print '(set-logic UFBV)'
print '(define-sort Bit () (_ BitVec 1))'

# Declare first level variables as global (it has exists semantics)
for vid in free_vars:
  print '(declare-fun', varn(vid), '() Bit)'
for vid in variables:
  if level[vid]==1:
    print '(declare-fun', varn(vid), '() Bit)'
# The whole formula is one assertion
negate = (levels>0) and not quantifier[1] # negate if first quant univ.
print '(assert'
# Print prefix
for l in range(2,levels+1): 
  existential = negate != quantifier[l]
  print ('(exists' if existential else '(forall'),
  print  '(',
  for vid in variables: 
    if  level[vid]==l: print '(', varn(vid), 'Bit)',
  print  ')' 
# Print clauses
if negate: print '(not'
if clauses:
 print  '(and '
 for c in clauses:
   if not c:
     print 'false'
     continue
   print  '(or ',
   for lit in c:
     print '(=', varn(abs(lit)), '#b'+('1' if lit>0 else '0'), ')',
   print  ')' # or 
 print  ')' # and 
else:
  print 'true'
if negate: print ')' # not
for i in range(levels-1): print  ')', 
print  ')' # assert 

print '(check-sat-using qfbv)'
#print '(get-model)'