diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index a95f1d8b1..c2f437391 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -379,10 +379,8 @@ extern "C" { for (unsigned i = 0; i < coll.m_rules.size(); ++i) { to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]); } - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - for (; it != end; ++it) { - to_fixedpoint_ref(d)->ctx().assert_expr(*it); + for (expr * e : ctx.assertions()) { + to_fixedpoint_ref(d)->ctx().assert_expr(e); } return of_ast_vector(v); diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 45832b5b6..0b56b788d 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -354,10 +354,8 @@ extern "C" { return; } - ptr_vector::const_iterator it = ctx->begin_assertions(); - ptr_vector::const_iterator end = ctx->end_assertions(); - for (; it != end; ++it) { - to_optimize_ptr(opt)->add_hard_constraint(*it); + for (expr * e : ctx->assertions()) { + to_optimize_ptr(opt)->add_hard_constraint(e); } } diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index b88f273f9..32c133d2b 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -71,10 +71,8 @@ extern "C" { SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str()); return of_ast_vector(v); } - ptr_vector::const_iterator it = ctx->begin_assertions(); - ptr_vector::const_iterator end = ctx->end_assertions(); - for (; it != end; ++it) { - v->m_ast_vector.push_back(*it); + for (expr * e : ctx->assertions()) { + v->m_ast_vector.push_back(e); } return of_ast_vector(v); Z3_CATCH_RETURN(nullptr); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index fc4e01f3a..204370346 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -157,10 +157,8 @@ extern "C" { bool initialized = to_solver(s)->m_solver.get() != nullptr; if (!initialized) init_solver(c, s); - ptr_vector::const_iterator it = ctx->begin_assertions(); - ptr_vector::const_iterator end = ctx->end_assertions(); - for (; it != end; ++it) { - to_solver_ref(s)->assert_expr(*it); + for (expr * e : ctx->assertions()) { + to_solver_ref(s)->assert_expr(e); } to_solver_ref(s)->set_model_converter(ctx->get_model_converter()); } diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index 47b3e9203..5cd3542df 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -393,10 +393,8 @@ expr_pattern_match::initialize(char const * spec_string) { VERIFY(parse_smt2_commands(ctx, is)); ctx.set_print_success(ps); - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - for (; it != end; ++it) { - compile(*it); + for (expr * e : ctx.assertions()) { + compile(e); } TRACE("expr_pattern_match", display(tout); ); } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 89fb4f3cc..8a23f80a0 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1312,7 +1312,7 @@ void cmd_context::assert_expr(expr * t) { m().inc_ref(t); m_assertions.push_back(t); if (produce_unsat_cores()) - m_assertion_names.push_back(0); + m_assertion_names.push_back(nullptr); if (m_solver) m_solver->assert_expr(t); } @@ -1491,7 +1491,18 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions expr_ref_vector asms(m()); asms.append(num_assumptions, assumptions); if (!m_processing_pareto) { - get_opt()->set_hard_constraints(m_assertions); + expr_ref_vector assertions(m()); + unsigned sz = m_assertions.size(); + for (unsigned i = 0; i < sz; ++i) { + if (m_assertion_names.size() > i && m_assertion_names[i]) { + asms.push_back(m_assertion_names[i]); + assertions.push_back(m().mk_implies(m_assertion_names[i], m_assertions[i])); + } + else { + assertions.push_back(m_assertions[i]); + } + } + get_opt()->set_hard_constraints(assertions); } try { r = get_opt()->optimize(asms); @@ -1802,11 +1813,8 @@ void cmd_context::validate_model() { cancel_eh eh(m().limit()); expr_ref r(m()); scoped_ctrl_c ctrlc(eh); - ptr_vector::const_iterator it = begin_assertions(); - ptr_vector::const_iterator end = end_assertions(); bool invalid_model = false; - for (; it != end; ++it) { - expr * a = *it; + for (expr * a : assertions()) { if (is_ground(a)) { r = nullptr; evaluator(a, r); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 87d80babe..cb49d1825 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -149,7 +149,7 @@ public: virtual void push() = 0; virtual void pop(unsigned n) = 0; virtual lbool optimize(expr_ref_vector const& asms) = 0; - virtual void set_hard_constraints(ptr_vector & hard) = 0; + virtual void set_hard_constraints(expr_ref_vector const & hard) = 0; virtual void display_assignment(std::ostream& out) = 0; virtual bool is_pareto() = 0; virtual void set_logic(symbol const& s) = 0; @@ -452,11 +452,8 @@ public: double get_seconds() const { return m_watch.get_seconds(); } - ptr_vector::const_iterator begin_assertions() const { return m_assertions.begin(); } - ptr_vector::const_iterator end_assertions() const { return m_assertions.end(); } - - ptr_vector::const_iterator begin_assertion_names() const { return m_assertion_names.begin(); } - ptr_vector::const_iterator end_assertion_names() const { return m_assertion_names.end(); } + ptr_vector const& assertions() const { return m_assertions; } + ptr_vector const& assertion_names() const { return m_assertion_names; } /** \brief Hack: consume assertions if there are no scopes. diff --git a/src/cmd_context/cmd_context_to_goal.cpp b/src/cmd_context/cmd_context_to_goal.cpp index a66f9e5de..de19805f2 100644 --- a/src/cmd_context/cmd_context_to_goal.cpp +++ b/src/cmd_context/cmd_context_to_goal.cpp @@ -28,20 +28,18 @@ void assert_exprs_from(cmd_context const & ctx, goal & t) { ast_manager & m = t.m(); bool proofs_enabled = t.proofs_enabled(); if (ctx.produce_unsat_cores()) { - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - ptr_vector::const_iterator it2 = ctx.begin_assertion_names(); - SASSERT(end - it == ctx.end_assertion_names() - it2); + ptr_vector::const_iterator it = ctx.assertions().begin(); + ptr_vector::const_iterator end = ctx.assertions().end(); + ptr_vector::const_iterator it2 = ctx.assertion_names().begin(); + SASSERT(ctx.assertions().size() == ctx.assertion_names().size()); for (; it != end; ++it, ++it2) { t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : nullptr, m.mk_leaf(*it2)); } } else { - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - for (; it != end; ++it) { - t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : nullptr, nullptr); + for (expr * e : ctx.assertions()) { + t.assert_expr(e, proofs_enabled ? m.mk_asserted(e) : nullptr, nullptr); } - SASSERT(ctx.begin_assertion_names() == ctx.end_assertion_names()); + SASSERT(ctx.assertion_names().empty()); } } diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 231dca0d3..8bea46bea 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -332,10 +332,8 @@ public: private: void set_background(cmd_context& ctx) { datalog::context& dlctx = m_dl_ctx->dlctx(); - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - for (; it != end; ++it) { - dlctx.assert_expr(*it); + for (expr * e : ctx.assertions()) { + dlctx.assert_expr(e); } } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8741ec419..ff37bfa95 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -79,13 +79,13 @@ namespace opt { m_hard.push_back(hard); } - bool context::scoped_state::set(ptr_vector & hard) { + bool context::scoped_state::set(expr_ref_vector const & hard) { bool eq = hard.size() == m_hard.size(); for (unsigned i = 0; eq && i < hard.size(); ++i) { - eq = hard[i] == m_hard[i].get(); + eq = hard.get(i) == m_hard.get(i); } m_hard.reset(); - m_hard.append(hard.size(), hard.c_ptr()); + m_hard.append(hard); return !eq; } @@ -177,7 +177,7 @@ namespace opt { r.append(m_core); } - void context::set_hard_constraints(ptr_vector& fmls) { + void context::set_hard_constraints(expr_ref_vector const& fmls) { if (m_scoped_state.set(fmls)) { clear_state(); } @@ -803,7 +803,20 @@ namespace opt { fmls.reset(); expr_ref tmp(m); for (unsigned i = 0; i < r->size(); ++i) { - fmls.push_back(r->form(i)); + if (asms.empty()) { + fmls.push_back(r->form(i)); + continue; + } + + ptr_vector deps; + expr_dependency_ref core(r->dep(i), m); + m.linearize(core, deps); + if (!deps.empty()) { + fmls.push_back(m.mk_implies(m.mk_and(deps.size(), deps.c_ptr()), r->form(i))); + } + else { + fmls.push_back(r->form(i)); + } } if (r->inconsistent()) { ptr_vector core_elems; diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index f57e937ba..fe0d4a13e 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -133,7 +133,7 @@ namespace opt { void push(); void pop(); void add(expr* hard); - bool set(ptr_vector & hard); + bool set(expr_ref_vector const& hard); unsigned add(expr* soft, rational const& weight, symbol const& id); unsigned add(app* obj, bool is_max); unsigned get_index(symbol const& id) { return m_indices[id]; } @@ -187,7 +187,7 @@ namespace opt { void push() override; void pop(unsigned n) override; bool empty() override { return m_scoped_state.m_objectives.empty(); } - void set_hard_constraints(ptr_vector & hard) override; + void set_hard_constraints(expr_ref_vector const& hard) override; lbool optimize(expr_ref_vector const& asms) override; void set_model(model_ref& _m) override { m_model = _m; } void get_model_core(model_ref& _m) override; diff --git a/src/parsers/smt2/marshal.cpp b/src/parsers/smt2/marshal.cpp index 11244760a..327414300 100644 --- a/src/parsers/smt2/marshal.cpp +++ b/src/parsers/smt2/marshal.cpp @@ -36,11 +36,12 @@ std::string marshal(expr_ref e, ast_manager &m) { expr_ref unmarshal(std::istream &is, ast_manager &m) { cmd_context ctx(false, &m); ctx.set_ignore_check(true); - if (!parse_smt2_commands(ctx, is)) { return expr_ref(nullptr, m); } + if (!parse_smt2_commands(ctx, is)) { + return expr_ref(nullptr, m); + } - ptr_vector::const_iterator it = ctx.begin_assertions(); - ptr_vector::const_iterator end = ctx.end_assertions(); - unsigned size = static_cast(end - it); + ptr_vector::const_iterator it = ctx.assertions().begin(); + unsigned size = ctx.assertions().size(); return expr_ref(mk_and(m, size, it), m); }