From 27dce71ea933ea79838ac0c37a95136260ec1a86 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Aug 2023 09:24:34 -0700 Subject: [PATCH] initial files to support theory-solver based synthesis --- src/ast/CMakeLists.txt | 1 + src/ast/reg_decl_plugins.cpp | 36 +++++-------- src/ast/synth_decl_plugin.cpp | 58 +++++++++++++++++++++ src/ast/synth_decl_plugin.h | 46 +++++++++++++++++ src/cmd_context/cmd_context.cpp | 3 ++ src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/euf_solver.cpp | 4 ++ src/sat/smt/synth_solver.cpp | 90 +++++++++++++++++++++++++++++++++ src/sat/smt/synth_solver.h | 47 +++++++++++++++++ 9 files changed, 264 insertions(+), 22 deletions(-) create mode 100644 src/ast/synth_decl_plugin.cpp create mode 100644 src/ast/synth_decl_plugin.h create mode 100644 src/sat/smt/synth_solver.cpp create mode 100644 src/sat/smt/synth_solver.h diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 7a4a03a27..f80d131d7 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -48,6 +48,7 @@ z3_add_component(ast shared_occs.cpp special_relations_decl_plugin.cpp static_features.cpp + synth_decl_plugin.cpp used_vars.cpp value_generator.cpp well_sorted.cpp diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index 8cb0bbe5a..b42591a4c 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -29,39 +29,31 @@ Revision History: #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/special_relations_decl_plugin.h" +#include "ast/synth_decl_plugin.h" void reg_decl_plugins(ast_manager & m) { - if (!m.get_plugin(m.mk_family_id(symbol("arith")))) { + if (!m.get_plugin(m.mk_family_id(symbol("arith")))) m.register_plugin(symbol("arith"), alloc(arith_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("bv")))) { + if (!m.get_plugin(m.mk_family_id(symbol("bv")))) m.register_plugin(symbol("bv"), alloc(bv_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("array")))) { + if (!m.get_plugin(m.mk_family_id(symbol("array")))) m.register_plugin(symbol("array"), alloc(array_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("datatype")))) { + if (!m.get_plugin(m.mk_family_id(symbol("datatype")))) m.register_plugin(symbol("datatype"), alloc(datatype_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("recfun")))) { + if (!m.get_plugin(m.mk_family_id(symbol("recfun")))) m.register_plugin(symbol("recfun"), alloc(recfun::decl::plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) { + if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) m.register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("char")))) { + if (!m.get_plugin(m.mk_family_id(symbol("char")))) m.register_plugin(symbol("char"), alloc(char_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("seq")))) { + if (!m.get_plugin(m.mk_family_id(symbol("seq")))) m.register_plugin(symbol("seq"), alloc(seq_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) { + if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("pb")))) { + if (!m.get_plugin(m.mk_family_id(symbol("pb")))) m.register_plugin(symbol("pb"), alloc(pb_decl_plugin)); - } - if (!m.get_plugin(m.mk_family_id(symbol("specrels")))) { + if (!m.get_plugin(m.mk_family_id(symbol("specrels")))) m.register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin)); - } + if (!m.get_plugin(m.mk_family_id(symbol("synth")))) + m.register_plugin(symbol("synth"), alloc(synth_decl_plugin)); } diff --git a/src/ast/synth_decl_plugin.cpp b/src/ast/synth_decl_plugin.cpp new file mode 100644 index 000000000..8934eefb2 --- /dev/null +++ b/src/ast/synth_decl_plugin.cpp @@ -0,0 +1,58 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + synth_decl_plugin.cpp + +Abstract: + + Plugin for function symbols used for synthesis + +Author: + + Petra Hozzova 2023-08-09 + Nikolaj Bjorner (nbjorner) 2023-08-08 + +--*/ + +#include "ast/synth_decl_plugin.h" + + + +synth_decl_plugin::synth_decl_plugin() {} + +func_decl * synth_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + auto& m = *m_manager; + if (!range) + range = m.mk_bool_sort(); + + if (!m.is_bool(range)) + m.raise_exception("range of synthesis declaration is Bool"); + + if (num_parameters > 0) + m.raise_exception("no parameters are expected"); + + symbol name; + switch (k) { + case OP_SYNTH_DECLARE_OUTPUT: + name = "synthesiz3"; + break; + case OP_SYNTH_DECLARE_GRAMMAR: + default: + NOT_IMPLEMENTED_YET(); + } + func_decl_info info(m_family_id, k, num_parameters, parameters); + return m.mk_func_decl(name, arity, domain, range, info); +} + +void synth_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { + if (logic == symbol::null) { + op_names.push_back(builtin_name("synthesiz3", OP_SYNTH_DECLARE_OUTPUT)); + } +} + + + + diff --git a/src/ast/synth_decl_plugin.h b/src/ast/synth_decl_plugin.h new file mode 100644 index 000000000..29a2d439d --- /dev/null +++ b/src/ast/synth_decl_plugin.h @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + synth_decl_plugin.h + +Abstract: + + Plugin for function symbols used for synthesis + +Author: + + Petra Hozzova 2023-08-09 + Nikolaj Bjorner (nbjorner) 2023-08-08 + +--*/ +#pragma once + +#include "ast/ast.h" + + +enum synth_op_kind { + OP_SYNTH_DECLARE_OUTPUT, + OP_SYNTH_DECLARE_GRAMMAR, + LAST_SYNTH_OP +}; + +class synth_decl_plugin : public decl_plugin { +public: + synth_decl_plugin(); + + decl_plugin * mk_fresh() override { + return alloc(synth_decl_plugin); + } + + func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) override; + + void get_op_names(svector & op_names, symbol const & logic) override; + + sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { return nullptr; } +}; + + + diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 6f04799f6..f9b851999 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -32,6 +32,7 @@ Notes: #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/special_relations_decl_plugin.h" +#include "ast/synth_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/rewriter/var_subst.h" #include "ast/pp.h" @@ -825,6 +826,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin), !has_logic()); + register_plugin(symbol("synth"), alloc(synth_decl_plugin), !has_logic()); } else { // the manager was created by an external module @@ -841,6 +843,7 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("seq"), logic_has_seq(), fids); load_plugin(symbol("fpa"), logic_has_fpa(), fids); load_plugin(symbol("pb"), logic_has_pb(), fids); + load_plugin(symbol("synth"), !has_logic(), fids); for (family_id fid : fids) { decl_plugin * p = m_manager->get_plugin(fid); diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 4a899ca9d..cc8466003 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -44,6 +44,7 @@ z3_add_component(sat_smt q_solver.cpp recfun_solver.cpp sat_th.cpp + synth_solver.cpp tseitin_theory_checker.cpp user_solver.cpp COMPONENT_DEPENDENCIES diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 6a6b43650..ee6d42a99 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -28,6 +28,7 @@ Author: #include "sat/smt/fpa_solver.h" #include "sat/smt/dt_solver.h" #include "sat/smt/recfun_solver.h" +#include "sat/smt/synth_solver.h" namespace euf { @@ -130,6 +131,7 @@ namespace euf { arith_util arith(m); datatype_util dt(m); recfun::util rf(m); + if (pb.get_family_id() == fid) ext = alloc(pb::solver, *this, fid); else if (bvu.get_family_id() == fid) @@ -144,6 +146,8 @@ namespace euf { ext = alloc(dt::solver, *this, fid); else if (rf.get_family_id() == fid) ext = alloc(recfun::solver, *this); + else if (m.mk_family_id("synth") == fid) + ext = alloc(synth::solver, *this); if (ext) add_solver(ext); diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp new file mode 100644 index 000000000..be2bf4f55 --- /dev/null +++ b/src/sat/smt/synth_solver.cpp @@ -0,0 +1,90 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + synth_solver.h + +Author: + + Petra Hozzova 2023-08-08 + Nikolaj Bjorner (nbjorner) 2020-08-17 + +--*/ + + +#include "sat/smt/synth_solver.h" +#include "sat/smt/euf_solver.h" + +namespace synth { + + solver::solver(euf::solver& ctx): + th_euf_solver(ctx, symbol("synth"), ctx.get_manager().mk_family_id("synth")) {} + + solver::~solver() {} + + + // recognize synthesis objective as part of search objective. + // register it for calls to check. + void solver::asserted(sat::literal lit) { + + } + + // block current model using realizer by E-graph (and arithmetic) + // + sat::check_result solver::check() { + + 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) { + NOT_IMPLEMENTED_YET(); + return sat::null_literal; + } + + // recognize synthesis objectives here and above + void solver::internalize(expr* e) {} + + // display current state (eg. current set of realizers) + std::ostream& solver::display(std::ostream& out) const { + 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; + } + +} diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h new file mode 100644 index 000000000..e23f1e0fb --- /dev/null +++ b/src/sat/smt/synth_solver.h @@ -0,0 +1,47 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + synth_solver.h + +Author: + + Petra Hozzova 2023-08-08 + Nikolaj Bjorner (nbjorner) 2020-08-17 + +--*/ + +#pragma once + +#include "sat/smt/sat_th.h" +#include "solver/solver.h" + + +namespace synth { + + class solver : public euf::th_euf_solver { + + public: + solver(euf::solver& ctx); + + ~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; + 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; + euf::th_solver* clone(euf::solver& ctx) override; + + }; +};