mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 10:35:36 +00:00
Code Activity

Store rational by value in parameter variant (#8518)

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
Copilot 2026-02-08 12:17:13 +00:00 • committed by GitHub
parent 6ed5b6d667
commit 47897d6fb6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast.cpp
View file

@ -41,18 +41,12 @@ Revision History:
// -----------------------------------
parameter::~parameter() {
if (auto p = std::get_if<rational*>(&m_val)) {
dealloc(*p);
}
if (auto p = std::get_if<zstring*>(&m_val)) {
dealloc(*p);
}
}
parameter::parameter(parameter const& other) : m_val(other.m_val) {
if (auto p = std::get_if<rational*>(&m_val)) {
m_val = alloc(rational, **p);
}
if (auto p = std::get_if<zstring*>(&m_val)) {
m_val = alloc(zstring, **p);
}

8
src/ast/ast.h
View file

@ -123,7 +123,7 @@ private:
ast*, // for PARAM_AST
symbol, // for PARAM_SYMBOL
zstring*, // for PARAM_ZSTRING
rational*, // for PARAM_RATIONAL
rational, // for PARAM_RATIONAL
double, // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
unsigned // for PARAM_EXTERNAL
> m_val = 0;
@ -135,8 +135,8 @@ public:
explicit parameter(unsigned val): m_val((int)val) {}
explicit parameter(ast * p): m_val(p) {}
explicit parameter(symbol const & s): m_val(s) {}
explicit parameter(rational const & r): m_val(alloc(rational, r)) {}
explicit parameter(rational && r) : m_val(alloc(rational, std::move(r))) {}
explicit parameter(rational const & r): m_val(r) {}
explicit parameter(rational && r) : m_val(std::move(r)) {}
explicit parameter(zstring const& s): m_val(alloc(zstring, s)) {}
explicit parameter(zstring && s): m_val(alloc(zstring, std::move(s))) {}
explicit parameter(double d): m_val(d) {}
@ -188,7 +188,7 @@ public:
int get_int() const { SASSERT(is_int()); return std::get<int>(m_val); }
ast * get_ast() const { SASSERT(is_ast()); return std::get<ast*>(m_val); }
symbol get_symbol() const { SASSERT(is_symbol()); return std::get<symbol>(m_val); }
rational const & get_rational() const { SASSERT(is_rational()); return *std::get<rational*>(m_val); }
rational const & get_rational() const { SASSERT(is_rational()); return std::get<rational>(m_val); }
zstring const& get_zstring() const { SASSERT(is_zstring()); return *std::get<zstring*>(m_val); }
double get_double() const { SASSERT(is_double()); return std::get<double>(m_val); }
unsigned get_ext_id() const { SASSERT(is_external()); return std::get<unsigned>(m_val); }