<commit_before>package regolic
package smtlib

import scala.collection.TraversableOnce

import regolic.asts.core.Trees.{Sort => TSort, _}
import regolic.asts.fol.Trees._
import regolic.asts.theories.int.{Trees => IntTrees}
import regolic.asts.theories.real.{Trees => RealTrees}
import regolic.asts.theories.array.{Trees => ArrayTrees}

import regolic.sexpr
import regolic.sexpr.SExprs._

import util.Logger

import Commands._

import java.io.OutputStream
import java.io.FileOutputStream
import java.io.PrintStream

/*
 * We assume symbols declaration are valid at the top level and are not scope (stack/frame) specific
 * (Even Z3 is not supporting that)
 * Though, we might want to actually support this as that is the standard and may not be that difficult to implement
 *
 * :print-success is at false by default, although the SMTLIB standard seems to assume it to be true by default. It seems more reasonnable to not print 'success' on each command
 */
class Interpreter(implicit val context: Context) {

  /*
   * TODO: ignoring logger from context because the SMTLIB scripting language provides option
   * to configure its own, as well as standard defaults. How to make it more configurable by still
   * using the context ?
   */

  private implicit val tag = Logger.Tag("SMTLIB Interpreter")

  private var funSymbols: Map[String, FunctionSymbol] = Map()
  private var predSymbols: Map[String, PredicateSymbol] = Map()

  private val solver = new cafesat.Solver
  private var expectedResult: Option[Boolean] = None

  private var regularOutput: PrintStream = System.out
  private var regularOutputClosable: Option[PrintStream] = None
  private var loggingOutput: PrintStream = System.err
  private var loggingOutputClosable: Option[PrintStream] = None
  private var loggingLevel: Logger.LogLevel = Logger.Warning

  private var printSuccess: Boolean = false

  //make a new logger according to current SMT options
  private val logger = new Logger {
    override def output(msg: String): Unit = loggingOutput.println(msg)

    override def logLevel: Logger.LogLevel = loggingLevel
  }

  def eval(command: Command): CommandResponse = {
    logger.info("Evaluating command: " + command)
    val res = command match {
      case SetLogic(QF_UF) => Success
      case SetLogic(_) => Unsupported
      case DeclareSort(SSymbol(name), arity) => Success
      case DeclareFun(SSymbol(name), sorts, sort) => {
        val paramSorts = sorts map parseSort
        val returnSort = parseSort(sort)
        if(returnSort == TSort("BOOL", List()))
          predSymbols += (name -> PredicateSymbol(name, paramSorts.toList))
        else
          funSymbols += (name -> FunctionSymbol(name, paramSorts.toList, returnSort))
        Success
      }
      case Pop(n) => {
        try {
          solver.pop(n)
          Success
        } catch {
          case (e: Exception) => Error("Cannot pop " + n + " scope frames")
        }
      }
      case Push(n) => {
        (1 to n).foreach(_ => solver.push())
        Success
      }
      case Assert(f) => {<commit_msg>double set-logic is an error<commit_after>package regolic
package smtlib

import scala.collection.TraversableOnce

import regolic.asts.core.Trees.{Sort => TSort, _}
import regolic.asts.fol.Trees._
import regolic.asts.theories.int.{Trees => IntTrees}
import regolic.asts.theories.real.{Trees => RealTrees}
import regolic.asts.theories.array.{Trees => ArrayTrees}

import regolic.sexpr
import regolic.sexpr.SExprs._

import util.Logger

import Commands._

import java.io.OutputStream
import java.io.FileOutputStream
import java.io.PrintStream

/*
 * We assume symbols declaration are valid at the top level and are not scope (stack/frame) specific
 * (Even Z3 is not supporting that)
 * Though, we might want to actually support this as that is the standard and may not be that difficult to implement
 *
 * :print-success is at false by default, although the SMTLIB standard seems to assume it to be true by default. It seems more reasonnable to not print 'success' on each command
 */
class Interpreter(implicit val context: Context) {

  /*
   * TODO: ignoring logger from context because the SMTLIB scripting language provides option
   * to configure its own, as well as standard defaults. How to make it more configurable by still
   * using the context ?
   */

  private var logic: Option[Logic] = None

  private var funSymbols: Map[String, FunctionSymbol] = Map()
  private var predSymbols: Map[String, PredicateSymbol] = Map()

  private val solver = new cafesat.Solver
  private var expectedResult: Option[Boolean] = None

  private var regularOutput: PrintStream = System.out
  private var regularOutputClosable: Option[PrintStream] = None
  private var loggingOutput: PrintStream = System.err
  private var loggingOutputClosable: Option[PrintStream] = None
  private var loggingLevel: Logger.LogLevel = Logger.Warning

  private var printSuccess: Boolean = false

  //make a new logger according to current SMT options
  private val logger = new Logger {
    override def output(msg: String): Unit = loggingOutput.println(msg)

    override def logLevel: Logger.LogLevel = loggingLevel
  }
  private implicit val tag = Logger.Tag("SMTLIB Interpreter")


  def eval(command: Command): CommandResponse = {
    logger.info("Evaluating command: " + command)
    val res = command match {
      case SetLogic(log) => logic match {
        case Some(l) => Error("Logic already set to: " + l)
        case None => {
          log match {
            case QF_UF => 
              logic = Some(QF_UF)
              Success
            case l =>
              logger.warning("Unsupported logic: " + l)
              Unsupported
          }
        }
      }
      case DeclareSort(SSymbol(name), arity) => Success
      case DeclareFun(SSymbol(name), sorts, sort) => {
        val paramSorts = sorts map parseSort
        val returnSort = parseSort(sort)
        if(returnSort == TSort("BOOL", List()))
          predSymbols += (name -> PredicateSymbol(name, paramSorts.toList))
        else
          funSymbols += (name -> FunctionSymbol(name, paramSorts.toList, returnSort))
        Success
      }
      case Pop(n) => {
        try {
          solver.pop(n)
          Success
        } catch {
          case (e: Exception) => Error("Cannot pop " + n + " scope frames")
        }
      }
      case Push(n) => {
        (1 to n).foreach(_ => solver.push())
        Success
      }
      case Assert(f) => {
{'fraction_non_alphanumeric': 0.08999691262735413, 'fraction_numerical': 0.0006174745291756715, 'mean_word_length': 3.113650793650794, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 36, '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': '927093', 'n_tokens_mistral': 1837, 'n_tokens_neox': 1813, 'n_words': 623}