From 3940322733426e5db54f575cf4101d9bd6943dc1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 11 May 2015 16:51:16 +0200
Subject: [PATCH] No point in naming them Targets if they are Solvers.
---
src/main/scala/leon/solvers/SolverFactory.scala | 12 ++++++------
...et.scala => SMTLIBCVC4CounterExampleSolver.scala} | 2 +-
...ProofTarget.scala => SMTLIBCVC4ProofSolver.scala} | 2 +-
...Target.scala => SMTLIBCVC4QuantifiedSolver.scala} | 2 +-
...SMTLIBCVC4Target.scala => SMTLIBCVC4Solver.scala} | 2 +-
...edTarget.scala => SMTLIBZ3QuantifiedSolver.scala} | 2 +-
.../{SMTLIBZ3Target.scala => SMTLIBZ3Solver.scala} | 2 +-
7 files changed, 12 insertions(+), 12 deletions(-)
rename src/main/scala/leon/solvers/smtlib/{SMTLIBCVC4CounterExampleTarget.scala => SMTLIBCVC4CounterExampleSolver.scala} (73%)
rename src/main/scala/leon/solvers/smtlib/{SMTLIBCVC4ProofTarget.scala => SMTLIBCVC4ProofSolver.scala} (79%)
rename src/main/scala/leon/solvers/smtlib/{SMTLIBCVC4QuantifiedTarget.scala => SMTLIBCVC4QuantifiedSolver.scala} (96%)
rename src/main/scala/leon/solvers/smtlib/{SMTLIBCVC4Target.scala => SMTLIBCVC4Solver.scala} (99%)
rename src/main/scala/leon/solvers/smtlib/{SMTLIBZ3QuantifiedTarget.scala => SMTLIBZ3QuantifiedSolver.scala} (93%)
rename src/main/scala/leon/solvers/smtlib/{SMTLIBZ3Target.scala => SMTLIBZ3Solver.scala} (99%)
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index fec39a7c1..31056406c 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -77,19 +77,19 @@ object SolverFactory {
SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
case "smt-z3" =>
- SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBZ3Target(ctx, program)) with TimeoutSolver)
+ SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
case "smt-z3-q" =>
- SolverFactory(() => new SMTLIBZ3QuantifiedTarget(ctx, program) with TimeoutSolver)
+ SolverFactory(() => new SMTLIBZ3QuantifiedSolver(ctx, program) with TimeoutSolver)
case "smt-cvc4" =>
- SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBCVC4Target(ctx, program)) with TimeoutSolver)
+ SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBCVC4Solver(ctx, program)) with TimeoutSolver)
case "smt-cvc4-proof" =>
- SolverFactory(() => new SMTLIBCVC4ProofTarget(ctx, program) with TimeoutSolver)
+ SolverFactory(() => new SMTLIBCVC4ProofSolver(ctx, program) with TimeoutSolver)
case "smt-cvc4-cex" =>
- SolverFactory(() => new SMTLIBCVC4CounterExampleTarget(ctx, program) with TimeoutSolver)
+ SolverFactory(() => new SMTLIBCVC4CounterExampleSolver(ctx, program) with TimeoutSolver)
case _ =>
ctx.reporter.error(s"Unknown solver $name")
@@ -127,7 +127,7 @@ object SolverFactory {
ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-based solver.")
reported = true
}
- SolverFactory(() => new SMTLIBZ3Target(ctx, program) with TimeoutSolver)
+ SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
similarity index 73%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index d3e9c0008..6a42646e6 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
@@ -5,7 +5,7 @@ package solvers.smtlib
import purescala.Definitions.Program
-class SMTLIBCVC4CounterExampleTarget(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedTarget(context, program) {
+class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
override val targetName = "cvc4-cex"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
similarity index 79%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 4d6b4d1ca..32bc12b4e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -5,7 +5,7 @@ package solvers.smtlib
import leon.purescala.Definitions.Program
-class SMTLIBCVC4ProofTarget(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedTarget(context, program) {
+class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
override val targetName = "cvc4-proof"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
similarity index 96%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 9ac752c74..f5de0bb34 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -14,7 +14,7 @@ import smtlib.theories.Core.Equals
// This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
// It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
-abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program) extends SMTLIBCVC4Target(context, program) {
+abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBCVC4Solver(context, program) {
override val targetName = "cvc4-quantified"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
similarity index 99%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 80930ba43..69d12b686 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -19,7 +19,7 @@ import _root_.smtlib.parser.Commands._
import _root_.smtlib.interpreters.CVC4Interpreter
import _root_.smtlib.theories._
-class SMTLIBCVC4Target(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) {
+class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) {
def targetName = "cvc4"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
similarity index 93%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index 041f52260..7e8dd0673 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -13,7 +13,7 @@ import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol}
* This solver models function definitions as universally quantified formulas.
* It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
*/
-class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends SMTLIBZ3Target(context, program) {
+class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBZ3Solver(context, program) {
private val typedFunDefExplorationLimit = 10000
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
similarity index 99%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index d7565c8d5..1fb33303f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -20,7 +20,7 @@ import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
import _root_.smtlib.theories.ArraysEx
-class SMTLIBZ3Target(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) {
+class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) {
def targetName = "z3"
--
GitLab