<commit_before>package leo

import leo.agents.{FifoController}
import leo.agents.impl.{CounterContextControlAgent, ContextControlAgent}
import leo.datastructures.blackboard.{DoneEvent, Blackboard}
import leo.datastructures.blackboard.impl.{FormulaDataStore, SZSDataStore}
import leo.datastructures.blackboard.scheduler.Scheduler
import leo.datastructures.context.Context
import leo.modules._
import leo.modules.Utility._
import leo.modules.output._
import leo.modules.phase.{PreprocessPhase, LoadPhase, Phase}
import Phase._


/**
 * Entry Point for Leo-III as an executable to
 * proof a TPTP File
 *
 * @author <NAME>
 * @since 7/8/14
 */
object Main {

  /**
   *
   * Tries to proof a Given TPTP file in
   * a given Time.
   *
   * @param args - See [[Configuration]] for argument treatment
   */
  def main(args : Array[String]){
    try {
      val beginTime = System.currentTimeMillis()
      try {
        Configuration.init(new CLParameterParser(args))
      } catch {
        case e: IllegalArgumentException => {
          Out.severe(e.getMessage)
          Configuration.help()
          return
        }
      }
      if (Configuration.HELP) {
        Configuration.help()
        return
      }

      val timeout = if (Configuration.TIMEOUT == 0) Double.PositiveInfinity else Configuration.TIMEOUT
      val interval = 10


      val deferredKill: DeferredKill = new DeferredKill(interval, timeout)
      deferredKill.start()

      // Create Scheduler
      Scheduler(Configuration.THREADCOUNT)

      //==========================================
      //
      // Initialize Phases and data strucutres for the blackboard.
      //
      //==========================================
      Blackboard().addDS(FormulaDataStore)
      Blackboard().addDS(SZSDataStore)
//      Utility.printSignature()
      var it: Iterator[Phase] = null
      if (Configuration.COUNTER_SAT) {
        new FifoController(CounterContextControlAgent).register()
        it = getCounterSat.iterator
      } else if (Configuration.isSet("with-prover")) {
        new FifoController(ContextControlAgent).register()
        it = getExternalPhases.iterator
      } else {
        new FifoController(ContextControlAgent).register()
        it = getHOStdPhase.iterator
      }
      var r = true
      while (it.hasNext && r && !deferredKill.isFinished) {
        val phase = it.next()
        Out.info(s"\n [Phase]:\n  Starting ${phase.name}\n${phase.description}")
        val start = System.currentTimeMillis()
        r = phase.execute()
        val end = System.currentTimeMillis()
        Out.info(s"\n [Phase]:\n  Ended ${phase.name}\n  Time: ${end - start}ms")
      }
      if(!deferredKill.isFinished) deferredKill.kill()


      val endTime = System.currentTimeMillis()
      Out.output(SZSOutput(SZSDataStore.getStatus(Context()).getOrElse(SZS_Unknown), Configuration.PROBLEMFILE, s"${endTime-beginTime} ms"))

      // TODO build switch for mulitple contexts
      // if (Configuration.PROOF_OBJECT) FormulaDataStore.getAll { p => p.clause.isEmpty}.foreach(Utility.printDerivation(_))
      //Utility.formulaContext()
      if (Configuration.PROOF_OBJECT) {
        Out.comment(s"SZS output start Proof for ${Configuration.PROBLEMFILE}")
        FormulaDataStore.getAll { p => p.clause.isEmpty}.headOption.fold(Out.comment("No proof found."))(Utility.printDerivation(_))
        Out.comment(s"SZS output end Proof for ${Configuration.PROBLEMFILE}")
      }
      
    } catch {
      case e:SZSException => {
        if (e.getMessage != null) {
          Out.info(e.getMessage)
          Out.output(SZSOutput(e.status, Configuration.PROBLEMFILE,e.getMessage))
        } else {
          Out.output(SZSOutput(e.status, Configuration.PROBLEMFILE))
        }
        Out.debug(e.debugMessage)
        Out.trace(stackTraceAsString(e))
        if (e.getCause != null) {
          Out.trace("Caused by: " + e.getCause.getMessage)
          Out.trace("at: " + e.getCause.getStackTrace.toString)
        }
      }
      case e:Throwable => {
        if (e.getMessage != null) {
          Out.info(e.getMessage)
          Out.output(SZSOutput(SZS_Error, Configuration.PROBLEMFILE,e.getMessage))
        } else {
          Out.output(SZSOutput(SZS_Error, Configuration.PROBLEMFILE))
        }
        Out.trace(stackTraceAsString(e))
        if (e.getCause != null) {
          Out.trace("Caused by: " + e.getCause.getMessage)
          Out.trace("at: " + e.getCause.getStackTrace.toString)
        }
      }
    } finally {
      Scheduler().killAll()
      System.exit(0)
    }
  }



