From 8542e4ae3df20070e9922b5e25e7381b6985ceb7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Aug 2017 00:05:53 -0700 Subject: [PATCH] add pre-processing simplificaiton of power to the legacy simplifier Fixes #1237 Signed-off-by: Nikolaj Bjorner --- .../simplifier/arith_simplifier_plugin.cpp | 21 ++++++++++++++++++- src/ast/simplifier/arith_simplifier_plugin.h | 1 + 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp index bfe72b232..d604ba2ff 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.cpp +++ b/src/ast/simplifier/arith_simplifier_plugin.cpp @@ -402,7 +402,7 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co case OP_TO_REAL: SASSERT(num_args == 1); mk_to_real(args[0], result); break; 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_POWER: SASSERT(num_args == 2); mk_power(args[0], args[1], result); break; case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break; case OP_IRRATIONAL_ALGEBRAIC_NUM: return false; default: @@ -412,6 +412,25 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co return true; } +void arith_simplifier_plugin::mk_power(expr* x, expr* y, expr_ref& result) { + rational a, b; + if (is_numeral(y, b) && b.is_one()) { + result = x; + return; + } + if (is_numeral(x, a) && is_numeral(y, b) && b.is_unsigned()) { + if (b.is_zero() && !a.is_zero()) { + result = m_util.mk_numeral(rational(1), m_manager.get_sort(x)); + return; + } + if (!b.is_zero()) { + result = m_util.mk_numeral(power(a, b.get_unsigned()), m_manager.get_sort(x)); + return; + } + } + result = m_util.mk_power(x, y); +} + void arith_simplifier_plugin::mk_abs(expr * arg, expr_ref & result) { expr_ref c(m_manager); expr_ref m_arg(m_manager); diff --git a/src/ast/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h index 21ab8f6b4..4f3a6add0 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_power(expr* x, expr* y, 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);