mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

fix #3528

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-29 12:10:16 -07:00
parent 9be7bda69a
commit 0b10cb3312
1 changed files with 13 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/opt/optsmt.cpp
View file

@ -101,7 +101,7 @@ namespace opt {
lbool optsmt::geometric_opt() { lbool optsmt::geometric_opt() {
lbool is_sat = l_true; lbool is_sat = l_true;
expr_ref bound(m); expr_ref bound(m), last_bound(m);
vector<inf_eps> lower(m_lower); vector<inf_eps> lower(m_lower);
unsigned steps = 0; unsigned steps = 0;
@ -134,21 +134,30 @@ namespace opt {
bound = m_s->mk_ge(delta_index, m_lower[delta_index] + inf_eps(delta_per_step)); bound = m_s->mk_ge(delta_index, m_lower[delta_index] + inf_eps(delta_per_step));
} }
TRACE("opt", tout << "index: " << delta_index << " delta: " << delta_per_step << " : " << bound << "\n";); TRACE("opt", tout << "index: " << delta_index << " delta: " << delta_per_step << " : " << bound << "\n";);
m_s->assert_expr(bound); if (bound == last_bound) {
is_sat = l_false;
}
else {
m_s->assert_expr(bound);
last_bound = bound;
continue;
}
} }
else if (is_sat == l_false && delta_per_step > rational::one()) { if (is_sat == l_false && delta_per_step > rational::one()) {
steps = 0; steps = 0;
step_incs = 0; step_incs = 0;
delta_per_step = 1; delta_per_step = 1;
SASSERT(num_scopes > 0); SASSERT(num_scopes > 0);
--num_scopes; --num_scopes;
m_s->pop(1); m_s->pop(1);
last_bound = nullptr;
} }
else if (is_sat == l_false) { else if (is_sat == l_false) {
// we are done with this delta_index. // we are done with this delta_index.
m_upper[delta_index] = m_lower[delta_index]; m_upper[delta_index] = m_lower[delta_index];
if (num_scopes > 0) m_s->pop(num_scopes); if (num_scopes > 0) m_s->pop(num_scopes);
num_scopes = 0; num_scopes = 0;
last_bound = nullptr;
bool all_tight = true; bool all_tight = true;
for (unsigned i = 0; i < m_lower.size(); ++i) { for (unsigned i = 0; i < m_lower.size(); ++i) {
all_tight &= m_lower[i] == m_upper[i]; all_tight &= m_lower[i] == m_upper[i];