Fix uninterpreted sort definition. There was a mismatch in the behavior of the API and SMT front-ends. The SMT front-ends were using user_sorts to be able to support parametric uninterpreted sorts. After this fix, the API also creates user_sorts.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/api/api_ast.cpp

@@ -78,7 +78,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_uninterpreted_sort(c, name);
         RESET_ERROR_CODE();
-        sort* ty = mk_c(c)->m().mk_sort(to_symbol(name));
+        sort* ty = mk_c(c)->m().mk_uninterpreted_sort(to_symbol(name));
         mk_c(c)->save_ast_trail(ty);
         RETURN_Z3(of_sort(ty));
         Z3_CATCH_RETURN(0);
@@ -620,7 +620,7 @@ extern "C" {
         CHECK_VALID_AST(t, Z3_UNKNOWN_SORT);
         family_id fid = to_sort(t)->get_family_id();
         decl_kind k   = to_sort(t)->get_decl_kind();
-        if (fid == null_family_id) {
+        if (mk_c(c)->m().is_uninterp(to_sort(t))) {
             return Z3_UNINTERPRETED_SORT;
         }
         else if (fid == mk_c(c)->m().get_basic_family_id() && k == BOOL_SORT) {

src/ast/ast.cpp

@@ -1816,6 +1816,12 @@ sort * ast_manager::mk_sort(symbol const & name, sort_info * info) {
     return register_node(new_node);
 }
 
+sort * ast_manager::mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters) {
+    user_sort_plugin * plugin = get_user_sort_plugin();
+    decl_kind kind = plugin->register_name(name);
+    return plugin->mk_sort(kind, num_parameters, parameters);
+}
+
 func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, 
                                       bool assoc, bool comm, bool inj) {
     func_decl_info info(null_family_id, null_decl_kind);
@@ -2058,7 +2064,7 @@ sort * ast_manager::mk_fresh_sort(char const * prefix) {
     string_buffer<32> buffer;
     buffer << prefix << "!" << m_fresh_id;
     m_fresh_id++;
-    return mk_sort(symbol(buffer.c_str()));
+    return mk_uninterpreted_sort(symbol(buffer.c_str()));
 }
 
 symbol ast_manager::mk_fresh_var_name(char const * prefix) {

src/ast/ast.h

@@ -1622,11 +1622,13 @@ private:
     sort * mk_sort(symbol const & name, sort_info * info);
     
 public:
-    sort * mk_sort(symbol const & name) { return mk_sort(name, 0); }
+    sort * mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters);
+
+    sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, 0); }
     
     sort * mk_sort(symbol const & name, sort_info const & info) {
         if (info.get_family_id() == null_family_id) {
-            return mk_sort(name, 0);
+            return mk_uninterpreted_sort(name);
         }
         else {
             return mk_sort(name, &const_cast<sort_info &>(info));

src/ast/ast_translation.cpp

@@ -111,7 +111,10 @@ void ast_translation::mk_sort(sort * s, frame & fr) {
     sort_info * si     = s->get_info();
     sort * new_s;
     if (si == 0) {
-        new_s = m_to_manager.mk_sort(s->get_name());
+        // TODO: investigate: this branch is probably unreachable.
+        // It became unreachable after we started using mk_uninterpreted_sort for creating uninterpreted sorts,
+        // and mk_uninterpreted_sort actually creates a user_sort.
+        new_s = m_to_manager.mk_uninterpreted_sort(s->get_name());
         SASSERT(m_result_stack.size() == fr.m_rpos);
     }
     else {

src/ast/seq_decl_plugin.cpp

@@ -117,8 +117,8 @@ void seq_decl_plugin::init() {
     if(m_init) return;
     ast_manager& m = *m_manager;
     m_init = true;
-    sort* A = m.mk_sort(symbol((unsigned)0));
+    sort* A = m.mk_uninterpreted_sort(symbol((unsigned)0));
-    sort* B = m.mk_sort(symbol((unsigned)1));
+    sort* B = m.mk_uninterpreted_sort(symbol((unsigned)1));
     parameter paramA(A);
     sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, &paramA);
     sort* reA  = m.mk_sort(m_family_id, RE_SORT, 1, &paramA);

src/cmd_context/pdecl.cpp

@@ -303,12 +303,10 @@ sort * psort_user_decl::instantiate(pdecl_manager & m, unsigned n, sort * const
     if (r)
         return r;
     if (m_def == 0) {
-        user_sort_plugin * plugin = m.m().get_user_sort_plugin();
         buffer<parameter> ps;
         for (unsigned i = 0; i < n; i++)
             ps.push_back(parameter(s[i]));
-        decl_kind kind = plugin->register_name(m_name);
+        r  = m.m().mk_uninterpreted_sort(m_name, ps.size(), ps.c_ptr());
-        r  = plugin->mk_sort(kind, ps.size(), ps.c_ptr());
     }
     else {
         r = m_def->instantiate(m, s);

src/parsers/smt/smtlib.cpp

@@ -193,7 +193,7 @@ func_decl * theory::declare_func(symbol const & id, sort_ref_buffer & domain, so
 
 
 sort * theory::declare_sort(symbol const & id) {
-    sort * decl = m_ast_manager.mk_sort(id);
+    sort * decl = m_ast_manager.mk_uninterpreted_sort(id);
     m_symtable.insert(id, decl);
     m_asts.push_back(decl);
     return decl;

src/parsers/smt/smtparser.cpp

@@ -880,8 +880,8 @@ private:
 
                 if (name == symbol("QF_AX")) {
                     // Hack for supporting new QF_AX theory...
-                    sort * index   = m_manager.mk_sort(symbol("Index"));
+                    sort * index   = m_manager.mk_uninterpreted_sort(symbol("Index"));
-                    sort * element = m_manager.mk_sort(symbol("Element"));
+                    sort * element = m_manager.mk_uninterpreted_sort(symbol("Element"));
                     parameter params[2] = { parameter(index), parameter(element) };
                     sort * array   = m_manager.mk_sort(m_array_fid, ARRAY_SORT, 2, params);
                     smtlib::symtable* table = m_benchmark.get_symtable();