From 39a614559caed919cacc8d864775ed1fa8910b44 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 Feb 2013 15:55:36 -0800 Subject: [PATCH] Add partial solution for the uneeded disambiguation issue raised by David Cok Signed-off-by: Leonardo de Moura --- src/ast/arith_decl_plugin.cpp | 14 ++++++++++++++ src/ast/ast.cpp | 16 +++++++++++++++- src/ast/bv_decl_plugin.cpp | 18 ++++++++++++++++-- 3 files changed, 45 insertions(+), 3 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 9d1f4343f..5e346fc0d 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -492,6 +492,13 @@ static bool is_const_op(decl_kind k) { func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { + if (range != 0) { + if (is_sort_of(range, m_family_id, REAL_SORT) || is_sort_of(range, m_family_id, INT_SORT)) + m_manager->raise_exception("unneeded disambiguation"); + else + m_manager->raise_exception("incorrect disambiguation"); + return 0; + } if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, arity); if (arity == 0 && !is_const_op(k)) { @@ -509,6 +516,13 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { + if (range != 0) { + if (is_sort_of(range, m_family_id, REAL_SORT) || is_sort_of(range, m_family_id, INT_SORT)) + m_manager->raise_exception("unneeded disambiguation"); + else + m_manager->raise_exception("incorrect disambiguation"); + return 0; + } if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, num_args); if (num_args == 0 && !is_const_op(k)) { diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 486aa9646..1ba468399 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1010,6 +1010,13 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) { func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { + if (range != 0) { + if (is_sort_of(range, m_family_id, BOOL_SORT)) + m_manager->raise_exception("unneeded disambiguation"); + else + m_manager->raise_exception("incorrect disambiguation"); + return 0; + } switch (static_cast(k)) { case OP_TRUE: return m_true_decl; case OP_FALSE: return m_false_decl; @@ -1044,7 +1051,14 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters } func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned num_args, expr * const * args, sort * range) { + unsigned num_args, expr * const * args, sort * range) { + if (range != 0) { + if (is_sort_of(range, m_family_id, BOOL_SORT)) + m_manager->raise_exception("unneeded disambiguation"); + else + m_manager->raise_exception("incorrect disambiguation"); + return 0; + } switch (static_cast(k)) { case OP_TRUE: return m_true_decl; case OP_FALSE: return m_false_decl; diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index dcefe59c3..823d9eaed 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -460,7 +460,14 @@ func_decl * bv_decl_plugin::mk_mkbv(unsigned arity, sort * const * domain) { } func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { + unsigned arity, sort * const * domain, sort * range) { + if (range != 0) { + if (is_sort_of(range, m_family_id, BV_SORT)) + m_manager->raise_exception("unneeded disambiguation"); + else + m_manager->raise_exception("incorrect disambiguation"); + return 0; + } int bv_size; if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { // bv_size is filled in. @@ -558,7 +565,14 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned num_args, expr * const * args, sort * range) { + unsigned num_args, expr * const * args, sort * range) { + if (range != 0) { + if (is_sort_of(range, m_family_id, BV_SORT)) + m_manager->raise_exception("unneeded disambiguation"); + else + m_manager->raise_exception("incorrect disambiguation"); + return 0; + } int bv_size; if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { // bv_size is filled in.