mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix #1577 again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
44a0dbbc61
commit
c4829dfa22
|
@ -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);
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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());
|
||||
}
|
||||
|
|
|
@ -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); );
|
||||
}
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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());
|
||||
}
|
||||
}
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue