Store uncomputable symbols in synth_solver

src/ast/synth_decl_plugin.cpp

@@ -41,6 +41,8 @@ namespace synth {
             name = "synthesiz3";
             break;
         case OP_DECLARE_GRAMMAR: 
+	    name = "uncomputable";
+	    break;
         default:
             NOT_IMPLEMENTED_YET();
         }
@@ -51,6 +53,7 @@ namespace synth {
     void plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
         if (logic == symbol::null) {
             op_names.push_back(builtin_name("synthesiz3", OP_DECLARE_OUTPUT));
+            op_names.push_back(builtin_name("uncomputable", OP_DECLARE_GRAMMAR));
         }
     }
 

src/sat/smt/synth_solver.cpp

@@ -30,37 +30,41 @@ namespace synth {
 
     }
 
+    bool solver::contains_uncomputable(expr* e) {
+	return false;
+    }
+
     bool solver::synthesize(app* e) {
 
         if (e->get_num_args() == 0)
             return false;
         
-    	auto * n = expr2enode(e->get_arg(0));
-	expr_ref_vector repr(m);
+        auto * n = expr2enode(e->get_arg(0));
+        expr_ref_vector repr(m);
 	euf::enode_vector todo;
         auto has_rep = [&](euf::enode* n) { return !!repr.get(n->get_root_id(), nullptr); };
         auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); };
-	for (unsigned i = 1; i < e->get_num_args(); ++i) {
+        for (unsigned i = 1; i < e->get_num_args(); ++i) {
 	    expr * arg = e->get_arg(i);
 	    auto * narg = expr2enode(arg);
-	    todo.push_back(narg);
+            todo.push_back(narg);
 	    repr.setx(narg->get_root_id(), arg);
-	}
+        }
 	for (unsigned i = 0; i < todo.size() && !has_rep(n); ++i) {
 	    auto * nn = todo[i];
-	    for (auto * p : euf::enode_parents(nn)) {
-		if (has_rep(p))
+            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))
+	            for (auto * ch : euf::enode_args(p))
                         args.push_back(get_rep(ch));
                     app * papp = m.mk_app(p->get_decl(), args);
-		    repr.setx(p->get_root_id(), papp);
+	            repr.setx(p->get_root_id(), papp);
 		    todo.push_back(p);
 		}
 	    }
-	}
+        }
 	expr * sol = get_rep(n);
         if (!sol)
             return false;
@@ -68,14 +72,14 @@ namespace synth {
         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 true;
     }
 
     // block current model using realizer by E-graph (and arithmetic)
     // 
     sat::check_result solver::check() {
-	for (app* e : m_synth) 
-	    if (synthesize(e))
+    for (app* e : m_synth)
+        if (synthesize(e))
                sat::check_result::CR_CONTINUE; 
         return sat::check_result::CR_DONE;
     }
@@ -101,9 +105,20 @@ namespace synth {
     // where we collect statistics (number of invocations?)
     void solver::collect_statistics(statistics& st) const {}
 
+    void solver::add_uncomputable(app* e) {
+        for (unsigned i = 0; i < e->get_num_args(); ++i) {
+	    expr* a = e->get_arg(i);
+	    if (is_app(a)) {
+		func_decl* f = to_app(a)->get_decl();
+		m_uncomputable.insert(f);
+		ctx.push(insert_obj_trail(m_uncomputable, f));
+            }
+	}
+    }
+
     // recognize synthesis objectives here.
     sat::literal solver::internalize(expr* e, bool sign, bool root) {
-	internalize(e);
+        internalize(e);
 	sat::literal lit = ctx.expr2literal(e);
 	if (sign)
 	    lit.neg();
@@ -112,13 +127,15 @@ namespace synth {
 
     // recognize synthesis objectives here and above
     void solver::internalize(expr* e) {
-	SASSERT(is_app(e));
+        SASSERT(is_app(e));
 	sat::bool_var bv = ctx.get_si().add_bool_var(e);
-	sat::literal lit(bv, false);
+        sat::literal lit(bv, false);
 	ctx.attach_lit(lit, e);
         synth::util util(m);
-        if (util.is_synthesiz3(e)) 
+        if (util.is_synthesiz3(e))
             ctx.push_vec(m_synth, to_app(e));
+        if (util.is_grammar(e))
+	    add_uncomputable(to_app(e));
     }
 
     // display current state (eg. current set of realizers)

src/sat/smt/synth_solver.h

@@ -14,6 +14,7 @@ Author:
 
 #pragma once
 
+#include "muz/spacer/spacer_util.h"
 #include "sat/smt/sat_th.h"
 #include "solver/solver.h"
 
@@ -45,8 +46,11 @@ namespace synth {
 
     private:
 	bool synthesize(app* e);
+	void add_uncomputable(app* e);
+	bool contains_uncomputable(expr* e);
 
     	ptr_vector<app> m_synth;
+	spacer::func_decl_set m_uncomputable;
 
     };