<commit_before>package leo.datastructures

import leo.Configuration

import scala.collection.LinearSeq


/**
 * Clause interface, the companion object `Clause` offers several constructors methods.
 * The `id` of a clause is unique and is monotonously increasing.
 *
 * @author <NAME>
 * @since 07.11.2014
 */
trait Clause extends Ordered[Clause] with Pretty with HasCongruence[Clause] {
  /** The unique, increasing clause number. */
  def id: Int
  /** The underlying sequence of literals. */
  def lits: Seq[Literal]
  /** The types of the implicitly universally quantified variables. */
  def implicitlyBound: LinearSeq[Type]
  /** The source from where the clause was created, See `ClauseOrigin`. */
  def origin: ClauseOrigin

  // Further properties
  /** Those literals in `lits` that are positive. */
  def posLits: Seq[Literal]
  /** Those literals in `lits` that are negative. */
  def negLits: Seq[Literal]

  /** True iff this clause is horn. */
  @inline final val horn: Boolean = posLits.length <= 1
  /** True iff this clause is a unit clause. */
  @inline final val unit: Boolean = lits.length == 1
  /** True iff this clause is a demodulator. */
  @inline final val demodulator: Boolean = posLits.length == 1 && negLits.isEmpty
  /** True iff this clause is a rewrite rule. */
  @inline final val rewriteRule: Boolean = demodulator && posLits.head.oriented
  /** True iff this clause is ground. */
  @inline final val ground: Boolean = lits.view.forall(_.ground)
  /** True iff this clause is purely positive. i.e.
    * if all literals are positive. */
  @inline final val positive: Boolean = lits.view.forall(_.polarity)
  /** True iff this clause is purely negative. i.e.
    * if all literals are negative. */
  @inline final val negative: Boolean = lits.view.forall(!_.polarity)

  /** Returns a term representation of this clause.
    * @return Term `[l1] || [l2] || ... || [ln]` where `[.]` is the term representation of a literal,
    * and li are the literals in `lits`, `n = lits.length`. */
  final lazy val term: Term = mkPolyUnivQuant(implicitlyBound, mkDisjunction(lits.map(_.term)))

  // Operations on clauses
  // FIXME: Not right! Substitute has to mention newly introduced implicit bindings
  def substitute(s : Subst) : Clause = Clause.mkClause(lits.map(_.substitute(s)))

  @inline final def map[A](f: Literal => A): Seq[A] = lits.map(f)
  @inline final def mapLit(f: Literal => Literal): Clause = Clause.mkClause(lits.map(f), Derived)
  @inline final def replace(what: Term, by: Term): Clause = Clause.mkClause(lits.map(_.replaceAll(what, by)))

  /** The clause's weight. */
  @inline final def weight: Int = Configuration.CLAUSE_WEIGHTING.weightOf(this)
  @inline final def compare(that: Clause) = Configuration.CLAUSE_ORDERING.compare(this, that)

  final lazy val pretty = s"[${lits.map(_.pretty).mkString(" , ")}]"


  // System function adaptions
  override final def equals(obj : Any): Boolean = obj match {<commit_msg>adjusted interface of clause to new methods<commit_after>package leo.datastructures

import leo.Configuration

import scala.collection.LinearSeq


/**
 * Clause interface, the companion object `Clause` offers several constructors methods.
 * The `id` of a clause is unique and is monotonously increasing.
 *
 * @author <NAME>
 * @since 07.11.2014
 */
trait Clause extends Ordered[Clause] with Pretty with HasCongruence[Clause] {
  /** The unique, increasing clause number. */
  def id: Int
  /** The underlying sequence of literals. */
  def lits: Seq[Literal]
  /** The types of the implicitly universally quantified variables. */
  def implicitlyBound: Set[(Type, Int)]
  /** The source from where the clause was created, See `ClauseOrigin`. */
  def origin: ClauseOrigin

  // Further properties
  /** Those literals in `lits` that are positive. */
  def posLits: Seq[Literal]
  /** Those literals in `lits` that are negative. */
  def negLits: Seq[Literal]

  /** True iff this clause is horn. */
  @inline final val horn: Boolean = posLits.length <= 1
  /** True iff this clause is a unit clause. */
  @inline final val unit: Boolean = lits.length == 1
  /** True iff this clause is a demodulator. */
  @inline final val demodulator: Boolean = posLits.length == 1 && negLits.isEmpty
  /** True iff this clause is a rewrite rule. */
  @inline final val rewriteRule: Boolean = demodulator && posLits.head.oriented
  /** True iff this clause is ground. */
  @inline final val ground: Boolean = lits.view.forall(_.ground)
  /** True iff this clause is purely positive. i.e.
    * if all literals are positive. */
  @inline final val positive: Boolean = negLits.isEmpty
  /** True iff this clause is purely negative. i.e.
    * if all literals are negative. */
  @inline final val negative: Boolean = posLits.isEmpty

  @inline final val empty: Boolean = lits.isEmpty
  @inline final val effectivelyEmpty: Boolean = lits.isEmpty || lits.forall(_.flexflex)

  /** Returns a term representation of this clause.
    * @return Term `[l1] || [l2] || ... || [ln]` where `[.]` is the term representation of a literal,
    * and li are the literals in `lits`, `n = lits.length`. */
  final lazy val term: Term = mkPolyUnivQuant(implicitlyBound.map(_._1).toSeq, mkDisjunction(lits.map(_.term)))

  // Operations on clauses
  def substitute(s : Subst) : Clause = Clause.mkClause(lits.map(_.substitute(s)))

  @inline final def map[A](f: Literal => A): Seq[A] = lits.map(f)
  @inline final def mapLit(f: Literal => Literal): Clause = Clause.mkClause(lits.map(f), Derived)
  @inline final def replace(what: Term, by: Term): Clause = Clause.mkClause(lits.map(_.replaceAll(what, by)))

  /** The clause's weight. */
  @inline final def weight: Int = Configuration.CLAUSE_WEIGHTING.weightOf(this)
  @inline final def compare(that: Clause) = Configuration.CLAUSE_ORDERING.compare(this, that)

  final lazy val pretty = s"[${lits.map(_.pretty).mkString(" , ")}]"


  // System function adaptions
  override final def equals(obj : Any): Boolean = obj match {
{'fraction_non_alphanumeric': 0.12373022481265612, 'fraction_numerical': 0.004496253122398002, 'mean_word_length': 3.7216981132075473, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 9, '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': '3862448', 'n_tokens_mistral': 1893, 'n_tokens_neox': 1798, 'n_words': 655}