mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

handle small powers in theory_lra #4616

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-13 11:47:51 -07:00
parent c63ad2e834
commit 9df6c10ad8
1 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/smt/theory_lra.cpp
View file

@ -487,6 +487,12 @@ class theory_lra::imp {
vars.push_back(v); vars.push_back(v);
++index; ++index;
} }
else if(a.is_power(n, n1, n2) && is_app(n1) && is_numeral(n2, r) && r.is_unsigned() && r <= 10) {
theory_var v = internalize_power(to_app(n), to_app(n1), r.get_unsigned());
coeffs[vars.size()] = coeffs[index];
vars.push_back(v);
++index;
}
else if (a.is_numeral(n, r)) { else if (a.is_numeral(n, r)) {
offset += coeffs[index]*r; offset += coeffs[index]*r;
++index; ++index;
@ -600,6 +606,23 @@ class theory_lra::imp {
} }
} }
theory_var internalize_power(app* t, app* n, unsigned p) {
internalize_args(t, true);
bool _has_var = has_var(t);
mk_enode(t);
theory_var v = mk_var(t);
if (_has_var)
return v;
theory_var w = mk_var(n);
svector<lpvar> vars;
for (unsigned i = 0; i < p; ++i)
vars.push_back(register_theory_var_in_lar_solver(w));
ensure_nla();
m_solver->register_existing_terms();
m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
return v;
}
theory_var internalize_mul(app* t) { theory_var internalize_mul(app* t) {
SASSERT(a.is_mul(t)); SASSERT(a.is_mul(t));
internalize_args(t, true); internalize_args(t, true);