Skip to content

Commit ff920ba

Browse files
NikolajBjornerNikolajBjorner
committed
handle root expressions, and checking exponentiation with nlsat
this one is for you @matthai
1 parent 2fe2735 commit ff920ba

File tree

2 files changed

+131
-61
lines changed

2 files changed

+131
-61
lines changed

‎src/math/lp/nla_powers.cpp

+123-61
Original file line numberDiff line numberDiff line change
@@ -80,113 +80,175 @@ namespace nla {
8080

8181
lbool powers::check(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) {
8282
TRACE("nla", tout << r << " == " << x << "^" << y << "\n");
83-
core& c = m_core;
83+
core& c = m_core;
8484
if (x == null_lpvar || y == null_lpvar || r == null_lpvar)
8585
return l_undef;
86-
if (c.lra.column_has_term(x) || c.lra.column_has_term(y) || c.lra.column_has_term(r))
87-
return l_undef;
88-
89-
if (c.use_nra_model())
90-
return l_undef;
91-
92-
auto xval = c.val(x);
93-
auto yval = c.val(y);
94-
auto rval = c.val(r);
86+
// if (c.lra.column_has_term(x) || c.lra.column_has_term(y) || c.lra.column_has_term(r))
87+
// return l_undef;
9588

9689
lemmas.reset();
9790

98-
if (xval != 0 && yval == 0 && rval != 1) {
91+
auto x_exp_0 = [&]() {
9992
new_lemma lemma(c, "x != 0 => x^0 = 1");
10093
lemma |= ineq(x, llc::EQ, rational::zero());
10194
lemma |= ineq(y, llc::NE, rational::zero());
10295
lemma |= ineq(r, llc::EQ, rational::one());
10396
return l_false;
104-
}
97+
};
10598

106-
if (xval == 0 && yval != 0 && rval != 0) {
99+
auto zero_exp_y = [&]() {
107100
new_lemma lemma(c, "y != 0 => 0^y = 0");
108101
lemma |= ineq(x, llc::NE, rational::zero());
109102
lemma |= ineq(y, llc::EQ, rational::zero());
110103
lemma |= ineq(r, llc::EQ, rational::zero());
111104
return l_false;
112-
}
105+
};
113106

114-
if (xval > 0 && rval <= 0) {
107+
auto x_gt_0 = [&]() {
115108
new_lemma lemma(c, "x > 0 => x^y > 0");
116109
lemma |= ineq(x, llc::LE, rational::zero());
117110
lemma |= ineq(r, llc::GT, rational::zero());
118111
return l_false;
119-
}
112+
};
120113

121-
if (xval > 1 && yval < 0 && rval >= 1) {
114+
auto y_lt_1 = [&]() {
122115
new_lemma lemma(c, "x > 1, y < 0 => x^y < 1");
123116
lemma |= ineq(x, llc::LE, rational::one());
124117
lemma |= ineq(y, llc::GE, rational::zero());
125118
lemma |= ineq(r, llc::LT, rational::one());
126119
return l_false;
127-
}
120+
};
128121

129-
if (xval > 1 && yval > 0 && rval <= 1) {
122+
auto y_gt_1 = [&]() {
130123
new_lemma lemma(c, "x > 1, y > 0 => x^y > 1");
131124
lemma |= ineq(x, llc::LE, rational::one());
132125
lemma |= ineq(y, llc::LE, rational::zero());
133126
lemma |= ineq(r, llc::GT, rational::one());
134127
return l_false;
135-
}
128+
};
136129

137-
if (xval >= 3 && yval != 0 && rval <= yval + 1) {
130+
auto x_ge_3 = [&]() {
138131
new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
139132
lemma |= ineq(x, llc::LT, rational(3));
140133
lemma |= ineq(y, llc::EQ, rational::zero());
141134
lemma |= ineq(lp::lar_term(r, rational::minus_one(), y), llc::GT, rational::one());
142135
return l_false;
136+
};
137+
138+
bool use_rational = !c.use_nra_model();
139+
rational xval, yval, rval;
140+
if (use_rational) {
141+
xval = c.val(x);
142+
yval = c.val(y);
143+
rval = c.val(r);
144+
}
145+
else {
146+
auto& am = c.m_nra.am();
147+
if (am.is_rational(c.m_nra.value(x)) &&
148+
am.is_rational(c.m_nra.value(y)) &&
149+
am.is_rational(c.m_nra.value(r))) {
150+
am.to_rational(c.m_nra.value(x), xval);
151+
am.to_rational(c.m_nra.value(y), yval);
152+
am.to_rational(c.m_nra.value(r), rval);
153+
use_rational = true;
154+
}
143155
}
144156

145-
if (xval > 0 && yval.is_unsigned()) {
146-
auto r2val = power(xval, yval.get_unsigned());
147-
if (rval == r2val)
148-
return l_true;
149-
if (c.random() % 2 == 0) {
150-
new_lemma lemma(c, "x == x0, y == y0 => r = x0^y0");
151-
lemma |= ineq(x, llc::NE, xval);
152-
lemma |= ineq(y, llc::NE, yval);
153-
lemma |= ineq(r, llc::EQ, r2val);
154-
return l_false;
157+
if (use_rational) {
158+
auto xval = c.val(x);
159+
auto yval = c.val(y);
160+
auto rval = c.val(r);
161+
if (xval != 0 && yval == 0 && rval != 1)
162+
return x_exp_0();
163+
else if (xval == 0 && yval != 0 && rval != 0)
164+
return zero_exp_y();
165+
else if (xval > 0 && rval <= 0)
166+
return x_gt_0();
167+
else if (xval > 1 && yval < 0 && rval >= 1)
168+
return y_lt_1();
169+
else if (xval > 1 && yval > 0 && rval <= 1)
170+
return y_gt_1();
171+
else if (xval >= 3 && yval != 0 && rval <= yval + 1)
172+
return x_ge_3();
173+
else if (xval > 0 && yval.is_unsigned()) {
174+
auto r2val = power(xval, yval.get_unsigned());
175+
if (rval == r2val)
176+
return l_true;
177+
if (c.random() % 2 == 0) {
178+
new_lemma lemma(c, "x == x0, y == y0 => r = x0^y0");
179+
lemma |= ineq(x, llc::NE, xval);
180+
lemma |= ineq(y, llc::NE, yval);
181+
lemma |= ineq(r, llc::EQ, r2val);
182+
return l_false;
183+
}
184+
if (yval > 0 && r2val > rval) {
185+
new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0");
186+
lemma |= ineq(x, llc::LT, xval);
187+
lemma |= ineq(y, llc::LT, yval);
188+
lemma |= ineq(r, llc::GE, r2val);
189+
return l_false;
190+
}
191+
if (r2val < rval) {
192+
new_lemma lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0");
193+
lemma |= ineq(x, llc::LE, rational::zero());
194+
lemma |= ineq(x, llc::GT, xval);
195+
lemma |= ineq(y, llc::GT, yval);
196+
lemma |= ineq(r, llc::LE, r2val);
197+
return l_false;
198+
}
155199
}
156-
if (yval > 0 && r2val > rval) {
157-
new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0");
158-
lemma |= ineq(x, llc::LT, xval);
159-
lemma |= ineq(y, llc::LT, yval);
160-
lemma |= ineq(r, llc::GE, r2val);
161-
return l_false;
200+
if (xval > 0 && yval > 0 && !yval.is_int()) {
201+
auto ynum = numerator(yval);
202+
auto yden = denominator(yval);
203+
// r = x^{yn/yd}
204+
// <=>
205+
// r^yd = x^yn
206+
if (ynum.is_unsigned() && yden.is_unsigned()) {
207+
auto ryd = power(rval, yden.get_unsigned());
208+
auto xyn = power(xval, ynum.get_unsigned());
209+
if (ryd == xyn)
210+
return l_true;
211+
}
162212
}
163-
if (r2val < rval) {
164-
new_lemma lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0");
165-
lemma |= ineq(x, llc::LE, rational::zero());
166-
lemma |= ineq(x, llc::GT, xval);
167-
lemma |= ineq(y, llc::GT, yval);
168-
lemma |= ineq(r, llc::LE, r2val);
169-
return l_false;
170-
}
171-
}
172-
if (xval > 0 && yval > 0 && !yval.is_int()) {
173-
auto ynum = numerator(yval);
174-
auto yden = denominator(yval);
175-
if (!ynum.is_unsigned())
176-
return l_undef;
177-
if (!yden.is_unsigned())
178-
return l_undef;
179-
// r = x^{yn/yd}
180-
// <=>
181-
// r^yd = x^yn
182-
auto ryd = power(rval, yden.get_unsigned());
183-
auto xyn = power(xval, ynum.get_unsigned());
184-
if (ryd == xyn)
185-
return l_true;
186213
}
187214

188-
return l_undef;
215+
if (!use_rational) {
216+
auto& am = c.m_nra.am();
217+
scoped_anum xval(am), yval(am), rval(am);
218+
am.set(xval, c.m_nra.value(x));
219+
am.set(yval, c.m_nra.value(y));
220+
am.set(rval, c.m_nra.value(r));
221+
if (xval != 0 && yval == 0 && rval != 1)
222+
return x_exp_0();
223+
else if (xval == 0 && yval != 0 && rval != 0)
224+
return zero_exp_y();
225+
else if (xval > 0 && rval <= 0)
226+
return x_gt_0();
227+
else if (xval > 1 && yval < 0 && rval >= 1)
228+
return y_lt_1();
229+
else if (xval > 1 && yval > 0 && rval <= 1)
230+
return y_gt_1();
231+
else if (xval >= 3 && yval != 0 && rval <= yval + 1)
232+
return x_ge_3();
233+
else if (xval > 0 && yval > 0 && am.is_rational(yval)) {
234+
rational yr;
235+
am.to_rational(yval, yr);
236+
auto ynum = numerator(yr);
237+
auto yden = denominator(yr);
238+
// r = x^{yn/yd}
239+
// <=>
240+
// r^yd = x^yn
241+
if (ynum.is_unsigned() && yden.is_unsigned()) {
242+
am.set(rval, power(rval, yden.get_unsigned()));
243+
am.set(xval, power(xval, ynum.get_unsigned()));
244+
if (rval == xval)
245+
return l_true;
246+
}
247+
}
248+
}
189249

250+
return l_undef;
190251
}
252+
191253

192254
}

‎src/smt/theory_lra.cpp

+8
Original file line numberDiff line numberDiff line change
@@ -1099,6 +1099,14 @@ class theory_lra::imp {
10991099
expr_ref zero(a.mk_real(0), m);
11001100
mk_axiom(~mk_literal(a.mk_le(p, zero)));
11011101
}
1102+
if (a.is_extended_numeral(y, r) && r > 0) {
1103+
// r is 1/n then x >= 0 => x = p^n
1104+
if (numerator(r) == 1 && denominator(r) > 1) {
1105+
expr_ref x_ge_0(a.mk_ge(x, a.mk_real(0)), m);
1106+
expr_ref x_eq_pn(a.mk_eq(x, a.mk_power(p, a.mk_real(denominator(r)))), m);
1107+
mk_axiom(~mk_literal(x_ge_0), mk_literal(x_eq_pn));
1108+
}
1109+
}
11021110
bool can_be_underspecified = false;
11031111
if (a.is_numeral(x, r) && r == 0 && (!a.is_numeral(y, r) || r == 0))
11041112
can_be_underspecified = true;

0 commit comments

Comments
 (0)