From 3184042f41fb1baf57dc95d4d6d35e92df745e5a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 8 Aug 2016 14:02:52 +0200
Subject: [PATCH] Concrete cvc4 and z3 solvers
---
.../solvers/smtlib/SMTLIBCVC4Solver.scala | 44 +++----------------
.../inox/solvers/smtlib/SMTLIBZ3Solver.scala | 18 ++------
2 files changed, 10 insertions(+), 52 deletions(-)
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
index bf1050680..16311ecbf 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -1,52 +1,22 @@
/* 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)
-}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala
index e49b29721..223097df4 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -1,21 +1,9 @@
/* 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
--
GitLab