mirror of
https://github.com/Z3Prover/z3
synced 2026-02-14 21:01:49 +00:00
2a5bfb818b
* 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>
57 lines
1.4 KiB
C++
57 lines
1.4 KiB
C++
/*++
|
|
Copyright (c) 2011 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
seq_offset_eq.h
|
|
|
|
Abstract:
|
|
|
|
Container for maintaining equalities between lengths of sequences.
|
|
|
|
Author:
|
|
|
|
Thai Minh Trinh 2017
|
|
Nikolaj Bjorner (nbjorner) 2020-4-16
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "util/obj_pair_hashtable.h"
|
|
#include "ast/seq_decl_plugin.h"
|
|
#include "ast/arith_decl_plugin.h"
|
|
#include "smt/smt_theory.h"
|
|
#include <optional>
|
|
|
|
namespace smt {
|
|
|
|
class seq_offset_eq {
|
|
theory& th;
|
|
ast_manager& m;
|
|
seq_util seq;
|
|
arith_util a;
|
|
obj_hashtable<enode> m_has_offset_equality;
|
|
obj_pair_map<enode, enode, int> m_offset_equalities;
|
|
int m_propagation_level;
|
|
|
|
bool match_x_minus_y(expr* e, expr*& x, expr*& y) const;
|
|
void len_offset(expr* e, int val);
|
|
void prop_arith_to_len_offset();
|
|
|
|
public:
|
|
|
|
seq_offset_eq(theory& th, ast_manager& m);
|
|
bool empty() const { return m_offset_equalities.empty(); }
|
|
/**
|
|
\brief determine if r1 = r2 + offset
|
|
\return optional containing the offset if found, nullopt otherwise
|
|
*/
|
|
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);
|
|
};
|
|
|
|
};
|
|
|