mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

in grobner optional treatment of fixed vars in rows, remove a field

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-05 16:19:17 -10:00
parent 0b1023c2c7
commit e62913999e
3 changed files with 13 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -129,8 +129,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
if (!c().is_monic_var(j)) { if (!c().is_monic_var(j)) {
if (fixed_as_scalars && c().var_is_fixed(j)) { if (fixed_as_scalars && c().var_is_fixed(j)) {
auto & b = c().m_lar_solver.get_lower_bound(j).x; auto & b = c().m_lar_solver.get_lower_bound(j).x;
if (b.is_zero()) if (b.is_zero()) {
TRACE("nla_grobner", tout << "[" << j << "] is fixed to zero\n";);
return nullptr; return nullptr;
}
return cn.mk_scalar(coeff * b); return cn.mk_scalar(coeff * b);
} }
c().insert_to_active_var_set(j); c().insert_to_active_var_set(j);
@ -150,9 +152,9 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
} }
c().insert_to_active_var_set(k); c().insert_to_active_var_set(k);
e->add_child(cn.mk_var(k)); e->add_child(cn.mk_var(k));
CTRACE("nla_horner", c().is_monic_var(k), c().print_var(k, tout) << "\n";); CTRACE("nla_grobner", c().is_monic_var(k), c().print_var(k, tout) << "\n";);
} }
TRACE("nla_cn", tout << *e;); TRACE("nla_grobner", tout << *e;);
return e; return e;
} }

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

@ -25,7 +25,9 @@ nla_grobner::nla_grobner(core *c, intervals *s)
: common(c, s), : common(c, s),
m_nl_gb_exhausted(false), m_nl_gb_exhausted(false),
m_dep_manager(m_val_manager, m_alloc), m_dep_manager(m_val_manager, m_alloc),
m_changed_leading_term(false) {} m_changed_leading_term(false),
m_look_for_fixed_vars_in_rows(false)
{}
bool nla_grobner::internalize_gb_eq(equation* ) { bool nla_grobner::internalize_gb_eq(equation* ) {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
@ -139,14 +141,11 @@ void nla_grobner::add_row(unsigned i) {
} }
); );
nex_sum * ns = m_nex_creator.mk_sum(); nex_sum * ns = m_nex_creator.mk_sum();
create_sum_from_row(row, m_nex_creator, *ns, m_look_for_fixed_vars_in_rows);
svector<lp::constraint_index> fixed_vars_constraints;
create_sum_from_row(row, m_nex_creator, *ns, true); // true to treat fixed vars as scalars
nex* e = m_nex_creator.simplify(ns); nex* e = m_nex_creator.simplify(ns);
TRACE("grobner", tout << "e = " << *e << "\n";); TRACE("grobner", tout << "e = " << *e << "\n";);
m_tmp_var_set.clear(); m_tmp_var_set.clear();
assert_eq_0(e, get_fixed_vars_dep_from_row(row, m_dep_manager)); assert_eq_0(e, m_look_for_fixed_vars_in_rows? get_fixed_vars_dep_from_row(row, m_dep_manager) : nullptr);
} }
void nla_grobner::simplify_equations_to_process() { void nla_grobner::simplify_equations_to_process() {
@ -158,7 +157,6 @@ void nla_grobner::simplify_equations_to_process() {
void nla_grobner::init() { void nla_grobner::init() {
m_reported = 0; m_reported = 0;
m_conflict = false; m_conflict = false;
m_equations_to_unfreeze.clear();
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_num_of_equations = 0;
@ -243,7 +241,6 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) {
TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq);); TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq););
return result ? eq : nullptr; return result ? eq : nullptr;
} }
const nex* nla_grobner::get_highest_monomial(const nex* e) const { const nex* nla_grobner::get_highest_monomial(const nex* e) const {
@ -288,7 +285,7 @@ unsigned nla_grobner::find_divisible(nex_sum* targ_sum,
for (unsigned j = 0; j < targ_sum->size(); j++) { for (unsigned j = 0; j < targ_sum->size(); j++) {
auto t = (*targ_sum)[j]; auto t = (*targ_sum)[j];
if (divide_ignore_coeffs_check_only(t, high_mon)) { if (divide_ignore_coeffs_check_only(t, high_mon)) {
TRACE("grobner", tout << "yes div: " << *targ_sum << " / " << *high_mon << "\n";); TRACE("grobner", tout << "yes div: " << *t << " / " << *high_mon << "\n";);
return j; return j;
} }
} }
@ -461,7 +458,6 @@ nla_grobner::equation * nla_grobner::simplify_source_target(equation * source, e
void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove) { void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove) {
if (new_target != target) { if (new_target != target) {
m_equations_to_unfreeze.push_back(target);
to_remove.push_back(target); to_remove.push_back(target);
if (m_changed_leading_term) { if (m_changed_leading_term) {
insert_to_simplify(new_target); insert_to_simplify(new_target);
@ -530,7 +526,6 @@ void nla_grobner::simplify_to_superpose(equation* eq) {
for (equation* target : m_to_simplify) { for (equation* target : m_to_simplify) {
equation * new_target = simplify_source_target(eq, target); equation * new_target = simplify_source_target(eq, target);
if (new_target != nullptr && new_target != target) { if (new_target != nullptr && new_target != target) {
m_equations_to_unfreeze.push_back(target);
to_insert.push_back(new_target); to_insert.push_back(new_target);
to_remove.push_back(target); to_remove.push_back(target);
target = new_target; target = new_target;
@ -695,7 +690,6 @@ bool nla_grobner::compute_basis_step() {
equation * new_eq = simplify_using_processed(eq); equation * new_eq = simplify_using_processed(eq);
if (new_eq != nullptr && eq != new_eq) { if (new_eq != nullptr && eq != new_eq) {
// equation was updated using non destructive updates // equation was updated using non destructive updates
m_equations_to_unfreeze.push_back(eq);
eq = new_eq; eq = new_eq;
} }
if (canceled()) return false; if (canceled()) return false;
@ -882,7 +876,7 @@ std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency*
{ {
lp::explanation e(expl); lp::explanation e(expl);
if (!expl.empty()) { if (!expl.empty()) {
out << "upper constraints\n"; out << "constraints\n";
m_core->print_explanation(e, out); m_core->print_explanation(e, out);
}else { }else {
out << "no constraints\n"; out << "no constraints\n";

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

@ -78,7 +78,6 @@ class nla_grobner : common {
typedef ptr_vector<equation> equation_vector; typedef ptr_vector<equation> equation_vector;
// fields // fields
equation_vector m_equations_to_unfreeze;
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; unsigned m_num_of_equations;
@ -95,6 +94,7 @@ class nla_grobner : common {
bool m_changed_leading_term; bool m_changed_leading_term;
unsigned m_reported; unsigned m_reported;
bool m_conflict; bool m_conflict;
bool m_look_for_fixed_vars_in_rows;
public: public:
nla_grobner(core *core, intervals *); nla_grobner(core *core, intervals *);
void grobner_lemmas(); void grobner_lemmas();