From 63d1716c11482306f6cb08d50500b9abdc55b43b Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Wed, 28 Aug 2024 00:12:16 +0200
Subject: [PATCH] Not collecting axioms and declarations unless necessary, and
 resetting properly

---
 src/main/scala/decider/ProverStdIO.scala       |  9 +++++++--
 src/main/scala/decider/Z3ProverAPI.scala       | 10 +++++-----
 src/main/scala/interfaces/decider/Prover.scala |  5 ++++-
 3 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/main/scala/decider/ProverStdIO.scala b/src/main/scala/decider/ProverStdIO.scala
index 1422047a..e86e7227 100644
--- a/src/main/scala/decider/ProverStdIO.scala
+++ b/src/main/scala/decider/ProverStdIO.scala
@@ -177,6 +177,8 @@ abstract class ProverStdIO(uniqueId: String,
         Runtime.getRuntime.removeShutdownHook(proverShutdownHook)
         proverShutdownHook = null
       }
+      allDecls = Seq()
+      allEmits = Seq()
     }
   }
 
@@ -196,7 +198,9 @@ abstract class ProverStdIO(uniqueId: String,
   }
 
   def emit(content: String): Unit = {
-    allEmits :+= content
+    if (debugMode) {
+      allEmits :+= content
+    }
     writeLine(content)
     readSuccess()
   }
@@ -403,7 +407,8 @@ abstract class ProverStdIO(uniqueId: String,
 
   def declare(decl: Decl): Unit = {
     val str = termConverter.convert(decl)
-    allDecls = allDecls :+ decl
+    if (debugMode)
+      allDecls = allDecls :+ decl
     emit(str)
   }
 
diff --git a/src/main/scala/decider/Z3ProverAPI.scala b/src/main/scala/decider/Z3ProverAPI.scala
index 8cc81a65..5ddc2839 100644
--- a/src/main/scala/decider/Z3ProverAPI.scala
+++ b/src/main/scala/decider/Z3ProverAPI.scala
@@ -92,7 +92,6 @@ class Z3ProverAPI(uniqueId: String,
   val emittedFuncs = mutable.LinkedHashSet[FuncDecl]()
   val emittedFuncSymbols = mutable.Queue[Symbol]()
   var allDecls: Seq[Decl] = Seq()
-  var allEmits: Seq[String] = Seq()
 
   // If true, we do not define macros on the Z3 level, but perform macro expansion ourselves on Silicon Terms.
   // Otherwise, we define a function on the Z3 level and axiomatize it according to the macro definition.
@@ -186,6 +185,7 @@ class Z3ProverAPI(uniqueId: String,
     emittedSorts.clear()
     emittedFuncSymbols.clear()
     emittedSortSymbols.clear()
+    allDecls = Seq()
   }
 
   def reset(): Unit = {
@@ -196,6 +196,7 @@ class Z3ProverAPI(uniqueId: String,
 
   def stop(): Unit = {
     emittedPreambleString.clear()
+    allDecls = Seq()
     preamblePhaseOver = false
     emittedFuncs.clear()
     emittedSorts.clear()
@@ -232,7 +233,6 @@ class Z3ProverAPI(uniqueId: String,
     if (preamblePhaseOver) {
       sys.error("emitting phase over")
     }
-    allEmits :+= content
     emittedPreambleString.append(content)
   }
 
@@ -240,11 +240,10 @@ class Z3ProverAPI(uniqueId: String,
     if (preamblePhaseOver) {
       sys.error("emitting phase over")
     }
-    allEmits ++= contents
     emittedPreambleString.appendAll(contents)
   }
 
-  def getAllEmits(): Seq[String] = allEmits
+  def getAllEmits(): Seq[String] = emittedPreambleString.toSeq
 
   override def emitSettings(contents: Iterable[String]): Unit = {
     // we ignore this, don't know any better solution atm.
@@ -448,7 +447,8 @@ class Z3ProverAPI(uniqueId: String,
     // current state) and record it in out collection(s) of emmitted declarations.
     // Special handling for macro declarations if expandMacros is true; in that case,
     // nothing is declared on the Z3 level, and we simply remember the definition ourselves.
-    allDecls = allDecls :+ decl
+    if (debugMode)
+      allDecls = allDecls :+ decl
     decl match {
       case SortDecl(s) =>
         val convertedSort = termConverter.convertSort(s)
diff --git a/src/main/scala/interfaces/decider/Prover.scala b/src/main/scala/interfaces/decider/Prover.scala
index 1827c4a2..8c881b1e 100644
--- a/src/main/scala/interfaces/decider/Prover.scala
+++ b/src/main/scala/interfaces/decider/Prover.scala
@@ -12,6 +12,7 @@ import viper.silicon.common.config.Version
 import viper.silver.components.StatefulComponent
 import viper.silicon.{Config, Map}
 import viper.silicon.state.terms._
+import viper.silicon.verifier.Verifier
 import viper.silver.verifier.Model
 
 sealed abstract class Result
@@ -21,12 +22,14 @@ object Unknown extends Result
 
 /* TODO: Should be generic, not hardcoded to Strings */
 trait ProverLike {
+  protected val debugMode = Verifier.config.enableDebugging()
   var preambleAssumptions: Seq[DebugAxiom] = Seq()
   def emit(content: String): Unit
   def emit(contents: Iterable[String]): Unit = { contents foreach emit }
   def emitSettings(contents: Iterable[String]): Unit
   def assumeAxioms(terms: InsertionOrderedSet[Term], description: String): Unit = {
-    preambleAssumptions :+= new DebugAxiom(description, terms)
+    if (debugMode)
+      preambleAssumptions :+= new DebugAxiom(description, terms)
     terms foreach assume
   }
   def setOption(name: String, value: String): String