mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
simplify dio handler by using bijection m_k2s
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
Lev Nachmanson
parent
33f5e303f8
commit
78d91f3794
|
|
@ -48,6 +48,75 @@ namespace lp {
|
|||
return t.find(j) != t.end();
|
||||
}
|
||||
|
||||
struct bijection {
|
||||
std::unordered_map<unsigned, unsigned> m_map;
|
||||
std::unordered_map<unsigned, unsigned> m_rev_map;
|
||||
|
||||
void add(unsigned a, unsigned b) {
|
||||
SASSERT(!contains(m_map, a) && !contains(m_rev_map, b));
|
||||
m_map[a] = b;
|
||||
m_rev_map[b] = a;
|
||||
}
|
||||
|
||||
unsigned get_key(unsigned b) const {
|
||||
SASSERT(has_val(b));
|
||||
return m_rev_map.find(b)->second;
|
||||
}
|
||||
|
||||
unsigned size() const {return m_map.size();}
|
||||
|
||||
void erase_val(unsigned b) {
|
||||
SASSERT(contains(m_rev_map, b) && contains(m_map, m_rev_map[b]));
|
||||
unsigned key = m_rev_map[b];
|
||||
m_rev_map.erase(b);
|
||||
m_map.erase(key);
|
||||
}
|
||||
bool has_val(unsigned b) const {
|
||||
return contains(m_rev_map, b);
|
||||
}
|
||||
|
||||
bool has_key(unsigned a) const {
|
||||
return contains(m_map, a);
|
||||
}
|
||||
|
||||
void transpose_val(unsigned b0, unsigned b1) {
|
||||
bool has_b0 = has_val(b0);
|
||||
bool has_b1 = has_val(b1);
|
||||
|
||||
// Both b0 and b1 exist
|
||||
if (has_b0 && has_b1) {
|
||||
unsigned a0 = m_rev_map.at(b0);
|
||||
unsigned a1 = m_rev_map.at(b1);
|
||||
|
||||
erase_val(b0);
|
||||
erase_val(b1);
|
||||
|
||||
add(a1, b0);
|
||||
add(a0, b1);
|
||||
}
|
||||
// Only b0 exists
|
||||
else if (has_b0) {
|
||||
unsigned a0 = m_rev_map.at(b0);
|
||||
|
||||
erase_val(b0);
|
||||
add(a0, b1);
|
||||
}
|
||||
// Only b1 exists
|
||||
else if (has_b1) {
|
||||
unsigned a1 = m_rev_map.at(b1);
|
||||
|
||||
erase_val(b1);
|
||||
add(a1, b0);
|
||||
}
|
||||
// Neither b0 nor b1 exists; do nothing
|
||||
}
|
||||
unsigned operator[](unsigned i) const {
|
||||
auto it = m_map.find(i);
|
||||
SASSERT(it != m_map.end());
|
||||
return it->second;
|
||||
}
|
||||
};
|
||||
|
||||
class dioph_eq::imp {
|
||||
// This class represents a term with an added constant number c, in form sum
|
||||
// {x_i*a_i} + c.
|
||||
|
|
@ -134,8 +203,8 @@ namespace lp {
|
|||
|
||||
std::ostream& print_S(std::ostream& out) {
|
||||
out << "S:\n";
|
||||
for (unsigned i : m_s) {
|
||||
print_entry(i, out);
|
||||
for (const auto & p: m_k2s.m_map) {
|
||||
print_entry(p.second, out);
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
|
@ -196,28 +265,17 @@ namespace lp {
|
|||
return out;
|
||||
}
|
||||
|
||||
/*
|
||||
An annotated state is a triple ⟨E′, λ, σ⟩, where E′ is a set of pairs ⟨e,
|
||||
ℓ⟩ in which e is an equation and ℓ is a linear combination of variables
|
||||
from L
|
||||
*/
|
||||
//
|
||||
enum class entry_status { F,
|
||||
S,
|
||||
FRESH
|
||||
};
|
||||
// consider to move m_c to an m_e_matrix column
|
||||
struct entry {
|
||||
//lar_term m_l; the term is taken from matrix m_l_matrix of the index entry
|
||||
mpq m_c; // the constant of the term, the term is taken from the row of
|
||||
// m_e_matrix with the same index as the entry
|
||||
entry_status m_entry_status;
|
||||
entry(const mpq & c) : m_c(c) {}
|
||||
};
|
||||
|
||||
var_register m_var_register;
|
||||
std_vector<entry> m_entries;
|
||||
// the terms are stored in m_A and m_c
|
||||
static_matrix<mpq, mpq> m_e_matrix; // the rows of the matrix are the terms,
|
||||
static_matrix<mpq, mpq> m_l_matrix; // the rows of the matrix are the l_terms providing the certificate to the entries modulo the constant part
|
||||
static_matrix<mpq, mpq> m_l_matrix; // the rows of the matrix are the l_terms providing the certificate to the entries modulo the constant part: look an entry_invariant that assures that the each two rows are in sync.
|
||||
int_solver& lia;
|
||||
lar_solver& lra;
|
||||
explanation m_infeas_explanation;
|
||||
|
|
@ -225,17 +283,12 @@ namespace lp {
|
|||
bool m_report_branch = false;
|
||||
|
||||
// set F
|
||||
std::list<unsigned> m_f; // F = {λ(t):t in m_f}
|
||||
// set S
|
||||
std::list<unsigned> m_s; // S = {λ(t): t in m_s}
|
||||
// iterate over all rows from 0 to m_e_matrix.row_count() - 1 and return those i such !m_k2s.has_val(i)
|
||||
// set S - iterate over bijection m_k2s
|
||||
mpq m_c; // the constant of the equation
|
||||
lar_term m_tmp_l;
|
||||
// the dependency of the equation
|
||||
// map to open the term e.m_l
|
||||
// suppose e.m_l = sum {coeff*k}, then subst(e.m_e) = fix_var(sum
|
||||
// {coeff*lar.get_term(k)})
|
||||
|
||||
std_vector<unsigned> m_k2s;
|
||||
bijection m_k2s;
|
||||
struct fresh_definition {
|
||||
unsigned m_ei;
|
||||
unsigned m_origin;
|
||||
|
|
@ -337,10 +390,8 @@ namespace lp {
|
|||
void remove_last_entry() {
|
||||
unsigned ei = m_entries.size() - 1;
|
||||
|
||||
if (m_entries.back().m_entry_status == entry_status::F) {
|
||||
remove_entry_index(this->m_f, ei);
|
||||
} else {
|
||||
remove_entry_index(this->m_s, ei);
|
||||
if (m_k2s.has_val(ei)) {
|
||||
m_k2s.erase_val(ei);
|
||||
}
|
||||
m_entries.pop_back();
|
||||
}
|
||||
|
|
@ -424,15 +475,12 @@ namespace lp {
|
|||
});
|
||||
if (it != m_fresh_definitions.end())
|
||||
*it = fresh_definition(-1, -1);
|
||||
for (unsigned k = 0; k < m_k2s.size() ; k++) {
|
||||
if (m_k2s[k] == i) {
|
||||
m_k2s[k] = -1;
|
||||
break;
|
||||
}
|
||||
|
||||
|
||||
if (m_k2s.has_val(i)) {
|
||||
m_k2s.erase_val(i);
|
||||
}
|
||||
|
||||
remove_entry_index(m_f, i);
|
||||
remove_entry_index(m_s, i);
|
||||
m_entries.pop_back();
|
||||
}
|
||||
|
||||
|
|
@ -531,9 +579,8 @@ namespace lp {
|
|||
// the term has form sum(a_i*x_i) - t.j() = 0,
|
||||
void fill_entry(const lar_term& t) {
|
||||
TRACE("dioph_eq", print_lar_term_L(t, tout) << std::endl;);
|
||||
entry te = { mpq(0), entry_status::F};
|
||||
entry te = { mpq(0)};
|
||||
unsigned entry_index = (unsigned) m_entries.size();
|
||||
m_f.push_back(entry_index);
|
||||
m_entries.push_back(te);
|
||||
entry& e = m_entries.back();
|
||||
SASSERT(m_l_matrix.row_count() == m_e_matrix.row_count());
|
||||
|
|
@ -557,8 +604,57 @@ namespace lp {
|
|||
m_e_matrix.add_new_element(entry_index, lj, p.coeff());
|
||||
}
|
||||
}
|
||||
TRACE("dioph_eq", print_entry(entry_index, tout) << std::endl;);
|
||||
subs_entry(entry_index);
|
||||
SASSERT(entry_invariant(entry_index));
|
||||
}
|
||||
void subs_entry(unsigned ei) {
|
||||
std::queue<unsigned> q;
|
||||
for (const auto& p: m_e_matrix.m_rows[ei]) {
|
||||
if (can_substitute(p.var()))
|
||||
q.push(p.var());
|
||||
}
|
||||
if (q.size() == 0) return;
|
||||
substitute_on_q(q, ei);
|
||||
SASSERT(entry_invariant(ei));
|
||||
}
|
||||
|
||||
void substitute_on_q(std::queue<unsigned> & q, unsigned ei) {
|
||||
// Track queued items
|
||||
std::unordered_set<unsigned> in_queue;
|
||||
// Initialize with the current queue contents
|
||||
{
|
||||
std::queue<unsigned> tmp = q;
|
||||
while (!tmp.empty()) {
|
||||
in_queue.insert(tmp.front());
|
||||
tmp.pop();
|
||||
}
|
||||
}
|
||||
while (!q.empty()) {
|
||||
unsigned j = pop_front(q);
|
||||
in_queue.erase(j);
|
||||
mpq alpha = get_coeff_in_e_row(ei, j);
|
||||
if (alpha.is_zero()) continue;
|
||||
unsigned ei_to_sub = m_k2s[j];
|
||||
int sign_j = get_sign_in_e_row(ei_to_sub, j);
|
||||
// we need to eliminate alpha*j in ei's row
|
||||
add_two_entries(-mpq(sign_j)*alpha, ei_to_sub, ei);
|
||||
for (const auto& p: m_e_matrix.m_rows[ei]) {
|
||||
unsigned jj = p.var();
|
||||
if (can_substitute(jj) && !contains(in_queue, jj)) {
|
||||
q.push(jj);
|
||||
in_queue.insert(jj);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// adds entry i0 multiplied by coeff to entry i1
|
||||
void add_two_entries(const mpq& coeff, unsigned i0, unsigned i1 ) {
|
||||
m_e_matrix.add_rows(coeff, i0, i1);
|
||||
m_l_matrix.add_rows(coeff, i0, i1);
|
||||
m_entries[i1].m_c += coeff* m_entries[i0].m_c;
|
||||
}
|
||||
|
||||
bool all_vars_are_int(const lar_term& term) const {
|
||||
for (const auto& p : term) {
|
||||
|
|
@ -580,6 +676,7 @@ namespace lp {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
void recalculate_entry(unsigned ei) {
|
||||
TRACE("dioph_eq", print_entry(ei, tout) << std::endl;);
|
||||
mpq &c = m_entries[ei].m_c;
|
||||
|
|
@ -600,7 +697,7 @@ namespace lp {
|
|||
m_l_matrix.multiply_row(ei, denom);
|
||||
m_e_matrix.multiply_row(ei, denom);
|
||||
}
|
||||
move_entry_from_s_to_f(ei);
|
||||
|
||||
SASSERT(entry_invariant(ei));
|
||||
}
|
||||
|
||||
|
|
@ -677,11 +774,15 @@ namespace lp {
|
|||
remove_last_row_in_matrix(m_l_matrix);
|
||||
remove_last_row_in_matrix(m_e_matrix);
|
||||
}
|
||||
for(unsigned ei : entries_to_recalculate) {
|
||||
if (ei < m_e_matrix.row_count())
|
||||
move_entry_from_s_to_f(ei);
|
||||
}
|
||||
|
||||
for(unsigned k : entries_to_recalculate) {
|
||||
if (k >= m_entries.size())
|
||||
for(unsigned ei : entries_to_recalculate) {
|
||||
if (ei >= m_e_matrix.row_count())
|
||||
continue;;
|
||||
recalculate_entry(k);
|
||||
recalculate_entry(ei);
|
||||
if (m_e_matrix.m_columns.back().size() == 0) {
|
||||
m_e_matrix.m_columns.pop_back();
|
||||
m_var_register.shrink(m_e_matrix.column_count());
|
||||
|
|
@ -690,81 +791,60 @@ namespace lp {
|
|||
m_l_matrix.m_columns.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
eliminate_substituted();
|
||||
SASSERT(entries_are_ok());
|
||||
m_changed_columns.clear();
|
||||
}
|
||||
|
||||
int get_sign_in_e_row(unsigned ei, unsigned j) const {
|
||||
const auto& row = m_e_matrix.m_rows[ei];
|
||||
auto it = std::find_if (row.begin(), row.end(), [j](const auto& p) {return p.var() == j;} );
|
||||
SASSERT(it != row.end() && abs(it->coeff()) == mpq(1));
|
||||
return it->coeff().is_pos()? 1:-1;
|
||||
}
|
||||
|
||||
mpq get_coeff_in_e_row (unsigned ei, unsigned j) {
|
||||
const auto& row = m_e_matrix.m_rows[ei];
|
||||
auto it = std::find_if (row.begin(), row.end(), [j](const auto& p) {return p.var() == j;} );
|
||||
if (it == row.end()) return mpq(0);
|
||||
return it->coeff();
|
||||
}
|
||||
|
||||
void eliminate_substituted() {
|
||||
for (const auto &p: m_k2s.m_map) {
|
||||
unsigned j = p.first;
|
||||
unsigned ei = p.second;
|
||||
int j_sign = get_sign_in_e_row(ei, j);
|
||||
eliminate_var_in_f(ei, j, j_sign);
|
||||
}
|
||||
}
|
||||
|
||||
void transpose_entries(unsigned i, unsigned k) {
|
||||
SASSERT(i != k);
|
||||
m_l_matrix.transpose_rows(i, k);
|
||||
m_e_matrix.transpose_rows(i, k);
|
||||
remove_entry_from_lists(i);
|
||||
remove_entry_from_lists(k);
|
||||
std::swap(m_entries[i], m_entries[k]);
|
||||
add_entry_to_lists(i);
|
||||
add_entry_to_lists(k);
|
||||
m_k2s.transpose_val(i, k);
|
||||
|
||||
NOT_IMPLEMENTED_YET();
|
||||
/*
|
||||
// transpose fresh definitions
|
||||
for (auto & fd: m_fresh_definitions) {
|
||||
if (fd.m_ei == i)
|
||||
fd.m_ei = k;
|
||||
else if (fd.m_ei == k)
|
||||
fd.m_ei = i;
|
||||
}
|
||||
//transpose m_k2s
|
||||
for (unsigned& t : m_k2s) {
|
||||
if (t == i)
|
||||
t = k;
|
||||
else if (t == k)
|
||||
t = i;
|
||||
}
|
||||
}
|
||||
|
||||
void remove_entry_from_lists(unsigned ei) {
|
||||
auto status = m_entries[ei].m_entry_status;
|
||||
if (status == entry_status::F) {
|
||||
m_f.remove(ei);
|
||||
} else {
|
||||
m_s.remove(ei);
|
||||
}
|
||||
}
|
||||
if (fd.m_origin == i)
|
||||
fd.m_origin = k;
|
||||
|
||||
void add_entry_to_lists(unsigned ei) {
|
||||
auto status = m_entries[ei].m_entry_status;
|
||||
if (status == entry_status::F) {
|
||||
m_f.push_back(ei);
|
||||
} else {
|
||||
m_s.push_back(ei);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void move_recalculated_to_F(const std::unordered_set<unsigned> &entries_to_recalculate) {
|
||||
for (auto it = this->m_s.begin(); it != m_s.end(); ) {
|
||||
if (contains(entries_to_recalculate, *it)) {
|
||||
auto nit = it;
|
||||
nit++;
|
||||
m_s.erase(it);
|
||||
it = nit;
|
||||
}
|
||||
else it++;
|
||||
}
|
||||
|
||||
for (unsigned k = 0; k < m_k2s.size(); k++) {
|
||||
if (m_k2s[k] != UINT_MAX && contains(entries_to_recalculate, m_k2s[k])) {
|
||||
m_k2s[k] = -1;
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned ei: entries_to_recalculate) {
|
||||
SASSERT(std::find(m_f.begin(), m_f.end(), ei) == m_f.end());
|
||||
SASSERT(!is_substituted(ei));
|
||||
m_f.push_back(ei);
|
||||
m_entries[ei].m_entry_status = entry_status::F;
|
||||
}
|
||||
}*/
|
||||
}
|
||||
|
||||
// returns true if a variable j is substituted
|
||||
bool is_substituted(unsigned j) const {
|
||||
return std::find(m_k2s.begin(), m_k2s.end(), j) != m_k2s.end();
|
||||
return m_k2s.has_key(j);
|
||||
}
|
||||
|
||||
bool entries_are_ok() {
|
||||
|
|
@ -773,6 +853,27 @@ namespace lp {
|
|||
TRACE("dioph_deb_eq", tout << "bad entry:"; print_entry(ei, tout););
|
||||
return false;
|
||||
}
|
||||
if (belongs_to_f(ei)) {
|
||||
// see that all vars are substituted
|
||||
const auto & row = m_e_matrix.m_rows[ei];
|
||||
for (const auto& p : row) {
|
||||
if (m_k2s.has_key(p.var())) {
|
||||
std::cout << "entry:" << ei << " belongs to f but depends on column " << p.var() << std::endl;
|
||||
std::cout << "m_var_register.local_to_external(p.var()):" << m_var_register.local_to_external(p.var()) << std::endl;
|
||||
print_entry(ei, std::cout);
|
||||
std::cout << "column " << p.var() << " of m_e_matrix:";
|
||||
for (const auto & c : m_e_matrix.m_columns[p.var()]) {
|
||||
std::cout << "row:" << c.var() << ", ";
|
||||
}
|
||||
|
||||
std::cout << std::endl;
|
||||
std::cout << "the other entry:";
|
||||
print_entry(m_k2s[p.var()],std::cout) << std::endl;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
@ -785,6 +886,7 @@ namespace lp {
|
|||
m_number_of_iterations = 0;
|
||||
m_branch_stack.clear();
|
||||
m_lra_level = 0;
|
||||
|
||||
process_changed_columns();
|
||||
for (const lar_term* t: m_added_terms) {
|
||||
m_active_terms.insert(t);
|
||||
|
|
@ -882,9 +984,10 @@ namespace lp {
|
|||
return false;
|
||||
}
|
||||
|
||||
// returns true if no conflict is found and false otherwise
|
||||
// iterate over F: return true if no conflict is found and false otherwise
|
||||
bool normalize_by_gcd() {
|
||||
for (unsigned l : m_f) {
|
||||
for (unsigned l = 0; l < m_e_matrix.row_count(); l++) {
|
||||
if (!belongs_to_f(l)) continue;
|
||||
if (!normalize_e_by_gcd(l)) {
|
||||
SASSERT(entry_invariant(l));
|
||||
m_conflict_index = l;
|
||||
|
|
@ -911,13 +1014,12 @@ namespace lp {
|
|||
if (m_indexed_work_vector[k].is_zero())
|
||||
return;
|
||||
const entry& e = entry_for_subs(k);
|
||||
SASSERT(e.m_entry_status != entry_status::F);
|
||||
SASSERT(is_substituted(k));
|
||||
TRACE("dioph_eq", tout << "k:" << k << ", in ";
|
||||
print_term_o(create_term_from_ind_c(), tout) << std::endl;
|
||||
tout << "subs with e:";
|
||||
print_entry(m_k2s[k], tout) << std::endl;);
|
||||
mpq coeff =
|
||||
m_indexed_work_vector[k]; // need to copy since it will be zeroed
|
||||
mpq coeff = m_indexed_work_vector[k]; // need to copy since it will be zeroed
|
||||
m_indexed_work_vector.erase(k); // m_indexed_work_vector[k] = 0;
|
||||
|
||||
const auto& e_row = m_e_matrix.m_rows[m_k2s[k]];
|
||||
|
|
@ -990,9 +1092,6 @@ namespace lp {
|
|||
return m_entries[m_k2s[k]];
|
||||
}
|
||||
|
||||
entry& entry_for_subs(unsigned k) {
|
||||
return m_entries[m_k2s[k]];
|
||||
}
|
||||
|
||||
const unsigned sub_index(unsigned k) const {
|
||||
return m_k2s[k];
|
||||
|
|
@ -1059,6 +1158,7 @@ namespace lp {
|
|||
unsigned lar_solver_to_local(unsigned j) const {
|
||||
return m_var_register.external_to_local(j);
|
||||
}
|
||||
|
||||
// j is the index of the column representing a term
|
||||
// return true if a conflict was found
|
||||
bool tighten_bounds_for_term_column(unsigned j) {
|
||||
|
|
@ -1242,7 +1342,8 @@ namespace lp {
|
|||
}
|
||||
|
||||
lia_move process_f() {
|
||||
while (m_f.size()) {
|
||||
unsigned empty_rows = 0;
|
||||
while (m_k2s.size() + empty_rows < m_e_matrix.row_count()) {
|
||||
if (!normalize_by_gcd()) {
|
||||
if (m_report_branch) {
|
||||
lra.stats().m_dio_cut_from_proofs++;
|
||||
|
|
@ -1253,7 +1354,7 @@ namespace lp {
|
|||
}
|
||||
return lia_move::conflict;
|
||||
}
|
||||
rewrite_eqs();
|
||||
empty_rows = rewrite_eqs();
|
||||
if (m_conflict_index != UINT_MAX) {
|
||||
lra.stats().m_dio_rewrite_conflicts++;
|
||||
return lia_move::conflict;
|
||||
|
|
@ -1663,9 +1764,10 @@ namespace lp {
|
|||
return (it->coeff() == mpq(1) && j_sign == 1) ||
|
||||
(it->coeff() == mpq(-1) && j_sign == -1);
|
||||
}
|
||||
// j is the variable to eliminate, it appears in row ei of m_e_matrix with
|
||||
// j is the variable to eliminate, or substitude, it appears in row ei of m_e_matrix with
|
||||
// a coefficient equal to j_sign which is +-1
|
||||
void eliminate_var_in_f(unsigned ei, unsigned j, int j_sign) {
|
||||
SASSERT(belongs_to_s(ei));
|
||||
const auto & e = m_entries[ei];
|
||||
SASSERT(j_sign_is_correct(ei, j, j_sign));
|
||||
TRACE("dioph_eq", tout << "eliminate var:" << j << " by using:";
|
||||
|
|
@ -1691,7 +1793,7 @@ namespace lp {
|
|||
unsigned cell_to_process = column.size() - 1;
|
||||
while (cell_to_process > 0) {
|
||||
auto& c = column[cell_to_process];
|
||||
if (m_entries[c.var()].m_entry_status != entry_status::F) {
|
||||
if (belongs_to_s(c.var())) {
|
||||
cell_to_process--;
|
||||
continue;
|
||||
}
|
||||
|
|
@ -1717,8 +1819,21 @@ namespace lp {
|
|||
SASSERT(entry_invariant(i));
|
||||
cell_to_process--;
|
||||
}
|
||||
SASSERT(is_eliminated_from_f(j));
|
||||
}
|
||||
bool is_eliminated_from_f(unsigned j) const {
|
||||
for (unsigned ei = 0; ei < m_e_matrix.row_count(); ei++) {
|
||||
if (!belongs_to_f(ei)) continue;
|
||||
const auto &row = m_e_matrix.m_rows[ei];
|
||||
for (const auto& p : row) {
|
||||
if (p.var() == j) {
|
||||
std::cout << "not eliminated from row " << ei << std::endl;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
term_o term_to_lar_solver(const term_o& eterm) const {
|
||||
term_o ret;
|
||||
for (const auto& p : eterm) {
|
||||
|
|
@ -1728,12 +1843,17 @@ namespace lp {
|
|||
return ret;
|
||||
}
|
||||
|
||||
bool entry_invariant(unsigned ei) const {
|
||||
const auto & e= m_entries[ei];
|
||||
if ((e.m_entry_status == entry_status::F && is_substituted(ei)) ||
|
||||
(e.m_entry_status != entry_status::F && !is_substituted(ei)))
|
||||
return false;
|
||||
bool belongs_to_s(unsigned ei) const {
|
||||
return m_k2s.has_val(ei);
|
||||
}
|
||||
|
||||
bool entry_invariant(unsigned ei) const {
|
||||
if (belongs_to_s(ei)) {
|
||||
auto it = m_k2s.m_rev_map.find(ei);
|
||||
SASSERT(it != m_k2s.m_rev_map.end());
|
||||
unsigned j = it->second;
|
||||
get_sign_in_e_row(ei, j);
|
||||
}
|
||||
|
||||
for (const auto &p: m_e_matrix.m_rows[ei]) {
|
||||
if (!p.coeff().is_int()) {
|
||||
|
|
@ -1856,7 +1976,7 @@ namespace lp {
|
|||
e.m_c = r;
|
||||
m_e_matrix.add_new_element(h, xt, ahk);
|
||||
|
||||
m_entries.push_back({q, entry_status::FRESH});
|
||||
m_entries.push_back({q});
|
||||
m_e_matrix.add_new_element(fresh_row, xt, -mpq(1));
|
||||
m_e_matrix.add_new_element(fresh_row, k, mpq(1));
|
||||
for (unsigned i : m_indexed_work_vector.m_index) {
|
||||
|
|
@ -1872,8 +1992,7 @@ namespace lp {
|
|||
|
||||
m_l_matrix.add_row();
|
||||
|
||||
m_k2s.resize(k + 1, -1);
|
||||
m_k2s[k] = fresh_row;
|
||||
m_k2s.add(k, fresh_row);
|
||||
fresh_definition fd(-1, -1);
|
||||
|
||||
m_fresh_definitions.resize(xt + 1, fd);
|
||||
|
|
@ -1888,7 +2007,7 @@ namespace lp {
|
|||
}
|
||||
|
||||
std::ostream& print_entry(unsigned i, std::ostream& out,
|
||||
bool print_dep = true) {
|
||||
bool print_dep = false) {
|
||||
out << "m_entries[" << i << "]:";
|
||||
return print_entry(i, m_entries[i], out, print_dep);
|
||||
}
|
||||
|
|
@ -1906,64 +2025,54 @@ namespace lp {
|
|||
print_dep(out, explain_fixed_in_meta_term(l_term_from_row(ei)));
|
||||
out << "}\n";
|
||||
}
|
||||
switch (e.m_entry_status) {
|
||||
case entry_status::F:
|
||||
out << "in F\n";
|
||||
break;
|
||||
case entry_status::S:
|
||||
if (belongs_to_f(ei)) { out << "in F\n"; }
|
||||
else {
|
||||
unsigned j = m_k2s.get_key(ei);
|
||||
if (local_to_lar_solver(j) == UINT_MAX) {
|
||||
out << "FRESH\n";
|
||||
} else {
|
||||
out << "in S\n";
|
||||
break;
|
||||
default:
|
||||
out << "NOSF\n";
|
||||
}
|
||||
}
|
||||
out << "}\n";
|
||||
return out;
|
||||
}
|
||||
|
||||
void move_entry_from_s_to_f(unsigned ei) {
|
||||
if (m_entries[ei].m_entry_status == entry_status::F) return;
|
||||
m_entries[ei].m_entry_status = entry_status::F;
|
||||
for (unsigned l = 0; l < m_k2s.size(); l++) {
|
||||
if (m_k2s[l] == ei) {
|
||||
m_k2s[l] = -1;
|
||||
}
|
||||
}
|
||||
m_s.remove(ei);
|
||||
m_f.push_back(ei);
|
||||
bool belongs_to_f(unsigned ei) const {
|
||||
return !m_k2s.has_val(ei);
|
||||
}
|
||||
|
||||
// k is the index of the variable that is being substituted
|
||||
void move_entry_from_f_to_s(unsigned k, unsigned h) {
|
||||
SASSERT(m_entries[h].m_entry_status == entry_status::F);
|
||||
m_entries[h].m_entry_status = entry_status::S;
|
||||
if (k >= m_k2s.size()) { // k is a fresh variable
|
||||
m_k2s.resize(k + 1, -1);
|
||||
void move_entry_from_s_to_f(unsigned ei) {
|
||||
m_k2s.erase_val(ei);
|
||||
}
|
||||
m_s.push_back(h);
|
||||
TRACE("dioph_eq", tout << "removed " << h << "th entry from F" << std::endl;);
|
||||
m_k2s[k] = h;
|
||||
m_f.remove(h);
|
||||
|
||||
// k is the variables that is being substituted
|
||||
// h is the index of the entry
|
||||
void move_entry_from_f_to_s(unsigned k, unsigned h) {
|
||||
m_k2s.add(k, h);
|
||||
}
|
||||
|
||||
// this is the step 6 or 7 of the algorithm
|
||||
void rewrite_eqs() {
|
||||
// returns the number of empty rows
|
||||
unsigned rewrite_eqs() {
|
||||
unsigned h = -1;
|
||||
auto it = m_f.begin();
|
||||
while (it != m_f.end()) {
|
||||
if (m_e_matrix.m_rows[*it].size() == 0) {
|
||||
if (m_entries[*it].m_c.is_zero()) {
|
||||
it = m_f.erase(it);
|
||||
unsigned empty_rows = 0;
|
||||
for (unsigned ei=0; ei < m_e_matrix.row_count(); ei++) {
|
||||
if (belongs_to_s(ei)) continue;
|
||||
if (m_e_matrix.m_rows[ei].size() == 0) {
|
||||
if (m_entries[ei].m_c.is_zero()) {
|
||||
empty_rows++;
|
||||
continue;
|
||||
} else {
|
||||
m_conflict_index = *it;
|
||||
return;
|
||||
m_conflict_index = ei;
|
||||
return empty_rows;
|
||||
}
|
||||
}
|
||||
h = *it;
|
||||
h = ei;
|
||||
break;
|
||||
}
|
||||
if (h == UINT_MAX)
|
||||
return;
|
||||
return empty_rows;
|
||||
auto [ahk, k, k_sign] = find_minimal_abs_coeff(h);
|
||||
TRACE("dioph_eq", tout << "eh:"; print_entry(h, tout);
|
||||
tout << "ahk:" << ahk << ", k:" << k << ", k_sign:" << k_sign
|
||||
|
|
@ -1976,6 +2085,7 @@ namespace lp {
|
|||
} else {
|
||||
fresh_var_step(h, k, ahk * mpq(k_sign));
|
||||
}
|
||||
return empty_rows;
|
||||
}
|
||||
|
||||
public:
|
||||
|
|
@ -2000,8 +2110,9 @@ namespace lp {
|
|||
return m_var_register.local_to_external(j) == UINT_MAX;
|
||||
}
|
||||
bool can_substitute(unsigned k) {
|
||||
return k < m_k2s.size() && m_k2s[k] != UINT_MAX;
|
||||
return m_k2s.has_key(k);
|
||||
}
|
||||
|
||||
};
|
||||
// Constructor definition
|
||||
dioph_eq::dioph_eq(int_solver& lia) {
|
||||
|
|
@ -2020,3 +2131,4 @@ namespace lp {
|
|||
}
|
||||
|
||||
} // namespace lp
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue