mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-03 18:55:19 -08:00
parent a05dec99cf
commit 7a946fd9d0
1 changed files with 11 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/smt/theory_arith_nl.h
View file

@ -1519,19 +1519,15 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
return nullptr; return nullptr;
if (varinfo.empty()) if (varinfo.empty())
return p2expr(p); return p2expr(p);
sbuffer<var_num_occs>::const_iterator it = varinfo.begin(); unsigned max = 0;
sbuffer<var_num_occs>::const_iterator end = varinfo.end(); for (auto const& kv : varinfo) {
var = it->first; if (kv.second >= max) {
unsigned max = it->second; max = kv.second;
++it; var = kv.first;
for (; it != end; ++it) {
if (it->second > max) {
var = it->first;
max = it->second;
} }
} }
} }
SASSERT(var != 0); SASSERT(var != nullptr);
unsigned i1 = UINT_MAX; unsigned i1 = UINT_MAX;
unsigned i2 = UINT_MAX; unsigned i2 = UINT_MAX;
rational a, b; rational a, b;
@ -1563,7 +1559,7 @@ expr * theory_arith<Ext>::cross_nested(sbuffer<coeff_expr> & p, expr * var) {
// b*x^{n-m}*[(x^{m} + a/(2b))^2 - (a/2b)^2] // b*x^{n-m}*[(x^{m} + a/(2b))^2 - (a/2b)^2]
// b*[(x^{m} + a/(2b))^2 - (a/2b)^2] for n == m // b*[(x^{m} + a/(2b))^2 - (a/2b)^2] for n == m
rational a2b = a; rational a2b = a;
expr * xm = power(var, m); expr_ref xm(power(var, m), get_manager());
a2b /= (rational(2) * b); a2b /= (rational(2) * b);
// we cannot create a numeral that has sort int, but it is a rational. // we cannot create a numeral that has sort int, but it is a rational.
if (!m_util.is_int(var) || a2b.is_int()) { if (!m_util.is_int(var) || a2b.is_int()) {
@ -1699,11 +1695,10 @@ bool theory_arith<Ext>::is_cross_nested_consistent(row const & r) {
TRACE("non_linear", tout << "check problematic row:\n"; display_row(tout, r); display_row(tout, r, false);); TRACE("non_linear", tout << "check problematic row:\n"; display_row(tout, r); display_row(tout, r, false););
sbuffer<coeff_expr> p; sbuffer<coeff_expr> p;
typename vector<row_entry>::const_iterator it = r.begin_entries(); for (auto & col : r) {
typename vector<row_entry>::const_iterator end = r.end_entries(); if (!col.is_dead()) {
for (; it != end; ++it) { p.push_back(coeff_expr(col.m_coeff.to_rational() * c, var2expr(col.m_var)));
if (!it->is_dead()) }
p.push_back(coeff_expr(it->m_coeff.to_rational() * c, var2expr(it->m_var)));
} }
SASSERT(!p.empty()); SASSERT(!p.empty());
CTRACE("cross_nested_bug", !c.is_one(), tout << "c: " << c << "\n"; display_row(tout, r); tout << "---> p (coeffs, exprs):\n"; display_coeff_exprs(tout, p);); CTRACE("cross_nested_bug", !c.is_one(), tout << "c: " << c << "\n"; display_row(tout, r); tout << "---> p (coeffs, exprs):\n"; display_coeff_exprs(tout, p););