diff --git a/contrib/cmake/src/opt/CMakeLists.txt b/contrib/cmake/src/opt/CMakeLists.txt
index c50f8be52..e4166e3d4 100644
--- a/contrib/cmake/src/opt/CMakeLists.txt
+++ b/contrib/cmake/src/opt/CMakeLists.txt
@@ -8,7 +8,6 @@ z3_add_component(opt
maxsls.cpp
maxsmt.cpp
mss.cpp
- mus.cpp
opt_cmds.cpp
opt_context.cpp
opt_pareto.cpp
diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/contrib/cmake/src/solver/CMakeLists.txt
index 5e76c91ce..8142ca872 100644
--- a/contrib/cmake/src/solver/CMakeLists.txt
+++ b/contrib/cmake/src/solver/CMakeLists.txt
@@ -2,6 +2,7 @@ z3_add_component(solver
SOURCES
check_sat_result.cpp
combined_solver.cpp
+ mus.cpp
solver.cpp
solver_na2as.cpp
tactic2solver.cpp
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 7c1fad80e..741bab4b5 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -119,7 +119,7 @@ public:
maxsmt_solver_base(c, ws, soft),
m_index(index),
m_B(m), m_asms(m), m_defs(m),
- m_mus(c.get_solver(), m),
+ m_mus(c.get_solver()),
m_mss(c.get_solver(), m),
m_trail(m),
m_st(st),
diff --git a/src/opt/mus.h b/src/opt/mus.h
deleted file mode 100644
index 8ca7ab91d..000000000
--- a/src/opt/mus.h
+++ /dev/null
@@ -1,55 +0,0 @@
-/*++
-Copyright (c) 2014 Microsoft Corporation
-
-Module Name:
-
- mus.h
-
-Abstract:
-
- Basic MUS extraction
-
-Author:
-
- Nikolaj Bjorner (nbjorner) 2014-20-7
-
-Notes:
-
---*/
-#ifndef MUS_H_
-#define MUS_H_
-
-namespace opt {
- class mus {
- struct imp;
- imp * m_imp;
- public:
- mus(solver& s, ast_manager& m);
- ~mus();
- /**
- Add soft constraint.
-
- Assume that the solver context enforces that
- cls is equivalent to a disjunction of args.
- Assume also that cls is a literal.
- */
- unsigned add_soft(expr* cls);
-
- lbool get_mus(unsigned_vector& mus);
-
- void reset();
-
- /**
- Instrument MUS extraction to also provide the minimal
- penalty model, if any is found.
- The minimal penalty model has the least weight for the
- supplied soft constraints.
- */
- void set_soft(unsigned sz, expr* const* soft, rational const* weights);
- rational get_best_model(model_ref& mdl);
-
- };
-
-};
-
-#endif
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index a9ca9e99d..4c6efdcd4 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -34,7 +34,9 @@ Notes:
#include "expr_replacer.h"
#include "th_rewriter.h"
#include "model_evaluator.h"
-
+#include "smt_solver.h"
+#include "solver.h"
+#include "mus.h"
namespace qe {
@@ -506,33 +508,58 @@ namespace qe {
}
class kernel {
- smt_params m_smtp;
- smt::kernel m_kernel;
+ ast_manager& m;
+ params_ref m_params;
+ ref<solver> m_solver;
public:
kernel(ast_manager& m):
- m_kernel(m, m_smtp)
+ m(m),
+ m_solver(mk_smt_solver(m, m_params, symbol::null))
{
- m_smtp.m_model = true;
- m_smtp.m_relevancy_lvl = 0;
- m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE;
+ m_params.set_bool("model", true);
+ m_params.set_uint("relevancy_lvl", 0);
+ m_params.set_uint("case_split_strategy", CS_ACTIVITY_WITH_CACHE);
+ m_solver->updt_params(m_params);
}
- smt::kernel& k() { return m_kernel; }
- smt::kernel const& k() const { return m_kernel; }
+ solver& s() { return *m_solver; }
+ solver const& s() const { return *m_solver; }
+
+ void reset() {
+ m_solver = mk_smt_solver(m, m_params, symbol::null);
+ }
void assert_expr(expr* e) {
- m_kernel.assert_expr(e);
+ m_solver->assert_expr(e);
}
+ ptr_vector<expr> m_core;
+
void get_core(expr_ref_vector& core) {
- unsigned sz = m_kernel.get_unsat_core_size();
core.reset();
- for (unsigned i = 0; i < sz; ++i) {
- core.push_back(m_kernel.get_unsat_core_expr(i));
+ m_core.reset();
+ m_solver->get_unsat_core(m_core);
+ core.append(m_core.size(), m_core.c_ptr());
+
+#if 0
+
+ mus mus(*m_solver);
+ for (unsigned i = 0; i < m_core.size(); ++i) {
+ VERIFY(i == mus.add_soft(m_core[i]));
}
+ unsigned_vector mus2;
+ core.reset();
+ if (mus.get_mus(mus2) != l_undef) {
+ for (unsigned i = 0; i < mus2.size(); ++i) {
+ core.push_back(m_core[mus2[i]]);
+ }
+ }
+ std::cout << m_core.size() << " => " << core.size() << "\n";
+#endif
+
TRACE("qe", tout << "core: " << core << "\n";
- m_kernel.display(tout);
+ m_solver->display(tout);
tout << "\n";
);
}
@@ -586,13 +613,13 @@ namespace qe {
expr_ref_vector asms(m_asms);
m_pred_abs.get_assumptions(m_model.get(), asms);
TRACE("qe", tout << asms << "\n";);
- smt::kernel& k = get_kernel(m_level).k();
- lbool res = k.check(asms);
+ solver& s = get_kernel(m_level).s();
+ lbool res = s.check_sat(asms);
switch (res) {
case l_true:
- k.get_model(m_model);
+ s.get_model(m_model);
SASSERT(validate_model(asms));
- TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
+ TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
push();
break;
case l_false:
@@ -655,8 +682,8 @@ namespace qe {
void reset() {
m_st.reset();
- m_fa.k().collect_statistics(m_st);
- m_ex.k().collect_statistics(m_st);
+ m_fa.s().collect_statistics(m_st);
+ m_ex.s().collect_statistics(m_st);
m_pred_abs.collect_statistics(m_st);
m_level = 0;
m_answer.reset();
@@ -664,8 +691,8 @@ namespace qe {
m_pred_abs.reset();
m_vars.reset();
m_model = 0;
- m_fa.k().reset();
- m_ex.k().reset();
+ m_fa.reset();
+ m_ex.reset();
m_free_vars.reset();
}
@@ -964,10 +991,12 @@ namespace qe {
bool validate_core(expr_ref_vector const& core) {
TRACE("qe", tout << "Validate core\n";);
- smt::kernel& k = get_kernel(m_level).k();
+ solver& s = get_kernel(m_level).s();
expr_ref_vector fmls(m);
fmls.append(core.size(), core.c_ptr());
- fmls.append(k.size(), k.get_formulas());
+ for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
+ fmls.push_back(s.get_assertion(i));
+ }
return check_fmls(fmls) || m.canceled();
}
@@ -985,10 +1014,14 @@ namespace qe {
bool validate_model(expr_ref_vector const& asms) {
TRACE("qe", tout << "Validate model\n";);
- smt::kernel& k = get_kernel(m_level).k();
+ solver& s = get_kernel(m_level).s();
+ expr_ref_vector fmls(m);
+ for (unsigned i = 0; i < s.get_num_assertions(); ++i) {
+ fmls.push_back(s.get_assertion(i));
+ }
return
validate_model(*m_model, asms.size(), asms.c_ptr()) &&
- validate_model(*m_model, k.size(), k.get_formulas());
+ validate_model(*m_model, fmls.size(), fmls.c_ptr());
}
bool validate_model(model& mdl, unsigned sz, expr* const* fmls) {
@@ -1161,9 +1194,9 @@ namespace qe {
break;
case l_undef:
result.push_back(in.get());
- std::string s = m_ex.k().last_failure_as_string();
- if (s == "ok") {
- s = m_fa.k().last_failure_as_string();
+ std::string s = m_ex.s().reason_unknown();
+ if (s == "ok" || s == "unknown") {
+ s = m_fa.s().reason_unknown();
}
throw tactic_exception(s.c_str());
}
@@ -1171,8 +1204,8 @@ namespace qe {
void collect_statistics(statistics & st) const {
st.copy(m_st);
- m_fa.k().collect_statistics(st);
- m_ex.k().collect_statistics(st);
+ m_fa.s().collect_statistics(st);
+ m_ex.s().collect_statistics(st);
m_pred_abs.collect_statistics(st);
st.update("qsat num rounds", m_stats.m_num_rounds);
m_pred_abs.collect_statistics(st);
@@ -1180,8 +1213,8 @@ namespace qe {
void reset_statistics() {
m_stats.reset();
- m_fa.k().reset_statistics();
- m_ex.k().reset_statistics();
+ m_fa.reset();
+ m_ex.reset();
}
void cleanup() {
@@ -1223,9 +1256,9 @@ namespace qe {
UNREACHABLE();
break;
case l_undef:
- std::string s = m_ex.k().last_failure_as_string();
+ std::string s = m_ex.s().reason_unknown();
if (s == "ok") {
- s = m_fa.k().last_failure_as_string();
+ s = m_fa.s().reason_unknown();
}
throw tactic_exception(s.c_str());
diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h
index e6586d492..b981b3119 100644
--- a/src/solver/check_sat_result.h
+++ b/src/solver/check_sat_result.h
@@ -54,6 +54,7 @@ public:
virtual void set_reason_unknown(char const* msg) = 0;
virtual void get_labels(svector<symbol> & r) = 0;
virtual ast_manager& get_manager() = 0;
+
};
/**
diff --git a/src/opt/mus.cpp b/src/solver/mus.cpp
similarity index 55%
rename from src/opt/mus.cpp
rename to src/solver/mus.cpp
index aa8446256..ebdffca13 100644
--- a/src/opt/mus.cpp
+++ b/src/solver/mus.cpp
@@ -19,14 +19,11 @@ Notes:
--*/
#include "solver.h"
-#include "smt_literal.h"
#include "mus.h"
#include "ast_pp.h"
#include "ast_util.h"
+#include "uint_set.h"
-using namespace opt;
-
-//
struct mus::imp {
solver& m_s;
@@ -38,15 +35,14 @@ struct mus::imp {
vector<rational> m_weights;
rational m_weight;
- imp(solver& s, ast_manager& m):
- m_s(s), m(m), m_cls2expr(m), m_soft(m)
+ imp(solver& s):
+ m_s(s), m(s.get_manager()), m_cls2expr(m), m_soft(m)
{}
void reset() {
m_cls2expr.reset();
m_expr2cls.reset();
- }
-
+ }
unsigned add_soft(expr* cls) {
SASSERT(is_uninterp_const(cls) ||
@@ -55,7 +51,7 @@ struct mus::imp {
m_expr2cls.insert(cls, idx);
m_cls2expr.push_back(cls);
TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n";
- display_vec(tout, m_cls2expr););
+ display_vec(tout, m_cls2expr););
return idx;
}
@@ -70,11 +66,16 @@ struct mus::imp {
mus.push_back(core.back());
return l_true;
}
+
mus.reset();
+ if (core.size() > 64) {
+ return qx(mus);
+ }
+
expr_ref_vector assumptions(m);
ptr_vector<expr> core_exprs;
while (!core.empty()) {
- IF_VERBOSE(2, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
+ IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
unsigned cls_id = core.back();
TRACE("opt",
display_vec(tout << "core: ", core);
@@ -84,11 +85,12 @@ struct mus::imp {
expr* cls = m_cls2expr[cls_id].get();
expr_ref not_cls(m);
not_cls = mk_not(m, cls);
- unsigned sz = assumptions.size();
- assumptions.push_back(not_cls);
- add_core(core, assumptions);
- lbool is_sat = m_s.check_sat(assumptions.size(), assumptions.c_ptr());
- assumptions.resize(sz);
+ lbool is_sat = l_undef;
+ {
+ scoped_append _sa(*this, assumptions, core);
+ assumptions.push_back(not_cls);
+ is_sat = m_s.check_sat(assumptions);
+ }
switch (is_sat) {
case l_undef:
return is_sat;
@@ -132,6 +134,30 @@ struct mus::imp {
return l_true;
}
+ class scoped_append {
+ expr_ref_vector& m_fmls;
+ unsigned m_size;
+ public:
+ scoped_append(imp& imp, expr_ref_vector& fmls1, unsigned_vector const& fmls2):
+ m_fmls(fmls1),
+ m_size(fmls1.size()) {
+ for (unsigned i = 0; i < fmls2.size(); ++i) {
+ fmls1.push_back(imp.m_cls2expr[fmls2[i]].get());
+ }
+ }
+ scoped_append(imp& imp, expr_ref_vector& fmls1, uint_set const& fmls2):
+ m_fmls(fmls1),
+ m_size(fmls1.size()) {
+ uint_set::iterator it = fmls2.begin(), end = fmls2.end();
+ for (; it != end; ++it) {
+ fmls1.push_back(imp.m_cls2expr[*it].get());
+ }
+ }
+ ~scoped_append() {
+ m_fmls.shrink(m_size);
+ }
+ };
+
void add_core(unsigned_vector const& core, expr_ref_vector& assumptions) {
for (unsigned i = 0; i < core.size(); ++i) {
assumptions.push_back(m_cls2expr[core[i]].get());
@@ -193,10 +219,110 @@ struct mus::imp {
}
+ lbool qx(unsigned_vector& mus) {
+ uint_set core, support;
+ for (unsigned i = 0; i < m_cls2expr.size(); ++i) {
+ core.insert(i);
+ }
+ lbool is_sat = qx(core, support, false);
+ if (is_sat == l_true) {
+ uint_set::iterator it = core.begin(), end = core.end();
+ mus.reset();
+ for (; it != end; ++it) {
+ mus.push_back(*it);
+ }
+ }
+ return is_sat;
+ }
+
+ lbool qx(uint_set& assignment, uint_set& support, bool has_support) {
+ lbool is_sat = l_true;
+#if 0
+ if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
+ IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
+ return l_true;
+ }
+#endif
+ if (has_support) {
+ expr_ref_vector asms(m);
+ scoped_append _sa(*this, asms, support);
+ is_sat = m_s.check_sat(asms);
+ switch (is_sat) {
+ case l_false: {
+ uint_set core;
+ get_core(core);
+ support &= core;
+ assignment.reset();
+ return l_true;
+ }
+ case l_undef:
+ return l_undef;
+ case l_true:
+ update_model();
+ break;
+ default:
+ break;
+ }
+ }
+ if (assignment.num_elems() == 1) {
+ return l_true;
+ }
+ uint_set assign2;
+ split(assignment, assign2);
+ support |= assignment;
+ is_sat = qx(assign2, support, !assignment.empty());
+ unsplit(support, assignment);
+ if (is_sat != l_true) return is_sat;
+ support |= assign2;
+ is_sat = qx(assignment, support, !assign2.empty());
+ assignment |= assign2;
+ unsplit(support, assign2);
+ return is_sat;
+ }
+
+ void get_core(uint_set& core) {
+ ptr_vector<expr> core_exprs;
+ m_s.get_unsat_core(core_exprs);
+ for (unsigned i = 0; i < core_exprs.size(); ++i) {
+ expr* cls = core_exprs[i];
+ core.insert(m_expr2cls.find(cls));
+ }
+ }
+
+ void unsplit(uint_set& A, uint_set& B) {
+ uint_set A1, B1;
+ uint_set::iterator it = A.begin(), end = A.end();
+ for (; it != end; ++it) {
+ if (B.contains(*it)) {
+ B1.insert(*it);
+ }
+ else {
+ A1.insert(*it);
+ }
+ }
+ A = A1;
+ B = B1;
+ }
+
+ void split(uint_set& lits1, uint_set& lits2) {
+ unsigned half = lits1.num_elems()/2;
+ uint_set lits3;
+ uint_set::iterator it = lits1.begin(), end = lits1.end();
+ for (unsigned i = 0; it != end; ++it, ++i) {
+ if (i < half) {
+ lits3.insert(*it);
+ }
+ else {
+ lits2.insert(*it);
+ }
+ }
+ lits1 = lits3;
+ }
+
};
-mus::mus(solver& s, ast_manager& m) {
- m_imp = alloc(imp, s, m);
+mus::mus(solver& s) {
+ m_imp = alloc(imp, s);
}
mus::~mus() {
diff --git a/src/solver/mus.h b/src/solver/mus.h
new file mode 100644
index 000000000..d66049030
--- /dev/null
+++ b/src/solver/mus.h
@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+ mus.h
+
+Abstract:
+
+ Basic MUS extraction
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2014-20-7
+
+Notes:
+
+--*/
+#ifndef MUS_H_
+#define MUS_H_
+
+class mus {
+ struct imp;
+ imp * m_imp;
+ public:
+ mus(solver& s);
+ ~mus();
+ /**
+ Add soft constraint.
+
+ Assume that the solver context enforces that
+ cls is equivalent to a disjunction of args.
+ Assume also that cls is a literal.
+ */
+ unsigned add_soft(expr* cls);
+
+ lbool get_mus(unsigned_vector& mus);
+
+ void reset();
+
+ /**
+ Instrument MUS extraction to also provide the minimal
+ penalty model, if any is found.
+ The minimal penalty model has the least weight for the
+ supplied soft constraints.
+ */
+ void set_soft(unsigned sz, expr* const* soft, rational const* weights);
+
+ rational get_best_model(model_ref& mdl);
+
+};
+
+
+#endif
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 5a1514795..0b2578968 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -108,6 +108,10 @@ public:
*/
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
+ lbool check_sat(expr_ref_vector const& asms) { return check_sat(asms.size(), asms.c_ptr()); }
+
+ lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); }
+
/**
\brief Set a progress callback procedure that is invoked by this solver during check_sat.