mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

Refactor seq_offset_eq::find to use std::optional (#8300)

Browse source 
* Initial plan

* Refactor seq_offset_eq::find to use std::optional

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-23 10:18:51 -08:00 • committed by Nikolaj Bjorner
parent a273db43da
commit 36dc400978
3 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/seq_offset_eq.h
View file

@ -21,6 +21,7 @@ Author:
#include "ast/seq_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "smt/smt_theory.h"
#include <optional>
namespace smt {
@ -43,9 +44,10 @@ namespace smt {
bool empty() const { return m_offset_equalities.empty(); }
/**
\brief determine if r1 = r2 + offset
\return optional containing the offset if found, nullopt otherwise
*/
bool find(enode* r1, enode* r2, int& offset) const;
bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); }
std::optional<int> find(enode* r1, enode* r2) const;
bool contains(enode* r1, enode* r2) const { return find(r1, r2).has_value(); }
bool contains(enode* r);
bool propagate();
void pop_scope_eh(unsigned num_scopes);