mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

add restore_patched_values

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-26 17:27:55 -07:00
parent 47d5515b78
commit 6a5579341d
3 changed files with 16 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/lar_solver.h
View file

@ -266,10 +266,10 @@ class lar_solver : public column_namer {
void register_normalized_term(const lar_term&, lpvar); void register_normalized_term(const lar_term&, lpvar);
void deregister_normalized_term(const lar_term&); void deregister_normalized_term(const lar_term&);
bool inside_bounds(lpvar, const impq&) const; bool inside_bounds(lpvar, const impq&) const;
public:
inline void set_column_value(unsigned j, const impq& v) { inline void set_column_value(unsigned j, const impq& v) {
m_mpq_lar_core_solver.m_r_solver.update_x(j, v); m_mpq_lar_core_solver.m_r_solver.update_x(j, v);
} }
public:
inline void set_column_value_test(unsigned j, const impq& v) { inline void set_column_value_test(unsigned j, const impq& v) {
set_column_value(j, v); set_column_value(j, v);
} }
@ -306,7 +306,9 @@ public:
bool column_corresponds_to_term(unsigned) const; bool column_corresponds_to_term(unsigned) const;
inline unsigned row_count() const { return A_r().row_count(); } inline unsigned row_count() const { return A_r().row_count(); }
bool var_is_registered(var_index vj) const; bool var_is_registered(var_index vj) const;
inline void remove_column_from_inf_set(unsigned j) {
m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j);
}
template <typename CallBeforeChange, typename ChangeReport> template <typename CallBeforeChange, typename ChangeReport>
void change_basic_columns_dependend_on_a_given_nb_column_report(unsigned j, void change_basic_columns_dependend_on_a_given_nb_column_report(unsigned j,
const numeric_pair<mpq> & delta, const numeric_pair<mpq> & delta,

10
src/math/lp/nla_core.cpp
View file

@ -1381,6 +1381,13 @@ void core::patch_monomial(lpvar j) {
} }
} }
void core::restore_patched_values() {
for (const auto & p : m_changes_of_patch) {
m_lar_solver.set_column_value(p.m_key, lp::impq(p.m_value));
m_lar_solver.remove_column_from_inf_set(p.m_key);
}
}
void core::patch_monomials() { void core::patch_monomials() {
m_changes_of_patch.reset(); m_changes_of_patch.reset();
auto to_refine = m_to_refine.index(); auto to_refine = m_to_refine.index();
@ -1393,6 +1400,9 @@ void core::patch_monomials() {
if (m_to_refine.size() == 0) if (m_to_refine.size() == 0)
break; break;
} }
if (m_to_refine.size()) {
restore_patched_values();
}
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
/* /*
If the tableau is not feasible we need to fix all non-linear If the tableau is not feasible we need to fix all non-linear

2
src/math/lp/nla_core.h
View file

@ -480,6 +480,8 @@ public:
void set_use_nra_model(bool m) { m_use_nra_model = m; } void set_use_nra_model(bool m) { m_use_nra_model = m; }
bool use_nra_model() const { return m_use_nra_model; } bool use_nra_model() const { return m_use_nra_model; }
void collect_statistics(::statistics&); void collect_statistics(::statistics&);
private:
void restore_patched_values();
}; // end of core }; // end of core
struct pp_mon { struct pp_mon {