#include "util/debug.h"
#include "ast/rewriter/rewriter_types.h"
#include "ast/ast_util.h"
#include "ast/ast_ll_pp.h"
#include "smt/smt_kernel.h"
#include "params/smt_params.h"
#include "params/smt_params_helper.hpp"
#include "smt/smt_solver.h"
#include "tactic/tactic.h"
#include "tactic/tactical.h"
#include "ast/converters/generic_model_converter.h"
#include "solver/solver2tactic.h"
#include "solver/solver.h"
#include "solver/mus.h"
#include "solver/parallel_tactical.h"
#include "solver/parallel_params.hpp"
#include <mutex>
typedef obj_map<expr, expr *> expr2expr_map;
class smt_tactic : public tactic {
ast_manager& m;
smt_params m_params;
params_ref m_params_ref;
expr_ref_vector m_vars;
vector<std::pair<expr_ref, expr_ref>> m_values;
statistics m_stats;
std::atomic<smt::kernel*> m_ctx = nullptr;
symbol m_logic;
progress_callback* m_callback = nullptr;
bool m_candidate_models = false;
bool m_fail_if_inconclusive = false;
mutable std::mutex m_mutex;
public:
smt_tactic(ast_manager& m, params_ref const & p):
m(m),
m_params_ref(p),
m_vars(m) {
updt_params_core(p);
TRACE(smt_tactic, tout << "p: " << p << "\n";);
}
tactic * translate(ast_manager & m) override {
return alloc(smt_tactic, m, m_params_ref);
}
~smt_tactic() override {
SASSERT(m_ctx.load() == nullptr);
}
char const* name() const override { return "smt"; }
smt_params & fparams() {
return m_params;
}
params_ref & params() {
return m_params_ref;
}
void updt_params_core(params_ref const & p) {
smt_params_helper _p(p);
m_candidate_models = _p.candidate_models();
m_fail_if_inconclusive = p.get_bool("fail_if_inconclusive", true);
}
void updt_params(params_ref const & p) override {
TRACE(smt_tactic, tout << "updt_params: " << p << "\n";);
updt_params_core(p);
fparams().updt_params(p);
m_params_ref.copy(p);
m_logic = p.get_sym(symbol("logic"), m_logic);
if (m_logic != symbol::null && m_ctx.load()) {
m_ctx.load()->set_logic(m_logic);
}
SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
}
void collect_param_descrs(param_descrs & r) override {
r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal.");
smt_params_helper::collect_param_descrs(r);
}
void collect_statistics(statistics & st) const override {
if (m_ctx.load()) {
std::scoped_lock lock(m_mutex);
if (m_ctx.load()) {
m_ctx.load()->collect_statistics(st); return;
}
}
st.copy(m_stats);
}
void cleanup() override {
}
void reset_statistics() override {
m_stats.reset();
}
void set_logic(symbol const & l) override {
m_logic = l;
}
void set_progress_callback(progress_callback * callback) override {
m_callback = callback;
}
struct scoped_init_ctx {
smt_tactic & m_owner;
smt_params m_params; params_ref m_params_ref;
scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
m_params = o.fparams();
m_params_ref.reset();
m_params_ref.append(o.params());
smt::kernel * new_ctx = alloc(smt::kernel, m, m_params, m_params_ref);
TRACE(smt_tactic, tout << "logic: " << o.m_logic << "\n";);
new_ctx->set_logic(o.m_logic);
if (o.m_callback) {
new_ctx->set_progress_callback(o.m_callback);
}
o.m_ctx = new_ctx;
}
~scoped_init_ctx() {
smt::kernel* d = nullptr;
{
std::scoped_lock lock(m_owner.m_mutex);
d = m_owner.m_ctx.load();
m_owner.m_ctx = nullptr;
m_owner.m_user_ctx = nullptr;
}
if (d)
dealloc(d);
}
};
void handle_canceled(goal_ref const & in,
goal_ref_buffer & result) {
}
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
try {
IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";);
tactic_report report("smt", *in);
TRACE(smt_tactic, tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
<< " PREPROCESS: " << fparams().m_preprocess << "\n";
tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n";
tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
tout << "params_ref: " << m_params_ref << "\n";
tout << "nnf: " << fparams().m_nnf_cnf << "\n";);
TRACE(smt_tactic_params, m_params.display(tout););
TRACE(smt_tactic_detail, in->display(tout););
TRACE(smt_tactic_memory, tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
scoped_init_ctx init(*this, m);
SASSERT(m_ctx.load());
expr_ref_vector clauses(m);
expr2expr_map bool2dep;
ptr_vector<expr> assumptions;
ref<generic_model_converter> fmc;
if (in->unsat_core_enabled()) {
extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
TRACE(mus, in->display_with_dependencies(tout);
tout << clauses << "\n";);
if (in->proofs_enabled() && !assumptions.empty())
throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores");
for (unsigned i = 0; i < clauses.size(); ++i) {
m_ctx.load()->assert_expr(clauses[i].get());
}
}
else if (in->proofs_enabled()) {
unsigned sz = in->size();
for (unsigned i = 0; i < sz; ++i) {
m_ctx.load()->assert_expr(in->form(i), in->pr(i));
}
}
else {
unsigned sz = in->size();
for (unsigned i = 0; i < sz; ++i) {
m_ctx.load()->assert_expr(in->form(i));
}
}
if (m_ctx.load()->canceled()) {
throw tactic_exception(Z3_CANCELED_MSG);
}
user_propagate_delay_init();
lbool r;
try {
if (assumptions.empty() && !m_user_ctx)
r = m_ctx.load()->setup_and_check();
else
r = m_ctx.load()->check(assumptions.size(), assumptions.data());
}
catch(...) {
TRACE(smt_tactic, tout << "exception\n";);
m_ctx.load()->collect_statistics(m_stats);
throw;
}
m_ctx.load()->collect_statistics(m_stats);
proof_ref pr(m_ctx.load()->get_proof(), m);
TRACE(smt_tactic, tout << r << " " << pr << "\n";);
switch (r) {
case l_true: {
if (m_fail_if_inconclusive && !in->sat_preserved())
throw tactic_exception("over-approximated goal found to be sat");
in->reset();
result.push_back(in.get());
if (in->models_enabled()) {
model_ref md;
m_ctx.load()->get_model(md);
buffer<symbol> r;
m_ctx.load()->get_relevant_labels(nullptr, r);
labels_vec rv;
rv.append(r.size(), r.data());
model_converter_ref mc;
mc = model_and_labels2model_converter(md.get(), rv);
mc = concat(fmc.get(), mc.get());
in->add(mc.get());
}
if (m_ctx.load()->canceled())
throw tactic_exception(Z3_CANCELED_MSG);
return;
}
case l_false: {
if (m_fail_if_inconclusive && !in->unsat_preserved()) {
TRACE(smt_tactic, tout << "failed to show to be unsat...\n";);
throw tactic_exception("under-approximated goal found to be unsat");
}
in->reset();
expr_dependency * lcore = nullptr;
if (in->unsat_core_enabled()) {
unsigned sz = m_ctx.load()->get_unsat_core_size();
for (unsigned i = 0; i < sz; ++i) {
expr * b = m_ctx.load()->get_unsat_core_expr(i);
SASSERT(is_uninterp_const(b) && m.is_bool(b));
expr * d = bool2dep.find(b);
lcore = m.mk_join(lcore, m.mk_leaf(d));
}
}
if (m.proofs_enabled() && !pr) pr = m.mk_asserted(m.mk_false()); if (pr && m.get_fact(pr) != m.mk_false()) pr = m.mk_asserted(m.mk_false()); in->assert_expr(m.mk_false(), pr, lcore);
result.push_back(in.get());
return;
}
case l_undef:
if (m_ctx.load()->canceled() && !pr) {
throw tactic_exception(Z3_CANCELED_MSG);
}
if (m_fail_if_inconclusive && !m_candidate_models && !pr) {
std::stringstream strm;
strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx.load()->last_failure_as_string();
throw tactic_exception(strm.str());
}
result.push_back(in.get());
if (pr) {
in->reset();
in->assert_expr(m.get_fact(pr), pr, nullptr);
in->updt_prec(goal::UNDER_OVER);
}
if (m_candidate_models) {
switch (m_ctx.load()->last_failure()) {
case smt::NUM_CONFLICTS:
case smt::THEORY:
case smt::QUANTIFIERS:
if (in->models_enabled()) {
model_ref md;
m_ctx.load()->get_model(md);
buffer<symbol> r;
m_ctx.load()->get_relevant_labels(nullptr, r);
labels_vec rv;
rv.append(r.size(), r.data());
in->add(model_and_labels2model_converter(md.get(), rv));
}
return;
default:
break;
}
}
if (pr) {
return;
}
throw tactic_exception(m_ctx.load()->last_failure_as_string());
}
}
catch (rewriter_exception & ex) {
throw tactic_exception(ex.what());
}
}
void* m_user_ctx = nullptr;
user_propagator::push_eh_t m_push_eh;
user_propagator::pop_eh_t m_pop_eh;
user_propagator::fresh_eh_t m_fresh_eh;
user_propagator::fixed_eh_t m_fixed_eh;
user_propagator::final_eh_t m_final_eh;
user_propagator::eq_eh_t m_eq_eh;
user_propagator::eq_eh_t m_diseq_eh;
user_propagator::created_eh_t m_created_eh;
user_propagator::decide_eh_t m_decide_eh;
void* m_on_clause_ctx = nullptr;
user_propagator::on_clause_eh_t m_on_clause_eh;
void on_clause_delay_init() {
if (m_on_clause_eh)
m_ctx.load()->register_on_clause(m_on_clause_ctx, m_on_clause_eh);
}
void user_propagate_delay_init() {
if (!m_user_ctx)
return;
m_ctx.load()->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh);
if (m_fixed_eh) m_ctx.load()->user_propagate_register_fixed(m_fixed_eh);
if (m_final_eh) m_ctx.load()->user_propagate_register_final(m_final_eh);
if (m_eq_eh) m_ctx.load()->user_propagate_register_eq(m_eq_eh);
if (m_diseq_eh) m_ctx.load()->user_propagate_register_diseq(m_diseq_eh);
if (m_created_eh) m_ctx.load()->user_propagate_register_created(m_created_eh);
if (m_decide_eh) m_ctx.load()->user_propagate_register_decide(m_decide_eh);
for (expr* v : m_vars)
m_ctx.load()->user_propagate_register_expr(v);
for (auto& [var, value] : m_values)
m_ctx.load()->user_propagate_initialize_value(var, value);
}
void user_propagate_clear() override {
m_user_ctx = nullptr;
m_vars.reset();
m_fixed_eh = nullptr;
m_final_eh = nullptr;
m_eq_eh = nullptr;
m_diseq_eh = nullptr;
m_created_eh = nullptr;
m_decide_eh = nullptr;
m_on_clause_eh = nullptr;
m_on_clause_ctx = nullptr;
}
void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override {
m_on_clause_ctx = ctx;
m_on_clause_eh = on_clause;
}
void user_propagate_init(
void* ctx,
user_propagator::push_eh_t& push_eh,
user_propagator::pop_eh_t& pop_eh,
user_propagator::fresh_eh_t& fresh_eh) override {
user_propagate_clear();
m_user_ctx = ctx;
m_push_eh = push_eh;
m_pop_eh = pop_eh;
m_fresh_eh = fresh_eh;
}
void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override {
m_fixed_eh = fixed_eh;
}
void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override {
m_final_eh = final_eh;
}
void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override {
m_eq_eh = eq_eh;
}
void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override {
m_diseq_eh = diseq_eh;
}
void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override {
m_ctx.load()->user_propagate_register_on_binding(binding_eh);
}
void user_propagate_register_expr(expr* e) override {
m_vars.push_back(e);
}
void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override {
m_created_eh = created_eh;
}
void user_propagate_register_decide(user_propagator::decide_eh_t& decide_eh) override {
m_decide_eh = decide_eh;
}
void user_propagate_initialize_value(expr* var, expr* value) override {
m_values.push_back({expr_ref(var, m), expr_ref(value, m)});
}
};
static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) {
return alloc(smt_tactic, m, p);
}
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
}
tactic * mk_smt_tactic_core(ast_manager& m, params_ref const& p, symbol const& logic) {
parallel_params pp(p);
return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(m, p);
}
tactic * mk_smt_tactic_core_using(ast_manager& m, bool auto_config, params_ref const& _p) {
parallel_params pp(_p);
params_ref p = _p;
p.set_bool("auto_config", auto_config);
return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(m, p), p);
}