From 7db0df22e86efb71f8e178aca8c088a970de209c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 9 Aug 2023 18:32:45 -0700
Subject: [PATCH] updates with constraints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/synth_decl_plugin.h  | 9 ++++++---
 src/sat/smt/synth_solver.cpp | 9 ++++-----
 src/sat/smt/synth_solver.h   | 4 ++--
 3 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/ast/synth_decl_plugin.h b/src/ast/synth_decl_plugin.h
index c3b502d22..6c56dbcfb 100644
--- a/src/ast/synth_decl_plugin.h
+++ b/src/ast/synth_decl_plugin.h
@@ -50,9 +50,12 @@ namespace synth {
     public:
         util(ast_manager& m): m(m), m_fid(m.get_family_id("synth")) {}
         
-        bool is_synthesiz3(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_OUTPUT); }
-        bool is_grammar(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_GRAMMAR); }
-        bool is_specification(expr* e) { return is_app_of(e, m_fid, OP_DECLARE_SPECIFICATION); }
+        bool is_synthesiz3(expr* e) const { return is_app_of(e, m_fid, OP_DECLARE_OUTPUT); }
+        bool is_grammar(expr* e) const { return is_app_of(e, m_fid, OP_DECLARE_GRAMMAR); }
+        bool is_specification(expr const* e) const { return is_app_of(e, m_fid, OP_DECLARE_SPECIFICATION); }
+        bool is_specification(func_decl const* f) const { return is_decl_of(f, m_fid, OP_DECLARE_SPECIFICATION); }
+
+        MATCH_UNARY(is_specification);
     };
     
 }
diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp
index fcfcb18f6..62ebcf5e4 100644
--- a/src/sat/smt/synth_solver.cpp
+++ b/src/sat/smt/synth_solver.cpp
@@ -85,10 +85,8 @@ namespace synth {
         }
     }
 
-    void solver::add_specification(app* e) {
+    void solver::add_specification(app* e, expr* arg) {
 	// This assumes that each (assert (constraint (...)) is asserting exactly one app
-	SASSERT((e->get_num_args() == 1) && (is_app(e->get_arg(0))));
-	app* arg = to_app(e->get_arg(0));
         sat::literal lit = ctx.mk_literal(arg);
         sat::bool_var bv = ctx.get_si().add_bool_var(e);
         sat::literal lit_e(bv, false);
@@ -115,12 +113,13 @@ namespace synth {
 	ctx.attach_lit(lit, e);
         synth::util util(m);
 	app* a = to_app(e);
+        expr* arg = nullptr;
         if (util.is_synthesiz3(e))
             add_synth_objective(a);
         if (util.is_grammar(e))
 	    add_uncomputable(a);
-	if (util.is_specification(e))
-	    add_specification(a);
+	if (util.is_specification(e, arg))
+	    add_specification(a, arg);
     }
 
     // display current state (eg. current set of realizers)
diff --git a/src/sat/smt/synth_solver.h b/src/sat/smt/synth_solver.h
index aeca4ae62..cd54a510f 100644
--- a/src/sat/smt/synth_solver.h
+++ b/src/sat/smt/synth_solver.h
@@ -42,7 +42,7 @@ namespace synth {
         sat::literal synthesize(app* e);
 	void add_uncomputable(app* e);
         void add_synth_objective(app* e);
-	void add_specification(app* e);
+	void add_specification(app* e, expr* arg);
 	bool contains_uncomputable(expr* e);
 
         void on_merge_eh(euf::enode* root, euf::enode* other);
@@ -59,7 +59,7 @@ namespace synth {
         typedef obj_hashtable<func_decl> func_decl_set;
 	func_decl_set m_uncomputable;
 	typedef obj_hashtable<app> app_set;
-	app_set m_spec;
+        obj_hashtable<expr> m_spec;
 
     };