import sexpParser
import pyparsing
import os.path
import sys
import subprocess

# Notes:
# 1. No shared variables included; shared optimization delayed...
# 2. Adding type constraints...

# ---------------------------------------------------------------
# Class for storing an Expression 
# ---------------------------------------------------------------
class Expr:
  def __init__(self, var=None, cst=None, op=None, args=[]):
    self.op = var if var!=None else cst if cst!=None else op
    self.args = args
  def __str__(self):
    '''print in Yices prefix s-expression syntax'''
    if self.args == []:
      assert type(self.op)==str, 'Err: not str {0}'.format(self.op)
      ans = "(" + self.op + ")"
    else:
      ans = "(" + self.op 
      for i in self.args:
        ans += " {0}".format(i)
      ans += ")"
    return ans
# ---------------------------------------------------------------

# ---------------------------------------------------------------
# Class for storing a EF-Yices input file 
# ---------------------------------------------------------------
class YicesFmla:
  def __init__(self,type_decls,fun_defs,evars,a,avars,b,c,aux):
    self.types = type_decls
    self.fun_defs = fun_defs	# list of (ffname, type, val)
    self.variables = evars	# dict from name to type string
    self.a = a			# list of asserted EXPRs 
    self.allvars = avars	# dict from name to type string
    self.b = b
    self.c = c
    self.aux = aux		# (line, lin1, lin2, fl) names...
  def add_to_a(self, e):
    self.a.append( e )
  def __str__(self):
    ans = ""
    for i in self.types:
      ans += str(i) + '\n'
    for (ff,ftype,fval) in self.fun_defs:
      ans += "(define {0}::{1} {2})\n".format(ff,ftype,fval)
    for (lin,v) in self.variables:
      for (i,j) in lin.items():
        for k in j:
          ans += "(define {0} :: {1})\n".format(k, v)
    for i in self.a:
      ans += "(assert {0})\n".format( i )
    ans += "(assert (forall ("
    for (lin,v) in self.allvars:
      if type(lin)!=dict:
        ans += "   {0} :: {1}\n".format(lin, v)
        continue
      for (i,j) in lin.items():
        for k in j:
          ans += "   {0} :: {1}\n".format(k, v)
    ans += " )\n"
    ans += " (=>\n"
    if len(self.b) > 1:
      ans += "  (and\n"
    for i in self.b:
      ans += "        {0}\n".format(i)
    if len(self.b) > 1:
      ans += "  )\n"		# for and
    if len(self.c) > 1:
      ans += "  (and\n"
    for i in self.c:
      ans += "        {0}\n".format(i)
    if len(self.c) > 1:
      ans += "  )\n"		# for and
    ans += "  )\n"              # for =>
    ans += "))\n\n"		# for assert forall
    ans += "(ef-solve)\n"
    return ans
# ---------------------------------------------------------------

# ---------------------------------------------------------------
def linename2blklinenum( linename ):
  '''input: b{0}l{num}'''
  l_index = linename.rfind( 'l' )
  linenum = int( linename[l_index+1:] )
  blk = linename[1:l_index]
  return (blk, linenum)
# ---------------------------------------------------------------

