From 6bfc8a045497cec31d55fc6fcfb4115c861800ad Mon Sep 17 00:00:00 2001
From: Lea Salome Brugger <leasalome.brugger@inf.ethz.ch>
Date: Mon, 8 Jul 2024 16:36:51 +0200
Subject: [PATCH] Remove refute transformer

---
 .../viper/gobra/translator/Translator.scala   |  5 ++-
 .../transformers/RefuteTransformer.scala      | 32 -------------------
 2 files changed, 2 insertions(+), 35 deletions(-)
 delete mode 100644 src/main/scala/viper/gobra/translator/transformers/RefuteTransformer.scala

diff --git a/src/main/scala/viper/gobra/translator/Translator.scala b/src/main/scala/viper/gobra/translator/Translator.scala
index 7fb3e0369..cb20b5d9a 100644
--- a/src/main/scala/viper/gobra/translator/Translator.scala
+++ b/src/main/scala/viper/gobra/translator/Translator.scala
@@ -13,7 +13,7 @@ import viper.gobra.frontend.{Config, PackageInfo}
 import viper.gobra.reporting.{ConsistencyError, GeneratedViperMessage, TransformerFailureMessage, VerifierError}
 import viper.gobra.translator.context.DfltTranslatorConfig
 import viper.gobra.translator.encodings.programs.ProgramsImpl
-import viper.gobra.translator.transformers.{AssumeTransformer, RefuteTransformer, TerminationDomainTransformer, ViperTransformer}
+import viper.gobra.translator.transformers.{AssumeTransformer, TerminationDomainTransformer, ViperTransformer}
 import viper.gobra.util.Violation
 import viper.silver.ast.{AbstractSourcePosition, SourcePosition}
 import viper.silver.ast.pretty.FastPrettyPrinter
@@ -38,8 +38,7 @@ object Translator {
 
     val transformers: Seq[ViperTransformer] = Seq(
       new AssumeTransformer,
-      new TerminationDomainTransformer,
-      new RefuteTransformer
+      new TerminationDomainTransformer
     )
 
     val transformedTask = transformers.foldLeft[Either[Vector[VerifierError], BackendVerifier.Task]](Right(task)) {
diff --git a/src/main/scala/viper/gobra/translator/transformers/RefuteTransformer.scala b/src/main/scala/viper/gobra/translator/transformers/RefuteTransformer.scala
deleted file mode 100644
index c6e25bfb3..000000000
--- a/src/main/scala/viper/gobra/translator/transformers/RefuteTransformer.scala
+++ /dev/null
@@ -1,32 +0,0 @@
-// This Source Code Form is subject to the terms of the Mozilla Public
-// License, v. 2.0. If a copy of the MPL was not distributed with this
-// file, You can obtain one at http://mozilla.org/MPL/2.0/.
-//
-// Copyright (c) 2011-2021 ETH Zurich.
-
-package viper.gobra.translator.transformers
-
-import viper.gobra.backend.BackendVerifier
-import viper.silver.plugin.SilverPlugin
-import viper.silver.plugin.standard.refute.RefutePlugin
-import viper.silver.verifier.AbstractError
-import viper.silver.{ast => vpr}
-
-class RefuteTransformer extends ViperTransformer {
-  override def transform(task: BackendVerifier.Task): Either[Seq[AbstractError], BackendVerifier.Task] = {
-    def applyPlugin(plugin: SilverPlugin, prog: vpr.Program): Either[Seq[AbstractError], vpr.Program] = {
-      val transformedProgram = plugin.beforeVerify(prog)
-      if (plugin.errors.isEmpty) {
-        Right(transformedProgram)
-      } else {
-        Left(plugin.errors)
-      }
-    }
-
-    val refutePlugin = new RefutePlugin(null, null, null, null)
-
-    for {
-      transformedProgram <- applyPlugin(refutePlugin, task.program)
-    } yield task.copy(program = transformedProgram)
-  }
-}