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

solving small problem for each other random seed

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-07 19:55:20 -10:00
parent 87d7ce69e3
commit 15dff85b22
3 changed files with 43 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -780,7 +780,7 @@ void grobner::simplify_m_to_simplify(equation * eq) {
\brief If m1 = (* c M M1) and m2 = (* d M M2) and M is non empty, then return true and store M1 in rest1 and M2 in rest2. \brief If m1 = (* c M M1) and m2 = (* d M M2) and M is non empty, then return true and store M1 in rest1 and M2 in rest2.
*/ */
bool grobner::unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2) { bool grobner::unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2) {
TRACE("grobner", tout << "unifying: "; display_monomial(tout, *m1); tout << " "; display_monomial(tout, *m2); tout << "\n";); TRACE("grobner", tout << "unifying: "; display_monomial(tout, *m1); tout << " and "; display_monomial(tout, *m2); tout << "\n";);
bool found_M = false; bool found_M = false;
unsigned i1 = 0; unsigned i1 = 0;
unsigned i2 = 0; unsigned i2 = 0;

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

@ -44,7 +44,7 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
unsigned row = s.var(); unsigned row = s.var();
if (m_rows.contains(row)) continue; if (m_rows.contains(row)) continue;
lpvar basic_in_row = core_slv.m_r_basis[row]; lpvar basic_in_row = core_slv.m_r_basis[row];
if (c().var_is_free(basic_in_row)) { if (false && c().var_is_free(basic_in_row)) {
TRACE("grobner", tout << "ignore the row " << row << " with the free basic var\n";); TRACE("grobner", tout << "ignore the row " << row << " with the free basic var\n";);
continue; // mimic the behavior of the legacy solver continue; // mimic the behavior of the legacy solver
} }
@ -138,7 +138,7 @@ void nla_grobner::add_row(unsigned i) {
void nla_grobner::simplify_equations_in_m_to_simplify() { void nla_grobner::simplify_equations_in_m_to_simplify() {
for (equation *eq : m_to_simplify) { for (equation *eq : m_to_simplify) {
eq->exp() = m_nex_creator.simplify(eq->exp()); eq->expr() = m_nex_creator.simplify(eq->expr());
} }
} }
@ -147,7 +147,6 @@ void nla_grobner::init() {
m_conflict = false; m_conflict = false;
del_equations(0); del_equations(0);
SASSERT(m_equations_to_delete.size() == 0); SASSERT(m_equations_to_delete.size() == 0);
m_num_of_equations = 0;
m_to_superpose.reset(); m_to_superpose.reset();
m_to_simplify.reset(); m_to_simplify.reset();
@ -161,8 +160,8 @@ void nla_grobner::init() {
} }
bool nla_grobner::is_trivial(equation* eq) const { bool nla_grobner::is_trivial(equation* eq) const {
SASSERT(m_nex_creator.is_simplified(eq->exp())); SASSERT(m_nex_creator.is_simplified(eq->expr()));
return eq->exp()->size() == 0; return eq->expr()->size() == 0;
} }
bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) { bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) {
@ -172,7 +171,7 @@ bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) {
return true; return true;
if (is_trivial(eq2)) if (is_trivial(eq2))
return false; return false;
return m_nex_creator.lt(eq2->exp(), eq1->exp()); return m_nex_creator.lt(eq2->expr(), eq1->expr());
} }
void nla_grobner::del_equation(equation * eq) { void nla_grobner::del_equation(equation * eq) {
@ -216,14 +215,14 @@ nla_grobner::equation* nla_grobner::simplify_using_to_superpose(equation* eq) {
if (canceled()) { if (canceled()) {
return nullptr; return nullptr;
} }
if (eq->exp()->is_scalar()) if (eq->expr()->is_scalar())
break; break;
} }
if (eq->exp()->is_scalar()) if (eq->expr()->is_scalar())
break; break;
} }
while (simplified); while (simplified);
if (result && eq->exp()->is_scalar()) { if (result && eq->expr()->is_scalar()) {
TRACE("grobner",); TRACE("grobner",);
} }
@ -248,13 +247,13 @@ const nex* nla_grobner::get_highest_monomial(const nex* e) const {
// target 2fg + 3fp + e = 0 // target 2fg + 3fp + e = 0
// target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e // target is replaced by 2(-k/3 - l/3)g + 3(-k/3 - l/3)p + e = -2/3kg -2/3lg - kp -lp + e
bool nla_grobner::simplify_target_monomials(equation * source, equation * target) { bool nla_grobner::simplify_target_monomials(equation * source, equation * target) {
auto * high_mon = get_highest_monomial(source->exp()); auto * high_mon = get_highest_monomial(source->expr());
if (high_mon == nullptr) if (high_mon == nullptr)
return false; return false;
SASSERT(high_mon->all_factors_are_elementary()); SASSERT(high_mon->all_factors_are_elementary());
TRACE("grobner", tout << "source = "; display_equation(tout, *source) << "target = "; display_equation(tout, *target) << "high_mon = " << *high_mon << "\n";); TRACE("grobner", tout << "source = "; display_equation(tout, *source) << "target = "; display_equation(tout, *target) << "high_mon = " << *high_mon << "\n";);
nex * te = target->exp(); nex * te = target->expr();
nex_sum * targ_sum; nex_sum * targ_sum;
if (te->is_sum()) { if (te->is_sum()) {
targ_sum = to_sum(te); targ_sum = to_sum(te);
@ -294,7 +293,7 @@ bool nla_grobner::simplify_target_monomials_sum(equation * source,
simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j); simplify_target_monomials_sum_j(source, target, targ_sum, high_mon, j);
} }
TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";); TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";);
target->exp() = m_nex_creator.simplify(targ_sum); target->expr() = m_nex_creator.simplify(targ_sum);
target->dep() = m_dep_manager.mk_join(source->dep(), target->dep()); target->dep() = m_dep_manager.mk_join(source->dep(), target->dep());
TRACE("grobner_d", tout << "target = "; display_equation(tout, *target);); TRACE("grobner_d", tout << "target = "; display_equation(tout, *target););
return true; return true;
@ -406,17 +405,17 @@ void nla_grobner::simplify_target_monomials_sum_j(equation * source, equation *t
nex_sum * ej_sum = m_nex_creator.mk_sum(); nex_sum * ej_sum = m_nex_creator.mk_sum();
(*targ_sum)[j] = ej_sum; (*targ_sum)[j] = ej_sum;
add_mul_skip_first(ej_sum ,-c/high_mon->coeff(), source->exp(), ej_over_high_mon); add_mul_skip_first(ej_sum ,-c/high_mon->coeff(), source->expr(), ej_over_high_mon);
TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";); TRACE("grobner_d", tout << "targ_sum = " << *targ_sum << "\n";);
} }
// return true iff simplified // return true iff simplified
bool nla_grobner::simplify_source_target(equation * source, equation * target) { bool nla_grobner::simplify_source_target(equation * source, equation * target) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source);); TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
TRACE("grobner_d", tout << "simplifying: " << *(target->exp()) << " using " << *(source->exp()) << "\n";); TRACE("grobner_d", tout << "simplifying: " << *(target->expr()) << " using " << *(source->expr()) << "\n";);
SASSERT(m_nex_creator.is_simplified(source->exp())); SASSERT(m_nex_creator.is_simplified(source->expr()));
SASSERT(m_nex_creator.is_simplified(target->exp())); SASSERT(m_nex_creator.is_simplified(target->expr()));
if (target->exp()->is_scalar()) { if (target->expr()->is_scalar()) {
TRACE("grobner_d", tout << "no simplification\n";); TRACE("grobner_d", tout << "no simplification\n";);
return false; return false;
} }
@ -437,7 +436,7 @@ bool nla_grobner::simplify_source_target(equation * source, equation * target) {
TRACE("grobner", tout << "result: " << result << "\n"; if (result) display_equation(tout, *target);); TRACE("grobner", tout << "result: " << result << "\n"; if (result) display_equation(tout, *target););
if (result) { if (result) {
target->dep() = m_dep_manager.mk_join(target->dep(), source->dep()); target->dep() = m_dep_manager.mk_join(target->dep(), source->dep());
TRACE("grobner_d", tout << "simplified to " << *(target->exp()) << "\n";); TRACE("grobner_d", tout << "simplified to " << *(target->expr()) << "\n";);
return true; return true;
} }
TRACE("grobner_d", tout << "no simplification\n";); TRACE("grobner_d", tout << "no simplification\n";);
@ -454,19 +453,19 @@ void nla_grobner::process_simplified_target(equation* target, ptr_buffer<equatio
} }
void nla_grobner::check_eq(equation* target) { void nla_grobner::check_eq(equation* target) {
if(m_intervals->check_cross_nested_expr(target->exp(), target->dep())) { if(m_intervals->check_cross_nested_expr(target->expr(), target->dep())) {
TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n"; TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n";
tout << "vars = \n"; tout << "vars = \n";
for (lpvar j : get_vars_of_expr(target->exp())) { for (lpvar j : get_vars_of_expr(target->expr())) {
c().print_var(j, tout); c().print_var(j, tout);
} }
tout << "\ntarget->exp() val = " << get_nex_val(target->exp(), [this](unsigned j) { return c().val(j); }) << "\n";); tout << "\ntarget->expr() val = " << get_nex_val(target->expr(), [this](unsigned j) { return c().val(j); }) << "\n";);
register_report(); register_report();
} }
} }
bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) { bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
TRACE("grobner_d", tout << "eq->exp " << *(eq->exp()) << "\n";); TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";);
ptr_buffer<equation> to_insert; ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove; ptr_buffer<equation> to_remove;
@ -483,7 +482,7 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
if (is_trivial(target)) if (is_trivial(target))
to_delete.push_back(target); to_delete.push_back(target);
else else
SASSERT(m_nex_creator.is_simplified(target->exp())); SASSERT(m_nex_creator.is_simplified(target->expr()));
} }
for (equation* eq : to_insert) for (equation* eq : to_insert)
insert_to_superpose(eq); insert_to_superpose(eq);
@ -498,7 +497,7 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
Use the given equation to simplify m_to_simplify equations Use the given equation to simplify m_to_simplify equations
*/ */
void nla_grobner::simplify_m_to_simplify(equation* eq) { void nla_grobner::simplify_m_to_simplify(equation* eq) {
TRACE("grobner_d", tout << "eq->exp " << *(eq->exp()) << "\n";); TRACE("grobner_d", tout << "eq->exp " << *(eq->expr()) << "\n";);
ptr_buffer<equation> to_delete; ptr_buffer<equation> to_delete;
for (equation* target : m_to_simplify) { for (equation* target : m_to_simplify) {
if (simplify_source_target(eq, target) && is_trivial(target)) if (simplify_source_target(eq, target) && is_trivial(target))
@ -544,8 +543,8 @@ nex * nla_grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac
// let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 // let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
void nla_grobner::superpose(equation * eq1, equation * eq2) { void nla_grobner::superpose(equation * eq1, equation * eq2) {
TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2);); TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););
const nex * ab = get_highest_monomial(eq1->exp()); const nex * ab = get_highest_monomial(eq1->expr());
const nex * ac = get_highest_monomial(eq2->exp()); const nex * ac = get_highest_monomial(eq2->expr());
nex_mul *b, *c; nex_mul *b, *c;
TRACE("grobner", tout << "ab="; if(ab) { tout << *ab; } else { tout << "null"; }; TRACE("grobner", tout << "ab="; if(ab) { tout << *ab; } else { tout << "null"; };
tout << " , " << " ac="; if(ac) { tout << *ac; } else { tout << "null"; }; tout << "\n";); tout << " , " << " ac="; if(ac) { tout << *ac; } else { tout << "null"; }; tout << "\n";);
@ -554,8 +553,14 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
return; return;
} }
equation* eq = alloc(equation); equation* eq = alloc(equation);
init_equation(eq, expr_superpose( eq1->exp(), eq2->exp(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep())); init_equation(eq, expr_superpose( eq1->expr(), eq2->expr(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep()));
insert_to_simplify(eq); if (m_nex_creator.lt(eq->expr(), eq1->expr()) || m_nex_creator.lt(eq->expr(), eq2->expr())) {
TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";);
del_equation(eq);
} else {
insert_to_simplify(eq);
}
} }
void nla_grobner::register_report() { void nla_grobner::register_report() {
@ -689,8 +694,6 @@ void nla_grobner::compute_basis(){
} }
void nla_grobner::compute_basis_init(){ void nla_grobner::compute_basis_init(){
c().lp_settings().stats().m_grobner_basis_computatins++; c().lp_settings().stats().m_grobner_basis_computatins++;
m_num_of_equations = 0;
} }
bool nla_grobner::canceled() const { bool nla_grobner::canceled() const {
@ -700,7 +703,7 @@ bool nla_grobner::canceled() const {
bool nla_grobner::done() const { bool nla_grobner::done() const {
if ( if (
m_num_of_equations >= c().m_nla_settings.grobner_eqs_threshold() num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()
|| ||
canceled() canceled()
|| ||
@ -709,8 +712,8 @@ bool nla_grobner::done() const {
m_conflict) { m_conflict) {
TRACE("grobner", TRACE("grobner",
tout << "done() is true because of "; tout << "done() is true because of ";
if (m_num_of_equations >= c().m_nla_settings.grobner_eqs_threshold()) { if (num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()) {
tout << "m_num_of_equations = " << m_num_of_equations << "\n"; tout << "m_num_of_equations = " << num_of_equations() << "\n";
} else if (canceled()) { } else if (canceled()) {
tout << "canceled\n"; tout << "canceled\n";
} else if (m_reported > 100000) { } else if (m_reported > 100000) {
@ -800,7 +803,7 @@ void nla_grobner::display_equations(std::ostream & out, equation_set const & v,
} }
std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) const { std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) const {
out << "expr = " << *eq.exp() << "\n"; out << "expr = " << *eq.expr() << "\n";
display_dependency(out, eq.dep()); display_dependency(out, eq.dep());
return out; return out;
} }
@ -844,7 +847,7 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
unsigned bidx = m_equations_to_delete.size(); unsigned bidx = m_equations_to_delete.size();
eq->m_bidx = bidx; eq->m_bidx = bidx;
eq->dep() = dep; eq->dep() = dep;
eq->exp() = e; eq->expr() = e;
m_equations_to_delete.push_back(eq); m_equations_to_delete.push_back(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
} }

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

@ -66,8 +66,8 @@ class nla_grobner : common {
default: return 0; default: return 0;
} }
} }
nex* & exp() { return m_expr; } nex* & expr() { return m_expr; }
const nex* exp() const { return m_expr; } const nex* expr() const { return m_expr; }
ci_dependency * dep() const { return m_dep; } ci_dependency * dep() const { return m_dep; }
ci_dependency *& dep() { return m_dep; } ci_dependency *& dep() { return m_dep; }
unsigned hash() const { return m_bidx; } unsigned hash() const { return m_bidx; }
@ -80,7 +80,6 @@ class nla_grobner : common {
// fields // fields
equation_vector m_equations_to_delete; equation_vector m_equations_to_delete;
lp::int_set m_rows; lp::int_set m_rows;
unsigned m_num_of_equations;
grobner_stats m_stats; grobner_stats m_stats;
equation_set m_to_superpose; equation_set m_to_superpose;
equation_set m_to_simplify; equation_set m_to_simplify;
@ -147,7 +146,7 @@ private:
m_to_simplify.insert(eq); m_to_simplify.insert(eq);
} }
void insert_to_superpose(equation *eq) { void insert_to_superpose(equation *eq) {
SASSERT(m_nex_creator.is_simplified(eq->exp())); SASSERT(m_nex_creator.is_simplified(eq->expr()));
TRACE("nla_grobner", display_equation(tout, *eq);); TRACE("nla_grobner", display_equation(tout, *eq););
m_to_superpose.insert(eq); m_to_superpose.insert(eq);
} }
@ -168,5 +167,6 @@ private:
void check_eq(equation*); void check_eq(equation*);
void register_report(); void register_report();
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(); }
}; // end of grobner }; // end of grobner
} }