From 0fb7055597afc0dd58e60cfb241d5c0181fc7665 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Aug 2023 20:39:53 -0700
Subject: [PATCH] synth

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 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<expr> 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<expr> 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<app> m_synth;