# ---------------------------------------------------------------
# Class for storing a Yices Model
# ---------------------------------------------------------------
class YicesModel:
  def __init__(self, model, yicesfmla, arityMap):
    self.model = model
    self.yicesfmla = yicesfmla
    self.arityMap = arityMap
  def get_val(self, var, default):
    if self.model.has_key(var):
      return self.model[var]
    else:
      return default
  def line2term(self, blk_linenum):
    '''return term coresponding to line number
    if blk_linenum has all vary, then output==[func,rec-t1,rec-t2]
    '''
    (line, lin1, lin2, fl, lin3) = self.yicesfmla.aux
    (blk, linenum) = blk_linenum
    func = self.get_val( fl[blk][linenum], None )
    l1 =   self.get_val( lin1[blk][linenum], None)
    l2 =   self.get_val( lin2[blk][linenum], None)
    if func==None and l1==None and l2==None:
      return ['base', blk, linenum]
    t1 = l1 if l1 == None else self.line2term( linename2blklinenum( l1 ) )
    if self.arityMap.has_key(func) and self.arityMap[func] == 2:
      t2 = l2 if l2 == None else self.line2term( linename2blklinenum( l2 ) )
      return [func, t1, t2]
    else:
      return [func, t1]
  def line_is_term_fmla(self, blk, linenum, term, depth, blocks):
    '''return fmla that says term_repr_at_line = term'''
    (line, lin1, lin2, fl, lin3) = self.yicesfmla.aux
    if term == None:
      return []
    assert len(term) in [2,3], 'Err: Term is {0}'.format(term)
    if term[0] == 'base':
      if blk == term[1] and linenum == term[2]:
        return ['true']
      else:
        return ['false']
    ans = []
    if self.model.has_key( fl[blk][linenum] ):
      if term[0] != None:
        ans.append( Expr(op='=', args=[fl[blk][linenum], term[0]]) )
    else:
      if term[0] != None:
        return ['false']
    # function part done...now move onto arguments...
    if depth == 0 or term[0] == None:
      return ans
    for j in range(1, len(term)):	# for each argument
      casesj = []
      for (blki,linei) in get_arg_choices(blocks, blk, linenum, term[0], j):
        ansi = self.line_is_term_fmla( blki, linei, term[j], depth-1, blocks )
        if ansi == ['false']:
          continue
        lin = lin2 if j==2 else lin1
        ansi.append( Expr(op='=', args=[ lin[blk][linenum], line[blki][linei] ]) )
        if len(ansi) > 1:
          casesj.append( Expr(op='and', args=ansi) )
        else:
          casesj.append( ansi[0] )
      if len(casesj) >= 2:
        fj = Expr(op='or', args=casesj)
      elif len(casesj) == 1:
        fj = casesj[0]
      else:
        fj = 'false'
      if fj == ['false']:
        return [fj]
      ans.append( fj )
    # fl=f and arg1=term[1] and arg2=term[2]
    return ans
    
  def negate(self, yfmla, blocks, blklines):
    '''return yfmla with a modified to reflect negation of this model'''
    '''add constraint to a that fl[N1-1] /= model[fl[N1-1,2]]'''
    #e1 = Expr(op='/=', args=[lin1[N1-1], self.model[ lin1[N1-1] ]])
    # new idea: analyze model, find smallest path from N1-1/N1-2 to l0,l1
    # negate that whole path
    #lines1 = self.get_relevant_lines( N1-1, [ 0, 1 ] )
    #lines2 = self.get_relevant_lines( N1-2, [ 0, 1 ] )
    #if len(lines1) <= len(lines2):
      #e1 = self.negate_lines(lines1) 
    #else:
      #e1 = self.negate_lines(lines2)
    # New new idea: do exact...
    fmla = { i: self.line2term(i) for i in blklines }
    print fmla
    ffList = []
    depth = 3
    for blkline in blklines:
      ffList.extend(self.line_is_term_fmla(blkline[0], blkline[1], fmla[blkline], depth, blocks ))
    e1 = Expr(op='not',args=[ mk_yices_and(ffList)])
    yfmla.add_to_a( e1 )
    return yfmla
  def get_relevant_lines( self, line_num, bases ):
    (line, lin1, lin2, fl, lin3) = self.yicesfmla.aux
    to_do, ans = [ line_num ], [ ]
    while len(to_do) > 0:
      line_num = to_do.pop()
      if line_num in ans or line_num in bases:
        continue
      ans.append(line_num)
      l1 = self.model[ lin1[ line_num ] ]
      l2 = self.model[ lin2[ line_num ] ]
      ln1 = int( l1[1:] )
      ln2 = int( l2[1:] )
      to_do.extend( [ln1, ln2] )
    return ans
  def negate_lines(self, lines):
    "lines = integer indices of lines; return not( fl[i]=model[ fl[i] ] and ...)"
    e = self.lines2fmla( lines )
    return Expr(op='not', args=[e])
  def lines2fmla(self, lines):
    "lines = integer indices of lines; return ( fl[i]=model[ fl[i] ] and ...)"
    (line, lin1, lin2, fl, lin3) = self.yicesfmla.aux
    ans = []
    for i in lines:
      ans.append( Expr(op='=', args = [ fl[i], self.model[fl[i]] ]) )
      ans.append( Expr(op='=', args = [ lin1[i], self.model[lin1[i]] ]) )
      ans.append( Expr(op='=', args = [ lin2[i], self.model[lin2[i]] ]) )
    return Expr(op='and', args = ans)
  def __str__(self):
    (line, lin1, lin2, fl, lin3) = self.yicesfmla.aux
    ans = ''
    for blk in line.keys():
      for i in range( len(line[blk]) ):
        if not self.model.has_key( fl[blk][i] ):
          continue
        if not self.model.has_key( lin1[blk][i] ):
          continue
        fi = self.model[ fl[blk][i] ]
        if self.arityMap[fi] == 2:
          ans += " {0} = {1} {2} {3};\n".format(line[blk][i], self.model[lin1[blk][i]], fi, self.model[lin2[blk][i]])
        elif self.arityMap[fi] == 3:
          ans += " {0} = {1}({2},{3},{4});\n".format(line[blk][i], fi, self.model[lin1[blk][i]], self.model[lin2[blk][i]], self.model[lin3[blk][i]])
        else:
          ans += " {0} = {2}({1});\n".format(line[blk][i], self.model[lin1[blk][i]], fi)
    ans += '-------------------------------------------------------\n\n'
    return ans
