mirror of
https://github.com/Z3Prover/z3
synced 2026-07-17 12:35:44 +00:00
6ac3075022
This is another PR towards the goal of getting Z3 to compile cleanly when included via FetchContents into clang-tidy, which uses a pretty strict set of warnings. This is a second version of https://github.com/Z3Prover/z3/pull/9957. I address @NikolajBjorner 's comments about not changing the semicolons after macro invocations, because some editors work better with them present. It now, to the best of my ability, only deletes semis: * after the closing brace of namespace decl. * after the closing brace of an extern "C" decl. * after a function definition. This PR is very large, but it consists entirely of deletions of semicolons in these situations. (If there was a way to update the previous PR, which had been closed, and that is preferable, please let me know. I couldn't figure it out.)
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);
|
|
};
|
|
|
|
}
|
|
|