mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

#6059

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-09 08:50:32 -08:00
parent 96a2c04026
commit 1434c7d394
2 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/api/c++/z3++.h
View file

@ -1566,6 +1566,11 @@ namespace z3 {
*/ */
expr substitute(expr_vector const& dst); expr substitute(expr_vector const& dst);
/**
\brief Apply function substitution by macro definitions.
*/
expr substitute(func_decl_vector const& funs, expr_vector const& bodies);
class iterator { class iterator {
expr& e; expr& e;
@ -4059,6 +4064,22 @@ namespace z3 {
return expr(ctx(), r); return expr(ctx(), r);
} }
inline expr expr::substitute(func_decl_vector const& funs, expr_vector const& dst) {
array<Z3_ast> _dst(dst.size());
array<Z3_func_decl> _funs(funs.size());
if (dst.size() != funs.size()) {
Z3_THROW(exception("length of argument lists don't align"));
return expr(ctx(), nullptr);
}
for (unsigned i = 0; i < dst.size(); ++i) {
_dst[i] = dst[i];
_funs[i] = funs[i];
}
Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
check_error();
return expr(ctx(), r);
}
typedef std::function<void(expr const& proof, expr_vector const& clause)> on_clause_eh_t; typedef std::function<void(expr const& proof, expr_vector const& clause)> on_clause_eh_t;
class on_clause { class on_clause {

2
src/api/python/z3/z3.py
View file

@ -8837,7 +8837,7 @@ def substitute_vars(t, *m):
return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx) return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
def substitute_funs(t, *m): def substitute_funs(t, *m):
"""Apply subistitution m on t, m is a list of pairs of a function and expression (from, to) """Apply substitution m on t, m is a list of pairs of a function and expression (from, to)
Every occurrence in to of the function from is replaced with the expression to. Every occurrence in to of the function from is replaced with the expression to.
The expression to can have free variables, that refer to the arguments of from. The expression to can have free variables, that refer to the arguments of from.
For examples, see For examples, see