# ---------------------------------------------------------------

# ---------------------------------------------------------------
def parse_yices_output( tmpfilename ):
  "return object of class Model if there is one in tmpfp, else None"
  with open(tmpfilename, 'r') as fp:
    fstr = fp.read()
  if fstr.find('unsat') != -1:
    return None
  if fstr.find('unknown') != -1:
    return None
  lines = fstr.split('\n')
  m = {}
  for i in lines:
    if i.find(':=') == -1:
      continue
    varval = i.split(':=')
    assert len(varval) == 2, 'Err: var := val expected, found {0}'.format(i)
    m[varval[0].strip()] = varval[1].strip()
  return m
# ---------------------------------------------------------------

# ---------------------------------------------------------------
# line type, and line names
# ---------------------------------------------------------------
def paramexpr2int( expr, pdict ):
  if type(expr) != int:
    assert pdict.has_key(expr), 'Err: {0} not a param'.format(expr)
    expr = pdict[ expr ]
  return expr

def get_lines( blocks, pdict ):
  '''destructively updates blocks, replace na, nb etc by their values'''
  line_var_type = "lineType"
  line, lineList = {}, []
  for block in blocks:
    (block_name, block_len, block_code) = block
    block_len = paramexpr2int( block_len, pdict )
    block[1] = block_len    # destructively update to int value!!
    # now block_len is an integer
    bl = ["b{0}l{1}".format(block_name,i) for i in range(block_len)]
    line[block_name] = bl
    lineList.extend(bl)
  linescalartype = Expr(op="scalar", args=lineList)
  type_decl = Expr(op="define-type", args=["lineType", linescalartype ])
  return (line_var_type, type_decl, line)

def get_funcs( library ):
  '''library = [ (f 1), (xor 2), ...]'''
  func_var_type = "funcType"
  funcs = [i[0] for i in library]
  funcscalartype = Expr(op="scalar", args=funcs)
  type_decl = Expr(op="define-type", args=["funcType", funcscalartype])
  actuals = {}
  for i in funcs:
    actuals[i] = 'f{0}'.format(i)
  return (func_var_type, type_decl, actuals)
# ---------------------------------------------------------------

# ---------------------------------------------------------------
def mk_yices_or( cases ):
  "return (or (= expr1 exprList[0]) ...)"
  if len(cases) == 0:
    return "false"
  assert len(cases) > 0, 'ERR: Expecting >= 1 cases'
  if len(cases) > 1:
    return Expr(op="or", args=cases)
  else:
    return cases[0]

def mk_yices_and( cases ):
  "return (or (= expr1 exprList[0]) ...)"
  if len(cases) == 0:
    return "true"
  if len(cases) > 1:
    return Expr(op="and", args=cases)
  else:
    return cases[0]

def mk_yices_in( expr1, exprList):
  "return (or (= expr1 exprList[0]) ...)"
  cases = []
  for i in exprList:
    cases.append( Expr(op='=', args=[expr1, i]) )
  if len(cases) == 0:
    return "false"
  assert len(cases) > 0, 'ERR: Expecting >= 1 cases'
  if len(cases) > 1:
    return Expr(op="or", args=cases)
  else:
    return cases[0]

def mk_yices_var_in_blkList( var, blkList, index, lineNames, currblk ):
  '''blkList = [l1 l2 -]'''
  choices = []
  for blk in blkList:
    if blk == '-':
      choices.extend( [ lineNames[currblk][j] for j in range(index)] )
    else:
      choices.extend( lineNames[blk] )
  return mk_yices_in(var, choices)

