diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 018095785a..afb5c15f79 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -1,6 +1,7 @@ package vct.col.ast +import hre.data.BitString import vct.col.ast.`type`._ import vct.col.ast.`type`.typeclass._ import vct.col.ast.declaration._ @@ -57,6 +58,7 @@ import vct.col.ast.family.bipglueelement._ import vct.col.ast.family.bipporttype._ import vct.col.ast.family.data._ import vct.col.ast.lang._ +import vct.col.ast.lang.smt._ import vct.col.ast.node._ import vct.col.ast.statement._ import vct.col.ast.statement.composite._ @@ -702,6 +704,148 @@ final case class ModelChoose[G](model: Expr[G], perm: Expr[G], totalProcess: Exp final case class ModelPerm[G](loc: Expr[G], perm: Expr[G])(implicit val o: Origin) extends Expr[G] with ModelPermImpl[G] final case class ActionPerm[G](loc: Expr[G], perm: Expr[G])(implicit val o: Origin) extends Expr[G] with ActionPermImpl[G] +sealed trait SmtlibType[G] extends Type[G] +case class TSmtlibArray[G](index: Seq[Type[G]], value: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends SmtlibType[G] +case class TSmtlibBitVector[G](size: Int)(implicit val o: Origin = DiagnosticOrigin) extends SmtlibType[G] +case class TSmtlibRoundingMode[G]()(implicit val o: Origin = DiagnosticOrigin) extends SmtlibType[G] +case class TSmtlibFloatingPoint[G](exponentBits: Int, mantissaAndSignBits: Int)(implicit val o: Origin = DiagnosticOrigin) extends SmtlibType[G] +case class TSmtlibString[G]()(implicit val o: Origin = DiagnosticOrigin) extends SmtlibType[G] +case class TSmtlibRegLan[G]()(implicit val o: Origin = DiagnosticOrigin) extends SmtlibType[G] +// Non-standard Z3 extensions +case class TSmtlibSeq[G](element: Type[G])(implicit val o: Origin = DiagnosticOrigin) extends SmtlibType[G] + +sealed trait SmtlibFunctionSymbol[G] extends NodeFamily[G] with SmtlibFunctionSymbolImpl[G] +case class SmtlibADTFunctionSymbol[G](ref: Ref[G, ADTFunction[G]])(implicit val o: Origin) extends SmtlibFunctionSymbol[G] +case class SmtlibProverFunctionSymbol[G](ref: Ref[G, ProverFunction[G]])(implicit val o: Origin) extends SmtlibFunctionSymbol[G] + +sealed trait SmtlibExpr[G] extends Expr[G] +case class SmtlibSelect[G](arr: Expr[G], is: Seq[Expr[G]])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibSelectImpl[G] +case class SmtlibStore[G](arr: Expr[G], is: Seq[Expr[G]], x: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStoreImpl[G] + +case class SmtlibBitvecLiteral[G](data: BitString)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBitvecLiteralImpl[G] +case class SmtlibConcat[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibConcatImpl[G] +case class SmtlibExtract[G](inclusiveEndIndexFromRight: Int, startIndexFromRight: Int, bv: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibExtractImpl[G] +case class SmtlibBvNot[G](bv: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvNotImpl[G] +case class SmtlibBvAnd[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvAndImpl[G] +case class SmtlibBvOr[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvOrImpl[G] +case class SmtlibBvNeg[G](bv: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvNegImpl[G] +case class SmtlibBvAdd[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvAddImpl[G] +case class SmtlibBvMul[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvMulImpl[G] +case class SmtlibBvUDiv[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvUDivImpl[G] +case class SmtlibBvURem[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvURemImpl[G] +case class SmtlibBvShl[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvShlImpl[G] +case class SmtlibBvShr[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvShrImpl[G] +case class SmtlibBvULt[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibBvULtImpl[G] + +case class SmtlibRNE[G]()(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibRNEImpl[G] +case class SmtlibRNA[G]()(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibRNAImpl[G] +case class SmtlibRTP[G]()(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibRTPImpl[G] +case class SmtlibRTN[G]()(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibRTNImpl[G] +case class SmtlibRTZ[G]()(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibRTZImpl[G] + +case class SmtlibFp[G](sign: Expr[G], exponent: Expr[G], mantissa: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpImpl[G] +case class SmtlibFpAbs[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpAbsImpl[G] +case class SmtlibFpNeg[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpNegImpl[G] +case class SmtlibFpAdd[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpAddImpl[G] +case class SmtlibFpSub[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpSubImpl[G] +case class SmtlibFpMul[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpMulImpl[G] +case class SmtlibFpDiv[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpDivImpl[G] +case class SmtlibFpFma[G](left: Expr[G], right: Expr[G], addend: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpFmaImpl[G] +case class SmtlibFpSqrt[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpSqrtImpl[G] +case class SmtlibFpRem[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpRemImpl[G] +case class SmtlibFpRoundToIntegral[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpRoundToIntegralImpl[G] +case class SmtlibFpMin[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpMinImpl[G] +case class SmtlibFpMax[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpMaxImpl[G] +case class SmtlibFpLeq[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpLeqImpl[G] +case class SmtlibFpLt[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpLtImpl[G] +case class SmtlibFpGeq[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpGeqImpl[G] +case class SmtlibFpGt[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpGtImpl[G] +case class SmtlibFpEq[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpEqImpl[G] +case class SmtlibFpIsNormal[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpIsNormalImpl[G] +case class SmtlibFpIsSubnormal[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpIsSubnormalImpl[G] +case class SmtlibFpIsZero[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpIsZeroImpl[G] +case class SmtlibFpIsInfinite[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpIsInfiniteImpl[G] +case class SmtlibFpIsNaN[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpIsNaNImpl[G] +case class SmtlibFpIsNegative[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpIsNegativeImpl[G] +case class SmtlibFpIsPositive[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpIsPositiveImpl[G] +case class SmtlibToFp[G](bv: Expr[G], exponentBits: Int, mantissaAndSignBits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibToFpImpl[G] +case class SmtlibFpCast[G](arg: Expr[G], exponentBits: Int, mantissaAndSignBits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpCastImpl[G] +case class SmtlibFpFromReal[G](arg: Expr[G], exponentBits: Int, mantissaAndSignBits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpFromRealImpl[G] +case class SmtlibFpFromSInt[G](bv: Expr[G], exponentBits: Int, mantissaAndSignBits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpFromSIntImpl[G] +case class SmtlibFpFromUInt[G](bv: Expr[G], exponentBits: Int, mantissaAndSignBits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpFromUIntImpl[G] +case class SmtlibFpToReal[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpToRealImpl[G] +case class SmtlibFpToSInt[G](arg: Expr[G], bits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpToSIntImpl[G] +case class SmtlibFpToUInt[G](arg: Expr[G], bits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpToUIntImpl[G] + +case class SmtlibLiteralString[G](data: String)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibLiteralStringImpl[G] +case class SmtlibStrConcat[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrConcatImpl[G] +case class SmtlibStrLen[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrLenImpl[G] +case class SmtlibStrLt[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrLtImpl[G] +case class SmtlibStrLeq[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrLeqImpl[G] +case class SmtlibStrAt[G](str: Expr[G], i: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrAtImpl[G] +case class SmtlibSubstr[G](str: Expr[G], i: Expr[G], n: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibSubstrImpl[G] +case class SmtlibStrPrefixOf[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrPrefixOfImpl[G] +case class SmtlibStrSuffixOf[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrSuffixOfImpl[G] +case class SmtlibStrContains[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrContainsImpl[G] +case class SmtlibStrIndexOf[G](haystack: Expr[G], needle: Expr[G], fromIndex: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrIndexOfImpl[G] +case class SmtlibStrReplace[G](haystack: Expr[G], needle: Expr[G], replacement: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrReplaceImpl[G] +case class SmtlibStrReplaceAll[G](haystack: Expr[G], needle: Expr[G], replacement: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrReplaceAllImpl[G] +case class SmtlibStrReplaceRe[G](haystack: Expr[G], re: Expr[G], replacement: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrReplaceReImpl[G] +case class SmtlibStrReplaceReAll[G](haystack: Expr[G], re: Expr[G], replacement: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrReplaceReAllImpl[G] +case class SmtlibStrIsDigit[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrIsDigitImpl[G] +case class SmtlibStrToCode[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrToCodeImpl[G] +case class SmtlibStrFromCode[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrFromCodeImpl[G] +case class SmtlibStrToInt[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrToIntImpl[G] +case class SmtlibStrFromInt[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibStrFromIntImpl[G] + +case class SmtlibReFromStr[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReFromStrImpl[G] +case class SmtlibReContains[G](re: Expr[G], str: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReContainsImpl[G] +case class SmtlibReNone[G]()(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReNoneImpl[G] +case class SmtlibReAll[G]()(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReAllImpl[G] +case class SmtlibReAllChar[G]()(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReAllCharImpl[G] +case class SmtlibReConcat[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReConcatImpl[G] +case class SmtlibReUnion[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReUnionImpl[G] +case class SmtlibReInter[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReInterImpl[G] +case class SmtlibReStar[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReStarImpl[G] +case class SmtlibReComp[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReCompImpl[G] +case class SmtlibReDiff[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReDiffImpl[G] +case class SmtlibRePlus[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibRePlusImpl[G] +case class SmtlibReOpt[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReOptImpl[G] +case class SmtlibReRange[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReRangeImpl[G] +case class SmtlibReRepeat[G](count: Int, arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReRepeatImpl[G] +case class SmtlibReRepeatRange[G](from: Int, to: Int, arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibReRepeatRangeImpl[G] + +// Non-standard Z3 extensions +case class Z3BvSub[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3BvSubImpl[G] +case class Z3BvSRem[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3BvSRemImpl[G] +case class Z3BvSMod[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3BvSModImpl[G] +case class Z3BvSShr[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3BvSShrImpl[G] +case class Z3BvNand[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3BvNandImpl[G] +case class Z3BvNor[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3BvNorImpl[G] +case class Z3BvXnor[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3BvXnorImpl[G] + +case class Z3ArrayConst[G](domain: Seq[Type[G]], codomain: Type[G], value: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3ArrayConstImpl[G] +case class Z3ArrayOfFunction[G](ref: SmtlibFunctionSymbol[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3ArrayOfFunctionImpl[G] +case class Z3ArrayMap[G](ref: SmtlibFunctionSymbol[G], args: Seq[Expr[G]])(implicit val o: Origin) extends SmtlibExpr[G] with Z3ArrayMapImpl[G] + +case class Z3SeqEmpty[G](elementType: Type[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqEmptyImpl[G] +case class Z3SeqUnit[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqUnitImpl[G] +case class Z3SeqConcat[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqConcatImpl[G] +case class Z3SeqLen[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqLenImpl[G] +case class Z3SeqExtract[G](seq: Expr[G], offset: Expr[G], len: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqExtractImpl[G] +case class Z3SeqAt[G](seq: Expr[G], offset: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqAtImpl[G] +case class Z3SeqNth[G](seq: Expr[G], offset: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqNthImpl[G] +case class Z3SeqContains[G](seq: Expr[G], subseq: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqContainsImpl[G] +case class Z3SeqPrefixOf[G](pre: Expr[G], subseq: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqPrefixOfImpl[G] +case class Z3SeqSuffixOf[G](post: Expr[G], seq: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqSuffixOfImpl[G] +case class Z3SeqReplace[G](haystack: Expr[G], needle: Expr[G], replacement: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqReplaceImpl[G] +case class Z3SeqMap[G](f: Expr[G], seq: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqMapImpl[G] +case class Z3SeqMapI[G](f: Expr[G], offset: Expr[G], seq: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqMapIImpl[G] +case class Z3SeqFoldl[G](f: Expr[G], base: Expr[G], seq: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqFoldlImpl[G] +case class Z3SeqFoldlI[G](f: Expr[G], offset: Expr[G], base: Expr[G], seq: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with Z3SeqFoldlIImpl[G] + +case class Z3TransitiveClosure[G](ref: SmtlibFunctionSymbol[G], args: Seq[Expr[G]])(implicit val o: Origin) extends SmtlibExpr[G] with Z3TransitiveClosureImpl[G] + sealed trait CDeclarationSpecifier[G] extends NodeFamily[G] with CDeclarationSpecifierImpl[G] sealed trait CSpecificationModifier[G] extends CDeclarationSpecifier[G] with CSpecificationModifierImpl[G] diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBitvecLiteralImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBitvecLiteralImpl.scala new file mode 100644 index 0000000000..386b07106a --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvAddImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvAddImpl.scala new file mode 100644 index 0000000000..fe4799b8eb --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvAndImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvAndImpl.scala new file mode 100644 index 0000000000..79439099a6 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvMulImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvMulImpl.scala new file mode 100644 index 0000000000..ac9e5cebe1 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvNegImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvNegImpl.scala new file mode 100644 index 0000000000..e09db42950 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvNotImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvNotImpl.scala new file mode 100644 index 0000000000..b5353b1ebd --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvOrImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvOrImpl.scala new file mode 100644 index 0000000000..08d1835c16 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvShlImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvShlImpl.scala new file mode 100644 index 0000000000..10f658271d --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvShrImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvShrImpl.scala new file mode 100644 index 0000000000..874bae9d7c --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvUDivImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvUDivImpl.scala new file mode 100644 index 0000000000..5602d17af3 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvULtImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvULtImpl.scala new file mode 100644 index 0000000000..5c09ad3d69 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibBvURemImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibBvURemImpl.scala new file mode 100644 index 0000000000..acd579255f --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibConcatImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibConcatImpl.scala new file mode 100644 index 0000000000..411a462367 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibExtractImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibExtractImpl.scala new file mode 100644 index 0000000000..d1821cc0a8 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpAbsImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpAbsImpl.scala new file mode 100644 index 0000000000..e24d63fa4d --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpAddImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpAddImpl.scala new file mode 100644 index 0000000000..a628d39467 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpCastImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpCastImpl.scala new file mode 100644 index 0000000000..be9b0d2be7 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpDivImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpDivImpl.scala new file mode 100644 index 0000000000..f618879a75 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpEqImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpEqImpl.scala new file mode 100644 index 0000000000..9dc695b3fc --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpFmaImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpFmaImpl.scala new file mode 100644 index 0000000000..7d2d3c2507 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpFromRealImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpFromRealImpl.scala new file mode 100644 index 0000000000..826bddfad0 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpFromSIntImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpFromSIntImpl.scala new file mode 100644 index 0000000000..816856498b --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpFromUIntImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpFromUIntImpl.scala new file mode 100644 index 0000000000..511020b0de --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpGeqImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpGeqImpl.scala new file mode 100644 index 0000000000..d19ce3a8c8 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpGtImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpGtImpl.scala new file mode 100644 index 0000000000..345ef2b644 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpImpl.scala new file mode 100644 index 0000000000..cebf7877de --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpIsInfiniteImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpIsInfiniteImpl.scala new file mode 100644 index 0000000000..2d47c38958 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpIsNaNImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpIsNaNImpl.scala new file mode 100644 index 0000000000..ba3ee8521e --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpIsNegativeImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpIsNegativeImpl.scala new file mode 100644 index 0000000000..0d6611336e --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpIsNormalImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpIsNormalImpl.scala new file mode 100644 index 0000000000..8d6ab9c140 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpIsPositiveImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpIsPositiveImpl.scala new file mode 100644 index 0000000000..815ffffd7d --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpIsSubnormalImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpIsSubnormalImpl.scala new file mode 100644 index 0000000000..58ad10f6fb --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpIsZeroImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpIsZeroImpl.scala new file mode 100644 index 0000000000..114670f6c6 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpLeqImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpLeqImpl.scala new file mode 100644 index 0000000000..29a48947f2 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpLtImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpLtImpl.scala new file mode 100644 index 0000000000..e3ad19a9f4 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpMaxImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpMaxImpl.scala new file mode 100644 index 0000000000..03ae1216f3 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpMinImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpMinImpl.scala new file mode 100644 index 0000000000..b492e69762 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpMulImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpMulImpl.scala new file mode 100644 index 0000000000..cff13a33a2 --- /dev/null +++ b/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 = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpNegImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpNegImpl.scala new file mode 100644 index 0000000000..7deff1c937 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFpNegImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.SmtlibFpNeg +import vct.col.ast.Type +import vct.col.print._ + +trait SmtlibFpNegImpl[G] { this: SmtlibFpNeg[G] => + override def t: Type[G] = arg.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpRemImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpRemImpl.scala new file mode 100644 index 0000000000..adef09ea97 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFpRemImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.SmtlibFpRem +import vct.col.ast.Type +import vct.col.print._ + +trait SmtlibFpRemImpl[G] { this: SmtlibFpRem[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpRoundToIntegralImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpRoundToIntegralImpl.scala new file mode 100644 index 0000000000..c2f4cdc17b --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFpRoundToIntegralImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.SmtlibFpRoundToIntegral +import vct.col.ast.Type +import vct.col.print._ + +trait SmtlibFpRoundToIntegralImpl[G] { this: SmtlibFpRoundToIntegral[G] => + override def t: Type[G] = arg.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpSqrtImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpSqrtImpl.scala new file mode 100644 index 0000000000..83409b0925 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFpSqrtImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.SmtlibFpSqrt +import vct.col.ast.Type +import vct.col.print._ + +trait SmtlibFpSqrtImpl[G] { this: SmtlibFpSqrt[G] => + override def t: Type[G] = arg.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpSubImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpSubImpl.scala new file mode 100644 index 0000000000..58e7c03463 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFpSubImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.SmtlibFpSub +import vct.col.ast.Type +import vct.col.print._ + +trait SmtlibFpSubImpl[G] { this: SmtlibFpSub[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpToRealImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpToRealImpl.scala new file mode 100644 index 0000000000..7dfd1533c2 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFpToRealImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibFpToReal, TRational, Type} +import vct.col.print._ + +trait SmtlibFpToRealImpl[G] { this: SmtlibFpToReal[G] => + override def t: Type[G] = TRational() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpToSIntImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpToSIntImpl.scala new file mode 100644 index 0000000000..bbb50f6a9d --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFpToSIntImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibFpToSInt, TSmtlibBitVector, Type} +import vct.col.print._ + +trait SmtlibFpToSIntImpl[G] { this: SmtlibFpToSInt[G] => + override def t: Type[G] = TSmtlibBitVector(bits) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFpToUIntImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFpToUIntImpl.scala new file mode 100644 index 0000000000..a12193a584 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFpToUIntImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibFpToUInt, TSmtlibBitVector, Type} +import vct.col.print._ + +trait SmtlibFpToUIntImpl[G] { this: SmtlibFpToUInt[G] => + override def t: Type[G] = TSmtlibBitVector(bits) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibFunctionSymbolImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibFunctionSymbolImpl.scala new file mode 100644 index 0000000000..465a8a8283 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibFunctionSymbolImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{Applicable, SmtlibFunctionSymbol} +import vct.col.ref.Ref + +trait SmtlibFunctionSymbolImpl[G] { this: SmtlibFunctionSymbol[G] => + def ref: Ref[G, _ <: Applicable[G]] +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibLiteralStringImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibLiteralStringImpl.scala new file mode 100644 index 0000000000..a7dffaca98 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibLiteralStringImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibLiteralString, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibLiteralStringImpl[G] { this: SmtlibLiteralString[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibRNAImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibRNAImpl.scala new file mode 100644 index 0000000000..e37dd2cf8a --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibRNAImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibRNA, TSmtlibRoundingMode, Type} +import vct.col.print._ + +trait SmtlibRNAImpl[G] { this: SmtlibRNA[G] => + override def t: Type[G] = TSmtlibRoundingMode() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibRNEImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibRNEImpl.scala new file mode 100644 index 0000000000..808d08de8e --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibRNEImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibRNE, TSmtlibRoundingMode, Type} +import vct.col.print._ + +trait SmtlibRNEImpl[G] { this: SmtlibRNE[G] => + override def t: Type[G] = TSmtlibRoundingMode() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibRTNImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibRTNImpl.scala new file mode 100644 index 0000000000..205b747bea --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibRTNImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibRTN, TSmtlibRoundingMode, Type} +import vct.col.print._ + +trait SmtlibRTNImpl[G] { this: SmtlibRTN[G] => + override def t: Type[G] = TSmtlibRoundingMode() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibRTPImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibRTPImpl.scala new file mode 100644 index 0000000000..1db2c04bde --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibRTPImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibRTP, TSmtlibRoundingMode, Type} +import vct.col.print._ + +trait SmtlibRTPImpl[G] { this: SmtlibRTP[G] => + override def t: Type[G] = TSmtlibRoundingMode() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibRTZImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibRTZImpl.scala new file mode 100644 index 0000000000..15e3ad0bf4 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibRTZImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibRTZ, TSmtlibRoundingMode, Type} +import vct.col.print._ + +trait SmtlibRTZImpl[G] { this: SmtlibRTZ[G] => + override def t: Type[G] = TSmtlibRoundingMode() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReAllCharImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReAllCharImpl.scala new file mode 100644 index 0000000000..cd2f337d4d --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReAllCharImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReAllChar, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReAllCharImpl[G] { this: SmtlibReAllChar[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReAllImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReAllImpl.scala new file mode 100644 index 0000000000..82bdbd1fa5 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReAllImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReAll, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReAllImpl[G] { this: SmtlibReAll[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReCompImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReCompImpl.scala new file mode 100644 index 0000000000..6378e664ae --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReCompImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReComp, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReCompImpl[G] { this: SmtlibReComp[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReConcatImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReConcatImpl.scala new file mode 100644 index 0000000000..382abdb8a8 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReConcatImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReConcat, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReConcatImpl[G] { this: SmtlibReConcat[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReContainsImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReContainsImpl.scala new file mode 100644 index 0000000000..725a143ac8 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReContainsImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReContains, TBool, Type} +import vct.col.print._ + +trait SmtlibReContainsImpl[G] { this: SmtlibReContains[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReDiffImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReDiffImpl.scala new file mode 100644 index 0000000000..bd66fcddc8 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReDiffImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReDiff, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReDiffImpl[G] { this: SmtlibReDiff[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReFromStrImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReFromStrImpl.scala new file mode 100644 index 0000000000..b7fe3ba4eb --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReFromStrImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReFromStr, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReFromStrImpl[G] { this: SmtlibReFromStr[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReInterImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReInterImpl.scala new file mode 100644 index 0000000000..83130b6106 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReInterImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReInter, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReInterImpl[G] { this: SmtlibReInter[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReNoneImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReNoneImpl.scala new file mode 100644 index 0000000000..659a8a142e --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReNoneImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReNone, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReNoneImpl[G] { this: SmtlibReNone[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReOptImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReOptImpl.scala new file mode 100644 index 0000000000..493f5b0ca3 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReOptImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReOpt, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReOptImpl[G] { this: SmtlibReOpt[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibRePlusImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibRePlusImpl.scala new file mode 100644 index 0000000000..ae213bbfc3 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibRePlusImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibRePlus, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibRePlusImpl[G] { this: SmtlibRePlus[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReRangeImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReRangeImpl.scala new file mode 100644 index 0000000000..d4b08d5413 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReRangeImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReRange, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReRangeImpl[G] { this: SmtlibReRange[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReRepeatImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReRepeatImpl.scala new file mode 100644 index 0000000000..4282fc18df --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReRepeatImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReRepeat, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReRepeatImpl[G] { this: SmtlibReRepeat[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReRepeatRangeImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReRepeatRangeImpl.scala new file mode 100644 index 0000000000..2c87d7c9ec --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReRepeatRangeImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReRepeatRange, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReRepeatRangeImpl[G] { this: SmtlibReRepeatRange[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReStarImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReStarImpl.scala new file mode 100644 index 0000000000..32d4bde04f --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReStarImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReStar, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReStarImpl[G] { this: SmtlibReStar[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibReUnionImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibReUnionImpl.scala new file mode 100644 index 0000000000..761c479400 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibReUnionImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibReUnion, TSmtlibRegLan, Type} +import vct.col.print._ + +trait SmtlibReUnionImpl[G] { this: SmtlibReUnion[G] => + override def t: Type[G] = TSmtlibRegLan() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibSelectImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibSelectImpl.scala new file mode 100644 index 0000000000..a094eb81e7 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibSelectImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.SmtlibSelect +import vct.col.ast.Type +import vct.col.print._ + +trait SmtlibSelectImpl[G] { this: SmtlibSelect[G] => + override def t: Type[G] = arr.t.asSmtlibArray.get.value + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStoreImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStoreImpl.scala new file mode 100644 index 0000000000..5e6ab2ae45 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStoreImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.SmtlibStore +import vct.col.ast.Type +import vct.col.print._ + +trait SmtlibStoreImpl[G] { this: SmtlibStore[G] => + override def t: Type[G] = arr.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrAtImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrAtImpl.scala new file mode 100644 index 0000000000..4267caec31 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrAtImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrAt, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibStrAtImpl[G] { this: SmtlibStrAt[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrConcatImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrConcatImpl.scala new file mode 100644 index 0000000000..06d7bb12fa --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrConcatImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrConcat, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibStrConcatImpl[G] { this: SmtlibStrConcat[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrContainsImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrContainsImpl.scala new file mode 100644 index 0000000000..5a956efb48 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrContainsImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrContains, TBool, Type} +import vct.col.print._ + +trait SmtlibStrContainsImpl[G] { this: SmtlibStrContains[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrFromCodeImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrFromCodeImpl.scala new file mode 100644 index 0000000000..e383eeb02c --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrFromCodeImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrFromCode, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibStrFromCodeImpl[G] { this: SmtlibStrFromCode[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrFromIntImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrFromIntImpl.scala new file mode 100644 index 0000000000..ca7ff2f018 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrFromIntImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrFromInt, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibStrFromIntImpl[G] { this: SmtlibStrFromInt[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrIndexOfImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrIndexOfImpl.scala new file mode 100644 index 0000000000..aab9833d88 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrIndexOfImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrIndexOf, TInt, Type} +import vct.col.print._ + +trait SmtlibStrIndexOfImpl[G] { this: SmtlibStrIndexOf[G] => + override def t: Type[G] = TInt() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrIsDigitImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrIsDigitImpl.scala new file mode 100644 index 0000000000..d7e9210f4a --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrIsDigitImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrIsDigit, TBool, Type} +import vct.col.print._ + +trait SmtlibStrIsDigitImpl[G] { this: SmtlibStrIsDigit[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrLenImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrLenImpl.scala new file mode 100644 index 0000000000..ce286206c1 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrLenImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrLen, TInt, Type} +import vct.col.print._ + +trait SmtlibStrLenImpl[G] { this: SmtlibStrLen[G] => + override def t: Type[G] = TInt() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrLeqImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrLeqImpl.scala new file mode 100644 index 0000000000..f59cb63c30 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrLeqImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrLeq, TBool, Type} +import vct.col.print._ + +trait SmtlibStrLeqImpl[G] { this: SmtlibStrLeq[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrLtImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrLtImpl.scala new file mode 100644 index 0000000000..33696d6e23 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrLtImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrLt, TBool, Type} +import vct.col.print._ + +trait SmtlibStrLtImpl[G] { this: SmtlibStrLt[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrPrefixOfImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrPrefixOfImpl.scala new file mode 100644 index 0000000000..1cac866c3c --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrPrefixOfImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrPrefixOf, TBool, Type} +import vct.col.print._ + +trait SmtlibStrPrefixOfImpl[G] { this: SmtlibStrPrefixOf[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceAllImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceAllImpl.scala new file mode 100644 index 0000000000..762581ce6f --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceAllImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrReplaceAll, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibStrReplaceAllImpl[G] { this: SmtlibStrReplaceAll[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceImpl.scala new file mode 100644 index 0000000000..997f6f0506 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrReplace, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibStrReplaceImpl[G] { this: SmtlibStrReplace[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceReAllImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceReAllImpl.scala new file mode 100644 index 0000000000..890e812a4c --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceReAllImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrReplaceReAll, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibStrReplaceReAllImpl[G] { this: SmtlibStrReplaceReAll[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceReImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceReImpl.scala new file mode 100644 index 0000000000..5a5bcc1753 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrReplaceReImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrReplaceRe, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibStrReplaceReImpl[G] { this: SmtlibStrReplaceRe[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrSuffixOfImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrSuffixOfImpl.scala new file mode 100644 index 0000000000..25081e1e3e --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrSuffixOfImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrSuffixOf, TBool, Type} +import vct.col.print._ + +trait SmtlibStrSuffixOfImpl[G] { this: SmtlibStrSuffixOf[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrToCodeImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrToCodeImpl.scala new file mode 100644 index 0000000000..ae6d042e5c --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrToCodeImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibStrToCode, TInt, Type} +import vct.col.print._ + +trait SmtlibStrToCodeImpl[G] { this: SmtlibStrToCode[G] => + override def t: Type[G] = TInt() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibStrToIntImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibStrToIntImpl.scala new file mode 100644 index 0000000000..f9dc6272c3 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibStrToIntImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.SmtlibStrToInt +import vct.col.ast.{Type, TInt} +import vct.col.print._ + +trait SmtlibStrToIntImpl[G] { this: SmtlibStrToInt[G] => + override def t: Type[G] = TInt() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibSubstrImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibSubstrImpl.scala new file mode 100644 index 0000000000..2e03bd893b --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibSubstrImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibSubstr, TSmtlibString, Type} +import vct.col.print._ + +trait SmtlibSubstrImpl[G] { this: SmtlibSubstr[G] => + override def t: Type[G] = TSmtlibString() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/SmtlibToFpImpl.scala b/src/col/vct/col/ast/lang/smt/SmtlibToFpImpl.scala new file mode 100644 index 0000000000..b402077500 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/SmtlibToFpImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{SmtlibToFp, TSmtlibFloatingPoint, Type} +import vct.col.print._ + +trait SmtlibToFpImpl[G] { this: SmtlibToFp[G] => + override def t: Type[G] = TSmtlibFloatingPoint(exponentBits, mantissaAndSignBits) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3ArrayConstImpl.scala b/src/col/vct/col/ast/lang/smt/Z3ArrayConstImpl.scala new file mode 100644 index 0000000000..7e66c01494 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3ArrayConstImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TSmtlibArray, Type, Z3ArrayConst} +import vct.col.print._ + +trait Z3ArrayConstImpl[G] { this: Z3ArrayConst[G] => + override def t: Type[G] = TSmtlibArray(domain, codomain) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3ArrayMapImpl.scala b/src/col/vct/col/ast/lang/smt/Z3ArrayMapImpl.scala new file mode 100644 index 0000000000..34378e52ee --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3ArrayMapImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3ArrayMap +import vct.col.ast.Type +import vct.col.print._ + +trait Z3ArrayMapImpl[G] { this: Z3ArrayMap[G] => + override def t: Type[G] = ref.ref.decl.returnType + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3ArrayOfFunctionImpl.scala b/src/col/vct/col/ast/lang/smt/Z3ArrayOfFunctionImpl.scala new file mode 100644 index 0000000000..039573e5be --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3ArrayOfFunctionImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TSmtlibArray, Type, Z3ArrayOfFunction} +import vct.col.print._ + +trait Z3ArrayOfFunctionImpl[G] { this: Z3ArrayOfFunction[G] => + override lazy val t: Type[G] = TSmtlibArray(ref.ref.decl.args.map(_.t), ref.ref.decl.returnType) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3BvNandImpl.scala b/src/col/vct/col/ast/lang/smt/Z3BvNandImpl.scala new file mode 100644 index 0000000000..f1e8306c67 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3BvNandImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3BvNand +import vct.col.ast.Type +import vct.col.print._ + +trait Z3BvNandImpl[G] { this: Z3BvNand[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3BvNorImpl.scala b/src/col/vct/col/ast/lang/smt/Z3BvNorImpl.scala new file mode 100644 index 0000000000..5bd1d4248a --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3BvNorImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3BvNor +import vct.col.ast.Type +import vct.col.print._ + +trait Z3BvNorImpl[G] { this: Z3BvNor[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3BvSModImpl.scala b/src/col/vct/col/ast/lang/smt/Z3BvSModImpl.scala new file mode 100644 index 0000000000..bd45e0b858 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3BvSModImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3BvSMod +import vct.col.ast.Type +import vct.col.print._ + +trait Z3BvSModImpl[G] { this: Z3BvSMod[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3BvSRemImpl.scala b/src/col/vct/col/ast/lang/smt/Z3BvSRemImpl.scala new file mode 100644 index 0000000000..0c27e86d69 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3BvSRemImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3BvSRem +import vct.col.ast.Type +import vct.col.print._ + +trait Z3BvSRemImpl[G] { this: Z3BvSRem[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3BvSShrImpl.scala b/src/col/vct/col/ast/lang/smt/Z3BvSShrImpl.scala new file mode 100644 index 0000000000..263d47436d --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3BvSShrImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3BvSShr +import vct.col.ast.Type +import vct.col.print._ + +trait Z3BvSShrImpl[G] { this: Z3BvSShr[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3BvSubImpl.scala b/src/col/vct/col/ast/lang/smt/Z3BvSubImpl.scala new file mode 100644 index 0000000000..5aedad10d3 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3BvSubImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3BvSub +import vct.col.ast.Type +import vct.col.print._ + +trait Z3BvSubImpl[G] { this: Z3BvSub[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3BvXnorImpl.scala b/src/col/vct/col/ast/lang/smt/Z3BvXnorImpl.scala new file mode 100644 index 0000000000..c7ae1bf88c --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3BvXnorImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3BvXnor +import vct.col.ast.Type +import vct.col.print._ + +trait Z3BvXnorImpl[G] { this: Z3BvXnor[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqAtImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqAtImpl.scala new file mode 100644 index 0000000000..e84795ca88 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqAtImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3SeqAt +import vct.col.ast.Type +import vct.col.print._ + +trait Z3SeqAtImpl[G] { this: Z3SeqAt[G] => + override def t: Type[G] = seq.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqConcatImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqConcatImpl.scala new file mode 100644 index 0000000000..07e6cae874 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqConcatImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3SeqConcat +import vct.col.ast.Type +import vct.col.print._ + +trait Z3SeqConcatImpl[G] { this: Z3SeqConcat[G] => + override def t: Type[G] = left.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqContainsImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqContainsImpl.scala new file mode 100644 index 0000000000..1bb366558e --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqContainsImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TBool, Type, Z3SeqContains} +import vct.col.print._ + +trait Z3SeqContainsImpl[G] { this: Z3SeqContains[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqEmptyImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqEmptyImpl.scala new file mode 100644 index 0000000000..c18ae67472 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqEmptyImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TSmtlibSeq, Type, Z3SeqEmpty} +import vct.col.print._ + +trait Z3SeqEmptyImpl[G] { this: Z3SeqEmpty[G] => + override def t: Type[G] = TSmtlibSeq(elementType) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqExtractImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqExtractImpl.scala new file mode 100644 index 0000000000..cca10c8727 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqExtractImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3SeqExtract +import vct.col.ast.Type +import vct.col.print._ + +trait Z3SeqExtractImpl[G] { this: Z3SeqExtract[G] => + override def t: Type[G] = seq.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqFoldlIImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqFoldlIImpl.scala new file mode 100644 index 0000000000..6eee420cdc --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqFoldlIImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3SeqFoldlI +import vct.col.ast.Type +import vct.col.print._ + +trait Z3SeqFoldlIImpl[G] { this: Z3SeqFoldlI[G] => + override def t: Type[G] = seq.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqFoldlImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqFoldlImpl.scala new file mode 100644 index 0000000000..490033367b --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqFoldlImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3SeqFoldl +import vct.col.ast.Type +import vct.col.print._ + +trait Z3SeqFoldlImpl[G] { this: Z3SeqFoldl[G] => + override def t: Type[G] = seq.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqLenImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqLenImpl.scala new file mode 100644 index 0000000000..6909a9126d --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqLenImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TInt, Type, Z3SeqLen} +import vct.col.print._ + +trait Z3SeqLenImpl[G] { this: Z3SeqLen[G] => + override def t: Type[G] = TInt() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqMapIImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqMapIImpl.scala new file mode 100644 index 0000000000..07dbed77e3 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqMapIImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TSmtlibSeq, Type, Z3SeqMapI} +import vct.col.print._ + +trait Z3SeqMapIImpl[G] { this: Z3SeqMapI[G] => + override lazy val t: Type[G] = TSmtlibSeq(f.t.asSmtlibArray.get.value) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqMapImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqMapImpl.scala new file mode 100644 index 0000000000..76aa2ddb5c --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqMapImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TSmtlibSeq, Type, Z3SeqMap} +import vct.col.print._ + +trait Z3SeqMapImpl[G] { this: Z3SeqMap[G] => + override def t: Type[G] = TSmtlibSeq(f.t.asSmtlibArray.get.value) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqNthImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqNthImpl.scala new file mode 100644 index 0000000000..2e2112e5ab --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqNthImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3SeqNth +import vct.col.ast.Type +import vct.col.print._ + +trait Z3SeqNthImpl[G] { this: Z3SeqNth[G] => + override def t: Type[G] = seq.t.asSmtlibSeq.get.element + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqPrefixOfImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqPrefixOfImpl.scala new file mode 100644 index 0000000000..c018bc25e9 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqPrefixOfImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TBool, Type, Z3SeqPrefixOf} +import vct.col.print._ + +trait Z3SeqPrefixOfImpl[G] { this: Z3SeqPrefixOf[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqReplaceImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqReplaceImpl.scala new file mode 100644 index 0000000000..63cb40d60e --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqReplaceImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.Z3SeqReplace +import vct.col.ast.Type +import vct.col.print._ + +trait Z3SeqReplaceImpl[G] { this: Z3SeqReplace[G] => + override def t: Type[G] = haystack.t + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqSuffixOfImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqSuffixOfImpl.scala new file mode 100644 index 0000000000..8cbc914425 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqSuffixOfImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TBool, Type, Z3SeqSuffixOf} +import vct.col.print._ + +trait Z3SeqSuffixOfImpl[G] { this: Z3SeqSuffixOf[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3SeqUnitImpl.scala b/src/col/vct/col/ast/lang/smt/Z3SeqUnitImpl.scala new file mode 100644 index 0000000000..75fcd50531 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3SeqUnitImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TSmtlibSeq, Type, Z3SeqUnit} +import vct.col.print._ + +trait Z3SeqUnitImpl[G] { this: Z3SeqUnit[G] => + override def t: Type[G] = TSmtlibSeq(arg.t) + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/lang/smt/Z3TransitiveClosureImpl.scala b/src/col/vct/col/ast/lang/smt/Z3TransitiveClosureImpl.scala new file mode 100644 index 0000000000..58ee5d50a3 --- /dev/null +++ b/src/col/vct/col/ast/lang/smt/Z3TransitiveClosureImpl.scala @@ -0,0 +1,9 @@ +package vct.col.ast.lang.smt + +import vct.col.ast.{TBool, Type, Z3TransitiveClosure} +import vct.col.print._ + +trait Z3TransitiveClosureImpl[G] { this: Z3TransitiveClosure[G] => + override def t: Type[G] = TBool() + // def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala index c61d029ba1..e5f01d072b 100644 --- a/src/col/vct/col/ast/type/typeclass/TypeImpl.scala +++ b/src/col/vct/col/ast/type/typeclass/TypeImpl.scala @@ -26,6 +26,10 @@ trait TypeImpl[G] { this: Type[G] => def asModel: Option[TModel[G]] = CoercionUtils.getAnyModelCoercion(this).map(_._2) def asClass: Option[TClass[G]] = CoercionUtils.getAnyClassCoercion(this).map(_._2) def asEither: Option[TEither[G]] = CoercionUtils.getAnyEitherCoercion(this).map(_._2) + def asBitvec: Option[TSmtlibBitVector[G]] = CoercionUtils.getAnyBitvecCoercion(this).map(_._2) + def asSmtlibFloat: Option[TSmtlibFloatingPoint[G]] = CoercionUtils.getAnySmtlibFloatCoercion(this).map(_._2) + def asSmtlibArray: Option[TSmtlibArray[G]] = CoercionUtils.getAnySmtlibArrayCoercion(this).map(_._2) + def asSmtlibSeq: Option[TSmtlibSeq[G]] = CoercionUtils.getAnySmtlibSeqCoercion(this).map(_._2) /*def asVector: Option[TVector] = optMatch(this) { case vec: TVector => vec }*/ def particularize(substitutions: Map[Variable[G], Type[G]]): Type[G] = { diff --git a/src/col/vct/col/rewrite/NonLatchingRewriter.scala b/src/col/vct/col/rewrite/NonLatchingRewriter.scala index 8ae596dd78..a5fc43f125 100644 --- a/src/col/vct/col/rewrite/NonLatchingRewriter.scala +++ b/src/col/vct/col/rewrite/NonLatchingRewriter.scala @@ -32,6 +32,7 @@ class NonLatchingRewriter[Pre, Post]() extends AbstractRewriter[Pre, Post] { override def dispatch(location: Location[Pre]): Location[Post] = rewriteDefault(location) override def dispatch(language: ProverLanguage[Pre]): ProverLanguage[Post] = rewriteDefault(language) + override def dispatch(func: SmtlibFunctionSymbol[Pre]): SmtlibFunctionSymbol[Post] = rewriteDefault(func) override def dispatch(node: CDeclarator[Pre]): CDeclarator[Post] = rewriteDefault(node) override def dispatch(cDeclSpec: CDeclarationSpecifier[Pre]): CDeclarationSpecifier[Post] = rewriteDefault(cDeclSpec) diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index a17f6aa32c..21984d108d 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -236,6 +236,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr case node: LlvmFunctionContract[Pre] => node case node: LlvmLoopContract[Pre] => node case node: ProverLanguage[Pre] => node + case node: SmtlibFunctionSymbol[Pre] => node } def preCoerce(e: Expr[Pre]): Expr[Pre] = e @@ -410,6 +411,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr def postCoerce(node: ProverLanguage[Pre]): ProverLanguage[Post] = rewriteDefault(node) override final def dispatch(node: ProverLanguage[Pre]): ProverLanguage[Post] = postCoerce(coerce(preCoerce(node))) + def preCoerce(node: SmtlibFunctionSymbol[Pre]): SmtlibFunctionSymbol[Pre] = node + def postCoerce(node: SmtlibFunctionSymbol[Pre]): SmtlibFunctionSymbol[Post] = rewriteDefault(node) + override final def dispatch(node: SmtlibFunctionSymbol[Pre]): SmtlibFunctionSymbol[Post] = postCoerce(coerce(preCoerce(node))) def coerce(value: Expr[Pre], target: Type[Pre]): Expr[Pre] = ApplyCoercion(value, CoercionUtils.getCoercion(value.t, target) match { @@ -515,6 +519,38 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr case Some((coercion, t)) => (ApplyCoercion(e, coercion)(CoercionOrigin(e)), t) case None => throw IncoercibleText(e, s"either") } + def bitvec(e: Expr[Pre]): (Expr[Pre], TSmtlibBitVector[Pre]) = + CoercionUtils.getAnyBitvecCoercion(e.t) match { + case Some((coercion, t)) => (ApplyCoercion(e, coercion)(CoercionOrigin(e)), t) + case None => throw IncoercibleText(e, s"(_ BitVec ?)") + } + def bitvec2[T](e1: Expr[Pre], e2: Expr[Pre], f: (Expr[Pre], Expr[Pre]) => T): T = { + val (e1c, t) = bitvec(e1) + val e2c = coerce(e2, t) + f(e1c, e2c) + } + def fp(e: Expr[Pre]): (Expr[Pre], TSmtlibFloatingPoint[Pre]) = + CoercionUtils.getAnySmtlibFloatCoercion(e.t) match { + case Some((coercion, t)) => (ApplyCoercion(e, coercion)(CoercionOrigin(e)), t) + case None => throw IncoercibleText(e, s"(_ FloatingPoint ? ?)") + } + def fp2[T](e1: Expr[Pre], e2: Expr[Pre], f: (Expr[Pre], Expr[Pre]) => T): T = { + val (e1c, t) = fp(e1) + val e2c = coerce(e2, t) + f(e1c, e2c) + } + def reglan(e: Expr[Pre]): Expr[Pre] = coerce(e, TSmtlibRegLan()) + def smtstr(e: Expr[Pre]): Expr[Pre] = coerce(e, TSmtlibString()) + def smtarr(e: Expr[Pre]): (Expr[Pre], TSmtlibArray[Pre]) = + CoercionUtils.getAnySmtlibArrayCoercion(e.t) match { + case Some((coercion, t)) => (ApplyCoercion(e, coercion)(CoercionOrigin(e)), t) + case None => throw IncoercibleText(e, s"(Array ? ?)") + } + def z3seq(e: Expr[Pre]): (Expr[Pre], TSmtlibSeq[Pre]) = + CoercionUtils.getAnySmtlibSeqCoercion(e.t) match { + case Some((coercion, t)) => (ApplyCoercion(e, coercion)(CoercionOrigin(e)), t) + case None => throw IncoercibleText(e, s"(Seq ?)") + } def firstOkHelper[T](thing: Either[Seq[CoercionError], T], onError: => T): Either[Seq[CoercionError], T] = thing match { @@ -1243,6 +1279,105 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr Size(sized(obj)._1) case Slice(xs, from, to) => Slice(seq(xs)._1, int(from), int(to)) + case SmtlibBitvecLiteral(data) => SmtlibBitvecLiteral(data) + case SmtlibBvAdd(left, right) => bitvec2(left, right, SmtlibBvAdd(_, _)) + case SmtlibBvAnd(left, right) => bitvec2(left, right, SmtlibBvAnd(_, _)) + case SmtlibBvMul(left, right) => bitvec2(left, right, SmtlibBvMul(_, _)) + case SmtlibBvNeg(bv) => SmtlibBvNeg(bitvec(bv)._1) + case SmtlibBvNot(bv) => SmtlibBvNot(bitvec(bv)._1) + case SmtlibBvOr(left, right) => bitvec2(left, right, SmtlibBvOr(_, _)) + case SmtlibBvShl(left, right) => bitvec2(left, right, SmtlibBvShl(_, _)) + case SmtlibBvShr(left, right) => bitvec2(left, right, SmtlibBvShr(_, _)) + case SmtlibBvUDiv(left, right) => bitvec2(left, right, SmtlibBvUDiv(_, _)) + case SmtlibBvULt(left, right) => bitvec2(left, right, SmtlibBvULt(_, _)) + case SmtlibBvURem(left, right) => bitvec2(left, right, SmtlibBvURem(_, _)) + case SmtlibConcat(left, right) => bitvec2(left, right, SmtlibConcat(_, _)) + case SmtlibExtract(inclusiveEndIndexFromRight, startIndexFromRight, bv) => + SmtlibExtract(inclusiveEndIndexFromRight, startIndexFromRight, bitvec(bv)._1) + case SmtlibFp(sign, exponent, mantissa) => + SmtlibFp(coerce(sign, TSmtlibBitVector(1)), bitvec(exponent)._1, bitvec(mantissa)._1) + case SmtlibFpAbs(arg) => SmtlibFpAbs(fp(arg)._1) + case SmtlibFpAdd(left, right) => fp2(left, right, SmtlibFpAdd(_, _)) + case SmtlibFpCast(arg, exponentBits, mantissaAndSignBits) => + SmtlibFpCast(fp(arg)._1, exponentBits, mantissaAndSignBits) + case SmtlibFpDiv(left, right) => fp2(left, right, SmtlibFpDiv(_, _)) + case SmtlibFpEq(left, right) => fp2(left, right, SmtlibFpEq(_, _)) + case SmtlibFpFma(left, right, addend) => + val (leftc, t) = fp(left) + SmtlibFpFma(left, coerce(right, t), coerce(addend, t)) + case SmtlibFpFromReal(arg, e, m) => SmtlibFpFromReal(rat(arg), e, m) + case SmtlibFpFromSInt(bv, e, m) => SmtlibFpFromSInt(bitvec(bv)._1, e, m) + case SmtlibFpFromUInt(bv, e, m) => SmtlibFpFromUInt(bitvec(bv)._1, e, m) + case SmtlibFpGeq(left, right) => fp2(left, right, SmtlibFpGeq(_, _)) + case SmtlibFpGt(left, right) => fp2(left, right, SmtlibFpGt(_, _)) + case SmtlibFpIsInfinite(arg) => SmtlibFpIsInfinite(fp(arg)._1) + case SmtlibFpIsNaN(arg) => SmtlibFpIsNaN(fp(arg)._1) + case SmtlibFpIsNegative(arg) => SmtlibFpIsNegative(fp(arg)._1) + case SmtlibFpIsNormal(arg) => SmtlibFpIsNormal(fp(arg)._1) + case SmtlibFpIsPositive(arg) => SmtlibFpIsPositive(fp(arg)._1) + case SmtlibFpIsSubnormal(arg) => SmtlibFpIsSubnormal(fp(arg)._1) + case SmtlibFpIsZero(arg) => SmtlibFpIsZero(fp(arg)._1) + case SmtlibFpLeq(left, right) => fp2(left, right, SmtlibFpLeq(_, _)) + case SmtlibFpLt(left, right) => fp2(left, right, SmtlibFpLt(_, _)) + case SmtlibFpMax(left, right) => fp2(left, right, SmtlibFpMax(_, _)) + case SmtlibFpMin(left, right) => fp2(left, right, SmtlibFpMin(_, _)) + case SmtlibFpMul(left, right) => fp2(left, right, SmtlibFpMul(_, _)) + case SmtlibFpNeg(arg) => SmtlibFpNeg(fp(arg)._1) + case SmtlibFpRem(left, right) => fp2(left, right, SmtlibFpRem(_, _)) + case SmtlibFpRoundToIntegral(arg) => SmtlibFpRoundToIntegral(fp(arg)._1) + case SmtlibFpSqrt(arg) => SmtlibFpSqrt(fp(arg)._1) + case SmtlibFpSub(left, right) => fp2(left, right, SmtlibFpSub(_, _)) + case SmtlibFpToReal(arg) => SmtlibFpToReal(fp(arg)._1) + case SmtlibFpToSInt(arg, bits) => SmtlibFpToSInt(fp(arg)._1, bits) + case SmtlibFpToUInt(arg, bits) => SmtlibFpToUInt(fp(arg)._1, bits) + case SmtlibLiteralString(data) => SmtlibLiteralString(data) + case SmtlibReAll() => SmtlibReAll() + case SmtlibReAllChar() => SmtlibReAllChar() + case SmtlibReComp(arg) => SmtlibReComp(reglan(arg)) + case SmtlibReConcat(left, right) => SmtlibReConcat(reglan(left), reglan(right)) + case SmtlibReContains(re, str) => SmtlibReContains(reglan(re), smtstr(str)) + case SmtlibReDiff(left, right) => SmtlibReDiff(reglan(left), reglan(right)) + case SmtlibReFromStr(arg) => SmtlibReFromStr(smtstr(arg)) + case SmtlibReInter(left, right) => SmtlibReInter(reglan(left), reglan(right)) + case SmtlibReNone() => SmtlibReNone() + case SmtlibReOpt(arg) => SmtlibReOpt(reglan(arg)) + case SmtlibRePlus(arg) => SmtlibRePlus(reglan(arg)) + case SmtlibReRange(left, right) => SmtlibReRange(smtstr(left), smtstr(right)) + case SmtlibReRepeat(count, arg) => SmtlibReRepeat(count, reglan(arg)) + case SmtlibReRepeatRange(from, to, arg) => SmtlibReRepeatRange(from, to, reglan(arg)) + case SmtlibReStar(arg) => SmtlibReStar(reglan(arg)) + case SmtlibReUnion(left, right) => SmtlibReUnion(reglan(left), reglan(right)) + case SmtlibRNA() => SmtlibRNA() + case SmtlibRNE() => SmtlibRNE() + case SmtlibRTN() => SmtlibRTN() + case SmtlibRTP() => SmtlibRTP() + case SmtlibRTZ() => SmtlibRTZ() + case SmtlibSelect(arr, i) => + val (e, t) = smtarr(arr) + SmtlibSelect(e, i.zip(t.index).map { case (e, t) => coerce(e, t) }) + case SmtlibStore(arr, i, x) => + val (e, t) = smtarr(arr) + SmtlibStore(e, i.zip(t.index).map { case (e, t) => coerce(e, t) }, coerce(x, t.value)) + case SmtlibStrAt(str, i) => SmtlibStrAt(smtstr(str), int(i)) + case SmtlibStrConcat(left, right) => SmtlibStrConcat(smtstr(left), smtstr(right)) + case SmtlibStrContains(left, right) => SmtlibStrContains(smtstr(left), smtstr(right)) + case SmtlibStrFromCode(arg) => SmtlibStrFromCode(int(arg)) + case SmtlibStrFromInt(arg) => SmtlibStrFromInt(int(arg)) + case SmtlibStrIndexOf(haystack, needle, fromIndex) => SmtlibStrIndexOf(smtstr(haystack), smtstr(needle), int(fromIndex)) + case SmtlibStrIsDigit(arg) => SmtlibStrIsDigit(smtstr(arg)) + case SmtlibStrLen(arg) => SmtlibStrLen(smtstr(arg)) + case SmtlibStrLeq(left, right) => SmtlibStrLeq(smtstr(left), smtstr(right)) + case SmtlibStrLt(left, right) => SmtlibStrLt(smtstr(left), smtstr(right)) + case SmtlibStrPrefixOf(left, right) => SmtlibStrPrefixOf(smtstr(left), smtstr(right)) + case SmtlibStrReplace(haystack, needle, replacement) => SmtlibStrReplace(smtstr(haystack), smtstr(needle), smtstr(replacement)) + case SmtlibStrReplaceAll(haystack, needle, replacement) => SmtlibStrReplaceAll(smtstr(haystack), smtstr(needle), smtstr(replacement)) + case SmtlibStrReplaceRe(haystack, re, replacement) => SmtlibStrReplaceRe(smtstr(haystack), reglan(re), smtstr(replacement)) + case SmtlibStrReplaceReAll(haystack, re, replacement) => SmtlibStrReplaceReAll(smtstr(haystack), reglan(re), smtstr(replacement)) + case SmtlibStrSuffixOf(left, right) => SmtlibStrSuffixOf(smtstr(left), smtstr(right)) + case SmtlibStrToCode(arg) => SmtlibStrToCode(smtstr(arg)) + case SmtlibStrToInt(arg) => SmtlibStrToInt(smtstr(arg)) + case SmtlibSubstr(str, i, n) => SmtlibSubstr(smtstr(str), int(i), int(n)) + case SmtlibToFp(bv, e, m) => SmtlibToFp(coerce(bv, TSmtlibBitVector(e + m)), e, m) case Star(left, right) => Star(res(left), res(right)) case starall @ Starall(bindings, triggers, body) => @@ -1336,6 +1471,46 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr With(pre, value) case WritePerm() => WritePerm() + case Z3ArrayConst(domain, codomain, value) => Z3ArrayConst(domain, codomain, coerce(value, codomain)) + case Z3ArrayMap(ref, Nil) => Z3ArrayMap(ref, Nil) + case Z3ArrayMap(ref, arg +: args) => + val (_, TSmtlibArray(keyType, _)) = smtarr(arg) + val ts = ref.ref.decl.args.map(_.t).map(TSmtlibArray(keyType, _)) + Z3ArrayMap(ref, (arg +: args).zip(ts).map { case (e, t) => coerce(e, t) }) + case Z3ArrayOfFunction(ref) => Z3ArrayOfFunction(ref) + case Z3BvNand(left, right) => bitvec2(left, right, Z3BvNand(_, _)) + case Z3BvNor(left, right) => bitvec2(left, right, Z3BvNor(_, _)) + case Z3BvSMod(left, right) => bitvec2(left, right, Z3BvSMod(_, _)) + case Z3BvSRem(left, right) => bitvec2(left, right, Z3BvSRem(_, _)) + case Z3BvSShr(left, right) => bitvec2(left, right, Z3BvSShr(_, _)) + case Z3BvSub(left, right) => bitvec2(left, right, Z3BvSub(_, _)) + case Z3BvXnor(left, right) => bitvec2(left, right, Z3BvXnor(_, _)) + case Z3SeqAt(seq, offset) => Z3SeqAt(z3seq(seq)._1, int(offset)) + case Z3SeqConcat(left, right) => Z3SeqConcat(z3seq(left)._1, z3seq(right)._1) + case Z3SeqContains(seq, subseq) => Z3SeqContains(z3seq(seq)._1, z3seq(subseq)._1) + case Z3SeqEmpty(elementType) => Z3SeqEmpty(elementType) + case Z3SeqExtract(seq, offset, len) => Z3SeqExtract(z3seq(seq)._1, int(offset), int(len)) + case Z3SeqFoldl(f, base, seq) => + val (cseq, seqt) = z3seq(seq) + Z3SeqFoldl(coerce(f, TSmtlibArray(Seq(base.t, seqt.element), base.t)), base, cseq) + case Z3SeqFoldlI(f, offset, base, seq) => + val (cseq, seqt) = z3seq(seq) + Z3SeqFoldlI(coerce(f, TSmtlibArray(Seq(TInt(), base.t, seqt.element), base.t)), int(offset), base, cseq) + case Z3SeqLen(arg) => Z3SeqLen(z3seq(arg)._1) + case Z3SeqMap(f, seq) => + val (cf, arrt) = smtarr(f) + if(arrt.index.size != 1) coerce(f, TSmtlibArray(Seq(TAny()), arrt.value)) + Z3SeqMap(cf, coerce(seq, TSmtlibSeq(arrt.index.head))) + case Z3SeqMapI(f, offset, seq) => + val (cf, arrt) = smtarr(f) + if(arrt.index.size != 2) coerce(f, TSmtlibArray(Seq(TInt(), TAny()), arrt.value)) + Z3SeqMapI(cf, int(offset), coerce(seq, TSmtlibSeq(arrt.index(1)))) + case Z3SeqNth(seq, offset) => Z3SeqNth(z3seq(seq)._1, int(offset)) + case Z3SeqPrefixOf(pre, subseq) => Z3SeqPrefixOf(z3seq(pre)._1, z3seq(subseq)._1) + case Z3SeqReplace(haystack, needle, replacement) => Z3SeqReplace(z3seq(haystack)._1, z3seq(needle)._1, z3seq(replacement)._1) + case Z3SeqSuffixOf(post, seq) => Z3SeqSuffixOf(z3seq(post)._1, z3seq(seq)._1) + case Z3SeqUnit(arg) => Z3SeqUnit(arg) + case Z3TransitiveClosure(ref, args) => Z3TransitiveClosure(ref, coerceArgs(args, ref.ref.decl)) case VeyMontCondition(c) => VeyMontCondition(c) case localIncoming: BipLocalIncomingData[Pre] => localIncoming case glue: JavaBipGlue[Pre] => glue @@ -1570,37 +1745,9 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr Program(decl)(node.blame) } - def coerce(node: Type[Pre]): Type[Pre] = { - implicit val o: Origin = node.o - node match { - case value: TNotAValue[_] => - value - case TUnion(types) => - TUnion(types) - case TArray(element) => - TArray(element) - case TPointer(element) => - TPointer(element) - case TType(t) => - TType(t) - case TVar(ref) => - TVar(ref) - case compositeType: CompositeType[_] => - compositeType - case primitiveType: PrimitiveType[_] => - primitiveType - case declaredType: DeclaredType[_] => - declaredType - case cType: CType[_] => - cType - case javaType: JavaType[_] => - javaType - case lType: PVLType[_] => - lType - case silverType: SilverType[_] => - silverType - } - } + // PB: types may very well contain expressions eventually, but for now they don't. + def coerce(node: Type[Pre]): Type[Pre] = + node def coerce(node: LoopContract[Pre]): LoopContract[Pre] = { implicit val o: Origin = node.o @@ -1837,4 +1984,5 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr def coerce(node: LlvmLoopContract[Pre]): LlvmLoopContract[Pre] = node def coerce(node: ProverLanguage[Pre]): ProverLanguage[Pre] = node + def coerce(node: SmtlibFunctionSymbol[Pre]): SmtlibFunctionSymbol[Pre] = node } diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 14bcad6097..6d87e9f72f 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -274,4 +274,28 @@ case object CoercionUtils { case t: TEither[G] => Some((CoerceIdentity(source), t)) case _ => None } + + def getAnyBitvecCoercion[G](source: Type[G]): Option[(Coercion[G], TSmtlibBitVector[G])] = source match { + case t: CPrimitiveType[G] => chainCCoercion(t, getAnyBitvecCoercion) + case t: TSmtlibBitVector[G] => Some((CoerceIdentity(source), t)) + case _ => None + } + + def getAnySmtlibFloatCoercion[G](source: Type[G]): Option[(Coercion[G], TSmtlibFloatingPoint[G])] = source match { + case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibFloatCoercion) + case t: TSmtlibFloatingPoint[G] => Some((CoerceIdentity(source), t)) + case _ => None + } + + def getAnySmtlibArrayCoercion[G](source: Type[G]): Option[(Coercion[G], TSmtlibArray[G])] = source match { + case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibArrayCoercion) + case t: TSmtlibArray[G] => Some((CoerceIdentity(source), t)) + case _ => None + } + + def getAnySmtlibSeqCoercion[G](source: Type[G]): Option[(Coercion[G], TSmtlibSeq[G])] = source match { + case t: CPrimitiveType[G] => chainCCoercion(t, getAnySmtlibSeqCoercion) + case t: TSmtlibSeq[G] => Some((CoerceIdentity(source), t)) + case _ => None + } } \ No newline at end of file diff --git a/src/colhelper/ColDefs.scala b/src/colhelper/ColDefs.scala index 1fa373be47..b1cd9c6172 100644 --- a/src/colhelper/ColDefs.scala +++ b/src/colhelper/ColDefs.scala @@ -18,6 +18,7 @@ object ColDefs { q"import vct.col.ref.Ref", q"import vct.col.resolve.ctx.Referrable", q"import vct.col.origin.ExpectedError", + q"import hre.data.BitString", ) /** diff --git a/src/colhelper/ColDescription.scala b/src/colhelper/ColDescription.scala index cc557213ef..762e673789 100644 --- a/src/colhelper/ColDescription.scala +++ b/src/colhelper/ColDescription.scala @@ -133,7 +133,8 @@ class ColDescription { q"rewriter.porcelainRefSucc[$decl[Post]]($term).getOrElse(rewriter.succ[${Type.Name(tDecl)}[Post]]($term.decl))" else q"rewriter.porcelainRefSucc[$decl[Post]]($term).getOrElse(rewriter.anySucc[${Type.Name(tDecl)}[Post]]($term.decl))" - case Type.Name("Int") | Type.Name("String") | Type.Name("Boolean") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") => + case Type.Name("Int") | Type.Name("String") | Type.Name("Boolean") | Type.Name("BigInt") | Type.Name("BigDecimal") | + Type.Name("BitString") | Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") => term case Type.Apply(Type.Name("Either"), List(t1, t2)) => q"$term.left.map(l => ${rewriteDefault(q"l", t1)}).map(r => ${rewriteDefault(q"r", t2)})" diff --git a/src/colhelper/ColHelperComparator.scala b/src/colhelper/ColHelperComparator.scala index 8f8f30be80..63dc9dae98 100644 --- a/src/colhelper/ColHelperComparator.scala +++ b/src/colhelper/ColHelperComparator.scala @@ -9,7 +9,9 @@ case class ColHelperComparator(info: ColDescription) extends ColHelperMaker { case Type.Apply(Type.Name("Ref"), _) => q"true" - case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") | Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") => q"$left == $right" + case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") | + Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") | Type.Name("BitString") => + q"$left == $right" case Type.Apply(Type.Name("Seq"), List(inner)) => q"$left.size == $right.size && $left.zip($right).forall { case (left, right) => ${valueEqual(inner, q"left", q"right")} }" @@ -42,7 +44,9 @@ case class ColHelperComparator(info: ColDescription) extends ColHelperMaker { case Type.Apply(Type.Name("Ref"), _) => q"LazyList(Comparator.MatchingReference($left.decl, $right.decl))" case Type.Apply(Type.Name(name), List(Type.Name("G"))) if info.supports("Node")(name) => q"LazyList.empty" - case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") | Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") => q"LazyList.empty" + case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") | + Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") | Type.Name("BitString") => + q"LazyList.empty" case Type.Apply(Type.Name("Seq"), List(inner)) => q"$left.zip($right).to(LazyList).flatMap { case (left, right) => ${refEqual(inner, q"left", q"right")} }" @@ -73,7 +77,9 @@ case class ColHelperComparator(info: ColDescription) extends ColHelperMaker { case Type.Apply(Type.Name(name), List(Type.Name("G"))) if info.supports("Node")(name) => q"Comparator.compare($left, $right)" case Type.Apply(Type.Name("Ref"), _) => q"LazyList.empty" - case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") | Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") => q"LazyList.empty" + case Type.Name("Int") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Name("String") | Type.Name("Boolean") | + Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Name("ExpectedError") | Type.Name("BitString") => + q"LazyList.empty" case Type.Apply(Type.Name("Seq"), List(inner)) => q"$left.zip($right).to(LazyList).flatMap { case (left, right) => ${nodeEqual(inner, q"left", q"right")} }" diff --git a/src/colhelper/ColHelperDeserialize.scala b/src/colhelper/ColHelperDeserialize.scala index 92d7847ab0..4045b4c099 100644 --- a/src/colhelper/ColHelperDeserialize.scala +++ b/src/colhelper/ColHelperDeserialize.scala @@ -41,6 +41,7 @@ case class ColHelperDeserialize(info: ColDescription, proto: ColProto) extends C case proto.TBigInt => q"BigInt(new java.math.BigInteger($term.data.toByteArray()))" case proto.TBigDecimal => q"BigDecimal(${deserializeTerm(q"$term.unscaledValue", proto.TBigInt, null)}, $term.scale)" case proto.TString => term + case proto.TBitString => q"new BitString($term.data.toByteArray(), $term.skipAtLastByte)" case proto.TOption(t) => q"$term.map[${lastTypeArg(scalaTyp)}](e => ${deserializeTerm(q"e", t, lastTypeArg(scalaTyp))})" case proto.TSeq(t) => q"$term.map[${lastTypeArg(scalaTyp)}](e => ${deserializeTerm(q"e", t, lastTypeArg(scalaTyp))})" case proto.TSet(t) => q"$term.map[${lastTypeArg(scalaTyp)}](e => ${deserializeTerm(q"e", t, lastTypeArg(scalaTyp))}).toSet" diff --git a/src/colhelper/ColHelperSerialize.scala b/src/colhelper/ColHelperSerialize.scala index 04510016a1..86c070156e 100644 --- a/src/colhelper/ColHelperSerialize.scala +++ b/src/colhelper/ColHelperSerialize.scala @@ -45,6 +45,7 @@ case class ColHelperSerialize(info: ColDescription, proto: ColProto) extends Col case proto.TBigInt => q"ser.BigInt(com.google.protobuf.ByteString.copyFrom($term.toByteArray))" case proto.TBigDecimal => q"ser.BigDecimal($term.scale, ser.BigInt(com.google.protobuf.ByteString.copyFrom($term.underlying().unscaledValue().toByteArray())))" case proto.TString => term + case proto.TBitString => q"ser.BitString(com.google.protobuf.ByteString.copyFrom($term.rawData), $term.skipAtLastByte)" case proto.TOption(t) => q"$term.map(e => ${serializeTerm(q"e", t)})" case proto.TSeq(t) => q"$term.map(e => ${serializeTerm(q"e", t)})" case proto.TSet(t) => q"$term.toSeq.map(e => ${serializeTerm(q"e", t)})" diff --git a/src/colhelper/ColHelperSubnodes.scala b/src/colhelper/ColHelperSubnodes.scala index 03f31d1eb3..02f7634725 100644 --- a/src/colhelper/ColHelperSubnodes.scala +++ b/src/colhelper/ColHelperSubnodes.scala @@ -25,7 +25,9 @@ case class ColHelperSubnodes(info: ColDescription) extends ColHelperMaker { } case Type.Apply(Type.Name(typ), List(Type.Name("G"))) if info.supports("NodeFamily")(typ) || info.supports("Declaration")(typ) => Some(node => q"Seq($node)") - case Type.Name("Int") | Type.Name("String") | Type.Name("Boolean") | Type.Name("BigInt") | Type.Name("BigDecimal") | Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Apply(Type.Name("Ref"), _) | Type.Name("ExpectedError") => + case Type.Name("Int") | Type.Name("String") | Type.Name("Boolean") | Type.Name("BigInt") | Type.Name("BigDecimal") | + Type.Apply(Type.Name("Referrable"), List(Type.Name("G"))) | Type.Apply(Type.Name("Ref"), _) | + Type.Name("ExpectedError") | Type.Name("BitString") => None case Type.Apply(Type.Name("Either"), List(t1, t2)) => val f1 = subnodePatternByType(t1).getOrElse((elem: Term) => q"Nil") diff --git a/src/colhelper/ColProto.scala b/src/colhelper/ColProto.scala index 5339aca3c6..e9d637f6f8 100644 --- a/src/colhelper/ColProto.scala +++ b/src/colhelper/ColProto.scala @@ -28,7 +28,7 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) = sealed trait Typ { def isPrimitive: Boolean = this match { - case TBool | TRef() | TInt | TBigInt | TBigDecimal | TString => true + case TBool | TRef() | TInt | TBigInt | TBigDecimal | TString | TBitString => true case TName(_) => true case TOption(t) if t.isMarkable => true case TSeq(t) if t.isMarkable => true @@ -37,7 +37,7 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) = } def isMarkable: Boolean = this match { - case TBool | TRef() | TInt | TBigInt | TBigDecimal | TString => true + case TBool | TRef() | TInt | TBigInt | TBigDecimal | TString | TBitString => true case TName(_) => true case _ => false } @@ -49,6 +49,7 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) = case TBigInt => "BigInt" case TBigDecimal => "BigDecimal" case TString => "String" + case TBitString => "BitString" case TName(name) => name case TOption(t) => "Opt" + t.toString case TSeq(t) => "Seq" + t.toString @@ -62,6 +63,7 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) = case object TBigInt extends Typ case object TBigDecimal extends Typ case object TString extends Typ + case object TBitString extends Typ case class TRef()(val scalaArg: SType) extends Typ case class TName(name: String) extends Typ case class TOption(t: Typ)(val scalaArg: SType) extends Typ @@ -83,6 +85,7 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) = case SType.Apply(SType.Name("Ref"), List(SType.Name("G"), decl)) => TRef()(decl) case SType.Name("Int") => TInt case SType.Name("String") => TString + case SType.Name("BitString") => TBitString case SType.Name("Boolean") => TBool case SType.Name("BigInt") => TBigInt case SType.Name("BigDecimal") => TBigDecimal @@ -136,6 +139,7 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) = case TBigInt => builder.setTypeName("BigInt") case TBigDecimal => builder.setTypeName("BigDecimal") case TString => builder.setType(PType.TYPE_STRING) + case TBitString => builder.setTypeName("BitString") case TName(name) => builder.setTypeName(name) case TOption(t) => builder.setLabel(FieldDescriptorProto.Label.LABEL_OPTIONAL); setType(builder, t) case TSeq(t) => builder.setLabel(FieldDescriptorProto.Label.LABEL_REPEATED); setType(builder, t) @@ -169,6 +173,10 @@ case class ColProto(info: ColDescription, output: File, writer: (File, String) = .addField(field("scale").setType(PType.TYPE_INT32)) .addField(field("unscaledValue").setTypeName("BigInt")) .build(), + message("BitString") + .addField(field("data").setType(PType.TYPE_BYTES)) + .addField(field("skipAtLastByte").setType(PType.TYPE_INT32)) + .build(), message("Ref") .addField(field("index").setType(PType.TYPE_INT64)) .build(), diff --git a/src/hre/hre/data/BitString.scala b/src/hre/hre/data/BitString.scala new file mode 100644 index 0000000000..b4071d2e30 --- /dev/null +++ b/src/hre/hre/data/BitString.scala @@ -0,0 +1,105 @@ +package hre.data + +object BitString { + def apply(input: String): BitString = { + val bytes = if(input.length % 8 == 0) input.length / 8 else input.length / 8 + 1 + val skip = if(input.length % 8 == 0) 0 else 8 - (input.length % 8) + val buf = new Array[Byte](bytes) + for(i <- 0 until bytes) { + val value = + (if(input(i*8+0) == '1') -128 else 0) + + (if(input(i*8+1) == '1') 64 else 0) + + (if(input(i*8+2) == '1') 32 else 0) + + (if(input(i*8+3) == '1') 16 else 0) + + (if(input(i*8+4) == '1') 8 else 0) + + (if(input(i*8+5) == '1') 4 else 0) + + (if(input(i*8+6) == '1') 2 else 0) + + (if(input(i*8+7) == '1') 1 else 0) + + buf(i) = value.toByte + } + new BitString(buf, skip) + } +} + +class BitString(val rawData: Array[Byte], val skipAtLastByte: Int) extends Seq[Boolean] { bitString => + + require(0 <= skipAtLastByte && skipAtLastByte < 8) + + def toSmt: String = + if(skipAtLastByte == 0 || skipAtLastByte == 4) toHexSmt + else toBinSmt + + def toHexSmt: String = { + val digit = "0123456789abcdef" + val sb = new StringBuilder("#x") + + for (i <- 0 until rawData.length - 1) { + val b = rawData(i) + sb += digit((b >> 4) & 0xf) + sb += digit((b >> 0) & 0xf) + } + + if (rawData.length > 0) { + val b = rawData.last + + if(skipAtLastByte == 0) { + sb += digit((b >> 4) & 0xf) + sb += digit((b >> 0) & 0xf) + } else { + sb += digit((b >> 4) & 0xf) + } + } + + sb.result() + } + + def toBinSmt: String = { + val bit = "01" + val sb = new StringBuilder("#b") + + for(i <- 0 until rawData.length - 1) { + val b = rawData(i) + sb += bit((b >> 7) & 1) + sb += bit((b >> 6) & 1) + sb += bit((b >> 5) & 1) + sb += bit((b >> 4) & 1) + sb += bit((b >> 3) & 1) + sb += bit((b >> 2) & 1) + sb += bit((b >> 1) & 1) + sb += bit((b >> 0) & 1) + } + + if(rawData.length > 0) { + val b = rawData.last + for(offset <- (skipAtLastByte until 8).reverse) { + sb += bit((b >> offset) & 1) + } + } + + sb.result() + } + + override def apply(i: Int): Boolean = { + if(i < 0 || i >= length) + throw new IndexOutOfBoundsException(i) + + (rawData(i / 8) >> (i % 8)) > 0 + } + + override def length: Int = rawData.length * 8 - skipAtLastByte + + class BitStringIterator extends Iterator[Boolean] { + private var index: Int = 0 + + override def hasNext: Boolean = index < bitString.length + override def next(): Boolean = + try { + bitString(index) + } finally { + index += 1 + } + } + + override def iterator: Iterator[Boolean] = new BitStringIterator +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/SmtlibToProverTypes.scala b/src/rewrite/vct/rewrite/SmtlibToProverTypes.scala new file mode 100644 index 0000000000..1bc7630e32 --- /dev/null +++ b/src/rewrite/vct/rewrite/SmtlibToProverTypes.scala @@ -0,0 +1,203 @@ +package vct.rewrite + +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} + +import scala.collection.mutable +import scala.jdk.StreamConverters.IntStreamHasToScala + +case object SmtlibToProverTypes extends RewriterBuilder { + override def key: String = "smtlib" + override def desc: String = "Encode smtlib types and functions into their stringified counterpart" +} + +case class SmtlibToProverTypes[Pre <: Generation]() extends Rewriter[Pre] { + def smtTypeString(t: Type[Pre]): String = t match { + case TSeq(element) => "$Seq<" + smtTypeString(element) + ">" + case TSet(element) => "$Set<" + smtTypeString(element) + ">" + case TBag(element) => "$Multiset<" + smtTypeString(element) + ">" + case TMap(key, value) => "$Map<" + smtTypeString(key) + "~_" + smtTypeString(value) + ">" + case TBool() => "Bool" + case TRef() => "$Ref" + case TInt() => "Int" + case TRational() => "$Perm" + case TAxiomatic(adt, args) => adt.decl.o.preferredName + "<" + args.map(smtTypeString).mkString("~_") + ">" + case TProverType(ref) => ref.decl.interpretation.collectFirst { case (SmtLib(), int) => int }.get + case TSmtlibArray(index, value) => s"(Array ${index.map(smtTypeString).mkString(" ")} ${smtTypeString(value)})" + case TSmtlibBitVector(size) => s"(_ BitVec $size)" + case TSmtlibRoundingMode() => "RoundingMode" + case TSmtlibFloatingPoint(exponentBits, mantissaAndSignBits) => s"(_ FloatingPoint $exponentBits $mantissaAndSignBits)" + case TSmtlibString() => "String" + case TSmtlibRegLan() => "RegLan" + case TSmtlibSeq(element) => s"(Seq ${smtTypeString(element)})" + } + + val declaredType: mutable.Map[String, ProverType[Post]] = mutable.Map() + val declaredFunc: mutable.Map[(String, Seq[Type[Pre]]), ProverFunction[Post]] = mutable.Map() + + def getType(t: Type[Pre]): TProverType[Post] = { + val asText = smtTypeString(t) + TProverType(declaredType.getOrElseUpdate(asText, { + implicit val o: Origin = t.o + globalDeclarations.declare(new ProverType[Post](Seq(SmtLib[Post]() -> asText))) + }).ref) + } + + def getExpr(e: Expr[Pre], f: String, args: Expr[Pre]*)(implicit o: Origin): Expr[Post] = + ProverFunctionInvocation(declaredFunc.getOrElseUpdate((f, args.map(_.t)), { + globalDeclarations.declare(new ProverFunction[Post]( + Seq(SmtLib[Post]() -> f), + args.map(arg => new Variable(dispatch(arg.t))), + dispatch(e.t), + )) + }).ref, args.map(dispatch)) + + override def dispatch(t: Type[Pre]): Type[Post] = t match { + case t: SmtlibType[Pre] => getType(t) + case other => rewriteDefault(other) + } + + override def dispatch(e: Expr[Pre]): Expr[Post] = e match { + case e: SmtlibExpr[Pre] => + implicit val o: Origin = e.o + e match { + case SmtlibSelect(arr, is) => getExpr(e, "select", (arr +: is): _*) + case SmtlibStore(arr, is, x) => getExpr(e, "store", (arr +: is) :+ x: _*) + case SmtlibBitvecLiteral(data) => getExpr(e, data.toSmt) + case SmtlibConcat(left, right) => getExpr(e, "concat", left, right) + case SmtlibExtract(inclusiveEndIndexFromRight, startIndexFromRight, bv) => + getExpr(e, s"(_ extract $inclusiveEndIndexFromRight $startIndexFromRight)", bv) + case SmtlibBvNot(bv) => getExpr(e, "bvnot", bv) + case SmtlibBvAnd(left, right) => getExpr(e, "bvand", left, right) + case SmtlibBvOr(left, right) => getExpr(e, "bvor", left, right) + case SmtlibBvNeg(bv) => getExpr(e, "bvneg", bv) + case SmtlibBvAdd(left, right) => getExpr(e, "bvadd", left, right) + case SmtlibBvMul(left, right) => getExpr(e, "bvmul", left, right) + case SmtlibBvUDiv(left, right) => getExpr(e, "bvudiv", left, right) + case SmtlibBvURem(left, right) => getExpr(e, "bvurem", left, right) + case SmtlibBvShl(left, right) => getExpr(e, "bvshl", left, right) + case SmtlibBvShr(left, right) => getExpr(e, "bvshr", left, right) + case SmtlibBvULt(left, right) => getExpr(e, "bvult", left, right) + case SmtlibRNE() => getExpr(e, "RNE") + case SmtlibRNA() => getExpr(e, "RNA") + case SmtlibRTP() => getExpr(e, "RTP") + case SmtlibRTN() => getExpr(e, "RTN") + case SmtlibRTZ() => getExpr(e, "RTZ") + case SmtlibFp(sign, exponent, mantissa) => getExpr(e, "fp", sign, exponent, mantissa) + case SmtlibFpAbs(arg) => getExpr(e, "fp.abs", arg) + case SmtlibFpNeg(arg) => getExpr(e, "fp.neg", arg) + case SmtlibFpAdd(left, right) => getExpr(e, "fp.add", left, right) + case SmtlibFpSub(left, right) => getExpr(e, "fp.sub", left, right) + case SmtlibFpMul(left, right) => getExpr(e, "fp.mul", left, right) + case SmtlibFpDiv(left, right) => getExpr(e, "fp.div", left, right) + case SmtlibFpFma(left, right, addend) => getExpr(e, "fp.fma", left, right, addend) + case SmtlibFpSqrt(arg) => getExpr(e, "fp.sqrt", arg) + case SmtlibFpRem(left, right) => getExpr(e, "fp.rem", left, right) + case SmtlibFpRoundToIntegral(arg) => getExpr(e, "fp.roundToIntegral", arg) + case SmtlibFpMin(left, right) => getExpr(e, "fp.min", left, right) + case SmtlibFpMax(left, right) => getExpr(e, "fp.max", left, right) + case SmtlibFpLeq(left, right) => getExpr(e, "fp.leq", left, right) + case SmtlibFpLt(left, right) => getExpr(e, "fp.lt", left, right) + case SmtlibFpGeq(left, right) => getExpr(e, "fp.geq", left, right) + case SmtlibFpGt(left, right) => getExpr(e, "fp.gt", left, right) + case SmtlibFpEq(left, right) => getExpr(e, "fp.eq", left, right) + case SmtlibFpIsNormal(arg) => getExpr(e, "fp.isNormal", arg) + case SmtlibFpIsSubnormal(arg) => getExpr(e, "fp.isSubnormal", arg) + case SmtlibFpIsZero(arg) => getExpr(e, "fp.isZero", arg) + case SmtlibFpIsInfinite(arg) => getExpr(e, "fp.isInfinite", arg) + case SmtlibFpIsNaN(arg) => getExpr(e, "fp.isNaN", arg) + case SmtlibFpIsNegative(arg) => getExpr(e, "fp.isNegative", arg) + case SmtlibFpIsPositive(arg) => getExpr(e, "fp.isPositive", arg) + case SmtlibToFp(bv, exponentBits, mantissaAndSignBits) => + getExpr(e, s"(_ to_fp $exponentBits $mantissaAndSignBits)", bv) + case SmtlibFpCast(arg, exponentBits, mantissaAndSignBits) => + getExpr(e, s"(_ to_fp $exponentBits $mantissaAndSignBits)", arg) + case SmtlibFpFromReal(arg, exponentBits, mantissaAndSignBits) => + getExpr(e, s"(_ to_fp $exponentBits $mantissaAndSignBits)", arg) + case SmtlibFpFromSInt(bv, exponentBits, mantissaAndSignBits) => + getExpr(e, s"(_ to_fp $exponentBits $mantissaAndSignBits)", bv) + case SmtlibFpFromUInt(bv, exponentBits, mantissaAndSignBits) => + getExpr(e, s"(_ to_fp_unsigned $exponentBits $mantissaAndSignBits)", bv) + case SmtlibFpToReal(arg) => getExpr(e, "fp.to_real", arg) + case SmtlibFpToSInt(arg, bits) => getExpr(e, s"(_ fp.to_sbv $bits)", arg) + case SmtlibFpToUInt(arg, bits) => getExpr(e, s"(_ fp.to_ubv $bits)", arg) + case SmtlibLiteralString(data) => + // PB: it seems "\" need not be escaped, except when an *entire* escape sequence occurs in the string + // literally in the string to be escaped. Here we just escape all backslashes, which is one way of + // ensuring we break up any accidental literal escape sequences :) + val content = data.codePoints().toScala(Seq).map { + case c if 0x20 <= c && c <= 0x7e && c != 0x5c => Character.toString(c) + case c => "\\u{" + c.toHexString + "}" + } + getExpr(e, "\"" + content + "\"") + case SmtlibStrConcat(left, right) => getExpr(e, "str.++", left, right) + case SmtlibStrLen(arg) => getExpr(e, "str.len", arg) + case SmtlibStrLt(left, right) => getExpr(e, "str.<", left, right) + case SmtlibStrLeq(left, right) => getExpr(e, "str.<=", left, right) + case SmtlibStrAt(str, i) => getExpr(e, "str.at", str, i) + case SmtlibSubstr(str, i, n) => getExpr(e, "str.substr", str, i, n) + case SmtlibStrPrefixOf(left, right) => getExpr(e, "str.prefixof", left, right) + case SmtlibStrSuffixOf(left, right) => getExpr(e, "str.suffixof", left, right) + case SmtlibStrContains(left, right) => getExpr(e, "str.contains", left, right) + case SmtlibStrIndexOf(haystack, needle, fromIndex) => getExpr(e, "str.indexof", haystack, needle, fromIndex) + case SmtlibStrReplace(haystack, needle, replacement) => getExpr(e, "str.replace", haystack, needle, replacement) + case SmtlibStrReplaceAll(haystack, needle, replacement) => getExpr(e, "str.replace_all", haystack, needle, replacement) + case SmtlibStrReplaceRe(haystack, re, replacement) => getExpr(e, "str.replace_re", haystack, re, replacement) + case SmtlibStrReplaceReAll(haystack, re, replacement) => getExpr(e, "str.replace_re_all", haystack, re, replacement) + case SmtlibStrIsDigit(arg) => getExpr(e, "str.indexof", arg) + case SmtlibStrToCode(arg) => getExpr(e, "str.to_code", arg) + case SmtlibStrFromCode(arg) => getExpr(e, "str.from_code", arg) + case SmtlibStrToInt(arg) => getExpr(e, "str.to_int", arg) + case SmtlibStrFromInt(arg) => getExpr(e, "str.from_int", arg) + case SmtlibReFromStr(arg) => getExpr(e, "str.to_re", arg) + case SmtlibReContains(re, str) => getExpr(e, "str.in_re", str, re) + case SmtlibReNone() => getExpr(e, "re.none") + case SmtlibReAll() => getExpr(e, "re.all") + case SmtlibReAllChar() => getExpr(e, "re.allchar") + case SmtlibReConcat(left, right) => getExpr(e, "re.++", left, right) + case SmtlibReUnion(left, right) => getExpr(e, "re.union", left, right) + case SmtlibReInter(left, right) => getExpr(e, "re.inter", left, right) + case SmtlibReStar(arg) => getExpr(e, "re.*", arg) + case SmtlibReComp(arg) => getExpr(e, "re.comp", arg) + case SmtlibReDiff(left, right) => getExpr(e, "re.diff", left, right) + case SmtlibRePlus(arg) => getExpr(e, "re.+", arg) + case SmtlibReOpt(arg) => getExpr(e, "re.opt", arg) + case SmtlibReRange(left, right) => getExpr(e, "re.range", left, right) + case SmtlibReRepeat(count, arg) => getExpr(e, s"(_ re.^ $count)", arg) + case SmtlibReRepeatRange(from, to, arg) => getExpr(e, s"(_ re.loop $from $to)", arg) + case Z3BvSub(left, right) => getExpr(e, "bvsub", left, right) + case Z3BvSRem(left, right) => getExpr(e, "bvsrem", left, right) + case Z3BvSMod(left, right) => getExpr(e, "bvsmod", left, right) + case Z3BvSShr(left, right) => getExpr(e, "bvashr", left, right) + case Z3BvNand(left, right) => getExpr(e, "bvnand", left, right) + case Z3BvNor(left, right) => getExpr(e, "bvnor", left, right) + case Z3BvXnor(left, right) => getExpr(e, "bvxnor", left, right) + case Z3ArrayConst(domain, codomain, value) => + getExpr(e, s"(as const ${smtTypeString(TSmtlibArray(domain, codomain))})", value) + case Z3ArrayOfFunction(ref) => + // https://github.com/utwente-fmt/vercors/issues/1022 + getExpr(e, s"(_ as-array ${ref.ref.decl.o.preferredName})") + case Z3ArrayMap(ref, args) => + getExpr(e, s"(_ map ${ref.ref.decl.o.preferredName})", args: _*) + case Z3SeqEmpty(elementType) => getExpr(e, s"(as seq.empty (Seq ${smtTypeString(elementType)}))") + case Z3SeqUnit(arg) => getExpr(e, "seq.unit", arg) + case Z3SeqConcat(left, right) => getExpr(e, "seq.++", left, right) + case Z3SeqLen(arg) => getExpr(e, "seq.len", arg) + case Z3SeqExtract(seq, offset, len) => getExpr(e, "seq.extract", seq, offset, len) + case Z3SeqAt(seq, offset) => getExpr(e, "seq.at", seq, offset) + case Z3SeqNth(seq, offset) => getExpr(e, "seq.nth", seq, offset) + case Z3SeqContains(seq, subseq) => getExpr(e, "seq.contains", seq, subseq) + case Z3SeqPrefixOf(pre, subseq) => getExpr(e, "seq.prefixof", pre, subseq) + case Z3SeqSuffixOf(post, seq) => getExpr(e, "seq.suffixof", post, seq) + case Z3SeqReplace(haystack, needle, replacement) => getExpr(e, "seq.replace", haystack, needle, replacement) + case Z3SeqMap(f, seq) => getExpr(e, "seq.map", f, seq) + case Z3SeqMapI(f, offset, seq) => getExpr(e, "seq.mapi", f, offset, seq) + case Z3SeqFoldl(f, base, seq) => getExpr(e, "seq.foldl", f, base, seq) + case Z3SeqFoldlI(f, offset, base, seq) => getExpr(e, "seq.foldli", f, offset, base, seq) + case Z3TransitiveClosure(ref, args) => + getExpr(e, s"(_ transitive-closure ${ref.ref.decl.o.preferredName})", args: _*) + } + case other => rewriteDefault(other) + } +} diff --git a/util/stubimpl/make_stub_impl.py b/util/stubimpl/make_stub_impl.py index 6447b19c66..cdbe2e7cb5 100644 --- a/util/stubimpl/make_stub_impl.py +++ b/util/stubimpl/make_stub_impl.py @@ -32,8 +32,10 @@ def package_to_path(package): f.write(f"package {IMPL_PACKAGE}.{package}\n") f.write("\n") f.write(f"import {AST_PACKAGE}.{node}\n") + f.write("import vct.col.ast.Type\n") f.write("import vct.col.print._\n") f.write("\n") f.write(f"trait {node}Impl[G] {'{'} this: {node}[G] =>\n") + f.write(" override def t: Type[G] = ???\n") f.write(" // def layout(implicit ctx: Ctx): Doc = ???\n") f.write("}\n")