mirror of
https://github.com/Z3Prover/z3
synced 2026-02-23 00:37:36 +00:00
17c8958d70
* Initial plan * Modernize C++ constructors to use C++11 default member initialization - Phase 1 Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> * Fix theory_pb.h struct definition - move reset() back inside struct Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> * Modernize C++ constructors to use C++11 default member initialization - Phase 2 Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> * Fix opt_solver.h - revert rational initialization (complex type) Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> * Modernize C++ constructors to use C++11 default member initialization - Phase 3 Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> * Fix sparse_matrix.h - explicitly initialize union member in default constructor Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> * Remove unnecessary default constructors when they're the only constructor Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
43 lines
1.2 KiB
C++
43 lines
1.2 KiB
C++
/*++
|
|
Copyright (c) 2007 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
approx_nat.h
|
|
|
|
Abstract:
|
|
|
|
Approximated natural numbers. It performs operations on the set [0, ..., 2^{n-2}, huge].
|
|
Where huge represents all numbers greater than 2^{n-2}.
|
|
|
|
Author:
|
|
|
|
Leonardo (leonardo) 2008-01-11
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include<ostream>
|
|
#include<climits>
|
|
|
|
class approx_nat {
|
|
unsigned m_value = 0;
|
|
static const unsigned m_limit = UINT_MAX >> 2;
|
|
public:
|
|
approx_nat() = default;
|
|
explicit approx_nat(unsigned val);
|
|
bool is_huge() const { return m_value == UINT_MAX; }
|
|
unsigned get_value() const { return m_value; }
|
|
approx_nat & operator=(unsigned w);
|
|
approx_nat & operator+=(unsigned w);
|
|
approx_nat & operator+=(approx_nat const & w) { return operator+=(w.m_value); }
|
|
approx_nat & operator*=(unsigned w);
|
|
approx_nat & operator*=(approx_nat const & w) { return operator*=(w.m_value); }
|
|
bool operator<(unsigned w) const { return !is_huge() && m_value < w; }
|
|
bool operator<(approx_nat const & w) const { return !is_huge() && !w.is_huge() && m_value < w.m_value; }
|
|
};
|
|
|
|
std::ostream & operator<<(std::ostream & target, approx_nat const & w);
|
|
|