mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Fix fixedpoint rc bug and fix optimize non-const bug (#5173)
* Fix fixedpoint rc bug and fix optimize non-const bug * Fix indentation
This commit is contained in:
parent
d73b883b38
commit
4625454a38
|
@ -275,7 +275,7 @@ namespace z3 {
|
|||
/**
|
||||
\brief Return a floating point sort.
|
||||
\c ebits is a number of exponent bits,
|
||||
\c sbits is a number of significand bits,
|
||||
\c sbits is a number of significand bits,
|
||||
\pre where ebits must be larger than 1 and sbits must be larger than 2.
|
||||
*/
|
||||
sort fpa_sort(unsigned ebits, unsigned sbits);
|
||||
|
@ -2836,9 +2836,8 @@ namespace z3 {
|
|||
unsigned h() const { return m_h; }
|
||||
};
|
||||
optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
|
||||
optimize(optimize& o):object(o) {
|
||||
optimize(optimize const & o):object(o), m_opt(o.m_opt) {
|
||||
Z3_optimize_inc_ref(o.ctx(), o.m_opt);
|
||||
m_opt = o.m_opt;
|
||||
}
|
||||
optimize(context& c, optimize& src):object(c) {
|
||||
m_opt = Z3_mk_optimize(c);
|
||||
|
@ -2934,7 +2933,15 @@ namespace z3 {
|
|||
Z3_fixedpoint m_fp;
|
||||
public:
|
||||
fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
|
||||
fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
|
||||
~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
|
||||
fixedpoint & operator=(fixedpoint const & o) {
|
||||
Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
|
||||
Z3_fixedpoint_dec_ref(ctx(), m_fp);
|
||||
m_fp = o.m_fp;
|
||||
object::operator=(o);
|
||||
return *this;
|
||||
}
|
||||
operator Z3_fixedpoint() const { return m_fp; }
|
||||
void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); }
|
||||
void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
|
||||
|
|
Loading…
Reference in a new issue