mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

Add partial solution for the uneeded disambiguation issue raised by David Cok

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-03 15:55:36 -08:00
parent 62c841c320
commit 39a614559c
3 changed files with 45 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/arith_decl_plugin.cpp
View file

@ -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, func_decl * arith_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, 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) if (k == OP_NUM)
return mk_num_decl(num_parameters, parameters, arity); return mk_num_decl(num_parameters, parameters, arity);
if (arity == 0 && !is_const_op(k)) { 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, 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) { 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) if (k == OP_NUM)
return mk_num_decl(num_parameters, parameters, num_args); return mk_num_decl(num_parameters, parameters, num_args);
if (num_args == 0 && !is_const_op(k)) { if (num_args == 0 && !is_const_op(k)) {

14
src/ast/ast.cpp
View file

@ -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, func_decl * basic_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, BOOL_SORT))
m_manager->raise_exception("unneeded disambiguation");
else
m_manager->raise_exception("incorrect disambiguation");
return 0;
}
switch (static_cast<basic_op_kind>(k)) { switch (static_cast<basic_op_kind>(k)) {
case OP_TRUE: return m_true_decl; case OP_TRUE: return m_true_decl;
case OP_FALSE: return m_false_decl; case OP_FALSE: return m_false_decl;
@ -1045,6 +1052,13 @@ 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, 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<basic_op_kind>(k)) { switch (static_cast<basic_op_kind>(k)) {
case OP_TRUE: return m_true_decl; case OP_TRUE: return m_true_decl;
case OP_FALSE: return m_false_decl; case OP_FALSE: return m_false_decl;

14
src/ast/bv_decl_plugin.cpp
View file

@ -461,6 +461,13 @@ 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, 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; int bv_size;
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
// bv_size is filled in. // bv_size is filled in.
@ -559,6 +566,13 @@ 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, 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; int bv_size;
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) { if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
// bv_size is filled in. // bv_size is filled in.