From ae24b73b19efaa293c480cb202c48eeba13383c8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 26 Jan 2023 21:19:45 -0800
Subject: [PATCH] bugfixes to incremental linearization for expanding power
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/lp/nla_powers.cpp | 12 ++++++------
src/smt/theory_lra.cpp | 3 ++-
2 files changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
index 847ef7a84..4054dd7c1 100644
--- a/src/math/lp/nla_powers.cpp
+++ b/src/math/lp/nla_powers.cpp
@@ -17,7 +17,7 @@ Description:
Special cases:
-1. Exponentiation. x is fixed numeral.
+1. Exponentiation. x is fixed numeral a.
TOCL18 axioms:
a^y > 0 (if a > 0)
@@ -29,13 +29,13 @@ TOCL18 axioms:
Other special case:
- y = 1 <= a^y = a
+ y = 1 <=> a^y = a
TOCL18 approach: Polynomial abstractions
Taylor: a^y = sum_i ln(a)*y^i/i!
-Truncation: P(n, a) = sum_{i=0}^n ln(a)*y^i/i!
+Truncation: P(n, a) = sum_{i=0}^n ln(a)*y^i/i! = 1 + ln(a)*y + ln(a)^2*y^2/2 +
y = 0: handled by axiom a^y = 1
y < 0: P(2n-1, y) <= a^y <= P(2n, y), n > 0 because Taylor contribution is negative at odd powers.
@@ -131,9 +131,9 @@ namespace nla {
return l_false;
}
- if (xval >= 2 && yval != 0 & rval <= yval + 1) {
- new_lemma lemma(c, "x >= 2, y != 0 => x^y > y + 1");
- lemma |= ineq(x, llc::LT, rational(2));
+ if (xval >= 3 && yval != 0 & rval <= yval + 1) {
+ new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
+ lemma |= ineq(x, llc::LT, rational(3));
lemma |= ineq(y, llc::EQ, rational::zero());
lemma |= ineq(lp::lar_term(r, rational::minus_one(), y), llc::GT, rational::one());
return l_false;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index c5b897d78..29f34655a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1115,7 +1115,8 @@ public:
void mk_power_axiom(expr* p, expr* x, expr* y) {
rational r;
- if (a.is_extended_numeral(x, r) && r.is_unsigned() && r.is_pos()) {
+ // r > 0 => r^y > 0
+ if (a.is_extended_numeral(x, r) && r > 0) {
expr_ref zero(a.mk_real(0), m);
mk_axiom(~mk_literal(a.mk_le(p, zero)));
}