mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

move lemma creation into nra_solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-12 19:47:29 -07:00
parent d706d43712
commit 8b546867f0
3 changed files with 15 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/math/lp/nla_core.cpp
View file

@ -1511,25 +1511,15 @@ lbool core::check(vector<lemma>& l_vec) {
m_tangents.tangent_lemma(); m_tangents.tangent_lemma();
} }
if (lp_settings().get_cancel_flag()) if (!m_reslim.inc())
return l_undef; return l_undef;
finish_up: finish_up:
lbool ret = l_vec.empty() ? l_undef : l_false; lbool ret = l_vec.empty() ? l_undef : l_false;
#if 0 #if 0
if (l_vec.empty()) { if (l_vec.empty())
lp::explanation expl; ret = m_nra.check();
ret = m_nra.check(expl); }
if (ret == l_false) {
new_lemma lemma(*this, __FUNCTION__);
lemma &= expl;
set_use_nra_model(true);
} else if (ret == l_true) {
set_use_nra_model(true);
}
}
#endif #endif
TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";); TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";);

15
src/math/lp/nra_solver.cpp
View file

@ -51,7 +51,8 @@ struct solver::imp {
TBD: use partial model from lra_solver to prime the state of nlsat_solver. TBD: use partial model from lra_solver to prime the state of nlsat_solver.
TBD: explore more incremental ways of applying nlsat (using assumptions) TBD: explore more incremental ways of applying nlsat (using assumptions)
*/ */
lbool check(lp::explanation& ex) { lbool check() {
lp::explanation ex;
SASSERT(need_check() && ex.size() == 0); SASSERT(need_check() && ex.size() == 0);
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false); m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
m_zero = alloc(scoped_anum, am()); m_zero = alloc(scoped_anum, am());
@ -89,8 +90,9 @@ struct solver::imp {
TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n");); TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n"););
switch (r) { switch (r) {
case l_true: case l_true:
m_nla_core.set_use_nra_model(true);
break; break;
case l_false: case l_false: {
ex.clear(); ex.clear();
m_nlsat->get_core(core); m_nlsat->get_core(core);
for (auto c : core) { for (auto c : core) {
@ -98,8 +100,11 @@ struct solver::imp {
ex.push_justification(idx, rational(1)); ex.push_justification(idx, rational(1));
TRACE("arith", tout << "ex: " << idx << "\n";); TRACE("arith", tout << "ex: " << idx << "\n";);
} }
nla::new_lemma lemma(m_nla_core, __FUNCTION__);
lemma &= ex;
m_nla_core.set_use_nra_model(true);
break; break;
}
case l_undef: case l_undef:
break; break;
} }
@ -231,8 +236,8 @@ solver::~solver() {
} }
lbool solver::check(lp::explanation& ex) { lbool solver::check() {
return m_imp->check(ex); return m_imp->check();
} }
bool solver::need_check() { bool solver::need_check() {

2
src/math/lp/nra_solver.h
View file

@ -34,7 +34,7 @@ namespace nra {
\brief Check feasiblity of linear constraints augmented by polynomial definitions \brief Check feasiblity of linear constraints augmented by polynomial definitions
that are added. that are added.
*/ */
lbool check(lp::explanation& ex); lbool check();
/* /*
\brief determine whether nra check is needed. \brief determine whether nra check is needed.