smt: make SMT + TransitionSystem lib public (#2350)

8 files changed, 79 insertions, 80 deletions

diff --git a/src/main/scala/firrtl/backends/experimental/smt/Btor2Serializer.scala b/src/main/scala/firrtl/backends/experimental/smt/Btor2Serializer.scala
index a6eaa51b..37f9228f 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/Btor2Serializer.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/Btor2Serializer.scala
@@ -5,7 +5,7 @@ package firrtl.backends.experimental.smt
 
 import scala.collection.mutable
 
-private object Btor2Serializer {
+object Btor2Serializer {
   def serialize(sys: TransitionSystem, skipOutput: Boolean = false): Iterable[String] = {
     new Btor2Serializer().run(sys, skipOutput)
   }
diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
index c5fff849..7da2e1e6 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/FirrtlToTransitionSystem.scala
@@ -17,7 +17,7 @@ import logger.LazyLogging
 
 import scala.collection.mutable
 
-private case class TransitionSystemAnnotation(sys: TransitionSystem) extends NoTargetAnnotation
+case class TransitionSystemAnnotation(sys: TransitionSystem) extends NoTargetAnnotation
 
 /** Contains code to convert a flat firrtl module into a functional transition system which
   * can then be exported as SMTLib or Btor2 file.
diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala
index 21a64f98..7b332b83 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/SMTCommand.scala
@@ -3,10 +3,10 @@
 
 package firrtl.backends.experimental.smt
 
-private sealed trait SMTCommand
-private case class Comment(msg: String) extends SMTCommand
-private case class SetLogic(logic: String) extends SMTCommand
-private case class DefineFunction(name: String, args: Seq[SMTFunctionArg], e: SMTExpr) extends SMTCommand
-private case class DeclareFunction(sym: SMTSymbol, args: Seq[SMTFunctionArg]) extends SMTCommand
-private case class DeclareUninterpretedSort(name: String) extends SMTCommand
-private case class DeclareUninterpretedSymbol(name: String, tpe: String) extends SMTCommand
+sealed trait SMTCommand
+case class Comment(msg: String) extends SMTCommand
+case class SetLogic(logic: String) extends SMTCommand
+case class DefineFunction(name: String, args: Seq[SMTFunctionArg], e: SMTExpr) extends SMTCommand
+case class DeclareFunction(sym: SMTSymbol, args: Seq[SMTFunctionArg]) extends SMTCommand
+case class DeclareUninterpretedSort(name: String) extends SMTCommand
+case class DeclareUninterpretedSymbol(name: String, tpe: String) extends SMTCommand
diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
index cc6a3e8a..45ec6898 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/SMTEmitter.scala
@@ -66,13 +66,14 @@ object SMTLibEmitter extends SMTEmitter {
   override def outputSuffix: String = ".smt2"
   override protected def serialize(sys: TransitionSystem): Annotation = {
     val hasMemory = sys.states.exists(_.sym.isInstanceOf[ArrayExpr])
-    val logic = SMTLibSerializer.setLogic(hasMemory) + "\n"
+    val logic = if (hasMemory) "QF_AUFBV" else "QF_UFBV"
+    val logicCmd = SMTLibSerializer.serialize(SetLogic(logic)) + "\n"
     val header = if (hasMemory) {
       "; We have to disable the logic for z3 to accept the non-standard \"as const\"\n" +
         "; see https://github.com/Z3Prover/z3/issues/1803\n" +
         "; for CVC4 you probably want to include the logic\n" +
-        ";" + logic
-    } else { logic }
+        ";" + logicCmd
+    } else { logicCmd }
     val smt = generatedHeader("SMT-LIBv2", sys.name) + header +
       SMTTransitionSystemEncoder.encode(sys).map(SMTLibSerializer.serialize).mkString("\n") + "\n"
     EmittedSMTModelAnnotation(sys.name, smt, outputSuffix)
diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTExpr.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTExpr.scala
index a40717f9..f2eae58a 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/SMTExpr.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/SMTExpr.scala
@@ -6,17 +6,17 @@
 package firrtl.backends.experimental.smt
 
 /** base trait for all SMT expressions */
-private sealed trait SMTExpr extends SMTFunctionArg {
+sealed trait SMTExpr extends SMTFunctionArg {
   def tpe:      SMTType
   def children: List[SMTExpr]
 }
-private sealed trait SMTSymbol extends SMTExpr with SMTNullaryExpr {
+sealed trait SMTSymbol extends SMTExpr with SMTNullaryExpr {
   def name: String
 
   /** keeps the type of the symbol while changing the name */
   def rename(newName: String): SMTSymbol
 }
-private object SMTSymbol {
+object SMTSymbol {
 
   /** makes a SMTSymbol of the same type as the expression */
   def fromExpr(name: String, e: SMTExpr): SMTSymbol = e match {
@@ -24,76 +24,76 @@ private object SMTSymbol {
     case a: ArrayExpr => ArraySymbol(name, a.indexWidth, a.dataWidth)
   }
 }
-private sealed trait SMTNullaryExpr extends SMTExpr {
+sealed trait SMTNullaryExpr extends SMTExpr {
   override def children: List[SMTExpr] = List()
 }
 
 /** a SMT bit vector expression: https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml */
-private sealed trait BVExpr extends SMTExpr {
+sealed trait BVExpr extends SMTExpr {
   def width: Int
   def tpe:               BVType = BVType(width)
   override def toString: String = SMTExprSerializer.serialize(this)
 }
-private case class BVLiteral(value: BigInt, width: Int) extends BVExpr with SMTNullaryExpr {
+case class BVLiteral(value: BigInt, width: Int) extends BVExpr with SMTNullaryExpr {
   private def minWidth = value.bitLength + (if (value <= 0) 1 else 0)
   assert(value >= 0, "Negative values are not supported! Please normalize by calculating 2s complement.")
   assert(width > 0, "Zero or negative width literals are not allowed!")
   assert(width >= minWidth, "Value (" + value.toString + ") too big for BitVector of width " + width + " bits.")
 }
-private object BVLiteral {
+object BVLiteral {
   def apply(nums: String): BVLiteral = nums.head match {
     case 'b' => BVLiteral(BigInt(nums.drop(1), 2), nums.length - 1)
   }
 }
-private case class BVSymbol(name: String, width: Int) extends BVExpr with SMTSymbol {
+case class BVSymbol(name: String, width: Int) extends BVExpr with SMTSymbol {
   assert(!name.contains("|"), s"Invalid id $name contains escape character `|`")
   assert(width > 0, "Zero width bit vectors are not supported!")
   override def rename(newName: String) = BVSymbol(newName, width)
 }
 
-private sealed trait BVUnaryExpr extends BVExpr {
+sealed trait BVUnaryExpr extends BVExpr {
   def e: BVExpr
 
   /** same function, different child, e.g.: not(x) -- reapply(Y) --> not(Y) */
   def reapply(expr: BVExpr): BVUnaryExpr
   override def children: List[BVExpr] = List(e)
 }
-private case class BVExtend(e: BVExpr, by: Int, signed: Boolean) extends BVUnaryExpr {
+case class BVExtend(e: BVExpr, by: Int, signed: Boolean) extends BVUnaryExpr {
   assert(by >= 0, "Extension must be non-negative!")
   override val width: Int = e.width + by
   override def reapply(expr: BVExpr) = BVExtend(expr, by, signed)
 }
 // also known as bit extract operation
-private case class BVSlice(e: BVExpr, hi: Int, lo: Int) extends BVUnaryExpr {
+case class BVSlice(e: BVExpr, hi: Int, lo: Int) extends BVUnaryExpr {
   assert(lo >= 0, s"lo (lsb) must be non-negative!")
   assert(hi >= lo, s"hi (msb) must not be smaller than lo (lsb): msb: $hi lsb: $lo")
   assert(e.width > hi, s"Out off bounds hi (msb) access: width: ${e.width} msb: $hi")
   override def width: Int = hi - lo + 1
   override def reapply(expr: BVExpr) = BVSlice(expr, hi, lo)
 }
-private case class BVNot(e: BVExpr) extends BVUnaryExpr {
+case class BVNot(e: BVExpr) extends BVUnaryExpr {
   override val width: Int = e.width
   override def reapply(expr: BVExpr) = new BVNot(expr)
 }
-private case class BVNegate(e: BVExpr) extends BVUnaryExpr {
+case class BVNegate(e: BVExpr) extends BVUnaryExpr {
   override val width: Int = e.width
   override def reapply(expr: BVExpr) = BVNegate(expr)
 }
 
-private case class BVReduceOr(e: BVExpr) extends BVUnaryExpr {
+case class BVReduceOr(e: BVExpr) extends BVUnaryExpr {
   override def width: Int = 1
   override def reapply(expr: BVExpr) = BVReduceOr(expr)
 }
-private case class BVReduceAnd(e: BVExpr) extends BVUnaryExpr {
+case class BVReduceAnd(e: BVExpr) extends BVUnaryExpr {
   override def width: Int = 1
   override def reapply(expr: BVExpr) = BVReduceAnd(expr)
 }
-private case class BVReduceXor(e: BVExpr) extends BVUnaryExpr {
+case class BVReduceXor(e: BVExpr) extends BVUnaryExpr {
   override def width: Int = 1
   override def reapply(expr: BVExpr) = BVReduceXor(expr)
 }
 
-private sealed trait BVBinaryExpr extends BVExpr {
+sealed trait BVBinaryExpr extends BVExpr {
   def a: BVExpr
   def b: BVExpr
   override def children: List[BVExpr] = List(a, b)
@@ -101,19 +101,19 @@ private sealed trait BVBinaryExpr extends BVExpr {
   /** same function, different child, e.g.: add(a,b) -- reapply(a,c) --> add(a,c) */
   def reapply(nA: BVExpr, nB: BVExpr): BVBinaryExpr
 }
-private case class BVEqual(a: BVExpr, b: BVExpr) extends BVBinaryExpr {
+case class BVEqual(a: BVExpr, b: BVExpr) extends BVBinaryExpr {
   assert(a.width == b.width, s"Both argument need to be the same width!")
   override def width: Int = 1
   override def reapply(nA: BVExpr, nB: BVExpr) = BVEqual(nA, nB)
 }
 // added as a separate node because it is used a lot in model checking and benefits from pretty printing
-private class BVImplies(val a: BVExpr, val b: BVExpr) extends BVBinaryExpr {
+class BVImplies(val a: BVExpr, val b: BVExpr) extends BVBinaryExpr {
   assert(a.width == 1, s"The antecedent needs to be a boolean expression!")
   assert(b.width == 1, s"The consequent needs to be a boolean expression!")
   override def width: Int = 1
   override def reapply(nA: BVExpr, nB: BVExpr) = new BVImplies(nA, nB)
 }
-private object BVImplies {
+object BVImplies {
   def apply(a: BVExpr, b: BVExpr): BVExpr = {
     assert(a.width == b.width, s"Both argument need to be the same width!")
     (a, b) match {
@@ -127,16 +127,16 @@ private object BVImplies {
   def unapply(i: BVImplies): Some[(BVExpr, BVExpr)] = Some((i.a, i.b))
 }
 
-private object Compare extends Enumeration {
+object Compare extends Enumeration {
   val Greater, GreaterEqual = Value
 }
-private case class BVComparison(op: Compare.Value, a: BVExpr, b: BVExpr, signed: Boolean) extends BVBinaryExpr {
+case class BVComparison(op: Compare.Value, a: BVExpr, b: BVExpr, signed: Boolean) extends BVBinaryExpr {
   assert(a.width == b.width, s"Both argument need to be the same width!")
   override def width: Int = 1
   override def reapply(nA: BVExpr, nB: BVExpr) = BVComparison(op, nA, nB, signed)
 }
 
-private object Op extends Enumeration {
+object Op extends Enumeration {
   val Xor = Value("xor")
   val ShiftLeft = Value("logical_shift_left")
   val ArithmeticShiftRight = Value("arithmetic_shift_right")
@@ -150,70 +150,70 @@ private object Op extends Enumeration {
   val UnsignedRem = Value("urem")
   val Sub = Value("sub")
 }
-private case class BVOp(op: Op.Value, a: BVExpr, b: BVExpr) extends BVBinaryExpr {
+case class BVOp(op: Op.Value, a: BVExpr, b: BVExpr) extends BVBinaryExpr {
   assert(a.width == b.width, s"Both argument need to be the same width!")
   override val width: Int = a.width
   override def reapply(nA: BVExpr, nB: BVExpr) = BVOp(op, nA, nB)
 }
-private case class BVConcat(a: BVExpr, b: BVExpr) extends BVBinaryExpr {
+case class BVConcat(a: BVExpr, b: BVExpr) extends BVBinaryExpr {
   override val width: Int = a.width + b.width
   override def reapply(nA: BVExpr, nB: BVExpr) = BVConcat(nA, nB)
 }
-private case class ArrayRead(array: ArrayExpr, index: BVExpr) extends BVExpr {
+case class ArrayRead(array: ArrayExpr, index: BVExpr) extends BVExpr {
   assert(array.indexWidth == index.width, "Index with does not match expected array index width!")
   override val width:    Int = array.dataWidth
   override def children: List[SMTExpr] = List(array, index)
 }
-private case class BVIte(cond: BVExpr, tru: BVExpr, fals: BVExpr) extends BVExpr {
+case class BVIte(cond: BVExpr, tru: BVExpr, fals: BVExpr) extends BVExpr {
   assert(cond.width == 1, s"Condition needs to be a 1-bit value not ${cond.width}-bit!")
   assert(tru.width == fals.width, s"Both branches need to be of the same width! ${tru.width} vs ${fals.width}")
   override val width:    Int = tru.width
   override def children: List[BVExpr] = List(cond, tru, fals)
 }
 
-private case class BVAnd(terms: List[BVExpr]) extends BVExpr {
+case class BVAnd(terms: List[BVExpr]) extends BVExpr {
   require(terms.size > 1)
   override val width: Int = terms.head.width
   require(terms.forall(_.width == width))
   override def children: List[BVExpr] = terms
 }
 
-private case class BVOr(terms: List[BVExpr]) extends BVExpr {
+case class BVOr(terms: List[BVExpr]) extends BVExpr {
   require(terms.size > 1)
   override val width: Int = terms.head.width
   require(terms.forall(_.width == width))
   override def children: List[BVExpr] = terms
 }
 
-private sealed trait ArrayExpr extends SMTExpr {
+sealed trait ArrayExpr extends SMTExpr {
   val indexWidth: Int
   val dataWidth:  Int
   def tpe:               ArrayType = ArrayType(indexWidth = indexWidth, dataWidth = dataWidth)
   override def toString: String = SMTExprSerializer.serialize(this)
 }
-private case class ArraySymbol(name: String, indexWidth: Int, dataWidth: Int) extends ArrayExpr with SMTSymbol {
+case class ArraySymbol(name: String, indexWidth: Int, dataWidth: Int) extends ArrayExpr with SMTSymbol {
   assert(!name.contains("|"), s"Invalid id $name contains escape character `|`")
   assert(!name.contains("\\"), s"Invalid id $name contains `\\`")
   override def rename(newName: String) = ArraySymbol(newName, indexWidth, dataWidth)
 }
-private case class ArrayConstant(e: BVExpr, indexWidth: Int) extends ArrayExpr {
+case class ArrayConstant(e: BVExpr, indexWidth: Int) extends ArrayExpr {
   override val dataWidth: Int = e.width
   override def children:  List[SMTExpr] = List(e)
 }
-private case class ArrayEqual(a: ArrayExpr, b: ArrayExpr) extends BVExpr {
+case class ArrayEqual(a: ArrayExpr, b: ArrayExpr) extends BVExpr {
   assert(a.indexWidth == b.indexWidth, s"Both argument need to be the same index width!")
   assert(a.dataWidth == b.dataWidth, s"Both argument need to be the same data width!")
   override def width:    Int = 1
   override def children: List[SMTExpr] = List(a, b)
 }
-private case class ArrayStore(array: ArrayExpr, index: BVExpr, data: BVExpr) extends ArrayExpr {
+case class ArrayStore(array: ArrayExpr, index: BVExpr, data: BVExpr) extends ArrayExpr {
   assert(array.indexWidth == index.width, "Index with does not match expected array index width!")
   assert(array.dataWidth == data.width, "Data with does not match expected array data width!")
   override val dataWidth:  Int = array.dataWidth
   override val indexWidth: Int = array.indexWidth
   override def children:   List[SMTExpr] = List(array, index, data)
 }
-private case class ArrayIte(cond: BVExpr, tru: ArrayExpr, fals: ArrayExpr) extends ArrayExpr {
+case class ArrayIte(cond: BVExpr, tru: ArrayExpr, fals: ArrayExpr) extends ArrayExpr {
   assert(cond.width == 1, s"Condition needs to be a 1-bit value not ${cond.width}-bit!")
   assert(
     tru.indexWidth == fals.indexWidth,
@@ -228,27 +228,27 @@ private case class ArrayIte(cond: BVExpr, tru: ArrayExpr, fals: ArrayExpr) exten
   override def children:   List[SMTExpr] = List(cond, tru, fals)
 }
 
-private case class BVForall(variable: BVSymbol, e: BVExpr) extends BVUnaryExpr {
+case class BVForall(variable: BVSymbol, e: BVExpr) extends BVUnaryExpr {
   assert(e.width == 1, "Can only quantify over boolean expressions!")
   override def width = 1
   override def reapply(expr: BVExpr) = BVForall(variable, expr)
 }
 
 /** apply arguments to a function which returns a result of bit vector type */
-private case class BVFunctionCall(name: String, args: List[SMTFunctionArg], width: Int) extends BVExpr {
+case class BVFunctionCall(name: String, args: List[SMTFunctionArg], width: Int) extends BVExpr {
   override def children = args.map(_.asInstanceOf[SMTExpr])
 }
 
 /** apply arguments to a function which returns a result of array type */
-private case class ArrayFunctionCall(name: String, args: List[SMTFunctionArg], indexWidth: Int, dataWidth: Int)
+case class ArrayFunctionCall(name: String, args: List[SMTFunctionArg], indexWidth: Int, dataWidth: Int)
     extends ArrayExpr {
   override def children = args.map(_.asInstanceOf[SMTExpr])
 }
-private sealed trait SMTFunctionArg
+sealed trait SMTFunctionArg
 // we allow symbols with uninterpreted type to be function arguments
-private case class UTSymbol(name: String, tpe: String) extends SMTFunctionArg
+case class UTSymbol(name: String, tpe: String) extends SMTFunctionArg
 
-private object BVAnd {
+object BVAnd {
   def apply(a: BVExpr, b: BVExpr): BVExpr = {
     assert(a.width == b.width, s"Both argument need to be the same width!")
     (a, b) match {
@@ -269,7 +269,7 @@ private object BVAnd {
     }
   }
 }
-private object BVOr {
+object BVOr {
   def apply(a: BVExpr, b: BVExpr): BVExpr = {
     assert(a.width == b.width, s"Both argument need to be the same width!")
     (a, b) match {
@@ -291,7 +291,7 @@ private object BVOr {
   }
 }
 
-private object BVNot {
+object BVNot {
   def apply(e: BVExpr): BVExpr = e match {
     case True()       => False()
     case False()      => True()
@@ -300,7 +300,7 @@ private object BVNot {
   }
 }
 
-private object SMTEqual {
+object SMTEqual {
   def apply(a: SMTExpr, b: SMTExpr): BVExpr = (a, b) match {
     case (ab: BVExpr, bb: BVExpr) => BVEqual(ab, bb)
     case (aa: ArrayExpr, ba: ArrayExpr) => ArrayEqual(aa, ba)
@@ -308,7 +308,7 @@ private object SMTEqual {
   }
 }
 
-private object SMTIte {
+object SMTIte {
   def apply(cond: BVExpr, tru: SMTExpr, fals: SMTExpr): SMTExpr = (tru, fals) match {
     case (ab: BVExpr, bb: BVExpr) => BVIte(cond, ab, bb)
     case (aa: ArrayExpr, ba: ArrayExpr) => ArrayIte(cond, aa, ba)
@@ -316,7 +316,7 @@ private object SMTIte {
   }
 }
 
-private object SMTExpr {
+object SMTExpr {
   def serializeType(e: SMTExpr): String = e match {
     case b: BVExpr    => s"bv<${b.width}>"
     case a: ArrayExpr => s"bv<${a.indexWidth}> -> bv<${a.dataWidth}>"
@@ -324,19 +324,19 @@ private object SMTExpr {
 }
 
 // unapply for matching BVLiteral(1, 1)
-private object True {
+object True {
   private val _True = BVLiteral(1, 1)
   def apply(): BVLiteral = _True
   def unapply(l: BVLiteral): Boolean = l.value == 1 && l.width == 1
 }
 
 // unapply for matching BVLiteral(0, 1)
-private object False {
+object False {
   private val _False = BVLiteral(0, 1)
   def apply(): BVLiteral = _False
   def unapply(l: BVLiteral): Boolean = l.value == 0 && l.width == 1
 }
 
-private sealed trait SMTType
-private case class BVType(width: Int) extends SMTType
-private case class ArrayType(indexWidth: Int, dataWidth: Int) extends SMTType
+sealed trait SMTType
+case class BVType(width: Int) extends SMTType
+case class ArrayType(indexWidth: Int, dataWidth: Int) extends SMTType
diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala
index bb4e0348..a70adc61 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/SMTLibSerializer.scala
@@ -11,9 +11,7 @@ import scala.util.matching.Regex
   *  before serializing!
   *  Automatically converts 1-bit vectors to bool.
   */
-private object SMTLibSerializer {
-  def setLogic(hasMem: Boolean) = "(set-logic QF_" + (if (hasMem) "A" else "") + "UFBV)"
-
+object SMTLibSerializer {
   def serialize(e: SMTExpr): String = e match {
     case b: BVExpr    => serialize(b)
     case a: ArrayExpr => serialize(a)
diff --git a/src/main/scala/firrtl/backends/experimental/smt/SMTTransitionSystemEncoder.scala b/src/main/scala/firrtl/backends/experimental/smt/SMTTransitionSystemEncoder.scala
index 472363cc..4f096c28 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/SMTTransitionSystemEncoder.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/SMTTransitionSystemEncoder.scala
@@ -11,7 +11,7 @@ import scala.collection.mutable
   * prevents this encoding from working with boolector.
   * For simplicity reasons, we do not support hierarchical designs (no `_h` function).
   */
-private object SMTTransitionSystemEncoder {
+object SMTTransitionSystemEncoder {
 
   def encode(sys: TransitionSystem): Iterable[SMTCommand] = {
     val cmds = mutable.ArrayBuffer[SMTCommand]()
diff --git a/src/main/scala/firrtl/backends/experimental/smt/TransitionSystem.scala b/src/main/scala/firrtl/backends/experimental/smt/TransitionSystem.scala
index 66a1b385..bd3ad740 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/TransitionSystem.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/TransitionSystem.scala
@@ -6,14 +6,14 @@ package firrtl.backends.experimental.smt
 import firrtl.graph.MutableDiGraph
 import scala.collection.mutable
 
-private case class State(sym: SMTSymbol, init: Option[SMTExpr], next: Option[SMTExpr]) {
+case class State(sym: SMTSymbol, init: Option[SMTExpr], next: Option[SMTExpr]) {
   def name: String = sym.name
 }
-private case class Signal(name: String, e: SMTExpr, lbl: SignalLabel = IsNode) {
+case class Signal(name: String, e: SMTExpr, lbl: SignalLabel = IsNode) {
   def toSymbol: SMTSymbol = SMTSymbol.fromExpr(name, e)
   def sym:      SMTSymbol = toSymbol
 }
-private case class TransitionSystem(
+case class TransitionSystem(
   name:     String,
   inputs:   List[BVSymbol],
   states:   List[State],
@@ -23,23 +23,23 @@ private case class TransitionSystem(
   def serialize: String = TransitionSystem.serialize(this)
 }
 
-private sealed trait SignalLabel
-private case object IsNode extends SignalLabel
-private case object IsOutput extends SignalLabel
-private case object IsConstraint extends SignalLabel
-private case object IsBad extends SignalLabel
-private case object IsFair extends SignalLabel
-private case object IsNext extends SignalLabel
-private case object IsInit extends SignalLabel
+sealed trait SignalLabel
+case object IsNode extends SignalLabel
+case object IsOutput extends SignalLabel
+case object IsConstraint extends SignalLabel
+case object IsBad extends SignalLabel
+case object IsFair extends SignalLabel
+case object IsNext extends SignalLabel
+case object IsInit extends SignalLabel
 
-private object SignalLabel {
+object SignalLabel {
   private val labels = Seq(IsNode, IsOutput, IsConstraint, IsBad, IsFair, IsNext, IsInit)
   val labelStrings = Seq("node", "output", "constraint", "bad", "fair", "next", "init")
   val labelToString: SignalLabel => String = labels.zip(labelStrings).toMap
   val stringToLabel: String => SignalLabel = labelStrings.zip(labels).toMap
 }
 
-private object TransitionSystem {
+object TransitionSystem {
   def serialize(sys: TransitionSystem): String = {
     (Iterator(sys.name) ++
       sys.inputs.map(i => s"input ${i.name} : ${SMTExpr.serializeType(i)}") ++