mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
add an assert test_find_b_c()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
2fbb4cac9d
commit
9661f75246
|
@ -429,7 +429,9 @@ bool grobner::simplify_source_target(equation * source, equation * target) {
|
||||||
TRACE("grobner_d", tout << "no simplification\n";);
|
TRACE("grobner_d", tout << "no simplification\n";);
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
void grobner::process_simplified_target(equation* target, ptr_buffer<equation>& to_remove) {
|
void grobner::process_simplified_target(equation* target, ptr_buffer<equation>& to_remove) {
|
||||||
if (is_trivial(target)) {
|
if (is_trivial(target)) {
|
||||||
to_remove.push_back(target);
|
to_remove.push_back(target);
|
||||||
|
@ -597,6 +599,7 @@ bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) {
|
||||||
nex_mul *a = divide_ignore_coeffs_perform(m_nex_creator.clone(ab), b);
|
nex_mul *a = divide_ignore_coeffs_perform(m_nex_creator.clone(ab), b);
|
||||||
SASSERT(ab->get_degree() == a->get_degree() + b->get_degree());
|
SASSERT(ab->get_degree() == a->get_degree() + b->get_degree());
|
||||||
SASSERT(ac->get_degree() == a->get_degree() + c->get_degree());
|
SASSERT(ac->get_degree() == a->get_degree() + c->get_degree());
|
||||||
|
SASSERT(test_find_b_c(ab, ac, b, c));
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -700,11 +703,9 @@ bool grobner::compute_basis_loop(){
|
||||||
while (!done()) {
|
while (!done()) {
|
||||||
if (compute_basis_step()) {
|
if (compute_basis_step()) {
|
||||||
TRACE("grobner", tout << "progress in compute_basis_step\n";);
|
TRACE("grobner", tout << "progress in compute_basis_step\n";);
|
||||||
TRACE("grobner_stats", print_stats(tout););
|
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
TRACE("grobner", tout << "continue compute_basis_loop\n";);
|
TRACE("grobner", tout << "continue compute_basis_loop\n";);
|
||||||
TRACE("grobner_stats", print_stats(tout););
|
|
||||||
}
|
}
|
||||||
TRACE("grobner", tout << "return false from compute_basis_loop\n";);
|
TRACE("grobner", tout << "return false from compute_basis_loop\n";);
|
||||||
TRACE("grobner_stats", print_stats(tout););
|
TRACE("grobner_stats", print_stats(tout););
|
||||||
|
@ -816,4 +817,19 @@ std::ostream& grobner::display_dependency(std::ostream& out, ci_dependency* dep)
|
||||||
}
|
}
|
||||||
return out;
|
return out;
|
||||||
}
|
}
|
||||||
|
#ifdef Z3DEBUG
|
||||||
|
bool grobner::test_find_b(const nex* ab, const nex_mul* b) {
|
||||||
|
nex_mul& ab_clone = m_nex_creator.clone(ab)->to_mul();
|
||||||
|
nex_mul * a= divide_ignore_coeffs_perform(&ab_clone, b);
|
||||||
|
ab_clone.coeff() = rational(1);
|
||||||
|
SASSERT(b->coeff().is_one());
|
||||||
|
nex * m = m_nex_creator.mk_mul(a, m_nex_creator.clone(b));
|
||||||
|
m = m_nex_creator.simplify(m);
|
||||||
|
return m_nex_creator.equal(m, &ab_clone);
|
||||||
|
}
|
||||||
|
|
||||||
|
bool grobner::test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c) {
|
||||||
|
return test_find_b(ab, b) && test_find_b(ac, c);
|
||||||
|
}
|
||||||
|
|
||||||
|
#endif
|
||||||
|
|
|
@ -160,8 +160,10 @@ private:
|
||||||
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex *e );
|
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex *e );
|
||||||
unsigned num_of_equations() const { return m_to_simplify.size() + m_to_superpose.size(); }
|
unsigned num_of_equations() const { return m_to_simplify.size() + m_to_superpose.size(); }
|
||||||
std::ostream& print_stats(std::ostream&) const;
|
std::ostream& print_stats(std::ostream&) const;
|
||||||
template <typename T>
|
void update_stats_max_degree_and_size(const equation*);
|
||||||
std::ostream& print_stats_eqs(T&, std::ostream&) const;
|
#ifdef Z3DEBUG
|
||||||
void update_stats_max_degree_and_size(const equation *e);
|
bool test_find_b_c(const nex* ab, const nex* ac, const nex_mul* b, const nex_mul* c);
|
||||||
|
bool test_find_b(const nex* ab, const nex_mul* b);
|
||||||
|
#endif
|
||||||
}; // end of grobner
|
}; // end of grobner
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue