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

fix #3898

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-10 11:56:35 -07:00
parent a7123062a0
commit 33677b9803
1 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_lra.cpp
View file

@ -898,10 +898,10 @@ class theory_lra::imp {
} }
void del_bounds(unsigned old_size) { void del_bounds(unsigned old_size) {
for (unsigned i = m_bounds_trail.size(); i > old_size; ) { for (unsigned i = m_bounds_trail.size(); i-- > old_size; ) {
--i;
unsigned v = m_bounds_trail[i]; unsigned v = m_bounds_trail[i];
lp_api::bound* b = m_bounds[v].back(); lp_api::bound* b = m_bounds[v].back();
m_bool_var2bound.erase(v);
// del_use_lists(b); // del_use_lists(b);
dealloc(b); dealloc(b);
m_bounds[v].pop_back(); m_bounds[v].pop_back();
@ -1063,6 +1063,14 @@ public:
v = internalize_def(to_app(n1)); v = internalize_def(to_app(n1));
k = lp_api::lower_t; k = lp_api::lower_t;
} }
if (a.is_le(atom, n1, n2) && is_numeral(n1, r) && is_app(n2)) {
v = internalize_def(to_app(n2));
k = lp_api::lower_t;
}
else if (a.is_ge(atom, n1, n2) && is_numeral(n1, r) && is_app(n2)) {
v = internalize_def(to_app(n2));
k = lp_api::upper_t;
}
else if (a.is_is_int(atom)) { else if (a.is_is_int(atom)) {
internalize_is_int(atom); internalize_is_int(atom);
return true; return true;
@ -2284,11 +2292,12 @@ public:
if (!can_propagate()) { if (!can_propagate()) {
return; return;
} }
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent()) { while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
bool_var bv = m_asserted_atoms[m_asserted_qhead].m_bv; bool_var bv = m_asserted_atoms[m_asserted_qhead].m_bv;
bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true; bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
m_to_check.push_back(bv); m_to_check.push_back(bv);
lp_api::bound* b = nullptr; lp_api::bound* b = nullptr;
TRACE("arith", tout << "propagate: " << bv << "\n";);
if (m_bool_var2bound.find(bv, b)) { if (m_bool_var2bound.find(bv, b)) {
assert_bound(bv, is_true, *b); assert_bound(bv, is_true, *b);
++m_asserted_qhead; ++m_asserted_qhead;
@ -3791,7 +3800,7 @@ public:
m_bounds[v].push_back(a); m_bounds[v].push_back(a);
m_bounds_trail.push_back(v); m_bounds_trail.push_back(v);
m_bool_var2bound.insert(bv, a); m_bool_var2bound.insert(bv, a);
TRACE("arith", tout << mk_pp(b, m) << "\n";); TRACE("arith", tout << "internalized " << bv << ": " << mk_pp(b, m) << "\n";);
} }
if (is_strict) { if (is_strict) {
b = m.mk_not(b); b = m.mk_not(b);