/*
 * Copyright (C) 2018-2024 University of Waterloo.
 *
 * This file is part of Perses.
 *
 * Perses is free software; you can redistribute it and/or modify it under the
 * terms of the GNU General Public License as published by the Free Software
 * Foundation; either version 3, or (at your option) any later version.
 *
 * Perses is distributed in the hope that it will be useful, but WITHOUT ANY
 * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
 * FOR A PARTICULAR PURPOSE.  See the GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License along with
 * Perses; see the file LICENSE.  If not see <http://www.gnu.org/licenses/>.
 */
package org.perses.grammar.smtlibv2

import com.google.common.truth.Truth.assertThat
import org.junit.Test
import org.junit.runner.RunWith
import org.junit.runners.JUnit4
import org.perses.TestUtility
import org.perses.antlr.ParseTreeWithParser

@RunWith(JUnit4::class)
class PnfSmtLibv2ParserFacadeTest {

  @Test
  fun test() {
    val pnfFacade = SmtLibV2ParserFacade()
    val origFacade = OrigSmtLibV2ParserFacade()
    val programs = TestUtility.smtTestFiles
    for (program in programs) {
      val parseTree = pnfFacade.parseFile(program)
      val pnfTokens = TestUtility.extractTokenTexts(parseTree.tree)
      val programFromFile = TestUtility.createSparTreeFromFile(program.fileName)
      assertThat(pnfTokens).isNotEmpty()
      assertThat(programFromFile).isNotNull()

      val origParseTree: ParseTreeWithParser = origFacade.parseFile(program)
      val origTokens = TestUtility.extractTokenTexts(origParseTree.tree)
      assertThat(origTokens).isEqualTo(pnfTokens)
    }
  }
}
