mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
NB's review
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
1df6411580
commit
ef2520ace2
|
|
@ -410,7 +410,7 @@ public:
|
|||
}
|
||||
|
||||
if (b->is_sum() && !to_sum(b)->is_linear()) {
|
||||
nex **ptr_to_a = &((*to_sum(e))[1]);
|
||||
nex **ptr_to_a = &(e->to_sum()[1]);
|
||||
push_to_front(front, ptr_to_a);
|
||||
}
|
||||
}
|
||||
|
|
@ -419,7 +419,7 @@ public:
|
|||
if (b == nullptr) {
|
||||
e = m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a);
|
||||
if (!to_sum(a)->is_linear())
|
||||
push_to_front(front, (*to_mul(e))[1].ee());
|
||||
push_to_front(front, e->to_mul()[1].ee());
|
||||
} else {
|
||||
update_front_with_split_with_non_empty_b(e, j, front, a, b);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -114,17 +114,15 @@ std::ostream& operator<<(std::ostream& out, const nex&);
|
|||
|
||||
class nex_var : public nex {
|
||||
lpvar m_j;
|
||||
public:
|
||||
unsigned number_of_child_powers() const { return 1; }
|
||||
nex_pow get_nex_pow(unsigned j);
|
||||
public:
|
||||
nex_var(lpvar j) : m_j(j) {}
|
||||
nex_var() {}
|
||||
expr_type type() const { return expr_type::VAR; }
|
||||
|
||||
lpvar var() const { return m_j; }
|
||||
lpvar& var() { return m_j; } // the setter
|
||||
std::ostream & print(std::ostream& out) const override { return out << "v" << m_j; }
|
||||
|
||||
bool contains(lpvar j) const { return j == m_j; }
|
||||
std::ostream & print(std::ostream& out) const override { return out << "v" << m_j; }
|
||||
expr_type type() const override { return expr_type::VAR; }
|
||||
unsigned number_of_child_powers() const override { return 1; }
|
||||
bool contains(lpvar j) const override { return j == m_j; }
|
||||
unsigned get_degree() const override { return 1; }
|
||||
bool is_linear() const override { return true; }
|
||||
};
|
||||
|
|
@ -133,12 +131,11 @@ class nex_scalar : public nex {
|
|||
rational m_v;
|
||||
public:
|
||||
nex_scalar(const rational& v) : m_v(v) {}
|
||||
nex_scalar() {}
|
||||
expr_type type() const { return expr_type::SCALAR; }
|
||||
const rational& value() const { return m_v; }
|
||||
rational& value() { return m_v; } // the setter
|
||||
std::ostream& print(std::ostream& out) const override { return out << m_v; }
|
||||
|
||||
const rational& value() const { return m_v; }
|
||||
|
||||
std::ostream& print(std::ostream& out) const override { return out << m_v; }
|
||||
expr_type type() const override { return expr_type::SCALAR; }
|
||||
unsigned get_degree() const override { return 0; }
|
||||
bool is_linear() const override { return true; }
|
||||
};
|
||||
|
|
@ -146,8 +143,7 @@ public:
|
|||
class nex_pow {
|
||||
nex* m_e;
|
||||
unsigned m_power;
|
||||
public:
|
||||
explicit nex_pow(nex* e): m_e(e), m_power(1) {}
|
||||
public:
|
||||
explicit nex_pow(nex* e, unsigned p): m_e(e), m_power(p) {}
|
||||
const nex * e() const { return m_e; }
|
||||
nex *& e() { return m_e; }
|
||||
|
|
@ -212,7 +208,7 @@ public:
|
|||
vector<nex_pow>& children() { return m_children;}
|
||||
const vector<nex_pow>& children() const { return m_children;}
|
||||
// A monomial is 'pure' if does not have a numeric coefficient.
|
||||
bool is_pure_monomial() const { return size() == 0 || (!m_children[0].e()->is_scalar()); }
|
||||
bool is_pure_monomial() const { return size() == 0 || !m_children[0].e()->is_scalar(); }
|
||||
|
||||
std::ostream & print(std::ostream& out) const override {
|
||||
bool first = true;
|
||||
|
|
@ -247,7 +243,6 @@ public:
|
|||
add_child_in_power(p.e(), p.pow());
|
||||
}
|
||||
|
||||
|
||||
const nex_pow& operator[](unsigned j) const { return m_children[j]; }
|
||||
nex_pow& operator[](unsigned j) { return m_children[j]; }
|
||||
const nex_pow* begin() const { return m_children.begin(); }
|
||||
|
|
@ -276,12 +271,11 @@ public:
|
|||
TRACE("nla_cn_details", tout << "powers of " << *this << "\n";);
|
||||
r.clear();
|
||||
for (const auto & c : *this) {
|
||||
if (!c.e()->is_var()) {
|
||||
continue;
|
||||
if (c.e()->is_var()) {
|
||||
lpvar j = c.e()->to_var().var();
|
||||
SASSERT(r.find(j) == r.end());
|
||||
r[j] = c.pow();
|
||||
}
|
||||
lpvar j = c.e()->to_var().var();
|
||||
SASSERT(r.find(j) == r.end());
|
||||
r[j] = c.pow();
|
||||
}
|
||||
TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";);
|
||||
}
|
||||
|
|
@ -312,12 +306,12 @@ class nex_sum : public nex {
|
|||
ptr_vector<nex> m_children;
|
||||
public:
|
||||
nex_sum() {}
|
||||
expr_type type() const override { return expr_type::SUM; }
|
||||
ptr_vector<nex>& children() { return m_children;}
|
||||
const ptr_vector<nex>& children() const { return m_children;}
|
||||
const ptr_vector<nex>* children_ptr() const { return &m_children;}
|
||||
unsigned size() const override { return m_children.size(); }
|
||||
nex_sum(ptr_vector<nex> const& ch) : m_children(ch) {}
|
||||
|
||||
expr_type type() const override { return expr_type::SUM; }
|
||||
ptr_vector<nex>& children() { return m_children; }
|
||||
const ptr_vector<nex>& children() const { return m_children; }
|
||||
unsigned size() const override { return m_children.size(); }
|
||||
|
||||
bool is_linear() const override {
|
||||
TRACE("nex_details", tout << *this << "\n";);
|
||||
|
|
@ -379,8 +373,6 @@ public:
|
|||
nex*& operator[](unsigned j) { return m_children[j]; }
|
||||
const ptr_vector<nex>::const_iterator begin() const { return m_children.begin(); }
|
||||
const ptr_vector<nex>::const_iterator end() const { return m_children.end(); }
|
||||
ptr_vector<nex>::iterator begin() { return m_children.begin(); }
|
||||
ptr_vector<nex>::iterator end() { return m_children.end(); }
|
||||
|
||||
void add_child(nex* e) { m_children.push_back(e); }
|
||||
#ifdef Z3DEBUG
|
||||
|
|
@ -432,20 +424,20 @@ inline rational get_nex_val(const nex* e, std::function<rational (unsigned)> var
|
|||
return to_scalar(e)->value();
|
||||
case expr_type::SUM: {
|
||||
rational r(0);
|
||||
for (auto c: *to_sum(e)) {
|
||||
for (nex* c: e->to_sum()) {
|
||||
r += get_nex_val(c, var_val);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
case expr_type::MUL: {
|
||||
auto & m = *to_mul(e);
|
||||
auto & m = e->to_mul();
|
||||
rational t = m.coeff();
|
||||
for (auto& c: m)
|
||||
for (nex_pow const& c: m)
|
||||
t *= get_nex_val(c.e(), var_val).expt(c.pow());
|
||||
return t;
|
||||
}
|
||||
case expr_type::VAR:
|
||||
return var_val(to_var(e)->var());
|
||||
return var_val(e->to_var().var());
|
||||
default:
|
||||
TRACE("nla_cn_details", tout << e->type() << "\n";);
|
||||
SASSERT(false);
|
||||
|
|
@ -458,20 +450,18 @@ inline std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
|
|||
switch (e->type()) {
|
||||
case expr_type::SCALAR:
|
||||
return r;
|
||||
case expr_type::SUM: {
|
||||
for (auto c: *to_sum(e))
|
||||
case expr_type::SUM:
|
||||
for (auto c: e->to_sum())
|
||||
for ( lpvar j : get_vars_of_expr(c))
|
||||
r.insert(j);
|
||||
return r;
|
||||
}
|
||||
case expr_type::MUL: {
|
||||
for (auto &c: *to_mul(e))
|
||||
return r;
|
||||
case expr_type::MUL:
|
||||
for (auto &c: e->to_mul())
|
||||
for ( lpvar j : get_vars_of_expr(c.e()))
|
||||
r.insert(j);
|
||||
return r;
|
||||
}
|
||||
return r;
|
||||
case expr_type::VAR:
|
||||
r.insert(to_var(e)->var());
|
||||
r.insert(e->to_var().var());
|
||||
return r;
|
||||
default:
|
||||
TRACE("nla_cn_details", tout << e->type() << "\n";);
|
||||
|
|
@ -481,7 +471,7 @@ inline std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
|
|||
}
|
||||
|
||||
inline bool is_zero_scalar(nex *e) {
|
||||
return e->is_scalar() && to_scalar(e)->value().is_zero();
|
||||
return e->is_scalar() && e->to_scalar().value().is_zero();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ nex * nex_creator::mk_div(const nex& a, lpvar j) {
|
|||
if (!seenj && c->contains(j)) {
|
||||
SASSERT(!c->is_var() || c->to_var().var() == j);
|
||||
if (!c->is_var()) {
|
||||
bv.push_back(nex_pow(mk_div(*c, j)));
|
||||
bv.push_back(nex_pow(mk_div(*c, j), 1));
|
||||
}
|
||||
if (pow != 1) {
|
||||
bv.push_back(nex_pow(clone(c), pow - 1));
|
||||
|
|
@ -437,42 +437,6 @@ void nex_creator::mul_to_powers(vector<nex_pow>& children) {
|
|||
});
|
||||
}
|
||||
|
||||
nex* nex_creator::create_child_from_nex_and_coeff(nex *e,
|
||||
const rational& coeff) {
|
||||
TRACE("grobner_d", tout << *e << ", coeff = " << coeff << "\n";);
|
||||
if (coeff.is_one())
|
||||
return e;
|
||||
SASSERT(is_simplified(*e));
|
||||
switch (e->type()) {
|
||||
case expr_type::VAR: {
|
||||
if (coeff.is_one())
|
||||
return e;
|
||||
return mk_mul(mk_scalar(coeff), e);
|
||||
}
|
||||
case expr_type::SCALAR: {
|
||||
return mk_scalar(coeff);
|
||||
}
|
||||
case expr_type::MUL: {
|
||||
nex_mul * em = to_mul(e);
|
||||
nex_pow *np = em->begin();
|
||||
if (np->e()->is_scalar()) {
|
||||
SASSERT(np->pow() == 1);
|
||||
to_scalar(np->e())->value() = coeff;
|
||||
return e;
|
||||
}
|
||||
em->add_child(mk_scalar(coeff));
|
||||
std::sort(em->begin(), em->end(), [this](const nex_pow& a,
|
||||
const nex_pow& b) {return gt_on_nex_pow(a, b); });
|
||||
return em;
|
||||
}
|
||||
case expr_type::SUM:
|
||||
return mk_mul(mk_scalar(coeff), e);
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
}
|
||||
// returns true if the key exists already
|
||||
bool nex_creator::register_in_join_map(std::map<nex*, rational, nex_lt>& map, nex* e, const rational& r) const{
|
||||
TRACE("grobner_d", tout << *e << ", r = " << r << std::endl;);
|
||||
|
|
@ -492,18 +456,12 @@ bool nex_creator::fill_join_map_for_sum(
|
|||
ptr_vector<nex> & children,
|
||||
std::map<nex*, rational, nex_lt>& map,
|
||||
std::unordered_set<nex*>& existing_nex,
|
||||
nex_scalar*& common_scalar) {
|
||||
common_scalar = nullptr;
|
||||
rational& common_scalar) {
|
||||
bool simplified = false;
|
||||
for (auto e : children) {
|
||||
if (e->is_scalar()) {
|
||||
nex_scalar * es = to_scalar(e);
|
||||
if (common_scalar == nullptr) {
|
||||
common_scalar = es;
|
||||
} else {
|
||||
simplified = true;
|
||||
common_scalar->value() += es->value();
|
||||
}
|
||||
simplified = true;
|
||||
common_scalar += e->to_scalar().value();
|
||||
continue;
|
||||
}
|
||||
existing_nex.insert(e);
|
||||
|
|
@ -523,7 +481,7 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
|
|||
std::map<nex*, rational, nex_lt> map([this](const nex *a , const nex *b)
|
||||
{ return gt_for_sort_join_sum(a, b); });
|
||||
std::unordered_set<nex*> allocated_nexs; // handling (nex*) as numbers
|
||||
nex_scalar * common_scalar = nullptr;
|
||||
rational common_scalar(0);
|
||||
fill_join_map_for_sum(children, map, allocated_nexs, common_scalar);
|
||||
|
||||
TRACE("grobner_d", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
|
||||
|
|
@ -531,8 +489,8 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
|
|||
for (auto& p : map) {
|
||||
process_map_pair(p.first, p.second, children, allocated_nexs);
|
||||
}
|
||||
if (common_scalar && !common_scalar->value().is_zero()) {
|
||||
children.push_back(common_scalar);
|
||||
if (!common_scalar.is_zero()) {
|
||||
children.push_back(mk_scalar(common_scalar));
|
||||
}
|
||||
TRACE("grobner_d",
|
||||
tout << "map=";
|
||||
|
|
|
|||
|
|
@ -162,9 +162,8 @@ public:
|
|||
}
|
||||
|
||||
nex_sum* mk_sum(const ptr_vector<nex>& v) {
|
||||
auto r = new nex_sum();
|
||||
auto r = new nex_sum(v);
|
||||
add_to_allocated(r);
|
||||
r->children() = v;
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
@ -227,20 +226,17 @@ public:
|
|||
|
||||
void mul_to_powers(vector<nex_pow>& children);
|
||||
|
||||
nex* create_child_from_nex_and_coeff(nex *e,
|
||||
const rational& coeff) ;
|
||||
|
||||
void sort_join_sum(ptr_vector<nex> & children);
|
||||
bool fill_join_map_for_sum(ptr_vector<nex> & children,
|
||||
std::map<nex*, rational, nex_lt>& map,
|
||||
std::unordered_set<nex*>& existing_nex,
|
||||
nex_scalar*& common_scalar);
|
||||
rational& common_scalar);
|
||||
bool register_in_join_map(std::map<nex*, rational, nex_lt>&, nex*, const rational&) const;
|
||||
|
||||
void simplify_children_of_sum(ptr_vector<nex> & children);
|
||||
|
||||
bool eat_scalar_pow(rational& r, const nex_pow& p, unsigned);
|
||||
void simplify_children_of_mul(vector<nex_pow> & children, lt_on_vars, std::function<nex_scalar*()> mk_scalar);
|
||||
|
||||
bool children_are_simplified(const vector<nex_pow>& children) const;
|
||||
bool gt(const nex* a, const nex* b) const;
|
||||
|
|
@ -253,7 +249,6 @@ public:
|
|||
bool gt_on_var_nex(const nex_var* a, const nex* b) const;
|
||||
bool gt_on_mul_nex(const nex_mul* a, const nex* b) const;
|
||||
bool gt_on_sum_sum(const nex_sum* a, const nex_sum* b) const;
|
||||
void fill_map_with_children(std::map<nex*, rational, nex_lt> & m, ptr_vector<nex> & children);
|
||||
void process_map_pair(nex *e, const rational& coeff, ptr_vector<nex> & children, std::unordered_set<nex*>&);
|
||||
#ifdef Z3DEBUG
|
||||
static
|
||||
|
|
|
|||
|
|
@ -62,7 +62,7 @@ void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::qu
|
|||
for (auto & s : matrix.m_columns[j]) {
|
||||
unsigned row = s.var();
|
||||
if (m_rows.contains(row)) continue;
|
||||
if (false && c().var_is_free(core_slv.m_r_basis[row])) {
|
||||
if (c().var_is_free(core_slv.m_r_basis[row])) {
|
||||
TRACE("grobner", tout << "ignore the row " << row << " with the free basic var\n";);
|
||||
continue; // mimic the behavior of the legacy solver
|
||||
}
|
||||
|
|
@ -345,7 +345,7 @@ bool grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
|
|||
|
||||
nex_mul * grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h) {
|
||||
nex_mul * r = m_nex_creator.mk_mul();
|
||||
unsigned j = 0; // points to t and k runs over h
|
||||
unsigned j = 0; // j points to t and k runs over h
|
||||
for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
|
||||
lpvar h_var = to_var(h->get_child_exp(k))->var();
|
||||
for (; j < t->size(); j++) {
|
||||
|
|
@ -701,15 +701,14 @@ bool grobner::done() const {
|
|||
}
|
||||
|
||||
bool grobner::compute_basis_loop(){
|
||||
int i = 0;
|
||||
while (!done()) {
|
||||
if (compute_basis_step()) {
|
||||
TRACE("grobner", tout << "progress in compute_basis_step\n";);
|
||||
return true;
|
||||
}
|
||||
TRACE("grobner", tout << "continue compute_basis_loop i= " << ++i << "\n";);
|
||||
TRACE("grobner", tout << "continue compute_basis_loop\n";);
|
||||
}
|
||||
TRACE("grobner", tout << "return false from compute_basis_loop i= " << i << "\n";);
|
||||
TRACE("grobner", tout << "return false from compute_basis_loop\n";);
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -793,8 +792,7 @@ void grobner::assert_eq_0(nex* e, ci_dependency * dep) {
|
|||
display_equation(tout, *eq);
|
||||
tout << "\nvars\n";
|
||||
for (unsigned j : get_vars_of_expr_with_opening_terms(e)) {
|
||||
tout << "(";
|
||||
c().print_var(j, tout) << ")\n";
|
||||
c().print_var(j, tout << "(") << ")\n";
|
||||
});
|
||||
insert_to_simplify(eq);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ class grobner : common {
|
|||
}
|
||||
}
|
||||
// can return not a nex_mul
|
||||
nex* get_monomial(unsigned idx) const {
|
||||
nex const* get_monomial(unsigned idx) const {
|
||||
switch(m_expr->type()) {
|
||||
case expr_type::VAR:
|
||||
case expr_type::SCALAR: UNREACHABLE();;
|
||||
|
|
@ -60,7 +60,7 @@ class grobner : common {
|
|||
SASSERT(idx == 0);
|
||||
return m_expr;
|
||||
case expr_type::SUM:
|
||||
return (*to_sum(m_expr))[idx];
|
||||
return m_expr->to_sum()[idx];
|
||||
default: return 0;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue