diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index e62b01941..0a0769918 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -37,6 +37,7 @@ z3_add_component(sat_smt q_model_fixer.cpp q_queue.cpp q_solver.cpp + recfun_solver.cpp sat_dual_solver.cpp sat_th.cpp user_solver.cpp diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp new file mode 100644 index 000000000..2a6626382 --- /dev/null +++ b/src/sat/smt/recfun_solver.cpp @@ -0,0 +1,116 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + recfun_solver.cpp + +Abstract: + + Recursive function solver plugin + +Author: + + Nikolaj Bjorner (nbjorner) 2021-02-09 + +--*/ + +#include "sat/smt/recfun_solver.h" +#include "sat/smt/euf_solver.h" + + + +namespace recfun { + + + solver::solver(euf::solver& ctx): + th_euf_solver(ctx, symbol("recfun"), ctx.get_manager().mk_family_id("recfun")), + m_plugin(*reinterpret_cast(m.get_plugin(ctx.get_manager().mk_family_id("recfun")))), + m_util(m_plugin.u()), + m_disabled_guards(m), + m_enabled_guards(m), + m_preds(m), + m_num_rounds(0), + m_q_case_expand(), + m_q_body_expand() { + m_num_rounds = 0; + } + + solver::~solver() { + reset(); + } + + void solver::reset() { + reset_queues(); + m_stats.reset(); + m_disabled_guards.reset(); + m_enabled_guards.reset(); + m_q_guards.reset(); + for (auto & kv : m_guard2pending) + dealloc(kv.m_value); + m_guard2pending.reset(); + } + + void solver::reset_queues() { + for (auto* e : m_q_case_expand) { + dealloc(e); + } + m_q_case_expand.reset(); + for (auto* e : m_q_body_expand) { + dealloc(e); + } + m_q_body_expand.reset(); + m_q_clauses.clear(); + } + + void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) { + + } + + void solver::asserted(sat::literal l) { + + } + + sat::check_result solver::check() { + return sat::check_result::CR_DONE; + } + + std::ostream& solver::display(std::ostream& out) const { + return out; + } + + std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { + return out; + } + + void solver::collect_statistics(statistics& st) const { + + } + + euf::th_solver* solver::clone(euf::solver& ctx) { + return nullptr; + } + + bool solver::unit_propagate() { + return false; + } + + sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { + return sat::null_literal; + } + + euf::theory_var solver::mk_var(euf::enode* n) { + return euf::null_theory_var; + } + + void solver::init_search() { + + } + + void solver::finalize_model(model& mdl) { + + } + + + +} diff --git a/src/sat/smt/recfun_solver.h b/src/sat/smt/recfun_solver.h new file mode 100644 index 000000000..06bf3a1c4 --- /dev/null +++ b/src/sat/smt/recfun_solver.h @@ -0,0 +1,166 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + recfun_solver.h + +Abstract: + + Recursive function solver plugin + +Author: + + Simon Cruanes December 2017 + Nikolaj Bjorner (nbjorner) 2021-02-09 + +--*/ +#pragma once + +#include "ast/recfun_decl_plugin.h" +#include "ast/ast_trail.h" +#include "sat/smt/sat_th.h" + + +namespace euf { + class solver; +} + +namespace recfun { + + class solver : public euf::th_euf_solver { + + struct stats { + unsigned m_case_expansions, m_body_expansions, m_macro_expansions; + void reset() { memset(this, 0, sizeof(stats)); } + stats() { reset(); } + }; + + // one case-expansion of `f(t1...tn)` + struct case_expansion { + app * m_lhs; // the term to expand + recfun::def * m_def; + ptr_vector m_args; + case_expansion(recfun::util& u, app * n) : + m_lhs(n), m_def(nullptr), m_args() { + SASSERT(u.is_defined(n)); + func_decl * d = n->get_decl(); + m_def = &u.get_def(d); + m_args.append(n->get_num_args(), n->get_args()); + } + case_expansion(case_expansion const & from) + : m_lhs(from.m_lhs), + m_def(from.m_def), + m_args(from.m_args) {} + case_expansion(case_expansion && from) + : m_lhs(from.m_lhs), + m_def(from.m_def), + m_args(std::move(from.m_args)) {} + }; + + struct pp_case_expansion { + case_expansion & e; + ast_manager & m; + pp_case_expansion(case_expansion & e, ast_manager & m) : e(e), m(m) {} + }; + + friend std::ostream& operator<<(std::ostream&, pp_case_expansion const &); + + // one body-expansion of `f(t1...tn)` using a `C_f_i(t1...tn)` + struct body_expansion { + app* m_pred; + recfun::case_def const * m_cdef; + ptr_vector m_args; + + body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(nullptr), m_args() { + m_cdef = &u.get_case_def(n); + m_args.append(n->get_num_args(), n->get_args()); + } + body_expansion(app* pred, recfun::case_def const & d, ptr_vector & args) : + m_pred(pred), m_cdef(&d), m_args(args) {} + body_expansion(body_expansion const & from): + m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {} + body_expansion(body_expansion && from) : + m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {} + }; + + struct pp_body_expansion { + body_expansion & e; + ast_manager & m; + pp_body_expansion(body_expansion & e, ast_manager & m) : e(e), m(m) {} + }; + + friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &); + + recfun::decl::plugin& m_plugin; + recfun::util& m_util; + stats m_stats; + + // book-keeping for depth of predicates + expr_ref_vector m_disabled_guards; + expr_ref_vector m_enabled_guards; + obj_map m_guard2pending; + obj_map m_pred_depth; + expr_ref_vector m_preds; + unsigned_vector m_preds_lim; + unsigned m_num_rounds; + + ptr_vector m_q_case_expand; + ptr_vector m_q_body_expand; + vector m_q_clauses; + ptr_vector m_q_guards; + + bool is_enabled_guard(expr* guard) { expr_ref ng(m.mk_not(guard), m); return m_enabled_guards.contains(ng); } + bool is_disabled_guard(expr* guard) { return m_disabled_guards.contains(guard); } + + recfun::util & u() const { return m_util; } + bool is_defined(expr * f) const { return u().is_defined(f); } + bool is_case_pred(expr * f) const { return u().is_case_pred(f); } + + bool is_defined(euf::enode * e) const { return is_defined(e->get_expr()); } + bool is_case_pred(euf::enode * e) const { return is_case_pred(e->get_expr()); } + + void activate_guard(expr* guard, expr_ref_vector const& guards); + + void reset_queues(); + expr_ref apply_args(unsigned depth, recfun::vars const & vars, ptr_vector const & args, expr * e); //!< substitute variables by args + void assert_macro_axiom(case_expansion & e); + void assert_case_axioms(case_expansion & e); + void assert_body_axiom(body_expansion & e); + sat::literal mk_literal(expr* e); + + void add_induction_lemmas(unsigned depth); + void disable_guard(expr* guard, expr_ref_vector const& guards); + unsigned get_depth(expr* e); + void set_depth(unsigned d, expr* e); + void set_depth_rec(unsigned d, expr* e); + + sat::literal mk_eq_lit(expr* l, expr* r); + bool is_standard_order(recfun::vars const& vars) const { + return vars.empty() || vars[vars.size()-1]->get_idx() == 0; + } + + void reset(); + + public: + + solver(euf::solver& ctx); + ~solver() override; + bool is_external(sat::bool_var v) override { return false; } + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override; + void asserted(sat::literal l) override; + sat::check_result check() override; + std::ostream& display(std::ostream& out) const override; + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return display_constraint(out, idx); } + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; + void collect_statistics(statistics& st) const override; + euf::th_solver* clone(euf::solver& ctx) override; + bool unit_propagate() override; + sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; + void internalize(expr* e, bool redundant) override { UNREACHABLE(); } + euf::theory_var mk_var(euf::enode* n) override; + void init_search() override; + void finalize_model(model& mdl) override; + bool is_shared(euf::theory_var v) const override { return true; } + }; +}