ikpx.py 39.1 KB
Newer Older
Adam P. Goucher's avatar
Adam P. Goucher committed
1

Adam P. Goucher's avatar
Adam P. Goucher committed
2
import multiprocessing
Adam P. Goucher's avatar
Adam P. Goucher committed
3
import random
Adam P. Goucher's avatar
Stuff  
Adam P. Goucher committed
4
import os
Adam P. Goucher's avatar
Adam P. Goucher committed
5
import argparse
6
import signal
Adam P. Goucher's avatar
Adam P. Goucher committed
7 8 9
import cPickle
import gzip
import time
10

Adam P. Goucher's avatar
Adam P. Goucher committed
11
from grills import *
12
from parserle import rle2bin
Adam P. Goucher's avatar
Adam P. Goucher committed
13
from velocities import parse_velocity, partial_derivatives
Adam P. Goucher's avatar
Adam P. Goucher committed
14
from sys import stderr, stdout
Adam P. Goucher's avatar
Adam P. Goucher committed
15
from collections import Counter
Adam P. Goucher's avatar
Adam P. Goucher committed
16

17 18 19 20 21 22
import subprocess

def run_command(cmd):

    proc = subprocess.Popen(cmd, shell=True, stdin=subprocess.PIPE)
    return proc
Adam P. Goucher's avatar
Adam P. Goucher committed
23

Adam P. Goucher's avatar
Adam P. Goucher committed
24 25 26
def calculate_padding(ddt, ddx, ddy):
    '''
    Finds the extent of the neighbourhood in either the u or v direction.
Adam P. Goucher's avatar
Adam P. Goucher committed
27 28 29
    This is used to calculate the length of tuples, and also to determine
    the number of blank columns to include on the left and right sides of
    the problem.
Adam P. Goucher's avatar
Adam P. Goucher committed
30 31 32 33 34
    '''
    l = abs(ddx) + abs(ddy)
    return l + max(l, abs(ddt))


Adam P. Goucher's avatar
Adam P. Goucher committed
35 36
class PartialExtender(basegrill):

Adam P. Goucher's avatar
Adam P. Goucher committed
37
    def __init__(self, W, K, initial_rows, params):
Adam P. Goucher's avatar
Adam P. Goucher committed
38
        super(PartialExtender, self).__init__()
Adam P. Goucher's avatar
Adam P. Goucher committed
39 40 41 42 43 44 45
        '''
        This constructor converts the problem (a rectangular grid of
        coordinates in logical (u,v)-space) into a set of (t, x, y) triples
        in physical spacetime, which are then fed to the basegrill. That is
        to say, this abstracts away the lattice quotient so that we can
        re-use the same code from GRILLS.
        '''
Adam P. Goucher's avatar
Adam P. Goucher committed
46

Adam P. Goucher's avatar
Adam P. Goucher committed
47
        # Safe amount of horizontal padding:
Adam P. Goucher's avatar
Adam P. Goucher committed
48
        HPADDING = calculate_padding(params['dudt'], params['dudx'], params['dudy'])
Adam P. Goucher's avatar
Adam P. Goucher committed
49

Adam P. Goucher's avatar
Adam P. Goucher committed
50 51
        self.full_width = W + 2 * HPADDING
        self.full_height = len(initial_rows) + 1 + K
Adam P. Goucher's avatar
Stuff  
Adam P. Goucher committed
52
        self.important_variables = set([])
Adam P. Goucher's avatar
Adam P. Goucher committed
53
        self.bottom_variables = set([])
Adam P. Goucher's avatar
Adam P. Goucher committed
54 55
        self.initial_rows = initial_rows

Adam P. Goucher's avatar
Adam P. Goucher committed
56 57 58 59 60 61
        p = params['p']
        a = params['a']
        dvdy = params['dvdy']
        dudy = params['dudy']
        dvdt = params['dvdt']

Adam P. Goucher's avatar
Adam P. Goucher committed
62
        self.reverse = params['reverse'] if ('reverse' in params) else False
Adam P. Goucher's avatar
Adam P. Goucher committed
63

Adam P. Goucher's avatar
Adam P. Goucher committed
64 65 66 67 68 69 70 71 72 73
        for v in xrange(self.full_height):
            for u in xrange(self.full_width):
                if (u < HPADDING) or (u >= self.full_width - HPADDING):
                    state = DEAD_VARIABLE_STATE
                elif (v < len(initial_rows)):
                    state = 1 << ((initial_rows[v] >> (u - HPADDING)) & 1)
                else:
                    state = UNKNOWN_VARIABLE_STATE

                variable = self.apply_state_to_variable(state)
Adam P. Goucher's avatar
Adam P. Goucher committed
74 75

                for t in xrange(p + 1):
Adam P. Goucher's avatar
Adam P. Goucher committed
76
                    ev = (-v) if self.reverse else v
Adam P. Goucher's avatar
Adam P. Goucher committed
77 78
                    xp = dvdy * u - dudy * ev - a * t
                    yq = ev - t * dvdt
Adam P. Goucher's avatar
Adam P. Goucher committed
79 80 81 82 83 84 85 86
                    if (xp % p != 0):
                        continue
                    if (yq % dvdy != 0):
                        continue
                    x = xp // p
                    y = yq // dvdy
                    self.relate(variable, (t, x, y))

Adam P. Goucher's avatar
Adam P. Goucher committed
87
                if (state == UNKNOWN_VARIABLE_STATE) and (v == len(initial_rows)):
Adam P. Goucher's avatar
Stuff  
Adam P. Goucher committed
88
                    self.important_variables.add(variable)
Adam P. Goucher's avatar
Adam P. Goucher committed
89 90 91 92
                if (v >= (self.full_height - len(initial_rows))):
                    self.bottom_variables.add(variable)

    def sol2rows(self, sol):
Adam P. Goucher's avatar
Adam P. Goucher committed
93 94 95 96
        '''
        Converts an iglucose solution string into a tuple of rows represented
        as unsigned integers.
        '''
Adam P. Goucher's avatar
Adam P. Goucher committed
97 98 99 100 101 102 103 104 105 106
        positives = {}
        for s in sol.split():
            try:
                w = int(s)
                positives[abs(w)] = (1 if (w > 0) else 0)
            except ValueError:
                continue
        rows = [sum([positives[(x*self.full_width)+i+1] << i for i in xrange(self.full_width)]) for x in xrange(self.full_height)]
        return tuple(rows)

Adam P. Goucher's avatar
Adam P. Goucher committed
107
    def exhaust(self, name, prefix, outqueue, timeout=600, skip_complete=False):
Adam P. Goucher's avatar
Adam P. Goucher committed
108 109 110 111 112 113 114
        '''
        Find all of the possibilities for the next row after the ones
        provided in the problem. Because iglucose is known to have
        wildly varying times, we cut this short if it exceeds the timeout,
        so it is not guaranteed to be exhaustive unless the timeout exceeds
        the maximum CPU time used by any iglucose instance.
        '''
Adam P. Goucher's avatar
Stuff  
Adam P. Goucher committed
115 116 117 118 119 120 121 122 123 124 125 126

        sol_fifoname = prefix + '.sol'
        cnf_fifoname = prefix + '.icnf'

        if os.path.exists(sol_fifoname):
            os.unlink(sol_fifoname)
        if os.path.exists(cnf_fifoname):
            os.unlink(cnf_fifoname)

        os.mkfifo(sol_fifoname)
        os.mkfifo(cnf_fifoname)

127 128
        # Track whether the solver is still running:
        running = True
Adam P. Goucher's avatar
Adam P. Goucher committed
129

Adam P. Goucher's avatar
Adam P. Goucher committed
130 131
        satisfied = False

