mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

working on pb

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-02-26 09:06:25 -08:00
parent 54e3b5ee0d
commit 3757f337e5
5 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/pb_rewriter_def.h
View file

@ -247,7 +247,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
// example: k = 5, min = 3, max = 4: 5/3 -> 2 5/4 -> 1, n = 2 // example: k = 5, min = 3, max = 4: 5/3 -> 2 5/4 -> 1, n = 2
// replace all coefficients by 1, and k by 2. // replace all coefficients by 1, and k by 2.
// //
if (false && !k.is_one()) { if (!k.is_one()) {
PBU::numeral min = args[0].second, max = args[0].second; PBU::numeral min = args[0].second, max = args[0].second;
for (unsigned i = 1; i < args.size(); ++i) { for (unsigned i = 1; i < args.size(); ++i) {
if (args[i].second < min) min = args[i].second; if (args[i].second < min) min = args[i].second;

4
src/math/simplex/simplex.h
View file

@ -59,9 +59,11 @@ namespace simplex {
struct stats { struct stats {
unsigned m_num_pivots; unsigned m_num_pivots;
unsigned m_num_infeasible;
unsigned m_num_checks;
stats() { reset(); } stats() { reset(); }
void reset() { void reset() {
memset(this, sizeof(*this), 0); memset(this, 0, sizeof(*this));
} }
}; };

4
src/math/simplex/simplex_def.h
View file

@ -250,6 +250,7 @@ namespace simplex {
template<typename Ext> template<typename Ext>
lbool simplex<Ext>::make_feasible() { lbool simplex<Ext>::make_feasible() {
++m_stats.m_num_checks;
m_left_basis.reset(); m_left_basis.reset();
m_infeasible_var = null_var; m_infeasible_var = null_var;
unsigned num_iterations = 0; unsigned num_iterations = 0;
@ -266,6 +267,7 @@ namespace simplex {
if (!make_var_feasible(v)) { if (!make_var_feasible(v)) {
m_to_patch.insert(v); m_to_patch.insert(v);
m_infeasible_var = v; m_infeasible_var = v;
++m_stats.m_num_infeasible;
return l_false; return l_false;
} }
++num_iterations; ++num_iterations;
@ -873,6 +875,8 @@ namespace simplex {
void simplex<Ext>::collect_statistics(::statistics & st) const { void simplex<Ext>::collect_statistics(::statistics & st) const {
M.collect_statistics(st); M.collect_statistics(st);
st.update("simplex num pivots", m_stats.m_num_pivots); st.update("simplex num pivots", m_stats.m_num_pivots);
st.update("simplex num infeasible", m_stats.m_num_infeasible);
st.update("simplex num checks", m_stats.m_num_checks);
} }

2
src/math/simplex/sparse_matrix.h
View file

@ -44,7 +44,7 @@ namespace simplex {
unsigned m_add_rows; unsigned m_add_rows;
stats() { reset(); } stats() { reset(); }
void reset() { void reset() {
memset(this, sizeof(*this), 0); memset(this, 0, sizeof(*this));
} }
}; };

2
src/smt/theory_pb.cpp
View file

@ -546,12 +546,10 @@ namespace smt {
mpq_inf zero(mpq(0),mpq(0)), one(mpq(1),mpq(0)); mpq_inf zero(mpq(0),mpq(0)), one(mpq(1),mpq(0));
switch(ctx.get_assignment(rep.lit(i))) { switch(ctx.get_assignment(rep.lit(i))) {
case l_true: case l_true:
std::cout << "true\n";
VERIFY(update_bound(v, literal(v), true, one)); VERIFY(update_bound(v, literal(v), true, one));
m_simplex.set_lower(v, one); m_simplex.set_lower(v, one);
break; break;
case l_false: case l_false:
std::cout << "false\n";
VERIFY(update_bound(v, ~literal(v), false, zero)); VERIFY(update_bound(v, ~literal(v), false, zero));
m_simplex.set_upper(v, zero); m_simplex.set_upper(v, zero);
break; break;