From 64233034cc0a415fc7b1b6d63110857b2c364d78 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Jul 2017 08:26:52 -0700 Subject: [PATCH] fix #1173 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 48 +++++++++++++++++++++++++++++++++++ src/ast/arith_decl_plugin.h | 1 + 2 files changed, 49 insertions(+) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 1c01496cf..66580a1dd 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -403,9 +403,57 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { } } +void arith_decl_plugin::check_arity(unsigned arity, unsigned expected_arity) { + if (arity != expected_arity) { + m_manager->raise_exception("invalid number of arguments passed to function"); + } +} + inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) { if (k == OP_SUB && arity == 1) { return OP_UMINUS; + } + switch (k) { + case OP_LE: check_arity(arity, 2); break; + case OP_GE: check_arity(arity, 2); break; + case OP_LT: check_arity(arity, 2); break; + case OP_GT: check_arity(arity, 2); break; + case OP_ADD: break; + case OP_SUB: break; + case OP_UMINUS: check_arity(arity, 1); break; + case OP_MUL: break; + case OP_DIV: check_arity(arity, 2); break; + case OP_IDIV: check_arity(arity, 2); break; + case OP_REM: check_arity(arity, 2); break; + case OP_MOD: check_arity(arity, 2); break; + case OP_TO_REAL: check_arity(arity, 1); break; + case OP_TO_INT: check_arity(arity, 1); break; + case OP_IS_INT: check_arity(arity, 1); break; + case OP_POWER: check_arity(arity, 2); break; + case OP_ABS: check_arity(arity, 1); break; + case OP_SIN: check_arity(arity, 1); break; + case OP_COS: check_arity(arity, 1); break; + case OP_TAN: check_arity(arity, 1); break; + case OP_ASIN: check_arity(arity, 1); break; + case OP_ACOS: check_arity(arity, 1); break; + case OP_ATAN: check_arity(arity, 1); break; + case OP_SINH: check_arity(arity, 1); break; + case OP_COSH: check_arity(arity, 1); break; + case OP_TANH: check_arity(arity, 1); break; + case OP_ASINH: check_arity(arity, 1); break; + case OP_ACOSH: check_arity(arity, 1); break; + case OP_ATANH: check_arity(arity, 1); break; + case OP_PI: break; + case OP_E: break; + case OP_0_PW_0_INT: break; + case OP_0_PW_0_REAL: break; + case OP_NEG_ROOT: break; + case OP_DIV_0: check_arity(arity, 1); break; + case OP_IDIV_0: check_arity(arity, 1); break; + case OP_MOD_0: check_arity(arity, 1); break; + case OP_U_ASIN: break; + case OP_U_ACOS: break; + } return k; } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 6d6da9ed5..43bf4be65 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -157,6 +157,7 @@ protected: func_decl * mk_func_decl(decl_kind k, bool is_real); virtual void set_manager(ast_manager * m, family_id id); decl_kind fix_kind(decl_kind k, unsigned arity); + void check_arity(unsigned arity, unsigned expected_arity); func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity); public: