mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

enforce reference count ownership in context of mk_derivative calls.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-01 13:13:17 -07:00
parent d75ce38016
commit d91ca423ab
2 changed files with 12 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/seq_rewriter.cpp
View file

@ -2545,7 +2545,8 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
if (lo > 0) { if (lo > 0) {
lo--; lo--;
} }
return mk_der_concat(mk_derivative(ele, r1), re().mk_loop(r1, lo)); result = re().mk_loop(r1, lo);
return mk_der_concat(mk_derivative(ele, r1), result);
} }
else if (re().is_loop(r, r1, lo, hi)) { else if (re().is_loop(r, r1, lo, hi)) {
if (hi == 0) { if (hi == 0) {
@ -2555,7 +2556,8 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
if (lo > 0) { if (lo > 0) {
lo--; lo--;
} }
return mk_der_concat(mk_derivative(ele, r1), re().mk_loop(r1, lo, hi)); result = re().mk_loop(r1, lo, hi);
return mk_der_concat(mk_derivative(ele, r1), result);
} }
else if (re().is_full_seq(r) || else if (re().is_full_seq(r) ||
re().is_empty(r)) { re().is_empty(r)) {
@ -2566,7 +2568,8 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
expr_ref hd(m()), tl(m()); expr_ref hd(m()), tl(m());
if (get_head_tail(r1, hd, tl)) { if (get_head_tail(r1, hd, tl)) {
// head must be equal; if so, derivative is tail // head must be equal; if so, derivative is tail
return re_and(m_br.mk_eq_rw(ele, hd), re().mk_to_re(tl)); result = re().mk_to_re(tl);
return re_and(m_br.mk_eq_rw(ele, hd), result);
} }
else if (str().is_empty(r1)) { else if (str().is_empty(r1)) {
return mk_empty(); return mk_empty();
@ -2575,10 +2578,11 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
#if 0 #if 0
hd = str().mk_nth_i(r1, m_autil.mk_int(0)); hd = str().mk_nth_i(r1, m_autil.mk_int(0));
tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1))); tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1)));
result = re().mk_to_re(tl);
result = result =
m().mk_ite(m_br.mk_eq_rw(r1, str().mk_empty(m().get_sort(r1))), m().mk_ite(m_br.mk_eq_rw(r1, str().mk_empty(m().get_sort(r1))),
mk_empty(), mk_empty(),
re_and(m_br.mk_eq_rw(ele, hd), re().mk_to_re(tl))); re_and(m_br.mk_eq_rw(ele, hd), result));
return result; return result;
#else #else
return expr_ref(re().mk_derivative(ele, r), m()); return expr_ref(re().mk_derivative(ele, r), m());

9
src/smt/diff_logic.h
View file

@ -1283,7 +1283,6 @@ public:
} }
} }
} }
} }
} }
@ -1291,14 +1290,14 @@ public:
return m_assignment[v]; return m_assignment[v];
} }
void set_assignment(dl_var v, numeral const & n) {
m_assignment[v] = n;
}
unsigned get_timestamp() const { unsigned get_timestamp() const {
return m_timestamp; return m_timestamp;
} }
void set_assignment(dl_var v, numeral const & n) {
m_assignment[v] = n;
}
private: private:
void inc_activity(edge_id e_id) { void inc_activity(edge_id e_id) {