mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

check monomial values in niil_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-13 12:48:41 +08:00
parent f6291abccb
commit 91086baa54
2 changed files with 27 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/util/lp/lar_solver.h
View file

@ -142,6 +142,11 @@ public :
const impq& get_column_value(unsigned j) const { const impq& get_column_value(unsigned j) const {
return m_mpq_lar_core_solver.m_r_x[j]; return m_mpq_lar_core_solver.m_r_x[j];
} }
const mpq& get_column_value_rational(unsigned j) const {
return m_mpq_lar_core_solver.m_r_x[j].x;
}
bool is_term(var_index j) const; bool is_term(var_index j) const;
bool column_is_fixed(unsigned j) const; bool column_is_fixed(unsigned j) const;
public: public:

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

@ -28,9 +28,9 @@ 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_solver; lp::lar_solver& m_lar_solver;
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
: m_solver(s) : m_lar_solver(s)
// m_limit(lim), // m_limit(lim),
// m_params(p) // m_params(p)
{ {
@ -49,8 +49,27 @@ struct solver::imp {
m_monomials_lim.shrink(m_monomials_lim.size() - n); m_monomials_lim.shrink(m_monomials_lim.size() - n);
} }
bool check_monomial(const mon_eq& m) {
SASSERT(m_lar_solver.get_column_value(m.var()).is_int());
const rational & model_val = m_lar_solver.get_column_value_rational(m.var());
rational r(1);
for (auto j : m.m_vs) {
r *= m_lar_solver.get_column_value_rational(j);
}
return r == model_val;
}
lbool check(lp::explanation_t& ex) { lbool check(lp::explanation_t& ex) {
lp_assert(m_solver.get_status() == lp::lp_status::OPTIMAL); lp_assert(m_lar_solver.get_status() == lp::lp_status::OPTIMAL);
svector<unsigned> to_refine;
for (unsigned i = 0; i < m_monomials.size(); i++) {
if (!check_monomial(m_monomials[i]))
to_refine.push_back(i);
}
std::cout << "to_refine size = " << to_refine.size() << std::endl;
if (to_refine.size() == 0)
return l_true;
return l_undef; return l_undef;
} }