mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-02 15:26:17 +00:00
Code Activity

Revert "Refactor find_probe() to use std::optional (#8334)"

Browse source 
This reverts commit 49817bc259.
This commit is contained in:
Nikolaj Bjorner 2026-01-26 13:19:56 -08:00
parent 7a2eea6f40
commit 3f26d42215
4 changed files with 13 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/cmd_context/tactic_cmds.cpp
View file

@ -767,9 +767,9 @@ MK_NARY_PROBE(mk_mul);
probe * sexpr2probe(cmd_context & ctx, sexpr * n) {
if (n->is_symbol()) {
auto pinfo = ctx.find_probe(n->get_symbol());
if (pinfo)
return (*pinfo)->get();
probe_info * pinfo = ctx.find_probe(n->get_symbol());
if (pinfo != nullptr)
return pinfo->get();
throw cmd_exception("invalid probe, unknown builtin probe ", n->get_symbol(), n->get_line(), n->get_pos());
}
else if (n->is_numeral()) {

7
src/cmd_context/tactic_manager.cpp
View file

@ -70,10 +70,9 @@ simplifier_cmd * tactic_manager::find_simplifier_cmd(symbol const & s) const {
return c;
}
std::optional<probe_info*> tactic_manager::find_probe(symbol const & s) const {
probe_info * tactic_manager::find_probe(symbol const & s) const {
probe_info * p = nullptr;
if (m_name2probe.find(s, p))
return p;
return std::nullopt;
m_name2probe.find(s, p);
return p;
}

2
src/cmd_context/tactic_manager.h
View file

@ -38,7 +38,7 @@ public:
void insert(simplifier_cmd* c);
void insert(probe_info * p);
std::optional<tactic_cmd*> find_tactic_cmd(symbol const & s) const;
std::optional<probe_info*> find_probe(symbol const & s) const;
probe_info * find_probe(symbol const & s) const;
simplifier_cmd* find_simplifier_cmd(symbol const& s) const;
unsigned num_tactics() const { return m_tactics.size(); }