diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index fc9b805d1..9d1f4343f 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -194,6 +194,9 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { MK_OP(m_r_power_decl, "^", OP_POWER, r); MK_OP(m_i_power_decl, "^", OP_POWER, i); + MK_UNARY(m_i_abs_decl, "abs", OP_ABS, i); + MK_UNARY(m_r_abs_decl, "abs", OP_ABS, r); + MK_UNARY(m_sin_decl, "sin", OP_SIN, r); MK_UNARY(m_cos_decl, "cos", OP_COS, r); MK_UNARY(m_tan_decl, "tan", OP_TAN, r); @@ -263,6 +266,8 @@ arith_decl_plugin::arith_decl_plugin(): m_is_int_decl(0), m_r_power_decl(0), m_i_power_decl(0), + m_r_abs_decl(0), + m_i_abs_decl(0), m_sin_decl(0), m_cos_decl(0), m_tan_decl(0), @@ -320,6 +325,8 @@ void arith_decl_plugin::finalize() { DEC_REF(m_is_int_decl); DEC_REF(m_i_power_decl); DEC_REF(m_r_power_decl); + DEC_REF(m_i_abs_decl); + DEC_REF(m_r_abs_decl); DEC_REF(m_sin_decl); DEC_REF(m_cos_decl); DEC_REF(m_tan_decl); @@ -372,6 +379,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { case OP_TO_INT: return m_to_int_decl; case OP_IS_INT: return m_is_int_decl; case OP_POWER: return is_real ? m_r_power_decl : m_i_power_decl; + case OP_ABS: return is_real ? m_r_abs_decl : m_i_abs_decl; case OP_SIN: return m_sin_decl; case OP_COS: return m_cos_decl; case OP_TAN: return m_tan_decl; @@ -538,6 +546,7 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("to_real",OP_TO_REAL)); op_names.push_back(builtin_name("to_int",OP_TO_INT)); op_names.push_back(builtin_name("is_int",OP_IS_INT)); + op_names.push_back(builtin_name("abs", OP_ABS)); if (logic == symbol::null) { op_names.push_back(builtin_name("^", OP_POWER)); op_names.push_back(builtin_name("sin", OP_SIN)); diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 53ab1881b..d048bb2f7 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -51,6 +51,7 @@ enum arith_op_kind { OP_TO_REAL, OP_TO_INT, OP_IS_INT, + OP_ABS, OP_POWER, // hyperbolic and trigonometric functions OP_SIN, @@ -121,6 +122,9 @@ protected: func_decl * m_r_power_decl; func_decl * m_i_power_decl; + func_decl * m_r_abs_decl; + func_decl * m_i_abs_decl; + func_decl * m_sin_decl; func_decl * m_cos_decl; func_decl * m_tan_decl; diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index a5dfda6e7..91d87cbfb 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -70,6 +70,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_TO_INT: SASSERT(num_args == 1); st = mk_to_int_core(args[0], result); break; case OP_IS_INT: SASSERT(num_args == 1); st = mk_is_int(args[0], result); break; case OP_POWER: SASSERT(num_args == 2); st = mk_power_core(args[0], args[1], result); break; + case OP_ABS: SASSERT(num_args == 1); st = mk_abs_core(args[0], result); break; case OP_SIN: SASSERT(num_args == 1); st = mk_sin_core(args[0], result); break; case OP_COS: SASSERT(num_args == 1); st = mk_cos_core(args[0], result); break; case OP_TAN: SASSERT(num_args == 1); st = mk_tan_core(args[0], result); break; @@ -1024,6 +1025,11 @@ br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) { } } +br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) { + result = m().mk_ite(m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg))), arg, m_util.mk_uminus(arg)); + return BR_REWRITE2; +} + void arith_rewriter::set_cancel(bool f) { m_util.set_cancel(f); } diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 833cc2515..bce59657a 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -131,6 +131,8 @@ public: } void mk_gt(expr * arg1, expr * arg2, expr_ref & result) { mk_gt_core(arg1, arg2, result); } + br_status mk_abs_core(expr * arg, expr_ref & result); + br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result); diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp index b9e93a973..f7751782d 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.cpp +++ b/src/ast/simplifier/arith_simplifier_plugin.cpp @@ -404,6 +404,7 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co case OP_TO_INT: SASSERT(num_args == 1); mk_to_int(args[0], result); break; case OP_IS_INT: SASSERT(num_args == 1); mk_is_int(args[0], result); break; case OP_POWER: return false; + case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break; case OP_IRRATIONAL_ALGEBRAIC_NUM: return false; default: UNREACHABLE(); @@ -413,6 +414,14 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co return true; } +void arith_simplifier_plugin::mk_abs(expr * arg, expr_ref & result) { + expr_ref c(m_manager); + expr_ref m_arg(m_manager); + mk_uminus(arg, m_arg); + mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg)), c); + m_bsimp.mk_ite(c, arg, m_arg, result); +} + bool arith_simplifier_plugin::is_arith_term(expr * n) const { return n->get_kind() == AST_APP && to_app(n)->get_family_id() == m_fid; } diff --git a/src/ast/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h index 4402fa8a1..4b8f579c0 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.h +++ b/src/ast/simplifier/arith_simplifier_plugin.h @@ -82,6 +82,7 @@ public: void mk_to_real(expr * arg, expr_ref & result); void mk_to_int(expr * arg, expr_ref & result); void mk_is_int(expr * arg, expr_ref & result); + void mk_abs(expr * arg, expr_ref & result); virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);