  /**
   * Thread to kill leo.
   *
   * TODO: Hook to let the kill Thread die.
   *
   * @param interval
   * @param timeout
   */
  private class DeferredKill(interval : Double, timeout : Double) extends Thread {

    var remain : Double = timeout
    var exit : Boolean = false

    private var finished = false

    def isFinished = synchronized(finished)

    def kill() : Unit = {
      synchronized{
        exit = true
        this.interrupt()
        Out.info("Scheduler killed before timeout.")
      }
    }

    override def run(): Unit = {
      //      println("Init delay kill.")
      synchronized{
        while(remain > 0 && !exit) {
          try {
            val w : Double = if (remain > interval) interval else remain
            wait((w * 1000).toInt)
          } catch {
            case e: InterruptedException => if(exit) return else Thread.interrupted()
            case _: Throwable => ()
          } finally {
            if(!exit) {
              Scheduler().signal()
              //agentStatus()
              remain -= interval
              Out.info(s"Leo-III is still working. (Remain=$remain)")
            }
          }
        }
        SZSDataStore.forceStatus(Context())(SZS_Timeout)
        Out.info(s"Timeout: Killing all Processes.")
        finished = true
        //TODO: Better mechanism
        Blackboard().filterAll(_.filter(DoneEvent()))
        Scheduler().killAll()
      }
    }
  }
}

<commit_msg>add unification store to blackboard<commit_after>package leo

import leo.agents.{FifoController}
import leo.agents.impl.{CounterContextControlAgent, ContextControlAgent}
import leo.datastructures.blackboard.{DoneEvent, Blackboard}
import leo.datastructures.blackboard.impl.{UnificationStore, FormulaDataStore, SZSDataStore}
import leo.datastructures.blackboard.scheduler.Scheduler
import leo.datastructures.context.Context
import leo.modules._
import leo.modules.Utility._
import leo.modules.output._
import leo.modules.phase.{PreprocessPhase, LoadPhase, Phase}
import Phase._


/**
 * Entry Point for Leo-III as an executable to
 * proof a TPTP File
 *
 * @author <NAME>
 * @since 7/8/14
 */
object Main {

