From 949f4d40d9e9e1fde4a57acac1ebdd4196373e6b Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Mon, 8 Aug 2016 14:49:50 +0200 Subject: [PATCH] Remove prefix from SMTLIB solvers --- .../smtlib/{SMTLIBCVC4Solver.scala => CVC4Solver.scala} | 4 ++-- .../smtlib/{SMTLIBCVC4Target.scala => CVC4Target.scala} | 2 +- .../solvers/smtlib/{SMTLIBZ3Solver.scala => Z3Solver.scala} | 4 ++-- .../solvers/smtlib/{SMTLIBZ3Target.scala => Z3Target.scala} | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) rename src/main/scala/inox/solvers/smtlib/{SMTLIBCVC4Solver.scala => CVC4Solver.scala} (88%) rename src/main/scala/inox/solvers/smtlib/{SMTLIBCVC4Target.scala => CVC4Target.scala} (99%) rename src/main/scala/inox/solvers/smtlib/{SMTLIBZ3Solver.scala => Z3Solver.scala} (53%) rename src/main/scala/inox/solvers/smtlib/{SMTLIBZ3Target.scala => Z3Target.scala} (99%) diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala similarity index 88% rename from src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala rename to src/main/scala/inox/solvers/smtlib/CVC4Solver.scala index 8bea481be..02306d219 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala +++ b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala @@ -6,9 +6,9 @@ package smtlib import inox.OptionParsers._ -class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions) +class CVC4Solver(val program: Program, val options: SolverOptions) extends SMTLIBSolver - with SMTLIBCVC4Target { + with CVC4Target { protected val userDefinedOps = { options.findOptionOrDefault(optCVC4Options) diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala similarity index 99% rename from src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala rename to src/main/scala/inox/solvers/smtlib/CVC4Target.scala index a263a3042..3936ea873 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala +++ b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala @@ -12,7 +12,7 @@ import _root_.smtlib.interpreters.CVC4Interpreter import _root_.smtlib.theories.experimental.Sets import _root_.smtlib.theories.experimental.Strings -trait SMTLIBCVC4Target extends SMTLIBTarget { +trait CVC4Target extends SMTLIBTarget { import program._ import trees._ import symbols._ diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/inox/solvers/smtlib/Z3Solver.scala similarity index 53% rename from src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala rename to src/main/scala/inox/solvers/smtlib/Z3Solver.scala index 223097df4..64b5b127f 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala +++ b/src/main/scala/inox/solvers/smtlib/Z3Solver.scala @@ -4,6 +4,6 @@ package inox package solvers package smtlib -class SMTLIBZ3Solver(val program: Program, val options: SolverOptions) +class Z3Solver(val program: Program, val options: SolverOptions) extends SMTLIBSolver - with SMTLIBZ3Target + with Z3Target diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/inox/solvers/smtlib/Z3Target.scala similarity index 99% rename from src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala rename to src/main/scala/inox/solvers/smtlib/Z3Target.scala index d08689741..2a59c4a97 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala +++ b/src/main/scala/inox/solvers/smtlib/Z3Target.scala @@ -10,7 +10,7 @@ import _root_.smtlib.interpreters.Z3Interpreter import _root_.smtlib.theories.Core.{Equals => SMTEquals, _} import _root_.smtlib.theories._ -trait SMTLIBZ3Target extends SMTLIBTarget { +trait Z3Target extends SMTLIBTarget { import program._ import trees._ -- GitLab