From c4829dfa22978ff7c8041b4826721d67ae6d9250 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 6 Oct 2018 09:01:01 -0700
Subject: [PATCH] fix #1577 again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_datalog.cpp | 6 ++----
src/api/api_opt.cpp | 6 ++----
src/api/api_parsers.cpp | 6 ++----
src/api/api_solver.cpp | 6 ++----
src/ast/pattern/expr_pattern_match.cpp | 6 ++----
src/cmd_context/cmd_context.cpp | 20 ++++++++++++++------
src/cmd_context/cmd_context.h | 9 +++------
src/cmd_context/cmd_context_to_goal.cpp | 16 +++++++---------
src/muz/fp/dl_cmds.cpp | 6 ++----
src/opt/opt_context.cpp | 23 ++++++++++++++++++-----
src/opt/opt_context.h | 4 ++--
src/parsers/smt2/marshal.cpp | 9 +++++----
12 files changed, 61 insertions(+), 56 deletions(-)
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<expr>::const_iterator it = ctx.begin_assertions();
- ptr_vector<expr>::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<expr>::const_iterator it = ctx->begin_assertions();
- ptr_vector<expr>::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<expr>::const_iterator it = ctx->begin_assertions();
- ptr_vector<expr>::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<expr>::const_iterator it = ctx->begin_assertions();
- ptr_vector<expr>::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<expr>::const_iterator it = ctx.begin_assertions();
- ptr_vector<expr>::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<reslimit> eh(m().limit());
expr_ref r(m());
scoped_ctrl_c ctrlc(eh);
- ptr_vector<expr>::const_iterator it = begin_assertions();
- ptr_vector<expr>::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<expr> & 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<expr>::const_iterator begin_assertions() const { return m_assertions.begin(); }
- ptr_vector<expr>::const_iterator end_assertions() const { return m_assertions.end(); }
-
- ptr_vector<expr>::const_iterator begin_assertion_names() const { return m_assertion_names.begin(); }
- ptr_vector<expr>::const_iterator end_assertion_names() const { return m_assertion_names.end(); }
+ ptr_vector<expr> const& assertions() const { return m_assertions; }
+ ptr_vector<expr> 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<expr>::const_iterator it = ctx.begin_assertions();
- ptr_vector<expr>::const_iterator end = ctx.end_assertions();
- ptr_vector<expr>::const_iterator it2 = ctx.begin_assertion_names();
- SASSERT(end - it == ctx.end_assertion_names() - it2);
+ ptr_vector<expr>::const_iterator it = ctx.assertions().begin();
+ ptr_vector<expr>::const_iterator end = ctx.assertions().end();
+ ptr_vector<expr>::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<expr>::const_iterator it = ctx.begin_assertions();
- ptr_vector<expr>::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<expr>::const_iterator it = ctx.begin_assertions();
- ptr_vector<expr>::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<expr> & 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<expr>& 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<expr> 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<expr> 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<expr> & 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<expr> & 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<expr>::const_iterator it = ctx.begin_assertions();
- ptr_vector<expr>::const_iterator end = ctx.end_assertions();
- unsigned size = static_cast<unsigned>(end - it);
+ ptr_vector<expr>::const_iterator it = ctx.assertions().begin();
+ unsigned size = ctx.assertions().size();
return expr_ref(mk_and(m, size, it), m);
}