132
        cnf_fifo = open(cnf_fifoname, 'w+')
Adam P. Goucher's avatar
Adam P. Goucher committed
133
        run_iglucose(("-cpu-lim=%d" % int(timeout)), cnf_fifoname, sol_fifoname);
Adam P. Goucher's avatar
Adam P. Goucher committed
134
        sol_fifo = open(sol_fifoname, 'r')
Adam P. Goucher's avatar
Stuff  
Adam P. Goucher committed
135

136 137 138
        try:
            cnf_fifo.write('p inccnf\n')
            self.write_dimacs(cnf_fifo, write_header=False)
139

140 141
            # Look for complete solutions:
            if skip_complete:
142
                stages_completed = 1
Adam P. Goucher's avatar
Stuff  
Adam P. Goucher committed
143
            else:
144 145 146 147 148 149 150 151
                stages_completed = 0
                cnf_fifo.write('a %s 0\n' % (' '.join([str(-x) for x in self.bottom_variables])))
                cnf_fifo.flush()
                sol = sol_fifo.readline()

                if (sol[:3] == 'SAT'):
                    # Completion found:
                    outqueue.put((name, self.sol2rows(sol)))
Adam P. Goucher's avatar
Adam P. Goucher committed
152
                    satisfied = True
153 154 155 156 157 158 159 160 161
                elif (sol[:5] == 'INDET'):
                    running = False

            # Try to extend the partial:
            while running:
                cnf_fifo.write('a 0\n')
                cnf_fifo.flush()
                sol = sol_fifo.readline()
                if (sol[:3] == 'SAT'):
Adam P. Goucher's avatar
Adam P. Goucher committed
162
                    satisfied = True
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185
                    stages_completed = 1
                    anticlause = []
                    next_term = 0
                    v0 = min(list(self.important_variables))
                    for s in sol.split():
                        try:
                            w = int(s)
                        except ValueError:
                            continue
                        if abs(w) in self.important_variables:
                            anticlause.append(-w)
                            if (w > 0):
                                next_term |= (1 << (w - v0))
                    anticlause = ' '.join([str(a) for a in anticlause if (a != 0)])
                    cnf_fifo.write('%s 0\n' % anticlause)
                    outqueue.put((name, self.sol2rows(sol)))
                elif (sol[:5] == 'INDET'):
                    running = False
                else:
                    stages_completed = 2
                    break

        finally:
Adam P. Goucher's avatar
Stuff  
Adam P. Goucher committed
186

187 188 189 190 191
            if running:
                # Kill iglucose by writing rubbish into the pipe:
                cnf_fifo.write('error\n')
                cnf_fifo.flush()
                stages_completed = 2
192

193 194 195 196 197
            # Close and delete the FIFOs:
            cnf_fifo.close()
            sol_fifo.close()
            os.unlink(sol_fifoname)
            os.unlink(cnf_fifoname)
Adam P. Goucher's avatar
Adam P. Goucher committed
198

Adam P. Goucher's avatar
Adam P. Goucher committed
199
        return (stages_completed, satisfied)
200 201


Adam P. Goucher's avatar
Adam P. Goucher committed
202
def canon6(rows):
Adam P. Goucher's avatar
Adam P. Goucher committed
203 204 205 206 207 208 209
    '''
    Takes a tuple of rows and returns a canonised version (divided by
    the highest power of 2 which divides the gcd of the rows) together
    with the number of columns necessary to store the tuple. The latter
    is used as a heuristic for deciding which branches of the search
    tree are most auspicious.
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
210 211 212 213 214 215 216 217

    x = reduce((lambda a, b : a | b), rows, 0)
    while ((x > 0) and ((x & 1) == 0)):
        rows = tuple([(r >> 1) for r in rows])
        x = reduce((lambda a, b : a | b), rows, 0)
    weight = (0 if (x == 0) else (len(bin(x)) - 2))
    return (rows, weight)

Adam P. Goucher's avatar
Adam P. Goucher committed
218
def splice(x, y, l):
Adam P. Goucher's avatar
Adam P. Goucher committed
219 220 221 222 223 224 225
    '''
    Create a new tuple from x and y by overlapping them by l elements.
    This function can left- or right-shift x and y independently to
    ensure they are compatibly normalised. This can be used iteratively
    to reconstruct a long sequence by splicing together short canonised
    sequences.
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
226 227 228

    xx = reduce((lambda a, b : a | b), x[-l:], 0)
    yy = reduce((lambda a, b : a | b), y[:l], 0)
Adam P. Goucher's avatar
Adam P. Goucher committed
229

Adam P. Goucher's avatar
Adam P. Goucher committed
230 231 232 233 234 235 236 237 238 239
    while (xx < yy):
        x = tuple([(r << 1) for r in x])
        xx = reduce((lambda a, b : a | b), x[-l:], 0)
    while (yy < xx):
        y = tuple([(r << 1) for r in y])
        yy = reduce((lambda a, b : a | b), y[:l], 0)

    return (x[:-l] + y)


Adam P. Goucher's avatar
Adam P. Goucher committed
240
def printint(x):
Adam P. Goucher's avatar
Adam P. Goucher committed
241 242 243 244
    '''
    Print an integer in reversed binary using asterisks for '1's and
    dots for '0's.
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
245
    print(bin(x)[2:][::-1].replace('0', '.').replace('1', '*'))
Adam P. Goucher's avatar
Adam P. Goucher committed
246

Adam P. Goucher's avatar
Adam P. Goucher committed
247

Adam P. Goucher's avatar
Adam P. Goucher committed
248 249 250 251 252
class ikpxtree(object):
    '''
    This represents a search tree. In a regular (front or back) search there
    will be precisely one ikpxtree; in a MITM search there are two.
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
253

Adam P. Goucher's avatar
Adam P. Goucher committed
254 255 256
    def __init__(self, name, worker_queue, i6tuple, search_width, lookahead, jumpahead):

        self.name = name
257
        self.lastmm = 0
Adam P. Goucher's avatar
Adam P. Goucher committed
258 259
        self.i6tuple = i6tuple
        self.f6tuple = tuple([0 for _ in i6tuple])
Adam P. Goucher's avatar
Adam P. Goucher committed
260
        self.preds = {i6tuple: (name, 0, 0)}
Adam P. Goucher's avatar
Adam P. Goucher committed
261 262 263 264 265
        self.bestlength = 0
        self.queue = worker_queue
        self.lookahead = lookahead
        self.jumpahead = jumpahead
        self.search_width = search_width
Adam P. Goucher's avatar
Adam P. Goucher committed
266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290
        self.hist = Counter()

        self.last_backup_saved = 0

    def save_state(self, directory):

        backup_parity = ['odd', 'even'][self.last_backup_saved]
        backup_name = 'backup_%s_%s.pkl.gz' % (self.name, backup_parity)
        backup_path = os.path.join(directory, backup_name)

        print('Saving backup %s' % backup_name)
        stdout.flush()

        fp = gzip.open(backup_path, 'wb')
        cPickle.dump(self.preds, fp, protocol=2)
        fp.close()
        self.last_backup_saved = 1 - self.last_backup_saved

        # Remember where we kept the last backup:
        with open(os.path.join(directory, ('backup_%s_location.txt' % self.name)), 'w') as f:
            f.write('%d\n%s' % (self.last_backup_saved, backup_name))

        print('Saved backup %s' % backup_name)
        stdout.flush()

Adam P. Goucher's avatar
Adam P. Goucher committed
291
    def load_state(self, directory, modus_operandi='append', prompt_user=False):
Adam P. Goucher's avatar
Adam P. Goucher committed
292

Adam P. Goucher's avatar
Adam P. Goucher committed
293 294 295
        bkpath = os.path.join(directory, ('backup_%s_location.txt' % self.name))

        if os.path.exists(bkpath):
