mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

include rewriter for recursive functions in model-evaluator

Browse source 
fixes bug reported by Tahina and Nick, @tahina-pro
This commit is contained in:
Nikolaj Bjorner 2023-08-28 11:31:32 -07:00
parent 5ba06f4e28
commit 09f911d8a8
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/model/model_evaluator.cpp
View file

@ -32,6 +32,7 @@ Revision History:
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/recfun_rewriter.h"
#include "model/model_smt2_pp.h"
#include "model/model.h"
#include "model/model_evaluator_params.hpp"
@ -53,6 +54,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
pb_rewriter m_pb_rw;
fpa_rewriter m_f_rw;
seq_rewriter m_seq_rw;
recfun_rewriter m_rec_rw;
array_util m_ar;
arith_util m_au;
fpa_util m_fpau;
@ -80,6 +82,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_pb_rw(m),
m_f_rw(m),
m_seq_rw(m),
m_rec_rw(m),
m_ar(m),
m_au(m),
m_fpau(m),
@ -283,6 +286,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
st = m_f_rw.mk_app_core(f, num, args, result);
else if (fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_app_core(f, num, args, result);
else if (fid == m_rec_rw.get_fid())
st = m_rec_rw.mk_app_core(f, num, args, result);
else if (fid == m.get_label_family_id() && num == 1) {
result = args[0];
st = BR_DONE;