From e944f89505748a4d685491f039741a12857d0995 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2015 02:36:01 -0700 Subject: [PATCH 1/2] fix bug introduced when clearing state between calls to Pareto/Box Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 14 +++++++++++--- src/opt/opt_context.h | 2 +- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 0503fa664..11ea9c93b 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -75,9 +75,14 @@ namespace opt { m_hard.push_back(hard); } - void context::scoped_state::set(ptr_vector & hard) { + bool context::scoped_state::set(ptr_vector & hard) { + bool eq = hard.size() == m_hard.size(); + for (unsigned i = 0; eq && i < hard.size(); ++i) { + eq = hard[i] == m_hard[i].get(); + } m_hard.reset(); m_hard.append(hard.size(), hard.c_ptr()); + return !eq; } unsigned context::scoped_state::add(expr* f, rational const& w, symbol const& id) { @@ -161,8 +166,9 @@ namespace opt { } void context::set_hard_constraints(ptr_vector& fmls) { - m_scoped_state.set(fmls); - clear_state(); + if (m_scoped_state.set(fmls)) { + clear_state(); + } } void context::add_hard_constraint(expr* f) { @@ -203,6 +209,7 @@ namespace opt { if (m_box_index != UINT_MAX) { return execute_box(); } + clear_state(); init_solver(); import_scoped_state(); normalize(); @@ -327,6 +334,7 @@ namespace opt { return l_false; } m_box_index = 1; + m_box_models.reset(); lbool r = m_optsmt.box(); for (unsigned i = 0, j = 0; r == l_true && i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 1b5671113..59868dd1e 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -131,7 +131,7 @@ namespace opt { void push(); void pop(); void add(expr* hard); - void set(ptr_vector & hard); + bool set(ptr_vector & hard); unsigned add(expr* soft, rational const& weight, symbol const& id); unsigned add(app* obj, bool is_max); }; From 6b995c4077b959f02ebae5f0fdb31b69ab30d284 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2015 02:56:40 -0700 Subject: [PATCH 2/2] disable wrong fix for simplification Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index faf5ce0ef..1acfcdf57 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() { proof_ref_vector new_prs1(m_manager); expr_ref_vector new_exprs2(m_manager); proof_ref_vector new_prs2(m_manager); - unsigned i = 0; + unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i);