mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-25 03:24:01 +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 GitHub
parent b778bf09f9
commit 2a5bfb818b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/seq_eq_solver.cpp
View file

@ -150,7 +150,8 @@ bool theory_seq::has_len_offset(expr_ref_vector const& ls, expr_ref_vector const
return true;
}
if (m_offset_eq.find(root1, root2, offset)) {
if (auto opt_offset = m_offset_eq.find(root1, root2)) {
offset = *opt_offset;
TRACE(seq, tout << "(" << mk_pp(l_fst, m) << ", " << mk_pp(r_fst,m) << " " << offset << ")\n";);
return true;
}

12
src/smt/seq_offset_eq.cpp
View file

@ -94,15 +94,17 @@ void seq_offset_eq::prop_arith_to_len_offset() {
}
}
bool seq_offset_eq::find(enode* n1, enode* n2, int& offset) const {
std::optional<int> seq_offset_eq::find(enode* n1, enode* n2) const {
n1 = n1->get_root();
n2 = n2->get_root();
if (n1->get_owner_id() > n2->get_owner_id())
std::swap(n1, n2);
return
!a.is_numeral(n1->get_expr()) &&
!a.is_numeral(n2->get_expr()) &&
m_offset_equalities.find(n1, n2, offset);
if (a.is_numeral(n1->get_expr()) || a.is_numeral(n2->get_expr()))
return std::nullopt;
int offset;
if (m_offset_equalities.find(n1, n2, offset))
return offset;
return std::nullopt;
}
bool seq_offset_eq::contains(enode* r) {

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);