initial files to support theory-solver based synthesis

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

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));
 }

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<builtin_name> & op_names, symbol const & logic) {
+    if (logic == symbol::null) {
+        op_names.push_back(builtin_name("synthesiz3", OP_SYNTH_DECLARE_OUTPUT));
+    }
+}
+   
+
+
+

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<builtin_name> & op_names, symbol const & logic) override;
+    
+    sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { return nullptr; }
+};
+
+
+

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);

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

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);        

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;
+    }
+
+}

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;
+
+    };
+};