Skip to content
Snippets Groups Projects
Commit d7579cef authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Add user options to CVC4

parent 1b65df8f
No related branches found
No related tags found
No related merge requests found
...@@ -4,7 +4,6 @@ package inox ...@@ -4,7 +4,6 @@ package inox
package solvers package solvers
import utils._ import utils._
import evaluators._
case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[SolverOptions] { case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[SolverOptions] {
def build(opts: Seq[InoxOption[Any]]): SolverOptions = SolverOptions(opts) def build(opts: Seq[InoxOption[Any]]): SolverOptions = SolverOptions(opts)
......
...@@ -4,10 +4,16 @@ package inox ...@@ -4,10 +4,16 @@ package inox
package solvers package solvers
package smtlib package smtlib
import inox.OptionParsers._
class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions) class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions)
extends SMTLIBSolver extends SMTLIBSolver
with SMTLIBCVC4Target { with SMTLIBCVC4Target {
protected val userDefinedOps = {
options.findOptionOrDefault(optCVC4Options)
}
def interpreterOps(ctx: InoxContext) = { def interpreterOps(ctx: InoxContext) = {
Seq( Seq(
"-q", "-q",
...@@ -17,6 +23,14 @@ class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions) ...@@ -17,6 +23,14 @@ class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions)
"--rewrite-divk", "--rewrite-divk",
"--print-success", "--print-success",
"--lang", "smt2.5" "--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>"
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment