mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
remove the fresh definition when removing its column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
Lev Nachmanson
parent
17d68c18aa
commit
dcd5783232
|
|
@ -46,7 +46,8 @@
|
|||
the i-th entry.
|
||||
*/
|
||||
namespace lp {
|
||||
template <typename T, typename K> bool contains(const T& t, K j) {
|
||||
template <typename T, typename K>
|
||||
bool contains(const T& t, K j) {
|
||||
return t.find(j) != t.end();
|
||||
}
|
||||
|
||||
|
|
@ -133,13 +134,11 @@ namespace lp {
|
|||
};
|
||||
|
||||
template <typename T>
|
||||
class bij_map {
|
||||
struct bij_map {
|
||||
// We store T indexed by 'b' in an std::unordered_map, and use bijection to map from 'a' to 'b'.
|
||||
|
||||
bijection m_bij;
|
||||
std::unordered_map<unsigned, T> m_data;
|
||||
|
||||
public:
|
||||
// Adds a->b in m_bij, associates val with b.
|
||||
void add(unsigned a, unsigned b, const T& val) {
|
||||
// You might have some method in bijection such as 'insert(a, b)'
|
||||
|
|
@ -155,7 +154,7 @@ namespace lp {
|
|||
}
|
||||
|
||||
void erase_by_second_key(unsigned b) {
|
||||
VERIFY(m_bij.has_val(b));
|
||||
SASSERT(m_bij.has_val(b));
|
||||
m_bij.erase_val(b);
|
||||
auto it = m_data.find(b);
|
||||
VERIFY(it != m_data.end());
|
||||
|
|
@ -258,7 +257,6 @@ namespace lp {
|
|||
[](int j) -> std::string { return "x" + std::to_string(j); }, out);
|
||||
}
|
||||
|
||||
|
||||
// used for debug only
|
||||
std::ostream& print_lar_term_L(const std_vector<iv>& t, std::ostream& out) const {
|
||||
vector<std::pair<mpq, unsigned>> tp;
|
||||
|
|
@ -417,8 +415,7 @@ namespace lp {
|
|||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
} else {
|
||||
// Check that var() in m_data[idx] matches j
|
||||
if (idx < 0 || static_cast<unsigned>(idx) >= m_data.size()) {
|
||||
return false;
|
||||
|
|
@ -452,14 +449,13 @@ namespace lp {
|
|||
m_data.clear();
|
||||
SASSERT(invariant());
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
term_with_index m_l_terms_workspace;
|
||||
term_with_index m_substitution_workspace;
|
||||
|
||||
bijection m_k2s;
|
||||
bij_map<lar_term> m_fresh_k2xt_terms;
|
||||
bij_map<std::pair<lar_term, unsigned>> m_fresh_k2xt_terms;
|
||||
// m_row2fresh_defs[i] is the set of all fresh variables xt
|
||||
// such that pairs (xt, m_fresh_k2xt_terms[xt]) is a fresh definition introduced for row i
|
||||
// When row i is changed all entries depending on m_fresh_k2xt_terms[xt] should be recalculated,
|
||||
|
|
@ -472,7 +468,6 @@ namespace lp {
|
|||
// m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j
|
||||
std::unordered_map<unsigned, std::unordered_set<unsigned>> m_columns_to_terms;
|
||||
|
||||
|
||||
unsigned m_conflict_index = -1; // the row index of the conflict
|
||||
unsigned m_max_of_branching_iterations = 0;
|
||||
unsigned m_number_of_branching_calls;
|
||||
|
|
@ -539,15 +534,7 @@ namespace lp {
|
|||
SASSERT(std::find(m_added_terms.begin(), m_added_terms.end(), t) == m_added_terms.end());
|
||||
SASSERT(contains(m_active_terms, t));
|
||||
m_active_terms.erase(t);
|
||||
TRACE("dioph_eq",
|
||||
tout << "the deleted term column in m_l_matrix" << std::endl;
|
||||
for (auto p: m_l_matrix.column(t->j())) {
|
||||
tout << "p.coeff():" << p.coeff()<< ", row " << p.var() << std::endl;
|
||||
}
|
||||
tout << "m_l_matrix has " << m_l_matrix.column_count() << " columns"<< std::endl;
|
||||
tout << "and " << m_l_matrix.row_count() << " rows" << std::endl;
|
||||
print_lar_term_L(*t, tout); tout << "; t->j()=" << t->j() << std::endl;
|
||||
);
|
||||
TRACE("dioph_eq", tout << "the deleted term column in m_l_matrix" << std::endl; for (auto p : m_l_matrix.column(t->j())) { tout << "p.coeff():" << p.coeff() << ", row " << p.var() << std::endl; } tout << "m_l_matrix has " << m_l_matrix.column_count() << " columns" << std::endl; tout << "and " << m_l_matrix.row_count() << " rows" << std::endl; print_lar_term_L(*t, tout); tout << "; t->j()=" << t->j() << std::endl;);
|
||||
shrink_matrices();
|
||||
}
|
||||
|
||||
|
|
@ -569,7 +556,7 @@ namespace lp {
|
|||
}
|
||||
|
||||
unsigned size() const {
|
||||
return m_q.size();
|
||||
return (unsigned)m_q.size();
|
||||
}
|
||||
|
||||
void push(unsigned j) {
|
||||
|
|
@ -688,7 +675,6 @@ namespace lp {
|
|||
m_sum_of_fixed.pop_back();
|
||||
}
|
||||
|
||||
|
||||
void remove_last_row_in_matrix(static_matrix<mpq, mpq>& m) {
|
||||
auto& last_row = m.m_rows.back();
|
||||
for (unsigned k = static_cast<unsigned>(last_row.size()); k-- > 0;) {
|
||||
|
|
@ -771,8 +757,7 @@ namespace lp {
|
|||
|
||||
if (it != m_columns_to_terms.end()) {
|
||||
it->second.insert(t.j());
|
||||
}
|
||||
else {
|
||||
} else {
|
||||
std::unordered_set<unsigned> s;
|
||||
s.insert(t.j());
|
||||
m_columns_to_terms[p.var()] = s;
|
||||
|
|
@ -835,7 +820,8 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
void substitute_with_fresh_def(protected_queue& q, unsigned ei, unsigned j, const mpq& alpha) {
|
||||
const lar_term& sub_term = m_fresh_k2xt_terms.get_by_key(j);
|
||||
const lar_term& sub_term = m_fresh_k2xt_terms.get_by_key(j).first;
|
||||
TRACE("dioph_eq", print_lar_term_L(sub_term, tout) << std::endl;);
|
||||
SASSERT(sub_term.get_coeff(j).is_one());
|
||||
// we need to eliminate alpha*j in ei's row
|
||||
add_term_to_entry(-alpha, sub_term, ei);
|
||||
|
|
@ -885,7 +871,6 @@ namespace lp {
|
|||
return false;
|
||||
}
|
||||
return lia.column_is_int(term.j());
|
||||
|
||||
}
|
||||
|
||||
void clear_e_row(unsigned ei) {
|
||||
|
|
@ -896,7 +881,6 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
void recalculate_entry(unsigned ei) {
|
||||
TRACE("dioph_eq", print_entry(ei, tout) << std::endl;);
|
||||
mpq& c = m_sum_of_fixed[ei];
|
||||
|
|
@ -935,7 +919,6 @@ namespace lp {
|
|||
for (const auto& p : m_e_matrix.column(this->lar_solver_to_local(j))) {
|
||||
m_changed_rows.insert(p.var()); // TODO: is it necessary?
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -943,19 +926,37 @@ namespace lp {
|
|||
auto it = m_row2fresh_defs.find(ei);
|
||||
if (it == m_row2fresh_defs.end()) return;
|
||||
for (unsigned xt : it->second) {
|
||||
if (m_fresh_k2xt_terms.has_second_key(xt))
|
||||
m_fresh_k2xt_terms.erase_by_second_key(xt);
|
||||
}
|
||||
m_row2fresh_defs.erase(it);
|
||||
}
|
||||
|
||||
void remove_irrelevant_fresh_defs() {
|
||||
std_vector<unsigned> xt_to_remove;
|
||||
std_vector<unsigned> rows_to_remove_the_defs_from;
|
||||
for (const auto& p : m_fresh_k2xt_terms.m_bij.m_rev_map) {
|
||||
unsigned xt = p.first;
|
||||
if (xt >= m_e_matrix.column_count()) {
|
||||
xt_to_remove.push_back(xt);
|
||||
rows_to_remove_the_defs_from.push_back(m_fresh_k2xt_terms.get_by_val(xt).second);
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned xt : xt_to_remove) {
|
||||
m_fresh_k2xt_terms.erase_by_second_key(xt);
|
||||
}
|
||||
|
||||
for (unsigned ei : m_changed_rows) {
|
||||
remove_irrelevant_fresh_defs_for_row(ei);
|
||||
}
|
||||
|
||||
for (unsigned ei : rows_to_remove_the_defs_from) {
|
||||
remove_irrelevant_fresh_defs_for_row(ei);
|
||||
}
|
||||
}
|
||||
|
||||
void process_changed_columns() {
|
||||
|
||||
find_changed_terms_and_more_changed_rows();
|
||||
for (unsigned j : m_changed_terms) {
|
||||
if (j >= m_l_matrix.column_count()) continue;
|
||||
|
|
@ -981,12 +982,9 @@ namespace lp {
|
|||
m_changed_rows.insert(ei);
|
||||
}
|
||||
|
||||
remove_irrelevant_fresh_defs();
|
||||
|
||||
|
||||
for (unsigned ei : m_changed_rows) {
|
||||
if (ei >= m_e_matrix.row_count())
|
||||
continue;;
|
||||
continue;
|
||||
recalculate_entry(ei);
|
||||
if (m_e_matrix.m_columns.back().size() == 0) {
|
||||
m_e_matrix.m_columns.pop_back();
|
||||
|
|
@ -997,6 +995,8 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
remove_irrelevant_fresh_defs();
|
||||
|
||||
eliminate_substituted_in_changed_rows();
|
||||
m_changed_columns.reset();
|
||||
SASSERT(m_changed_columns.size() == 0);
|
||||
|
|
@ -1078,7 +1078,6 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
@ -1196,9 +1195,8 @@ namespace lp {
|
|||
t.c() = -c.rhs();
|
||||
}
|
||||
|
||||
|
||||
void subs_front_in_indexed_vector_by_fresh(unsigned k, protected_queue& q) {
|
||||
const lar_term& e = m_fresh_k2xt_terms.get_by_key(k);
|
||||
const lar_term& e = m_fresh_k2xt_terms.get_by_key(k).first;
|
||||
TRACE("dioph_eq", tout << "k:" << k << ", in ";
|
||||
print_term_o(create_term_from_ind_c(), tout) << std::endl;
|
||||
tout << "subs with e:";
|
||||
|
|
@ -1428,25 +1426,8 @@ namespace lp {
|
|||
// term_to_lar_solver(remove_fresh_vars(create_term_from_ind_c())))
|
||||
// enable_trace("dioph_eq");
|
||||
|
||||
TRACE("dioph_eq_deb_subs", tout << "after subs\n";
|
||||
print_term_o(create_term_from_ind_c(), tout) << std::endl;
|
||||
tout << "term_to_tighten:";
|
||||
print_lar_term_L(term_to_tighten, tout) << std::endl;
|
||||
tout << "m_tmp_l:"; print_lar_term_L(m_l_terms_workspace.to_term(), tout) << std::endl;
|
||||
tout << "open_ml:";
|
||||
print_lar_term_L(open_ml(m_l_terms_workspace.to_term()), tout) << std::endl;
|
||||
tout << "term_to_tighten + open_ml:";
|
||||
print_term_o(term_to_tighten + open_ml(m_l_terms_workspace.to_term()), tout)
|
||||
<< std::endl;
|
||||
term_o ls = fix_vars(term_to_tighten + open_ml(m_l_terms_workspace.to_term()));
|
||||
tout << "ls:"; print_term_o(ls,tout) << std::endl;
|
||||
term_o rs = term_to_lar_solver(remove_fresh_vars(create_term_from_ind_c()));
|
||||
tout << "rs:"; print_term_o(rs, tout ) << std::endl;
|
||||
term_o diff = ls - rs;
|
||||
if (!diff.is_empty()) {
|
||||
tout << "diff:"; print_term_o(diff, tout ) << std::endl;
|
||||
}
|
||||
);
|
||||
TRACE("dioph_eq_deb_subs", tout << "after subs\n"; print_term_o(create_term_from_ind_c(), tout) << std::endl; tout << "term_to_tighten:"; print_lar_term_L(term_to_tighten, tout) << std::endl; tout << "m_tmp_l:"; print_lar_term_L(m_l_terms_workspace.to_term(), tout) << std::endl; tout << "open_ml:"; print_lar_term_L(open_ml(m_l_terms_workspace.to_term()), tout) << std::endl; tout << "term_to_tighten + open_ml:"; print_term_o(term_to_tighten + open_ml(m_l_terms_workspace.to_term()), tout) << std::endl; term_o ls = fix_vars(term_to_tighten + open_ml(m_l_terms_workspace.to_term())); tout << "ls:"; print_term_o(ls, tout) << std::endl; term_o rs = term_to_lar_solver(remove_fresh_vars(create_term_from_ind_c())); tout << "rs:"; print_term_o(rs, tout) << std::endl; term_o diff = ls - rs; if (!diff.is_empty()) {
|
||||
tout << "diff:"; print_term_o(diff, tout ) << std::endl; });
|
||||
|
||||
SASSERT(
|
||||
fix_vars(term_to_tighten + open_ml(m_l_terms_workspace.to_term())) ==
|
||||
|
|
@ -1574,7 +1555,8 @@ namespace lp {
|
|||
return true;
|
||||
}
|
||||
|
||||
template <typename T> u_dependency* explain_fixed_in_meta_term (const T& t) {
|
||||
template <typename T>
|
||||
u_dependency* explain_fixed_in_meta_term(const T& t) {
|
||||
return explain_fixed(open_ml(t));
|
||||
}
|
||||
|
||||
|
|
@ -1591,7 +1573,8 @@ namespace lp {
|
|||
}
|
||||
|
||||
lia_move process_f() {
|
||||
while (rewrite_eqs()) {}
|
||||
while (rewrite_eqs()) {
|
||||
}
|
||||
if (m_conflict_index != UINT_MAX) {
|
||||
lra.stats().m_dio_rewrite_conflicts++;
|
||||
return lia_move::conflict;
|
||||
|
|
@ -1662,7 +1645,8 @@ namespace lp {
|
|||
*/
|
||||
if (m_k2s.has_key(j)) { // j is substituted but using an entry
|
||||
TRACE("dio_br",
|
||||
tout << "fixed j:" << j <<", was substited by "; print_entry(m_k2s[j], tout););
|
||||
tout << "fixed j:" << j << ", was substited by ";
|
||||
print_entry(m_k2s[j], tout););
|
||||
if (check_fixing(j) == lia_move::conflict) {
|
||||
for (auto ci : lra.flatten(explain_fixed_in_meta_term(m_l_matrix.m_rows[m_k2s[j]]))) {
|
||||
m_explanation_of_branches.push_back(ci);
|
||||
|
|
@ -1731,7 +1715,6 @@ namespace lp {
|
|||
if (this->lra.constraints().valid_index(ci))
|
||||
m_infeas_explanation.push_back(ci);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
lia_move branching_on_undef() {
|
||||
|
|
@ -1826,7 +1809,6 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
branch create_branch() {
|
||||
unsigned bj = UINT_MAX;
|
||||
double score = std::numeric_limits<double>::infinity();
|
||||
|
|
@ -1882,35 +1864,18 @@ namespace lp {
|
|||
} else {
|
||||
it->second.insert(t->j());
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
}
|
||||
for (const auto& p : c2t) {
|
||||
unsigned j = p.first;
|
||||
const auto it = m_columns_to_terms.find(j);
|
||||
if (it == m_columns_to_terms.end()) {
|
||||
TRACE("dioph_eq", tout << "column j" << j << " is not registered" << std::endl;
|
||||
tout << "the column belongs to the the following terms:";
|
||||
for (unsigned tj : p.second) {
|
||||
tout << " " << tj;
|
||||
}
|
||||
tout << std::endl;
|
||||
);
|
||||
TRACE("dioph_eq", tout << "column j" << j << " is not registered" << std::endl; tout << "the column belongs to the the following terms:"; for (unsigned tj : p.second) { tout << " " << tj; } tout << std::endl;);
|
||||
|
||||
return false;
|
||||
}
|
||||
if (it->second != p.second) {
|
||||
TRACE("dioph_eq_deb", tout << "m_columns_to_terms[" << j << "] has to be ";
|
||||
tout << "{";
|
||||
for(unsigned lll : p.second) {
|
||||
tout << lll << ", ";
|
||||
}
|
||||
tout << "}, \nbut it is {";
|
||||
for (unsigned lll : it->second) {
|
||||
tout << lll << ", ";
|
||||
};
|
||||
tout << "}" << std::endl;
|
||||
TRACE("dioph_eq_deb", tout << "m_columns_to_terms[" << j << "] has to be "; tout << "{"; for (unsigned lll : p.second) { tout << lll << ", "; } tout << "}, \nbut it is {"; for (unsigned lll : it->second) { tout << lll << ", "; }; tout << "}" << std::endl;
|
||||
|
||||
);
|
||||
return false;
|
||||
|
|
@ -2162,13 +2127,13 @@ namespace lp {
|
|||
tout << "ls:";
|
||||
print_term_o(remove_fresh_vars(get_term_from_entry(ei)), tout)
|
||||
<< std::endl;
|
||||
tout << "e.m_l:"; print_lar_term_L(l_term_from_row(ei), tout) << std::endl;
|
||||
tout << "e.m_l:";
|
||||
print_lar_term_L(l_term_from_row(ei), tout) << std::endl;
|
||||
tout << "open_ml(e.m_l):";
|
||||
print_lar_term_L(open_ml(l_term_from_row(ei)), tout) << std::endl;
|
||||
tout << "rs:";
|
||||
print_term_o(fix_vars(open_ml(m_l_matrix.m_rows[ei])), tout) << std::endl;
|
||||
}
|
||||
);
|
||||
});
|
||||
|
||||
return ret;
|
||||
}
|
||||
|
|
@ -2183,7 +2148,7 @@ namespace lp {
|
|||
}
|
||||
while (!q.empty()) {
|
||||
unsigned xt = q.pop_front(); // xt is a fresh var
|
||||
const lar_term& fresh_t = m_fresh_k2xt_terms.get_by_val(xt);
|
||||
const lar_term& fresh_t = m_fresh_k2xt_terms.get_by_val(xt).first;
|
||||
TRACE("dioph_eq", print_lar_term_L(fresh_t, tout););
|
||||
SASSERT(fresh_t.get_coeff(xt).is_minus_one());
|
||||
if (!t.contains(xt))
|
||||
|
|
@ -2196,7 +2161,6 @@ namespace lp {
|
|||
q.push(p.j());
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
return t;
|
||||
}
|
||||
|
|
@ -2206,7 +2170,8 @@ namespace lp {
|
|||
return print_lar_term_L(opened_ml, out);
|
||||
}
|
||||
|
||||
template <typename T> term_o open_ml(const T& ml) const {
|
||||
template <typename T>
|
||||
term_o open_ml(const T& ml) const {
|
||||
term_o r;
|
||||
for (const auto& p : ml) {
|
||||
r += p.coeff() * (lra.get_term(p.var()) - lar_term(p.var()));
|
||||
|
|
@ -2276,7 +2241,7 @@ namespace lp {
|
|||
fresh_t.add_monomial(q, i.var());
|
||||
}
|
||||
|
||||
m_fresh_k2xt_terms.add(k, xt, fresh_t);
|
||||
m_fresh_k2xt_terms.add(k, xt, std::make_pair(fresh_t, h));
|
||||
SASSERT(var_is_fresh(xt));
|
||||
register_var_in_fresh_defs(h, xt);
|
||||
eliminate_var_in_f_with_term(fresh_t, k, 1);
|
||||
|
|
@ -2297,8 +2262,9 @@ namespace lp {
|
|||
print_deps(out, explain_fixed_in_meta_term(l_term));
|
||||
out << "}\n";
|
||||
}
|
||||
if (belongs_to_f(i)) { out << "in F\n"; }
|
||||
else {
|
||||
if (belongs_to_f(i)) {
|
||||
out << "in F\n";
|
||||
} else {
|
||||
unsigned j = m_k2s.get_key(i);
|
||||
if (local_to_lar_solver(j) == UINT_MAX) {
|
||||
out << "FRESH\n";
|
||||
|
|
@ -2408,7 +2374,6 @@ namespace lp {
|
|||
SASSERT(!ret || m_var_register.local_to_external(j) == UINT_MAX);
|
||||
return ret;
|
||||
}
|
||||
|
||||
};
|
||||
// Constructor definition
|
||||
dioph_eq::dioph_eq(int_solver& lia) {
|
||||
|
|
@ -2427,4 +2392,3 @@ namespace lp {
|
|||
}
|
||||
|
||||
} // namespace lp
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue