<commit_before>package leo.modules.seqpproc

import leo.datastructures.impl.Signature
import leo.datastructures._
import leo.datastructures.Term.:::>
import leo.modules.SZSException
import leo.modules.calculus.CalculusRule
import leo.modules.calculus.HuetsPreUnification
import leo.modules.normalization.Simplification
import leo.modules.output.{SZS_Error, SZS_EquiSatisfiable, SZS_Theorem, SZS_CounterSatisfiable}
import leo.Out

import scala.annotation.tailrec
import scala.collection.SortedSet

object DefExpSimp extends CalculusRule {
  val name = "defexp_and_simp"
  override val inferenceStatus = Some(SZS_Theorem)
  def apply(t: Term): Term = {
    val sig = Signature.get
    val symb: Set[Signature#Key] = Set(sig("?").key, sig("&").key, sig("=>").key, sig("<=>").key)
    Simplification.normalize(t.exhaustive_δ_expand_upTo(symb))
  }
}

////////////////////////////////////////////////////////////////
////////// Normalization
////////////////////////////////////////////////////////////////

object PolaritySwitch extends CalculusRule {
  val name = "polarity_switch"
  override val inferenceStatus = Some(SZS_Theorem)
  def canApply(t: Term): Boolean = t match {
    case Not(_) => true
    case _ => false
  }
  def canApply(l: Literal): Boolean = canApply(l.left) || canApply(l.right)

  def apply(t: Term): Term = t match {
    case Not(t2) => t2
    case _ => t
  }

  def apply(l: Literal): Literal = if (l.equational) {
    (l.left, l.right) match {
      case (Not(l2), Not(r2)) => Literal(l2, r2, l.polarity)
      case (Not(l2), _) => Literal(l2, l.right, !l.polarity)
      case (_, Not(r2)) => Literal(l.left, r2, !l.polarity)
      case _ => l
    }
  } else {
    l.left match {
      case Not(l2) => Literal(l2, !l.polarity)
      case _ => l
    }
  }
}

object CNF_Forall extends CalculusRule {
  val name = "cnf_forall"
  override val inferenceStatus = Some(SZS_Theorem)
  def apply(t: Term, polarity: Boolean): Term =  {
    removeLeadingQuants(t, polarity)
  }
  def removeLeadingQuants(t: Term, polarity: Boolean): Term = t match {
    case Forall(ty :::> body) => removeLeadingQuants(body, polarity)
    case _ => t
  }
}

/** Non-extensional CNF rule. */
object CNF extends CalculusRule {
  // TODO: Can be optimize this? E.g. dependencies for skolemterm
  final val name = "cnf"
  final override val inferenceStatus = Some(SZS_Theorem)

  type FormulaCharacter = Byte
  final val none: FormulaCharacter = 0.toByte
  final val alpha: FormulaCharacter = 1.toByte
  final val beta: FormulaCharacter = 2.toByte
//  final val one: FormulaCharacter = 3.toByte  // A bit hacky, we want to omit ++ operations below
//  final val four: FormulaCharacter = 4.toByte  // A bit hacky, we want to omit ++ operations below

  final def canApply(l: Literal): Boolean = if (!l.equational) {
    l.left match {
      case Not(t) => true
      case s ||| t => true
      case s & t => true
      case s Impl t => true
      case s <=> t => true
      case Forall(ty :::> t) => true
      case Exists(ty :::> t) => true
      case _ => false
    }
  } else false

  final def apply(vargen: leo.modules.calculus.FreshVarGen, l: Literal): (FormulaCharacter, Seq[Literal]) = {
    import leo.datastructures.{|||, &, Not, Forall, Exists, Impl, <=>}
    if (l.equational) {
      (none, Seq(l))
    } else {
      if (l.polarity) {
        l.left match {
          case Not(t) => (alpha, Seq(Literal(t, false)))
          case s ||| t => (beta, Seq(Literal(s, true),Literal(t,true)))
          case s & t => (alpha, Seq(Literal(s, true),Literal(t,true)))
          case s Impl t => (beta, Seq(Literal(s, false),Literal(t,true)))
          case s <=> t => ???
          case Forall(ty :::> t) => (beta, Seq(Literal(t.substitute(Subst.singleton(1, vargen.apply(ty))),true)))
          case Exists(ty :::> t) => (beta, Seq(Literal(t.substitute(Subst.singleton(1, leo.modules.calculus.skTerm(ty, vargen.existingVars))),true)))
          case _ => (none, Seq(l))
        }
      } else {
        l.left match {
          case Not(t) => (alpha, Seq(Literal(t, true)))
          case s ||| t => (alpha, Seq(Literal(s, false),Literal(t,false)))
          case s & t => (beta, Seq(Literal(s, false),Literal(t,false)))
          case s Impl t => (alpha, Seq(Literal(s, true),Literal(t,false)))
          case s <=> t => ???
          case Forall(ty :::> t) => (beta, Seq(Literal(t.substitute(Subst.singleton(1, leo.modules.calculus.skTerm(ty, vargen.existingVars))),false)))
          case Exists(ty :::> t) => (beta, Seq(Literal(t.substitute(Subst.singleton(1, vargen.apply(ty))),false)))
          case _ => (none, Seq(l))
        }
      }
    }
  }

