mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

change lar_term into a class and make lar_terms::m_coeffs private

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-01 10:55:26 -07:00
parent f170d80d38
commit c74893016a
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/util/lp/lar_term.h
View file

@ -20,12 +20,10 @@
#pragma once #pragma once
#include "util/lp/indexed_vector.h" #include "util/lp/indexed_vector.h"
#include "util/map.h" #include "util/map.h"
namespace lp { namespace lp {
class lar_term { class lar_term {
// the term evaluates to sum of m_coeffs // the term evaluates to sum of m_coeffs
u_map<mpq> m_coeffs; u_map<mpq> m_coeffs;
// mpq m_v;
public: public:
lar_term() {} lar_term() {}
void add_monomial(const mpq& c, unsigned j) { void add_monomial(const mpq& c, unsigned j) {
@ -41,6 +39,11 @@ public:
} }
} }
void add_var(unsigned j) {
rational c(1);
add_monomial(c, j);
}
bool is_empty() const { bool is_empty() const {
return m_coeffs.empty(); // && is_zero(m_v); return m_coeffs.empty(); // && is_zero(m_v);
} }