[smt] make SMTLib + Btor2 emitters public objects (#2326)

This will make it easier for formal verification
libraries to make use of these emitters.

1 files changed, 4 insertions, 12 deletions

diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
index ca472578..cc6a3e8a 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
@@ -22,14 +22,6 @@ private[firrtl] abstract class SMTEmitter private[firrtl] ()
 
   protected def serialize(sys: TransitionSystem): Annotation
 
-  private val BleedingEdgeWarning =
-    """WARNING: The SMT and BTOR2 emitters are experimental preview features.
-      |- they might be removed in future versions without deprecation warning
-      |- their behavior and interfaces might change without notice
-      |- they are unsupported, we won't be able to fix any issues you find in them
-      |- however, we do accept pull requests: https://github.com/freechipsproject/firrtl/pulls
-      |""".stripMargin
-
   override protected def execute(state: CircuitState): CircuitState = {
     val emitCircuit = state.annotations.exists {
       case EmitCircuitAnnotation(a) if this.getClass == a    => true
@@ -39,8 +31,6 @@ private[firrtl] abstract class SMTEmitter private[firrtl] ()
 
     if (!emitCircuit) { return state }
 
-    logger.warn(BleedingEdgeWarning)
-
     val sys = state.annotations.collectFirst { case TransitionSystemAnnotation(sys) => sys }.getOrElse {
       error("Could not find the transition system!")
     }
@@ -62,7 +52,8 @@ case class EmittedSMTModelAnnotation(name: String, src: String, outputSuffix: St
   override def getBytes:         Iterable[Byte] = src.getBytes
 }
 
-private[firrtl] class Btor2Emitter extends SMTEmitter {
+/** Turns the transition system generated by [[FirrtlToTransitionSystem]] into a btor2 file. */
+object Btor2Emitter extends SMTEmitter {
   override def outputSuffix: String = ".btor2"
   override protected def serialize(sys: TransitionSystem): Annotation = {
     val btor = generatedHeader("BTOR", sys.name) + Btor2Serializer.serialize(sys).mkString("\n") + "\n"
@@ -70,7 +61,8 @@ private[firrtl] class Btor2Emitter extends SMTEmitter {
   }
 }
 
-private[firrtl] class SMTLibEmitter extends SMTEmitter {
+/** Turns the transition system generated by [[FirrtlToTransitionSystem]] into an SMTLib file. */
+object SMTLibEmitter extends SMTEmitter {
   override def outputSuffix: String = ".smt2"
   override protected def serialize(sys: TransitionSystem): Annotation = {
     val hasMemory = sys.states.exists(_.sym.isInstanceOf[ArrayExpr])