<commit_before>package regolic.smt

import regolic.asts.core.Trees._
import regolic.asts.core.Manip._
import regolic.asts.fol.Trees._
import regolic.asts.fol.Manip._
import regolic.parsers.SmtLib2.Trees._

import regolic.smt.qfeuf.CongruenceSolver
import regolic.smt.qfeuf.CongruenceClosure
import regolic.smt.qfeuf.FastCongruenceSolver
import regolic.smt.qflra.SimplexSolver

import regolic.dpllt.LazyBasicSolver
import regolic.dpllt.DPLLTSolverWrapper

trait TheorySolver {

  val logic: Logic
    
  def initialize(ls: Set[Formula]): Unit

  def isTrue(l: Formula): Boolean

  def backtrack(n: Int): Unit

  def explain(l: Formula, lPrime: Formula): Set[Formula]

  def setTrue(l: Formula): Option[Set[Formula]]
  
}

object TheorySolver {

  val allSolvers: List[TheorySolver] = List() // TODO wrapper object for congruence closure

  def execute(cmds: List[Command]) {
    println("Executing following script: " + cmds)
    var solver: Option[TheorySolver] = None
    var asserts: List[Formula] = List(True())

    for(cmd <- cmds) {
      cmd match {
        case SetLogic(logic) => solver = getSolver(logic)
        case Pop(n) => {
          asserts = asserts.tail
        }
        case Push(n) => {
          asserts ::= True()
        }
        case Assert(f) => {
          asserts = And(f, asserts.head) :: asserts.tail
        }
        case CheckSat => {
          val formula = simplify(asserts.foldLeft(True(): Formula)((acc, f) => And(acc, f)))
          //println("isSat: "+ FastCongruenceSolver.isSat(formula))
          val cc = new CongruenceClosure
          //println("isSat: " + DPLLTSolverWrapper(solver.get, formula))
          println("isSat: " + DPLLTSolverWrapper(cc, formula))
        }
        case Exit => {
          // TODO
        }
      }
    }

  }


  def getSolver(logic: Logic): Option[TheorySolver] = allSolvers.find(_.logic == logic)
<commit_msg>Added support for set-info in theory solver<commit_after>package regolic.smt

import regolic.asts.core.Trees._
import regolic.asts.core.Manip._
import regolic.asts.fol.Trees._
import regolic.asts.fol.Manip._
import regolic.parsers.SmtLib2.Trees._

import regolic.smt.qfeuf.CongruenceSolver
import regolic.smt.qfeuf.CongruenceClosure
import regolic.smt.qfeuf.FastCongruenceSolver
import regolic.smt.qflra.SimplexSolver

import regolic.dpllt.LazyBasicSolver
import regolic.dpllt.DPLLTSolverWrapper
import regolic.dpllt.Results._

import regolic.sexpr.SExprs._

trait TheorySolver {

  val logic: Logic
    
  def initialize(ls: Set[Formula]): Unit

  def isTrue(l: Formula): Boolean

  def backtrack(n: Int): Unit

  def explain(l: Formula, lPrime: Formula): Set[Formula]

  def setTrue(l: Formula): Option[Set[Formula]]
  
}

object TheorySolver {

  val allSolvers: List[TheorySolver] = List() // TODO wrapper object for congruence closure

  def execute(cmds: List[Command]) {
    var solver: Option[TheorySolver] = None
    var asserts: List[Formula] = List(True())

    var expectedResult: Option[Boolean] = None

    for(cmd <- cmds) {
      cmd match {
        case SetLogic(logic) => solver = getSolver(logic)
        case Pop(n) => {
          asserts = asserts.tail
        }
        case Push(n) => {
          asserts ::= True()
        }
        case Assert(f) => {
          asserts = And(f, asserts.head) :: asserts.tail
        }
        case CheckSat => {
          val formula = simplify(asserts.foldLeft(True(): Formula)((acc, f) => And(acc, f)))
          val cc = new CongruenceClosure
          val result = DPLLTSolverWrapper(cc, formula)

          val resultString = result match {
            case Satisfiable(_) if expectedResult == Some(false) => "sat | should be unsat"
            case Satisfiable(_) => "sat"
            case Unsatisfiable if expectedResult == Some(true) => "unsat | should be sat"
            case Unsatisfiable => "unsat"
          }
          println(resultString)
        }
        case SetInfo(attr) => {
          attr match {
            case Attribute("STATUS", Some(SSymbol("SAT"))) => expectedResult = Some(true)
            case Attribute("STATUS", Some(SSymbol("UNSAT"))) => expectedResult = Some(false)
            case Attribute("STATUS", _) => {
              println("WARNING: set-info status set to unsupported value")
              expectedResult = None
            }
            // TODO
            case Attribute("SOURCE", Some(SSymbol(src))) => ()
            case Attribute("SMT-LIB-VERSION", Some(SDouble(ver))) => ()
            case Attribute("CATEGORY", Some(SString(cat))) => ()
            case _ => println("WARNING: unsupported set-info attribute")
          }
        }
        case Exit => {
          // TODO
          sys.exit()
        }
      }
    }

  }


  def getSolver(logic: Logic): Option[TheorySolver] = allSolvers.find(_.logic == logic)

{'fraction_non_alphanumeric': 0.12079701120797011, 'fraction_numerical': 0.00041511000415110004, 'mean_word_length': 2.6260346124905944, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 29, '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': '816266', 'n_tokens_mistral': 1602, 'n_tokens_neox': 1509, 'n_words': 336}