mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

port grobner: fix the sum from row creation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-30 12:22:43 -07:00
parent 809647ec2f
commit 4651eb7042
5 changed files with 55 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/math/grobner/grobner.cpp
View file

@ -90,15 +90,6 @@ void grobner::unfreeze_equations(unsigned old_size) {
m_equations_to_unfreeze.shrink(old_size);
}
void grobner::reset() {
flush();
m_to_superpose.reset();
m_to_simplify.reset();
m_equations_to_unfreeze.reset();
m_equations_to_delete.reset();
m_unsat = nullptr;
}
void grobner::display_var(std::ostream & out, expr * var) const {
if (is_app(var) && to_app(var)->get_num_args() > 0)
out << mk_bounded_pp(var, m_manager);

2
src/math/grobner/grobner.h
View file

@ -271,8 +271,6 @@ public:
/**
\brief Reset state. Remove all equalities asserted with assert_eq.
*/
void reset();
void get_equations(ptr_vector<equation> & result) const;
void display_equation(std::ostream & out, equation const & eq) const;

8
src/math/lp/nex_creator.cpp
View file

@ -672,12 +672,12 @@ void nex_creator::sort_join_sum(ptr_vector<nex> & children) {
TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
children.clear();
if (common_scalar) {
children.push_back(common_scalar);
}
for (auto& p : map) {
process_map_pair(p.first, p.second, children, existing_nex);
}
if (common_scalar) {
children.push_back(common_scalar);
}
TRACE("nla_cn_details", for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";});
}
@ -856,7 +856,7 @@ void nex_creator::process_map_pair(nex *e, const rational& coeff, ptr_vector<nex
}
bool nex_creator::is_simplified(const nex *e) const
{
{
if (e->is_mul())
return mul_is_simplified(to_mul(e));
if (e->is_sum())

62
src/math/lp/nla_grobner.cpp
View file

@ -159,6 +159,14 @@ void nla_grobner::simplify_equations_to_process() {
void nla_grobner::init() {
m_reported = 0;
m_conflict = false;
m_equations_to_unfreeze.clear();
del_equations(0);
SASSERT(m_equations_to_delete.size() == 0);
m_num_of_equations = 0;
m_to_superpose.reset();
m_to_simplify.reset();
find_nl_cluster();
c().clear_and_resize_active_var_set();
for (unsigned i : m_rows) {
@ -276,26 +284,28 @@ bool nla_grobner::simplify_target_monomials(equation * source, equation * target
return simplify_target_monomials_sum(source, target, targ_sum, high_mon);
}
bool nla_grobner::simplify_target_monomials_sum_check_only(nex_sum* targ_sum,
unsigned nla_grobner::find_divisible(nex_sum* targ_sum,
const nex* high_mon) const {
for (auto t : *targ_sum) {
for (unsigned j = 0; j < targ_sum->size(); j++) {
auto t = (*targ_sum)[j];
if (divide_ignore_coeffs_check_only(t, high_mon)) {
TRACE("grobner", tout << "yes div: " << *targ_sum << " / " << *high_mon << "\n";);
return true;
return j;
}
}
TRACE("grobner", tout << "no div: " << *targ_sum << " / " << *high_mon << "\n";);
return false;
return -1;
}
bool nla_grobner::simplify_target_monomials_sum(equation * source,
equation * target, nex_sum* targ_sum,
const nex* high_mon) {
if (!simplify_target_monomials_sum_check_only(targ_sum, high_mon))
unsigned j = find_divisible(targ_sum, high_mon);
if (j + 1 == 0)
return false;
unsigned targ_orig_size = targ_sum->size();
for (unsigned j = 0; j < targ_orig_size; j++) {
for (; j < targ_orig_size; j++) {
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j);
}
target->exp() = m_nex_creator.simplify(targ_sum);
@ -305,15 +315,14 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
}
nex_mul* nla_grobner::divide_ignore_coeffs(nex* ej, const nex* h) {
if (!ej->is_mul())
TRACE("grobner", tout << "ej = " << *ej << " , h = " << *h << "\n";);
if (!divide_ignore_coeffs_check_only(ej, h))
return nullptr;
nex_mul* m = to_mul(ej);
if (!divide_ignore_coeffs_check_only(m, h))
return nullptr;
return divide_ignore_coeffs_perform(m, h);
return divide_ignore_coeffs_perform(ej, h);
}
bool nla_grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h) const {
TRACE("grobner", tout << "t = " << *t << ", h=" << *h << "\n";);
SASSERT(m_nex_creator.is_simplified(t) && m_nex_creator.is_simplified(h));
unsigned j = 0; // points to t
for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
@ -361,9 +370,7 @@ bool nla_grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
return false;
}
// perform the division t / h, but ignores the coefficients
// h does not change
nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex_mul* t, const nex* h) {
nex_mul * nla_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
for(unsigned k = 0; k < h->number_of_child_powers(); k++) {
@ -386,6 +393,15 @@ nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex_mul* t, const nex* h) {
return r;
}
// perform the division t / h, but ignores the coefficients
// h does not change
nex_mul * nla_grobner::divide_ignore_coeffs_perform(nex* e, const nex* h) {
if (e->is_mul())
return divide_ignore_coeffs_perform_nex_mul(to_mul(e), h);
SASSERT(e->is_var());
return m_nex_creator.mk_mul(); // return the empty nex_mul
}
// if targ_sum->children()[j] = c*high_mon*p,
// and b*high_mon + e = 0, so high_mon = -e/b
// then targ_sum->children()[j] = - (c/b) * e*p
@ -407,6 +423,8 @@ void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *t
nla_grobner::equation * nla_grobner::simplify_source_target(equation * source, equation * target) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
SASSERT(m_nex_creator.is_simplified(source->exp()));
SASSERT(m_nex_creator.is_simplified(target->exp()));
if (target->exp()->is_scalar()) {
return nullptr;
}
@ -470,6 +488,8 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
}
if (is_trivial(target))
to_delete.push_back(target);
else
SASSERT(m_nex_creator.is_simplified(target->exp()));
}
for (equation* eq : to_insert)
insert_to_superpose(eq);
@ -684,7 +704,18 @@ bool nla_grobner::canceled() const {
bool nla_grobner::done() const {
return m_num_of_equations >= c().m_nla_settings.grobner_eqs_threshold() || canceled() || m_reported > 10 || m_conflict;
if (
m_num_of_equations >= c().m_nla_settings.grobner_eqs_threshold()
||
canceled()
||
m_reported > 10
||
m_conflict) {
TRACE("grobner", tout << "done()\n";);
return true;
}
return false;
}
bool nla_grobner::compute_basis_loop(){
@ -739,6 +770,7 @@ void nla_grobner::grobner_lemmas() {
while(push_calculation_forward(eqs, next_weight));
}
void nla_grobner:: del_equations(unsigned old_size) {
TRACE("grobner", );
SASSERT(m_equations_to_delete.size() >= old_size);
equation_vector::iterator it = m_equations_to_delete.begin();
equation_vector::iterator end = m_equations_to_delete.end();

6
src/math/lp/nla_grobner.h
View file

@ -150,18 +150,20 @@ private:
m_to_simplify.insert(eq);
}
void insert_to_superpose(equation *eq) {
SASSERT(m_nex_creator.is_simplified(eq->exp()));
m_to_superpose.insert(eq);
}
void simplify_equations_to_process();
const nex * get_highest_monomial(const nex * e) const;
ci_dependency* dep_from_vector( svector<lp::constraint_index> & fixed_vars_constraints);
bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*);
bool simplify_target_monomials_sum_check_only(nex_sum*, const nex*) const;
unsigned find_divisible(nex_sum*, const nex*) const;
void simplify_target_monomials_sum_j(equation *, equation *, nex_sum*, const nex*, unsigned);
nex_mul * divide_ignore_coeffs(nex* ej, const nex*);
bool divide_ignore_coeffs_check_only(nex* , const nex*) const;
bool divide_ignore_coeffs_check_only_nex_mul(nex_mul* , const nex*) const;
nex_mul * divide_ignore_coeffs_perform(nex_mul* , const nex*);
nex_mul * divide_ignore_coeffs_perform(nex* , const nex*);
nex_mul * divide_ignore_coeffs_perform_nex_mul(nex_mul* , const nex*);
nex * expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, nex_mul* b, nex_mul* c);
void add_mul_skip_first(nex_sum* r, const rational& beta, nex *e, nex_mul* c);
bool done() const;