mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

improve diagnosability

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-26 14:58:17 -07:00
parent e89071d366
commit 0c25d2560d
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_lra.cpp
View file

@ -183,7 +183,7 @@ class theory_lra::imp {
// non-linear arithmetic
scoped_ptr<nla::solver> m_nla;
scoped_ptr<scoped_anum> m_a1, m_a2;
mutable scoped_ptr<scoped_anum> m_a1, m_a2;
// integer arithmetic
scoped_ptr<lp::int_solver> m_lia;
@ -200,7 +200,7 @@ class theory_lra::imp {
}
};
bool use_nra_model() {
bool use_nra_model() const {
if (m_nla && m_nla->use_nra_model()) {
if (!m_a1) {
m_a1 = alloc(scoped_anum, m_nla->am());
@ -1237,12 +1237,13 @@ public:
return;
}
expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m);
#if 0
expr_ref eqr(m.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p), m);
expr_ref eqr(m.mk_eq(mod_r, p), m);
ctx().get_rewriter()(eqr);
literal eq = mk_literal(eqr);
#else
literal eq = th.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p, false);
literal eq = th.mk_eq(mod_r, p, false);
#endif
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
@ -2195,7 +2196,6 @@ public:
TRACE("arith", tout << "v" << v << " " << be.kind() << " " << be.m_bound << "\n";);
reserve_bounds(v);
if (m_unassigned_bounds[v] == 0 && !should_refine_bounds()) {
TRACE("arith", tout << "return\n";);
@ -3238,7 +3238,7 @@ public:
TRACE("arith", display(tout););
}
nlsat::anum const& nl_value(theory_var v, scoped_anum& r) {
nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const {
SASSERT(use_nra_model());
auto t = get_tv(v);
if (t.is_term()) {
@ -3658,7 +3658,7 @@ public:
}
void display(std::ostream & out) {
void display(std::ostream & out) const {
if (m_solver) {
m_solver->display(out);
}