From 8e5581b4fea2ec9b41355b23369f7401b04cf61d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 Feb 2013 08:19:33 -0800
Subject: [PATCH] Retract changes in the commit 39a614559cae. The fix was
affecting benchmarks using the array theory map construct.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/ast/arith_decl_plugin.cpp | 14 --------------
src/ast/ast.cpp | 14 --------------
src/ast/bv_decl_plugin.cpp | 14 --------------
3 files changed, 42 deletions(-)
diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 5e346fc0d..9d1f4343f 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -492,13 +492,6 @@ 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)) {
@@ -516,13 +509,6 @@ 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 1ba468399..63a450094 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1010,13 +1010,6 @@ 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<basic_op_kind>(k)) {
case OP_TRUE: return m_true_decl;
case OP_FALSE: return m_false_decl;
@@ -1052,13 +1045,6 @@ 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) {
- 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)) {
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 823d9eaed..0ef3b60d6 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -461,13 +461,6 @@ 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) {
- 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.
@@ -566,13 +559,6 @@ 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) {
- 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.