text: #!/usr/bin/env python
  
  import os
  import readline
  import atexit
  import signal
  import clingo
  from threading import Condition
  
  class Controller:
      def __init__(self):
          histfile = os.path.join(os.path.expanduser("~"), ".controller")
          try: readline.read_history_file(histfile)
          except IOError: pass
          readline.parse_and_bind('tab: complete')
          def complete(commands, text, state):
              matches = []
              if state == 0: matches = [ c for c in commands if c.startswith(text) ]
              return matches[state] if state < len(matches) else None
          readline.set_completer(lambda text, state: complete(['more_pigeon_please', 'less_pigeon_please', 'solve', 'exit'], text, state))
          atexit.register(readline.write_history_file, histfile)
          self.solving = False
          self.condition = Condition()
  
      def register_solver(self, solver):
          self.solver = solver
  
      def interrupt(self, a, b):
          signal.signal(signal.SIGINT, signal.SIG_IGN)
          self.solver.stop()
  
      def on_finish(self, ret):
          self.message = "finish: " + str(ret) + (" (INTERRUPTED)" if ret.interrupted else "")
          self.condition.acquire()
          self.solving = False
          self.condition.notify()
          self.condition.release()
  
      def run(self):
          print("")
          print("this prompt accepts the following commands:")
          print("  solve              - start solving")
          print("  exit/EOF           - terminate the solver")
          print("  Ctrl-C             - interrupt current search")
          print("  less_pigeon_please - select an easy problem")
          print("  more_pigeon_please - select a difficult problem")
          print("")
  
          pyInt = signal.getsignal(signal.SIGINT)
          while True:
              signal.signal(signal.SIGINT, pyInt)
              try:
                  try: input_ = raw_input
                  except NameError: input_ = input
                  line = input_('> ')
                  signal.signal(signal.SIGINT, signal.SIG_IGN)
              except EOFError:
                  signal.signal(signal.SIGINT, signal.SIG_IGN)
                  line = "exit"
                  print(line)
              except KeyboardInterrupt:
                  signal.signal(signal.SIGINT, signal.SIG_IGN)
                  print
                  continue
              if line == "solve":
                  print("Solving...")
                  self.solving = True
                  self.solver.start(self.on_finish)
                  signal.signal(signal.SIGINT, self.interrupt)
                  self.condition.acquire()
                  while self.solving:
                      # NOTE: we need a timeout to catch signals
                      self.condition.wait(1000)
                  self.condition.release()
                  self.solver.finish()
                  for model in self.solver.models:
                      print("model: " + model)
                  print(self.message)
              elif line == "exit":
                  break
              elif line == "less_pigeon_please":
                  self.solver.set_more_pigeon(False)
              elif line == "more_pigeon_please":
                  self.solver.set_more_pigeon(True)
              else:
                  print("unknown command: " + line)
  
  class Solver:
      def __init__(self):
          self.k   = 0
          self.prg = clingo.Control()
          self.prg.load("client.lp")
          self.prg.ground([("pigeon", []), ("sleep",  [self.k])])
          self.prg.assign_external(clingo.Function("sleep", [self.k]), True)
          self.ret = None
          self.models = []
  
      def on_model(self, model):
          self.models.append(str(model))
  
      def start(self, on_finish):
          if self.ret is not None and not self.ret.unknown():
              self.k = self.k + 1
              self.prg.ground([("sleep", [self.k])])
              self.prg.release_external(clingo.Function("sleep", [self.k-1]))
              self.prg.assign_external(clingo.Function("sleep", [self.k]), True)
          self.future = self.prg.solve(on_model=self.on_model, on_finish=on_finish, async_=True)
  
      def stop(self):
          self.future.cancel()
  
      def finish(self):
          ret = self.future.get()
          return ret
  
      def set_more_pigeon(self, more):
          self.prg.assign_external(clingo.Function("p"), more)
  
  st = Solver()
  ct = Controller()
  ct.register_solver(st)
  ct.run()
  
  