mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

start on generate_lemma in niil_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-14 17:14:52 +08:00
parent 31d44471a1
commit 134ebb5712
1 changed files with 64 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,10 +25,10 @@ namespace niil {
typedef nra::mon_eq mon_eq; typedef nra::mon_eq mon_eq;
struct solver::imp { struct solver::imp {
vector<mon_eq> m_monomials;
vector<mon_eq> m_monomials; unsigned_vector m_monomials_lim;
unsigned_vector m_monomials_lim; lp::lar_solver& m_lar_solver;
lp::lar_solver& m_lar_solver; std::unordered_map<lp::var_index, svector<unsigned>> m_var_to_monomials;
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
: m_lar_solver(s) : m_lar_solver(s)
// m_limit(lim), // m_limit(lim),
@ -59,7 +59,61 @@ struct solver::imp {
return r == model_val; return r == model_val;
} }
lbool check(lemma& ) { bool generate_basic_lemma_for_mon_sign(const mon_eq& m, lemma& l) {
return false;
}
bool generate_basic_lemma_for_mon_zero(const mon_eq& m, lemma& l) {
return false;
}
bool generate_basic_lemma_for_mon_neutral(const mon_eq& m, lemma& l) {
return false;
}
bool generate_basic_lemma_for_mon_proportionality(const mon_eq& m, lemma& l) {
return false;
}
bool generate_basic_lemma_for_mon(const mon_eq& m, lemma & l) {
return generate_basic_lemma_for_mon_sign(m, l)
|| generate_basic_lemma_for_mon_zero(m, l)
|| generate_basic_lemma_for_mon_neutral(m, l)
|| generate_basic_lemma_for_mon_proportionality(m, l);
}
bool generate_basic_lemma(lemma & l, svector<unsigned> & to_refine) {
for (unsigned i : to_refine)
if (generate_basic_lemma_for_mon(m_monomials[i], l))
return true;
return false;
}
void map_monominals_vars(unsigned i) {
const mon_eq& m = m_monomials[i];
for (lp::var_index j : m.m_vs) {
auto it = m_var_to_monomials.find(j);
if (it == m_var_to_monomials.end()) {
auto vect = svector<unsigned>();
vect.push_back(i);
m_var_to_monomials[j] = vect;
}
else {
it->second.push_back(i);
}
}
}
void map_var_to_monomials() {
for (unsigned i = 0; i < m_monomials.size(); i++)
map_monominals_vars(i);
}
void init_search() {
map_var_to_monomials();
}
lbool check(lemma& l) {
lp_assert(m_lar_solver.get_status() == lp::lp_status::OPTIMAL); lp_assert(m_lar_solver.get_status() == lp::lp_status::OPTIMAL);
svector<unsigned> to_refine; svector<unsigned> to_refine;
for (unsigned i = 0; i < m_monomials.size(); i++) { for (unsigned i = 0; i < m_monomials.size(); i++) {
@ -70,6 +124,11 @@ struct solver::imp {
if (to_refine.size() == 0) if (to_refine.size() == 0)
return l_true; return l_true;
init_search();
if (generate_basic_lemma(l, to_refine))
return l_true;
return l_undef; return l_undef;
} }