From 3a15db524403ffbb79a3765484fbcb2380710e43 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Feb 2013 14:34:31 -0800 Subject: [PATCH] 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 --- src/api/api_ast.cpp | 4 ++-- src/ast/ast.cpp | 8 +++++++- src/ast/ast.h | 6 ++++-- src/ast/ast_translation.cpp | 5 ++++- src/ast/seq_decl_plugin.cpp | 4 ++-- src/cmd_context/pdecl.cpp | 4 +--- src/parsers/smt/smtlib.cpp | 2 +- src/parsers/smt/smtparser.cpp | 4 ++-- 8 files changed, 23 insertions(+), 14 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 81a716b12..e93e1a178 100644 --- a/src/api/api_ast.cpp +++ b/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) { diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 63a450094..04268d1f5 100644 --- a/src/ast/ast.cpp +++ b/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) { diff --git a/src/ast/ast.h b/src/ast/ast.h index 3f03b86b9..4c924691c 100644 --- a/src/ast/ast.h +++ b/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(info)); diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp index 8dd6b2f3f..e49edb7ab 100644 --- a/src/ast/ast_translation.cpp +++ b/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 { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 44511cd1f..330227193 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/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* B = m.mk_sort(symbol((unsigned)1)); + sort* A = m.mk_uninterpreted_sort(symbol((unsigned)0)); + sort* B = m.mk_uninterpreted_sort(symbol((unsigned)1)); parameter paramA(A); sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, ¶mA); sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, ¶mA); diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index bafd76f0b..44ba2b4d2 100644 --- a/src/cmd_context/pdecl.cpp +++ b/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 ps; for (unsigned i = 0; i < n; i++) ps.push_back(parameter(s[i])); - decl_kind kind = plugin->register_name(m_name); - r = plugin->mk_sort(kind, ps.size(), ps.c_ptr()); + r = m.m().mk_uninterpreted_sort(m_name, ps.size(), ps.c_ptr()); } else { r = m_def->instantiate(m, s); diff --git a/src/parsers/smt/smtlib.cpp b/src/parsers/smt/smtlib.cpp index 3384e1ffd..d53d3cafa 100644 --- a/src/parsers/smt/smtlib.cpp +++ b/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; diff --git a/src/parsers/smt/smtparser.cpp b/src/parsers/smt/smtparser.cpp index c1ebd251b..b6b40c01a 100644 --- a/src/parsers/smt/smtparser.cpp +++ b/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 * element = m_manager.mk_sort(symbol("Element")); + sort * index = m_manager.mk_uninterpreted_sort(symbol("Index")); + 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();