mirror of
https://github.com/Z3Prover/z3
synced 2026-02-11 19:34:32 +00:00
2e7b700769
* Initial plan * Update z3 codebase to use std::string_view (except z3++.h) - Updated params.cpp/h to use string_view internally for parameter descriptions - Updated trace.h/cpp to accept string_view for trace tag functions - Updated hash.h/cpp to use string_view for string_hash function - Updated all callers of string_hash to use string_view - Properly handled nullptr to empty string_view conversions - All tests passing Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add missing string_view includes to headers 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>
86 lines
1.9 KiB
C++
86 lines
1.9 KiB
C++
/*++
|
|
Copyright (c) 2006 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
id_gen.h
|
|
|
|
Abstract:
|
|
|
|
Basic support for generating & recycling ids.
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2008-02-02.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "util/vector.h"
|
|
#include "util/util.h"
|
|
|
|
class id_gen {
|
|
unsigned m_next_id;
|
|
unsigned_vector m_free_ids;
|
|
public:
|
|
id_gen(unsigned start = 0):m_next_id(start) {}
|
|
|
|
unsigned mk() {
|
|
unsigned r;
|
|
if (m_free_ids.empty()) {
|
|
r = m_next_id;
|
|
m_next_id++;
|
|
}
|
|
else {
|
|
r = m_free_ids.back();
|
|
m_free_ids.pop_back();
|
|
}
|
|
return r;
|
|
}
|
|
|
|
void recycle(unsigned id) {
|
|
if (memory::is_out_of_memory())
|
|
return;
|
|
m_free_ids.push_back(id);
|
|
}
|
|
|
|
void reset(unsigned start = 0) {
|
|
m_next_id = start;
|
|
m_free_ids.reset();
|
|
}
|
|
|
|
void cleanup(unsigned start = 0) {
|
|
m_next_id = start;
|
|
m_free_ids.finalize();
|
|
}
|
|
|
|
unsigned show_hash(){
|
|
unsigned h = string_hash(std::string_view((char *)&m_free_ids[0],m_free_ids.size()*sizeof(unsigned)),17);
|
|
return hash_u_u(h,m_next_id);
|
|
}
|
|
|
|
/**
|
|
\brief Return N if the range of ids generated by this module is in the set [0..N)
|
|
*/
|
|
unsigned get_id_range() const { return m_next_id; }
|
|
|
|
|
|
/**
|
|
\brief Debugging support method: set m_next_id to the least value id' s.t. id' >= id and id' is not in m_free_ids.
|
|
This method is only used to create small repros that exposes bugs in Z3.
|
|
*/
|
|
unsigned set_next_id(unsigned id) {
|
|
m_next_id = id;
|
|
while (std::find(m_free_ids.begin(), m_free_ids.end(), m_next_id) != m_free_ids.end())
|
|
m_next_id++;
|
|
return m_next_id;
|
|
}
|
|
|
|
void display_free_ids(std::ostream & out) {
|
|
::display(out, m_free_ids.begin(), m_free_ids.end());
|
|
}
|
|
|
|
};
|
|
|