<commit_before>package at.forsyte.apalache.tla.bmcmt.rules

import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.lir.oper.TlaBoolOper
import at.forsyte.apalache.tla.lir.values.TlaFalse
import at.forsyte.apalache.tla.lir.{NameEx, OperEx, TlaEx, ValEx}

/**
  * Implements the rules: SE-AND[1-4].
  *
  * @author <NAME>
  */
class AndRule(rewriter: SymbStateRewriter) extends RewritingRule {
  override def isApplicable(symbState: SymbState): Boolean = {
    symbState.ex match {
      case OperEx(TlaBoolOper.and, _*) => true
      case _ => false
    }
  }

  override def apply(state: SymbState): SymbState = {
    val falseConst = rewriter.solverContext.falseConst
    state.ex match {
      case OperEx(TlaBoolOper.and, args@_*) =>
        // We preprocess the arguments twice: before rewriting them and after rewriting them
        // Hence, we call preprocessOrCall two times.
        def mapPreprocessMkAnd: SymbState = {
          val (newState: SymbState, preds: Seq[TlaEx]) =
            rewriter.rewriteSeqUntilDone(state.setTheory(BoolTheory()), args)

          def mkAnd: SymbState = {
            val newPred = rewriter.solverContext.introBoolConst()
            val cons = OperEx(TlaBoolOper.equiv,
              NameEx(newPred),
              OperEx(TlaBoolOper.and, preds: _*))
            rewriter.solverContext.assertGroundExpr(cons)
            newState.setRex(NameEx(newPred))
          }

          preprocessOrCall(newState, preds, mkAnd)
        }

        val finalState = preprocessOrCall(state, args, mapPreprocessMkAnd)
        rewriter.coerce(finalState, state.theory) // coerce if needed

      case _ =>
        throw new RewriterException("%s is not applicable".format(getClass.getSimpleName))
    }
  }

  private def preprocessOrCall(state: SymbState, args: Seq[TlaEx],
                               defaultFun: => SymbState) = {
    // funny syntax for a function without arguments (similar to Unit-functions in OCaml)
    def isFalse(ex: TlaEx): Boolean =
      ex match {
        case ValEx(TlaFalse) =>
          true

        case NameEx(name) =>
          (name == state.arena.cellFalse().toString
            || name == rewriter.solverContext.falseConst)

        case _ =>
          false
      }

    if (args.isEmpty) {
      // empty conjunction is always true
      state.setTheory(BoolTheory())
        .setRex(NameEx(rewriter.solverContext.trueConst))

    } else if (args.exists(isFalse)) {
      // one false makes all false
      state.setTheory(BoolTheory())
        .setRex(NameEx(rewriter.solverContext.falseConst))
    } else {
      // note that defaultFun is called only here and thus does not add constraints in the other branches
      defaultFun
    }
  }
}<commit_msg>TLC-like conjunctions, e.g., A /\ B is IF A THEN B ELSE FALSE<commit_after>package at.forsyte.apalache.tla.bmcmt.rules

import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.lir.convenience.tla
import at.forsyte.apalache.tla.lir.oper.TlaBoolOper
import at.forsyte.apalache.tla.lir.{NameEx, OperEx, TlaEx, ValEx}

/**
  * Implements the rules: SE-AND[1-4].
  *
  * @author <NAME>
  */
class AndRule(rewriter: SymbStateRewriter) extends RewritingRule {
  override def isApplicable(symbState: SymbState): Boolean = {
    symbState.ex match {
      case OperEx(TlaBoolOper.and, _*) => true
      case _ => false
    }
  }

  override def apply(state: SymbState): SymbState = {
    val falseConst = rewriter.solverContext.falseConst
    val trueConst = rewriter.solverContext.trueConst
    val simplfier = new ConstSimplifier()
    simplfier.simplifyShallow(state.ex) match {
      case OperEx(TlaBoolOper.and, args @ _*) =>
        val finalState =
          if (args.isEmpty) {
            // empty conjunction is always true
            state.setRex(NameEx(trueConst)).setTheory(BoolTheory())
          } else {
            // use short-circuiting on state-level expressions (like in TLC)
            def toIte(es: Seq[TlaEx]): TlaEx = {
              es match {
                case Seq(last) => last
                case hd +: tail => tla.ite(hd, toIte(tail), NameEx(falseConst))
              }
            }
            // create a chain of IF-THEN-ELSE expressions and rewrite them
            val newState = state.setRex(toIte(args)).setTheory(BoolTheory())
            rewriter.rewriteUntilDone(newState)
          }

        rewriter.coerce(finalState, state.theory) // coerce if needed

      case e @ ValEx(_) =>
        // the simplifier has rewritten the disjunction to TRUE or FALSE
        rewriter.rewriteUntilDone(state.setRex(e))

      case e @ _ =>
        throw new RewriterException("%s is not applicable to %s".format(getClass.getSimpleName, e))
    }
  }
}
{'fraction_non_alphanumeric': 0.10506329113924051, 'fraction_numerical': 0.0008438818565400844, 'mean_word_length': 2.511851851851852, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 20, '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': '3874902', 'n_tokens_mistral': 1573, 'n_tokens_neox': 1522, 'n_words': 330}