  /**
   *
   * Tries to proof a Given TPTP file in
   * a given Time.
   *
   * @param args - See [[Configuration]] for argument treatment
   */
  def main(args : Array[String]){
    try {
      val beginTime = System.currentTimeMillis()
      try {
        Configuration.init(new CLParameterParser(args))
      } catch {
        case e: IllegalArgumentException => {
          Out.severe(e.getMessage)
          Configuration.help()
          return
        }
      }
      if (Configuration.HELP) {
        Configuration.help()
        return
      }

      val timeout = if (Configuration.TIMEOUT == 0) Double.PositiveInfinity else Configuration.TIMEOUT
      val interval = 10


      val deferredKill: DeferredKill = new DeferredKill(interval, timeout)
      deferredKill.start()

      // Create Scheduler
      Scheduler(Configuration.THREADCOUNT)

      //==========================================
      //
      // Initialize Phases and data strucutres for the blackboard.
      //
      //==========================================
      Blackboard().addDS(FormulaDataStore)
      Blackboard().addDS(SZSDataStore)
      Blackboard().addDS(UnificationStore)
//      Utility.printSignature()
      var it: Iterator[Phase] = null
      if (Configuration.COUNTER_SAT) {
        new FifoController(CounterContextControlAgent).register()
        it = getCounterSat.iterator
      } else if (Configuration.isSet("with-prover")) {
        new FifoController(ContextControlAgent).register()
        it = getExternalPhases.iterator
      } else {
        new FifoController(ContextControlAgent).register()
        it = getHOStdPhase.iterator
      }
      var r = true
      while (it.hasNext && r && !deferredKill.isFinished) {
        val phase = it.next()
        Out.info(s"\n [Phase]:\n  Starting ${phase.name}\n${phase.description}")
        val start = System.currentTimeMillis()
        r = phase.execute()
        val end = System.currentTimeMillis()
        Out.info(s"\n [Phase]:\n  Ended ${phase.name}\n  Time: ${end - start}ms")
      }
      if(!deferredKill.isFinished) deferredKill.kill()


      val endTime = System.currentTimeMillis()
      Out.output(SZSOutput(SZSDataStore.getStatus(Context()).getOrElse(SZS_Unknown), Configuration.PROBLEMFILE, s"${endTime-beginTime} ms"))

      // TODO build switch for mulitple contexts
      // if (Configuration.PROOF_OBJECT) FormulaDataStore.getAll { p => p.clause.isEmpty}.foreach(Utility.printDerivation(_))
      //Utility.formulaContext()
      if (Configuration.PROOF_OBJECT) {
        Out.comment(s"SZS output start Proof for ${Configuration.PROBLEMFILE}")
        FormulaDataStore.getAll { p => p.clause.isEmpty}.headOption.fold(Out.comment("No proof found."))(Utility.printDerivation(_))
        Out.comment(s"SZS output end Proof for ${Configuration.PROBLEMFILE}")
      }
      
    } catch {
      case e:SZSException => {
        if (e.getMessage != null) {
          Out.info(e.getMessage)
          Out.output(SZSOutput(e.status, Configuration.PROBLEMFILE,e.getMessage))
        } else {
          Out.output(SZSOutput(e.status, Configuration.PROBLEMFILE))
        }
        Out.debug(e.debugMessage)
        Out.trace(stackTraceAsString(e))
        if (e.getCause != null) {
          Out.trace("Caused by: " + e.getCause.getMessage)
          Out.trace("at: " + e.getCause.getStackTrace.toString)
        }
      }
      case e:Throwable => {
        if (e.getMessage != null) {
          Out.info(e.getMessage)
          Out.output(SZSOutput(SZS_Error, Configuration.PROBLEMFILE,e.getMessage))
        } else {
          Out.output(SZSOutput(SZS_Error, Configuration.PROBLEMFILE))
        }
        Out.trace(stackTraceAsString(e))
        if (e.getCause != null) {
          Out.trace("Caused by: " + e.getCause.getMessage)
          Out.trace("at: " + e.getCause.getStackTrace.toString)
        }
      }
    } finally {
      Scheduler().killAll()
      System.exit(0)
    }
  }



  /**
   * Thread to kill leo.
   *
   * TODO: Hook to let the kill Thread die.
   *
   * @param interval
   * @param timeout
   */
  private class DeferredKill(interval : Double, timeout : Double) extends Thread {

    var remain : Double = timeout
    var exit : Boolean = false

    private var finished = false

    def isFinished = synchronized(finished)

    def kill() : Unit = {
      synchronized{
        exit = true
        this.interrupt()
        Out.info("Scheduler killed before timeout.")
      }
    }

    override def run(): Unit = {
      //      println("Init delay kill.")
      synchronized{
        while(remain > 0 && !exit) {
          try {
            val w : Double = if (remain > interval) interval else remain
            wait((w * 1000).toInt)
          } catch {
            case e: InterruptedException => if(exit) return else Thread.interrupted()
            case _: Throwable => ()
          } finally {
            if(!exit) {
              Scheduler().signal()
              //agentStatus()
              remain -= interval
              Out.info(s"Leo-III is still working. (Remain=$remain)")
            }
          }
        }
        SZSDataStore.forceStatus(Context())(SZS_Timeout)
        Out.info(s"Timeout: Killing all Processes.")
        finished = true
        //TODO: Better mechanism
        Blackboard().filterAll(_.filter(DoneEvent()))
        Scheduler().killAll()
      }
    }
  }
}


{'fraction_non_alphanumeric': 0.1291278926130281, 'fraction_numerical': 0.0021411512805731697, 'mean_word_length': 2.3865030674846626, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 23, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2620440', 'n_tokens_mistral': 3646, 'n_tokens_neox': 3546, 'n_words': 726}