kdrag.contrib.expr

Functions

`Const`(name, sort[, ctx])
`Consts`(names, sort)
`FreshConst`(sort[, prefix])
`Function`(name, *sig[, ctx])
`main_ctx`()

Classes

`AstRef`(ctx)
`Context`()
`ExprRef`(ctx, _decl, _args)
`FuncDeclRef`(ctx, _name, _domain, _range)
`SortRef`(ctx, _kind, _name)
`TypeVarRef`(ctx)

class kdrag.contrib.expr.AstRef(ctx: kdrag.contrib.expr.Context)

Bases: object

Parameters:: ctx (Context)

ctx: Context

eq(other)

get_id()

kdrag.contrib.expr.Const(name: str, sort: SortRef, ctx=None) → ExprRef

Parameters:

name (str)
sort (SortRef)

Return type:

ExprRef

kdrag.contrib.expr.Consts(names: str, sort: SortRef) → list[ExprRef]

Parameters:

names (str)
sort (SortRef)

Return type:

list[ExprRef]

class kdrag.contrib.expr.Context

Bases: object

counter = 0

class kdrag.contrib.expr.ExprRef(ctx: kdrag.contrib.expr.Context, _decl: kdrag.contrib.expr.FuncDeclRef, _args: tuple[kdrag.contrib.expr.AstRef, ...])

Bases: AstRef

Parameters:

ctx (Context)
_decl (FuncDeclRef)
_args (tuple[AstRef, ...])

arg(i)

children()

ctx: Context

decl()

eq(other)

get_id()

num_args()

kdrag.contrib.expr.FreshConst(sort: SortRef, prefix='c')

Parameters:: sort (SortRef)

class kdrag.contrib.expr.FuncDeclRef(ctx: kdrag.contrib.expr.Context, _name: str, _domain: tuple[kdrag.contrib.expr.SortRef, ...], _range: kdrag.contrib.expr.SortRef)

Bases: AstRef

Parameters:

ctx (Context)
_name (str)
_domain (tuple[SortRef, ...])
_range (SortRef)

arity()

ctx: Context

domain(i)

eq(other)

get_id()

name()

range()

kdrag.contrib.expr.Function(name, *sig, ctx=None)

class kdrag.contrib.expr.SortRef(ctx: kdrag.contrib.expr.Context, _kind: object, _name: str)

Bases: AstRef

Parameters:

ctx (Context)
_kind (object)
_name (str)

ctx: Context

eq(other)

get_id()

kind()

name()

class kdrag.contrib.expr.TypeVarRef(ctx: kdrag.contrib.expr.Context)

Bases: AstRef

Parameters:: ctx (Context)

ctx: Context

eq(other)

get_id()

kdrag.contrib.expr.main_ctx()