smt/io.github.jmltoolkit.smt/JmlExpr2Smt

JmlExpr2Smt

class JmlExpr2Smt(smtLog: SmtQuery, val translator: ArithmeticTranslator) : GenericVisitorAdapter<SExpr, Any?> (source)

Author

Alexander Weigl

Constructors

Link copied to clipboard
constructor(smtLog: SmtQuery, translator: ArithmeticTranslator)

Types

Link copied to clipboard
object Companion

Properties

Link copied to clipboard

Functions

Link copied to clipboard
open fun visit(n: ArrayCreationLevel?, arg: Any?): SExpr?
open fun visit(n: CompilationUnit?, arg: Any?): SExpr?
open fun visit(n: ImportDeclaration?, arg: Any?): SExpr?
open fun visit(n: Modifier?, arg: Any?): SExpr?
open fun visit(n: NodeList<*>?, arg: Any?): SExpr?
open fun visit(n: PackageDeclaration?, arg: Any?): SExpr?
open fun visit(n: AnnotationDeclaration?, arg: Any?): SExpr?
open fun visit(n: AnnotationMemberDeclaration?, arg: Any?): SExpr?
open fun visit(n: ClassOrInterfaceDeclaration?, arg: Any?): SExpr?
open fun visit(n: CompactConstructorDeclaration?, arg: Any?): SExpr?
open fun visit(n: ConstructorDeclaration?, arg: Any?): SExpr?
open fun visit(n: EnumConstantDeclaration?, arg: Any?): SExpr?
open fun visit(n: EnumDeclaration?, arg: Any?): SExpr?
open fun visit(n: FieldDeclaration?, arg: Any?): SExpr?
open fun visit(n: InitializerDeclaration?, arg: Any?): SExpr?
open fun visit(n: MethodDeclaration?, arg: Any?): SExpr?
open fun visit(n: Parameter?, arg: Any?): SExpr?
open fun visit(n: ReceiverParameter?, arg: Any?): SExpr?
open fun visit(n: RecordDeclaration?, arg: Any?): SExpr?
open fun visit(n: VariableDeclarator?, arg: Any?): SExpr?
open fun visit(n: BlockComment?, arg: Any?): SExpr?
open fun visit(n: LineComment?, arg: Any?): SExpr?
open fun visit(n: MarkdownComment?, arg: Any?): SExpr?
open fun visit(n: TraditionalJavadocComment?, arg: Any?): SExpr?
open fun visit(n: EnclosedExpr?, arg: Any?): SExpr?
open fun visit(n: MarkerAnnotationExpr?, arg: Any?): SExpr?
open fun visit(n: MatchAllPatternExpr?, arg: Any?): SExpr?
open fun visit(n: MemberValuePair?, arg: Any?): SExpr?
open fun visit(n: MethodReferenceExpr?, arg: Any?): SExpr?
open fun visit(n: Name?, arg: Any?): SExpr?
open fun visit(n: NormalAnnotationExpr?, arg: Any?): SExpr?
open fun visit(n: SimpleName?, arg: Any?): SExpr?
open fun visit(n: SingleMemberAnnotationExpr?, arg: Any?): SExpr?
open fun visit(n: VariableDeclarationExpr?, arg: Any?): SExpr?
open fun visit(n: JmlClassAccessibleDeclaration?, arg: Any?): SExpr?
open fun visit(n: JmlClassExprDeclaration?, arg: Any?): SExpr?
open fun visit(n: JmlFieldDeclaration?, arg: Any?): SExpr?
open fun visit(n: JmlMethodDeclaration?, arg: Any?): SExpr?
open fun visit(n: JmlRepresentsDeclaration?, arg: Any?): SExpr?
open fun visit(n: JmlCallableClause?, arg: Any?): SExpr?
open fun visit(n: JmlConditionalClause?, arg: Any?): SExpr?
open fun visit(n: JmlContract?, arg: Any?): SExpr?
open fun visit(n: JmlForallClause?, arg: Any?): SExpr?
open fun visit(n: JmlInfFlowClause?, arg: Any?): SExpr?
open fun visit(n: JmlLabledClause?, arg: Any?): SExpr?
open fun visit(n: JmlMethodSignature?, arg: Any?): SExpr?
open fun visit(n: JmlMultiExprClause?, arg: Any?): SExpr?
open fun visit(n: JmlOldClause?, arg: Any?): SExpr?
open fun visit(n: JmlSignalsClause?, arg: Any?): SExpr?
open fun visit(n: JmlSignalsOnlyClause?, arg: Any?): SExpr?
open fun visit(n: JmlSimpleExprClause?, arg: Any?): SExpr?
open fun visit(n: JmlDoc?, arg: Any?): SExpr?
open fun visit(n: JmlDocDeclaration?, arg: Any?): SExpr?
open fun visit(n: JmlDocStmt?, arg: Any?): SExpr?
open fun visit(n: JmlDocType?, arg: Any?): SExpr?
open fun visit(n: JmlSetComprehensionExpr?, arg: Any?): SExpr?
open fun visit(n: JmlBeginStmt?, arg: Any?): SExpr?
open fun visit(n: JmlEndStmt?, arg: Any?): SExpr?
open fun visit(n: JmlExpressionStmt?, arg: Any?): SExpr?
open fun visit(n: JmlGhostStmt?, arg: Any?): SExpr?
open fun visit(n: JmlLabelStmt?, arg: Any?): SExpr?
open fun visit(n: JmlRefiningStmt?, arg: Any?): SExpr?
open fun visit(n: JmlUnreachableStmt?, arg: Any?): SExpr?
open fun visit(n: KeyCatchAllStmt?, arg: Any?): SExpr?
open fun visit(n: KeyCcatchBreak?, arg: Any?): SExpr?
open fun visit(n: KeyCcatchContinue?, arg: Any?): SExpr?
open fun visit(n: KeyCcatchParameter?, arg: Any?): SExpr?
open fun visit(n: KeyCcatchReturn?, arg: Any?): SExpr?
open fun visit(n: KeyEscapeExpression?, arg: Any?): SExpr?
open fun visit(n: KeyExecStmt?, arg: Any?): SExpr?
open fun visit(n: KeyExecutionContext?, arg: Any?): SExpr?
open fun visit(n: KeyLoopScopeBlockStmt?, arg: Any?): SExpr?
open fun visit(n: KeyMarkerStatement?, arg: Any?): SExpr?
open fun visit(n: KeyMergePointStmt?, arg: Any?): SExpr?
open fun visit(n: KeyMethodBodyStatement?, arg: Any?): SExpr?
open fun visit(n: KeyMethodCallStmt?, arg: Any?): SExpr?
open fun visit(n: KeyMethodSignature?, arg: Any?): SExpr?
open fun visit(n: KeyPassiveExpression?, arg: Any?): SExpr?
open fun visit(n: KeyTransactionStmt?, arg: Any?): SExpr?
open fun visit(n: KeyCcatchSV?, arg: Any?): SExpr?
open fun visit(n: KeyContextStatementBlock?, arg: Any?): SExpr?
open fun visit(n: KeyExecCtxtSV?, arg: Any?): SExpr?
open fun visit(n: KeyExecutionContextSV?, arg: Any?): SExpr?
open fun visit(n: KeyExpressionSV?, arg: Any?): SExpr?
open fun visit(n: KeyJumpLabelSV?, arg: Any?): SExpr?
open fun visit(n: KeyMetaConstruct?, arg: Any?): SExpr?
open fun visit(n: KeyMetaConstructExpression?, arg: Any?): SExpr?
open fun visit(n: KeyMetaConstructType?, arg: Any?): SExpr?
open fun visit(n: KeyMethodSignatureSV?, arg: Any?): SExpr?
open fun visit(n: KeyProgramVariableSV?, arg: Any?): SExpr?
open fun visit(n: KeyStatementSV?, arg: Any?): SExpr?
open fun visit(n: KeyTypeSV?, arg: Any?): SExpr?
open fun visit(n: ModuleDeclaration?, arg: Any?): SExpr?
open fun visit(n: ModuleExportsDirective?, arg: Any?): SExpr?
open fun visit(n: ModuleOpensDirective?, arg: Any?): SExpr?
open fun visit(n: ModuleProvidesDirective?, arg: Any?): SExpr?
open fun visit(n: ModuleRequiresDirective?, arg: Any?): SExpr?
open fun visit(n: ModuleUsesDirective?, arg: Any?): SExpr?
open fun visit(n: AssertStmt?, arg: Any?): SExpr?
open fun visit(n: BlockStmt?, arg: Any?): SExpr?
open fun visit(n: BreakStmt?, arg: Any?): SExpr?
open fun visit(n: CatchClause?, arg: Any?): SExpr?
open fun visit(n: ContinueStmt?, arg: Any?): SExpr?
open fun visit(n: DoStmt?, arg: Any?): SExpr?
open fun visit(n: EmptyStmt?, arg: Any?): SExpr?
open fun visit(n: ExplicitConstructorInvocationStmt?, arg: Any?): SExpr?
open fun visit(n: ExpressionStmt?, arg: Any?): SExpr?
open fun visit(n: ForEachStmt?, arg: Any?): SExpr?
open fun visit(n: ForStmt?, arg: Any?): SExpr?
open fun visit(n: IfStmt?, arg: Any?): SExpr?
open fun visit(n: LabeledStmt?, arg: Any?): SExpr?
open fun visit(n: LocalClassDeclarationStmt?, arg: Any?): SExpr?
open fun visit(n: LocalRecordDeclarationStmt?, arg: Any?): SExpr?
open fun visit(n: ReturnStmt?, arg: Any?): SExpr?
open fun visit(n: SwitchEntry?, arg: Any?): SExpr?
open fun visit(n: SwitchStmt?, arg: Any?): SExpr?
open fun visit(n: SynchronizedStmt?, arg: Any?): SExpr?
open fun visit(n: ThrowStmt?, arg: Any?): SExpr?
open fun visit(n: TryStmt?, arg: Any?): SExpr?
open fun visit(n: UnparsableStmt?, arg: Any?): SExpr?
open fun visit(n: WhileStmt?, arg: Any?): SExpr?
open fun visit(n: YieldStmt?, arg: Any?): SExpr?
open fun visit(n: ArrayType?, arg: Any?): SExpr?
open fun visit(n: ClassOrInterfaceType?, arg: Any?): SExpr?
open fun visit(n: IntersectionType?, arg: Any?): SExpr?
open fun visit(n: PrimitiveType?, arg: Any?): SExpr?
open fun visit(n: TypeParameter?, arg: Any?): SExpr?
open fun visit(n: UnionType?, arg: Any?): SExpr?
open fun visit(n: UnknownType?, arg: Any?): SExpr?
open fun visit(n: VarType?, arg: Any?): SExpr?
open fun visit(n: VoidType?, arg: Any?): SExpr?
open fun visit(n: WildcardType?, arg: Any?): SExpr?
open override fun visit(n: ArrayAccessExpr, arg: Any?): SExpr
open override fun visit(n: ArrayCreationExpr, arg: Any?): SExpr?
open override fun visit(n: ArrayInitializerExpr, arg: Any?): SExpr
open override fun visit(n: AssignExpr?, arg: Any?): SExpr?
open override fun visit(n: BinaryExpr, arg: Any?): SExpr
open override fun visit(n: BooleanLiteralExpr, arg: Any?): SExpr
open override fun visit(n: CastExpr?, arg: Any?): SExpr
open override fun visit(n: CharLiteralExpr, arg: Any?): SExpr
open override fun visit(n: ClassExpr?, arg: Any?): SExpr
open override fun visit(n: ConditionalExpr, arg: Any?): SExpr
open override fun visit(n: DoubleLiteralExpr?, arg: Any?): SExpr
open override fun visit(n: FieldAccessExpr, arg: Any?): SExpr
open override fun visit(n: InstanceOfExpr, arg: Any?): SExpr
open override fun visit(n: IntegerLiteralExpr, arg: Any?): SExpr
open override fun visit(n: LambdaExpr?, arg: Any?): SExpr
open override fun visit(n: LongLiteralExpr, arg: Any?): SExpr
open override fun visit(n: MethodCallExpr, arg: Any?): SExpr
open override fun visit(n: NameExpr, arg: Any?): SExpr
open override fun visit(n: NullLiteralExpr?, arg: Any?): SExpr
open override fun visit(n: ObjectCreationExpr?, arg: Any?): SExpr
open override fun visit(n: RecordPatternExpr, arg: Any?): SExpr
open override fun visit(n: StringLiteralExpr, arg: Any?): SExpr
open override fun visit(n: SuperExpr?, arg: Any?): SExpr
open override fun visit(n: SwitchExpr?, arg: Any?): SExpr
open override fun visit(n: TextBlockLiteralExpr, arg: Any?): SExpr
open override fun visit(n: ThisExpr?, arg: Any?): SExpr
open override fun visit(n: TypeExpr?, arg: Any?): SExpr
open override fun visit(n: TypePatternExpr, arg: Any?): SExpr
open override fun visit(n: UnaryExpr, arg: Any?): SExpr
open override fun visit(n: JmlBinaryInfixExpr, arg: Any?): SExpr
open override fun visit(n: JmlLabelExpr, arg: Any?): SExpr
open override fun visit(n: JmlLetExpr, arg: Any?): SExpr
open override fun visit(n: JmlMultiCompareExpr, arg: Any?): SExpr
open override fun visit(n: JmlQuantifiedExpr, arg: Any?): SExpr?
open override fun visit(n: JmlTypeExpr?, arg: Any?): SExpr
Generated by Dokka
© 2026 Copyright