diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 7ce1e3f88..53c5f2b16 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -20,12 +20,10 @@ #pragma once #include "util/lp/indexed_vector.h" #include "util/map.h" - namespace lp { class lar_term { // the term evaluates to sum of m_coeffs u_map m_coeffs; - // mpq m_v; public: lar_term() {} void add_monomial(const mpq& c, unsigned j) { @@ -40,6 +38,11 @@ public: m_coeffs.erase(j); } } + + void add_var(unsigned j) { + rational c(1); + add_monomial(c, j); + } bool is_empty() const { return m_coeffs.empty(); // && is_zero(m_v);