<commit_before>package leo

import java.util.logging.Level

import leo.datastructures.{Literal}
import leo.modules.CLParameterParser
import leo.modules.output.Output

/**
 * Configuration access point where central parameter settings of Leo-III
 * can be accessed and read. The Configuration object needs to be initialized
 * using the `init` method and a command line argument parser, i.e. subclasses of
 * `CLParameterParser`,
 *
 * @author <NAME>
 * @since 13.11.2014
 */
object Configuration extends DefaultConfiguration {
  private var configMap: Map[String, Seq[String]] = null

  private val PARAM_THREADCOUNT = "n"
  private val PARAM_VERBOSITY = "v"
  private val PARAM_TIMEOUT = "t"
  private val PARAM_PROOFOBJECT = "p"
  private val PARAM_HELP = "h"
  private val PARAM_COUNTERSAT = "c"

  // Collect standard options for nice output: short-option -> (long option, argname, description)
  private val optionsMap : Map[Char, (String, String, String)] = {
    Map(
      'h' -> ("", "", "Display this help message"),
      'n' -> ("", "N", "Maximum number of threads"),
      'p' -> ("", "", "Display proof output"),
      't' -> ("", "N", "Timeout in seconds"),
      'v' -> ("", "Lvl", "Set verbosity: From 0 (No Logging output) to 6 (very fine-grained debug output)"),
      'c' -> ("", "Csat", "Sets the proof mode to counter satisfiable (Through remote proof")
    )
  }

  /////////////////////////

  def init(parameterParser: CLParameterParser): Unit = configMap match {
    case null => {
      configMap = Map()
      for(param <- parameterParser.getParameters) {
        configMap += (param)
      }
      // Force computation of lazy values for early error output
      PROBLEMFILE
      THREADCOUNT
      TIMEOUT
      PROOF_OBJECT
      VERBOSITY
      COUNTER_SAT
      ()
    }
    case _ => ()
  }

  //////////////////////////
  // Predefined parameters
  //////////////////////////

  lazy val HELP: Boolean = isSet(PARAM_HELP)

  lazy val PROBLEMFILE: String = configMap.get(CLParameterParser.ARG0Name) match {
    case None => throw new IllegalArgumentException("No problem file given. Aborting.")
    case Some(str :: Nil) => str
    case Some(_) => throw new IllegalArgumentException("This should not happen. Please call support hotline.")
  }

  lazy val THREADCOUNT: Int = uniqueIntFor(PARAM_THREADCOUNT, DEFAULT_THREADCOUNT)

  lazy val VERBOSITY: java.util.logging.Level = {
    val v = configMap.get(PARAM_VERBOSITY) match {
      case None => DEFAULT_VERBOSITY
      case Some(arg :: Nil) => processLevel(arg)
      case Some(arg :: _) => Out.warn(multiDefOutput(PARAM_VERBOSITY));
                             processLevel(arg)
      case Some(_) => Out.warn(intExpectedOutput(PARAM_VERBOSITY,"None"));
                      DEFAULT_VERBOSITY
    }
    Out.setLogLevel(v)
    v
  }

  lazy val TIMEOUT: Int = uniqueIntFor(PARAM_TIMEOUT, DEFAULT_TIMEOUT)

  lazy val PROOF_OBJECT : Boolean = isSet(PARAM_PROOFOBJECT)


  lazy val COUNTER_SAT : Boolean = isSet(PARAM_COUNTERSAT)
  import leo.datastructures.{SizeBasedOrdering,LitWeight_TermSize, CLWeight_LitWeightSum, Orderings, CLOrdering_Lex_Weight_Age_Origin}

  lazy val CLAUSE_WEIGHTING: ClauseWeight = CLWeight_LitWeightSum
  lazy val CLAUSE_ORDERING: ClauseOrdering = CLOrdering_Lex_Weight_Age_Origin

  lazy val LITERAL_WEIGHTING: LiteralWeight = LitWeight_TermSize
  lazy val LITERAL_ORDERING: LiteralOrdering = Orderings.simple[Literal](LitWeight_TermSize)

  lazy val TERM_ORDERING: TermOrdering = SizeBasedOrdering

  // more to come ...

