mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

work on switcher

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-08-10 15:17:13 +08:00 • committed by Lev Nachmanson
parent 032a4efdb6
commit 253facff46
3 changed files with 37 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/smt/theory_lra.cpp
View file

@ -282,6 +282,18 @@ class theory_lra::imp {
}
}
void pop(unsigned scopes) {
if (m_use_niil) {
if (m_niil != nullptr)
(*m_niil)->pop(scopes);
}
else {
if (m_nra != nullptr)
(*m_nra)->pop(scopes);
}
}
void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
if (m_use_niil) {
m_th_imp.ensure_niil();
@ -398,10 +410,21 @@ class theory_lra::imp {
return add_const(1, is_int ? m_one_var : m_rone_var, is_int);
}
lp::var_index get_zero(bool is_int) {
return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int);
lp::var_index get_zero() {
add_const(0, m_zero_var);
return m_zero_var;
}
void ensure_niil() {
if (!m_niil) {
std::cout << "ensure_niil\n";
m_niil = alloc(niil::solver, *m_solver.get(), m.limit(), ctx().get_params());
m_switcher.m_niil = &m_niil;
for (auto const& _s : m_scopes) {
(void)_s;
m_niil->push();
}
}
}
void found_not_handled(expr* n) {
m_not_handled = n;
@ -598,13 +621,7 @@ class theory_lra::imp {
}
TRACE("arith", tout << "v" << v << "(" << get_var_index(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";);
if (!_has_var) {
if (m_use_niil) {
ensure_niil();
m_niil->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
} else {
ensure_nra();
m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
}
m_switcher.add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
}
}
@ -1068,7 +1085,7 @@ public:
// VERIFY(l_false != make_feasible());
m_new_bounds.reset();
m_to_check.reset();
if (m_nra) m_nra->pop(num_scopes);
m_switcher.pop(num_scopes);
TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
}

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

@ -32,6 +32,12 @@ struct solver::imp {
void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) {
std::cout << "called add_monomial\n";
}
void solver::pop(unsigned) {
}
void solver::push(){ }
solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) {
m_imp = alloc(imp, s, lim, p);
}

3
src/util/lp/niil_solver.h
View file

@ -33,5 +33,8 @@ public:
void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);
solver(lp::lar_solver& s, reslimit& lim, params_ref const& p);
imp* get_imp();
void push();
void pop(unsigned scopes);
};
}