From 7a2eea6f40f80e79918ea9dd5ac205520f35e490 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Jan 2026 13:19:51 -0800 Subject: [PATCH] Revert "Refactor find_psort_decl() to return std::optional (#8339)" This reverts commit 445f995c54df8be09b62dc2d732767e0275f564a. --- src/cmd_context/basic_cmds.cpp | 8 +++---- src/cmd_context/cmd_context.cpp | 7 +++--- src/cmd_context/cmd_context.h | 3 +-- src/parsers/smt2/smt2parser.cpp | 40 ++++++++++++++++----------------- 4 files changed, 28 insertions(+), 30 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index aec2ab59f..46e66aaec 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -887,20 +887,20 @@ public: m_array_fid = null_family_id; } void execute(cmd_context & ctx) override { - auto array_sort = ctx.find_psort_decl(m_array_sort); - if (!array_sort) + psort_decl * array_sort = ctx.find_psort_decl(m_array_sort); + if (array_sort == nullptr) throw cmd_exception("Array sort is not available"); ptr_vector & array_sort_args = m_domain; sort_ref_buffer domain(ctx.m()); unsigned arity = m_f->get_arity(); for (unsigned i = 0; i < arity; ++i) { array_sort_args.push_back(m_f->get_domain(i)); - domain.push_back((*array_sort)->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data())); + domain.push_back(array_sort->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data())); array_sort_args.pop_back(); } sort_ref range(ctx.m()); array_sort_args.push_back(m_f->get_range()); - range = (*array_sort)->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data()); + range = array_sort->instantiate(ctx.pm(), array_sort_args.size(), array_sort_args.data()); parameter p(m_f); func_decl_ref new_map(ctx.m()); new_map = ctx.m().mk_func_decl(get_array_fid(ctx), OP_ARRAY_MAP, 1, &p, domain.size(), domain.data(), range.get()); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 42b19cfdc..b065607f6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1166,11 +1166,10 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, throw cmd_exception("invalid function declaration reference, unknown indexed function ", s); } -std::optional cmd_context::find_psort_decl(symbol const & s) const { +psort_decl * cmd_context::find_psort_decl(symbol const & s) const { psort_decl * p = nullptr; - if (m_psort_decls.find(s, p)) - return p; - return std::nullopt; + m_psort_decls.find(s, p); + return p; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index eb4a84de4..8a742824b 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -20,7 +20,6 @@ Notes: --*/ #pragma once -#include #include #include #include "util/stopwatch.h" @@ -471,7 +470,7 @@ public: func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, unsigned arity, sort * const * domain, sort * range); recfun::promise_def decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range); - std::optional find_psort_decl(symbol const & s) const; + psort_decl * find_psort_decl(symbol const & s) const; cmd * find_cmd(symbol const & s) const; sexpr * find_user_tactic(symbol const & s) const; object_ref * find_object_ref(symbol const & s) const; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 8e7ec0dbe..3f04ad9f0 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -582,12 +582,12 @@ namespace smt2 { sort * parse_sort_name(char const* context = "") { SASSERT(curr_is_identifier()); symbol id = curr_id(); - auto d = m_ctx.find_psort_decl(id); - if (!d) + psort_decl * d = m_ctx.find_psort_decl(id); + if (d == nullptr) unknown_sort(id, context); - if (!(*d)->has_var_params() && (*d)->get_num_params() != 0) + if (!d->has_var_params() && d->get_num_params() != 0) throw parser_exception("sort constructor expects parameters"); - sort * r = (*d)->instantiate(pm()); + sort * r = d->instantiate(pm()); if (r == nullptr) throw parser_exception("invalid sort application"); next(); @@ -597,12 +597,12 @@ namespace smt2 { psort * parse_psort_name(bool ignore_unknown_sort = false) { SASSERT(curr_is_identifier()); symbol id = curr_id(); - auto d = m_ctx.find_psort_decl(id); - if (d) { - if (!(*d)->has_var_params() && (*d)->get_num_params() != 0) + psort_decl * d = m_ctx.find_psort_decl(id); + if (d != nullptr) { + if (!d->has_var_params() && d->get_num_params() != 0) throw parser_exception("sort constructor expects parameters"); next(); - return pm().mk_psort_app(*d); + return pm().mk_psort_app(d); } else { int idx = 0; @@ -625,8 +625,8 @@ namespace smt2 { SASSERT(curr_id_is_underscore()); next(); symbol id = check_identifier_next("invalid indexed sort, symbol expected"); - auto d = m_ctx.find_psort_decl(id); - if (!d) + psort_decl * d = m_ctx.find_psort_decl(id); + if (d == nullptr) unknown_sort(id); sbuffer args; while (!curr_is_rparen()) { @@ -635,7 +635,7 @@ namespace smt2 { args.push_back(u); next(); } - sort * r = (*d)->instantiate(pm(), args.size(), args.data()); + sort * r = d->instantiate(pm(), args.size(), args.data()); if (r == nullptr) throw parser_exception("invalid sort application"); next(); @@ -645,13 +645,13 @@ namespace smt2 { void push_psort_app_frame() { SASSERT(curr_is_identifier()); symbol id = curr_id(); - auto d = m_ctx.find_psort_decl(id); - if (!d) { + psort_decl * d = m_ctx.find_psort_decl(id); + if (d == nullptr) { unknown_sort(id); } next(); void * mem = m_stack.allocate(sizeof(psort_frame)); - new (mem) psort_frame(*this, *d, psort_stack().size()); + new (mem) psort_frame(*this, d, psort_stack().size()); } void pop_psort_app_frame() { @@ -708,12 +708,12 @@ namespace smt2 { void push_sort_app_frame() { SASSERT(curr_is_identifier()); symbol id = curr_id(); - auto d = m_ctx.find_psort_decl(id); - if (!d) + psort_decl * d = m_ctx.find_psort_decl(id); + if (d == nullptr) unknown_sort(id); next(); void * mem = m_stack.allocate(sizeof(sort_frame)); - new (mem) sort_frame(*this, *d, sort_stack().size()); + new (mem) sort_frame(*this, d, sort_stack().size()); } void pop_sort_app_frame() { @@ -867,7 +867,7 @@ namespace smt2 { check_nonreserved_identifier("invalid sort declaration, symbol expected"); symbol id = curr_id(); - if (m_ctx.find_psort_decl(id)) + if (m_ctx.find_psort_decl(id) != nullptr) throw parser_exception("invalid sort declaration, sort already declared/defined"); next(); check_rparen("invalid sort declaration, ')' expected"); @@ -2273,7 +2273,7 @@ namespace smt2 { check_nonreserved_identifier("invalid sort declaration, symbol expected"); symbol id = curr_id(); - if (m_ctx.find_psort_decl(id)) + if (m_ctx.find_psort_decl(id) != nullptr) throw parser_exception("invalid sort declaration, sort already declared/defined"); next(); if (curr_is_rparen()) { @@ -2298,7 +2298,7 @@ namespace smt2 { next(); check_nonreserved_identifier("invalid sort definition, symbol expected"); symbol id = curr_id(); - if (m_ctx.find_psort_decl(id)) + if (m_ctx.find_psort_decl(id) != nullptr) throw parser_exception("invalid sort definition, sort already declared/defined"); next(); parse_sort_decl_params();