  ///////////////
  // Help output
  ///////////////
  lazy val helptext = {
    val sb = StringBuilder.newBuilder
    sb.append("Leo III -- A Higher-Order Theorem Prover.\n")
    sb.append("<NAME>, <NAME>, <NAME> and others.\n\n")
    sb.append("Usage: ... PROBLEM_FILE [OPTIONS]\n")
    sb.append("Options:\n")
    val it = optionsMap.iterator
    while (it.hasNext) {
      val entry = it.next()
      sb.append(s"-${entry._1}")
      if (!entry._2._2.isEmpty) {
        sb.append(s" ${entry._2._2}")
      }<commit_msg>now really set literal count as clause weight as default<commit_after>package leo

import java.util.logging.Level

import leo.datastructures.{ClWeight_LitCount, Literal}
import leo.modules.CLParameterParser
import leo.modules.output.Output

/**
 * Configuration access point where central parameter settings of Leo-III
 * can be accessed and read. The Configuration object needs to be initialized
 * using the `init` method and a command line argument parser, i.e. subclasses of
 * `CLParameterParser`,
 *
 * @author <NAME>
 * @since 13.11.2014
 */
object Configuration extends DefaultConfiguration {
  private var configMap: Map[String, Seq[String]] = null

  private val PARAM_THREADCOUNT = "n"
  private val PARAM_VERBOSITY = "v"
  private val PARAM_TIMEOUT = "t"
  private val PARAM_PROOFOBJECT = "p"
  private val PARAM_HELP = "h"
  private val PARAM_COUNTERSAT = "c"

  // Collect standard options for nice output: short-option -> (long option, argname, description)
  private val optionsMap : Map[Char, (String, String, String)] = {
    Map(
      'h' -> ("", "", "Display this help message"),
      'n' -> ("", "N", "Maximum number of threads"),
      'p' -> ("", "", "Display proof output"),
      't' -> ("", "N", "Timeout in seconds"),
      'v' -> ("", "Lvl", "Set verbosity: From 0 (No Logging output) to 6 (very fine-grained debug output)"),
      'c' -> ("", "Csat", "Sets the proof mode to counter satisfiable (Through remote proof")
    )
  }

  /////////////////////////

  def init(parameterParser: CLParameterParser): Unit = configMap match {
    case null => {
      configMap = Map()
      for(param <- parameterParser.getParameters) {
        configMap += (param)
      }
      // Force computation of lazy values for early error output
      PROBLEMFILE
      THREADCOUNT
      TIMEOUT
      PROOF_OBJECT
      VERBOSITY
      COUNTER_SAT
      ()
    }
    case _ => ()
  }

  //////////////////////////
  // Predefined parameters
  //////////////////////////

  lazy val HELP: Boolean = isSet(PARAM_HELP)

  lazy val PROBLEMFILE: String = configMap.get(CLParameterParser.ARG0Name) match {
    case None => throw new IllegalArgumentException("No problem file given. Aborting.")
    case Some(str :: Nil) => str
    case Some(_) => throw new IllegalArgumentException("This should not happen. Please call support hotline.")
  }

  lazy val THREADCOUNT: Int = uniqueIntFor(PARAM_THREADCOUNT, DEFAULT_THREADCOUNT)

  lazy val VERBOSITY: java.util.logging.Level = {
    val v = configMap.get(PARAM_VERBOSITY) match {
      case None => DEFAULT_VERBOSITY
      case Some(arg :: Nil) => processLevel(arg)
      case Some(arg :: _) => Out.warn(multiDefOutput(PARAM_VERBOSITY));
                             processLevel(arg)
      case Some(_) => Out.warn(intExpectedOutput(PARAM_VERBOSITY,"None"));
                      DEFAULT_VERBOSITY
    }
    Out.setLogLevel(v)
    v
  }

  lazy val TIMEOUT: Int = uniqueIntFor(PARAM_TIMEOUT, DEFAULT_TIMEOUT)

  lazy val PROOF_OBJECT : Boolean = isSet(PARAM_PROOFOBJECT)


  lazy val COUNTER_SAT : Boolean = isSet(PARAM_COUNTERSAT)
  import leo.datastructures.{SizeBasedOrdering,LitWeight_TermSize, CLWeight_LitWeightSum, Orderings, CLOrdering_Lex_Weight_Age_Origin}

  lazy val CLAUSE_WEIGHTING: ClauseWeight = ClWeight_LitCount
  lazy val CLAUSE_ORDERING: ClauseOrdering = CLOrdering_Lex_Weight_Age_Origin

  lazy val LITERAL_WEIGHTING: LiteralWeight = LitWeight_TermSize
  lazy val LITERAL_ORDERING: LiteralOrdering = Orderings.simple[Literal](LitWeight_TermSize)

  lazy val TERM_ORDERING: TermOrdering = SizeBasedOrdering

  // more to come ...

  ///////////////
  // Help output
  ///////////////
  lazy val helptext = {
    val sb = StringBuilder.newBuilder
    sb.append("Leo III -- A Higher-Order Theorem Prover.\n")
    sb.append("<NAME>, <NAME>, <NAME> and others.\n\n")
    sb.append("Usage: ... PROBLEM_FILE [OPTIONS]\n")
    sb.append("Options:\n")
    val it = optionsMap.iterator
    while (it.hasNext) {
      val entry = it.next()
      sb.append(s"-${entry._1}")
      if (!entry._2._2.isEmpty) {
        sb.append(s" ${entry._2._2}")
      }
{'fraction_non_alphanumeric': 0.13550830889540566, 'fraction_numerical': 0.0039100684261974585, 'mean_word_length': 2.9675230247212796, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 43, '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': '116107', 'n_tokens_mistral': 2583, 'n_tokens_neox': 2506, 'n_words': 676}