mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

fix #2613 fix #2612

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-05 16:57:51 -07:00
parent 016732aa59
commit 39edf73e78
16 changed files with 222 additions and 162 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/ast/arith_decl_plugin.cpp
View file

@ -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);
}

3
src/ast/arith_decl_plugin.h
View file

@ -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);
};

67
src/math/polynomial/algebraic_numbers.cpp
View file

@ -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);
}

4
src/math/polynomial/algebraic_numbers.h
View file

@ -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);

42
src/math/polynomial/polynomial.cpp
View file

@ -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);
}

11
src/math/polynomial/polynomial.h
View file

@ -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.
*/

1
src/math/polynomial/polynomial_cache.cpp
View file

@ -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);

40
src/math/polynomial/upolynomial.cpp
View file

@ -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]);

22
src/math/polynomial/upolynomial.h
View file

@ -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

9
src/model/model_evaluator.cpp
View file

@ -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;

45
src/nlsat/nlsat_evaluator.cpp
View file

@ -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;

50
src/nlsat/nlsat_explain.cpp
View file

@ -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];

2
src/nlsat/nlsat_solver.cpp
View file

@ -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);

1
src/smt/asserted_formulas.cpp
View file

@ -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) {

68
src/smt/theory_seq.cpp
View file

@ -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);
}
}

2
src/smt/theory_seq.h
View file

@ -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);