kdrag.contrib.fast

Functions

`astptr`(ast)
`ctxptr`(ctx)
`intify`(ptr)
`test`()

kdrag.contrib.fast.astptr(ast: AstRef)

Parameters:: ast (AstRef)

kdrag.contrib.fast.ctxptr(ctx: Context)

Parameters:: ctx (Context)

kdrag.contrib.fast.intify(ptr)

kdrag.contrib.fast.test()

>>> myadd(2, 3)
5
>>> ctx = ffibuilder.cast("void *", z3.main_ctx().ctx.value)
>>> ast = my_mk_true(ctx)
>>> value = intify(ast)
>>> z3.BoolRef(value)
True
>>> z3.BoolRef(intify(my_mk_and(ctx, ast, ast)))
And(True, True)
>>> z3.AstVector(intify(KDRAG_get_consts(ctx, ast)), z3.main_ctx())
[True]
>>> x = z3.Int("x")
>>> z3.AstVector(intify(KDRAG_get_consts(ctx, astptr(x + x + x))), z3.main_ctx())
[x]