1#!/usr/bin/env python
2import sys, getopt
3
4QUEENS_MODE = 0
5QUEENS_MODE_NP1 = 1
6QUEENS_MODE_GTN = 2
7NO_THREE_IN_LINE_MODE = 3
8NO_THREE_IN_LINE_MODE_2NP1 = 4
9NO_THREE_IN_LINE_MODE_GT2N = 5
10
11SEQ_ADDER_ENCODING = 0
12PAR_ADDER_ENCODING = 1
13ITE_ENCODING = 2
14LOOKUP_ENCODING = 3
15SHIFTER_ENCODING = 4
16
17def usage():
18  print ("usage: queensbv [-h] [-s <size>] [-m <mode>] [-e <encoding>]")
19  print ("")
20  print (" available modes: ")
21  print ("   0:  regular queens mode (default)")
22  print ("   1:  try to place n + 1 queens on an n x n board")
23  print ("   2:  try to place m queens on an n x n board with m > n")
24  print ("   3:  regular no-3-in-line mode")
25  print ("   4:  no-3-in-line mode with 2 * n + 1 queens on an n x n board")
26  print ("   5:  no-3-in-line mode with m queens on an n x n board with m > 2n")
27  print ("")
28  print (" available encodings: ")
29  print ("   0:  simple adder encoding (default)")
30  print ("   1:  parallel adder encoding")
31  print ("   2:  if-then-else encoding")
32  print ("   3:  lookup encoding")
33  print ("   4:  shifter encoding")
34  print ("")
35  sys.exit(0)
36
37def die(msg):
38  assert msg != None
39  print (msg)
40  sys.exit(1)
41
42def is_power_of_2 (x):
43  assert x > 0
44  return (x & (x - 1)) == 0
45
46def next_power_of_2 (x):
47  assert x > 0
48  x -= 1
49  i = 1
50  while i < 32:
51    x = x | (x >> i)
52    i *= 2
53  return x + 1
54
55def log2 (x):
56  result = 0
57  assert x > 0
58  assert is_power_of_2 (x)
59  while x > 1:
60    x >>= 1
61    result += 1
62  assert result >= 0
63  return result
64
65def board_field (x, y):
66  assert x >= 0
67  assert y >= 0
68  return "board" + str(x) + "_" + str(y)
69
70mode = QUEENS_MODE
71encoding = SEQ_ADDER_ENCODING
72size = 8
73id = 1
74constraints = []
75num_bits_size = 0
76num_bits_fields = 0
77shiftvarslistmap = {}
78shiftvarscounter = 0
79logsize = -1
80
81def add_seq (list, ext):
82  global id
83
84  assert list != None
85  assert len (list) >= 2
86  assert ext >= 0
87
88  print ("(let (?e" + str(id) + " (zero_extend[" + str(ext) + \
89         "] " + list[0] + "))")
90  last = "?e" + str(id)
91  id += 1
92  for i in range(1, len(list)):
93    print ("(let (?e" + str(id) + " (bvadd " + last + " (zero_extend[" + \
94           str(ext) + "] " + list[i] + ")))")
95    last = "?e" + str(id)
96    id += 1
97  return last, ext + 1
98
99def add_par (list, bw):
100  global id
101
102  assert list != None
103  assert len (list) >= 2
104  assert bw > 0
105
106  while len(list) != 1:
107    i = 0
108    next = []
109    while i < len(list):
110      if i != len(list) - 1:
111        print ("(let (?e" + str(id) + " (bvadd (zero_extend[1] " + \
112               list[i] + ") (zero_extend[1] " + list[i + 1] + ")))")
113      else:
114        print ("(let (?e" + str(id) + " (zero_extend[1] " + list[i] + "))")
115      last = "?e" + str(id)
116      next.append(last)
117      id += 1
118      i += 2
119    list = next
120    bw += 1
121  return last, bw
122
123def or_par (list, bw):
124  global id
125
126  assert list != None
127  assert len (list) >= 2
128  assert bw > 0
129
130  while len(list) != 1:
131    i = 0
132    next = []
133    while i < len(list):
134      if i != len(list) - 1:
135        print ("(let (?e" + str(id) + " (bvor " + list[i] + " " + list[i + 1] + \
136               "))")
137      else:
138        print ("(let (?e" + str(id) + " (bvor " + list[i] + " " + \
139               "bv0[" + str(bw) + "]))")
140      last = "?e" + str(id)
141      next.append(last)
142      id += 1
143      i += 2
144    list = next
145  return last
146
147def and_par (list, bw):
148  global id
149
150  assert list != None
151  assert len (list) >= 2
152  assert bw > 0
153
154  bits = ""
155  for i in range(bw):
156    bits += "1"
157  while len(list) != 1:
158    i = 0
159    next = []
160    while i < len(list):
161      if i != len(list) - 1:
162        print ("(let (?e" + str(id) + " (bvand " + list[i] + " " + \
163               list[i + 1] + "))")
164      else:
165        print ("(let (?e" + str(id) + " (bvand " + list[i] + " " + \
166               "bv" + str(int(bits, 2)) + "[" + str(bw) + "]))")
167      last = "?e" + str(id)
168      next.append(last)
169      id += 1
170      i += 2
171    list = next
172  return last
173
174def add_lookup_8_4 (list):
175  global id
176  global lookup
177
178  assert list != None
179  assert len(list) != 1
180
181  addlist = []
182  numloops = len(list) / 8
183  if (len(list) % 8) > 0:
184    numloops += 1
185  for i in range(numloops):
186    concatlist = []
187    for j in range(8):
188      if i * 8 + j < len(list):
189        concatlist.append (list[i * 8 + j])
190      else:
191        concatlist.append ("bv0[1]")
192    last = concat_list (concatlist)
193    print ("(let (?e" + str(id) + " (select " + lookup + " " + last + "))")
194    last = "?e" + str(id)
195    id += 1
196    addlist.append (last)
197  assert len(addlist) > 0
198  if len(addlist) == 1:
199    return addlist[0], 4
200  else:
201    return add_par (addlist, 4)
202
203def ite_encode_eq_rec (list, pos, k):
204  assert list != None
205  assert pos >= 0
206
207  if pos == len(list):
208    if k == 0:
209      return "true"
210    return "false"
211  if len(list) - pos < k or k < 0:
212    return "false"
213  result = "(if_then_else (= " + list[pos] + " bv1[1]) "
214  result += ite_encode_eq_rec (list, pos + 1, k - 1) + " "
215  result += ite_encode_eq_rec (list, pos + 1, k) + ")"
216  return result
217
218def ite_encode_eq (list, k):
219  global id
220
221  assert list != None
222  assert len(list) >= 2
223  assert k > 0
224  result = ite_encode_eq_rec (list, 0, k)
225  sys.stdout.write("(flet ($e" + str(id) + " " + result +")\n")
226
227def ite_encode_lt_rec (list, pos, counter, k):
228  assert list != None
229  assert pos >= 0
230  assert counter >= 0
231
232  if len(list) - pos + counter < k:
233    return "true"
234  if counter >= k:
235    return "false"
236  result = "(if_then_else (= " + list[pos] + " bv1[1]) "
237  result += ite_encode_lt_rec (list, pos + 1, counter + 1, k) + " "
238  result += ite_encode_lt_rec (list, pos + 1, counter, k) + ")"
239  return result
240
241def ite_encode_lt (list, k):
242  global id
243
244  assert list != None
245  assert len(list) >= 2
246  assert k > 0
247  result = ite_encode_lt_rec (list, 0, 0, k)
248  sys.stdout.write("(flet ($e" + str(id) + " " + result +")\n")
249
250def ite_encode_ge (list, k):
251  global id
252
253  assert list != None
254  assert len(list) >= 2
255  assert k > 0
256  result = ite_encode_lt_rec (list, 0, 0, k)
257  sys.stdout.write("(flet ($e" + str(id) + " (not " + result +"))\n")
258
259def concat_list (list):
260  global id
261
262  assert list != None
263  assert len(list) >= 2
264
265  while len(list) != 1:
266    i = 0
267    next = []
268    while i < len(list):
269      if i != len(list) - 1:
270        print ("(let (?e" + str(id) + " (concat " + list[i] + " " + \
271               list[i + 1] + "))")
272      else:
273        next.pop()
274        print ("(let (?e" + str(id) + " (concat " + last + " " + list[i] + "))")
275      last = "?e" + str(id)
276      next.append(last)
277      id += 1
278      i += 2
279    list = next
280  return last
281
282def shift_encode_eq_1 (list, shiftvarlist):
283  global id
284  global logsize
285
286  assert list != None
287  assert len(list) >= 2
288  assert shiftvarlist != None
289  assert len(shiftvarlist) >= 1
290
291  listlen = len(list)
292  print ("(let (?e" + str(id) + " (bvshl bv1[" + str(listlen) + "] " + \
293         "(zero_extend[" + str(listlen - logsize) + "] " + \
294         shiftvarlist.pop() + ")))")
295  last = "?e" + str(id)
296  id += 1
297  vec = concat_list (list)
298  print ("(flet ($e" + str(id) + " (= " + last + " " + vec + "))")
299
300def shift_encode_eq_2 (list, shiftvarlist):
301  global id
302  global logsize
303
304  assert list != None
305  assert len(list) >= 2
306  assert shiftvarlist != None
307  assert len(shiftvarlist) >= 1
308
309  listlen = len(list)
310  print ("(let (?e" + str(id) + " (bvshl bv1[" + str(listlen) + "] " + \
311         "(zero_extend[" + str(listlen - logsize) + "] " + \
312         shiftvarlist.pop() + ")))")
313  shift1 = "?e" + str(id)
314  id += 1
315  print ("(let (?e" + str(id) + " (bvshl bv1[" + str(listlen) + "] " + \
316         "(zero_extend[" + str(listlen - logsize) + "] " + \
317         shiftvarlist.pop() + ")))")
318  shift2 = "?e" + str(id)
319  id += 1
320  print ("(let (?e" + str(id) + " (bvor " + shift1 + " " + shift2 + "))")
321  orshift = "?e" + str(id)
322  id += 1
323  vec = concat_list (list)
324  print ("(flet ($e" + str(id) + " (= " + orshift + " " + vec + "))")
325  and1 = "$e" + str(id)
326  id += 1
327  print ("(flet ($e" + str(id) + " (not (= " + shift1 + " " + shift2 + ")))")
328  and2 = "$e" + str(id)
329  id += 1
330  print ("(flet ($e" + str(id) + " (and " + and1 + " " + and2 + "))")
331
332def shift_encode_eq_k (list, shiftvarlist, k):
333  global id
334
335  assert list != None
336  assert len(list) >= 2
337  assert shiftvarlist != None
338  assert k > 2
339  assert len(shiftvarlist) >= k
340
341  listlen = len(list)
342  log2listlen = log2(listlen)
343  orlist = []
344  for i in range (k):
345    print ("(let (?e" + str(id) + " (bvshl bv1[" + str(listlen) + "] " + \
346           "(zero_extend[" + str(listlen - log2listlen) + "] " + \
347           shiftvarlist.pop() + ")))")
348    last = "?e" + str(id)
349    id += 1
350    orlist.append (last)
351  orshift = or_par (orlist, listlen)
352  vec = concat_list (list)
353  print ("(flet ($e" + str(id) + " (= " + orshift + " " + vec + "))")
354  and1 = "$e" + str(id)
355  id += 1
356  print ("(flet ($e" + str(id) + " (distinct")
357  for i in range(len(orlist)):
358    print (orlist[i])
359  print ("))")
360  and2 = "$e" + str(id)
361  id += 1
362  print ("(flet ($e" + str(id) + " (and " + and1 + " " + and2 + "))")
363
364def shift_encode_gt_k (list, shiftvarlist, shiftvarlistone, k):
365  global id
366
367  assert list != None
368  assert len(list) >= 2
369  assert shiftvarlist != None
370  assert shiftvarlistone != None
371  assert len(shiftvarlistone) > 0
372  assert k > 2
373  assert len(shiftvarlist) >= len(list) - k - 1 - 1
374
375  listlen = len(list)
376  log2listlen = log2(listlen)
377  andlist = []
378  bits = "10"
379  for i in range(2, listlen):
380    bits += "1"
381
382  print ("(let (?e" + str(id) + " (concat " + shiftvarlistone.pop() + " bv" + \
383         str(2 ** (listlen - 2)) + "[" + str(listlen - 1) + "]))")
384  last = "?e" + str(id)
385  id += 1
386  andlist.append (last)
387
388  for i in range (1, len(list) - k - 1):
389    print ("(let (?e" + str(id) + " (bvashr bv" + str(int(bits, 2)) + "[" + \
390           str(listlen) + "] " + shiftvarlist.pop() + "))")
391    last = "?e" + str(id)
392    id += 1
393    andlist.append (last)
394  andshift = and_par (andlist, listlen)
395  vec = concat_list (list)
396  print ("(flet ($e" + str(id) + " (= " + andshift + " " + vec + "))")
397
398def shift_encode_le_1 (list, shiftvarlist):
399  global id
400
401  assert list != None
402  assert len(list) >= 2
403  assert shiftvarlist != None
404  assert len(shiftvarlist) >= 1
405
406  listlen = len(list)
407  print ("(let (?e" + str(id) + " (bvshl bv1[" + str(listlen) + "] " + \
408         shiftvarlist.pop() + "))")
409  last = "?e" + str(id)
410  id += 1
411  vec = concat_list (list)
412  print ("(flet ($e" + str(id) + " (= " + last + " " + vec + "))")
413
414def shift_encode_le_2 (list, shiftvarlist):
415  global id
416
417  assert list != None
418  assert len(list) >= 2
419  assert shiftvarlist != None
420  assert len(shiftvarlist) >= 1
421
422  listlen = len(list)
423  print ("(let (?e" + str(id) + " (bvshl bv1[" + str(listlen) + "] " + \
424         shiftvarlist.pop() + "))")
425  shift1 = "?e" + str(id)
426  id += 1
427  print ("(let (?e" + str(id) + " (bvshl bv1[" + str(listlen) + "] " + \
428         shiftvarlist.pop() + "))")
429  shift2 = "?e" + str(id)
430  id += 1
431  print ("(let (?e" + str(id) + " (bvor " + shift1 + " " + shift2 + "))" )
432  orshift = "?e" + str(id)
433  id += 1
434  vec = concat_list (list)
435  print ("(flet ($e" + str(id) + " (= " + orshift + " " + vec + "))")
436  and1 = "$e" + str(id)
437  id += 1
438  print ("(flet ($e" + str(id) + " (not (= " + shift1 + " " + shift2 + ")))")
439  and2 = "$e" + str(id)
440  id += 1
441  print ("(flet ($e" + str(id) + " (and " + and1 + " " + and2 + "))")
442
443
444try:
445  opts, args = getopt.getopt(sys.argv[1:], "hm:s:e:")
446except getopt.GetoptError as err:
447  print (str(err))
448  usage()
449
450for o, a in opts:
451  if o in ("-h"):
452    usage()
453  elif o in ("-m"):
454    if a == "0":
455      mode = QUEENS_MODE
456    elif a == "1":
457      mode = QUEENS_MODE_NP1
458    elif a == "2":
459      mode = QUEENS_MODE_GTN
460    elif a == "3":
461      mode = NO_THREE_IN_LINE_MODE
462    elif a == "4":
463      mode = NO_THREE_IN_LINE_MODE_2NP1
464    elif a == "5":
465      mode = NO_THREE_IN_LINE_MODE_GT2N
466    else:
467      die ("mode must be >= 0 and <= 5")
468  elif o in ("-e"):
469    if a == "0":
470      encoding = SEQ_ADDER_ENCODING
471    elif a == "1":
472      encoding = PAR_ADDER_ENCODING
473    elif a == "2":
474      encoding = ITE_ENCODING
475    elif a == "3":
476      encoding = LOOKUP_ENCODING
477    elif a == "4":
478      encoding = SHIFTER_ENCODING
479    else:
480      die ("encoding must be >= 0 and <= 4")
481  elif o in ("-s"):
482    size = int (a)
483    if size < 4:
484      die ("size must be >= 4")
485
486if encoding == SHIFTER_ENCODING:
487  if not is_power_of_2 (size):
488    die ("shifter encoding needs that the board size is a power of two")
489  logsize = log2(size)
490
491sizesqr = size * size
492num_bits_size = log2 (next_power_of_2 (size + 1))
493num_bits_fields = log2 (next_power_of_2 (sizesqr + 1))
494
495if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
496   mode == NO_THREE_IN_LINE_MODE_GT2N:
497  print ("(benchmark queensNoThreeInLine" + str(size) + "x" + str(size) )
498else:
499  print ("(benchmark queens" + str(size) + "x" + str(size))
500print (":source {")
501if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
502   mode == NO_THREE_IN_LINE_MODE_GT2N:
503  print ("BV encoding of no three-in-line problem")
504else:
505  print ("BV encoding of n-queens problem")
506if mode == QUEENS_MODE:
507  print ("We try to place " + str(size) + \
508         " queens on a " + str(size) + " x " + str(size) + " board")
509elif mode == QUEENS_MODE_NP1:
510  print ("We try to place n + 1 queens on an n x n board")
511elif mode == QUEENS_MODE_GTN:
512  print ("We try to place m queens on an n x n board with m > n")
513elif mode == NO_THREE_IN_LINE_MODE:
514  print ("We try to place " + str(2 * size) + \
515         " queens on a " + str(size) + " x " + str(size) + " board")
516elif mode == NO_THREE_IN_LINE_MODE_2NP1:
517  print ("We try to place " + str(2 * size + 1) + \
518         " queens on a " + str(size) + " x " + str(size) + " board")
519elif mode == NO_THREE_IN_LINE_MODE_GT2N:
520  print ("We try to place m queens on an n x n board with m > 2n")
521if encoding == SEQ_ADDER_ENCODING:
522  print ("Cardinality constraints are encoded by simple adder circuits")
523elif encoding == PAR_ADDER_ENCODING:
524  print ("Cardinality constraints are encoded by parallel adder circuits")
525elif encoding == ITE_ENCODING:
526  print ("Cardinality constraints are encoded by ITEs")
527elif encoding == SHIFTER_ENCODING:
528  print ("Cardinality constraints are encoded by shifters")
529else:
530  assert encoding == LOOKUP_ENCODING
531  print ("Cardinality constraints are encoded by lookups and parallel adders")
532print ("Contributed by Robert Brummayer (robert.brummayer@gmail.com)")
533print ("}")
534if mode == QUEENS_MODE:
535  print (":status sat")
536elif mode == NO_THREE_IN_LINE_MODE:
537  print (":status unknown")
538else:
539  print (":status unsat")
540if encoding == LOOKUP_ENCODING:
541  print (":logic QF_AUFBV")
542  print (":extrafuns ((lookup Array[8:4]))")
543else:
544  print (":logic QF_BV")
545for i in range(size):
546  for j in range(size):
547    print (":extrafuns ((" + board_field(i, j) + " BitVec[1]))")
548
549#generate additional variables for shifters
550if encoding == SHIFTER_ENCODING:
551  varlist = []
552  assert is_power_of_2 (size)
553  if mode == QUEENS_MODE or mode == QUEENS_MODE_NP1 or \
554     mode == QUEENS_MODE_GTN:
555    #generate variables for rows and cols
556    for i in range(2 * size):
557      var = "v" + str(shiftvarscounter)
558      print (":extrafuns ((" + var + " BitVec[" + str(logsize) + "]))")
559      shiftvarscounter += 1
560      varlist.append(var)
561    shiftvarslistmap[str(logsize)] = varlist
562
563    for i in range (2, size + 1):
564      istring = str(i)
565      if shiftvarslistmap.has_key (istring):
566        varlist = shiftvarslistmap[istring]
567      else:
568        varlist = []
569      if i == size:
570        limit = 2
571      else:
572        limit = 4
573      for j in range(limit):
574        var = "v" + str(shiftvarscounter)
575        print (":extrafuns ((" + var + " BitVec[" + istring + "]))")
576        shiftvarscounter += 1
577        varlist.append(var)
578      shiftvarslistmap[istring] = varlist
579
580    if mode == QUEENS_MODE_NP1:
581      log2sizesqr = log2 (sizesqr)
582      if shiftvarslistmap.has_key (str(log2sizesqr)):
583        varlist = shiftvarslistmap[str(log2sizesqr)]
584      else:
585        varlist = []
586      for i in range(size + 1):
587        var = "v" + str(shiftvarscounter)
588        print (":extrafuns ((" + var + " BitVec[" + str(log2sizesqr) + "]))")
589        shiftvarscounter += 1
590        varlist.append(var)
591      shiftvarslistmap[str(log2sizesqr)] = varlist
592    elif mode == QUEENS_MODE_GTN:
593      if shiftvarslistmap.has_key ("1"):
594        varlist = shiftvarslistmap["1"]
595      else:
596        varlist = []
597      var = "v" + str(shiftvarscounter)
598      print (":extrafuns ((" + var + " BitVec[1]))")
599      shiftvarscounter += 1
600      varlist.append(var)
601      shiftvarslistmap["1"] = varlist
602
603      if shiftvarslistmap.has_key (str(sizesqr)):
604        varlist = shiftvarslistmap[str(sizesqr)]
605      else:
606        varlist = []
607      for i in range(1, sizesqr - size - 1):
608        var = "v" + str(shiftvarscounter)
609        print (":extrafuns ((" + var + " BitVec[" + str(sizesqr) + "]))")
610        shiftvarscounter += 1
611        varlist.append(var)
612      shiftvarslistmap[str(sizesqr)] = varlist
613  else:
614    assert mode == NO_THREE_IN_LINE_MODE or \
615           mode == NO_THREE_IN_LINE_MODE_2NP1 or \
616           mode == NO_THREE_IN_LINE_MODE_GT2N
617    #generate variables for rows and cols
618    for i in range(4 * size):
619      var = "v" + str(shiftvarscounter)
620      print (":extrafuns ((" + var + " BitVec[" + str(logsize) + "]))")
621      shiftvarscounter += 1
622      varlist.append(var)
623    shiftvarslistmap[str(logsize)] = varlist
624
625    for i in range (3, size + 1):
626      istring = str(i)
627      if shiftvarslistmap.has_key (istring):
628        varlist = shiftvarslistmap[istring]
629      else:
630        varlist = []
631      if i == size:
632        limit = 4
633      else:
634        limit = 8
635      for j in range(limit):
636        var = "v" + str(shiftvarscounter)
637        print (":extrafuns ((" + var + " BitVec[" + istring + "]))")
638        shiftvarscounter += 1
639        varlist.append(var)
640      shiftvarslistmap[istring] = varlist
641
642    if mode == NO_THREE_IN_LINE_MODE_2NP1:
643      log2sizesqr = log2 (sizesqr)
644      if shiftvarslistmap.has_key (str(log2sizesqr)):
645        varlist = shiftvarslistmap[str(log2sizesqr)]
646      else:
647        varlist = []
648      for i in range(2 * size + 1):
649        var = "v" + str(shiftvarscounter)
650        print (":extrafuns ((" + var + " BitVec[" + str(log2sizesqr) + "]))")
651        shiftvarscounter += 1
652        varlist.append(var)
653      shiftvarslistmap[str(log2sizesqr)] = varlist
654    elif mode == NO_THREE_IN_LINE_MODE_GT2N:
655      if shiftvarslistmap.has_key ("1"):
656        varlist = shiftvarslistmap["1"]
657      else:
658        varlist = []
659      var = "v" + str(shiftvarscounter)
660      print (":extrafuns ((" + var + " BitVec[1]))")
661      shiftvarscounter += 1
662      varlist.append(var)
663      shiftvarslistmap["1"] = varlist
664
665      if shiftvarslistmap.has_key (str(sizesqr)):
666        varlist = shiftvarslistmap[str(sizesqr)]
667      else:
668        varlist = []
669      for i in range(1, sizesqr - 2 * size - 1):
670        var = "v" + str(shiftvarscounter)
671        print (":extrafuns ((" + var + " BitVec[" + str(sizesqr) + "]))")
672        shiftvarscounter += 1
673        varlist.append(var)
674      shiftvarslistmap[str(sizesqr)] = varlist
675
676
677print (":formula")
678
679#generate lookup table
680if encoding == LOOKUP_ENCODING:
681  last = "lookup"
682  for i in range(2):
683    for j in range(2):
684      for k in range(2):
685        for l in range(2):
686          for m in range(2):
687            for n in range(2):
688              for o in range(2):
689                for p in range(2):
690                  index = str(i) + str(j) + str(k) + str(l) + str(m) + \
691                          str(n) + str(o) + str(p)
692                  sum = 0
693                  for bit in index:
694                    if bit == '1':
695                      sum += 1
696                  print ("(let (?e" + str(id) + " (store " + last + " bv" + \
697                         str(int(index, 2)) + "[8]" + " bv" + str(sum) + \
698                         "[4]))")
699                  last = "?e" + str(id)
700                  id += 1
701  lookup = last
702
703# generate row constraints
704for i in range(size):
705  list = []
706  for j in range(size):
707    list.append(board_field(i, j))
708  if encoding == ITE_ENCODING:
709    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
710       mode == NO_THREE_IN_LINE_MODE_GT2N:
711      ite_encode_eq (list, 2);
712    else:
713      ite_encode_eq (list, 1);
714  elif encoding == SHIFTER_ENCODING:
715    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
716       mode == NO_THREE_IN_LINE_MODE_GT2N:
717      shift_encode_eq_2 (list, shiftvarslistmap[str(logsize)]);
718    else:
719      shift_encode_eq_1 (list, shiftvarslistmap[str(logsize)]);
720  else:
721    if encoding == SEQ_ADDER_ENCODING:
722      last, bw_adder = add_seq (list, num_bits_size - 1)
723    elif encoding == LOOKUP_ENCODING:
724      last, bw_adder = add_lookup_8_4 (list)
725    else:
726      assert encoding == PAR_ADDER_ENCODING
727      last, bw_adder = add_par (list, 1)
728    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
729       mode == NO_THREE_IN_LINE_MODE_GT2N:
730      print ("(flet ($e" + str(id) + " (= " + last + " bv2[" + \
731             str(bw_adder) + "]))")
732    else:
733      print ("(flet ($e" + str(id) + " (= " + last + " bv1[" + \
734             str(bw_adder) + "]))")
735  constraints.append ("$e" + str(id))
736  id += 1
737
738# generate col constraints
739for i in range(size):
740  list = []
741  for j in range(size):
742    list.append(board_field(j, i))
743  if encoding == ITE_ENCODING:
744    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
745       mode == NO_THREE_IN_LINE_MODE_GT2N:
746      ite_encode_eq (list, 2)
747    else:
748      ite_encode_eq (list, 1)
749  elif encoding == SHIFTER_ENCODING:
750    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
751       mode == NO_THREE_IN_LINE_MODE_GT2N:
752      shift_encode_eq_2 (list, shiftvarslistmap[str(logsize)]);
753    else:
754      shift_encode_eq_1 (list, shiftvarslistmap[str(logsize)]);
755  else:
756    if encoding == SEQ_ADDER_ENCODING:
757      last, bw_adder = add_seq (list, num_bits_size - 1)
758    elif encoding == LOOKUP_ENCODING:
759      last, bw_adder = add_lookup_8_4 (list)
760    else:
761      assert encoding == PAR_ADDER_ENCODING
762      last, bw_adder = add_par (list, 1)
763    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
764       mode == NO_THREE_IN_LINE_MODE_GT2N:
765      print ("(flet ($e" + str(id) + " (= " + last + " bv2[" + \
766             str(bw_adder) + "]))")
767    else:
768      print ("(flet ($e" + str(id) + " (= " + last + " bv1[" + \
769             str(bw_adder) + "]))")
770  constraints.append ("$e" + str(id))
771  id += 1
772
773#generate diagonal constraints
774for i in range(1, size):
775  list = []
776  list.append (board_field(i, 0))
777  row = i - 1
778  col = 1
779  assert row >= 0 and col < size
780  while row >= 0 and col < size:
781    list.append(board_field(row, col))
782    row -= 1
783    col += 1
784  if (mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
785      mode == NO_THREE_IN_LINE_MODE_GT2N) and len(list) < 3:
786    continue
787  if encoding == ITE_ENCODING:
788    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
789       mode == NO_THREE_IN_LINE_MODE_GT2N:
790      ite_encode_lt (list, 3)
791    else:
792      ite_encode_lt (list, 2)
793  elif encoding == SHIFTER_ENCODING:
794    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
795       mode == NO_THREE_IN_LINE_MODE_GT2N:
796      shift_encode_le_2 (list, shiftvarslistmap[str(len(list))])
797    else:
798      shift_encode_le_1 (list, shiftvarslistmap[str(len(list))])
799  else:
800    if encoding == SEQ_ADDER_ENCODING:
801      last, bw_adder = add_seq (list, num_bits_size - 1)
802    elif encoding == LOOKUP_ENCODING:
803      last, bw_adder = add_lookup_8_4 (list)
804    else:
805      assert encoding == PAR_ADDER_ENCODING
806      last, bw_adder = add_par (list, 1)
807    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
808       mode == NO_THREE_IN_LINE_MODE_GT2N:
809      print ("(flet ($e" + str(id) + " (bvult " + last + " bv3[" + \
810             str(bw_adder) + "]))")
811    else:
812      print ("(flet ($e" + str(id) + " (bvule " + last + " bv1[" + \
813             str(bw_adder) + "]))")
814  constraints.append ("$e" + str(id))
815  id += 1
816
817for i in range(1, size - 1):
818  list = []
819  list.append(board_field(size - 1, i))
820  row = size - 1 - 1
821  col = i + 1
822  assert row >= 0 and col < size
823  while row >= 0 and col < size:
824    list.append(board_field(row, col))
825    row -= 1
826    col += 1
827  if (mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
828      mode == NO_THREE_IN_LINE_MODE_GT2N) and len(list) < 3:
829    continue
830  if encoding == ITE_ENCODING:
831    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
832       mode == NO_THREE_IN_LINE_MODE_GT2N:
833      ite_encode_lt (list, 3)
834    else:
835      ite_encode_lt (list, 2)
836  elif encoding == SHIFTER_ENCODING:
837    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
838       mode == NO_THREE_IN_LINE_MODE_GT2N:
839      shift_encode_le_2 (list, shiftvarslistmap[str(len(list))])
840    else:
841      shift_encode_le_1 (list, shiftvarslistmap[str(len(list))])
842  else:
843    if encoding == SEQ_ADDER_ENCODING:
844      last, bw_adder = add_seq (list, num_bits_size - 1)
845    elif encoding == LOOKUP_ENCODING:
846      last, bw_adder = add_lookup_8_4 (list)
847    else:
848      assert encoding == PAR_ADDER_ENCODING
849      last, bw_adder = add_par (list, 1)
850    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
851       mode == NO_THREE_IN_LINE_MODE_GT2N:
852      print ("(flet ($e" + str(id) + " (bvult " + last + " bv3[" + \
853             str(bw_adder) + "]))")
854    else:
855      print ("(flet ($e" + str(id) + " (bvule " + last + " bv1[" + \
856             str(bw_adder) + "]))")
857  constraints.append ("$e" + str(id))
858  id += 1
859
860for i in range(1, size):
861  list = []
862  list.append (board_field(i, size - 1))
863  row = i - 1
864  col = size - 1 - 1
865  assert row >= 0 and col >= 0
866  while row >= 0 and col >= 0:
867    list.append (board_field(row, col))
868    row -= 1
869    col -= 1
870  if (mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
871      mode == NO_THREE_IN_LINE_MODE_GT2N) and len(list) < 3:
872    continue
873  if encoding == ITE_ENCODING:
874    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
875       mode == NO_THREE_IN_LINE_MODE_GT2N:
876      ite_encode_lt (list, 3)
877    else:
878      ite_encode_lt (list, 2)
879  elif encoding == SHIFTER_ENCODING:
880    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
881       mode == NO_THREE_IN_LINE_MODE_GT2N:
882      shift_encode_le_2 (list, shiftvarslistmap[str(len(list))])
883    else:
884      shift_encode_le_1 (list, shiftvarslistmap[str(len(list))])
885  else:
886    if encoding == SEQ_ADDER_ENCODING:
887      last, bw_adder = add_seq (list, num_bits_size - 1)
888    elif encoding == LOOKUP_ENCODING:
889      last, bw_adder = add_lookup_8_4 (list)
890    else:
891      assert encoding == PAR_ADDER_ENCODING
892      last, bw_adder = add_par (list, 1)
893    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
894       mode == NO_THREE_IN_LINE_MODE_GT2N:
895      print ("(flet ($e" + str(id) + " (bvult " + last + " bv3[" + \
896             str(bw_adder) + "]))")
897    else:
898      print ("(flet ($e" + str(id) + " (bvule " + last + " bv1[" + \
899             str(bw_adder) + "]))")
900  constraints.append ("$e" + str(id))
901  id += 1
902
903for i in range(1, size - 1):
904  list = []
905  list.append (board_field(size - 1, size - 1 - i))
906  row = size - 1 - 1
907  col = size - 1 - i - 1
908  assert row >= 0 and col >= 0
909  while row >= 0 and col >= 0:
910    list.append (board_field(row, col))
911    row -= 1
912    col -= 1
913  if (mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
914      mode == NO_THREE_IN_LINE_MODE_GT2N) and len(list) < 3:
915    continue
916  if encoding == ITE_ENCODING:
917    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
918       mode == NO_THREE_IN_LINE_MODE_GT2N:
919      ite_encode_lt (list, 3)
920    else:
921      ite_encode_lt (list, 2)
922  elif encoding == SHIFTER_ENCODING:
923    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
924       mode == NO_THREE_IN_LINE_MODE_GT2N:
925      shift_encode_le_2 (list, shiftvarslistmap[str(len(list))])
926    else:
927      shift_encode_le_1 (list, shiftvarslistmap[str(len(list))])
928  else:
929    if encoding == SEQ_ADDER_ENCODING:
930      last, bw_adder = add_seq (list, num_bits_size - 1)
931    elif encoding == LOOKUP_ENCODING:
932      last, bw_adder = add_lookup_8_4 (list)
933    else:
934      assert encoding == PAR_ADDER_ENCODING
935      last, bw_adder = add_par (list, 1)
936    if mode == NO_THREE_IN_LINE_MODE or mode == NO_THREE_IN_LINE_MODE_2NP1 or \
937       mode == NO_THREE_IN_LINE_MODE_GT2N:
938      print ("(flet ($e" + str(id) + " (bvult " + last + " bv3[" + \
939             str(bw_adder) + "]))")
940    else:
941      print ("(flet ($e" + str(id) + " (bvule " + last + " bv1[" + \
942             str(bw_adder) + "]))")
943  constraints.append ("$e" + str(id))
944  id += 1
945
946# generate additional constraints
947if mode == QUEENS_MODE_NP1 or mode == QUEENS_MODE_GTN or \
948   mode ==  NO_THREE_IN_LINE_MODE_2NP1 or mode == NO_THREE_IN_LINE_MODE_GT2N:
949  list = []
950  for i in range(size):
951    for j in range(size):
952      list.append (board_field(i, j))
953  if encoding == ITE_ENCODING:
954    if mode == QUEENS_MODE_NP1:
955      ite_encode_eq (list, size + 1)
956    elif mode == QUEENS_MODE_GTN:
957      ite_encode_ge (list, size + 1)
958    elif mode == NO_THREE_IN_LINE_MODE_2NP1:
959      ite_encode_eq (list, 2 * size + 1)
960    else:
961      ite_encode_ge (list, 2 * size + 1)
962      assert mode == NO_THREE_IN_LINE_MODE_GT2N
963  elif encoding == SHIFTER_ENCODING:
964    if mode == QUEENS_MODE_NP1:
965      shift_encode_eq_k (list, shiftvarslistmap[str(log2(sizesqr))], size + 1)
966    elif mode == QUEENS_MODE_GTN:
967      shift_encode_gt_k (list, shiftvarslistmap[str(sizesqr)], \
968                         shiftvarslistmap["1"], size)
969    elif mode == NO_THREE_IN_LINE_MODE_2NP1:
970      shift_encode_eq_k (list, shiftvarslistmap[str(log2(sizesqr))], \
971                         2 *size + 1)
972    else:
973      assert mode == NO_THREE_IN_LINE_MODE_GT2N
974      shift_encode_gt_k (list, shiftvarslistmap[str(sizesqr)], \
975                         shiftvarslistmap["1"], 2 * size)
976  else:
977    if encoding == SEQ_ADDER_ENCODING:
978      last, bw_adder = add_seq (list, num_bits_fields - 1)
979    elif encoding == LOOKUP_ENCODING:
980      last, bw_adder = add_lookup_8_4 (list)
981    else:
982      assert encoding == PAR_ADDER_ENCODING
983      last, bw_adder = add_par (list, 1)
984    if mode == QUEENS_MODE_NP1:
985      print ("(flet ($e" + str(id) + " (= " + last + " bv" + str(size + 1) + \
986              "[" + str(bw_adder) + "]))")
987    elif mode == QUEENS_MODE_GTN:
988      print ("(flet ($e" + str(id) + " (bvugt " + last + " bv" + str(size) + \
989              "[" + str(bw_adder) + "]))")
990    elif mode == NO_THREE_IN_LINE_MODE_2NP1:
991      print ("(flet ($e" + str(id) + " (= " + last + " bv" + \
992             str(2 * size + 1) + "[" + str(bw_adder) + "]))")
993    else:
994      assert mode == NO_THREE_IN_LINE_MODE_GT2N
995      print ("(flet ($e" + str(id) + " (bvugt " + last + " bv" + \
996             str(2 * size) + "[" + str(bw_adder) + "]))")
997  constraints.append ("$e" + str(id))
998  id += 1
999
1000# combine all constraints by AND
1001assert len(constraints) >= 2
1002last = constraints[0]
1003for i in range(1, len(constraints)):
1004  print ("(flet ($e" + str(id) + " (and " + last + " " + constraints[i] + "))")
1005  last = "$e" + str(id)
1006  id += 1
1007print (last)
1008pars = ""
1009for i in range(id):
1010  pars = pars + ")"
1011print (pars)
1012
1013if encoding == SHIFTER_ENCODING:
1014  assert shiftvarslistmap != None
1015  for list in shiftvarslistmap.values():
1016    assert len(list) == 0
1017