From d7579cef1e544f03360b7e2d67bd38d61dd48801 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 8 Aug 2016 14:16:18 +0200
Subject: [PATCH] Add user options to CVC4
---
src/main/scala/inox/solvers/Solver.scala | 1 -
.../inox/solvers/smtlib/SMTLIBCVC4Solver.scala | 16 +++++++++++++++-
2 files changed, 15 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index 5b71c1854..c85ed8688 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -4,7 +4,6 @@ package inox
package solvers
import utils._
-import evaluators._
case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[SolverOptions] {
def build(opts: Seq[InoxOption[Any]]): SolverOptions = SolverOptions(opts)
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
index 16311ecbf..8bea481be 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -4,10 +4,16 @@ package inox
package solvers
package smtlib
+import inox.OptionParsers._
+
class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions)
extends SMTLIBSolver
with SMTLIBCVC4Target {
+ protected val userDefinedOps = {
+ options.findOptionOrDefault(optCVC4Options)
+ }
+
def interpreterOps(ctx: InoxContext) = {
Seq(
"-q",
@@ -17,6 +23,14 @@ class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions)
"--rewrite-divk",
"--print-success",
"--lang", "smt2.5"
- )
+ ) ++ userDefinedOps.toSeq
}
}
+
+object optCVC4Options extends InoxOptionDef[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>"
+}
--
GitLab