Smtlib types

src/col/vct/col/ast/lang/smt/SmtlibBitvecLiteralImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibBitvecLiteral, TSmtlibBitVector, Type}
+import vct.col.print._
+
+trait SmtlibBitvecLiteralImpl[G] { this: SmtlibBitvecLiteral[G] =>
+  override def t: Type[G] = TSmtlibBitVector(data.length)
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvAddImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvAdd
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvAddImpl[G] { this: SmtlibBvAdd[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvAndImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvAnd
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvAndImpl[G] { this: SmtlibBvAnd[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvMulImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvMul
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvMulImpl[G] { this: SmtlibBvMul[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvNegImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvNeg
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvNegImpl[G] { this: SmtlibBvNeg[G] =>
+  override def t: Type[G] = bv.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvNotImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvNot
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvNotImpl[G] { this: SmtlibBvNot[G] =>
+  override def t: Type[G] = bv.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvOrImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvOr
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvOrImpl[G] { this: SmtlibBvOr[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvShlImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvShl
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvShlImpl[G] { this: SmtlibBvShl[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvShrImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvShr
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvShrImpl[G] { this: SmtlibBvShr[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvUDivImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvUDiv
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvUDivImpl[G] { this: SmtlibBvUDiv[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvULtImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvULt
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvULtImpl[G] { this: SmtlibBvULt[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibBvURemImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibBvURem
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibBvURemImpl[G] { this: SmtlibBvURem[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibConcatImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibConcat, TSmtlibBitVector, Type}
+import vct.col.print._
+
+trait SmtlibConcatImpl[G] { this: SmtlibConcat[G] =>
+  override lazy val t: Type[G] = TSmtlibBitVector(left.t.asBitvec.get.size + right.t.asBitvec.get.size)
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibExtractImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibExtract, TSmtlibBitVector, Type}
+import vct.col.print._
+
+trait SmtlibExtractImpl[G] { this: SmtlibExtract[G] =>
+  override def t: Type[G] = TSmtlibBitVector(inclusiveEndIndexFromRight - startIndexFromRight + 1)
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpAbsImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibFpAbs
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibFpAbsImpl[G] { this: SmtlibFpAbs[G] =>
+  override def t: Type[G] = arg.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpAddImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibFpAdd
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibFpAddImpl[G] { this: SmtlibFpAdd[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpCastImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpCast, TSmtlibFloatingPoint, Type}
+import vct.col.print._
+
+trait SmtlibFpCastImpl[G] { this: SmtlibFpCast[G] =>
+  override def t: Type[G] = TSmtlibFloatingPoint(exponentBits, mantissaAndSignBits)
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpDivImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibFpDiv
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibFpDivImpl[G] { this: SmtlibFpDiv[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpEqImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibFpEq
+import vct.col.ast.{Type, TBool}
+import vct.col.print._
+
+trait SmtlibFpEqImpl[G] { this: SmtlibFpEq[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpFmaImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibFpFma
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibFpFmaImpl[G] { this: SmtlibFpFma[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpFromRealImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpFromReal, TSmtlibFloatingPoint, Type}
+import vct.col.print._
+
+trait SmtlibFpFromRealImpl[G] { this: SmtlibFpFromReal[G] =>
+  override def t: Type[G] = TSmtlibFloatingPoint(exponentBits, mantissaAndSignBits)
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpFromSIntImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpFromSInt, TSmtlibFloatingPoint, Type}
+import vct.col.print._
+
+trait SmtlibFpFromSIntImpl[G] { this: SmtlibFpFromSInt[G] =>
+  override def t: Type[G] = TSmtlibFloatingPoint(exponentBits, mantissaAndSignBits)
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpFromUIntImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpFromUInt, TSmtlibFloatingPoint, Type}
+import vct.col.print._
+
+trait SmtlibFpFromUIntImpl[G] { this: SmtlibFpFromUInt[G] =>
+  override def t: Type[G] = TSmtlibFloatingPoint(exponentBits, mantissaAndSignBits)
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpGeqImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpGeq, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpGeqImpl[G] { this: SmtlibFpGeq[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpGtImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpGt, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpGtImpl[G] { this: SmtlibFpGt[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFp, TSmtlibFloatingPoint, Type}
+import vct.col.print._
+
+trait SmtlibFpImpl[G] { this: SmtlibFp[G] =>
+  override def t: Type[G] = TSmtlibFloatingPoint(exponent.t.asBitvec.get.size, mantissa.t.asBitvec.get.size + 1)
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpIsInfiniteImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpIsInfinite, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpIsInfiniteImpl[G] { this: SmtlibFpIsInfinite[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpIsNaNImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpIsNaN, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpIsNaNImpl[G] { this: SmtlibFpIsNaN[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpIsNegativeImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpIsNegative, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpIsNegativeImpl[G] { this: SmtlibFpIsNegative[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpIsNormalImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpIsNormal, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpIsNormalImpl[G] { this: SmtlibFpIsNormal[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpIsPositiveImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpIsPositive, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpIsPositiveImpl[G] { this: SmtlibFpIsPositive[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpIsSubnormalImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpIsSubnormal, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpIsSubnormalImpl[G] { this: SmtlibFpIsSubnormal[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpIsZeroImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpIsZero, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpIsZeroImpl[G] { this: SmtlibFpIsZero[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpLeqImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpLeq, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpLeqImpl[G] { this: SmtlibFpLeq[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpLtImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibFpLt, TBool, Type}
+import vct.col.print._
+
+trait SmtlibFpLtImpl[G] { this: SmtlibFpLt[G] =>
+  override def t: Type[G] = TBool()
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpMaxImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibFpMax
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibFpMaxImpl[G] { this: SmtlibFpMax[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpMinImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibFpMin
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibFpMinImpl[G] { this: SmtlibFpMin[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/lang/smt/SmtlibFpMulImpl.scala

@@ -0,0 +1,10 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.SmtlibFpMul
+import vct.col.ast.Type
+import vct.col.print._
+
+trait SmtlibFpMulImpl[G] { this: SmtlibFpMul[G] =>
+  override def t: Type[G] = left.t
+  // def layout(implicit ctx: Ctx): Doc = ???
+}