diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 88fc59524..f372b9b6f 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -779,3 +779,20 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
}
return result;
}
+
+bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args) {
+ rational r;
+ if (is_decl_of(f, m_afid, OP_DIV) && is_numeral(args[1], r) && r.is_zero()) {
+ return true;
+ }
+ if (is_decl_of(f, m_afid, OP_IDIV) && is_numeral(args[1], r) && r.is_zero()) {
+ return true;
+ }
+ if (is_decl_of(f, m_afid, OP_MOD) && is_numeral(args[1], r) && r.is_zero()) {
+ return true;
+ }
+ if (is_decl_of(f, m_afid, OP_REM) && is_numeral(args[1], r) && r.is_zero()) {
+ return true;
+ }
+ return plugin().is_considered_uninterpreted(f);
+}
diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 00c7e694f..aa650697d 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -442,6 +442,9 @@ public:
expr_ref mk_add_simplify(expr_ref_vector const& args);
expr_ref mk_add_simplify(unsigned sz, expr* const* args);
+
+ bool is_considered_uninterpreted(func_decl* f, unsigned n, expr* const* args);
+
};
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 31346acd9..e2cc249dd 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -257,7 +257,7 @@ namespace algebraic_numbers {
SASSERT(bqm().ge(upper(c), candidate));
- if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == 0) {
+ if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == polynomial::sign_zero) {
m_wrapper.set(a, candidate);
return true;
}
@@ -320,7 +320,7 @@ namespace algebraic_numbers {
SASSERT(bqm().ge(upper(c), candidate));
// Find if candidate is an actual root
- if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == 0) {
+ if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == polynomial::sign_zero) {
saved_a.restore_if_too_small();
set(a, candidate);
return true;
@@ -379,11 +379,11 @@ namespace algebraic_numbers {
}
void update_sign_lower(algebraic_cell * c) {
- int sl = upm().eval_sign_at(c->m_p_sz, c->m_p, lower(c));
+ polynomial::sign sl = upm().eval_sign_at(c->m_p_sz, c->m_p, lower(c));
// The isolating intervals are refinable. Thus, the polynomial has opposite signs at lower and upper.
- SASSERT(sl != 0);
+ SASSERT(sl != polynomial::sign_zero);
SASSERT(upm().eval_sign_at(c->m_p_sz, c->m_p, upper(c)) == -sl);
- c->m_sign_lower = sl < 0;
+ c->m_sign_lower = sl == polynomial::sign_neg;
}
// Make sure the GCD of the coefficients is one and the leading coefficient is positive
@@ -1594,8 +1594,8 @@ namespace algebraic_numbers {
#define REFINE_LOOP(BOUND, TARGET_SIGN) \
while (true) { \
bqm().div2(BOUND); \
- int new_sign = upm().eval_sign_at(cell_a->m_p_sz, cell_a->m_p, BOUND); \
- if (new_sign == 0) { \
+ polynomial::sign new_sign = upm().eval_sign_at(cell_a->m_p_sz, cell_a->m_p, BOUND); \
+ if (new_sign == polynomial::sign_zero) { \
/* found actual root */ \
scoped_mpq r(qm()); \
to_mpq(qm(), BOUND, r); \
@@ -1695,8 +1695,8 @@ namespace algebraic_numbers {
if (bqm().ge(l, b))
return 1;
// b is in the isolating interval (l, u)
- int sign_b = upm().eval_sign_at(c->m_p_sz, c->m_p, b);
- if (sign_b == 0)
+ auto sign_b = upm().eval_sign_at(c->m_p_sz, c->m_p, b);
+ if (sign_b == polynomial::sign_zero)
return 0;
return sign_b == sign_lower(c) ? 1 : -1;
}
@@ -1979,7 +1979,7 @@ namespace algebraic_numbers {
};
polynomial::var_vector m_eval_sign_vars;
- int eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
+ polynomial::sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
polynomial::manager & ext_pm = p.m();
TRACE("anum_eval_sign", tout << "evaluating sign of: " << p << "\n";);
while (true) {
@@ -1990,7 +1990,7 @@ namespace algebraic_numbers {
scoped_mpq r(qm());
ext_pm.eval(p, x2v_basic, r);
TRACE("anum_eval_sign", tout << "all variables are assigned to rationals, value of p: " << r << "\n";);
- return qm().sign(r);
+ return polynomial::to_sign(qm().sign(r));
}
catch (const opt_var2basic::failed &) {
// continue
@@ -2004,13 +2004,13 @@ namespace algebraic_numbers {
if (ext_pm.is_zero(p_prime)) {
// polynomial vanished after substituting rational values.
- return 0;
+ return polynomial::sign_zero;
}
if (is_const(p_prime)) {
// polynomial became the constant polynomial after substitution.
SASSERT(size(p_prime) == 1);
- return ext_pm.m().sign(ext_pm.coeff(p_prime, 0));
+ return polynomial::to_sign(ext_pm.m().sign(ext_pm.coeff(p_prime, 0)));
}
// Try to find sign using intervals
@@ -2026,7 +2026,7 @@ namespace algebraic_numbers {
ext_pm.eval(p_prime, x2v_interval, ri);
TRACE("anum_eval_sign", tout << "evaluating using intervals: " << ri << "\n";);
if (!bqim().contains_zero(ri)) {
- return bqim().is_pos(ri) ? 1 : -1;
+ return bqim().is_pos(ri) ? polynomial::sign_pos : polynomial::sign_neg;
}
// refine intervals if magnitude > m_min_magnitude
bool refined = false;
@@ -2067,7 +2067,7 @@ namespace algebraic_numbers {
// Remark: m_zero_accuracy == 0 means use precise computation.
if (m_zero_accuracy > 0) {
// assuming the value is 0, since the result is in (-1/2^k, 1/2^k), where m_zero_accuracy = k
- return 0;
+ return polynomial::sign_zero;
}
#if 0
// Evaluating sign using algebraic arithmetic
@@ -2143,7 +2143,7 @@ namespace algebraic_numbers {
bqm().div2k(mL, k);
bqm().div2k(L, k);
if (bqm().lt(mL, ri.lower()) && bqm().lt(ri.upper(), L))
- return 0;
+ return polynomial::sign_zero;
// keep refining ri until ri is inside (-L, L) or
// ri does not contain zero.
@@ -2166,14 +2166,13 @@ namespace algebraic_numbers {
TRACE("anum_eval_sign", tout << "evaluating using intervals: " << ri << "\n";
tout << "zero lower bound is: " << L << "\n";);
if (!bqim().contains_zero(ri)) {
- return bqim().is_pos(ri) ? 1 : -1;
+ return bqim().is_pos(ri) ? polynomial::sign_pos : polynomial::sign_neg;
}
if (bqm().lt(mL, ri.lower()) && bqm().lt(ri.upper(), L))
- return 0;
+ return polynomial::sign_zero;
- for (unsigned i = 0; i < xs.size(); i++) {
- polynomial::var x = xs[i];
+ for (auto x : xs) {
SASSERT(x2v.contains(x));
anum const & v = x2v(x);
SASSERT(!v.is_basic());
@@ -2242,18 +2241,14 @@ namespace algebraic_numbers {
unsigned sz = roots.size();
unsigned j = 0;
- // std::cout << "p: " << p << "\n";
- // std::cout << "sz: " << sz << "\n";
for (unsigned i = 0; i < sz; i++) {
checkpoint();
- // display_root(std::cout, roots[i]); std::cout << std::endl;
ext_var2num ext_x2v(m_wrapper, x2v, x, roots[i]);
TRACE("isolate_roots", tout << "filter_roots i: " << i << ", ext_x2v: x" << x << " -> "; display_root(tout, roots[i]); tout << "\n";);
- int sign = eval_sign_at(p, ext_x2v);
+ polynomial::sign sign = eval_sign_at(p, ext_x2v);
TRACE("isolate_roots", tout << "filter_roots i: " << i << ", result sign: " << sign << "\n";);
if (sign != 0)
continue;
- // display_decimal(std::cout, roots[i], 10); std::cout << " is root" << std::endl;
if (i != j)
set(roots[j], roots[i]);
j++;
@@ -2453,7 +2448,7 @@ namespace algebraic_numbers {
}
}
- int eval_at_mpbq(polynomial_ref const & p, polynomial::var2anum const & x2v, polynomial::var x, mpbq const & v) {
+ polynomial::sign eval_at_mpbq(polynomial_ref const & p, polynomial::var2anum const & x2v, polynomial::var x, mpbq const & v) {
scoped_mpq qv(qm());
to_mpq(qm(), v, qv);
scoped_anum av(m_wrapper);
@@ -2568,13 +2563,13 @@ namespace algebraic_numbers {
#define DEFAULT_PRECISION 2
- void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<int> & signs) {
+ void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<polynomial::sign> & signs) {
isolate_roots(p, x2v, roots);
unsigned num_roots = roots.size();
if (num_roots == 0) {
anum zero;
ext2_var2num ext_x2v(m_wrapper, x2v, zero);
- int s = eval_sign_at(p, ext_x2v);
+ polynomial::sign s = eval_sign_at(p, ext_x2v);
signs.push_back(s);
}
else {
@@ -2601,8 +2596,8 @@ namespace algebraic_numbers {
TRACE("isolate_roots_bug", tout << "w: "; display_root(tout, w); tout << "\n";);
{
ext2_var2num ext_x2v(m_wrapper, x2v, w);
- int s = eval_sign_at(p, ext_x2v);
- SASSERT(s != 0);
+ auto s = eval_sign_at(p, ext_x2v);
+ SASSERT(s != polynomial::sign_zero);
signs.push_back(s);
}
@@ -2611,16 +2606,16 @@ namespace algebraic_numbers {
numeral & curr = roots[i];
select(prev, curr, w);
ext2_var2num ext_x2v(m_wrapper, x2v, w);
- int s = eval_sign_at(p, ext_x2v);
- SASSERT(s != 0);
+ auto s = eval_sign_at(p, ext_x2v);
+ SASSERT(s != polynomial::sign_zero);
signs.push_back(s);
}
int_gt(roots[num_roots - 1], w);
{
ext2_var2num ext_x2v(m_wrapper, x2v, w);
- int s = eval_sign_at(p, ext_x2v);
- SASSERT(s != 0);
+ auto s = eval_sign_at(p, ext_x2v);
+ SASSERT(s != polynomial::sign_zero);
signs.push_back(s);
}
}
@@ -2879,7 +2874,7 @@ namespace algebraic_numbers {
m_imp->isolate_roots(p, x2v, roots);
}
- void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<int> & signs) {
+ void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<polynomial::sign> & signs) {
m_imp->isolate_roots(p, x2v, roots, signs);
}
@@ -3037,7 +3032,7 @@ namespace algebraic_numbers {
l = rational(_l);
}
- int manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
+ polynomial::sign manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
SASSERT(&(x2v.m()) == this);
return m_imp->eval_sign_at(p, x2v);
}
diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h
index fa9731b62..59e6401d7 100644
--- a/src/math/polynomial/algebraic_numbers.h
+++ b/src/math/polynomial/algebraic_numbers.h
@@ -173,7 +173,7 @@ namespace algebraic_numbers {
/**
\brief Isolate the roots of the given polynomial, and compute its sign between them.
*/
- void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<int> & signs);
+ void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<polynomial::sign> & signs);
/**
\brief Store in r the i-th root of p.
@@ -304,7 +304,7 @@ namespace algebraic_numbers {
Return 0 if p(alpha_1, ..., alpha_n) == 0
Return positive number if p(alpha_1, ..., alpha_n) > 0
*/
- int eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v);
+ polynomial::sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v);
void get_polynomial(numeral const & a, svector<mpz> & r);
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 8d4755e82..a368c9507 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -1068,12 +1068,12 @@ namespace polynomial {
g.reserve(std::min(sz1, sz2));
r1.reserve(sz2); // r1 has at most num_args2 arguments
r2.reserve(sz1); // r2 has at most num_args1 arguments
- bool found = false;
- unsigned i1 = 0;
- unsigned i2 = 0;
- unsigned j1 = 0;
- unsigned j2 = 0;
- unsigned j3 = 0;
+ bool found = false;
+ unsigned i1 = 0;
+ unsigned i2 = 0;
+ unsigned j1 = 0;
+ unsigned j2 = 0;
+ unsigned j3 = 0;
while (true) {
if (i1 == sz1) {
if (found) {
@@ -2501,6 +2501,32 @@ namespace polynomial {
return p;
}
+ void gcd_simplify(polynomial * p) {
+ if (m_manager.finite()) return;
+ auto& m = m_manager.m();
+ unsigned sz = p->size();
+ if (sz == 0)
+ return;
+ unsigned g = 0;
+ for (unsigned i = 0; i < sz; i++) {
+ if (!m.is_int(p->a(i))) {
+ return;
+ }
+ int j = m.get_int(p->a(i));
+ if (j == INT_MIN || j == 1 || j == -1)
+ return;
+ g = u_gcd(abs(j), g);
+ if (g == 1)
+ return;
+ }
+ scoped_mpz r(m), gg(m);
+ m.set(gg, g);
+ for (unsigned i = 0; i < sz; ++i) {
+ m.div_gcd(p->a(i), gg, r);
+ m.set(p->a(i), r);
+ }
+ }
+
polynomial * mk_zero() {
return m_zero;
}
@@ -7041,6 +7067,10 @@ namespace polynomial {
return m_imp->hash(p);
}
+ void manager::gcd_simplify(polynomial * p) {
+ m_imp->gcd_simplify(p);
+ }
+
polynomial * manager::coeff(polynomial const * p, var x, unsigned k) {
return m_imp->coeff(p, x, k);
}
diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h
index 0aa3f5db5..45d7c189d 100644
--- a/src/math/polynomial/polynomial.h
+++ b/src/math/polynomial/polynomial.h
@@ -44,6 +44,11 @@ namespace polynomial {
typedef svector<var> var_vector;
class monomial;
+ typedef enum { sign_neg = -1, sign_zero = 0, sign_pos = 1} sign;
+ inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } };
+ inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); }
+ inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); }
+
int lex_compare(monomial const * m1, monomial const * m2);
int lex_compare2(monomial const * m1, monomial const * m2, var min_var);
int graded_lex_compare(monomial const * m1, monomial const * m2);
@@ -278,6 +283,12 @@ namespace polynomial {
*/
static unsigned id(polynomial const * p);
+
+ /**
+ \brief Normalize coefficients by dividing by their gcd
+ */
+ void gcd_simplify(polynomial* p);
+
/**
\brief Return true if \c m is the unit monomial.
*/
diff --git a/src/math/polynomial/polynomial_cache.cpp b/src/math/polynomial/polynomial_cache.cpp
index a617e9412..9f5f014e4 100644
--- a/src/math/polynomial/polynomial_cache.cpp
+++ b/src/math/polynomial/polynomial_cache.cpp
@@ -139,6 +139,7 @@ namespace polynomial {
polynomial * mk_unique(polynomial * p) {
if (m_in_cache.get(pid(p), false))
return p;
+ // m.gcd_simplify(p);
polynomial * p_prime = m_poly_table.insert_if_not_there(p);
if (p == p_prime) {
m_cached_polys.push_back(p_prime);
diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp
index cfc8339d7..9076a4d50 100644
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@@ -1327,25 +1327,25 @@ namespace upolynomial {
div(sz, p, 2, two_x_1, buffer);
}
- int manager::sign_of(numeral const & c) {
+ polynomial::sign manager::sign_of(numeral const & c) {
if (m().is_zero(c))
- return 0;
+ return polynomial::sign_zero;
if (m().is_pos(c))
- return 1;
+ return polynomial::sign_pos;
else
- return -1;
+ return polynomial::sign_neg;
}
// Return the number of sign changes in the coefficients of p
unsigned manager::sign_changes(unsigned sz, numeral const * p) {
unsigned r = 0;
- int prev_sign = 0;
+ auto prev_sign = polynomial::sign_zero;
unsigned i = 0;
for (; i < sz; i++) {
- int sign = sign_of(p[i]);
- if (sign == 0)
+ auto sign = sign_of(p[i]);
+ if (sign == polynomial::sign_zero)
continue;
- if (sign != prev_sign && prev_sign != 0)
+ if (sign != prev_sign && prev_sign != polynomial::sign_zero)
r++;
prev_sign = sign;
}
@@ -1729,14 +1729,14 @@ namespace upolynomial {
}
// Evaluate the sign of p(b)
- int manager::eval_sign_at(unsigned sz, numeral const * p, mpbq const & b) {
+ polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpbq const & b) {
// Actually, given b = c/2^k, we compute the sign of (2^k)^n*p(b)
// Original Horner Sequence
// ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ...
// Variation of the Horner Sequence for (2^k)^n*p(b)
// ((a_n * c + a_{n-1}*2_k)*c + a_{n-2}*(2_k)^2)*c + a_{n-3}*(2_k)^3 ... + a_0*(2_k)^n
if (sz == 0)
- return 0;
+ return polynomial::sign_zero;
if (sz == 1)
return sign_of(p[0]);
numeral const & c = b.numerator();
@@ -1762,14 +1762,14 @@ namespace upolynomial {
}
// Evaluate the sign of p(b)
- int manager::eval_sign_at(unsigned sz, numeral const * p, mpq const & b) {
+ polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpq const & b) {
// Actually, given b = c/d, we compute the sign of (d^n)*p(b)
// Original Horner Sequence
// ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ...
// Variation of the Horner Sequence for (d^n)*p(b)
// ((a_n * c + a_{n-1}*d)*c + a_{n-2}*d^2)*c + a_{n-3}*d^3 ... + a_0*d^n
if (sz == 0)
- return 0;
+ return polynomial::sign_zero;
if (sz == 1)
return sign_of(p[0]);
numeral const & c = b.numerator();
@@ -1796,11 +1796,11 @@ namespace upolynomial {
}
// Evaluate the sign of p(b)
- int manager::eval_sign_at(unsigned sz, numeral const * p, mpz const & b) {
+ polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpz const & b) {
// Using Horner Sequence
// ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ...
if (sz == 0)
- return 0;
+ return polynomial::sign_zero;
if (sz == 1)
return sign_of(p[0]);
scoped_numeral r(m());
@@ -1817,21 +1817,21 @@ namespace upolynomial {
return sign_of(r);
}
- int manager::eval_sign_at_zero(unsigned sz, numeral const * p) {
+ polynomial::sign manager::eval_sign_at_zero(unsigned sz, numeral const * p) {
if (sz == 0)
- return 0;
+ return polynomial::sign_zero;
return sign_of(p[0]);
}
- int manager::eval_sign_at_plus_inf(unsigned sz, numeral const * p) {
+ polynomial::sign manager::eval_sign_at_plus_inf(unsigned sz, numeral const * p) {
if (sz == 0)
- return 0;
+ return polynomial::sign_zero;
return sign_of(p[sz-1]);
}
- int manager::eval_sign_at_minus_inf(unsigned sz, numeral const * p) {
+ polynomial::sign manager::eval_sign_at_minus_inf(unsigned sz, numeral const * p) {
if (sz == 0)
- return 0;
+ return polynomial::sign_zero;
unsigned degree = sz - 1;
if (degree % 2 == 0)
return sign_of(p[sz-1]);
diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h
index 52115ebc1..c8e868f4b 100644
--- a/src/math/polynomial/upolynomial.h
+++ b/src/math/polynomial/upolynomial.h
@@ -554,7 +554,7 @@ namespace upolynomial {
numeral_vector m_tr_tmp;
numeral_vector m_push_tmp;
- int sign_of(numeral const & c);
+ polynomial::sign sign_of(numeral const & c);
struct drs_frame;
void pop_top_frame(numeral_vector & p_stack, svector<drs_frame> & frame_stack);
void push_child_frames(unsigned sz, numeral const * p, numeral_vector & p_stack, svector<drs_frame> & frame_stack);
@@ -735,32 +735,32 @@ namespace upolynomial {
/**
\brief Evaluate the sign of p(b)
*/
- int eval_sign_at(unsigned sz, numeral const * p, mpbq const & b);
+ polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpbq const & b);
+
+ /**
+ \brief Evaluate the sign of p(b)
+ */
+ polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpq const & b);
/**
\brief Evaluate the sign of p(b)
*/
- int eval_sign_at(unsigned sz, numeral const * p, mpq const & b);
-
- /**
- \brief Evaluate the sign of p(b)
- */
- int eval_sign_at(unsigned sz, numeral const * p, mpz const & b);
+ polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpz const & b);
/**
\brief Evaluate the sign of p(0)
*/
- int eval_sign_at_zero(unsigned sz, numeral const * p);
+ polynomial::sign eval_sign_at_zero(unsigned sz, numeral const * p);
/**
\brief Evaluate the sign of p(+oo)
*/
- int eval_sign_at_plus_inf(unsigned sz, numeral const * p);
+ polynomial::sign eval_sign_at_plus_inf(unsigned sz, numeral const * p);
/**
\brief Evaluate the sign of p(-oo)
*/
- int eval_sign_at_minus_inf(unsigned sz, numeral const * p);
+ polynomial::sign eval_sign_at_minus_inf(unsigned sz, numeral const * p);
/**
\brief Evaluate the sign variations in the polynomial sequence at -oo
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 35c637ade..d01541790 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -333,13 +333,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
return BR_REWRITE_FULL;
}
- rational r;
- if (is_decl_of(f, m_au.get_family_id(), OP_DIV) && m_au.is_numeral(args[1], r) && r.is_zero()) {
- result = m_au.mk_real(0);
- return BR_DONE;
- }
- if (is_decl_of(f, m_au.get_family_id(), OP_IDIV) && m_au.is_numeral(args[1], r) && r.is_zero()) {
- result = m_au.mk_int(0);
+ if (m_au.is_considered_uninterpreted(f, num, args)) {
+ result = m_au.mk_numeral(rational(0), f->get_range());
return BR_DONE;
}
return BR_FAILED;
diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
index ddce9fc09..81e8cf536 100644
--- a/src/nlsat/nlsat_evaluator.cpp
+++ b/src/nlsat/nlsat_evaluator.cpp
@@ -43,7 +43,7 @@ namespace nlsat {
svector<section> m_sections;
unsigned_vector m_sorted_sections; // refs to m_sections
unsigned_vector m_poly_sections; // refs to m_sections
- svector<int> m_poly_signs;
+ svector<polynomial::sign> m_poly_signs;
struct poly_info {
unsigned m_num_roots;
unsigned m_first_section; // idx in m_poly_sections;
@@ -149,18 +149,18 @@ namespace nlsat {
\brief Add polynomial with the given roots and signs.
*/
unsigned_vector p_section_ids;
- void add(anum_vector & roots, svector<int> & signs) {
+ void add(anum_vector & roots, svector<polynomial::sign> & signs) {
p_section_ids.reset();
if (!roots.empty())
merge(roots, p_section_ids);
unsigned first_sign = m_poly_signs.size();
unsigned first_section = m_poly_sections.size();
- unsigned num_signs = signs.size();
+ unsigned num_poly_signs = signs.size();
// Must normalize signs since we use arithmetic operations such as *
// during evaluation.
// Without normalization, overflows may happen, and wrong results may be produced.
- for (unsigned i = 0; i < num_signs; i++)
- m_poly_signs.push_back(normalize_sign(signs[i]));
+ for (unsigned i = 0; i < num_poly_signs; i++)
+ m_poly_signs.push_back(signs[i]);
m_poly_sections.append(p_section_ids);
m_info.push_back(poly_info(roots.size(), first_section, first_sign));
SASSERT(check_invariant());
@@ -169,10 +169,10 @@ namespace nlsat {
/**
\brief Add constant polynomial
*/
- void add_const(int sign) {
+ void add_const(polynomial::sign sign) {
unsigned first_sign = m_poly_signs.size();
unsigned first_section = m_poly_sections.size();
- m_poly_signs.push_back(normalize_sign(sign));
+ m_poly_signs.push_back(sign);
m_info.push_back(poly_info(0, first_section, first_sign));
}
@@ -226,12 +226,12 @@ namespace nlsat {
}
// Return the sign idx of pinfo
- int sign(poly_info const & pinfo, unsigned i) const {
+ polynomial::sign sign(poly_info const & pinfo, unsigned i) const {
return m_poly_signs[pinfo.m_first_sign + i];
}
#define LINEAR_SEARCH_THRESHOLD 8
- int sign_at(unsigned info_id, unsigned c) const {
+ polynomial::sign sign_at(unsigned info_id, unsigned c) const {
poly_info const & pinfo = m_info[info_id];
unsigned num_roots = pinfo.m_num_roots;
if (num_roots < LINEAR_SEARCH_THRESHOLD) {
@@ -239,7 +239,7 @@ namespace nlsat {
for (; i < num_roots; i++) {
unsigned section_cell_id = cell_id(pinfo, i);
if (section_cell_id == c)
- return 0;
+ return polynomial::sign_zero;
else if (section_cell_id > c)
break;
}
@@ -253,7 +253,7 @@ namespace nlsat {
if (c < root_1_cell_id)
return sign(pinfo, 0);
else if (c == root_1_cell_id || c == root_n_cell_id)
- return 0;
+ return polynomial::sign_zero;
else if (c > root_n_cell_id)
return sign(pinfo, num_roots);
int low = 0;
@@ -272,7 +272,7 @@ namespace nlsat {
SASSERT(low < mid && mid < high);
unsigned mid_cell_id = cell_id(pinfo, mid);
if (mid_cell_id == c) {
- return 0;
+ return polynomial::sign_zero;
}
if (c < mid_cell_id) {
high = mid;
@@ -319,7 +319,7 @@ namespace nlsat {
for (unsigned j = 0; j < num_cells(); j++) {
if (j > 0)
out << " ";
- int s = sign_at(i, j);
+ auto s = sign_at(i, j);
if (s < 0) out << "-";
else if (s == 0) out << "0";
else out << "+";
@@ -381,11 +381,10 @@ namespace nlsat {
\pre All variables of p are assigned in the current interpretation.
*/
- int eval_sign(poly * p) {
+ polynomial::sign eval_sign(poly * p) {
// TODO: check if it is useful to cache results
SASSERT(m_assignment.is_assigned(max_var(p)));
- int r = m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment);
- return r > 0 ? +1 : (r < 0 ? -1 : 0);
+ return m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment);
}
bool satisfied(int sign, atom::kind k) {
@@ -450,7 +449,7 @@ namespace nlsat {
return a->is_ineq_atom() ? eval_ineq(to_ineq_atom(a), neg) : eval_root(to_root_atom(a), neg);
}
- svector<int> m_add_signs_tmp;
+ svector<polynomial::sign> m_add_signs_tmp;
void add(poly * p, var x, sign_table & t) {
SASSERT(m_pm.max_var(p) <= x);
if (m_pm.max_var(p) < x) {
@@ -459,7 +458,7 @@ namespace nlsat {
else {
// isolate roots of p
scoped_anum_vector & roots = m_add_roots_tmp;
- svector<int> & signs = m_add_signs_tmp;
+ svector<polynomial::sign> & signs = m_add_signs_tmp;
roots.reset();
signs.reset();
TRACE("nlsat_evaluator", tout << "x: " << x << " max_var(p): " << m_pm.max_var(p) << "\n";);
@@ -471,18 +470,18 @@ namespace nlsat {
}
// Evaluate the sign of p1^e1*...*pn^en (of atom a) in cell c of table t.
- int sign_at(ineq_atom * a, sign_table const & t, unsigned c) const {
- int sign = 1;
+ polynomial::sign sign_at(ineq_atom * a, sign_table const & t, unsigned c) const {
+ auto sign = polynomial::sign_pos;
unsigned num_ps = a->size();
for (unsigned i = 0; i < num_ps; i++) {
- int curr_sign = t.sign_at(i, c);
+ polynomial::sign curr_sign = t.sign_at(i, c);
TRACE("nlsat_evaluator_bug", tout << "sign of i: " << i << " at cell " << c << "\n";
m_pm.display(tout, a->p(i));
tout << "\nsign: " << curr_sign << "\n";);
if (a->is_even(i) && curr_sign < 0)
- curr_sign = 1;
+ curr_sign = polynomial::sign_pos;
sign = sign * curr_sign;
- if (sign == 0)
+ if (sign == polynomial::sign_zero)
break;
}
return sign;
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 3f02ec672..3c3120d5d 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -197,9 +197,10 @@ namespace nlsat {
\brief Reset m_already_added vector using m_result
*/
void reset_already_added() {
- SASSERT(m_result != 0);
+ SASSERT(m_result != nullptr);
for (literal lit : *m_result)
m_already_added_literal[lit.index()] = false;
+ SASSERT(check_already_added());
}
@@ -207,9 +208,9 @@ namespace nlsat {
\brief evaluate the given polynomial in the current interpretation.
max_var(p) must be assigned in the current interpretation.
*/
- int sign(polynomial_ref const & p) {
+ polynomial::sign sign(polynomial_ref const & p) {
SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p)));
- int s = m_am.eval_sign_at(p, m_assignment);
+ auto s = m_am.eval_sign_at(p, m_assignment);
TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";);
return s;
}
@@ -270,7 +271,7 @@ namespace nlsat {
polynomial_ref f(m_pm);
for (unsigned i = 0; i < num_factors; i++) {
f = m_factors.get(i);
- if (sign(f) == 0) {
+ if (sign(f) == polynomial::sign_zero) {
m_zero_fs.push_back(m_factors.get(i));
m_is_even.push_back(false);
}
@@ -323,7 +324,7 @@ namespace nlsat {
return; // lc is a nonzero constant
lc = m_pm.coeff(p, x, k, reduct);
if (!is_zero(lc)) {
- if (sign(lc) != 0)
+ if (sign(lc) != polynomial::sign_zero)
return;
// lc is not the zero polynomial, but it vanished in the current interpretation.
// so we keep searching...
@@ -959,8 +960,9 @@ namespace nlsat {
if (ps.empty())
return;
m_todo.reset();
- for (unsigned i = 0; i < ps.size(); i++)
- m_todo.insert(ps.get(i));
+ for (poly* p : ps) {
+ m_todo.insert(p);
+ }
var x = m_todo.remove_max_polys(ps);
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
if (x < max_x)
@@ -983,8 +985,8 @@ namespace nlsat {
}
bool check_already_added() const {
- for (unsigned i = 0; i < m_already_added_literal.size(); i++) {
- SASSERT(m_already_added_literal[i] == false);
+ for (bool b : m_already_added_literal) {
+ SASSERT(!b);
}
return true;
}
@@ -1062,7 +1064,7 @@ namespace nlsat {
void simplify(literal l, eq_info & info, var max, scoped_literal & new_lit) {
bool_var b = l.var();
atom * a = m_atoms[b];
- SASSERT(a != 0);
+ SASSERT(a);
if (a->is_root_atom()) {
new_lit = l;
return;
@@ -1091,19 +1093,24 @@ namespace nlsat {
modified_lit = true;
unsigned d;
m_pm.pseudo_remainder(f, info.m_eq, info.m_x, d, new_factor);
+ polynomial_ref fact(f, m_pm), eq(const_cast<poly*>(info.m_eq), m_pm);
+
+ TRACE("nlsat_simplify_core", tout << "d: " << d << " factor " << fact << " eq " << eq << " new factor " << new_factor << "\n";);
// adjust sign based on sign of lc of eq
- if (d % 2 == 1 && // d is odd
- !is_even && // degree of the factor is odd
- info.m_lc_sign < 0 // lc of the eq is negative
- ) {
+ if (d % 2 == 1 && // d is odd
+ !is_even && // degree of the factor is odd
+ info.m_lc_sign < 0) { // lc of the eq is negative
atom_sign = -atom_sign; // flipped the sign of the current literal
+ TRACE("nlsat_simplify_core", tout << "odd degree\n";);
}
if (is_const(new_factor)) {
- int s = sign(new_factor);
- if (s == 0) {
+ TRACE("nlsat_simplify_core", tout << "new factor is const\n";);
+ polynomial::sign s = sign(new_factor);
+ if (s == polynomial::sign_zero) {
bool atom_val = a->get_kind() == atom::EQ;
bool lit_val = l.sign() ? !atom_val : atom_val;
new_lit = lit_val ? true_literal : false_literal;
+ TRACE("nlsat_simplify_core", tout << "zero sign: " << info.m_lc_const << "\n";);
if (!info.m_lc_const) {
// We have essentially shown the current factor must be zero If the leading coefficient is not zero.
// Note that, if the current factor is zero, then the whole polynomial is zero.
@@ -1115,6 +1122,7 @@ namespace nlsat {
return;
}
else {
+ TRACE("nlsat_simplify_core", tout << "non-zero sign: " << info.m_lc_const << "\n";);
// We have shown the current factor is a constant MODULO the sign of the leading coefficient (of the equation used to rewrite the factor).
if (!info.m_lc_const) {
// If the leading coefficient is not a constant, we must store this information as an extra assumption.
@@ -1266,11 +1274,9 @@ namespace nlsat {
var_vector m_select_tmp;
ineq_atom * select_lower_stage_eq(scoped_literal_vector & C, var max) {
var_vector & xs = m_select_tmp;
- unsigned sz = C.size();
- for (unsigned i = 0; i < sz; i++) {
- literal l = C[i];
+ for (literal l : C) {
bool_var b = l.var();
- atom * a = m_atoms[b];
+ atom * a = m_atoms[b];
if (a->is_root_atom())
continue; // we don't rewrite root atoms
ineq_atom * _a = to_ineq_atom(a);
@@ -1279,9 +1285,7 @@ namespace nlsat {
poly * p = _a->p(j);
xs.reset();
m_pm.vars(p, xs);
- unsigned xs_sz = xs.size();
- for (unsigned k = 0; k < xs_sz; k++) {
- var y = xs[k];
+ for (var y : xs) {
if (y >= max)
continue;
atom * eq = m_x2eq[y];
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 41c60c80d..d8beb0c63 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -766,7 +766,7 @@ namespace nlsat {
TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n";
display(tout););
IF_VERBOSE(0, display(verbose_stream() << "check lemma: ", n, cls) << "\n");
- for (clause* c : m_learned) IF_VERBOSE(0, display(verbose_stream() << "lemma: ", *c) << "\n");
+ for (clause* c : m_learned) IF_VERBOSE(1, display(verbose_stream() << "lemma: ", *c) << "\n");
solver solver2(m_ctx);
imp& checker = *(solver2.m_imp);
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 3125287bd..73f7ffe72 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -439,7 +439,6 @@ void asserted_formulas::commit() {
}
void asserted_formulas::commit(unsigned new_qhead) {
- TRACE("asserted_formulas", tout << "commit " << new_qhead << "\n";);
m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.c_ptr() + m_qhead);
m_expr2depth.reset();
for (unsigned i = m_qhead; i < new_qhead; ++i) {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 2eb0aa8c4..8597bd144 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -474,11 +474,11 @@ bool theory_seq::branch_binary_variable(eq const& e) {
return true;
}
if (!get_length(x, lenX)) {
- enforce_length(x);
+ add_length_to_eqc(x);
return true;
}
if (!get_length(y, lenY)) {
- enforce_length(y);
+ add_length_to_eqc(y);
return true;
}
if (lenX + rational(xs.size()) != lenY + rational(ys.size())) {
@@ -555,7 +555,7 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
rational lenX;
if (!get_length(X, lenX)) {
TRACE("seq", tout << "enforce length on " << mk_bounded_pp(X, m, 2) << "\n";);
- enforce_length(X);
+ add_length_to_eqc(X);
return;
}
if (lenX > rational(units.size())) {
@@ -732,13 +732,13 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
rational lenX, lenY1, lenY2;
context& ctx = get_context();
if (!get_length(x, lenX)) {
- enforce_length(x);
+ add_length_to_eqc(x);
}
if (!get_length(y1, lenY1)) {
- enforce_length(y1);
+ add_length_to_eqc(y1);
}
if (!get_length(y2, lenY2)) {
- enforce_length(y2);
+ add_length_to_eqc(y2);
}
SASSERT(!xs.empty() && !ys.empty());
@@ -848,13 +848,13 @@ bool theory_seq::branch_ternary_variable2(eq const& e, bool flag1) {
rational lenX, lenY1, lenY2;
context& ctx = get_context();
if (!get_length(x, lenX)) {
- enforce_length(x);
+ add_length_to_eqc(x);
}
if (!get_length(y1, lenY1)) {
- enforce_length(y1);
+ add_length_to_eqc(y1);
}
if (!get_length(y2, lenY2)) {
- enforce_length(y2);
+ add_length_to_eqc(y2);
}
SASSERT(!xs.empty() && !ys.empty());
unsigned_vector indexes = overlap2(xs, ys);
@@ -922,16 +922,16 @@ bool theory_seq::branch_quat_variable(eq const& e) {
rational lenX1, lenX2, lenY1, lenY2;
context& ctx = get_context();
if (!get_length(x1_l, lenX1)) {
- enforce_length(x1_l);
+ add_length_to_eqc(x1_l);
}
if (!get_length(y1_l, lenY1)) {
- enforce_length(y1_l);
+ add_length_to_eqc(y1_l);
}
if (!get_length(x2, lenX2)) {
- enforce_length(x2);
+ add_length_to_eqc(x2);
}
if (!get_length(y2, lenY2)) {
- enforce_length(y2);
+ add_length_to_eqc(y2);
}
SASSERT(!xs.empty() && !ys.empty());
@@ -1608,7 +1608,7 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & le
len.push_back(val);
}
else {
- enforce_length(e);
+ add_length_to_eqc(e);
all_have_length = false;
}
}
@@ -1897,7 +1897,6 @@ bool theory_seq::check_length_coherence0(expr* e) {
bool theory_seq::check_length_coherence() {
-#if 1
for (expr* l : m_length) {
expr* e = nullptr;
VERIFY(m_util.str.is_length(l, e));
@@ -1905,15 +1904,18 @@ bool theory_seq::check_length_coherence() {
return true;
}
}
-#endif
+ bool change = false;
for (expr* l : m_length) {
expr* e = nullptr;
VERIFY(m_util.str.is_length(l, e));
if (check_length_coherence(e)) {
return true;
}
+ if (add_length_to_eqc(e)) {
+ change = true;
+ }
}
- return false;
+ return change;
}
bool theory_seq::fixed_length(bool is_zero) {
@@ -2270,16 +2272,16 @@ bool theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vect
}
}
if (!asserted) {
- std::cout << "not asserted\n";
+ IF_VERBOSE(0, verbose_stream() << "not asserted\n";);
context& ctx = get_context();
for (assumption const& a : assumptions) {
if (a.lit != null_literal) {
- std::cout << a.lit << " " << ctx.get_assignment(a.lit) << " ";
- ctx.display_literal_info(std::cout, a.lit);
- ctx.display_detailed_literal(std::cout, a.lit) << "\n";
+ IF_VERBOSE(0,
+ verbose_stream() << a.lit << " " << ctx.get_assignment(a.lit) << " ";
+ ctx.display_literal_info(verbose_stream(), a.lit);
+ ctx.display_detailed_literal(verbose_stream(), a.lit) << "\n";);
}
}
- // ctx.display(std::cout);
exit(0);
}
return asserted;
@@ -2390,14 +2392,15 @@ bool theory_seq::propagate_eq(dependency* dep, literal lit, expr* e1, expr* e2,
void theory_seq::enforce_length_coherence(enode* n1, enode* n2) {
expr* o1 = n1->get_owner();
expr* o2 = n2->get_owner();
+ // std::cout << mk_pp(o1, m) << " " << mk_pp(o2, m) << " " << has_length(o1) << " " << has_length(o2) << "\n";
if (m_util.str.is_concat(o1) && m_util.str.is_concat(o2)) {
return;
}
if (has_length(o1) && !has_length(o2)) {
- enforce_length(o2);
+ add_length_to_eqc(o2);
}
else if (has_length(o2) && !has_length(o1)) {
- enforce_length(o1);
+ add_length_to_eqc(o1);
}
}
@@ -3355,8 +3358,8 @@ bool theory_seq::solve_nc(unsigned idx) {
if (ctx.get_assignment(len_gt) == l_true) {
VERIFY(m_util.str.is_contains(n.contains(), a, b));
- enforce_length(a);
- enforce_length(b);
+ add_length_to_eqc(a);
+ add_length_to_eqc(b);
TRACE("seq", tout << len_gt << " is true\n";);
return true;
}
@@ -3640,19 +3643,22 @@ void theory_seq::add_length(expr* e, expr* l) {
/*
ensure that all elements in equivalence class occur under an application of 'length'
*/
-void theory_seq::enforce_length(expr* e) {
+bool theory_seq::add_length_to_eqc(expr* e) {
enode* n = ensure_enode(e);
enode* n1 = n;
+ bool change = false;
do {
expr* o = n->get_owner();
if (!has_length(o)) {
expr_ref len(m_util.str.mk_length(o), m);
enque_axiom(len);
add_length(o, len);
+ change = true;
}
n = n->get_next();
}
while (n1 != n);
+ return change;
}
@@ -3733,7 +3739,7 @@ bool theory_seq::add_itos_val_axiom(expr* e) {
if (m_util.str.is_stoi(n)) {
return false;
}
- enforce_length(e);
+ add_length_to_eqc(e);
if (get_length(e, val) && val.is_pos() && val.is_unsigned() && (!m_si_axioms.find(e, val2) || val != val2)) {
add_si_axiom(e, n, val.get_unsigned());
@@ -3756,7 +3762,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
if (m_util.str.is_itos(n)) {
return false;
}
- enforce_length(n);
+ add_length_to_eqc(n);
if (get_length(n, val) && val.is_pos() && val.is_unsigned() && (!m_si_axioms.find(e, val2) || val2 != val)) {
add_si_axiom(n, e, val.get_unsigned());
@@ -4564,7 +4570,7 @@ void theory_seq::deque_axiom(expr* n) {
add_length_axiom(n);
}
else if (m_util.str.is_empty(n) && !has_length(n) && !m_has_length.empty()) {
- enforce_length(n);
+ add_length_to_eqc(n);
}
else if (m_util.str.is_index(n)) {
add_indexof_axiom(n);
@@ -5906,7 +5912,7 @@ void theory_seq::relevant_eh(app* n) {
expr* arg;
if (m_util.str.is_length(n, arg) && !has_length(arg) && get_context().e_internalized(arg)) {
- enforce_length(arg);
+ add_length_to_eqc(arg);
}
}
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 6be5b3b2c..16503cd40 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -592,7 +592,7 @@ namespace smt {
bool has_length(expr *e) const { return m_has_length.contains(e); }
void add_length(expr* e, expr* l);
- void enforce_length(expr* n);
+ bool add_length_to_eqc(expr* n);
bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
void enforce_length_coherence(enode* n1, enode* n2);