mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

move out sign

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-19 09:34:22 -06:00
parent 89c91765f6
commit d3b105f9f8
15 changed files with 176 additions and 168 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/ast/ast.cpp
View file

@ -744,7 +744,6 @@ basic_decl_plugin::basic_decl_plugin():
m_th_assumption_add_decl(nullptr),
m_th_lemma_add_decl(nullptr),
m_redundant_del_decl(nullptr),
m_clause_trail_decl(nullptr),
m_hyper_res_decl0(nullptr) {
}
@ -835,9 +834,9 @@ func_decl * basic_decl_plugin::mk_compressed_proof_decl(char const * name, basic
func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector<func_decl> & cache) {
if (num_parents >= cache.size()) {
cache.resize(num_parents+1);
cache.resize(num_parents+1, nullptr);
}
if (cache[num_parents] == 0) {
if (!cache[num_parents]) {
cache[num_parents] = mk_proof_decl(name, k, num_parents);
}
return cache[num_parents];
@ -920,7 +919,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_TH_ASSUMPTION_ADD: return mk_proof_decl("add-th-assume", k, num_parents, m_th_assumption_add_decl);
case PR_TH_LEMMA_ADD: return mk_proof_decl("add-th-lemma", k, num_parents, m_th_lemma_add_decl);
case PR_REDUNDANT_DEL: return mk_proof_decl("del-redundant", k, num_parents, m_redundant_del_decl);
case PR_CLAUSE_TRAIL: return mk_proof_decl("proof-trail", k, num_parents, m_clause_trail_decl);
case PR_CLAUSE_TRAIL: return mk_proof_decl("proof-trail", k, num_parents);
default:
UNREACHABLE();
return nullptr;
@ -1041,7 +1040,6 @@ void basic_decl_plugin::finalize() {
DEC_REF(m_th_assumption_add_decl);
DEC_REF(m_th_lemma_add_decl);
DEC_REF(m_redundant_del_decl);
DEC_REF(m_clause_trail_decl);
DEC_ARRAY_REF(m_apply_def_decls);
DEC_ARRAY_REF(m_nnf_pos_decls);
DEC_ARRAY_REF(m_nnf_neg_decls);
@ -1900,6 +1898,22 @@ ast * ast_manager::register_node_core(ast * n) {
default:
break;
}
#if 0
// std::cout << n->m_id << " " << n->hash() << "\n";
if (n->m_id == 1523) {
std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
}
if (n->m_id == 1524) {
std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
VERIFY(false);
}
if (n->m_id == 1525) {
std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
}
//VERIFY(n->m_id != 1549);
//VERIFY(s_count != 2);
#endif
return n;
}

1
src/ast/ast.h
View file

@ -1167,7 +1167,6 @@ protected:
func_decl * m_th_assumption_add_decl;
func_decl * m_th_lemma_add_decl;
func_decl * m_redundant_del_decl;
func_decl * m_clause_trail_decl;
ptr_vector<func_decl> m_apply_def_decls;
ptr_vector<func_decl> m_nnf_pos_decls;
ptr_vector<func_decl> m_nnf_neg_decls;

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

@ -126,7 +126,7 @@ namespace algebraic_numbers {
bool acell_inv(algebraic_cell const& c) {
auto s = upm().eval_sign_at(c.m_p_sz, c.m_p, lower(&c));
return s == polynomial::sign_zero || c.m_sign_lower == (s == polynomial::sign_neg);
return s == sign_zero || c.m_sign_lower == (s == sign_neg);
}
void checkpoint() {
@ -262,7 +262,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) == polynomial::sign_zero) {
if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == sign_zero) {
m_wrapper.set(a, candidate);
return true;
}
@ -325,7 +325,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) == polynomial::sign_zero) {
if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == sign_zero) {
saved_a.restore_if_too_small();
set(a, candidate);
return true;
@ -371,8 +371,8 @@ namespace algebraic_numbers {
return c;
}
polynomial::sign sign_lower(algebraic_cell * c) const {
return c->m_sign_lower == 0 ? polynomial::sign_pos : polynomial::sign_neg;
sign sign_lower(algebraic_cell * c) const {
return c->m_sign_lower == 0 ? sign_pos : sign_neg;
}
mpbq const & lower(algebraic_cell const * c) const { return c->m_interval.lower(); }
@ -384,11 +384,11 @@ namespace algebraic_numbers {
mpbq & upper(algebraic_cell * c) { return c->m_interval.upper(); }
void update_sign_lower(algebraic_cell * c) {
polynomial::sign sl = upm().eval_sign_at(c->m_p_sz, c->m_p, lower(c));
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 != polynomial::sign_zero);
SASSERT(sl != sign_zero);
SASSERT(upm().eval_sign_at(c->m_p_sz, c->m_p, upper(c)) == -sl);
c->m_sign_lower = sl == polynomial::sign_neg;
c->m_sign_lower = sl == sign_neg;
SASSERT(acell_inv(*c));
}
@ -1607,14 +1607,14 @@ namespace algebraic_numbers {
if (!bqm().is_zero(_lower) && !bqm().is_zero(_upper))
return;
auto sign_l = sign_lower(cell_a);
SASSERT(!polynomial::is_zero(sign_l));
SASSERT(!::is_zero(sign_l));
auto sign_u = -sign_l;
#define REFINE_LOOP(BOUND, TARGET_SIGN) \
while (true) { \
bqm().div2(BOUND); \
polynomial::sign new_sign = upm().eval_sign_at(cell_a->m_p_sz, cell_a->m_p, BOUND); \
if (new_sign == polynomial::sign_zero) { \
sign new_sign = upm().eval_sign_at(cell_a->m_p_sz, cell_a->m_p, BOUND); \
if (new_sign == sign_zero) { \
/* found actual root */ \
scoped_mpq r(qm()); \
to_mpq(qm(), BOUND, r); \
@ -1689,10 +1689,10 @@ namespace algebraic_numbers {
}
// Todo: move to MPQ
int compare(mpq const & a, mpq const & b) {
::sign compare(mpq const & a, mpq const & b) {
if (qm().eq(a, b))
return 0;
return qm().lt(a, b) ? -1 : 1;
return sign_zero;
return qm().lt(a, b) ? sign_neg : sign_pos;
}
/**
@ -1710,18 +1710,18 @@ namespace algebraic_numbers {
p(b) == 0 then c == b
(p(b) < 0) == (p(l) < 0) then c > b else c < b
*/
int compare(algebraic_cell * c, mpq const & b) {
::sign compare(algebraic_cell * c, mpq const & b) {
mpbq const & l = lower(c);
mpbq const & u = upper(c);
if (bqm().le(u, b))
return -1;
return sign_neg;
if (bqm().ge(l, b))
return 1;
return sign_pos;
// b is in the isolating interval (l, u)
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;
if (sign_b == sign_zero)
return sign_zero;
return sign_b == sign_lower(c) ? sign_pos : sign_neg;
}
// Return true if the polynomials of cell_a and cell_b are the same.
@ -1729,7 +1729,7 @@ namespace algebraic_numbers {
return upm().eq(cell_a->m_p_sz, cell_a->m_p, cell_b->m_p_sz, cell_b->m_p);
}
int compare_core(numeral & a, numeral & b) {
::sign compare_core(numeral & a, numeral & b) {
SASSERT(!a.is_basic() && !b.is_basic());
algebraic_cell * cell_a = a.to_algebraic();
algebraic_cell * cell_b = b.to_algebraic();
@ -1741,11 +1741,11 @@ namespace algebraic_numbers {
#define COMPARE_INTERVAL() \
if (bqm().le(a_upper, b_lower)) { \
m_compare_cheap++; \
return -1; \
return sign_neg; \
} \
if (bqm().ge(a_lower, b_upper)) { \
m_compare_cheap++; \
return 1; \
return sign_pos; \
}
COMPARE_INTERVAL();
@ -1755,7 +1755,7 @@ namespace algebraic_numbers {
// the same root.
if (compare_p(cell_a, cell_b)) {
m_compare_poly_eq++;
return 0;
return sign_zero;
}
TRACE("algebraic", tout << "comparing\n";
@ -1786,8 +1786,8 @@ namespace algebraic_numbers {
}
}
if (!m_limit.inc())
return 0;
if (!m_limit.inc())
return sign_zero;
// make sure that intervals of a and b have the same magnitude
int a_m = magnitude(a_lower, a_upper);
@ -1843,11 +1843,11 @@ namespace algebraic_numbers {
TRACE("algebraic", tout << "comparing using sturm\n"; display_interval(tout, a); tout << "\n"; display_interval(tout, b); tout << "\n";
tout << "V: " << V << ", sign_lower(a): " << sign_lower(cell_a) << ", sign_lower(b): " << sign_lower(cell_b) << "\n";);
if (V == 0)
return 0;
return sign_zero;
if ((V < 0) == (sign_lower(cell_b) < 0))
return -1;
return sign_neg;
else
return 1;
return sign_pos;
// Here is an unexplored option for comparing numbers.
//
@ -1883,7 +1883,7 @@ namespace algebraic_numbers {
// (l1 - u2, u1 - l2) contains only one root of r(x)
}
int compare(numeral & a, numeral & b) {
::sign compare(numeral & a, numeral & b) {
TRACE("algebraic", tout << "comparing: "; display_interval(tout, a); tout << " "; display_interval(tout, b); tout << "\n";);
if (a.is_basic()) {
if (b.is_basic())
@ -2002,7 +2002,7 @@ namespace algebraic_numbers {
};
polynomial::var_vector m_eval_sign_vars;
polynomial::sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
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) {
@ -2013,7 +2013,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 polynomial::to_sign(qm().sign(r));
return ::to_sign(qm().sign(r));
}
catch (const opt_var2basic::failed &) {
// continue
@ -2027,13 +2027,13 @@ namespace algebraic_numbers {
if (ext_pm.is_zero(p_prime)) {
// polynomial vanished after substituting rational values.
return polynomial::sign_zero;
return sign_zero;
}
if (is_const(p_prime)) {
// polynomial became the constant polynomial after substitution.
SASSERT(size(p_prime) == 1);
return polynomial::to_sign(ext_pm.m().sign(ext_pm.coeff(p_prime, 0)));
return to_sign(ext_pm.m().sign(ext_pm.coeff(p_prime, 0)));
}
// Try to find sign using intervals
@ -2049,7 +2049,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) ? polynomial::sign_pos : polynomial::sign_neg;
return bqim().is_pos(ri) ? sign_pos : sign_neg;
}
// refine intervals if magnitude > m_min_magnitude
bool refined = false;
@ -2090,7 +2090,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 polynomial::sign_zero;
return sign_zero;
}
#if 0
// Evaluating sign using algebraic arithmetic
@ -2163,7 +2163,7 @@ namespace algebraic_numbers {
bqm().div2k(mL, k);
bqm().div2k(L, k);
if (bqm().lt(mL, ri.lower()) && bqm().lt(ri.upper(), L))
return polynomial::sign_zero;
return sign_zero;
// keep refining ri until ri is inside (-L, L) or
// ri does not contain zero.
@ -2186,11 +2186,11 @@ 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) ? polynomial::sign_pos : polynomial::sign_neg;
return bqim().is_pos(ri) ? sign_pos : sign_neg;
}
if (bqm().lt(mL, ri.lower()) && bqm().lt(ri.upper(), L))
return polynomial::sign_zero;
return sign_zero;
for (auto x : xs) {
SASSERT(x2v.contains(x));
@ -2265,7 +2265,7 @@ namespace algebraic_numbers {
checkpoint();
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";);
polynomial::sign sign = eval_sign_at(p, ext_x2v);
sign sign = eval_sign_at(p, ext_x2v);
TRACE("isolate_roots", tout << "filter_roots i: " << i << ", result sign: " << sign << "\n";);
if (sign != 0)
continue;
@ -2468,7 +2468,7 @@ namespace algebraic_numbers {
}
}
polynomial::sign eval_at_mpbq(polynomial_ref const & p, polynomial::var2anum const & x2v, polynomial::var x, mpbq const & v) {
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);
@ -2583,13 +2583,13 @@ namespace algebraic_numbers {
#define DEFAULT_PRECISION 2
void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<polynomial::sign> & signs) {
void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<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);
polynomial::sign s = eval_sign_at(p, ext_x2v);
sign s = eval_sign_at(p, ext_x2v);
signs.push_back(s);
}
else {
@ -2617,7 +2617,7 @@ namespace algebraic_numbers {
{
ext2_var2num ext_x2v(m_wrapper, x2v, w);
auto s = eval_sign_at(p, ext_x2v);
SASSERT(s != polynomial::sign_zero);
SASSERT(s != sign_zero);
signs.push_back(s);
}
@ -2627,7 +2627,7 @@ namespace algebraic_numbers {
select(prev, curr, w);
ext2_var2num ext_x2v(m_wrapper, x2v, w);
auto s = eval_sign_at(p, ext_x2v);
SASSERT(s != polynomial::sign_zero);
SASSERT(s != sign_zero);
signs.push_back(s);
}
@ -2635,7 +2635,7 @@ namespace algebraic_numbers {
{
ext2_var2num ext_x2v(m_wrapper, x2v, w);
auto s = eval_sign_at(p, ext_x2v);
SASSERT(s != polynomial::sign_zero);
SASSERT(s != sign_zero);
signs.push_back(s);
}
}
@ -2894,7 +2894,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<polynomial::sign> & signs) {
void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<sign> & signs) {
m_imp->isolate_roots(p, x2v, roots, signs);
}
@ -2952,7 +2952,7 @@ namespace algebraic_numbers {
m_imp->inv(a);
}
int manager::compare(numeral const & a, numeral const & b) {
sign manager::compare(numeral const & a, numeral const & b) {
return m_imp->compare(const_cast<numeral&>(a), const_cast<numeral&>(b));
}
@ -3052,7 +3052,7 @@ namespace algebraic_numbers {
l = rational(_l);
}
polynomial::sign manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
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);
}

6
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<polynomial::sign> & signs);
void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<sign> & signs);
/**
\brief Store in r the i-th root of p.
@ -250,7 +250,7 @@ namespace algebraic_numbers {
Return 0 if a == b
Return 1 if a > b
*/
int compare(numeral const & a, numeral const & b);
sign compare(numeral const & a, numeral const & b);
/**
\brief a == b
@ -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
*/
polynomial::sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v);
sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v);
void get_polynomial(numeral const & a, svector<mpz> & r);

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

@ -30,6 +30,7 @@ Notes:
#include "util/mpbqi.h"
#include "util/rlimit.h"
#include "util/lbool.h"
#include "util/sign.h"
class small_object_allocator;
@ -44,12 +45,6 @@ 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); }
inline bool is_zero(sign s) { return s == sign_zero; }
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);

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

@ -1327,25 +1327,25 @@ namespace upolynomial {
div(sz, p, 2, two_x_1, buffer);
}
polynomial::sign manager::sign_of(numeral const & c) {
sign manager::sign_of(numeral const & c) {
if (m().is_zero(c))
return polynomial::sign_zero;
return sign_zero;
if (m().is_pos(c))
return polynomial::sign_pos;
return sign_pos;
else
return polynomial::sign_neg;
return 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;
auto prev_sign = polynomial::sign_zero;
auto prev_sign = sign_zero;
unsigned i = 0;
for (; i < sz; i++) {
auto sign = sign_of(p[i]);
if (sign == polynomial::sign_zero)
if (sign == sign_zero)
continue;
if (sign != prev_sign && prev_sign != polynomial::sign_zero)
if (sign != prev_sign && prev_sign != sign_zero)
r++;
prev_sign = sign;
}
@ -1375,7 +1375,7 @@ namespace upolynomial {
}
return sign_changes(Q.size(), Q.c_ptr());
#endif
polynomial::sign prev_sign = polynomial::sign_zero;
sign prev_sign = sign_zero;
unsigned num_vars = 0;
// a0 a1 a2 a3
// a0 a0+a1 a0+a1+a2 a0+a1+a2+a3
@ -1389,9 +1389,9 @@ namespace upolynomial {
m().add(Q[k], Q[k-1], Q[k]);
}
auto sign = sign_of(Q[k-1]);
if (polynomial::is_zero(sign))
if (::is_zero(sign))
continue;
if (sign != prev_sign && !polynomial::is_zero(prev_sign)) {
if (sign != prev_sign && !::is_zero(prev_sign)) {
num_vars++;
if (num_vars > 1)
return num_vars;
@ -1729,14 +1729,14 @@ namespace upolynomial {
}
// Evaluate the sign of p(b)
polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpbq const & b) {
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 polynomial::sign_zero;
return 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)
polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpq const & b) {
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 polynomial::sign_zero;
return 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)
polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpz const & b) {
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 polynomial::sign_zero;
return sign_zero;
if (sz == 1)
return sign_of(p[0]);
scoped_numeral r(m());
@ -1817,21 +1817,21 @@ namespace upolynomial {
return sign_of(r);
}
polynomial::sign manager::eval_sign_at_zero(unsigned sz, numeral const * p) {
sign manager::eval_sign_at_zero(unsigned sz, numeral const * p) {
if (sz == 0)
return polynomial::sign_zero;
return sign_zero;
return sign_of(p[0]);
}
polynomial::sign manager::eval_sign_at_plus_inf(unsigned sz, numeral const * p) {
sign manager::eval_sign_at_plus_inf(unsigned sz, numeral const * p) {
if (sz == 0)
return polynomial::sign_zero;
return sign_zero;
return sign_of(p[sz-1]);
}
polynomial::sign manager::eval_sign_at_minus_inf(unsigned sz, numeral const * p) {
sign manager::eval_sign_at_minus_inf(unsigned sz, numeral const * p) {
if (sz == 0)
return polynomial::sign_zero;
return sign_zero;
unsigned degree = sz - 1;
if (degree % 2 == 0)
return sign_of(p[sz-1]);
@ -2751,7 +2751,7 @@ namespace upolynomial {
The arguments sign_a and sign_b must contain the values returned by
eval_sign_at(sz, p, a) and eval_sign_at(sz, p, b).
*/
bool manager::refine_core(unsigned sz, numeral const * p, polynomial::sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b) {
bool manager::refine_core(unsigned sz, numeral const * p, sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b) {
SASSERT(sign_a == eval_sign_at(sz, p, a));
SASSERT(-sign_a == eval_sign_at(sz, p, b));
SASSERT(sign_a != 0);
@ -2759,7 +2759,7 @@ namespace upolynomial {
bqm.add(a, b, mid);
bqm.div2(mid);
auto sign_mid = eval_sign_at(sz, p, mid);
if (polynomial::is_zero(sign_mid)) {
if (::is_zero(sign_mid)) {
swap(mid, a);
return false;
}
@ -2774,8 +2774,8 @@ namespace upolynomial {
// See refine_core
bool manager::refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b) {
polynomial::sign sign_a = eval_sign_at(sz, p, a);
SASSERT(!polynomial::is_zero(sign_a));
sign sign_a = eval_sign_at(sz, p, a);
SASSERT(!::is_zero(sign_a));
return refine_core(sz, p, sign_a, bqm, a, b);
}
@ -2784,8 +2784,8 @@ namespace upolynomial {
//
// Return TRUE, if interval was squeezed, and new interval is stored in (a,b).
// Return FALSE, if the actual root was found, it is stored in a.
bool manager::refine_core(unsigned sz, numeral const * p, polynomial::sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k) {
SASSERT(sign_a != polynomial::sign_zero);
bool manager::refine_core(unsigned sz, numeral const * p, sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k) {
SASSERT(sign_a != sign_zero);
SASSERT(sign_a == eval_sign_at(sz, p, a));
SASSERT(-sign_a == eval_sign_at(sz, p, b));
scoped_mpbq w(bqm);
@ -2802,16 +2802,16 @@ namespace upolynomial {
}
bool manager::refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k) {
polynomial::sign sign_a = eval_sign_at(sz, p, a);
sign sign_a = eval_sign_at(sz, p, a);
SASSERT(eval_sign_at(sz, p, b) == -sign_a);
SASSERT(sign_a != 0);
return refine_core(sz, p, sign_a, bqm, a, b, prec_k);
}
bool manager::convert_q2bq_interval(unsigned sz, numeral const * p, mpq const & a, mpq const & b, mpbq_manager & bqm, mpbq & c, mpbq & d) {
polynomial::sign sign_a = eval_sign_at(sz, p, a);
polynomial::sign sign_b = eval_sign_at(sz, p, b);
SASSERT(!polynomial::is_zero(sign_a) && !polynomial::is_zero(sign_b));
sign sign_a = eval_sign_at(sz, p, a);
sign sign_b = eval_sign_at(sz, p, b);
SASSERT(!::is_zero(sign_a) && !::is_zero(sign_b));
SASSERT(sign_a == -sign_b);
bool found_d = false;
TRACE("convert_bug",
@ -2843,7 +2843,7 @@ namespace upolynomial {
SASSERT(bqm.lt(upper, b));
while (true) {
auto sign_upper = eval_sign_at(sz, p, upper);
if (polynomial::is_zero(sign_upper)) {
if (::is_zero(sign_upper)) {
// found root
bqm.swap(c, upper);
bqm.del(lower); bqm.del(upper);
@ -2887,8 +2887,8 @@ namespace upolynomial {
SASSERT(bqm.lt(lower, upper));
SASSERT(bqm.lt(lower, b));
while (true) {
polynomial::sign sign_lower = eval_sign_at(sz, p, lower);
if (polynomial::is_zero(sign_lower)) {
sign sign_lower = eval_sign_at(sz, p, lower);
if (::is_zero(sign_lower)) {
// found root
bqm.swap(c, lower);
bqm.del(lower); bqm.del(upper);

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

@ -554,7 +554,7 @@ namespace upolynomial {
numeral_vector m_tr_tmp;
numeral_vector m_push_tmp;
polynomial::sign sign_of(numeral const & c);
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)
*/
polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpbq const & b);
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);
sign eval_sign_at(unsigned sz, numeral const * p, mpq const & b);
/**
\brief Evaluate the sign of p(b)
*/
polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpz const & b);
sign eval_sign_at(unsigned sz, numeral const * p, mpz const & b);
/**
\brief Evaluate the sign of p(0)
*/
polynomial::sign eval_sign_at_zero(unsigned sz, numeral const * p);
sign eval_sign_at_zero(unsigned sz, numeral const * p);
/**
\brief Evaluate the sign of p(+oo)
*/
polynomial::sign eval_sign_at_plus_inf(unsigned sz, numeral const * p);
sign eval_sign_at_plus_inf(unsigned sz, numeral const * p);
/**
\brief Evaluate the sign of p(-oo)
*/
polynomial::sign eval_sign_at_minus_inf(unsigned sz, numeral const * p);
sign eval_sign_at_minus_inf(unsigned sz, numeral const * p);
/**
\brief Evaluate the sign variations in the polynomial sequence at -oo
@ -863,11 +863,11 @@ namespace upolynomial {
// Return FALSE, if the actual root was found, it is stored in a.
//
// See upolynomial.cpp for additional comments
bool refine_core(unsigned sz, numeral const * p, polynomial::sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b);
bool refine_core(unsigned sz, numeral const * p, sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b);
bool refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b);
bool refine_core(unsigned sz, numeral const * p, polynomial::sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k);
bool refine_core(unsigned sz, numeral const * p, sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k);
bool refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k);
/////////////////////

32
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<polynomial::sign> m_poly_signs;
svector<sign> m_poly_signs;
struct poly_info {
unsigned m_num_roots;
unsigned m_first_section; // idx in m_poly_sections;
@ -149,7 +149,7 @@ namespace nlsat {
\brief Add polynomial with the given roots and signs.
*/
unsigned_vector p_section_ids;
void add(anum_vector & roots, svector<polynomial::sign> & signs) {
void add(anum_vector & roots, svector<sign> & signs) {
p_section_ids.reset();
if (!roots.empty())
merge(roots, p_section_ids);
@ -169,7 +169,7 @@ namespace nlsat {
/**
\brief Add constant polynomial
*/
void add_const(polynomial::sign sign) {
void add_const(sign sign) {
unsigned first_sign = m_poly_signs.size();
unsigned first_section = m_poly_sections.size();
m_poly_signs.push_back(sign);
@ -226,12 +226,12 @@ namespace nlsat {
}
// Return the sign idx of pinfo
polynomial::sign sign(poly_info const & pinfo, unsigned i) const {
::sign sign(poly_info const & pinfo, unsigned i) const {
return m_poly_signs[pinfo.m_first_sign + i];
}
#define LINEAR_SEARCH_THRESHOLD 8
polynomial::sign sign_at(unsigned info_id, unsigned c) const {
::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 polynomial::sign_zero;
return 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 polynomial::sign_zero;
return 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 polynomial::sign_zero;
return sign_zero;
}
if (c < mid_cell_id) {
high = mid;
@ -381,7 +381,7 @@ namespace nlsat {
\pre All variables of p are assigned in the current interpretation.
*/
polynomial::sign eval_sign(poly * p) {
sign eval_sign(poly * p) {
// TODO: check if it is useful to cache results
SASSERT(m_assignment.is_assigned(max_var(p)));
return m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment);
@ -449,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<polynomial::sign> m_add_signs_tmp;
svector<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) {
@ -458,7 +458,7 @@ namespace nlsat {
else {
// isolate roots of p
scoped_anum_vector & roots = m_add_roots_tmp;
svector<polynomial::sign> & signs = m_add_signs_tmp;
svector<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";);
@ -470,18 +470,18 @@ namespace nlsat {
}
// Evaluate the sign of p1^e1*...*pn^en (of atom a) in cell c of table t.
polynomial::sign sign_at(ineq_atom * a, sign_table const & t, unsigned c) const {
auto sign = polynomial::sign_pos;
sign sign_at(ineq_atom * a, sign_table const & t, unsigned c) const {
auto sign = sign_pos;
unsigned num_ps = a->size();
for (unsigned i = 0; i < num_ps; i++) {
polynomial::sign curr_sign = t.sign_at(i, c);
::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 = polynomial::sign_pos;
curr_sign = sign_pos;
sign = sign * curr_sign;
if (sign == polynomial::sign_zero)
if (is_zero(sign))
break;
}
return sign;

12
src/nlsat/nlsat_explain.cpp
View file

@ -208,7 +208,7 @@ namespace nlsat {
\brief evaluate the given polynomial in the current interpretation.
max_var(p) must be assigned in the current interpretation.
*/
polynomial::sign sign(polynomial_ref const & p) {
::sign sign(polynomial_ref const & p) {
SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p)));
auto s = m_am.eval_sign_at(p, m_assignment);
TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";);
@ -271,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) == polynomial::sign_zero) {
if (is_zero(sign(f))) {
m_zero_fs.push_back(m_factors.get(i));
m_is_even.push_back(false);
}
@ -338,7 +338,7 @@ namespace nlsat {
lc = m_pm.coeff(p, x, k, reduct);
TRACE("nlsat_explain", tout << "lc: " << lc << " reduct: " << reduct << "\n";);
if (!is_zero(lc)) {
if (sign(lc) != polynomial::sign_zero)
if (!::is_zero(sign(lc)))
return;
// lc is not the zero polynomial, but it vanished in the current interpretation.
// so we keep searching...
@ -653,7 +653,7 @@ namespace nlsat {
TRACE("nlsat_explain", tout << "done, psc is a constant\n";);
return;
}
if (sign(s) == polynomial::sign_zero) {
if (is_zero(sign(s))) {
TRACE("nlsat_explain", tout << "psc vanished, adding zero assumption\n";);
add_zero_assumption(s);
continue;
@ -1137,8 +1137,8 @@ namespace nlsat {
}
if (is_const(new_factor)) {
TRACE("nlsat_simplify_core", tout << "new factor is const\n";);
polynomial::sign s = sign(new_factor);
if (s == polynomial::sign_zero) {
auto s = sign(new_factor);
if (is_zero(s)) {
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;

4
src/nlsat/nlsat_interval_set.cpp
View file

@ -78,11 +78,11 @@ namespace nlsat {
SASSERT(i.m_upper_open);
}
if (!i.m_lower_inf && !i.m_upper_inf) {
int s = am.compare(i.m_lower, i.m_upper);
auto s = am.compare(i.m_lower, i.m_upper);
TRACE("nlsat_interval", tout << "lower: "; am.display_decimal(tout, i.m_lower); tout << ", upper: "; am.display_decimal(tout, i.m_upper);
tout << "\ns: " << s << "\n";);
SASSERT(s <= 0);
if (s == 0) {
if (::is_zero(s)) {
SASSERT(!i.m_lower_open && !i.m_upper_open);
}
}

31
src/qe/qe_mbi.cpp
View file

@ -273,12 +273,7 @@ namespace qe {
split_arith(lits, alits, uflits);
auto avars = get_arith_vars(lits);
vector<def> defs = arith_project(mdl, avars, alits);
#if 0
prune_defs(defs);
substitute(defs, uflits);
#else
for (auto const& d : defs) uflits.push_back(m.mk_eq(d.var, d.term));
#endif
project_euf(mdl, uflits);
lits.reset();
lits.append(alits);
@ -309,18 +304,6 @@ namespace qe {
}
/**
* prune defs to only contain substitutions of terms with leading uninterpreted function.
*/
void uflia_mbi::prune_defs(vector<def>& defs) {
unsigned i = 0;
for (auto& d : defs) {
if (!is_shared(to_app(d.var)->get_decl())) {
defs[i++] = d;
}
}
defs.shrink(i);
}
/**
\brief add difference certificates to formula.
@ -337,20 +320,6 @@ namespace qe {
TRACE("qe", tout << "project: " << lits << "\n";);
}
/**
* \brief substitute solution to arithmetical variables into lits
*/
void uflia_mbi::substitute(vector<def> const& defs, expr_ref_vector& lits) {
TRACE("qe", tout << "start substitute: " << lits << "\n";);
for (auto const& def : defs) {
expr_safe_replace rep(m);
rep.insert(def.var, def.term);
rep(lits);
TRACE("qe", tout << "substitute: " << def.var << " |-> " << def.term << ": " << lits << "\n";);
}
IF_VERBOSE(1, verbose_stream() << "substituted: " << lits << "\n");
}
/**
* \brief project private symbols.
*/

2
src/qe/qe_mbi.h
View file

@ -122,12 +122,10 @@ namespace qe {
void add_dcert(model_ref& mdl, expr_ref_vector& lits);
app_ref_vector get_arith_vars(expr_ref_vector const& lits);
vector<def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
void substitute(vector<def> const& defs, expr_ref_vector& lits);
void project_euf(model_ref& mdl, expr_ref_vector& lits);
void split_arith(expr_ref_vector const& lits,
expr_ref_vector& alits,
expr_ref_vector& uflits);
void prune_defs(vector<def>& defs);
public:
uflia_mbi(solver* s, solver* emptySolver);
~uflia_mbi() override {}

4
src/smt/smt_conflict_resolution.cpp
View file

@ -1384,7 +1384,9 @@ namespace smt {
}
while (true) {
TRACE("unsat_core_bug", tout << consequent << ", idx: " << idx << " " << js.get_kind() << "\n";);
TRACE("unsat_core_trail", tout << consequent << ", idx: " << idx << " " << js.get_kind() << "\n";
m_ctx.display_literal_smt2(tout, consequent) << "\n";
);
switch (js.get_kind()) {
case b_justification::CLAUSE: {
clause * cls = js.get_clause();

11
src/smt/theory_seq.cpp
View file

@ -1992,7 +1992,9 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
seq = mk_concat(elems.size(), elems.c_ptr());
}
TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
add_axiom(~mk_eq(len_e, m_autil.mk_numeral(lo, true), false), mk_seq_eq(seq, e));
literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
literal b = mk_seq_eq(seq, e);
add_axiom(~a, b);
if (!ctx.at_base_level()) {
m_trail_stack.push(push_replay(alloc(replay_fixed_length, m, len_e)));
}
@ -3398,6 +3400,7 @@ bool theory_seq::solve_ne(unsigned idx) {
dependency* deps1 = nullptr;
if (explain_eq(n.l(), n.r(), deps1)) {
std::cout << "updated explain\n";
literal diseq = mk_eq(n.l(), n.r(), false);
if (ctx.get_assignment(diseq) == l_false) {
new_lits.reset();
@ -5647,6 +5650,10 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); push_lit_as_expr(l4, exprs); }
if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); push_lit_as_expr(l5, exprs); }
TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";);
IF_VERBOSE(10, verbose_stream() << "ax ";
for (literal l : lits) ctx.display_literal_smt2(verbose_stream() << " ", l);
verbose_stream() << "\n");
m_new_propagation = true;
++m_stats.m_add_axiom;
@ -6329,7 +6336,7 @@ void theory_seq::add_unit_axiom(expr* n) {
expr* u = nullptr;
VERIFY(m_util.str.is_unit(n, u));
sort* s = m.get_sort(u);
expr_ref rhs(mk_skolem(symbol("inv-unit"), n, nullptr, nullptr, nullptr, s), m);
expr_ref rhs(mk_skolem(symbol("seq.inv-unit"), n, nullptr, nullptr, nullptr, s), m);
add_axiom(mk_eq(u, rhs, false));
}

24
src/util/sign.h Normal file
View file

@ -0,0 +1,24 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
sign.h
Abstract:
Sign
Author:
Nikolaj Bjorner
--*/
#pragma once
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); }
inline bool is_zero(sign s) { return s == sign_zero; }