mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-10 02:50:55 +00:00
Code Activity

Refactor find_tactic_cmd to use std::optional<tactic_cmd*> (#8331)

Browse source 
* Initial plan

* Refactor find_tactic_cmd to use std::optional<tactic_cmd*>

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-25 12:38:34 -08:00 • committed by GitHub
parent 944777afc0
commit 7b182c9440
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 15 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_tactic.cpp
View file

@ -59,14 +59,14 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_tactic(c, name);
RESET_ERROR_CODE();
tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
if (t == nullptr) {
auto t = mk_c(c)->find_tactic_cmd(symbol(name));
if (!t) {
std::stringstream err;
err << "unknown tactic " << name;
SET_ERROR_CODE(Z3_INVALID_ARG, err.str());
RETURN_Z3(nullptr);
}
tactic * new_t = t->mk(mk_c(c)->m());
tactic * new_t = (*t)->mk(mk_c(c)->m());
RETURN_TACTIC(new_t);
Z3_CATCH_RETURN(nullptr);
}
@ -391,12 +391,12 @@ extern "C" {
Z3_TRY;
LOG_Z3_tactic_get_descr(c, name);
RESET_ERROR_CODE();
tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
if (t == nullptr) {
auto t = mk_c(c)->find_tactic_cmd(symbol(name));
if (!t) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return "";
}
return t->get_descr();
return (*t)->get_descr();
Z3_CATCH_RETURN("");
}