From 74621e0b7d366bd83c1b88ea3aba64a5f17d57b4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 11 Jun 2018 23:28:50 -0700
Subject: [PATCH] first eufi example running
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_solver.cpp | 22 +++++++-------
src/cmd_context/basic_cmds.cpp | 2 +-
src/muz/spacer/spacer_iuc_solver.cpp | 12 ++------
src/muz/spacer/spacer_iuc_solver.h | 9 ++++--
src/muz/spacer/spacer_prop_solver.cpp | 2 +-
src/opt/maxres.cpp | 13 ++++----
src/opt/opt_context.cpp | 2 +-
src/opt/opt_context.h | 2 +-
src/opt/opt_solver.cpp | 3 +-
src/opt/opt_solver.h | 2 +-
src/qe/qe_mbi.cpp | 13 ++------
src/qe/qe_term_graph.cpp | 6 ++--
src/sat/sat_solver/inc_sat_solver.cpp | 2 +-
src/smt/smt_context.cpp | 14 ++++-----
src/smt/smt_solver.cpp | 14 ++++-----
src/solver/check_sat_result.cpp | 6 ++--
src/solver/check_sat_result.h | 9 ++----
src/solver/combined_solver.cpp | 2 +-
src/solver/mus.cpp | 30 ++++++-------------
src/solver/mus.h | 2 --
src/solver/solver2tactic.cpp | 2 +-
src/solver/solver_pool.cpp | 6 ++--
src/solver/tactic2solver.cpp | 4 +--
.../portfolio/bounded_int2bv_solver.cpp | 2 +-
src/tactic/portfolio/enum2bv_solver.cpp | 2 +-
src/tactic/portfolio/pb2bv_solver.cpp | 2 +-
26 files changed, 80 insertions(+), 105 deletions(-)
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 657ff025c..ad5e7731d 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -460,12 +460,12 @@ extern "C" {
LOG_Z3_solver_get_unsat_core(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
- ptr_vector<expr> core;
+ expr_ref_vector core(mk_c(c)->m());
to_solver_ref(s)->get_unsat_core(core);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
mk_c(c)->save_object(v);
- for (unsigned i = 0; i < core.size(); i++) {
- v->m_ast_vector.push_back(core[i]);
+ for (expr* e : core) {
+ v->m_ast_vector.push_back(e);
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(nullptr);
@@ -537,23 +537,23 @@ extern "C" {
expr_ref_vector _assumptions(m), _consequences(m), _variables(m);
ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions);
unsigned sz = __assumptions.size();
- for (unsigned i = 0; i < sz; ++i) {
- if (!is_expr(__assumptions[i])) {
+ for (ast* e : __assumptions) {
+ if (!is_expr(e)) {
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
SET_ERROR_CODE(Z3_INVALID_USAGE);
return Z3_L_UNDEF;
}
- _assumptions.push_back(to_expr(__assumptions[i]));
+ _assumptions.push_back(to_expr(e));
}
ast_ref_vector const& __variables = to_ast_vector_ref(variables);
sz = __variables.size();
- for (unsigned i = 0; i < sz; ++i) {
- if (!is_expr(__variables[i])) {
+ for (ast* a : __variables) {
+ if (!is_expr(a)) {
_assumptions.finalize(); _consequences.finalize(); _variables.finalize();
SET_ERROR_CODE(Z3_INVALID_USAGE);
return Z3_L_UNDEF;
}
- _variables.push_back(to_expr(__variables[i]));
+ _variables.push_back(to_expr(a));
}
lbool result = l_undef;
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
@@ -578,8 +578,8 @@ extern "C" {
if (result == l_undef) {
to_solver_ref(s)->set_reason_unknown(eh);
}
- for (unsigned i = 0; i < _consequences.size(); ++i) {
- to_ast_vector_ref(consequences).push_back(_consequences[i].get());
+ for (expr* e : _consequences) {
+ to_ast_vector_ref(consequences).push_back(e);
}
return static_cast<Z3_lbool>(result);
Z3_CATCH_RETURN(Z3_L_UNDEF);
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 1d8fdb3de..4e5202fd8 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -223,7 +223,7 @@ ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it
});
static void print_core(cmd_context& ctx) {
- ptr_vector<expr> core;
+ expr_ref_vector core(ctx.m());
ctx.get_check_sat_result()->get_unsat_core(core);
ctx.regular_stream() << "(";
bool first = true;
diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp
index a0bc2a627..6d824a1f2 100644
--- a/src/muz/spacer/spacer_iuc_solver.cpp
+++ b/src/muz/spacer/spacer_iuc_solver.cpp
@@ -215,10 +215,11 @@ void iuc_solver::reset_statistics ()
m_learn_core_sw.reset();
}
-void iuc_solver::get_unsat_core (ptr_vector<expr> &core)
+void iuc_solver::get_unsat_core (expr_ref_vector &core)
{
m_solver.get_unsat_core (core);
- undo_proxies_in_core (core);
+ ptr_vector<expr> _core(core.size(), core.c_ptr());
+ undo_proxies_in_core (_core);
}
void iuc_solver::undo_proxies_in_core (ptr_vector<expr> &r)
{
@@ -258,13 +259,6 @@ void iuc_solver::undo_proxies (expr_ref_vector &r)
}
}
-void iuc_solver::get_unsat_core (expr_ref_vector &_core)
-{
- ptr_vector<expr> core;
- get_unsat_core (core);
- _core.append (core.size (), core.c_ptr ());
-}
-
void iuc_solver::elim_proxies (expr_ref_vector &v)
{
expr_ref f = mk_and (v);
diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h
index 0195ea134..3c6251be0 100644
--- a/src/muz/spacer/spacer_iuc_solver.h
+++ b/src/muz/spacer/spacer_iuc_solver.h
@@ -92,7 +92,6 @@ public:
~iuc_solver() override {}
/* iuc solver specific */
- void get_unsat_core(expr_ref_vector &core) override;
virtual void get_iuc(expr_ref_vector &core);
void set_split_literals(bool v) { m_split_literals = v; }
bool mk_proxies(expr_ref_vector &v, unsigned from = 0);
@@ -102,7 +101,11 @@ public:
void pop_bg(unsigned n);
unsigned get_num_bg();
- void get_full_unsat_core(ptr_vector<expr> &core) { m_solver.get_unsat_core(core); }
+ void get_full_unsat_core(ptr_vector<expr> &core) {
+ expr_ref_vector _core(m);
+ m_solver.get_unsat_core(_core);
+ core.append(_core.size(), _core.c_ptr());
+ }
/* solver interface */
@@ -142,7 +145,7 @@ public:
void collect_statistics(statistics &st) const override ;
virtual void reset_statistics();
- void get_unsat_core(ptr_vector<expr> &r) override;
+ void get_unsat_core(expr_ref_vector &r) override;
void get_model_core(model_ref &m) override {m_solver.get_model(m);}
proof *get_proof() override {return m_solver.get_proof();}
std::string reason_unknown() const override { return m_solver.reason_unknown(); }
diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index 64f1bfc9a..435f0af3a 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -245,7 +245,7 @@ lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,
soft.reset();
expr_ref saved(m);
- ptr_vector<expr> core;
+ expr_ref_vector core(m);
m_ctx->get_unsat_core(core);
// while there are soft constraints
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index d49044d8d..e86b20820 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -88,7 +88,7 @@ private:
expr_ref_vector m_asms;
expr_ref_vector m_defs;
obj_map<expr, rational> m_asm2weight;
- ptr_vector<expr> m_new_core;
+ expr_ref_vector m_new_core;
mus m_mus;
expr_ref_vector m_trail;
strategy_t m_st;
@@ -119,6 +119,7 @@ public:
maxsmt_solver_base(c, ws, soft),
m_index(index),
m_B(m), m_asms(m), m_defs(m),
+ m_new_core(m),
m_mus(c.get_solver()),
m_trail(m),
m_st(st),
@@ -351,11 +352,13 @@ public:
exprs core;
while (is_sat == l_false) {
core.reset();
- s().get_unsat_core(core);
- // verify_core(core);
+ expr_ref_vector _core(m);
+ s().get_unsat_core(_core);
model_ref mdl;
get_mus_model(mdl);
- is_sat = minimize_core(core);
+ is_sat = minimize_core(_core);
+ core.append(_core.size(), _core.c_ptr());
+ // verify_core(core);
++m_stats.m_num_cores;
if (is_sat != l_true) {
IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";);
@@ -538,7 +541,7 @@ public:
return nullptr != mdl.get();
}
- lbool minimize_core(exprs& core) {
+ lbool minimize_core(expr_ref_vector& core) {
if (core.empty()) {
return l_true;
}
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2850dd59c..37dbd0817 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -172,7 +172,7 @@ namespace opt {
r.append(m_labels);
}
- void context::get_unsat_core(ptr_vector<expr> & r) {
+ void context::get_unsat_core(expr_ref_vector & r) {
throw default_exception("Unsat cores are not supported with optimization");
}
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 29b327855..1172e68b6 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -195,7 +195,7 @@ namespace opt {
void collect_statistics(statistics& stats) const override;
proof* get_proof() override { return nullptr; }
void get_labels(svector<symbol> & r) override;
- void get_unsat_core(ptr_vector<expr> & r) override;
+ void get_unsat_core(expr_ref_vector & r) override;
std::string reason_unknown() const override;
void set_reason_unknown(char const* msg) override { m_unknown = msg; }
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 1a6587585..ca0474314 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -294,7 +294,8 @@ namespace opt {
return r;
}
- void opt_solver::get_unsat_core(ptr_vector<expr> & r) {
+ void opt_solver::get_unsat_core(expr_ref_vector & r) {
+ r.reset();
unsigned sz = m_context.get_unsat_core_size();
for (unsigned i = 0; i < sz; i++) {
r.push_back(m_context.get_unsat_core_expr(i));
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 7ffb531be..39562ec54 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -96,7 +96,7 @@ namespace opt {
void push_core() override;
void pop_core(unsigned n) override;
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override;
- void get_unsat_core(ptr_vector<expr> & r) override;
+ void get_unsat_core(expr_ref_vector & r) override;
void get_model_core(model_ref & _m) override;
proof * get_proof() override;
std::string reason_unknown() const override;
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 298a1da99..31b6001ea 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -30,19 +30,12 @@ Revision History:
namespace qe {
lbool mbi_plugin::check(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) {
- ast_manager& m = lits.get_manager();
- expr_ref_vector lits0(lits);
while (true) {
- lits.reset();
- lits.append(lits0);
switch ((*this)(vars, lits, mdl)) {
case mbi_sat:
return l_true;
case mbi_unsat:
- if (lits.empty()) return l_false;
- TRACE("qe", tout << "block: " << lits << "\n";);
- block(lits);
- break;
+ return l_false;
case mbi_undef:
return l_undef;
case mbi_augment:
@@ -113,8 +106,7 @@ namespace qe {
m(s->get_manager()),
m_atoms(m),
m_solver(s),
- m_dual_solver(sNot)
- {
+ m_dual_solver(sNot) {
params_ref p;
p.set_bool("core.minimize", true);
m_solver->updt_params(p);
@@ -256,6 +248,7 @@ namespace qe {
case l_true:
return l_true;
case l_false:
+ std::cout << lits << "\n";
a.block(lits);
itps.push_back(mk_not(mk_and(lits)));
break;
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index 084391368..2fa652828 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -701,7 +701,7 @@ namespace qe {
}
void solve() {
- ptr_vector<term> worklist;
+ ptr_vector<term> worklist;
for (term * t : m_tg.m_terms) {
// skip pure terms
if (m_term2app.contains(t->get_id())) continue;
@@ -785,8 +785,7 @@ namespace qe {
do {
expr* member = mk_pure(*r);
SASSERT(member);
- if (!members.contains(member) &&
- (!is_projected(*r) || !is_solved_eq(rep, member))) {
+ if (!members.contains(member) && (!is_projected(*r) || !is_solved_eq(rep, member))) {
res.push_back(m.mk_eq(rep, member));
members.insert(member);
}
@@ -814,6 +813,7 @@ namespace qe {
return mk_equalities(false, res);
}
+ // TBD: generalize for also the case of a (:var n)
bool is_solved_eq(expr *_lhs, expr* _rhs) {
if (!is_app(_lhs) || !is_app(_rhs)) return false;
app *lhs, *rhs;
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index e1e0e0b0a..8b7e2e63c 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -299,7 +299,7 @@ public:
if (m_preprocess) m_preprocess->collect_statistics(st);
m_solver.collect_statistics(st);
}
- void get_unsat_core(ptr_vector<expr> & r) override {
+ void get_unsat_core(expr_ref_vector & r) override {
r.reset();
r.append(m_core.size(), m_core.c_ptr());
}
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index bc5814186..0bc21d627 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3258,7 +3258,7 @@ namespace smt {
m_assumptions.reset();
}
- lbool context::mk_unsat_core(lbool r) {
+ lbool context::mk_unsat_core(lbool r) {
if (r != l_false) return r;
SASSERT(inconsistent());
if (!tracking_assumptions()) {
@@ -3276,18 +3276,16 @@ namespace smt {
SASSERT(m_literal2assumption.contains(l.index()));
if (!already_found_assumptions.contains(l.index())) {
already_found_assumptions.insert(l.index());
- m_unsat_core.push_back(m_literal2assumption[l.index()]);
+ expr* orig_assumption = m_literal2assumption[l.index()];
+ m_unsat_core.push_back(orig_assumption);
+ TRACE("assumptions", tout << l << ": " << mk_pp(orig_assumption, m_manager) << "\n";);
}
}
reset_assumptions();
pop_to_base_lvl(); // undo the push_scope() performed by init_assumptions
m_search_lvl = m_base_lvl;
std::sort(m_unsat_core.c_ptr(), m_unsat_core.c_ptr() + m_unsat_core.size(), ast_lt_proc());
- TRACE("unsat_core_bug", tout << "unsat core:\n";
- unsigned sz = m_unsat_core.size();
- for (unsigned i = 0; i < sz; i++) {
- tout << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
- });
+ TRACE("unsat_core_bug", tout << "unsat core:\n" << m_unsat_core << "\n";);
validate_unsat_core();
// theory validation of unsat core
for (theory* th : m_theory_set) {
@@ -3403,7 +3401,6 @@ namespace smt {
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel, bool already_did_theory_assumptions) {
if (!check_preamble(reset_cancel)) return l_undef;
- TRACE("before_search", display(tout););
SASSERT(at_base_level());
setup_context(false);
expr_ref_vector asms(m_manager, num_assumptions, assumptions);
@@ -3412,6 +3409,7 @@ namespace smt {
TRACE("unsat_core_bug", tout << asms << "\n";);
internalize_assertions();
init_assumptions(asms);
+ TRACE("before_search", display(tout););
lbool r = search();
r = mk_unsat_core(r);
r = check_finalize(r);
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index b0a8153a5..48f6053fc 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -209,7 +209,7 @@ namespace smt {
}
};
- void get_unsat_core(ptr_vector<expr> & r) override {
+ void get_unsat_core(expr_ref_vector & r) override {
unsigned sz = m_context.get_unsat_core_size();
for (unsigned i = 0; i < sz; i++) {
r.push_back(m_context.get_unsat_core_expr(i));
@@ -219,7 +219,7 @@ namespace smt {
scoped_minimize_core scm(*this);
mus mus(*this);
mus.add_soft(r.size(), r.c_ptr());
- ptr_vector<expr> r2;
+ expr_ref_vector r2(m);
if (l_true == mus.get_mus(r2)) {
r.reset();
r.append(r2);
@@ -333,7 +333,7 @@ namespace smt {
for_each_expr(p, visited, e);
}
- void compute_assrtn_fds(ptr_vector<expr> & core, vector<func_decl_set> & assrtn_fds) {
+ void compute_assrtn_fds(expr_ref_vector & core, vector<func_decl_set> & assrtn_fds) {
assrtn_fds.resize(m_name2assertion.size());
unsigned i = 0;
for (auto & kv : m_name2assertion) {
@@ -354,7 +354,7 @@ namespace smt {
return false;
}
- void add_pattern_literals_to_core(ptr_vector<expr> & core) {
+ void add_pattern_literals_to_core(expr_ref_vector & core) {
ast_manager & m = get_manager();
expr_ref_vector new_core_literals(m);
@@ -413,7 +413,7 @@ namespace smt {
for_each_expr(p, visited, e);
}
- void add_nonlocal_pattern_literals_to_core(ptr_vector<expr> & core) {
+ void add_nonlocal_pattern_literals_to_core(expr_ref_vector & core) {
ast_manager & m = get_manager();
for (auto const& kv : m_name2assertion) {
expr_ref name(kv.m_key, m);
@@ -425,8 +425,8 @@ namespace smt {
collect_body_func_decls(assrtn, body_fds);
for (func_decl *fd : pattern_fds) {
- if (!body_fds.contains(fd)) {
- core.insert(name);
+ if (!body_fds.contains(fd) && !core.contains(name)) {
+ core.push_back(name);
break;
}
}
diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp
index 0d3c112b3..28e6afeca 100644
--- a/src/solver/check_sat_result.cpp
+++ b/src/solver/check_sat_result.cpp
@@ -48,9 +48,11 @@ void simple_check_sat_result::collect_statistics(statistics & st) const {
st.copy(m_stats);
}
-void simple_check_sat_result::get_unsat_core(ptr_vector<expr> & r) {
- if (m_status == l_false)
+void simple_check_sat_result::get_unsat_core(expr_ref_vector & r) {
+ if (m_status == l_false) {
+ r.reset();
r.append(m_core.size(), m_core.c_ptr());
+ }
}
void simple_check_sat_result::get_model_core(model_ref & m) {
diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h
index 762735b8d..7e698b806 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -50,12 +50,7 @@ public:
lbool set_status(lbool r) { return m_status = r; }
lbool status() const { return m_status; }
virtual void collect_statistics(statistics & st) const = 0;
- virtual void get_unsat_core(ptr_vector<expr> & r) = 0;
- virtual void get_unsat_core(expr_ref_vector & r) {
- ptr_vector<expr> core;
- get_unsat_core(core);
- r.append(core.size(), core.c_ptr());
- }
+ virtual void get_unsat_core(expr_ref_vector & r) = 0;
void set_model_converter(model_converter* mc) { m_mc0 = mc; }
model_converter* mc0() const { return m_mc0.get(); }
virtual void get_model_core(model_ref & m) = 0;
@@ -87,7 +82,7 @@ struct simple_check_sat_result : public check_sat_result {
~simple_check_sat_result() override;
ast_manager& get_manager() const override { return m_proof.get_manager(); }
void collect_statistics(statistics & st) const override;
- void get_unsat_core(ptr_vector<expr> & r) override;
+ void get_unsat_core(expr_ref_vector & r) override;
void get_model_core(model_ref & m) override;
proof * get_proof() override;
std::string reason_unknown() const override;
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index a47302f5d..ad166d425 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -298,7 +298,7 @@ public:
m_solver1->collect_statistics(st);
}
- void get_unsat_core(ptr_vector<expr> & r) override {
+ void get_unsat_core(expr_ref_vector & r) override {
if (m_use_solver1_results)
m_solver1->get_unsat_core(r);
else
diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp
index a7925f268..b3d6c9ad9 100644
--- a/src/solver/mus.cpp
+++ b/src/solver/mus.cpp
@@ -64,7 +64,6 @@ struct mus::imp {
}
void add_assumption(expr* lit) {
- SASSERT(is_literal(lit));
m_assumptions.push_back(lit);
}
@@ -78,17 +77,9 @@ struct mus::imp {
return get_mus1(mus);
}
- lbool get_mus(ptr_vector<expr>& mus) {
- mus.reset();
- expr_ref_vector result(m);
- lbool r = get_mus(result);
- mus.append(result.size(), result.c_ptr());
- return r;
- }
-
lbool get_mus1(expr_ref_vector& mus) {
ptr_vector<expr> unknown(m_lit2expr.size(), m_lit2expr.c_ptr());
- ptr_vector<expr> core_exprs;
+ expr_ref_vector core_exprs(m);
TRACE("mus", m_solver.display(tout););
while (!unknown.empty()) {
IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";);
@@ -116,12 +107,12 @@ struct mus::imp {
if (!core_exprs.contains(not_lit)) {
// unknown := core_exprs \ mus
unknown.reset();
- for (unsigned i = 0; i < core_exprs.size(); ++i) {
- if (!mus.contains(core_exprs[i])) {
- unknown.push_back(core_exprs[i]);
+ for (expr* c : core_exprs) {
+ if (!mus.contains(c)) {
+ unknown.push_back(c);
}
}
- TRACE("mus", display_vec(tout << "core exprs:", core_exprs);
+ TRACE("mus", tout << "core exprs:" << core_exprs << "\n";
display_vec(tout << "core:", unknown);
display_vec(tout << "mus:", mus);
);
@@ -242,11 +233,11 @@ struct mus::imp {
void get_core(expr_set& core) {
core.reset();
- ptr_vector<expr> core_exprs;
+ expr_ref_vector core_exprs(m);
m_solver.get_unsat_core(core_exprs);
- for (unsigned i = 0; i < core_exprs.size(); ++i) {
- if (m_expr2lit.contains(core_exprs[i])) {
- core.insert(core_exprs[i]);
+ for (expr* c : core_exprs) {
+ if (m_expr2lit.contains(c)) {
+ core.insert(c);
}
}
}
@@ -375,9 +366,6 @@ void mus::add_assumption(expr* lit) {
return m_imp->add_assumption(lit);
}
-lbool mus::get_mus(ptr_vector<expr>& mus) {
- return m_imp->get_mus(mus);
-}
lbool mus::get_mus(expr_ref_vector& mus) {
return m_imp->get_mus(mus);
diff --git a/src/solver/mus.h b/src/solver/mus.h
index f2e543f04..807b07873 100644
--- a/src/solver/mus.h
+++ b/src/solver/mus.h
@@ -47,8 +47,6 @@ class mus {
*/
void add_assumption(expr* lit);
- lbool get_mus(ptr_vector<expr>& mus);
-
lbool get_mus(expr_ref_vector& mus);
void reset();
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
index 68d4b11f6..3c4f291a5 100644
--- a/src/solver/solver2tactic.cpp
+++ b/src/solver/solver2tactic.cpp
@@ -134,7 +134,7 @@ public:
in->set(proof2proof_converter(m, pr));
}
if (in->unsat_core_enabled()) {
- ptr_vector<expr> core;
+ expr_ref_vector core(m);
local_solver->get_unsat_core(core);
for (expr* c : core) {
lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(c)));
diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp
index 1d0fd0c11..9dacfb5ce 100644
--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@@ -83,12 +83,12 @@ public:
unsigned get_num_assertions() const override { return m_base->get_num_assertions(); }
expr * get_assertion(unsigned idx) const override { return m_base->get_assertion(idx); }
- void get_unsat_core(ptr_vector<expr> & r) override {
+ void get_unsat_core(expr_ref_vector& r) override {
m_base->get_unsat_core(r);
unsigned j = 0;
for (unsigned i = 0; i < r.size(); ++i)
- if (m_pred != r[i])
- r[j++] = r[i];
+ if (m_pred != r.get(i))
+ r[j++] = r.get(i);
r.shrink(j);
}
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 9118bb658..94509e3f6 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -62,7 +62,7 @@ public:
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override;
void collect_statistics(statistics & st) const override;
- void get_unsat_core(ptr_vector<expr> & r) override;
+ void get_unsat_core(expr_ref_vector & r) override;
void get_model_core(model_ref & m) override;
proof * get_proof() override;
std::string reason_unknown() const override;
@@ -219,7 +219,7 @@ void tactic2solver::collect_statistics(statistics & st) const {
//SASSERT(m_stats.size() > 0);
}
-void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
+void tactic2solver::get_unsat_core(expr_ref_vector & r) {
if (m_result.get()) {
m_result->get_unsat_core(r);
}
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index 8767644f3..6389ed739 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -148,7 +148,7 @@ public:
void set_produce_models(bool f) override { m_solver->set_produce_models(f); }
void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback); }
void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); }
- void get_unsat_core(ptr_vector<expr> & r) override { m_solver->get_unsat_core(r); }
+ void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
void get_model_core(model_ref & mdl) override {
m_solver->get_model(mdl);
if (mdl) {
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 6b5fe9056..29c6aeb39 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -88,7 +88,7 @@ public:
void set_produce_models(bool f) override { m_solver->set_produce_models(f); }
void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback); }
void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); }
- void get_unsat_core(ptr_vector<expr> & r) override { m_solver->get_unsat_core(r); }
+ void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
void get_model_core(model_ref & mdl) override {
m_solver->get_model(mdl);
if (mdl) {
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index f8794ca41..60ca6a5dc 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -87,7 +87,7 @@ public:
m_rewriter.collect_statistics(st);
m_solver->collect_statistics(st);
}
- void get_unsat_core(ptr_vector<expr> & r) override { m_solver->get_unsat_core(r); }
+ void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); }
void get_model_core(model_ref & mdl) override {
m_solver->get_model(mdl);
if (mdl) {