/* Copyright 2009-2015 EPFL, Lausanne */

package leon.regression
package verification

import leon._
import leon.verification.AnalysisPhase

import _root_.smtlib.interpreters._

// If you add another regression test, make sure it contains one object whose name matches the file name
// This is because we compile all tests from each folder separately.
class PureScalaVerificationSuite extends VerificationSuite {
  
  val testDir = "regression/verification/purescala/"
  val pipeFront = xlang.NoXLangFeaturesChecking
  val pipeBack = AnalysisPhase

  override val ignored = Seq(
    "verification/purescala/valid/Nested15.scala",
    "verification/purescala/invalid/Nested15.scala"
  )

  val optionVariants: List[List[String]] = {
    val isZ3Available = try {
      Z3Interpreter.buildDefault.free()
      true
    } catch {
      case e: java.io.IOException =>
        false
    }

    val isCVC4Available = try {
      CVC4Interpreter.buildDefault.free()
      true
    } catch {
      case e: java.io.IOException =>
        false
    }

    List(
      List("--feelinglucky"),
      List("--codegen", "--evalground", "--feelinglucky"),
      List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
    ) ++ (
      if (isZ3Available) List(
        List("--solvers=smt-z3", "--feelinglucky")
      ) else Nil
    ) ++ (
      if (isCVC4Available) List(
        List("--solvers=smt-cvc4", "--feelinglucky")
      ) else Nil
    )
  }

}