From 876d7c92fba44d7068d28de35ed5e58e98d4db16 Mon Sep 17 00:00:00 2001 From: Olaf Tomalka Date: Wed, 22 Jan 2020 21:54:10 +0000 Subject: [PATCH] Added FreshFunction to Python bindings. All other declarations can be done use appropriate Fresh*() call, or FreshConst() with a desired sort, except Functions. I've added the abillity to do that in Python bindings using already existing APIs --- src/api/python/z3/z3.py | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 326122741..d78517b5b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -818,6 +818,29 @@ def Function(name, *sig): ctx = rng.ctx return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx) +def FreshFunction(*sig): + """Create a new fresh Z3 uninterpreted function with the given sorts. + + >>> f = FreshFunction(IntSort(), IntSort()) + >>> f(f(0)) + f!0(f!0(0)) + """ + sig = _get_args(sig) + if z3_debug(): + _z3_assert(len(sig) > 0, "At least two arguments expected") + arity = len(sig) - 1 + rng = sig[arity] + if z3_debug(): + _z3_assert(is_sort(rng), "Z3 sort expected") + dom = (z3.Sort * arity)() + for i in range(arity): + if z3_debug(): + _z3_assert(is_sort(sig[i]), "Z3 sort expected") + dom[i] = sig[i].ast + ctx = rng.ctx + return FuncDeclRef(Z3_mk_fresh_func_decl(ctx.ref(), 'f', arity, dom, rng.ast), ctx) + + def _to_func_decl_ref(a, ctx): return FuncDeclRef(a, ctx)