Adam P. Goucher's avatar
Adam P. Goucher committed
296
            print('Backup file %s found' % bkpath)
Adam P. Goucher's avatar
Adam P. Goucher committed
297
        else:
Adam P. Goucher's avatar
Adam P. Goucher committed
298
            print('Backup file %s not found' % bkpath)
Adam P. Goucher's avatar
Adam P. Goucher committed
299 300 301 302 303 304 305 306 307
            stdout.flush()
            return

        if prompt_user:
            should_resume = yn2bool(raw_input("Would you like to resume %s search from saved tree? [y] : " % self.name) or 'y')
            if not should_resume:
                return

        with open(bkpath, 'r') as f:
Adam P. Goucher's avatar
Adam P. Goucher committed
308
            lines = [x for x in f]
Adam P. Goucher's avatar
Adam P. Goucher committed
309

Adam P. Goucher's avatar
Adam P. Goucher committed
310 311
        self.last_backup_saved = int(lines[0][0])
        backup_name = lines[1]
312 313
        while (backup_name[-1] == '\n'):
            backup_name = backup_name[:-1]
Adam P. Goucher's avatar
Adam P. Goucher committed
314 315
        backup_path = os.path.join(directory, backup_name)

Adam P. Goucher's avatar
Adam P. Goucher committed
316
        fp = gzip.open(backup_path, 'rb')
Adam P. Goucher's avatar
Adam P. Goucher committed
317 318 319 320 321 322 323
        newdict = cPickle.load(fp)
        fp.close()

        if (modus_operandi == 'append'):
            self.preds.update(newdict)
        else:
            raise ValueError("modus_operandi must be 'append'")
Adam P. Goucher's avatar
Adam P. Goucher committed
324 325

    def traceship(self, y):
Adam P. Goucher's avatar
Adam P. Goucher committed
326 327 328 329
        '''
        Produce the entire genealogy of a tuple and splice it together to
        recover the partial head or tail.
        '''
Adam P. Goucher's avatar
Adam P. Goucher committed
330
        l = len(self.i6tuple)
Adam P. Goucher's avatar
Adam P. Goucher committed
331
        x, _ = canon6(y[:l])
Adam P. Goucher's avatar
Adam P. Goucher committed
332 333
        while (x != self.i6tuple):
            x = self.preds[x][0]
Adam P. Goucher's avatar
Adam P. Goucher committed
334 335
            if isinstance(x, basestring):
                break
Adam P. Goucher's avatar
Adam P. Goucher committed
336 337 338
            y = splice(x, y, l-1)
        return y

339
    def enqueue_work(self, fsegment, min_W=None, narrow=True):
Adam P. Goucher's avatar
Adam P. Goucher committed
340

341
        K = self.lookahead
342 343 344 345
        max_W = self.search_width

        if narrow:
            max_W -= min(self.lastmm, 4)
346

Adam P. Goucher's avatar
Adam P. Goucher committed
347 348 349
        fsegment, w = canon6(fsegment)

        if min_W is None:
350
            min_W = max_W
Adam P. Goucher's avatar
Adam P. Goucher committed
351

Adam P. Goucher's avatar
Adam P. Goucher committed
352
        # Low-memory mode:
Adam P. Goucher's avatar
Adam P. Goucher committed
353 354
        if max_W >= min_W:
            self.queue.put((fsegment, w, min_W, max_W, K))
Adam P. Goucher's avatar
Adam P. Goucher committed
355

Adam P. Goucher's avatar
Adam P. Goucher committed
356
    def rundict(self):
Adam P. Goucher's avatar
Adam P. Goucher committed
357 358 359 360

        from collections import Counter
        plengths = Counter()

361
        self.lastmm = 0
Adam P. Goucher's avatar
Adam P. Goucher committed
362
        for (k, v) in self.preds.iteritems():
363
            self.enqueue_work(k, v[2], narrow=False)
Adam P. Goucher's avatar
Adam P. Goucher committed
364 365 366 367
            plengths[v[1]] += 1

        plengths = [x[1] for x in sorted(plengths.items())]
        print('%s partial lengths: %s' % (self.name, plengths))
Adam P. Goucher's avatar
Adam P. Goucher committed
368
        stdout.flush()
Adam P. Goucher's avatar
Adam P. Goucher committed
369

Adam P. Goucher's avatar
Adam P. Goucher committed
370 371 372 373 374
    def adaptive_widen(self):

        self.search_width += 1
        print('Increasing %s search width to %d...' % (self.name, self.search_width))
        stdout.flush()
Adam P. Goucher's avatar
Adam P. Goucher committed
375
        self.rundict()
Adam P. Goucher's avatar
Adam P. Goucher committed
376 377 378
        print('...adaptive widening completed.')
        stdout.flush()

Adam P. Goucher's avatar
Adam P. Goucher committed
379 380 381 382
    def addpred(self, fsegment, isegment, w):
        if fsegment in self.preds:
            return 0
        else:
Adam P. Goucher's avatar
Adam P. Goucher committed
383 384 385 386
            if isegment not in self.preds:
                print('Warning: new initial segment found.')
                stdout.flush()
                self.preds[isegment] = (self.name, 0, 0)
Adam P. Goucher's avatar
Adam P. Goucher committed
387 388 389 390 391
            currlength = self.preds[isegment][1] + 1
            self.preds[fsegment] = (isegment, currlength, w)
            self.hist[currlength] += 1
            return currlength

Adam P. Goucher's avatar
Adam P. Goucher committed
392
    def process_item(self, item, othertree=None, found=set([]), params=None, cmd=None):
Adam P. Goucher's avatar
Adam P. Goucher committed
393 394 395 396 397
        '''
        The main orchestration code performed by the master thread. We keep it
        here instead of in master_function to avoid having duplicated code
        when handling both fronts and backs of spaceships.
        '''
Adam P. Goucher's avatar
Adam P. Goucher committed
398

Adam P. Goucher's avatar
Adam P. Goucher committed
399
        worker_queue = self.queue
Adam P. Goucher's avatar
Adam P. Goucher committed
400

Adam P. Goucher's avatar
Adam P. Goucher committed
401 402
        if isinstance(item, basestring):
            if (item == 'done'):
403
                pass
Adam P. Goucher's avatar
Adam P. Goucher committed
404 405
            elif (item == 'commence'):
                self.rundict()
Adam P. Goucher's avatar
Adam P. Goucher committed
406 407
            elif (item == 'adawide'):
                self.adaptive_widen()
408 409 410
            elif ((len(item) >= 6) and (item[:5] == 'load ')):
                t = rle2bin(item[5:])
                self.engulf_partial(t, othertree=othertree, found=found)
Adam P. Goucher's avatar
Adam P. Goucher committed
411 412
            else:
                raise ValueError("Command '%s' not recognised." % item)
413
            worker_queue.task_done()
Adam P. Goucher's avatar
Adam P. Goucher committed
414
            return
Adam P. Goucher's avatar
Adam P. Goucher committed
415

Adam P. Goucher's avatar
Adam P. Goucher committed
416 417 418 419 420 421 422 423 424 425
        if isinstance(item[0], basestring):
            if (item[0] == 'done'):
                _, segment, attained_W = item
                oldpred = self.preds[segment]
                self.preds[segment] = (oldpred[0], oldpred[1], attained_W + 1)
                worker_queue.task_done()
            else:
                raise ValueError("Command '%s' not recognised." % item[0])
            return

Adam P. Goucher's avatar
Adam P. Goucher committed
426
        if hasattr(item[0], '__iter__'):
Adam P. Goucher's avatar
Adam P. Goucher committed
427 428 429
            # Worker was lazy and rejected the job:
            worker_queue.put(item)
            worker_queue.task_done()
Adam P. Goucher's avatar
Adam P. Goucher committed
430 431
            return

Adam P. Goucher's avatar
Adam P. Goucher committed
432
        self.engulf_partial(item, othertree=othertree, found=found, jumpahead=self.jumpahead, params=params, cmd=cmd)
Adam P. Goucher's avatar
Adam P. Goucher committed
433 434


Adam P. Goucher's avatar
Adam P. Goucher committed
435
    def engulf_partial(self, item, othertree=None, found=set([]), jumpahead=None, params=None, cmd=None):
Adam P. Goucher's avatar
Adam P. Goucher committed
436 437 438 439 440 441 442 443
        '''
        Take a partial (sequence of integers encoding rows in binary) and
        digest it, adding new edges to the search tree and enqueueing work
        as appropriate.
        '''

        worker_queue = self.queue

Adam P. Goucher's avatar
Adam P. Goucher committed
444
        completed = ('extending %ss' % self.name) if (item[-len(self.f6tuple):] == self.f6tuple) else None
Adam P. Goucher's avatar
Adam P. Goucher committed
445

Adam P. Goucher's avatar
Adam P. Goucher committed
446
        ts = None
447
        currlength = 0
Adam P. Goucher's avatar
Adam P. Goucher committed
448

Adam P. Goucher's avatar
Adam P. Goucher committed
449 450
        if jumpahead is None:
            jumpahead = len(item) - len(self.i6tuple)
Adam P. Goucher's avatar
Adam P. Goucher committed
451 452
        else:
            jumpahead = min(jumpahead, len(item) - len(self.i6tuple))
Adam P. Goucher's avatar
Adam P. Goucher committed
453 454

        for j in xrange(jumpahead):
Adam P. Goucher's avatar
Adam P. Goucher committed
455

Adam P. Goucher's avatar
Adam P. Goucher committed
456 457 458
            tuple7 = item[j:len(self.i6tuple)+j+1]
            isegment, _ = canon6(tuple7[:-1])
            fsegment, w = canon6(tuple7[1:])
Adam P. Goucher's avatar
Adam P. Goucher committed
459

Adam P. Goucher's avatar
Adam P. Goucher committed
460 461 462
            currlength = self.addpred(fsegment, isegment, w)

            if (currlength > 0):
463

Adam P. Goucher's avatar
Adam P. Goucher committed
464
                self.enqueue_work(fsegment, w)
465

Adam P. Goucher's avatar
Adam P. Goucher committed
466
                if (len(self.preds) % 100 == 0):
467
                    try:
468 469 470
                        wqs = worker_queue.qsize()
                        queue_size = ' (%s queue size ~= %d)' % (self.name, wqs)
                        self.lastmm = wqs // 1000000
471 472 473 474
                    except NotImplementedError:
                        # Mac OS X
                        queue_size = ''
                    print("%d %s edges traversed%s." % (len(self.preds), self.name, queue_size))
Adam P. Goucher's avatar
Adam P. Goucher committed
475
                    stdout.flush()
Adam P. Goucher's avatar
Adam P. Goucher committed
476

477 478 479 480 481 482 483
                if (cmd is not None) and (self.name == 'head'):
                    tempts = self.traceship(fsegment)
                    tempts, _ = canon6(tempts)
                    rle = trace_to_rle(tempts, params)
                    cmd.stdin.write(rle)
                    cmd.stdin.flush()

Adam P. Goucher's avatar
Adam P. Goucher committed
484 485 486 487 488 489 490 491
                if othertree is not None:
                    # We compare the head against known tails (or vice-versa):
                    if fsegment[::-1] in othertree.preds:
                        hts = self.traceship(fsegment)
                        tts = othertree.traceship(fsegment[::-1])[::-1]
                        ts = splice(hts, tts, len(self.i6tuple))
                        completed = 'meet-in-the-middle approach'

492
        showship = None
Adam P. Goucher's avatar
Adam P. Goucher committed
493

Adam P. Goucher's avatar
Adam P. Goucher committed
494
        if completed is not None:
495
            showship = ('Spaceship completed by %s.' % completed)
496
        elif (currlength > self.bestlength):
Adam P. Goucher's avatar
Adam P. Goucher committed
497
            self.bestlength = currlength
498
            showship = ("Found partial %s of length %d." % (self.name, currlength))
Adam P. Goucher's avatar
Adam P. Goucher committed
499

500 501
        if showship is not None:
            # Produce a trace of the ship or partial:
Adam P. Goucher's avatar
Adam P. Goucher committed
502 503 504 505
            if ts is None:
                ts = self.traceship(item[1:])
            if self.name == 'tail':
                ts = ts[::-1]
506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521
            ts, _ = canon6(ts)

            # Strip trailing and leading zeros:
            while (len(ts) > 1) and (ts[0] == 0):
                ts = ts[1:]
            while (len(ts) > 1) and (ts[-1] == 0):
                ts = ts[:-1]

            # Ensure we haven't displayed this image before:
            if ts not in found:
                found.add(ts)
                print(showship)
                print("As integer list: %s" % repr(ts))
                print("As plaintext:")
                for t in ts:
                    printint(t)
Adam P. Goucher's avatar
Adam P. Goucher committed
522 523 524 525 526
                if params is not None:
                    print("As RLE:\n")
                    try:
                        rle = trace_to_rle(ts, params)
                        print(rle)
527 528 529
                        if cmd is not None:
                            cmd.stdin.write(rle)
                            cmd.stdin.flush()
Adam P. Goucher's avatar
Adam P. Goucher committed
530 531 532
                    except:
                        import traceback
                        traceback.print_exc()
533
                stdout.flush()
Adam P. Goucher's avatar
Adam P. Goucher committed
534 535


