mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
a version with less pointers: got a conflict
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
Lev Nachmanson
parent
5a36e02c58
commit
52653e6e43
|
|
@ -12,6 +12,14 @@ namespace lp {
|
|||
class term_o:public lar_term {
|
||||
mpq m_c;
|
||||
public:
|
||||
term_o clone() const {
|
||||
term_o ret;
|
||||
for (const auto & p: *this) {
|
||||
ret.add_monomial(p.coeff(), p.j());
|
||||
}
|
||||
ret.c() = c();
|
||||
return ret;
|
||||
}
|
||||
const mpq& c() const { return m_c; }
|
||||
mpq& c() { return m_c; }
|
||||
term_o():m_c(0) {}
|
||||
|
|
@ -32,7 +40,11 @@ namespace lp {
|
|||
}
|
||||
};
|
||||
|
||||
std::ostream& print_term(term_o const& term, std::ostream& out, const std::string & var_prefix) const {
|
||||
std::ostream& print_lar_term_L(lar_term & t, std::ostream & out) const {
|
||||
return print_linear_combination_customized(t.coeffs_as_vector(), [](int j)->std::string {return "y"+std::to_string(j);}, out );
|
||||
}
|
||||
|
||||
std::ostream& print_term_o(term_o const& term, std::ostream& out, const std::string & var_prefix) const {
|
||||
if (term.size() == 0) {
|
||||
out << "0";
|
||||
return out;
|
||||
|
|
@ -57,8 +69,13 @@ namespace lp {
|
|||
out << var_prefix << p.j();
|
||||
}
|
||||
|
||||
if (!term.c().is_zero())
|
||||
out << " + " << term.c();
|
||||
if (!term.c().is_zero()) {
|
||||
if (term.c().is_pos())
|
||||
out << " + " << term.c();
|
||||
else
|
||||
out << " - " << -term.c();
|
||||
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
@ -67,19 +84,19 @@ namespace lp {
|
|||
e is an equation and ℓ is a linear combination of variables from L
|
||||
*/
|
||||
struct eprime_pair {
|
||||
term_o * m_e;
|
||||
lar_term * m_l;
|
||||
term_o m_e;
|
||||
lar_term m_l;
|
||||
};
|
||||
vector<eprime_pair> m_eprime;
|
||||
/*
|
||||
Let L be a set of variables disjoint from X, and let λ be a mapping from variables in
|
||||
L to linear combinations of variables in X and of integer constants
|
||||
*/
|
||||
u_map<unsigned> m_lambda; // maps to the index of the term in m_eprime
|
||||
u_map<unsigned> m_lambda; // maps to the index of the eprime_pair in m_eprime
|
||||
/* let σ be a partial mapping from variables in L united with X to linear combinations
|
||||
of variables in X and of integer constants showing the substitutions
|
||||
*/
|
||||
u_map<lar_term*> m_sigma;
|
||||
u_map<term_o> m_sigma;
|
||||
|
||||
public:
|
||||
int_solver& lia;
|
||||
|
|
@ -90,20 +107,13 @@ namespace lp {
|
|||
std::list<unsigned> m_f; // F = {λ(t):t in m_f}
|
||||
// set S
|
||||
std::list<unsigned> m_s; // S = {λ(t): t in m_s}
|
||||
|
||||
unsigned m_conflict_index = -1; // m_eprime[m_conflict_index] gives the conflict
|
||||
|
||||
imp(int_solver& lia, lar_solver& lra): lia(lia), lra(lra) {
|
||||
m_last_fresh_x_var = -1;
|
||||
}
|
||||
|
||||
bool belongs_to_list(term_o* t, std::list<term_o*> l) {
|
||||
for (auto& item : l) {
|
||||
if (item == t) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void init() {
|
||||
unsigned n_of_rows = static_cast<unsigned>(lra.r_basis().size());
|
||||
unsigned skipped = 0;
|
||||
|
|
@ -122,31 +132,32 @@ namespace lp {
|
|||
}
|
||||
|
||||
if (all_vars_are_int) {
|
||||
term_o* t = new term_o();
|
||||
term_o t;
|
||||
const auto lcm = get_denominators_lcm(row);
|
||||
for (const auto & p: row) {
|
||||
t->add_monomial(lcm * p.coeff(), p.var());
|
||||
t.add_monomial(lcm * p.coeff(), p.var());
|
||||
if(lia.is_fixed(p.var())) {
|
||||
t->c() += lia.lower_bound(p.var()).x;
|
||||
t.c() += lia.lower_bound(p.var()).x;
|
||||
}
|
||||
}
|
||||
unsigned lvar = static_cast<unsigned>(m_f.size());
|
||||
lar_term* lt = new lar_term();
|
||||
lt->add_var(lvar);
|
||||
lar_term lt = lar_term(lvar);
|
||||
eprime_pair pair = {t, lt};
|
||||
m_eprime.push_back(pair);
|
||||
m_lambda.insert(lvar, lvar);
|
||||
m_f.push_back(lvar);
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
// returns true if no conflict is found and false otherwise
|
||||
bool normalize_e_by_gcd(term_o& e) {
|
||||
bool normalize_e_by_gcd(eprime_pair& ep) {
|
||||
mpq g(0);
|
||||
for (auto & p : e) {
|
||||
TRACE("dioph_eq", print_term_o(ep.m_e, tout << "m_e:", "x") << std::endl;
|
||||
print_lar_term_L(ep.m_l, tout << "m_l:") << std::endl;
|
||||
);
|
||||
for (auto & p : ep.m_e) {
|
||||
if (g.is_zero()) {
|
||||
g = abs(p.coeff());
|
||||
} else {
|
||||
|
|
@ -158,20 +169,38 @@ namespace lp {
|
|||
}
|
||||
if (g.is_one())
|
||||
return true;
|
||||
std::cout << "reached\n";
|
||||
e.c() *= (1/g);
|
||||
if (!e.c().is_int()) {
|
||||
mpq new_c = ep.m_e.c() / g;
|
||||
if (new_c.is_int() == false) {
|
||||
// conlict: todo - collect the conflict
|
||||
NOT_IMPLEMENTED_YET();
|
||||
TRACE("dioph_eq",
|
||||
print_term_o(ep.m_e, tout << "conflict m_e:", "x") << std::endl;
|
||||
tout << "g:" << g << std::endl;
|
||||
print_lar_term_L(ep.m_l, tout << "m_l:") << std::endl;
|
||||
for (const auto & p: ep.m_l) {
|
||||
tout << p.coeff() << "("; print_term_o(m_eprime[p.j()].m_e, tout, "x") << ")"<< std::endl;
|
||||
}
|
||||
tout << "S:\n";
|
||||
for (const auto& t : m_sigma) {
|
||||
tout << "x" << t.m_key << " -> ";
|
||||
print_term_o(t.m_value, tout, "x") << std::endl;
|
||||
}
|
||||
);
|
||||
return false;
|
||||
} else {
|
||||
for (auto& p: ep.m_e.coeffs()) {
|
||||
p.m_value /= g;
|
||||
}
|
||||
ep.m_e.c() = new_c;
|
||||
ep.m_l *= (1/g);
|
||||
|
||||
}
|
||||
return true;
|
||||
}
|
||||
// returns true if no conflict is found and false otherwise
|
||||
bool normalize_by_gcd() {
|
||||
for (unsigned l: m_f) {
|
||||
term_o* e = m_eprime[l].m_e;
|
||||
if (!normalize_e_by_gcd(*e)) {
|
||||
if (!normalize_e_by_gcd(m_eprime[l])) {
|
||||
m_conflict_index = l;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
|
@ -191,50 +220,69 @@ namespace lp {
|
|||
return m_f.begin(); // TODO: make a smarter joice
|
||||
}
|
||||
|
||||
void substitute(unsigned k, term_o* s) {
|
||||
print_term(*s, std::cout<< k<< "->", "x") << std::endl;
|
||||
void substitute_var_on_f(unsigned k, int k_sign, const term_o& k_subst, const lar_term& l_term) {
|
||||
TRACE("dioph_eq", print_term_o(k_subst, tout<< k<< "->", "x") << std::endl;);
|
||||
for (unsigned e_index: m_f) {
|
||||
term_o* e = m_eprime[e_index].m_e;
|
||||
if (!e->contains(k)) continue;
|
||||
print_term(*e, std::cout << "before:", "x") << std::endl;
|
||||
e->substitute(*s, k);
|
||||
print_term(*e, std::cout << "after :", "x") << std::endl;
|
||||
term_o& e = m_eprime[e_index].m_e;
|
||||
if (!e.contains(k)) continue;
|
||||
const mpq& k_coeff = e.get_coeff(k);
|
||||
TRACE("dioph_eq", print_term_o(e, tout << "before:", "x") << std::endl;
|
||||
tout << "k_coeff:" << k_coeff << std::endl;);
|
||||
m_eprime[e_index].m_l = k_sign*k_coeff*l_term + lar_term(e_index); // m_l is set to k_sign*e + e_sub
|
||||
e.substitute(k_subst, k);
|
||||
TRACE("dioph_eq", print_term_o(e, tout << "after :", "x") << std::endl;
|
||||
print_lar_term_L(m_eprime[e_index].m_l, tout) << std::endl;);
|
||||
}
|
||||
}
|
||||
|
||||
std::tuple<mpq, unsigned, int> find_minimal_abs_coeff(const term_o& eh) const {
|
||||
bool first = true;
|
||||
mpq ahk;
|
||||
unsigned k;
|
||||
int k_sign;
|
||||
mpq t;
|
||||
for (auto& p : eh) {
|
||||
t = abs(p.coeff());
|
||||
if (first || t < ahk) {
|
||||
ahk = t;
|
||||
k_sign = p.coeff().is_pos() ? 1 : -1;
|
||||
k = p.j();
|
||||
if (ahk.is_one())
|
||||
break;
|
||||
first = false;
|
||||
}
|
||||
}
|
||||
return std::make_tuple(ahk, k, k_sign);
|
||||
}
|
||||
|
||||
term_o get_term_to_subst(const term_o& eh, unsigned k, int k_sign) {
|
||||
term_o t;
|
||||
for (const auto & p: eh) {
|
||||
if (p.j() == k) continue;
|
||||
t.add_monomial(-k_sign*p.coeff(), p.j());
|
||||
}
|
||||
t.c() = eh.c();
|
||||
TRACE("dioph_eq", tout << "subst_term:"; print_term_o(t, tout, "x") << std::endl;);
|
||||
return t;
|
||||
}
|
||||
// this is the step 6 or 7 of the algorithm
|
||||
void rewrite_eqs() {
|
||||
auto eh_it = pick_eh();
|
||||
auto eprime_entry = m_eprime[*eh_it];
|
||||
std
|
||||
term_o* eh = m_eprime[*eh_it].m_e;
|
||||
|
||||
// looking for minimal in absolute value coefficient
|
||||
bool first = true;
|
||||
mpq ahk;
|
||||
unsigned k;
|
||||
int k_sign;
|
||||
for (auto& p: *eh) {
|
||||
if (first || abs(p.coeff()) < ahk) {
|
||||
ahk = abs(p.coeff());
|
||||
k_sign = p.coeff().is_pos()? 1:-1;
|
||||
k = p.j();
|
||||
if (ahk.is_one())
|
||||
break;
|
||||
first = false;
|
||||
}
|
||||
}
|
||||
TRACE("dioph_eq", tout << "eprime_entry[" << *eh_it << "]{\n";
|
||||
print_term_o(m_eprime[*eh_it].m_e, tout << "\tm_e:", "x") << "," << std::endl;
|
||||
print_lar_term_L(m_eprime[*eh_it].m_l, tout<< "\tm_l:") << "\n}"<< std::endl;);
|
||||
|
||||
term_o& eh = m_eprime[*eh_it].m_e;
|
||||
auto [ahk, k, k_sign] = find_minimal_abs_coeff(eh);
|
||||
|
||||
if (ahk.is_one()) {
|
||||
// step 6
|
||||
term_o *s_term = new term_o();
|
||||
s_term->j() = k; // keep the assigned variable in m_j of the term
|
||||
for (auto& p:*eh) {
|
||||
if (p.j() == k) continue;
|
||||
s_term->add_monomial(-k_sign*p.coeff(), p.j());
|
||||
}
|
||||
m_s.push_back(*eh_it);
|
||||
m_f.erase(eh_it);
|
||||
m_sigma.insert(k, s_term);
|
||||
substitute(k, s_term);
|
||||
term_o t = get_term_to_subst(eh, k, k_sign);
|
||||
m_sigma.insert(k, t);
|
||||
substitute_var_on_f(k, k_sign, t, eprime_entry.m_l) ;
|
||||
} else {
|
||||
// step 7
|
||||
// the fresh variable
|
||||
|
|
@ -244,7 +292,21 @@ namespace lp {
|
|||
}
|
||||
|
||||
}
|
||||
|
||||
void explain(lp::explanation& ex) {
|
||||
auto & ep = m_eprime[m_conflict_index];
|
||||
for (const auto & p : ep.m_l) {
|
||||
remove_fresh_variables(m_eprime[p.j()].m_e);
|
||||
}
|
||||
u_dependency* dep = nullptr;
|
||||
for (const auto & p : ep.m_l) {
|
||||
if (lra.column_is_fixed(p.j())) {
|
||||
lra.explain_fixed_column(p.j(), ex);
|
||||
}
|
||||
}
|
||||
}
|
||||
void remove_fresh_variables(term_o& t) {
|
||||
// TODO implement
|
||||
}
|
||||
};
|
||||
// Constructor definition
|
||||
dioph_eq::dioph_eq(int_solver& lia): lia(lia) {
|
||||
|
|
@ -255,8 +317,10 @@ namespace lp {
|
|||
}
|
||||
|
||||
lia_move dioph_eq::check() {
|
||||
return m_imp->check();
|
||||
|
||||
return m_imp->check();
|
||||
}
|
||||
void dioph_eq::explain(lp::explanation& ex) {
|
||||
m_imp->explain(ex);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -29,5 +29,6 @@ namespace lp {
|
|||
dioph_eq(int_solver& lia);
|
||||
~dioph_eq();
|
||||
lia_move check();
|
||||
void explain(lp::explanation&);
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -166,7 +166,14 @@ namespace lp {
|
|||
|
||||
lia_move solve_dioph_eq() {
|
||||
dioph_eq de(lia);
|
||||
de.check();
|
||||
lia_move r = de.check();
|
||||
|
||||
if (r == lia_move::unsat) {
|
||||
de.explain(*this->m_ex);
|
||||
} else if (r == lia_move::sat) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
return lia_move::undef;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -760,6 +760,13 @@ namespace lp {
|
|||
}
|
||||
|
||||
|
||||
void lar_solver::explain_fixed_column(unsigned j, explanation& ex) {
|
||||
SASSERT(column_is_fixed(j));
|
||||
auto* deps = get_bound_constraint_witnesses_for_column(j);
|
||||
for (auto ci : flatten(deps))
|
||||
ex.push_back(ci);
|
||||
}
|
||||
|
||||
void lar_solver::remove_fixed_vars_from_base() {
|
||||
// this will allow to disable and restore the tracking of the touched rows
|
||||
flet<indexed_uint_set*> f(m_mpq_lar_core_solver.m_r_solver.m_touched_rows, nullptr);
|
||||
|
|
|
|||
|
|
@ -591,6 +591,7 @@ public:
|
|||
}
|
||||
return dep;
|
||||
}
|
||||
void explain_fixed_column(unsigned j, explanation& ex);
|
||||
u_dependency* join_deps(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); }
|
||||
inline constraint_set const& constraints() const { return m_constraints; }
|
||||
void push();
|
||||
|
|
|
|||
|
|
@ -118,6 +118,12 @@ public:
|
|||
m_coeffs.erase(j);
|
||||
}
|
||||
|
||||
|
||||
const mpq & get_coeff(unsigned j) const {
|
||||
auto* it = m_coeffs.find_core(j);
|
||||
SASSERT(it != nullptr);
|
||||
return it->get_data().m_value;
|
||||
}
|
||||
// the monomial ax[j] is substituted by ax[k]
|
||||
void subst_index(unsigned j, unsigned k) {
|
||||
auto* it = m_coeffs.find_core(j);
|
||||
|
|
@ -145,6 +151,33 @@ public:
|
|||
return ret;
|
||||
}
|
||||
|
||||
|
||||
lar_term clone() const {
|
||||
lar_term ret;
|
||||
for (const auto& p : *this) {
|
||||
ret.add_monomial(p.coeff(), p.j());
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
|
||||
lar_term operator+(const lar_term& other) const {
|
||||
lar_term ret = other.clone();
|
||||
for (const auto& p : *this) {
|
||||
ret.add_monomial(p.coeff(), p.j());
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
|
||||
friend lar_term operator*(const mpq& k, const lar_term& term) {
|
||||
lar_term result;
|
||||
for (const auto& p : term) {
|
||||
result.add_monomial(p.coeff()*k, p.j());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
lar_term& operator*=(mpq const& k) {
|
||||
for (auto & t : m_coeffs)
|
||||
t.m_value *= k;
|
||||
|
|
|
|||
|
|
@ -273,13 +273,7 @@ public:
|
|||
}
|
||||
return base;
|
||||
}
|
||||
|
||||
void explain_fixed_column(unsigned j, explanation& ex) {
|
||||
SASSERT(column_is_fixed(j));
|
||||
auto* deps = lp().get_bound_constraint_witnesses_for_column(j);
|
||||
for (auto ci : lp().flatten(deps))
|
||||
ex.push_back(ci);
|
||||
}
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
bool all_fixed_in_row(unsigned row) const {
|
||||
for (const auto& c : lp().get_row(row))
|
||||
|
|
|
|||
Loading…
Reference in a new issue