mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove reference count debugging, add substitution to C++ header
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ec2726ac66
commit
2afcc493e0
|
@ -29,7 +29,6 @@ Revision History:
|
|||
#define Z3_CATCH_RETURN_NO_HANDLE(VAL) } catch (z3_exception &) { return VAL; }
|
||||
|
||||
#define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
|
||||
#define VALIDATE(a) SASSERT(!a || CHECK_REF_COUNT(a))
|
||||
|
||||
namespace api {
|
||||
// Generic wrapper for ref-count objects exposed by the API
|
||||
|
@ -44,30 +43,30 @@ namespace api {
|
|||
};
|
||||
};
|
||||
|
||||
inline ast * to_ast(Z3_ast a) { VALIDATE(a); return reinterpret_cast<ast *>(a); }
|
||||
inline ast * to_ast(Z3_ast a) { return reinterpret_cast<ast *>(a); }
|
||||
inline Z3_ast of_ast(ast* a) { return reinterpret_cast<Z3_ast>(a); }
|
||||
|
||||
inline expr * to_expr(Z3_ast a) { VALIDATE(a); return reinterpret_cast<expr*>(a); }
|
||||
inline expr * to_expr(Z3_ast a) { return reinterpret_cast<expr*>(a); }
|
||||
inline Z3_ast of_expr(expr* e) { return reinterpret_cast<Z3_ast>(e); }
|
||||
|
||||
inline expr * const * to_exprs(Z3_ast const* a) { return reinterpret_cast<expr* const*>(a); }
|
||||
inline Z3_ast * const * of_exprs(expr* const* e) { return reinterpret_cast<Z3_ast* const*>(e); }
|
||||
|
||||
inline app * to_app(Z3_app a) { VALIDATE(a); return reinterpret_cast<app*>(a); }
|
||||
inline app * to_app(Z3_ast a) { VALIDATE(a); return reinterpret_cast<app*>(a); }
|
||||
inline app * to_app(Z3_app a) { return reinterpret_cast<app*>(a); }
|
||||
inline app * to_app(Z3_ast a) { return reinterpret_cast<app*>(a); }
|
||||
inline Z3_app of_app(app* a) { return reinterpret_cast<Z3_app>(a); }
|
||||
|
||||
inline app * const* to_apps(Z3_ast const* a) { VALIDATE(a); return reinterpret_cast<app * const*>(a); }
|
||||
inline app * const* to_apps(Z3_ast const* a) { return reinterpret_cast<app * const*>(a); }
|
||||
|
||||
inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast<ast* const*>(a); }
|
||||
|
||||
inline sort * to_sort(Z3_sort a) { VALIDATE(a); return reinterpret_cast<sort*>(a); }
|
||||
inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); }
|
||||
inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); }
|
||||
|
||||
inline sort * const * to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); }
|
||||
inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }
|
||||
|
||||
inline func_decl * to_func_decl(Z3_func_decl a) { VALIDATE(a); return reinterpret_cast<func_decl*>(a); }
|
||||
inline func_decl * to_func_decl(Z3_func_decl a) { return reinterpret_cast<func_decl*>(a); }
|
||||
inline Z3_func_decl of_func_decl(func_decl* f) { return reinterpret_cast<Z3_func_decl>(f); }
|
||||
|
||||
inline func_decl * const * to_func_decls(Z3_func_decl const* f) { return reinterpret_cast<func_decl*const*>(f); }
|
||||
|
@ -75,7 +74,7 @@ inline func_decl * const * to_func_decls(Z3_func_decl const* f) { return reinter
|
|||
inline symbol to_symbol(Z3_symbol s) { return symbol::mk_symbol_from_c_ptr(reinterpret_cast<void*>(s)); }
|
||||
inline Z3_symbol of_symbol(symbol s) { return reinterpret_cast<Z3_symbol>(const_cast<void*>(s.c_ptr())); }
|
||||
|
||||
inline Z3_pattern of_pattern(ast* a) { VALIDATE(a); return reinterpret_cast<Z3_pattern>(a); }
|
||||
inline Z3_pattern of_pattern(ast* a) { return reinterpret_cast<Z3_pattern>(a); }
|
||||
inline app* to_pattern(Z3_pattern p) { return reinterpret_cast<app*>(p); }
|
||||
|
||||
inline Z3_lbool of_lbool(lbool b) { return static_cast<Z3_lbool>(b); }
|
||||
|
|
|
@ -872,7 +872,18 @@ namespace z3 {
|
|||
\brief Return a simplified version of this expression. The parameter \c p is a set of parameters for the Z3 simplifier.
|
||||
*/
|
||||
expr simplify(params const & p) const { Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Apply substitution. Replace src expressions by dst.
|
||||
*/
|
||||
expr substitute(expr_vector const& src, expr_vector const& dst);
|
||||
|
||||
/**
|
||||
\brief Apply substitution. Replace bound variables by expressions.
|
||||
*/
|
||||
expr substitute(expr_vector const& dst);
|
||||
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Wraps a Z3_ast as an expr object. It also checks for errors.
|
||||
|
@ -1680,6 +1691,30 @@ namespace z3 {
|
|||
d.check_error();
|
||||
return expr(d.ctx(), r);
|
||||
}
|
||||
|
||||
inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
|
||||
assert(src.size() == dst.size());
|
||||
array<Z3_ast> _src(src.size());
|
||||
array<Z3_ast> _dst(dst.size());
|
||||
for (unsigned i = 0; i < src.size(); ++i) {
|
||||
_src[i] = src[i];
|
||||
_dst[i] = dst[i];
|
||||
}
|
||||
Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
|
||||
check_error();
|
||||
return expr(ctx(), r);
|
||||
}
|
||||
|
||||
inline expr expr::substitute(expr_vector const& dst) {
|
||||
array<Z3_ast> _dst(dst.size());
|
||||
for (unsigned i = 0; i < dst.size(); ++i) {
|
||||
_dst[i] = dst[i];
|
||||
}
|
||||
Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
|
||||
check_error();
|
||||
return expr(ctx(), r);
|
||||
}
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue