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

import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.lir.oper.TlaOper
import at.forsyte.apalache.tla.lir.values.TlaInt
import at.forsyte.apalache.tla.lir.{NameEx, OperEx, ValEx}

/**
  * Implements the rule SE-INT-CONST.
  *
  * @author <NAME>
  */
class IntConstRule(rewriter: SymbStateRewriter) extends RewritingRule {
  override def isApplicable(symbState: SymbState): Boolean = {
    symbState.ex match {
      case ValEx(TlaInt(_)) => true
      case _ => false
    }
  }

  override def apply(state: SymbState): SymbState = {
    state.ex match {
      case ValEx(TlaInt(n)) =>
        val intConst = state.solverCtx.introIntConst()
        state.solverCtx.assertGroundExpr(OperEx(TlaOper.eq, NameEx(intConst), ValEx(TlaInt(n))))
        val finalState =
          state.setTheory(IntTheory()).setRex(NameEx(intConst))
        rewriter.coerce(finalState, state.theory)

      case _ =>
        throw new RewriterException("IntConstRule is not applicable")
    }
  }
}
<commit_msg>value cache for integer literals<commit_after>package at.forsyte.apalache.tla.bmcmt.rules

import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.lir.oper.TlaOper
import at.forsyte.apalache.tla.lir.values.TlaInt
import at.forsyte.apalache.tla.lir.{NameEx, OperEx, ValEx}

import scala.collection.mutable

/**
  * Implements the rule SE-INT-CONST.
  *
  * @author <NAME>
  */
class IntConstRule(rewriter: SymbStateRewriter) extends RewritingRule {
  // cache the integer constants that are introduced for integer literals
  private val cache: mutable.Map[BigInt, String] = new mutable.HashMap()

  override def isApplicable(symbState: SymbState): Boolean = {
    symbState.ex match {
      case ValEx(TlaInt(_)) => true
      case _ => false
    }
  }

  override def apply(state: SymbState): SymbState = {
    state.ex match {
      case ValEx(TlaInt(n)) =>
        val intConst =
          if (cache.contains(n)) {
            cache(n)
          } else {
            // introduce a new constant
            val intConst = state.solverCtx.introIntConst()
            state.solverCtx.assertGroundExpr(OperEx(TlaOper.eq, NameEx(intConst), ValEx(TlaInt(n))))
            cache.put(n, intConst)
            intConst
          }
        val finalState =
          state.setTheory(IntTheory()).setRex(NameEx(intConst))
        rewriter.coerce(finalState, state.theory)

      case _ =>
        throw new RewriterException("IntConstRule is not applicable")
    }
  }
}

{'fraction_non_alphanumeric': 0.11377952755905511, 'fraction_numerical': 0.0, 'mean_word_length': 3.001574803149606, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 13, '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': '2373813', 'n_tokens_mistral': 908, 'n_tokens_neox': 886, 'n_words': 160}