def blk_choice1(choice, index, fvar, lin1v, lin2v, lineNames, blk, default):
  '''return Yices fmla for choice="(f (l1))" OR None '''
  ci = []
  # fl[blk][i]=fname and lin1[blk][i] in ... and ...
  fname = choice[0]
  fargs = choice[1:]
  assert type(fname)==str, 'Err: typ({1})={0}'.format(type(fname),fname)
  if fname == 'input' or fname == 'rand':
    return []
  ci.append( Expr(op='=', args=[fvar, fname]) )
  if len(fargs) >= 1:
    ci.append( mk_yices_var_in_blkList( lin1v, fargs[0], index, lineNames, blk))
  else:
    # optimization: fix to some ONE value
    ci.append( Expr(op='=', args=[lin1v, default[0]]) )
  if len(fargs) >= 2:
    ci.append( mk_yices_var_in_blkList( lin2v, fargs[1], index, lineNames, blk))
  else:
    ci.append( Expr(op='=', args=[lin2v, default[1]]) )
  yi = ci  # Expr(op='and', args=ci)
  return yi

def blk_choice1_new(choice, index, fvar, lin1v, lin2v, lin3v, lineNames, blk, default, tout):
  '''return Yices fmla for choice="(f (l1))" OR None '''
  # fl[blk][i]=fname and lin1[blk][i] in ... and ...
  fname = choice[0]
  fargs = choice[1:]
  assert type(fname)==str, 'Err: typ({1})={0}'.format(type(fname),fname)
  if fname == 'input' or fname == 'rand':
    ci = input_type_constraint(fargs, blk, index, tout)
    # ci = []
  elif len(fargs) == 1:
    ci = blk_choice_arity1(choice,fvar, blk, index, lin1v, lin2v, lin3v, lineNames, tout, default)
  elif len(fargs) == 2:
    ci = blk_choice_arity2(choice,fvar, blk, index, lin1v, lin2v, lin3v, lineNames, tout, default)
  elif len(fargs) == 3:
    ci = blk_choice_arity3(choice,fvar, blk, index, lin1v, lin2v, lin3v, lineNames, tout)
  else:
    assert False, 'Err: arity not 1 or 2'
  return ci  # Expr(op='and', args=ci)

def get_line_choices( blkList, currblk, currindex, lineNames ):
  '''blkList = [l1 l2 -]; return all (l1,0),(l1,1)... options'''
  # print blkList, currblk, currindex, lineNames
  ans = []
  for blk in blkList:
    if blk == '-':
      for i in range(currindex):
        ans.append( (currblk, i) )
    else:
      index = lineNames[blk] if type(lineNames[blk])==int else len(lineNames[blk])
      for i in range( index ):
        ans.append( (blk, i) )
  return ans

def get_arg_choices( blocks, blk, index, func, argnum):
  blockLenMap, blockCodeMap = {}, {}
  for (blockName, blockLen, blockCode) in blocks:
    blockLenMap[blockName] = blockLen
    blockCodeMap[blockName] = blockCode
  ans_blks = []
  for choice in blockCodeMap[blk]:
    if choice[0] != func and func != None:
      continue
    if len(choice) < argnum+1:
      continue
    for i in choice[argnum]:
      if i not in ans_blks:
        ans_blks.append( i )
  return get_line_choices( ans_blks, blk, index, blockLenMap )

def input_type_constraint(var_type, blk, index, tout):
  ''' tout[blk][index] = type_of_input or rand '''
  if var_type[0].find('::') == -1:
    print 'No type  declaration found in {0}'.format(var_type)
    return []
  # print var_type[0]
  # print var_type[1]
  var_type_list = var_type[0].split('::')
  assert len(var_type_list)==2, 'Err: No type  declaration found {0}'.format(var_type)
  typestr = var_type_list[1]
  typestr = sexpr2Expr( var_type[1],None,None,None ) if typestr == '' else typestr
  return [ Expr(op='=', args=[tout[blk][index], typestr]) ]

