mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
bugfixes to incremental linearization for expanding power
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8be43ca68b
commit
ae24b73b19
|
@ -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;
|
||||
|
|
|
@ -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)));
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue