From d084a19630a7c21018cb298258ac165e52f7fa2f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 17 Jan 2024 14:17:07 -1000 Subject: [PATCH] take care of strategy undecided, Nikolaj's comments Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 10 ++-------- src/math/lp/lar_solver.h | 1 - 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 5762cbc9a..d14a7489e 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1577,12 +1577,6 @@ namespace lp { } } - - var_index lar_solver::add_term_undecided(const vector>& coeffs) { - push_term(new lar_term(coeffs)); - return tv::mask_term(m_terms.size() - 1); - } - #if Z3DEBUG_CHECK_UNIQUE_TERMS bool lar_solver::term_coeffs_are_ok(const vector>& coeffs) { @@ -1645,9 +1639,9 @@ namespace lp { lar_term* t = new lar_term(coeffs); subst_known_terms(t); m_term_register.add_var(ext_i, term_is_int(t)); - if (strategy_is_undecided()) - return add_term_undecided(coeffs); push_term(t); + if (strategy_is_undecided()) + return tv::mask_term(m_terms.size() - 1); SASSERT(m_terms.size() == m_term_register.size()); unsigned adjusted_term_index = m_terms.size() - 1; var_index ret = tv::mask_term(adjusted_term_index); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 91d506e1e..b1abb21f7 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -137,7 +137,6 @@ class lar_solver : public column_namer { // terms bool all_vars_are_registered(const vector>& coeffs); - var_index add_term_undecided(const vector>& coeffs); bool term_coeffs_are_ok(const vector>& coeffs); void push_term(lar_term* t); void add_row_from_term_no_constraint(const lar_term* term, unsigned term_ext_index);