# These are NEW versions -- include type constraints, apart from syntactic constraints
def blk_choice_arity1(choice, fvar, currblk, currindex, lin1v, lin2v, lin3v, lineNames, tout, default):
  '''type constraint: fvar=fname and (or (lin1v=line and tfname(tNames[line],tout)))'''
  ci = []
  fname = choice[0]
  fargs = choice[1]
  ci.append( Expr(op='=', args=[fvar, fname]) )
  choices = get_line_choices(fargs, currblk, currindex, lineNames)
  # assert len(choices) > 0, 'Err: No lines as inputs?'
  if len(choices) == 0:
    return [ 'false' ]
  ors = []
  for (blk,ind) in choices:
    e1 =  Expr(op='=', args=[lin1v, lineNames[blk][ind]]) 
    e2 =  Expr(op='t{0}'.format(fname), args=[tout[blk][ind], tout[currblk][currindex]])
    ors.append( Expr(op='and', args=[e1, e2]) )
  ci.append( mk_yices_or( ors ) )
  ci.append( Expr(op='=', args=[lin2v, lineNames[default[1]][0]]) )
  ci.append( Expr(op='=', args=[lin3v, lineNames[default[2]][0]]) )
  return ci

def blk_choice_arity2(choice, fvar, currblk, currindex, lin1v, lin2v, lin3v, lineNames, tout, default):
  '''type constraint: fvar=fname and (or (lin1v=line and tfname(tNames[line],tout)))'''
  ci = []
  fname = choice[0]
  fargs1 = choice[1]
  fargs2 = choice[2]
  ci.append( Expr(op='=', args=[fvar, fname]) )
  choices1 = get_line_choices(fargs1, currblk, currindex, lineNames)
  choices2 = get_line_choices(fargs2, currblk, currindex, lineNames)
  # assert len(choices1) > 0 and len(choices2) > 0, 'Err: No lines as inputs?'
  if len(choices1) == 0 or len(choices2) == 0:
    return [ 'false' ]
  ors = []
  for (blk1,ind1) in choices1:
    for (blk2,ind2) in choices2:
      e1 =  Expr(op='=', args=[lin1v, lineNames[blk1][ind1]]) 
      e2 =  Expr(op='=', args=[lin2v, lineNames[blk2][ind2]]) 
      e3 =  Expr(op='t{0}'.format(fname), args=[tout[blk1][ind1], tout[blk2][ind2], tout[currblk][currindex]])
      ors.append( Expr(op='and', args=[e1, e2, e3]) )
  ci.append( mk_yices_or( ors ) )
  ci.append( Expr(op='=', args=[lin3v, lineNames[default[2]][0]]) )
  return ci

def blk_choice_arity3(choice, fvar, currblk, currindex, lin1v, lin2v, lin3v, lineNames, tout):
  '''type constraint: fvar=fname and (or (lin1v=line and tfname(tNames[line],tout)))'''
  ci = []
  fname = choice[0]
  fargs1 = choice[1]
  fargs2 = choice[2]
  fargs3 = choice[3]
  ci.append( Expr(op='=', args=[fvar, fname]) )
  choices1 = get_line_choices(fargs1, currblk, currindex, lineNames)
  choices2 = get_line_choices(fargs2, currblk, currindex, lineNames)
  choices3 = get_line_choices(fargs3, currblk, currindex, lineNames)
  # assert len(choices1) > 0 and len(choices2) > 0, 'Err: No lines as inputs?'
  if len(choices1) == 0 or len(choices2) == 0 or len(choices3) == 0:
    return [ 'false' ]
  ors = []
  for (blk1,ind1) in choices1:
    for (blk2,ind2) in choices2:
      for (blk3,ind3) in choices3:
        e1 =  Expr(op='=', args=[lin1v, lineNames[blk1][ind1]]) 
        e2 =  Expr(op='=', args=[lin2v, lineNames[blk2][ind2]]) 
        e3 =  Expr(op='=', args=[lin3v, lineNames[blk3][ind3]]) 
        e4 =  Expr(op='t{0}'.format(fname), args=[tout[blk1][ind1], tout[blk2][ind2], tout[blk3][ind3], tout[currblk][currindex]])
        ors.append( Expr(op='and', args=[e1, e2, e3, e4]) )
  ci.append( mk_yices_or( ors ) )
  return ci
# ---------------------------------------------------------------

# ---------------------------------------------------------------
def get_fname_app(library, aritymap, fname, args):
  assert library.has_key(fname), 'Err: Undefined {0}'.format(fname)
  actual = library[fname]
  arity = aritymap[fname]
  nargs = args[0:arity]
  return Expr(op=actual, args=nargs)
# ---------------------------------------------------------------

# ---------------------------------------------------------------
def get_all_fun_choices(block_code):
  funcs = []
  for choice in block_code:
    if choice[0] in ['input', 'rand']:
      continue
    funcs.append( choice[0] )
  return funcs

