From f4a6c0df3e403e9525a6a890c7faabb8311d597f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Aug 2023 18:53:04 -0700 Subject: [PATCH 1/3] nits, add local functions Signed-off-by: Nikolaj Bjorner --- src/ast/for_each_expr.cpp | 6 +++--- src/ast/for_each_expr.h | 6 +++--- src/sat/smt/synth_solver.cpp | 15 +++++++++------ src/util/util.h | 4 ++-- 4 files changed, 17 insertions(+), 14 deletions(-) diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 832c1d0bc..8feb217db 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -109,9 +109,9 @@ bool has_skolem_functions(expr * n) { subterms::subterms(expr_ref_vector const& es, bool include_bound, ptr_vector* esp, expr_mark* vp): m_include_bound(include_bound), m_es(es), m_esp(esp), m_vp(vp) {} subterms::subterms(expr_ref const& e, bool include_bound, ptr_vector* esp, expr_mark* vp) : m_include_bound(include_bound), m_es(e.m()), m_esp(esp), m_vp(vp) { if (e) m_es.push_back(e); } -subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); } -subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); } -subterms::iterator::iterator(subterms& f, ptr_vector* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) { +subterms::iterator subterms::begin() const { return iterator(* this, m_esp, m_vp, true); } +subterms::iterator subterms::end() const { return iterator(*this, nullptr, nullptr, false); } +subterms::iterator::iterator(subterms const& f, ptr_vector* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) { if (!esp) m_esp = &m_es; else diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h index 0ba0dc992..77b01e939 100644 --- a/src/ast/for_each_expr.h +++ b/src/ast/for_each_expr.h @@ -186,7 +186,7 @@ public: expr_mark m_visited; expr_mark* m_visitedp = nullptr; public: - iterator(subterms& f, ptr_vector* esp, expr_mark* vp, bool start); + iterator(subterms const& f, ptr_vector* esp, expr_mark* vp, bool start); expr* operator*(); iterator operator++(int); iterator& operator++(); @@ -198,8 +198,8 @@ public: static subterms ground(expr_ref const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); } static subterms all(expr_ref_vector const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); } static subterms ground(expr_ref_vector const& e, ptr_vector* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); } - iterator begin(); - iterator end(); + iterator begin() const; + iterator end() const; }; class subterms_postorder { diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp index ce98a6203..52da9e823 100644 --- a/src/sat/smt/synth_solver.cpp +++ b/src/sat/smt/synth_solver.cpp @@ -37,15 +37,18 @@ namespace synth { auto * n = expr2enode(e->get_arg(0)); expr_ref_vector repr(m); - euf::enode_vector todo; - auto has_rep = [&](euf::enode* n) { return !!repr.get(n->get_root_id(), nullptr); }; auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); }; + auto has_rep = [&](euf::enode* n) { return !!get_rep(n); }; + auto set_rep = [&](euf::enode* n, expr* e) { repr.setx(n->get_root_id(), e); }; + + euf::enode_vector todo; + for (unsigned i = 1; i < e->get_num_args(); ++i) { expr * arg = e->get_arg(i); auto * narg = expr2enode(arg); todo.push_back(narg); - repr.setx(narg->get_root_id(), arg); - } + set_rep(narg, arg); + } for (unsigned i = 0; i < todo.size() && !has_rep(n); ++i) { auto * nn = todo[i]; for (auto * p : euf::enode_parents(nn)) { @@ -56,8 +59,8 @@ namespace synth { for (auto * ch : euf::enode_args(p)) args.push_back(get_rep(ch)); app * papp = m.mk_app(p->get_decl(), args); - repr.setx(p->get_root_id(), papp); - todo.push_back(p); + set_rep(p, papp); + todo.push_back(p); } } } diff --git a/src/util/util.h b/src/util/util.h index 6d4efb671..180c0a864 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -363,7 +363,7 @@ void set_fatal_error_handler(void (*pfn)(int error_code)); template -bool any_of(S& set, T const& p) { +bool any_of(S const & set, T const& p) { for (auto const& s : set) if (p(s)) return true; @@ -371,7 +371,7 @@ bool any_of(S& set, T const& p) { } template -bool all_of(S& set, T const& p) { +bool all_of(S const & set, T const& p) { for (auto const& s : set) if (!p(s)) return false; From 90780576f150981fbb8a2957c0d496310003a369 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Aug 2023 20:08:27 -0700 Subject: [PATCH 2/3] clean up header/cpp division Signed-off-by: Nikolaj Bjorner --- src/sat/smt/synth_solver.cpp | 42 +++--------------------------------- src/sat/smt/synth_solver.h | 23 ++++++++------------ 2 files changed, 12 insertions(+), 53 deletions(-) diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp index 52da9e823..e5a9bc482 100644 --- a/src/sat/smt/synth_solver.cpp +++ b/src/sat/smt/synth_solver.cpp @@ -23,13 +23,6 @@ namespace synth { solver::~solver() {} - - // recognize synthesis objective as part of search objective. - // register it for calls to check. - void solver::asserted(sat::literal lit) { - - } - bool solver::synthesize(app* e) { if (e->get_num_args() == 0) @@ -83,27 +76,6 @@ namespace synth { return sat::check_result::CR_DONE; } - // nothing particular to do - void solver::push_core() { - - } - - // nothing particular to do - void solver::pop_core(unsigned n) { - } - - // nothing particular to do - bool solver::unit_propagate() { - return false; - } - - // retrieve explanation for assertions made by synth solver. It only asserts unit literals so nothing to retrieve - void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) { - } - - // where we collect statistics (number of invocations?) - void solver::collect_statistics(statistics& st) const {} - // recognize synthesis objectives here. sat::literal solver::internalize(expr* e, bool sign, bool root) { internalize(e); @@ -126,22 +98,14 @@ namespace synth { // display current state (eg. current set of realizers) std::ostream& solver::display(std::ostream& out) const { + for (auto * e : m_synth) + out << "synth objective " << mk_pp(e, m) << "\n"; return out; } - // justified by "synth". - std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const { - return out << "synth"; - } - - std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { - return out << "synth"; - } - // create a clone of the solver. euf::th_solver* solver::clone(euf::solver& ctx) { - NOT_IMPLEMENTED_YET(); - return nullptr; + return alloc(solver, ctx); } } diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h index 56a640cce..ce302b579 100644 --- a/src/sat/smt/synth_solver.h +++ b/src/sat/smt/synth_solver.h @@ -21,26 +21,21 @@ Author: namespace synth { class solver : public euf::th_euf_solver { - public: solver(euf::solver& ctx); - - ~solver() override; - - - void asserted(sat::literal lit) override; - + ~solver() override; + void asserted(sat::literal lit) override {} sat::check_result check() override; - void push_core() override; - void pop_core(unsigned n) override; - bool unit_propagate() override; - void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override; - void collect_statistics(statistics& st) const override; + void push_core() override {} + void pop_core(unsigned n) override {} + bool unit_propagate() override { return false; } + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override {} + void collect_statistics(statistics& st) const override {} sat::literal internalize(expr* e, bool sign, bool root) override; void internalize(expr* e) override; std::ostream& display(std::ostream& out) const override; - std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override; - std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override; + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return out << "synth"; } + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out << "synth"; } euf::th_solver* clone(euf::solver& ctx) override; private: From 0fb7055597afc0dd58e60cfb241d5c0181fc7665 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Aug 2023 20:39:53 -0700 Subject: [PATCH 3/3] synth Signed-off-by: Nikolaj Bjorner --- src/sat/smt/synth_solver.cpp | 46 +++++++++++++++++++++--------------- src/sat/smt/synth_solver.h | 2 +- 2 files changed, 28 insertions(+), 20 deletions(-) diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp index e5a9bc482..19af62ba5 100644 --- a/src/sat/smt/synth_solver.cpp +++ b/src/sat/smt/synth_solver.cpp @@ -23,16 +23,17 @@ namespace synth { solver::~solver() {} - bool solver::synthesize(app* e) { + sat::literal solver::synthesize(app* e) { if (e->get_num_args() == 0) - return false; + return sat::null_literal; auto * n = expr2enode(e->get_arg(0)); expr_ref_vector repr(m); auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); }; auto has_rep = [&](euf::enode* n) { return !!get_rep(n); }; auto set_rep = [&](euf::enode* n, expr* e) { repr.setx(n->get_root_id(), e); }; + auto is_computable = [&](func_decl* f) { return true; }; euf::enode_vector todo; @@ -47,33 +48,40 @@ namespace synth { for (auto * p : euf::enode_parents(nn)) { if (has_rep(p)) continue; - if (all_of(euf::enode_args(p), [&](auto * ch) { return has_rep(ch); })) { - ptr_buffer args; - for (auto * ch : euf::enode_args(p)) - args.push_back(get_rep(ch)); - app * papp = m.mk_app(p->get_decl(), args); - set_rep(p, papp); - todo.push_back(p); - } - } + if (!is_computable(p->get_decl())) + continue; + if (!all_of(euf::enode_args(p), [&](auto * ch) { return has_rep(ch); })) + continue; + ptr_buffer args; + for (auto * ch : euf::enode_args(p)) + args.push_back(get_rep(ch)); + app * papp = m.mk_app(p->get_decl(), args); + set_rep(p, papp); + todo.push_back(p); + } } expr * sol = get_rep(n); if (!sol) - return false; + return sat::null_literal; - sat::literal lit = eq_internalize(n->get_expr(), sol); - add_unit(~lit); IF_VERBOSE(0, verbose_stream() << mk_pp(sol, m) << "\n"); - return true; + return eq_internalize(n->get_expr(), sol); } // block current model using realizer by E-graph (and arithmetic) // sat::check_result solver::check() { - for (app* e : m_synth) - if (synthesize(e)) - sat::check_result::CR_CONTINUE; - return sat::check_result::CR_DONE; + sat::literal_vector clause; + for (app* e : m_synth) { + auto lit = synthesize(e); + if (lit == sat::null_literal) + return sat::check_result::CR_GIVEUP; + clause.push_back(~lit); + } + if (clause.empty()) + return sat::check_result::CR_DONE; + add_clause(clause); + return sat::check_result::CR_CONTINUE; } // recognize synthesis objectives here. diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h index ce302b579..767f30a18 100644 --- a/src/sat/smt/synth_solver.h +++ b/src/sat/smt/synth_solver.h @@ -39,7 +39,7 @@ namespace synth { euf::th_solver* clone(euf::solver& ctx) override; private: - bool synthesize(app* e); + sat::literal synthesize(app* e); ptr_vector m_synth;