mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Fix the build on g++, Fix g++ warnings

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-15 16:36:57 -08:00
parent 4a97e6daea
commit f46c7f9bd9
2 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz_qe/hilbert_basis.cpp
View file

@ -63,7 +63,7 @@ public:
for (; it != end; ++it) {
offset_t offs(*it);
++m_stats.m_num_comparisons;
if (*it != idx.m_offset && hb.is_subsumed(idx, offs)) {
if (*it != static_cast<int>(idx.m_offset) && hb.is_subsumed(idx, offs)) {
found_idx = offs;
++m_stats.m_num_hit;
return true;
@ -743,7 +743,7 @@ hilbert_basis::sign_t hilbert_basis::get_sign(offset_t idx) const {
return zero;
}
hilbert_basis::numeral hilbert_basis::get_weight(values& val, num_vector const& ineq) const {
hilbert_basis::numeral hilbert_basis::get_weight(values const & val, num_vector const& ineq) const {
numeral result(0);
unsigned num_vars = get_num_vars();
for (unsigned i = 0; i < num_vars; ++i) {
@ -753,7 +753,6 @@ hilbert_basis::numeral hilbert_basis::get_weight(values& val, num_vector const&
}
void hilbert_basis::display(std::ostream& out) const {
unsigned nv = get_num_vars();
out << "inequalities:\n";
for (unsigned i = 0; i < m_ineqs.size(); ++i) {
display_ineq(out, m_ineqs[i], m_iseq[i]);

2
src/muz_qe/hilbert_basis.h
View file

@ -96,7 +96,7 @@ private:
void add_unit_vector(unsigned i, numeral const& e);
unsigned get_num_vars() const;
numeral get_weight(values& val, num_vector const& ineq) const;
numeral get_weight(values const & val, num_vector const& ineq) const;
bool is_geq(values const& v, values const& w) const;
bool is_abs_geq(numeral const& v, numeral const& w) const;
bool is_subsumed(offset_t idx);