From 6733a8a5ddae600dcd6d97907925b50044c46399 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 14 Aug 2023 22:21:43 -0700
Subject: [PATCH] prepare for arithmetic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/synth_solver.cpp | 23 +++++++++++++++++++----
 src/sat/smt/synth_solver.h   |  1 +
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp
index 8b49fc1a2..ce553e75e 100644
--- a/src/sat/smt/synth_solver.cpp
+++ b/src/sat/smt/synth_solver.cpp
@@ -19,6 +19,9 @@ Author:
 #include "ast/rewriter/th_rewriter.h"
 #include "sat/smt/synth_solver.h"
 #include "sat/smt/euf_solver.h"
+#include "qe/mbp/mbp_term_graph.h"
+#include "qe/mbp/mbp_arith.h"
+#include "qe/mbp/mbp_arrays.h"
 
 namespace synth {
 
@@ -90,10 +93,13 @@ namespace synth {
         expr* arg = nullptr;
         if (util.is_synthesiz3(e))
             add_synth_objective(synth_objective(m, a));
-        if (util.is_grammar(e))
+        else if (util.is_grammar(e))
             add_uncomputable(a);
-        if (util.is_specification(e, arg))
+        else if (util.is_specification(e, arg))
             add_specification(a, arg);
+        else {
+            IF_VERBOSE(0, verbose_stream() << "unrecognized synthesis objective " << mk_pp(e, m) << "\n");
+        }
     }
 
     sat::check_result solver::check() {
@@ -103,8 +109,9 @@ namespace synth {
         for (auto& s : m_synth) {
             if (s.is_solved())
                 continue;
-            if (m.is_uninterp(s.output()->get_sort()) &&
-                synthesize_uninterpreted_sort(s))
+            if (synthesize_uninterpreted_sort(s))
+                continue;
+            if (synthesize_arithmetic(s))
                 continue;
             IF_VERBOSE(2, ctx.display(verbose_stream()));
             return sat::check_result::CR_GIVEUP;
@@ -359,6 +366,9 @@ namespace synth {
     }
 
     bool solver::synthesize_uninterpreted_sort(synth_objective& obj) {
+        if (!m.is_uninterp(obj.output()->get_sort()))
+            return false;
+                
         sort* srt = obj.output()->get_sort();
         euf::enode* r = expr2enode(obj.output());
         VERIFY(r);
@@ -398,4 +408,9 @@ namespace synth {
         return false;
     }
 
+    bool solver::synthesize_arithmetic(synth_objective& obj) {
+        return false;
+    }
+
+
 }
diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h
index 4803b3f16..d0f3e66d7 100644
--- a/src/sat/smt/synth_solver.h
+++ b/src/sat/smt/synth_solver.h
@@ -75,6 +75,7 @@ namespace synth {
         void compute_rep();
 
         bool synthesize_uninterpreted_sort(synth_objective& obj);
+        bool synthesize_arithmetic(synth_objective& obj);
 
         expr* get_rep(euf::enode* n) { return m_rep.get(n->get_root_id(), nullptr); };
         bool has_rep(euf::enode* n) { return !!get_rep(n); };