Adam P. Goucher's avatar
Adam P. Goucher committed
536
def master_function(master_queue, backup_directory, argdict, params, cmd):
Adam P. Goucher's avatar
Adam P. Goucher committed
537 538 539 540 541
    '''
    The function executed by the master thread. It simply pops items from the
    master_queue, reads the name of the ikpxtree to which they belong ('head'
    or 'tail'), and calls the process_item method.
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
542

543 544 545
    if isinstance(cmd, basestring):
        cmd = run_command(cmd)

Adam P. Goucher's avatar
Adam P. Goucher committed
546 547 548 549 550 551 552 553 554
    if os.path.exists(backup_directory):
        print('Directory %s already exists.' % backup_directory)
    else:
        os.makedirs(backup_directory)
        print('Directory %s created.' % backup_directory)

    # Global function variables:
    trees = {}
    found = set([])
555 556

    fgs = {'is_interrupted': False, 'is_saving': False, 'last_backup_time': time.time(), 'backup_duration': 0.0}
Adam P. Goucher's avatar
Adam P. Goucher committed
557

558
    def raise_keyboard_interrupt(signal, frame):
Adam P. Goucher's avatar
Adam P. Goucher committed
559 560
        print("Master received SIGINT.")
        stdout.flush()
561 562
        fgs['is_interrupted'] = True
        if not fgs['is_saving']:
Adam P. Goucher's avatar
Adam P. Goucher committed
563 564 565
            save_trees()

    def save_trees():
566
        fgs['is_saving'] = True
Adam P. Goucher's avatar
Adam P. Goucher committed
567 568 569 570 571 572

        start_backup_time = time.time()

        for v in trees.itervalues():
            v.save_state(backup_directory)

573 574
        fgs['last_backup_time'] = time.time()
        fgs['backup_duration'] = fgs['last_backup_time'] - start_backup_time
Adam P. Goucher's avatar
Adam P. Goucher committed
575

576
        print('Backup process took %.1f seconds.' % fgs['backup_duration'])
Adam P. Goucher's avatar
Adam P. Goucher committed
577 578
        stdout.flush()

579 580
        if fgs['is_interrupted']:
            fgs['is_saving'] = False
Adam P. Goucher's avatar
Adam P. Goucher committed
581
            raise KeyboardInterrupt
582
        fgs['is_saving'] = False
583 584 585

    signal.signal(signal.SIGINT, raise_keyboard_interrupt)

Adam P. Goucher's avatar
Adam P. Goucher committed
586
    # Create search trees:
Adam P. Goucher's avatar
Adam P. Goucher committed
587 588
    for (name, args) in argdict.iteritems():
        trees[name] = ikpxtree(name, *args)
Adam P. Goucher's avatar
Adam P. Goucher committed
589
        trees[name].load_state(backup_directory)
Adam P. Goucher's avatar
Adam P. Goucher committed
590 591 592 593 594 595 596

    # Determine whether running a regular or MITM search:
    if len(trees) == 2:
        othertrees = {k : [v for (l, v) in trees.iteritems() if (l != k)][0] for k in trees}
    else:
        othertrees = {k : None for k in trees}

Adam P. Goucher's avatar
Adam P. Goucher committed
597 598 599 600
    print("To quit the program, either Ctrl+C or run the command:")
    print("\033[31;1m kill -SIGINT -%d \033[0m" % os.getpgid(0))
    stdout.flush()

Adam P. Goucher's avatar
Adam P. Goucher committed
601
    # Process items from the master queue and delegate work:
602 603 604
    try:
        while True:
            origitem = master_queue.get()
Adam P. Goucher's avatar
Adam P. Goucher committed
605

606 607
            if origitem is None:
                break
608

609
            (name, item) = origitem
Adam P. Goucher's avatar
Adam P. Goucher committed
610
            trees[name].process_item(item, othertree=othertrees[name], found=found, params=params, cmd=cmd)
Adam P. Goucher's avatar
Adam P. Goucher committed
611

612
            if (time.time() - fgs['last_backup_time']) > max(3600, 20 * fgs['backup_duration']):
Adam P. Goucher's avatar
Adam P. Goucher committed
613 614
                save_trees()

615
    except KeyboardInterrupt:
Adam P. Goucher's avatar
Adam P. Goucher committed
616
        print("Master received KeyboardInterrupt.")
617 618
    finally:
        print("Master finished.")
619
        # Prevent threads from deadlocking by self-terminating:
620 621 622 623 624 625
        if cmd is not None:
            print("Waiting for command to finish...")
            cmd.stdin.flush()
            cmd.stdin.close()
            cmd.wait()
            print("...command finished.")
626
        os.kill(os.getpid(), signal.SIGTERM)
Adam P. Goucher's avatar
Adam P. Goucher committed
627

Adam P. Goucher's avatar
Adam P. Goucher committed
628

Adam P. Goucher's avatar
Adam P. Goucher committed
629 630 631 632 633 634 635
def worker_function(name, master_queue, worker_queue, worker_root,
                    params, diligence, timeout, encoding):
    '''
    The function executed by the worker threads. This receives work from
    the master thread, encodes it as a SAT problem, and delegates it down to
    the iglucose solvers (the _real_ workers!).
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
636

637 638 639 640 641
    def raise_keyboard_interrupt(signal, frame):
        raise KeyboardInterrupt

    signal.signal(signal.SIGINT, raise_keyboard_interrupt)

Adam P. Goucher's avatar
Adam P. Goucher committed
642 643 644 645 646 647
    def single_work(rows, w, W, K):
        px = PartialExtender(W, K, rows, params)
        px.enforce_rule(encoding=encoding)
        if px.easy_unsat():
            # The problem has been deemed unsatisfiable by easy deductions
            # so it would be overkill to run a new instance of iglucose:
Adam P. Goucher's avatar
Adam P. Goucher committed
648
            return False
Adam P. Goucher's avatar
Adam P. Goucher committed
649 650 651 652 653 654 655 656 657
        else:
            if px.reverse:
                # Growing things in reverse is difficult, so we don't even
                # attempt completion here:
                stages_completed = 0
            else:
                # The problem may have solutions, so we run iglucose to find
                # all possible completions of the next row (within a time
                # limit to ensure things continue moving quickly):
Adam P. Goucher's avatar
Adam P. Goucher committed
658
                stages_completed, satisfied = px.exhaust(name, worker_root, master_queue, timeout=timeout)
Adam P. Goucher's avatar
Adam P. Goucher committed
659 660 661 662 663

            if (stages_completed == 0):
                # The time limit was reached without a satisfactory
                # conclusion, so we retry without the initial attempt to
                # complete the pattern:
Adam P. Goucher's avatar
Adam P. Goucher committed
664 665 666
                stages_completed, satisfied = px.exhaust(name, worker_root, master_queue, skip_complete=True, timeout=timeout)

            return (satisfied or (stages_completed < 2))
Adam P. Goucher's avatar
Adam P. Goucher committed
667 668

    def multiple_work(fsegment, w, min_W, max_W, K):
Adam P. Goucher's avatar
Adam P. Goucher committed
669

670 671 672
        # No empty work:
        min_W = max(min_W, 2)

Adam P. Goucher's avatar
Adam P. Goucher committed
673 674 675 676 677
        # We enumerate widths backwards so we can eliminate impossible tasks:
        widths = list(xrange(min_W, max_W + 1))[::-1]
        unsats = set([])

        for W in widths:
678 679 680 681 682 683 684 685 686

            if (w == 0):
                # Zero tuple:
                offsets = [0]
            else:
                # Try different offsets:
                offsets = list(xrange(W - w + 1))

            for i in offsets:
Adam P. Goucher's avatar
Adam P. Goucher committed
687 688 689 690 691 692 693 694 695 696
                j = W - w - i

                if ((i+1, j) in unsats) or ((i, j+1) in unsats):
                    satisfied = False
                else:
                    rows = tuple([(r << i) for r in fsegment])
                    satisfied = single_work(rows, w, W, K)

                if not satisfied:
                    unsats.add((i, j))
Adam P. Goucher's avatar
Adam P. Goucher committed
697

Adam P. Goucher's avatar
Adam P. Goucher committed
698 699
        return (fsegment, max_W)

Adam P. Goucher's avatar
Adam P. Goucher committed
700 701 702 703
    def perform_work(item):
        if len(item) == 4:
            # Legacy mode:
            single_work(*item)
Adam P. Goucher's avatar
Adam P. Goucher committed
704
            return None
Adam P. Goucher's avatar
Adam P. Goucher committed
705 706
        if len(item) == 5:
            # Low-memory mode:
Adam P. Goucher's avatar
Adam P. Goucher committed
707
            return multiple_work(*item)
Adam P. Goucher's avatar
Adam P. Goucher committed
708

709 710 711
    try:
        while True:
            item = worker_queue.get()
712

713 714 715
            if item is None:
                # Swallow the sentinel and exit:
                break
716

717 718 719 720
            if isinstance(item, basestring) or (random.random() > (diligence ** (item[1] - 12))):
                # Return the item to the master:
                master_queue.put((name, item))
                continue
Adam P. Goucher's avatar
Adam P. Goucher committed
721

Adam P. Goucher's avatar
Adam P. Goucher committed
722 723 724 725 726
            returned_work = perform_work(item)
            if returned_work is not None:
                master_queue.put((name, ('done',) + returned_work))
            else:
                master_queue.put((name, 'done'))
727 728 729 730 731
    except KeyboardInterrupt:
        print("SIGINT occurred on worker %s" % worker_root)
        stdout.flush()
    finally:
        worker_queue.task_done()
