kdrag.contrib.expr

Functions

main_ctx()

Classes

`AstNode`(kind, children, hash)
`AstRef`(ctx, ast)
`Context`(table)
`ExprRef`(ctx, ast)
`FuncDeclRef`(ctx, ast)
`Kind`(*values)
`SortRef`(ctx, ast)

class kdrag.contrib.expr.AstNode(kind, children, hash)

Bases: NamedTuple

Parameters:

kind (Kind)
children (tuple)
hash (int)

children: tuple: Alias for field number 1

count(value, /): Return number of occurrences of value.

static create(kind: Kind, children: tuple) → AstNode

Parameters:

kind (Kind)
children (tuple)

Return type:

AstNode

hash: int: Alias for field number 2

index(value, start=0, stop=9223372036854775807, /)

Return first index of value.

Raises ValueError if the value is not present.

kind: Kind: Alias for field number 0

class kdrag.contrib.expr.AstRef(ctx: 'Context', ast: kdrag.contrib.expr.AstNode)

Bases: object

Parameters:

ctx (Context)
ast (AstNode)

ast: AstNode

ctx: Context

eq(other)

get_id()

class kdrag.contrib.expr.Context(table: dict = <factory>)

Bases: object

>>> ctx = Context()
>>> s1 = ctx.DeclareSort("S")
>>> s2 = ctx.DeclareSort("S")
>>> s1.eq(s2)
True
>>> f = ctx.Function("f", s1, ctx.BoolSort())
>>> x = ctx.Const("x", s1)
>>> f(x) == ctx.BoolVal(True)
(= (f x) true)
>>> ctx.FreshConst(s1, prefix="foo")
foo!0

Parameters:: table (dict)

BoolSort() → SortRef

Return type:: SortRef

BoolVal(value: bool) → ExprRef

Parameters:: value (bool)
Return type:: ExprRef

Const(name: str, sort: SortRef) → ExprRef

Parameters:

name (str)
sort (SortRef)

Return type:

ExprRef

Consts(names: str, sort: SortRef) → list[ExprRef]

Parameters:

names (str)
sort (SortRef)

Return type:

list[ExprRef]

DeclareSort(name: str) → SortRef

Parameters:: name (str)
Return type:: SortRef

FreshConst(sort: SortRef, prefix='c') → ExprRef

Parameters:: sort (SortRef)
Return type:: ExprRef

Function(name: str, *sig: SortRef) → FuncDeclRef

Parameters:

name (str)
sig (SortRef)

Return type:

FuncDeclRef

IntSort() → SortRef

Return type:: SortRef

IntVal(value: int) → ExprRef

Parameters:: value (int)
Return type:: ExprRef

counter = 0

hashcons(kind: Kind, children: tuple) → AstNode

Parameters:

kind (Kind)
children (tuple)

Return type:

AstNode

table: dict

translate(expr: AstRef | AstRef) → AstRef

Parameters:: expr (AstRef | AstRef)
Return type:: AstRef

class kdrag.contrib.expr.ExprRef(ctx: Context, ast: AstNode)

Bases: AstRef

Parameters:

ctx (Context)
ast (AstNode)

arg(i: int) → ExprRef

Parameters:: i (int)
Return type:: ExprRef

ast: AstNode

children()

ctx: Context

decl()

eq(other)

get_id()

sort() → SortRef

Return type:: SortRef

class kdrag.contrib.expr.FuncDeclRef(ctx: Context, ast: AstNode)

Bases: AstRef

Parameters:

ctx (Context)
ast (AstNode)

ast: AstNode

ctx: Context

domain(i: int) → SortRef

Parameters:: i (int)
Return type:: SortRef

eq(other)

get_id()

name()

range() → SortRef

Return type:: SortRef

class kdrag.contrib.expr.Kind(*values)

Bases: Enum

APP = 2

DECL = 1

SORT = 0

VAR = 3

classmethod __contains__(value)

Return True if value is in cls.

value is in cls if: 1) value is a member of cls, or 2) value is the value of one of the cls’s members. 3) value is a pseudo-member (flags)

classmethod __getitem__(name): Return the member matching name.

classmethod __iter__(): Return members in definition order.

classmethod __len__(): Return the number of members (no aliases)

class kdrag.contrib.expr.SortRef(ctx: Context, ast: AstNode)

Bases: AstRef

Parameters:

ctx (Context)
ast (AstNode)

ast: AstNode

ctx: Context

eq(other)

get_id()

kdrag.contrib.expr.main_ctx()