mirror of
https://github.com/Z3Prover/z3
synced 2026-02-05 16:56:18 +00:00
Refactor find_psort_decl() to return std::optional<psort_decl*> (#8339)
* Initial plan * Refactor find_psort_decl() to return std::optional<psort_decl*> 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:
parent
49817bc259
commit
445f995c54
4 changed files with 30 additions and 28 deletions
|
|
@ -20,6 +20,7 @@ Notes:
|
|||
--*/
|
||||
#pragma once
|
||||
|
||||
#include<optional>
|
||||
#include<sstream>
|
||||
#include<vector>
|
||||
#include "util/stopwatch.h"
|
||||
|
|
@ -470,7 +471,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);
|
||||
psort_decl * find_psort_decl(symbol const & s) const;
|
||||
std::optional<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;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue