mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 22:36:10 +00:00
Code Activity

Update src/math/simplex/model_based_opt.h

Browse source 
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-02-27 17:29:37 -10:00 • committed by GitHub
parent fc6696c5e4
commit 835da14afa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/simplex/model_based_opt.h
View file

@ -162,18 +162,18 @@ namespace opt {
struct add_def : public def { struct add_def : public def {
def* x, *y; def* x, *y;
add_def(def* x, def* y) : x(x), y(y) { m_type = add_t; x->inc_ref(); y->inc_ref(); } add_def(def* x, def* y) : x(x), y(y) { m_type = add_t; x->inc_ref(); y->inc_ref(); }
~add_def() { x->dec_ref(); y->dec_ref(); } ~add_def() override { x->dec_ref(); y->dec_ref(); }
}; };
struct mul_def : public def { struct mul_def : public def {
def* x, *y; def* x, *y;
mul_def(def* x, def* y) : x(x), y(y) { m_type = mul_t; x->inc_ref(); y->inc_ref(); } mul_def(def* x, def* y) : x(x), y(y) { m_type = mul_t; x->inc_ref(); y->inc_ref(); }
~mul_def() { x->dec_ref(); y->dec_ref(); } ~mul_def() override { x->dec_ref(); y->dec_ref(); }
}; };
struct div_def : public def { struct div_def : public def {
def* x; def* x;
rational m_div{ 1 }; rational m_div{ 1 };
div_def(def* x, rational const& d) : x(x), m_div(d) { m_type = div_t; x->inc_ref(); } div_def(def* x, rational const& d) : x(x), m_div(d) { m_type = div_t; x->inc_ref(); }
~div_def() { x->dec_ref(); } ~div_def() override { x->dec_ref(); }
}; };
struct var_def : public def { struct var_def : public def {
var v; var v;