mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Make a few variables private

Browse source
This commit is contained in:
Anh-Dung Phan 2013-10-30 06:30:51 +01:00
parent f5e6a18015
commit a6e103dd36
5 changed files with 24 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/network_flow_def.h
View file

@ -125,10 +125,10 @@ namespace smt {
edge_id e_id;
get_edge_id(u, v, e_id);
if (m_upwards[u]) {
m_potentials[u] = m_potentials[v] + m_graph.get_weight(e_id);
m_potentials[u] = m_potentials[v] - m_graph.get_weight(e_id);
}
else {
m_potentials[u] = m_potentials[v] - m_graph.get_weight(e_id);
m_potentials[u] = m_potentials[v] + m_graph.get_weight(e_id);
}
u = m_thread[u];
}

5
src/smt/theory_arith.h
View file

@ -432,6 +432,8 @@ namespace smt {
bool m_eager_gcd; // true if gcd should be applied at every add_row
unsigned m_final_check_idx;
inf_rational m_objective_value;
// backtracking
svector<bound_trail> m_bound_trail;
svector<unsigned> m_unassigned_atoms_trail;
@ -997,8 +999,7 @@ namespace smt {
virtual theory_var add_objective(app* term);
virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
virtual expr* block_lower_bound(theory_var v, inf_rational const& val);
inf_rational m_objective_value;
// -----------------------------------
//
// Pretty Printing

5
src/smt/theory_arith_aux.h
View file

@ -998,9 +998,8 @@ namespace smt {
}
template<typename Ext>
inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) {
inf_eps_rational<inf_rational> val(m_objective_value);
return val;
inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) {
return inf_eps_rational<inf_rational>(m_objective_value);
}
/**

16
src/smt/theory_diff_logic.h
View file

@ -185,7 +185,13 @@ namespace smt {
arith_factory * m_factory;
rational m_delta;
nc_functor m_nc_functor;
nc_functor m_nc_functor;
// For optimization purpose
typedef vector <std::pair<theory_var, rational> > objective_term;
vector<objective_term> m_objectives;
vector<rational> m_objective_consts;
numeral m_objective_value;
// Set a conflict due to a negative cycle.
void set_neg_cycle_conflict();
@ -309,14 +315,6 @@ namespace smt {
virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
virtual expr* block_lower_bound(theory_var v, inf_rational const& val);
// TBD: why are these public?:
numeral m_objective_value;
typedef vector <std::pair<theory_var, rational> > objective_term;
vector<objective_term> m_objectives;
vector<rational> m_objective_consts;
bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);
private:

15
src/smt/theory_diff_logic_def.h
View file

@ -1004,10 +1004,10 @@ bool theory_diff_logic<Ext>::maximize(theory_var v) {
objective_term const& objective = m_objectives[v];
IF_VERBOSE(1,
for (unsigned i = 0; i < objective.size(); ++i) {
verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
}
verbose_stream() << m_objective_consts[v] << "\n";);
for (unsigned i = 0; i < objective.size(); ++i) {
verbose_stream() << "coefficient " << objective[i].second << " of theory_var " << objective[i].first << "\n";
}
verbose_stream() << m_objective_consts[v] << "\n";);
// Objective coefficients now become balances
vector<fin_numeral> balances(m_graph.get_num_nodes());
@ -1023,7 +1023,12 @@ bool theory_diff_logic<Ext>::maximize(theory_var v) {
vector<numeral> potentials;
m_objective_value = net_flow.get_optimal_solution(potentials, true);
std::cout << "Objective value of var " << v << ": " << m_objective_value << std::endl;
// TODO: return the model of the optimal solution from potential
// TODO: return the model of the optimal solution from potentials
IF_VERBOSE(1,
for (unsigned i = 0; i < potentials.size(); ++i) {
verbose_stream() << "v" << i << " -> " << potentials[i] << "\n";
});
}
else {
std::cout << "Unbounded objective" << std::endl;