From a0f0b53686ac52ac9cc287671ab59c838836b831 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Apr 2015 14:48:59 -0700 Subject: [PATCH] fixes to #52, #53 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 7 +++- src/opt/opt_solver.cpp | 53 +++++++++++++++++----------- src/opt/opt_solver.h | 3 +- src/opt/optsmt.cpp | 45 +++++++++++++++-------- src/opt/optsmt.h | 2 +- src/smt/params/smt_params_helper.pyg | 12 +++---- src/tactic/bv/bit_blaster_tactic.cpp | 3 +- 7 files changed, 80 insertions(+), 45 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 11ea9c93b..3cae51bc2 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -388,7 +388,6 @@ namespace opt { } break; case O_MAXSMT: { - m_opt_solver->ensure_pb(); pb_util pb(m); unsigned sz = obj.m_terms.size(); ptr_vector terms; @@ -475,6 +474,9 @@ namespace opt { m_opt_solver->set_logic(m_logic); m_solver = m_opt_solver.get(); } + if (opt_params(m_params).priority() == symbol("pareto")) { + m_opt_solver->ensure_pb(); + } } void context::setup_arith_solver() { @@ -497,6 +499,9 @@ namespace opt { m_maxsat_engine != symbol("sls")) { return; } + if (opt_params(m_params).priority() == symbol("pareto")) { + return; + } m_params.set_bool("minimize_core_partial", true); // false); m_params.set_bool("minimize_core", true); m_sat_solver = mk_inc_sat_solver(m, m_params); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 4556cd080..4f268268d 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -204,38 +204,52 @@ namespace opt { m_valid_objectives[i] = true; TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";); if (m_context.get_context().update_model(has_shared)) { - if (has_shared) { - val2 = current_objective_value(i); - if (val2 != val) { - decrement_value(i, val); - } + if (has_shared && val != current_objective_value(i)) { + decrement_value(i, val); + } + else { + set_model(i); } } else { SASSERT(has_shared); - // model is not final. We set the current objective to - // close to the optimal (ignoring types). - decrement_value(i, val); + decrement_value(i, val); } m_objective_values[i] = val; + TRACE("opt", { tout << val << "\n"; + tout << blocker << "\n"; + model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); }); + } + void opt_solver::set_model(unsigned i) { model_ref mdl; get_model(mdl); m_models.set(i, mdl.get()); - - TRACE("opt", { tout << m_objective_values[i] << "\n"; - tout << blocker << "\n"; - model_smt2_pp(tout << "update model:\n", m, *mdl, 0); }); } - void opt_solver::decrement_value(unsigned i, inf_eps& val) { - if (arith_util(m).is_real(m_objective_sorts[i].get())) { - val -= inf_eps(inf_rational(rational(0),true)); + lbool opt_solver::decrement_value(unsigned i, inf_eps& val) { + push_core(); + expr_ref ge = mk_ge(i, val); + TRACE("opt", tout << ge << "\n";); + assert_expr(ge); + lbool is_sat = m_context.check(0, 0); + if (is_sat == l_true) { + set_model(i); } - else { - val -= inf_eps(inf_rational(rational(1))); + pop_core(1); + TRACE("opt", tout << is_sat << "\n";); + if (is_sat != l_true) { + // cop-out approximation + if (arith_util(m).is_real(m_objective_sorts[i].get())) { + val -= inf_eps(inf_rational(rational(0), true)); + } + else { + val -= inf_eps(inf_rational(rational(1))); + } + m_valid_objectives[i] = false; } - m_valid_objectives[i] = false; + return is_sat; + } @@ -308,8 +322,7 @@ namespace opt { smt::theory_var v = m_objective_vars[i]; return get_optimizer().value(v); } - - + expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) { smt::theory_opt& opt = get_optimizer(); smt::theory_var v = m_objective_vars[var]; diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 9ceee89a7..f3a4099d0 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -134,7 +134,8 @@ namespace opt { char const * logic = "", char const * status = "unknown", char const * attributes = ""); private: - void decrement_value(unsigned i, inf_eps& val); + lbool decrement_value(unsigned i, inf_eps& val); + void set_model(unsigned i); }; } diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index d64730335..6b061f9cd 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -69,10 +69,19 @@ namespace opt { lbool optsmt::basic_opt() { lbool is_sat = l_true; + expr_ref bound(m.mk_true(), m), tmp(m); + expr* vars[1]; + + solver::scoped_push _push(*m_s); while (is_sat == l_true && !m_cancel) { - is_sat = m_s->check_sat(0, 0); + + tmp = m.mk_fresh_const("b", m.mk_bool_sort()); + vars[0] = tmp; + bound = m.mk_implies(tmp, bound); + m_s->assert_expr(bound); + is_sat = m_s->check_sat(1, vars); if (is_sat == l_true) { - update_lower(); + bound = update_lower(); } } @@ -125,17 +134,23 @@ namespace opt { expr_ref_vector ors(m), disj(m); - expr_ref fml(m), bound(m.mk_true(), m); - for (unsigned i = 0; i < m_upper.size(); ++i) { - ors.push_back(m_s->mk_ge(i, m_upper[i])); - } + expr_ref fml(m), bound(m.mk_true(), m), tmp(m); + expr* vars[1]; { - solver::scoped_push _push(*m_s); + for (unsigned i = 0; i < m_upper.size(); ++i) { + ors.push_back(m_s->mk_ge(i, m_upper[i])); + } + fml = m.mk_or(ors.size(), ors.c_ptr()); - m_s->assert_expr(fml); + tmp = m.mk_fresh_const("b", m.mk_bool_sort()); + fml = m.mk_implies(tmp, fml); + vars[0] = tmp; lbool is_sat = l_true; + + solver::scoped_push _push(*m_s); while (!m_cancel) { - is_sat = m_s->check_sat(0,0); + m_s->assert_expr(fml); + is_sat = m_s->check_sat(1,vars); if (is_sat == l_true) { disj.reset(); m_s->maximize_objectives(disj); @@ -151,7 +166,9 @@ namespace opt { } set_max(m_lower, m_s->get_objective_values(), disj); fml = m.mk_or(ors.size(), ors.c_ptr()); - m_s->assert_expr(fml); + tmp = m.mk_fresh_const("b", m.mk_bool_sort()); + fml = m.mk_implies(tmp, fml); + vars[0] = tmp; } else if (is_sat == l_undef) { return l_undef; @@ -181,7 +198,7 @@ namespace opt { m_upper[idx] = v; } - void optsmt::update_lower() { + expr_ref optsmt::update_lower() { expr_ref_vector disj(m); m_s->get_model(m_model); m_s->maximize_objectives(disj); @@ -201,9 +218,7 @@ namespace opt { IF_VERBOSE(3, verbose_stream() << disj << "\n";); IF_VERBOSE(3, model_pp(verbose_stream(), *m_model);); - expr_ref constraint(m); - constraint = m.mk_or(disj.size(), disj.c_ptr()); - m_s->assert_expr(constraint); + return expr_ref(m.mk_or(disj.size(), disj.c_ptr()), m); } lbool optsmt::update_upper() { @@ -243,7 +258,7 @@ namespace opt { IF_VERBOSE(2, verbose_stream() << "(optsmt lower bound for v" << m_vars[i] << " := " << m_upper[i] << ")\n";); m_lower[i] = mid[i]; th.enable_record_conflict(0); - update_lower(); + m_s->assert_expr(update_lower()); break; case l_false: IF_VERBOSE(2, verbose_stream() << "(optsmt conflict: " << th.conflict_minimize() << ") \n";); diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 0a6882b24..ff970556a 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -80,7 +80,7 @@ namespace opt { void set_max(vector& dst, vector const& src, expr_ref_vector& fmls); - void update_lower(); + expr_ref update_lower(); lbool update_upper(); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 6b40d3a62..240d45f15 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -51,10 +51,10 @@ def_module_params(module_name='smt', ('pb.enable_simplex', BOOL, False, 'enable simplex to check rational feasibility'), ('array.weak', BOOL, False, 'weak array theory'), ('array.extensional', BOOL, True, 'extensional array theory'), - ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), - ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'), - ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'), - ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), - ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), - ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded') + ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), + ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'), + ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'), + ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), + ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), + ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded') )) diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 5dbfc4ebd..0391aad51 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -19,7 +19,7 @@ Notes: #include"tactical.h" #include"bit_blaster_model_converter.h" #include"bit_blaster_rewriter.h" -#include"ast_smt2_pp.h" +#include"ast_pp.h" #include"model_pp.h" #include"rewriter_types.h" @@ -82,6 +82,7 @@ class bit_blaster_tactic : public tactic { } if (curr != new_curr) { change = true; + TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << mk_pp(new_curr, m()) << "\n";); g->update(idx, new_curr, new_pr, g->dep(idx)); } }