mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

add dependencies for row in grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-10 17:10:02 -10:00
parent 03f7c96c5a
commit a86d4b0675
6 changed files with 55 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/horner.cpp
View file

@ -78,7 +78,7 @@ bool horner::lemmas_on_row(const T& row) {
SASSERT (row_is_interesting(row));
c().clear_and_resize_active_var_set();
create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars);
create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_as_scalars, nullptr);
set_active_vars_weights(); // without this call the comparisons will be incorrect
nex* e = m_nex_creator.simplify(&m_row_sum);
TRACE("nla_horner", tout << "e = " << * e << "\n";);

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

@ -159,20 +159,33 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, bool fixe
}
template <typename T> void common::create_sum_from_row(const T& row,
nex_creator& cn,
nex_sum& sum, bool fixed_as_scalars) {
template <typename T> common::ci_dependency* common::create_sum_from_row(const T& row,
nex_creator& cn,
nex_sum& sum,
bool fixed_as_scalars,
ci_dependency_manager* dep_manager
) {
TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
ci_dependency * dep = nullptr;
SASSERT(row.size() > 1);
sum.children().clear();
for (const auto &p : row) {
nex* e = nexvar(p.coeff(), p.var(), cn, fixed_as_scalars);
if (e)
sum.add_child(e);
if (!e)
continue;
unsigned lc, uc;
if (dep_manager) {
c().m_lar_solver.get_bound_constraint_witnesses_for_column(p.var(), lc, uc);
if (lc + 1)
dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(lc));
if (uc + 1)
dep = dep_manager->mk_join(dep, dep_manager->mk_leaf(uc));
sum.add_child(e);
}
}
TRACE("nla_horner", tout << "sum =" << sum << "\n";);
TRACE("nla_grobner", tout << "sum =" << sum << "\ndep="; m_intervals->print_dependencies(dep, tout););
return dep;
}
template <typename T>
@ -242,6 +255,6 @@ var_weight common::get_var_weight(lpvar j) const {
}
template void nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, bool);
template nla::common::ci_dependency* nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, bool, ci_dependency_manager*);
template dependency_manager<nla::common::ci_dependency_config>::dependency* nla::common::get_fixed_vars_dep_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, dependency_manager<nla::common::ci_dependency_config>&);

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

@ -122,7 +122,7 @@ struct common {
// nex* nexvar(lpvar j, nex_creator&, svector<lp::constraint_index> & fixed_vars_constraints);
nex* nexvar(const rational& coeff, lpvar j, nex_creator&, bool);
template <typename T>
void create_sum_from_row(const T&, nex_creator&, nex_sum&, bool);
ci_dependency* create_sum_from_row(const T&, nex_creator&, nex_sum&, bool, ci_dependency_manager*);
template <typename T>
ci_dependency* get_fixed_vars_dep_from_row(const T&, ci_dependency_manager& dep_manager);
void set_active_vars_weights();

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

@ -129,11 +129,10 @@ void nla_grobner::add_row(unsigned i) {
}
);
nex_sum * ns = m_nex_creator.mk_sum();
create_sum_from_row(row, m_nex_creator, *ns, m_look_for_fixed_vars_in_rows);
ci_dependency* dep = create_sum_from_row(row, m_nex_creator, *ns, m_look_for_fixed_vars_in_rows, &m_dep_manager);
nex* e = m_nex_creator.simplify(ns);
TRACE("grobner", tout << "e = " << *e << "\n";);
m_tmp_var_set.clear();
assert_eq_0(e, m_look_for_fixed_vars_in_rows? get_fixed_vars_dep_from_row(row, m_dep_manager) : nullptr);
assert_eq_0(e, dep);
}
void nla_grobner::simplify_equations_in_m_to_simplify() {
@ -144,7 +143,6 @@ void nla_grobner::simplify_equations_in_m_to_simplify() {
void nla_grobner::init() {
m_reported = 0;
m_conflict = false;
del_equations(0);
SASSERT(m_equations_to_delete.size() == 0);
m_to_superpose.reset();
@ -566,8 +564,7 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
void nla_grobner::register_report() {
m_reported++;
if (c().current_lemma().expl().size() == 0)
m_conflict = true;
m_conflict = true;
}
// Let a be the greatest common divider of ab and bc,
// then ab/a is stored in b, and ac/a is stored in c
@ -833,10 +830,12 @@ std::unordered_set<lpvar> nla_grobner::get_vars_of_expr_with_opening_terms(const
void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
if (e == nullptr || is_zero_scalar(e))
return;
m_tmp_var_set.clear();
equation * eq = alloc(equation);
init_equation(eq, e, dep);
TRACE("grobner",
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";
@ -866,7 +865,9 @@ std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency*
out << "constraints\n";
m_core->print_explanation(e, out);
out << "\n";
}
} else {
out << "no deps\n";
}
}
return out;

44
src/math/lp/nla_intervals.cpp
View file

@ -244,9 +244,24 @@ intervals::interv intervals::interval_of_mul(const nex_mul* e) {
return a;
}
std::ostream & intervals::print_dependencies(ci_dependency* deps , std::ostream& out) const {
svector<lp::constraint_index> expl;
m_dep_manager.linearize(deps, expl);
{
lp::explanation e(expl);
if (!expl.empty()) {
m_core->print_explanation(e, out);
expl.clear();
} else {
out << "\nno constraints\n";
}
}
return out;
}
// return true iff the interval of n is does not contain 0
bool intervals::check_nex(const nex* n, ci_dependency* initial_deps) {
TRACE("nla_grobner", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";);
TRACE("nla_grobner", tout << "n = " << *n << "\n";);
m_core->lp_settings().stats().m_cross_nested_forms++;
auto i = interval_of_expr(n, 1);
@ -256,7 +271,7 @@ bool intervals::check_nex(const nex* n, ci_dependency* initial_deps) {
return false;
}
auto interv_wd = interval_of_expr_with_deps(n, 1);
TRACE("nla_grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n";);
TRACE("nla_grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) << *n << "\n, initial deps\n"; print_dependencies(initial_deps, tout););
check_interval_for_conflict_on_zero(interv_wd, initial_deps);
reset(); // clean the memory allocated by the interval bound dependencies
return true;
@ -615,26 +630,13 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]");
}
svector<lp::constraint_index> expl;
m_dep_manager.linearize(i.m_lower_dep, expl);
{
lp::explanation e(expl);
if (!expl.empty()) {
out << "\nlower constraints\n";
m_core->print_explanation(e, out);
expl.clear();
} else {
out << "\nno lower constraints\n";
}
if (i.m_lower_dep) {
out << "\nlower deps\n";
print_dependencies(i.m_lower_dep, out);
}
m_dep_manager.linearize(i.m_upper_dep, expl);
{
lp::explanation e(expl);
if (!expl.empty()) {
out << "upper constraints\n";
m_core->print_explanation(e, out);
}else {
out << "no upper constraints\n";
}
if (i.m_upper_dep) {
out << "\nupper deps\n";
print_dependencies(i.m_upper_dep, out);
}
return out;
}

1
src/math/lp/nla_intervals.h
View file

@ -167,6 +167,7 @@ public:
interval mul(const svector<lpvar>&) const;
void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
std::ostream & print_dependencies(ci_dependency* , std::ostream&) const;
std::ostream& print_explanations(const svector<lp::constraint_index> &, std::ostream&) const;
std::ostream& display(std::ostream& out, const intervals::interval& i) const;
void set_lower(interval & a, rational const & n) const { m_config.set_lower(a, n.to_mpq()); }