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

nra to nla

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-07 17:12:38 -07:00
parent dae67987b5
commit 151397a067
1 changed files with 5 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/smt/theory_lra.cpp
View file

@ -270,20 +270,6 @@ class theory_lra::imp {
scoped_ptr<nla::solver> m_nla; scoped_ptr<nla::solver> m_nla;
scoped_ptr<scoped_anum> m_a1, m_a2; scoped_ptr<scoped_anum> m_a1, m_a2;
struct switcher {
theory_lra::imp& m_th_imp;
scoped_ptr<nla::solver>* m_nla;
switcher(theory_lra::imp& i): m_th_imp(i), m_nla(nullptr) {
}
bool need_check() {
if (m_nla != nullptr)
return (*m_nla)->need_check();
return false;
}
};
// integer arithmetic // integer arithmetic
scoped_ptr<lp::int_solver> m_lia; scoped_ptr<lp::int_solver> m_lia;
@ -314,7 +300,6 @@ class theory_lra::imp {
scoped_ptr<lp::lar_solver> m_solver; scoped_ptr<lp::lar_solver> m_solver;
resource_limit m_resource_limit; resource_limit m_resource_limit;
lp_bounds m_new_bounds; lp_bounds m_new_bounds;
switcher m_switcher;
symbol m_farkas; symbol m_farkas;
context& ctx() const { return th.get_context(); } context& ctx() const { return th.get_context(); }
@ -957,7 +942,6 @@ public:
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)), m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
m_solver(nullptr), m_solver(nullptr),
m_resource_limit(*this), m_resource_limit(*this),
m_switcher(*this),
m_farkas("farkas") { m_farkas("farkas") {
} }
@ -1710,7 +1694,7 @@ public:
break; break;
} }
switch (check_nra()) { switch (check_nla()) {
case l_true: case l_true:
break; break;
case l_false: case l_false:
@ -2151,7 +2135,7 @@ public:
set_conflict_or_lemma(core, false); set_conflict_or_lemma(core, false);
} }
lbool check_nra_continue() { lbool check_nla_continue() {
m_a1 = nullptr; m_a2 = nullptr; m_a1 = nullptr; m_a2 = nullptr;
auto & lv = m_nla_lemma_vector; auto & lv = m_nla_lemma_vector;
lbool r = m_nla->check(lv); lbool r = m_nla->check(lv);
@ -2174,14 +2158,14 @@ public:
return r; return r;
} }
lbool check_nra() { lbool check_nla() {
if (!m.inc()) { if (!m.inc()) {
TRACE("arith", tout << "canceled\n";); TRACE("arith", tout << "canceled\n";);
return l_undef; return l_undef;
} }
if (!m_nla) return l_true; if (!m_nla) return l_true;
if (!m_switcher.need_check()) return l_true; if (!m_nla->need_check()) return l_true;
return check_nra_continue(); return check_nla_continue();
} }
/** /**