mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-14 13:39:52 -08:00
parent b1d167de5b
commit 03b5380a20
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/var_subst.h
View file

@ -48,6 +48,7 @@ public:
Otherwise, (VAR 0) is stored in the first position, (VAR 1) in the second, and so on. Otherwise, (VAR 0) is stored in the first position, (VAR 1) in the second, and so on.
*/ */
expr_ref operator()(expr * n, unsigned num_args, expr * const * args); expr_ref operator()(expr * n, unsigned num_args, expr * const * args);
inline expr_ref operator()(expr* n, expr* arg) { return (*this)(n, 1, &arg); }
inline expr_ref operator()(expr * n, expr_ref_vector const& args) { return (*this)(n, args.size(), args.data()); } inline expr_ref operator()(expr * n, expr_ref_vector const& args) { return (*this)(n, args.size(), args.data()); }
inline expr_ref operator()(expr * n, var_ref_vector const& args) { return (*this)(n, args.size(), (expr*const*)args.data()); } inline expr_ref operator()(expr * n, var_ref_vector const& args) { return (*this)(n, args.size(), (expr*const*)args.data()); }
inline expr_ref operator()(expr * n, app_ref_vector const& args) { return (*this)(n, args.size(), (expr*const*)args.data()); } inline expr_ref operator()(expr * n, app_ref_vector const& args) { return (*this)(n, args.size(), (expr*const*)args.data()); }