def get_all_arg_choices(blockMap, block_code, argNum, currblk, linei, default):
  ans_blks = []
  for choice in block_code:
    # choice = [ prod (L7) (L1 L2) ]
    if choice[0] in ['input', 'rand'] or len(choice) < 2+argNum:
      continue
    blks = choice[1 + argNum]
    for blk in blks:
      if blk not in ans_blks:
        ans_blks.append( blk )
  ans = get_line_choices( ans_blks, currblk, linei, blockMap )
  if (default[argNum],0) not in ans:
    ans.append( (default[argNum],0) )
  return ans
# ---------------------------------------------------------------

# ---------------------------------------------------------------
def cleanup(a):
  c = a.count('false')
  for i in range(c):
    a.remove('false')
  c = a.count(None)
  for i in range(c):
    a.remove(None)
  return a
# ---------------------------------------------------------------

# ---------------------------------------------------------------
def get_default_val( block_code, lineNames, blk ):
  '''defualt value for 2nd argument to use for unary func'''
  default = [None, None, None]
  for choice in block_code:
    if choice[0] in ['rand', 'input']:
      break
    if default[0] == None and len( choice ) >= 2:
      farg1 = choice[1]
      assert len(farg1) > 0, 'Err: arg choice zero?'
      for blk1 in farg1:
        if blk1 != '-':
          default[0] = blk1
          break
    if default[1] == None and len( choice ) == 3:
      farg2 = choice[2]
      assert len(farg2) > 0, 'Err: arg choice zero?'
      for blk2 in farg2:
        if blk2 != '-':
          default[1] = blk2
          break
    if default[2] == None and len( choice ) == 4:
      farg3 = choice[3]
      assert len(farg3) > 0, 'Err: arg choice zero?'
      for blk2 in farg3:
        if blk2 != '-':
          default[2] = blk2
          break
    if default[0] != None and default[1] != None and default[2] != None:
      return default
  if default[0] == None:
    default[0] = blk
  if default[1] == None:
    default[1] = blk
  if default[2] == None:
    default[2] = blk
  return default
# ---------------------------------------------------------------

# ---------------------------------------------------------------
def sexpr2efyices( sexpr, pdict ):
  '''input: s-expression from sketch file
     pdict is a dict from parameter name to int-value
     output: Object of class YicesFmla'''
  # print 'Processing the sketch', sexpr[0]
  sdict = {}
  for i in sexpr[1:]:
    sdict[i[0]] = i[1:]
  # now it is easy to access decls, inputs, parameters, etc...

  # process parameters
  if sdict.has_key('parameters'):
    param_names = sdict['parameters']
  else:
    param_names = []
  for i in param_names:
    assert pdict.has_key(i), 'ERR: Param {0} has no value'.format(i)
    print 'parameter {0} := {1}'.format(i, pdict[i])

  # process inputs

  # process blocks
  # lineType: b1l1, b1l2, ..., b3l1, ...
  blocks = sdict['blocks']
  (lineTypeName, lineTypeDecl, lineNames) = get_lines(blocks, pdict)
  library = sdict['library']
  (funcTypeName, funcTypeDecl, funcNames) = get_funcs(library)
  type_decls = [ lineTypeDecl, funcTypeDecl ]
  
  # now generate all the variables 
  # lineNames: dict blockName -> list of lines in that block
  # funcNames: dict abstract_func_name -> concrete_name
  # lin1, lin2: inputs for the lines
  # vin1, vin2: values for inputs the lines
  # tout, vout: type and values for outputs at each line
  lin1, lin2, lin3 = {}, {}, {}
  vin1, vin2, vin3 = {}, {}, {}
  fl, vout, tout = {}, {}, {}
  for (blk,lineList) in lineNames.items():
    lin1[blk] = ["{0}i1".format(l) for l in lineList]
    lin2[blk] = ["{0}i2".format(l) for l in lineList]
    lin3[blk] = ["{0}i3".format(l) for l in lineList]
    vin1[blk] = ["{0}v1".format(l) for l in lineList]
    vin2[blk] = ["{0}v2".format(l) for l in lineList]
    vin3[blk] = ["{0}v3".format(l) for l in lineList]
    fl[blk] = ["{0}f".format(l) for l in lineList]
    vout[blk] = ["{0}vo".format(l) for l in lineList]
    tout[blk] = ["{0}typ".format(l) for l in lineList]

  # set default : blk -> [blk,blk]
  default = {}
  for block in blocks:
    (blk, block_len, block_code) = block
    default[blk] = get_default_val( block_code, lineNames, blk )
  # exists- and forall-variables
  # not creating now, maybe later, perhaps not needed

  # now, create the a,b,c parts of the formula
  a,b,c = [],[],[]
  # ---------------------------------------------------------------------
  # first, declare "a" constraints
  # ---------------------------------------------------------------------
  # ---------------------------------------------------------------------
  # program well-formedness constraints on exists variables : lin[i] < i
  # ---------------------------------------------------------------------
  for block in blocks:
    (blk, block_len, block_code) = block
    assert type(block_len)==int, 'Err: Unexpected'
    for linei in range(block_len):
      yiList = []
      for choice in block_code:
        # yi = blk_choice1( choice, linei, fl[blk][linei], lin1[blk][linei], lin2[blk][linei], lineNames, blk, default )
        yi = blk_choice1_new( choice, linei, fl[blk][linei], lin1[blk][linei], lin2[blk][linei], lin3[blk][linei], lineNames, blk, default[blk], tout )
        yiList.append( yi )
      assert len(yiList) >= 1, 'Err: block_code empty??'
      if len(yiList) == 1:
        a.extend( yiList[0] )
      else:
        tmp = [ mk_yices_and(i) for i in yiList ]
        a.append( Expr(op='or', args=tmp) )
  # each output should be used?
  # type requirements should be satisfied
  # shared constraint???  ignoring for now...

  # ---------------------------------------------------------------------
  # Now constraint b -- guards for forall variables
  # ---------------------------------------------------------------------
  # vin1[blki][i] = vout[blkj][j] if lin1[blki][i]=line[blkj][j]
  arityMap = { i:int(j) for (i,j) in library }
  blockMap = { blk:blen for (blk,blen,code) in blocks }
  for block in blocks:
    (blk, block_len, block_code) = block
    # print '----Block {0} with {1} lines-------'.format(blk, block_len)
    func_choices = get_all_fun_choices(block_code)
    if func_choices == []:
      continue
    for linei in range(block_len):
      f, fvin1, fvin2, fvin3 = [], [], [], []
      arg1_choices = get_all_arg_choices(blockMap, block_code, 0, blk, linei, default[blk])
      for (blkj,j) in arg1_choices:
        case1 = Expr(op="=", args=[vin1[blk][linei],vout[blkj][j]])
        case2 = Expr(op="=", args=[lin1[blk][linei],lineNames[blkj][j]])
        fvin1.append( Expr(op="and", args=[case1, case2]) )
      b.append( mk_yices_or( fvin1) )
      arg2_choices = get_all_arg_choices(blockMap, block_code, 1, blk, linei, default[blk])
      for (blkj,j) in arg2_choices:
        case1 = Expr(op="=", args=[vin2[blk][linei],vout[blkj][j]])
        case2 = Expr(op="=", args=[lin2[blk][linei],lineNames[blkj][j]])
        fvin2.append( Expr(op="and", args=[case1, case2]) )
      b.append( mk_yices_or(fvin2) )
      arg3_choices = get_all_arg_choices(blockMap, block_code, 2, blk, linei, default[blk])
      for (blkj,j) in arg3_choices:
        case1 = Expr(op="=", args=[vin3[blk][linei],vout[blkj][j]])
        case2 = Expr(op="=", args=[lin3[blk][linei],lineNames[blkj][j]])
        fvin3.append( Expr(op="and", args=[case1, case2]) )
      b.append( mk_yices_or(fvin3) )
      # vout[blk][linei] = f() if fl = f
      for fname in func_choices:
        args = [vin1[blk][linei], vin2[blk][linei], vin3[blk][linei]]
        f1 = Expr(op="=", args=[vout[blk][linei], get_fname_app(funcNames, arityMap, fname,args)])
        f2 = Expr(op="=", args=[fl[blk][linei], fname])
        f.append( Expr(op="and", args=[f1, f2]) )
      b.append( mk_yices_or( f ) )
      # No constraint is added for rand and input; No special vars either
  # ---------------------------------------------------------------------
  # Now constraint c 
  # ---------------------------------------------------------------------
  # remove 'false' from a and b.
  #a = cleanup(a)
  #b = cleanup(b)
  cfmla = sdict['ensure']
  cfmls = [sexpr2Expr( i, vout, tout, pdict ) for i in cfmla] 
  c.extend( cfmls )
  # print 'a is: ', [ str(i) for i in a]
  # print 'b is: ', [ str(i) for i in b]
  # print 'c is: ', [ str(i) for i in c]
  # ---------------------------------------------------------------------
  # type_decls -- add all decls from sdict
  # ---------------------------------------------------------------------
  if sdict.has_key('decls'):
    decls_list = sdict['decls']
    type_decls.extend( [sexpr2Expr(i,vout,tout,pdict) for i in decls_list] )
  # print 'type_decls:'
  # for i in type_decls:
    # print str(i)

  # ---------------------------------------------------------------------
  # Now set evars and avars
  # ---------------------------------------------------------------------
  valTypeName = 'word'    # This is FIXED
  evars = [(lin1,lineTypeName), (lin2,lineTypeName), (fl,funcTypeName)] 
  evars.append( (lin3, lineTypeName) )
  evars.append( (tout, 'typ') )
  avars = [(vin1, valTypeName), (vin2, valTypeName), (vout,valTypeName)] 
  avars.append( (vin3, valTypeName) )
  avars.extend( sdict['inputs'] )
  aux = (lineNames, lin1, lin2, fl, lin3)
  return (YicesFmla(type_decls,[],evars,a,avars,b,c,aux), arityMap, sdict)
