mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

rename function

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-04 18:39:12 -07:00
parent eb4e28d5d4
commit 26ab0de8fc
2 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_recfun.cpp
View file

@ -225,7 +225,6 @@ namespace smt {
recfun::vars const & vars,
expr_ref_vector const & args,
expr * e) {
SASSERT(is_standard_order(vars));
var_subst subst(m, true);
expr_ref new_body = subst(e, args);
ctx.get_rewriter()(new_body); // simplify
@ -377,7 +376,6 @@ namespace smt {
recfun::def & d = *e.m_cdef->get_def();
auto & vars = d.get_vars();
auto & args = e.m_args;
SASSERT(is_standard_order(vars));
unsigned depth = get_depth(e.m_pred);
expr_ref lhs(u().mk_fun_defined(d, args), m);
expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());

2
src/smt/theory_recfun.h
View file

@ -82,7 +82,7 @@ namespace smt {
void set_depth_rec(unsigned d, expr* e);
literal mk_eq_lit(expr* l, expr* r);
bool is_standard_order(recfun::vars const& vars) const {
bool is_decreasing_order(recfun::vars const& vars) const {
return vars.empty() || vars[vars.size()-1]->get_idx() == 0;
}
protected: