mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

about to create a lemma in niil_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-16 13:03:42 +08:00
parent 0340c8c338
commit fd0f6bcbf9
1 changed files with 43 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/util/lp/niil_solver.cpp
View file

@ -174,23 +174,61 @@ struct solver::imp {
return r == model_val; return r == model_val;
} }
std::unordered_set<lpvar> vec_to_set(const svector<lpvar> & a) const {
std::unordered_set<lpvar> ret;
for (auto j : a)
ret.insert(j);
return ret;
}
bool var_vectors_are_equal(const svector<lpvar> & a, const svector<lpvar> & b) const {
return vec_to_set(a) == vec_to_set(b);
}
bool generate_basic_lemma_for_mon_sign_var_other_mon( bool generate_basic_lemma_for_mon_sign_var_other_mon(
unsigned i_mon,
unsigned j_var, unsigned j_var,
const svector<unsigned> & mon_vars, const svector<unsigned> & mon_vars,
const mon_eq& other_m, bool sign, lemma& l) { const mon_eq& other_m, int sign, lemma& l) {
if (mon_vars.size() != other_m.size()) if (mon_vars.size() != other_m.size())
return false; return false;
auto other_vars_copy = other_m.m_vs;
int other_sign = 1;
reduce_monomial_to_minimal(other_vars_copy, other_sign);
if (var_vectors_are_equal(mon_vars, other_vars_copy)
&& values_are_different(m_monomials[i_mon].var(),
sign * other_sign, other_m.var())) {
fill_lemma();
return true;
}
return false; return false;
} }
bool values_are_different(lpvar j, int sign, lpvar k) const {
SASSERT(sign == 1 || sign == -1);
if (sign == 1)
return m_lar_solver.get_column_value(j) != m_lar_solver.get_column_value(k);
return m_lar_solver.get_column_value(j) != - m_lar_solver.get_column_value(k);
}
void fill_lemma() {
SASSERT(false); // not implemented
}
bool generate_basic_lemma_for_mon_sign_var(unsigned i_mon, bool generate_basic_lemma_for_mon_sign_var(unsigned i_mon,
unsigned j_var, const svector<lpvar>& mon_vars, lemma& l, bool sign) { unsigned j_var, const svector<lpvar>& mon_vars, lemma& l, int sign) {
auto it = m_var_to_monomials.find(j_var); auto it = m_var_to_monomials.find(j_var);
for (auto other_i_mon : it->second) { for (auto other_i_mon : it->second) {
if (other_i_mon == i_mon) continue; if (other_i_mon == i_mon) continue;
if (generate_basic_lemma_for_mon_sign_var_other_mon(j_var, mon_vars, if (generate_basic_lemma_for_mon_sign_var_other_mon(
m_monomials[other_i_mon], sign, l)) i_mon,
j_var,
mon_vars,
m_monomials[other_i_mon],
sign,
l))
return true; return true;
} }
return false; return false;