732

Adam P. Goucher's avatar
Adam P. Goucher committed
733

Adam P. Goucher's avatar
Adam P. Goucher committed
734
def telephone_sanitiser_function(direc, worker_queue, njobs, widenings):
735 736 737 738
    '''
    Acts as a middle-manager between the master and workers, as well as
    ensuring that the interprocess communication between them is cleaned
    up correctly.
Adam P. Goucher's avatar
Adam P. Goucher committed
739

740 741
    This thread is also responsible for adaptive widening.
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
742

743 744 745 746 747 748
    def raise_keyboard_interrupt(signal, frame):
        raise KeyboardInterrupt

    signal.signal(signal.SIGINT, raise_keyboard_interrupt)

    try:
Adam P. Goucher's avatar
Adam P. Goucher committed
749 750 751
        # Search at current width:
        worker_queue.put('commence')
        worker_queue.join()
752
        for i in xrange(widenings):
Adam P. Goucher's avatar
Adam P. Goucher committed
753
            # Search at next width:
754
            worker_queue.put('adawide')
Adam P. Goucher's avatar
Adam P. Goucher committed
755
            worker_queue.join()
756 757 758 759 760 761 762 763 764
        print('Cleaning up %d %s worker threads...' % (njobs, direc))
        stdout.flush()
        for _ in xrange(njobs):
            worker_queue.put(None)
        worker_queue.join()
        print('...done.')
    except KeyboardInterrupt:
        print('KeyboardInterrupt triggered in telephone_sanitiser.')
    finally:
765
        worker_queue.cancel_join_thread()
766
        worker_queue.close()
Adam P. Goucher's avatar
Adam P. Goucher committed
767

Adam P. Goucher's avatar
Adam P. Goucher committed
768
def horizontal_line():
Adam P. Goucher's avatar
Adam P. Goucher committed
769 770 771 772
    '''
    Draw a bright green horizontal line of asterisks to stdout, flanked by
    a blank line before and after.
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
773 774
    print('\n\033[32;1m' + ('*'*64) + '\033[0m\n')
    stdout.flush()
Adam P. Goucher's avatar
Adam P. Goucher committed
775

Adam P. Goucher's avatar
Adam P. Goucher committed
776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826
def printrun(outstream, quantity, char):

    if (quantity <= 0):
        return
    elif (quantity == 1):
        tok = char
    else:
        tok = str(quantity) + char

    if len(outstream[-1]) + len(tok) > 70:
        outstream.append(tok)
    else:
        outstream[-1] += tok

def trace_to_rle(ts, params):

    dvdy = params['dvdy']
    dudy = params['dudy']
    dvdt = params['dvdt']
    a = params['a']
    p = params['p']

    gcells = {t : [] for t in xrange(p)}

    cells = [(u, v) for (v, x) in enumerate(ts) for (u, dig) in enumerate(bin(x)[2:][::-1]) if (dig == '1')]

    for (u, v) in cells:
        for t in xrange(p):
            xp = dvdy * u - dudy * v - a * t
            yq = v - t * dvdt
            if (xp % p != 0):
                continue
            if (yq % dvdy != 0):
                continue
            x = xp // p
            y = yq // dvdy
            gcells[t].append((y, x))

    outstream = []

    for g in gcells.values():

        if len(g) == 0:
            continue

        g = sorted(g)
        minx = min([cc[1] for cc in g])
        miny = min([cc[0] for cc in g])
        g = [(y - miny, x - minx) for (y, x) in g]
        maxx = max([cc[1] for cc in g])
        maxy = max([cc[0] for cc in g])
Adam P. Goucher's avatar
Adam P. Goucher committed
827

Adam P. Goucher's avatar
Adam P. Goucher committed
828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854
        outstream.append('x = %d, y = %d' % (maxx + 1, maxy + 1))
        outstream.append('')
        lastx = 0
        lasty = 0
        runlength = 0

        for (y, x) in g:

            if ((y > lasty) or (x > lastx)):
                printrun(outstream, runlength, 'o');
                if (y > lasty):
                    printrun(outstream, y - lasty, "$");
                    lasty = y;
                    lastx = 0;
                if (x > lastx):
                    printrun(outstream, x - lastx, 'b');
                runlength = 0;
            runlength += 1;
            lastx = x + 1;

        printrun(outstream, runlength, 'o');
        outstream[-1] += '!\n'

    return '\n'.join(outstream)

def dict_to_rle(psets, params, homedir, cmd):

855 856 857
    if isinstance(cmd, basestring):
        cmd = run_command(cmd)

Adam P. Goucher's avatar
Adam P. Goucher committed
858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876
    backup_dir = os.path.join(homedir, 'backup')
    if not os.path.exists(backup_dir):
        raise ValueError("Backup directory does not exist.")

    pset = psets['head']

    # Prepare initial work:
    i6tuple, _ = canon6(pset['i'])
    W = pset['w']
    K = pset['k']
    J = pset['j']

    tree = ikpxtree('head', None, i6tuple, W, K, J)
    tree.load_state(backup_dir)

    for k in tree.preds:
        if k != i6tuple:
            ts = tree.traceship(k)
            rle = trace_to_rle(ts, params)
877 878 879 880 881 882 883 884 885
            if cmd is None:
                print(rle)
            else:
                cmd.stdin.write(rle)
                cmd.stdin.flush()

    if cmd is not None:
        cmd.stdin.close()
        cmd.wait()
Adam P. Goucher's avatar
Adam P. Goucher committed
886 887

def do_everything(psets, params, homedir, encoding='split', loadhead=None, cmd=None):
Adam P. Goucher's avatar
Adam P. Goucher committed
888 889 890 891
    '''
    ...apart from reading and interpreting command-line arguments, which is
    accomplished in the function clmain().
    '''
Adam P. Goucher's avatar
Adam P. Goucher committed
892 893 894 895

    if os.path.exists(homedir):
        print('Directory %s already exists.' % homedir)
    else:
Adam P. Goucher's avatar
Adam P. Goucher committed
896
        os.makedirs(homedir)
Adam P. Goucher's avatar
Adam P. Goucher committed
897 898
        print('Directory %s created.' % homedir)

Adam P. Goucher's avatar
Adam P. Goucher committed
899 900
    backup_dir = os.path.join(homedir, 'backup')

Adam P. Goucher's avatar
Adam P. Goucher committed
901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918
    print('Ensuring iglucose is installed and operational:')
    horizontal_line()

    status = runbash(os.path.join(scriptdir, 'scripts', 'iglucose.sh'), '--help')

    print('Exit status: %d' % status)

    if (status != 0):
        raise ValueError('iglucose exited with status %d' % status)
    horizontal_line()

    if (len(psets) == 0):
        raise ValueError("At least one head or tail thread must be specified.")
    else:
        print('Commencing search with the following parameters:')
        for (k, v) in psets.iteritems():
            print("%s search: %s" % (k, repr(v)))
        stdout.flush()
Adam P. Goucher's avatar
Adam P. Goucher committed
919 920

    master_queue = multiprocessing.Queue()
Adam P. Goucher's avatar
Adam P. Goucher committed
921 922
    argdict = {}
    workers = []
Adam P. Goucher's avatar
Adam P. Goucher committed
923
    telephone_sanitisers = []
Adam P. Goucher's avatar
Adam P. Goucher committed
924 925 926 927 928 929

    for (direc, pset) in psets.iteritems():
        new_params = {k : v for (k, v) in params.iteritems()}
        new_params['reverse'] = (direc == 'tail')

        # Prepare initial work:
Adam P. Goucher's avatar
Adam P. Goucher committed
930
        i6tuple, _ = canon6(pset['i'])
