mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

toward full patching in nl

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-28 10:21:04 -07:00
parent c58bd3105b
commit 91d9b0319e
3 changed files with 26 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1306,11 +1306,10 @@ bool core::patch_blocker(lpvar u, const monic& m, const lp::impq& ival) const {
}
bool core::try_to_patch(lpvar k, const rational& v, const monic & m) {
auto call_before_change = [this](lpvar u) { m_changes_of_patch.insert_if_not_there(u, val(u)); };
auto blocker = [this, k, m](lpvar u, const lp::impq& v)
{ return u != k && patch_blocker(u, m, v); };
auto change_report = [this](lpvar u) { update_to_refine_of_var(u); };
return m_lar_solver.try_to_patch(k, v, blocker, call_before_change, change_report);
return m_lar_solver.try_to_patch(k, v, blocker, change_report);
}
bool in_power(const svector<lpvar>& vs, unsigned l) {
@ -1382,16 +1381,7 @@ 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() {
m_changes_of_patch.reset();
m_cautious_patching = true;
void core::patch_monomials_on_to_refine() {
auto to_refine = m_to_refine.index();
// the rest of the function might change m_to_refine, so have to copy
unsigned sz = to_refine.size();
@ -1402,19 +1392,24 @@ void core::patch_monomials() {
if (m_to_refine.size() == 0)
break;
}
}
void core::patch_monomials() {
m_cautious_patching = true;
patch_monomials_on_to_refine();
if (m_to_refine.size() == 0 || !m_nla_settings.expensive_patching()) {
return;
}
m_cautious_patching = false; //
NOT_IMPLEMENTED_YET(); // have to repeat the patching
patch_monomials_on_to_refine();
m_lar_solver.push();
save_tableau();
constrain_nl_in_tableau();
if (solve_tableau() && integrality_holds()) {
m_lar_solver.pop(1);
} else {
m_lar_solver.pop();
restore_patched_values();
restore_tableau();
m_lar_solver.clear_inf_set();
}
SASSERT(m_lar_solver.ax_is_correct());
@ -1428,6 +1423,14 @@ bool core::solve_tableau() {
NOT_IMPLEMENTED_YET();
}
void core::restore_tableau() {
NOT_IMPLEMENTED_YET();
}
void core::save_tableau() {
NOT_IMPLEMENTED_YET();
}
bool core::integrality_holds() {
NOT_IMPLEMENTED_YET();
}