  final def apply(vargen: leo.modules.calculus.FreshVarGen, cl: Clause): Seq[Clause] = {
    apply0(vargen, cl.lits, Seq(Seq())).map(Clause.apply)
  }

  final private def apply0(vargen: leo.modules.calculus.FreshVarGen, lits: Seq[Literal], acc: Seq[Seq[Literal]]): Seq[Seq[Literal]] = {
    if (lits.isEmpty) {
      acc
    } else {
      val hd = lits.head
      val tail = lits.tail
      val (resChar, res) = apply(vargen, hd)
      if (resChar == none) {
        // Already normalized
        apply0(vargen, tail, acc.map(hd +: _))
      } else if (resChar == alpha) {
        val deepRes = apply0(vargen, res, Seq(Seq()))
        apply0(vargen, tail, deepRes.flatMap(res => res.flatMap(r => acc.map(_ :+ r))))
      } else if (resChar == beta) {
        val deepRes = apply0(vargen, res, Seq(Seq()))
        apply0(vargen, tail, deepRes.flatMap(res => acc.map(_ ++ res)))
      } else {
        throw new SZSException(SZS_Error,
          "cnf calculus error: returning something other than alpha or beta",
          s"Returning ${resChar} while normalizing ${hd.pretty}")
      }

    }
  }


}


object LiftEq extends CalculusRule {
  val name = "lifteq"
  override val inferenceStatus = Some(SZS_Theorem)

  import leo.datastructures.{=== => EQ}
  def canApply(t: Term): Boolean = t match {
    case EQ(_,_) => true
    case _ => false
  }<commit_msg>new version of CNF rule<commit_after>package leo.modules.seqpproc

import leo.datastructures.impl.Signature
import leo.datastructures._
import leo.datastructures.Term.:::>
import leo.modules.SZSException
import leo.modules.calculus.CalculusRule
import leo.modules.calculus.HuetsPreUnification
import leo.modules.normalization.Simplification
import leo.modules.output.{SZS_Error, SZS_EquiSatisfiable, SZS_Theorem, SZS_CounterSatisfiable}
import leo.Out

import scala.annotation.tailrec
import scala.collection.SortedSet

object DefExpSimp extends CalculusRule {
  val name = "defexp_and_simp"
  override val inferenceStatus = Some(SZS_Theorem)
  def apply(t: Term): Term = {
    val sig = Signature.get
    val symb: Set[Signature#Key] = Set(sig("?").key, sig("&").key, sig("=>").key, sig("<=>").key)
    Simplification.normalize(t.exhaustive_δ_expand_upTo(symb))
  }
}

////////////////////////////////////////////////////////////////
////////// Normalization
////////////////////////////////////////////////////////////////

object PolaritySwitch extends CalculusRule {
  val name = "polarity_switch"
  override val inferenceStatus = Some(SZS_Theorem)
  def canApply(t: Term): Boolean = t match {
    case Not(_) => true
    case _ => false
  }
  def canApply(l: Literal): Boolean = canApply(l.left) || canApply(l.right)

  def apply(t: Term): Term = t match {
    case Not(t2) => t2
    case _ => t
  }

  def apply(l: Literal): Literal = if (l.equational) {
    (l.left, l.right) match {
      case (Not(l2), Not(r2)) => Literal(l2, r2, l.polarity)
      case (Not(l2), _) => Literal(l2, l.right, !l.polarity)
      case (_, Not(r2)) => Literal(l.left, r2, !l.polarity)
      case _ => l
    }
  } else {
    l.left match {
      case Not(l2) => Literal(l2, !l.polarity)
      case _ => l
    }
  }
}

object CNF_Forall extends CalculusRule {
  val name = "cnf_forall"
  override val inferenceStatus = Some(SZS_Theorem)
  def apply(t: Term, polarity: Boolean): Term =  {
    removeLeadingQuants(t, polarity)
  }
  def removeLeadingQuants(t: Term, polarity: Boolean): Term = t match {
    case Forall(ty :::> body) => removeLeadingQuants(body, polarity)
    case _ => t
  }
}

/** Non-extensional CNF rule. */
object CNF extends CalculusRule {
  // TODO: Can be optimize this? E.g. dependencies for skolemterm
  final val name = "cnf"
  final override val inferenceStatus = Some(SZS_Theorem)

  type FormulaCharacter = Byte
  final val none: FormulaCharacter = 0.toByte
  final val alpha: FormulaCharacter = 1.toByte
  final val beta: FormulaCharacter = 2.toByte
  final val one: FormulaCharacter = 3.toByte  // A bit hacky, we want to omit ++ operations below
//  final val four: FormulaCharacter = 4.toByte  // A bit hacky, we want to omit ++ operations below

