Skip to content

Commit d581dc1

Browse files
#7630 propagate parameters on lazy tactics
1 parent 322e444 commit d581dc1

File tree

2 files changed

+14
-11
lines changed

2 files changed

+14
-11
lines changed

src/tactic/portfolio/default_tactic.cpp

+10-10
Original file line numberDiff line numberDiff line change
@@ -34,22 +34,22 @@ Module Name:
3434
#include "tactic/smtlogics/smt_tactic.h"
3535

3636
tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
37-
tactic * st = using_params(and_then(mk_simplify_tactic(m),
37+
tactic * st = using_params(and_then(mk_simplify_tactic(m, p),
3838
cond(mk_and(mk_is_propositional_probe(), mk_not(mk_produce_proofs_probe())),
3939
mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_fd_tactic(m, p); }),
40-
cond(mk_is_qfbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfbv_tactic(m); }),
41-
cond(mk_is_qfaufbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfaufbv_tactic(m); }),
42-
cond(mk_is_qflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qflia_tactic(m); }),
43-
cond(mk_is_qfauflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfauflia_tactic(m); }),
44-
cond(mk_is_qflra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qflra_tactic(m); }),
45-
cond(mk_is_qfnra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnra_tactic(m); }),
46-
cond(mk_is_qfnia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnia_tactic(m); }),
40+
cond(mk_is_qfbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfbv_tactic(m, p); }),
41+
cond(mk_is_qfaufbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfaufbv_tactic(m, p); }),
42+
cond(mk_is_qflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qflia_tactic(m, p); }),
43+
cond(mk_is_qfauflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfauflia_tactic(m, p); }),
44+
cond(mk_is_qflra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qflra_tactic(m, p); }),
45+
cond(mk_is_qfnra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnra_tactic(m, p); }),
46+
cond(mk_is_qfnia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnia_tactic(m, p); }),
4747
cond(mk_is_lira_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_lira_tactic(m, p); }),
48-
cond(mk_is_nra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_nra_tactic(m); }),
48+
cond(mk_is_nra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_nra_tactic(m, p); }),
4949
cond(mk_is_qffp_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qffp_tactic(m, p); }),
5050
cond(mk_is_qffplra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qffplra_tactic(m, p); }),
5151
//cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
52-
and_then(mk_preamble_tactic(m), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_smt_tactic(m);}))))))))))))))),
52+
and_then(mk_preamble_tactic(m), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_smt_tactic(m, p);}))))))))))))))),
5353
p);
5454
return st;
5555
}

src/tactic/tactic.cpp

+4-1
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,6 @@ void report_tactic_progress(char const * id, unsigned val) {
7474
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(" << id << " " << val << ")\n");
7575
}
7676
}
77-
7877
statistics_report::~statistics_report() {
7978
statistics st;
8079
if (m_tactic)
@@ -108,6 +107,10 @@ class lazy_tactic : public tactic {
108107
ensure_tactic();
109108
(*m_tactic)(in, result);
110109
}
110+
void updt_params(params_ref const& p) override {
111+
this->p.append(p);
112+
if (m_tactic) m_tactic->updt_params(p);
113+
}
111114
void cleanup() override { if (m_tactic) m_tactic->cleanup(); }
112115
char const* name() const override { return "lazy tactic"; }
113116
void collect_statistics(statistics& st) const override { if (m_tactic) m_tactic->collect_statistics(st); }

0 commit comments

Comments
 (0)