mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

work on niil_solver::check()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-13 11:55:30 +08:00
parent 07c9e22303
commit a86601f7d2
2 changed files with 28 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/smt/theory_lra.cpp
View file

@ -274,8 +274,10 @@ class theory_lra::imp {
lbool check(lp::explanation_t& ex) {
if (m_use_niil) {
if (m_niil != nullptr)
if (m_niil != nullptr) {
std::cout << "check niil\n";
return (*m_niil)->check(ex);
}
}
else {
if (m_nra != nullptr)
@ -2047,16 +2049,7 @@ public:
return lia_check;
}
lbool check_nra() {
m_use_nra_model = false;
if (m.canceled()) {
TRACE("arith", tout << "canceled\n";);
return l_undef;
}
if (!m_nra) return l_true;
if (!m_switcher.need_check()) return l_true;
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_switcher.check(m_explanation);
lbool check_aftermath_nra(lbool r) {
m_a1 = alloc(scoped_anum, m_nra->am());
m_a2 = alloc(scoped_anum, m_nra->am());
switch (r) {
@ -2077,6 +2070,23 @@ public:
return r;
}
lbool check_aftermath_niil(lbool r) {
return r;
}
lbool check_nra() {
m_use_nra_model = false;
if (m.canceled()) {
TRACE("arith", tout << "canceled\n";);
return l_undef;
}
if (!m_nra && !m_niil) return l_true;
if (!m_switcher.need_check()) return l_true;
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_switcher.check(m_explanation);
return m_nra? check_aftermath_nra(r) : check_aftermath_niil(r);
}
/**
\brief We must redefine this method, because theory of arithmetic contains
underspecified operators such as division by 0.

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

@ -48,6 +48,12 @@ struct solver::imp {
m_monomials.shrink(m_monomials_lim[m_monomials_lim.size() - n]);
m_monomials_lim.shrink(m_monomials_lim.size() - n);
}
lbool check(lp::explanation_t& ex) {
lp_assert(m_solver.get_status() == lp::lp_status::OPTIMAL);
return l_undef;
}
};
void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
std::cout << "called add_monomial\n";
@ -56,8 +62,7 @@ void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs)
bool solver::need_check() { return true; }
lbool solver::check(lp::explanation_t& ex) {
lp_assert(false);
return l_undef;
return m_imp->check(ex);
}