  final def canApply(l: Literal): Boolean = if (!l.equational) {
    l.left match {
      case Not(t) => true
      case s ||| t => true
      case s & t => true
      case s Impl t => true
      case s <=> t => true
      case Forall(ty :::> t) => true
      case Exists(ty :::> t) => true
      case _ => false
    }
  } else false

  final def apply(vargen: leo.modules.calculus.FreshVarGen, l: Literal): (FormulaCharacter, Seq[Literal]) = {
    import leo.datastructures.{|||, &, Not, Forall, Exists, Impl, <=>}
    if (l.equational) {
      (none, Seq(l))
    } else {
      if (l.polarity) {
        l.left match {
          case Not(t) => (one, Seq(Literal(t, false)))
          case s ||| t => (beta, Seq(Literal(s, true),Literal(t,true)))
          case s & t => (alpha, Seq(Literal(s, true),Literal(t,true)))
          case s Impl t => (beta, Seq(Literal(s, false),Literal(t,true)))
          case s <=> t => ???
          case Forall(ty :::> t) => (beta, Seq(Literal(t.substitute(Subst.singleton(1, vargen.apply(ty))),true)))
          case Exists(ty :::> t) => (beta, Seq(Literal(t.substitute(Subst.singleton(1, leo.modules.calculus.skTerm(ty, vargen.existingVars))),true)))
          case _ => (none, Seq(l))
        }
      } else {
        l.left match {
          case Not(t) => (one, Seq(Literal(t, true)))
          case s ||| t => (alpha, Seq(Literal(s, false),Literal(t,false)))
          case s & t => (beta, Seq(Literal(s, false),Literal(t,false)))
          case s Impl t => (alpha, Seq(Literal(s, true),Literal(t,false)))
          case s <=> t => ???
          case Forall(ty :::> t) => (beta, Seq(Literal(t.substitute(Subst.singleton(1, leo.modules.calculus.skTerm(ty, vargen.existingVars))),false)))
          case Exists(ty :::> t) => (beta, Seq(Literal(t.substitute(Subst.singleton(1, vargen.apply(ty))),false)))
          case _ => (none, Seq(l))
        }
      }
    }
  }

  final def apply(vargen: leo.modules.calculus.FreshVarGen, cl: Clause): Seq[Clause] = {
    apply0(vargen, cl.lits, Seq(Seq())).map(Clause.apply)
  }

  final private def apply0(vargen: leo.modules.calculus.FreshVarGen, lits: Seq[Literal], acc: Seq[Seq[Literal]]): Seq[Seq[Literal]] = {
    if (lits.isEmpty) {
      acc
    } else {
      val hd = lits.head
      val tail = lits.tail
      val (resChar, res) = apply(vargen, hd)
      if (resChar == none) {
        // Already normalized
        apply0(vargen, tail, acc.map(hd +: _))
      } else if (resChar == one) {
        val deepRes = apply0(vargen, res, Seq(Seq()))
        apply0(vargen, tail, deepRes.flatMap(res => res.flatMap(r => acc.map(_ :+ r))))
      } else if (resChar == alpha) {
        val deepRes0 = apply0(vargen, res.take(1), Seq(Seq()))
        val deepRes1 = apply0(vargen, res.drop(1), Seq(Seq()))
        val deepRes = deepRes0 ++ deepRes1
//        leo.Out.comment(s"Deep res alpha: ${deepRes.map(_.map(_.pretty))}")
        apply0(vargen, tail, deepRes.flatMap(res => acc.map(r => r ++ res)))
      } else if (resChar == beta) {
        val deepRes0 = apply0(vargen, res.take(1), Seq(Seq()))
        val deepRes1 = apply0(vargen, res.drop(1), Seq(Seq()))
        val deepRes = deepRes0.flatMap(res => deepRes1.map(res2 => res ++ res2))
//        leo.Out.comment(s"Deep res beta: ${deepRes.map(_.map(_.pretty))}")
        apply0(vargen, tail, deepRes.flatMap(res => acc.map(r => r ++ res)))
      } else {
        throw new SZSException(SZS_Error,
          "cnf calculus error: returning something other than alpha or beta",
          s"Returning ${resChar} while normalizing ${hd.pretty}")
      }

    }
  }


}


object LiftEq extends CalculusRule {
  val name = "lifteq"
  override val inferenceStatus = Some(SZS_Theorem)

  import leo.datastructures.{=== => EQ}
  def canApply(t: Term): Boolean = t match {
    case EQ(_,_) => true
    case _ => false
  }
{'fraction_non_alphanumeric': 0.17078384798099763, 'fraction_numerical': 0.005859065716547902, 'mean_word_length': 2.782869122491764, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 120, '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': '7383897', 'n_tokens_mistral': 4539, 'n_tokens_neox': 4365, 'n_words': 1054}