Concrete cvc4 and z3 solvers

src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala

 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package solvers
 package smtlib
 
-import OptionParsers._
+class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions)
+  extends SMTLIBSolver
+     with SMTLIBCVC4Target {
 
-import solvers.theories._
-import purescala.Definitions.Program
-
-class SMTLIBCVC4Solver(context: SolverContext, program: Program)
-  extends SMTLIBSolver(context, program, new BagEncoder(context.context, program) >> new ArrayEncoder(context.context, program))
-     with SMTLIBCVC4Target
-     with cvc4.CVC4Solver {
-
-  def targetName = "cvc4"
-
-  def userDefinedOps(ctx: LeonContext) = {
-    ctx.findOptionOrDefault(SMTLIBCVC4Component.optCVC4Options)
-  }
-
-  def interpreterOps(ctx: LeonContext) = {
+  def interpreterOps(ctx: InoxContext) = {
     Seq(
       "-q",
       "--produce-models",
       "--incremental",
-//      "--no-incremental",
-//      "--tear-down-incremental",
-//      "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs
+      // "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs
       "--rewrite-divk",
       "--print-success",
       "--lang", "smt2.5"
-    ) ++ userDefinedOps(ctx).toSeq
+    )
   }
 }
-
-object SMTLIBCVC4Component extends LeonComponent {
-  val name = "CVC4 solver"
-
-  val description = "Solver invoked with --solvers=smt-cvc4"
-
-  val optCVC4Options = new LeonOptionDef[Set[String]] {
-    val name = "solver:cvc4"
-    val description = "Pass extra arguments to CVC4"
-    val default = Set[String]()
-    val parser = setParser(stringParser)
-    val usageRhs = "<cvc4-opt>"
-  }
-
-  override val definedOptions : Set[LeonOptionDef[Any]] = Set(optCVC4Options)
-}

src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala

 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package solvers
 package smtlib
 
-import purescala.Definitions.Program
-import purescala.Common.Identifier
-import purescala.Expressions.Expr
-
-import _root_.smtlib.parser.Terms.{Identifier => _, _}
-import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
-import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
-import _root_.smtlib.theories.Core.{Equals => _, _}
-
-import theories._
-
-class SMTLIBZ3Solver(sctx: SolverContext, program: Program)
-  extends SMTLIBSolver(sctx, program, new StringEncoder(sctx.context, program) >> new ArrayEncoder(sctx.context, program))
+class SMTLIBZ3Solver(val program: Program, val options: SolverOptions)
+  extends SMTLIBSolver
      with SMTLIBZ3Target
-     with z3.Z3Solver