Adam P. Goucher's avatar
Adam P. Goucher committed
931 932 933 934
        W = pset['w']
        K = pset['k']
        J = pset['j']
        njobs = pset['p']
Adam P. Goucher's avatar
Adam P. Goucher committed
935

Adam P. Goucher's avatar
Adam P. Goucher committed
936 937 938 939 940
        # i6tuple, iw = canon6(i6tuple)
        # ls = (W - iw) // 2
        # centred_i6tuple = tuple([(r << ls) for r in i6tuple])
        # worker_queue.put((centred_i6tuple, iw, W, K))

Adam P. Goucher's avatar
Adam P. Goucher committed
941
        worker_queue = multiprocessing.JoinableQueue()
Adam P. Goucher's avatar
Adam P. Goucher committed
942

943 944 945
        if (direc == 'head') and (loadhead is not None):
            worker_queue.put('load %s' % loadhead)

Adam P. Goucher's avatar
Adam P. Goucher committed
946 947 948 949
        for _ in xrange(njobs):
            worker_path = os.path.join(homedir, ('worker%d' % len(workers)))
            workers.append(multiprocessing.Process(target = worker_function,
                args = (direc, master_queue, worker_queue, worker_path,
Adam P. Goucher's avatar
Adam P. Goucher committed
950
                        new_params, pset['d'], pset['t'], encoding)))
Adam P. Goucher's avatar
Adam P. Goucher committed
951

Adam P. Goucher's avatar
Adam P. Goucher committed
952 953
        argdict[direc] = (worker_queue, i6tuple, W, K, J)

Adam P. Goucher's avatar
Adam P. Goucher committed
954 955 956
        telephone_sanitisers.append(multiprocessing.Process(target = telephone_sanitiser_function,
                args = (direc, worker_queue, njobs, pset['a'])))

Adam P. Goucher's avatar
Adam P. Goucher committed
957
    master = multiprocessing.Process(target = master_function,
Adam P. Goucher's avatar
Adam P. Goucher committed
958
                args = (master_queue, backup_dir, argdict, params, cmd))
Adam P. Goucher's avatar
Adam P. Goucher committed
959

960 961 962
    # Swallow SIGINT:
    signal.signal(signal.SIGINT, signal.SIG_IGN)

Adam P. Goucher's avatar
Adam P. Goucher committed
963 964
    # Launch the threads:
    master.start()
Adam P. Goucher's avatar
Adam P. Goucher committed
965

Adam P. Goucher's avatar
Adam P. Goucher committed
966 967 968 969 970 971
    for w in workers:
        w.start()
    for t in telephone_sanitisers:
        t.start()
    for t in telephone_sanitisers:
        t.join()
972 973 974 975 976 977 978
    for w in workers:
        w.join()

    print('Cleaning up master thread...')
    stdout.flush()
    master_queue.put(None)
    master.join()
Adam P. Goucher's avatar
Adam P. Goucher committed
979
    master_queue.close()
Adam P. Goucher's avatar
Adam P. Goucher committed
980

981 982 983
    print('...ikpx terminated.')
    stdout.flush()

Adam P. Goucher's avatar
Adam P. Goucher committed
984

Adam P. Goucher's avatar
Adam P. Goucher committed
985 986 987 988
# TIM_COE_PARTIAL = (1410, 2024, 3648, 2384, 3476, 3329)
# ROKICKI_PARTIAL = (77128, 66136, 80510, 79606, 41037, 172229)
# ROKICKI_PARTIAL2 = (5084, 12556, 10565, 11629, 11970, 1170)
# ROKICKI_PARTIAL3 = (458, 390, 181, 28, 72, 336)
Adam P. Goucher's avatar
Adam P. Goucher committed
989 990


991 992 993 994 995
def parse_descriptor(s, tsize, name, default_k=None):

    if default_k is None:
        default_k = 30
    default_k = str(default_k)
Adam P. Goucher's avatar
Adam P. Goucher committed
996

Adam P. Goucher's avatar
Adam P. Goucher committed
997
    s = s.lower()
Adam P. Goucher's avatar
Adam P. Goucher committed
998
    s = ''.join([(c if (c in '0123456789.') else ((' '+c) if (c in 'ijkpwtda') else '')) for c in s])
Adam P. Goucher's avatar
Adam P. Goucher committed
999 1000
    s = s.split()
    d = {k[0]: k[1:] for k in s}
Adam P. Goucher's avatar
Adam P. Goucher committed
1001

Adam P. Goucher's avatar
Adam P. Goucher committed
1002 1003 1004 1005 1006
    defaulti = repr(tuple([(1 if (i == (tsize-1)) else 0) for i in xrange(tsize)]))
    if 'i' not in d:
        d['i'] = defaulti
    elif d['i'] == '':
        d['i'] = raw_input("Please enter %d initial rows for %s search [%s] : " % (tsize, name, defaulti)) or defaulti
Adam P. Goucher's avatar
Adam P. Goucher committed
1007
    else:
Adam P. Goucher's avatar
Adam P. Goucher committed
1008
        d['i'] = '(%s,)' % d['i'].replace('.', ',')
Adam P. Goucher's avatar
Adam P. Goucher committed
1009

Adam P. Goucher's avatar
Adam P. Goucher committed
1010
    if 'w' not in d:
1011 1012 1013 1014
        if 'a' not in d:
            d['w'] = repr(4 + canon6(eval(d['i']))[1])
        else:
            d['w'] = raw_input("Please enter width for %s search [34] : " % name) or '34'
Adam P. Goucher's avatar
Adam P. Goucher committed
1015 1016 1017

    if 'a' not in d:
        d['a'] = '999999'
Adam P. Goucher's avatar
Adam P. Goucher committed
1018 1019

    if 'k' not in d:
1020
        d['k'] = raw_input("Please enter lookahead for %s search [%s] : " % (name, default_k)) or default_k
Adam P. Goucher's avatar
Adam P. Goucher committed
1021 1022 1023

    if 'j' not in d:
        d['j'] = '(%s) // 2' % d['k']
Adam P. Goucher's avatar
Adam P. Goucher committed
1024

Adam P. Goucher's avatar
Adam P. Goucher committed
1025 1026
    if 'p' not in d:
        d['p'] = raw_input("Please enter number of CPU cores for %s search [40] : " % name) or '40'
Adam P. Goucher's avatar
Adam P. Goucher committed
1027

Adam P. Goucher's avatar
Adam P. Goucher committed
1028 1029
    if 't' not in d:
        d['t'] = '600'
Adam P. Goucher's avatar
Adam P. Goucher committed
1030

Adam P. Goucher's avatar
Adam P. Goucher committed
1031 1032 1033 1034 1035
    if 'd' not in d:
        d['d'] = '0.9'

    d = {k : eval(v) for (k, v) in d.iteritems()}

Adam P. Goucher's avatar
Adam P. Goucher committed
1036 1037 1038
    for k in 'wkjpt':
        if not isinstance(d[k], int):
            raise TypeError('%s must be a positive *integer*.' % k)
Adam P. Goucher's avatar
Adam P. Goucher committed
1039
        if d[k] < (0 if (k == 'p') else 1):
Adam P. Goucher's avatar
Adam P. Goucher committed
1040 1041 1042 1043 1044 1045 1046 1047 1048
            raise ValueError('%s must be a *positive* integer.' % k)

    if not isinstance(d['i'], tuple):
        raise TypeError('Initial rows must be a %d-tuple.' % tsize)
    if len(d['i']) != tsize:
        raise ValueError('Precisely %d initial rows must be specified.' % tsize)

    if not isinstance(d['d'], float):
        raise TypeError('Diligence must be a float.')
Adam P. Goucher's avatar
bugfix  
Adam P. Goucher committed
1049
    if (d['d'] <= 0.0) or (d['d'] > 1.0):
Adam P. Goucher's avatar
Adam P. Goucher committed
1050 1051
        raise ValueError('Diligence must be in the semiopen interval (0, 1].')

Adam P. Goucher's avatar
Adam P. Goucher committed
1052 1053 1054
    if not isinstance(d['a'], int):
        raise TypeError('Adaptive widening parameter must be an integer.')

Adam P. Goucher's avatar
Adam P. Goucher committed
1055
    return d
Adam P. Goucher's avatar
Adam P. Goucher committed
1056 1057 1058 1059


def clmain():

Adam P. Goucher's avatar
Adam P. Goucher committed
1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096
    parser = argparse.ArgumentParser(formatter_class=argparse.RawTextHelpFormatter)
    parser.add_argument('-d', '--directory', default=None, help='''
    This must be a fully-qualified path name, such as '/tmp/ikpx'. If the
    directory does not already exist, it will be created. If unspecified,
    the user will be prompted to specify the directory herself.
    ''')

    parser.add_argument('-v', '--velocity', default=None, help='''
    This can be either in Cartesian coordinates such as '(2,1)c/6' or a
    speed with direction (such as 'c/3o' or 'c/4d') for non-oblique. If a
    speed is specified without direction (such as '2c/5'), it will assume
    orthogonal. Again, the user will be prompted if unspecified.

    The velocity is canonicalised so that orthogonal spaceships point north,
    diagonal spaceships point north-west, and oblique spaceships point in a
    direction betwixt these two extremes.

    Note: as a result of the internal lattice transformation used to convert
    physical spacetime coordinates into logical coordinates, the velocity
    (a, b)c/p may only be searched if gcd(a, b, p) = 1.
    ''')

    hth = '''
    Search from the %s of the spaceship.

    This should be a string such as 'p8w34k30'. The possible specifiers are:

        p : number of cores over which to parallelise;
        w : width of search (in 'logical columns');
        k : lookahead (in 'logical rows');
        j : maximum jumpahead (in 'logical rows') -- this should be less than
            the lookahead parameter K, and defaults to floor(K/2);
        i : initial rows -- omit to auto-infer or provide an empty string to
            request user input;
        d : diligence -- exponential decay parameter alpha such that an
            item of width x is weighted by alpha^x (defaults to 0.9);
        t : timeout (in seconds) -- amount of time permitted for each
Adam P. Goucher's avatar
Adam P. Goucher committed
1097 1098
            instance of the underlying SAT solver (defaults to 600);
        a : adaptive widening -- maximum number of times to increment the
Adam P. Goucher's avatar
Adam P. Goucher committed
1099 1100 1101 1102
            search width to allow the search to continue.

    If neither the 'a' nor the 'w' parameters are specified, it will default
    to unlimited adaptive widening with a narrow initial width. If 'a' alone
Adam P. Goucher's avatar
Adam P. Goucher committed
1103
    is specified, the user will be prompted for the initial width.'''
Adam P. Goucher's avatar
Adam P. Goucher committed
1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115

    parser.add_argument('-f', '--head', default=None, help=(hth % 'front'))

    hth += '''

    If both --head and --tail are specified, then ikpx will attempt a
    meet-in-the-middle search by growing from both the front and back and
    looking for compatible overlaps. Note that in this case, the number of
    cores used will be the sum of the 'p' parameters for both search halves.
    '''

    parser.add_argument('-b', '--tail', default=None, help=(hth % 'back'))
Adam P. Goucher's avatar
Adam P. Goucher committed
1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131

    parser.add_argument('-e', '--encoding', default='split', help='''
    Method of encoding the cellular automaton transition rules as a set of
    SAT clauses. Possibilities are:

        'knuth' : the 'sophisticated' encoding suggested by Donald Knuth in
            The Art of Computer Programming. This sums neighbour counts using
            a binary tree and involves 13 extra variables per cell.
        'split' : the default encoding, which deviates from Knuth by using a
            mixed binary/ternary tree instead of a pure binary tree. This
            involves only 8 extra variables per cell, at the expense of
            (very slightly) more clauses.
        'naive' : uses only 3 extra variables per cell, but with much more
            complex clauses.
    ''')

1132 1133 1134 1135
    parser.add_argument('-l', '--loadhead', default=None, help='''
    RLE file in ikpx format to load as an additional head.
    ''')

Adam P. Goucher's avatar
Adam P. Goucher committed
1136 1137 1138 1139 1140 1141
    parser.add_argument('-c', '--command', default=None, help='''
    If specified, RLE representations of all phases of all partials will
    be piped into the standard input of this command. This probably needs
    to be in quotes to ensure it is treated as a single argument to ikpx.
    ''')

Adam P. Goucher's avatar
Adam P. Goucher committed
1142 1143
    args = parser.parse_args()

Adam P. Goucher's avatar
Adam P. Goucher committed
1144 1145 1146 1147
    horizontal_line()
    print("Incremental Knightship Partial Extend (ikpx)")
    horizontal_line()

Adam P. Goucher's avatar
Adam P. Goucher committed
1148 1149
    directory = args.directory
    if directory is None:
Adam P. Goucher's avatar
Adam P. Goucher committed
1150
        directory = raw_input("Please enter fully-qualified target directory [/tmp/ikpx] : ") or '/tmp/ikpx'
Adam P. Goucher's avatar
Adam P. Goucher committed
1151 1152 1153 1154 1155

    velocity = args.velocity
    if velocity is None:
        velocity = raw_input("Please enter velocity [(2,1)c/6] : ") or '(2,1)c/6'

Adam P. Goucher's avatar
Adam P. Goucher committed
1156 1157 1158
    psets = {}

    print("Parsing velocity...")
Adam P. Goucher's avatar
Adam P. Goucher committed
1159 1160
    a, b, p = parse_velocity(velocity)
    params = partial_derivatives(a, b, p)
Adam P. Goucher's avatar
Adam P. Goucher committed
1161
    tsize = calculate_padding(params['dvdt'], params['dvdx'], params['dvdy'])
Adam P. Goucher's avatar
Adam P. Goucher committed
1162 1163
    print("Parameters: %s" % repr(params))
    stdout.flush()
Adam P. Goucher's avatar
Adam P. Goucher committed
1164

Adam P. Goucher's avatar
Adam P. Goucher committed
1165
    if args.head:
1166
        psets['head'] = parse_descriptor(args.head, tsize, 'head', 6*params['dvdy'] + 12)
Adam P. Goucher's avatar
Adam P. Goucher committed
1167

Adam P. Goucher's avatar
Adam P. Goucher committed
1168
    if args.tail:
1169
        psets['tail'] = parse_descriptor(args.tail, tsize, 'tail', 8*params['dvdy'] + 12)
Adam P. Goucher's avatar
Adam P. Goucher committed
1170

Adam P. Goucher's avatar
Adam P. Goucher committed
1171 1172
    if (len(psets) == 0):
        print("Neither head nor tail specified; defaulting to head.")
1173
        psets['head'] = parse_descriptor('', tsize, 'the', 6*params['dvdy'] + 12)
Adam P. Goucher's avatar
Adam P. Goucher committed
1174

Adam P. Goucher's avatar
Adam P. Goucher committed
1175 1176 1177 1178
    if ('head' in psets) and (psets['head']['p'] == 0):
        dict_to_rle(psets, params, directory, args.command)
    else:
        do_everything(psets, params, directory, encoding=args.encoding, loadhead=args.loadhead, cmd=args.command)
Adam P. Goucher's avatar
Adam P. Goucher committed
1179 1180 1181

if __name__ == '__main__':

Adam P. Goucher's avatar
Adam P. Goucher committed