# --------------------------------------------------------------

# --------------------------------------------------------------
def sexpr2Expr( sexpr, vout, tout, pdict ):
  '''(= (output lm 1) (output l4 nb))'''
  if type(sexpr) != list:
    # assert type(sexpr) in [int,str], 'Err: Expected int or list'
    return sexpr
  if sexpr[0]=='output':
    blk, line = sexpr[1], sexpr[2]
    line = paramexpr2int( line, pdict)
    return vout[blk][line-1]
  if sexpr[0]=='type':
    blk, line = sexpr[1], sexpr[2]
    line = paramexpr2int( line, pdict)
    return tout[blk][line-1]
  # not base case
  myargs = [ sexpr2Expr( i, vout, tout, pdict) for i in sexpr[1:] ]
  return Expr(op=sexpr[0], args=myargs)
# --------------------------------------------------------------

# ---------------------------------------------------------------
def main():
  args = sys.argv[1:]
  if len(args) == 0:
    print 'Usage: python prog_synth.py f.sketch p1 p2 p3...'
    sys.exit(1)
  filename = args[0]
  assert os.path.isfile(filename), 'Error: File {0} does not exist'.format(filename)
  try:
    sexpr = sexpParser.sexp.parseFile(filename, parseAll=True)
    sexpr_list = sexpr.asList()
    #print sexpr_list
  except pyparsing.ParseFatalException, pfe:
    print "Error:", pfe.msg
    print pfe.markInputline('^')
  params, pdict = args[1:], {}
  for i in params:
    varval = i.split('=')
    assert len(varval) == 2, 'Err: var := val expected, found {0}'.format(i)
    pdict[varval[0]] = int( varval[1] )
  yfmla, arityMap, sdict = sexpr2efyices( sexpr_list[0], pdict )
  filename = "synth.ys"
  outfilename = filename[:-3] + '.yout'
  tmpfilename = 'tmp.txt'
  outfilefp = open( outfilename, 'w')
  number_answers = 1
  if pdict.has_key('answers'):
    number_answers = pdict['answers']
  if sdict.has_key('outputLines'):
    outputLines = [(i[0],int(i[1])-1) for i in sdict['outputLines'] ]
  for i in range(number_answers):
    with open( filename, "w") as fp:
      print >> fp, '(set-param ef-max-iters 20000)'
      print >> fp, str(yfmla)
    print "Created file {0} with EF Yices formula".format(filename)
    with open( tmpfilename, 'w' ) as tmpfp:
      subprocess.call(['yices_main', '--mode=ef', filename], stdout=tmpfp)
    model = parse_yices_output( tmpfilename )
    if model == None:
      print "No more models found, terminating at i = {0}".format(i)
      break
    model = YicesModel(model, yfmla, arityMap)
    print >> outfilefp, str(model)
    if sdict.has_key('outputLines'):
      yfmla = model.negate(yfmla, sdict['blocks'], outputLines)
  outfilefp.close()

if __name__ == "__main__":
    main()