mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 00:20:27 +00:00
Code Activity

updates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-09 17:42:11 -07:00
parent dbd725bdc0
commit 0e29a35da5
4 changed files with 39 additions and 141 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2947,7 +2947,9 @@ bool seq_rewriter::check_deriv_normal_form(expr* r, int level) {
#endif
expr_ref seq_rewriter::mk_derivative(expr* r) {
return m_derive(r);
auto result = m_derive(r);
TRACE(seq, tout << "Derivative of " << mk_pp(r, m()) << "\nis\n" << result << std::endl;);
return result;
}
expr_ref seq_rewriter::mk_brz_derivative(expr* r) {
@ -2959,7 +2961,10 @@ expr_ref seq_rewriter::mk_brz_derivative(expr* r) {
}
expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
return m_derive(ele, r);
auto result = m_derive(ele, r);
TRACE(seq,
tout << "Derivative of " << mk_pp(r, m()) << " w.r.t. " << mk_pp(ele, m()) << "\nis\n" << result << std::endl;);
return result;
}