mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

smarter explanation.h (#4385)

Browse source 
* smarter explanation.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* clean explanation API

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* suppress warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* disable the warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-19 12:38:44 -07:00 committed by GitHub
parent 3b0c40044f
commit af2f74c05f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
16 changed files with 109 additions and 89 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

77
src/math/lp/explanation.h
View file

@ -18,47 +18,70 @@ Revision History:
--*/
#pragma once
#include <unordered_set>
#include "math/lp/lp_utils.h"
#include "util/map.h"
#include "util/optional.h"
namespace lp {
class explanation {
vector<std::pair<mpq, constraint_index>> m_explanation;
std::unordered_set<unsigned> m_set_of_ci;
u_map<optional<mpq>> m_j_to_mpq;
public:
explanation() {}
template <typename T>
explanation(const T& t) { for ( unsigned c : t) add(c); }
void clear() { m_explanation.clear(); m_set_of_ci.clear(); }
vector<std::pair<mpq, constraint_index>>::const_iterator begin() const { return m_explanation.begin(); }
vector<std::pair<mpq, constraint_index>>::const_iterator end() const { return m_explanation.end(); }
void push_justification(constraint_index j, const mpq& v) {
if (m_set_of_ci.find(j) != m_set_of_ci.end()) return;
m_set_of_ci.insert(j);
m_explanation.push_back(std::make_pair(v, j));
explanation(const T& t) {
for ( unsigned c : t)
push_back(c);
}
void push_justification(constraint_index j) {
if (m_set_of_ci.find(j) != m_set_of_ci.end()) return;
m_set_of_ci.insert(j);
m_explanation.push_back(std::make_pair(one_of_type<mpq>(), j));
void clear() { m_j_to_mpq.reset(); }
void add_with_coeff(constraint_index j, const mpq& v) {
SASSERT(m_j_to_mpq.contains(j) == false); // if we hit the assert then we
// might start using summation
m_j_to_mpq.insert(j, optional<mpq>(v));
}
// this signature is needed to use it in a template that also works for the vector type
void push_back(constraint_index j) {
push_justification(j);
if (m_j_to_mpq.contains(j))
return;
m_j_to_mpq.insert(j, optional<mpq>());
}
void add(const explanation& e) {
for (const auto& p: e.m_explanation) {
add(p.second);
void add_expl(const explanation& e) {
for (const auto& p: e.m_j_to_mpq) {
m_j_to_mpq.insert(p.m_key, p.m_value);
}
}
template <typename T>
void add_expl(const T& e) { for (auto j: e) add(j); }
void add(unsigned ci) { push_justification(ci); }
void add(const std::pair<mpq, constraint_index>& j) { push_justification(j.second, j.first); }
bool empty() const { return m_explanation.empty(); }
size_t size() const { return m_explanation.size(); }
void add_pair(const std::pair<mpq, constraint_index>& j) {
add_with_coeff(j.second, j.first);
}
bool empty() const { return m_j_to_mpq.empty(); }
size_t size() const { return m_j_to_mpq.size(); }
class cimpq {
constraint_index m_var;
const optional<mpq> & m_coeff;
public:
cimpq(constraint_index var, const optional<mpq> & val) : m_var(var), m_coeff(val) { }
constraint_index ci() const { return m_var; }
mpq coeff() const { return m_coeff.undef()? one_of_type<mpq>(): *m_coeff; }
};
class iterator {
u_map<optional<mpq>>::iterator m_it;
public:
cimpq operator*() const {
return cimpq(m_it->m_key, m_it->m_value);
}
iterator operator++() { iterator i = *this; m_it++; return i; }
iterator operator++(int) { m_it++; return *this; }
iterator(u_map<optional<mpq>>::iterator it) : m_it(it) {}
bool operator==(const iterator &other) const { return m_it == other.m_it; }
bool operator!=(const iterator &other) const { return !(*this == other); }
};
iterator begin() const { return iterator(m_j_to_mpq.begin()); }
iterator end() const { return iterator(m_j_to_mpq.end()); }
};
}

12
src/math/lp/gomory.cpp
View file

@ -67,7 +67,7 @@ class create_cut {
new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f);
lp_assert(new_a.is_pos());
m_k.addmul(new_a, lower_bound(j).x);
m_ex->push_justification(column_lower_bound_constraint(j));
m_ex->push_back(column_lower_bound_constraint(j));
}
else {
lp_assert(at_upper(j));
@ -75,7 +75,7 @@ class create_cut {
new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f));
lp_assert(new_a.is_neg());
m_k.addmul(new_a, upper_bound(j).x);
m_ex->push_justification(column_upper_bound_constraint(j));
m_ex->push_back(column_upper_bound_constraint(j));
}
m_t.add_monomial(new_a, j);
m_lcm_den = lcm(m_lcm_den, denominator(new_a));
@ -100,7 +100,7 @@ class create_cut {
}
m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than
// k += lower_bound(j).x * new_a;
m_ex->push_justification(column_lower_bound_constraint(j));
m_ex->push_back(column_lower_bound_constraint(j));
}
else {
lp_assert(at_upper(j));
@ -113,7 +113,7 @@ class create_cut {
new_a = a / m_one_minus_f;
}
m_k.addmul(new_a, upper_bound(j).x); // k += upper_bound(j).x * new_a;
m_ex->push_justification(column_upper_bound_constraint(j));
m_ex->push_back(column_upper_bound_constraint(j));
}
m_t.add_monomial(new_a, j);
TRACE("gomory_cut_detail_real", tout << "add " << new_a << "*v" << j << ", k: " << m_k << "\n";
@ -320,8 +320,8 @@ public:
// use -p.coeff() to make the format compatible with the format used in: Integrating Simplex with DPLL(T)
try {
if (lia.is_fixed(j)) {
m_ex->push_justification(column_lower_bound_constraint(j));
m_ex->push_justification(column_upper_bound_constraint(j));
m_ex->push_back(column_lower_bound_constraint(j));
m_ex->push_back(column_upper_bound_constraint(j));
continue;
}
if (is_real(j)) {

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

@ -263,7 +263,7 @@ namespace lp {
lia.settings().stats().m_hnf_cuts++;
lia.m_ex->clear();
for (unsigned i : constraints_for_explanation()) {
lia.m_ex->push_justification(i);
lia.m_ex->push_back(i);
}
}
return r;

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

@ -30,7 +30,7 @@ public:
// for a column element it points to the row element offset
unsigned m_other;
indexed_value() {}
indexed_value(T v, unsigned i) : m_value(v), m_index(i) {}
indexed_value(T v, unsigned i, unsigned other) :
m_value(v), m_index(i), m_other(other) {
}

5
src/math/lp/int_branch.cpp
View file

@ -51,7 +51,6 @@ lia_move int_branch::create_branch_on_column(int j) {
}
int int_branch::find_inf_int_base_column() {
int result = -1;
mpq range;
@ -59,7 +58,7 @@ int int_branch::find_inf_int_base_column() {
mpq small_range_thresold(1024);
unsigned n = 0;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
unsigned prev_usage;
unsigned prev_usage = 0; // to quiet down the compile
unsigned k = 0;
unsigned usage;
unsigned j;
@ -103,5 +102,5 @@ int int_branch::find_inf_int_base_column() {
}
return result;
}
}

4
src/math/lp/int_gcd_test.cpp
View file

@ -210,8 +210,8 @@ namespace lp {
void int_gcd_test::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
constraint_index lc, uc;
lra.get_bound_constraint_witnesses_for_column(j, lc, uc);
lia.m_ex->push_justification(lc);
lia.m_ex->push_justification(uc);
lia.m_ex->push_back(lc);
lia.m_ex->push_back(uc);
}
}

12
src/math/lp/lar_solver.cpp
View file

@ -307,8 +307,8 @@ void lar_solver::fill_explanation_from_crossed_bounds_column(explanation & evide
// this is the case when the lower bound is in conflict with the upper one
const ul_pair & ul = m_columns_to_ul_pairs[m_crossed_bounds_column];
evidence.push_justification(ul.upper_bound_witness(), numeric_traits<mpq>::one());
evidence.push_justification(ul.lower_bound_witness(), -numeric_traits<mpq>::one());
evidence.add_with_coeff(ul.upper_bound_witness(), numeric_traits<mpq>::one());
evidence.add_with_coeff(ul.lower_bound_witness(), -numeric_traits<mpq>::one());
}
@ -1097,9 +1097,9 @@ bool lar_solver::inf_explanation_is_correct() const {
mpq lar_solver::sum_of_right_sides_of_explanation(explanation& exp) const {
mpq ret = numeric_traits<mpq>::zero();
for (auto & it : exp) {
mpq coeff = it.first;
constraint_index con_ind = it.second;
for (auto it : exp) {
mpq coeff = it.coeff();
constraint_index con_ind = it.ci();
lp_assert(m_constraints.valid_index(con_ind));
ret += (m_constraints[con_ind].rhs() - m_constraints[con_ind].get_free_coeff_of_left_side()) * coeff;
}
@ -1195,7 +1195,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.lower_bound_witness();
lp_assert(m_constraints.valid_index(bound_constr_i));
exp.push_justification(bound_constr_i, coeff);
exp.add_with_coeff(bound_constr_i, coeff);
}
}

28
src/math/lp/nla_core.cpp
View file

@ -259,9 +259,9 @@ std::ostream& core::print_monic_with_vars(const monic& m, std::ostream& out) con
std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const {
out << "expl: ";
unsigned i = 0;
for (auto &p : exp) {
out << "(" << p.second << ")";
m_lar_solver.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.second);
for (auto p : exp) {
out << "(" << p.ci() << ")";
m_lar_solver.constraints().display(out, [this](lpvar j) { return var_str(j);}, p.ci());
if (++i < exp.size())
out << " ";
}
@ -312,7 +312,7 @@ bool core::explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& boun
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_lower_bound(p.column()).x;
e.add(c);
e.push_back(c);
return true;
}
// a.is_neg()
@ -320,7 +320,7 @@ bool core::explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& boun
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_upper_bound(p.column()).x;
e.add(c);
e.push_back(c);
return true;
}
@ -334,7 +334,7 @@ bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& boun
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_lower_bound(j).x;
e.add(c);
e.push_back(c);
return true;
}
// a.is_pos()
@ -342,7 +342,7 @@ bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& boun
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_upper_bound(j).x;
e.add(c);
e.push_back(c);
return true;
}
@ -855,7 +855,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
}
}
for (const auto& p : l.expl()) {
const auto& c = m_lar_solver.constraints()[p.second];
const auto& c = m_lar_solver.constraints()[p.ci()];
for (const auto& r : c.coeffs()) {
insert_j(r.second);
}
@ -1060,7 +1060,7 @@ lemma& new_lemma::current() const {
}
new_lemma& new_lemma::operator&=(lp::explanation const& e) {
expl().add(e);
expl().add_expl(e);
return *this;
}
@ -1124,7 +1124,7 @@ new_lemma& new_lemma::explain_var_separated_from_zero(lpvar j) {
new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) {
SASSERT(c.has_lower_bound(j));
lp::explanation ex;
ex.add(c.m_lar_solver.get_column_lower_bound_witness(j));
ex.push_back(c.m_lar_solver.get_column_lower_bound_witness(j));
*this &= ex;
TRACE("nla_solver", tout << j << ": " << *this << "\n";);
return *this;
@ -1133,7 +1133,7 @@ new_lemma& new_lemma::explain_existing_lower_bound(lpvar j) {
new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) {
SASSERT(c.has_upper_bound(j));
lp::explanation ex;
ex.add(c.m_lar_solver.get_column_upper_bound_witness(j));
ex.push_back(c.m_lar_solver.get_column_upper_bound_witness(j));
*this &= ex;
return *this;
}
@ -1141,9 +1141,9 @@ new_lemma& new_lemma::explain_existing_upper_bound(lpvar j) {
std::ostream& new_lemma::display(std::ostream & out) const {
auto const& lemma = current();
for (auto &p : lemma.expl()) {
out << "(" << p.second << ") ";
c.m_lar_solver.constraints().display(out, [this](lpvar j) { return c.var_str(j);}, p.second);
for (auto p : lemma.expl()) {
out << "(" << p.ci() << ") ";
c.m_lar_solver.constraints().display(out, [this](lpvar j) { return c.var_str(j);}, p.ci());
}
out << " ==> ";
if (lemma.ineqs().empty()) {

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

@ -214,9 +214,9 @@ u_dependency *intervals::mk_dep(const lp::explanation& expl) {
u_dependency * r = nullptr;
for (auto p : expl) {
if (r == nullptr) {
r = m_dep_intervals.mk_leaf(p.second);
r = m_dep_intervals.mk_leaf(p.ci());
} else {
r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.second));
r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.ci()));
}
}
return r;
@ -285,7 +285,7 @@ bool intervals::interval_from_term(const nex& e, scoped_dep_interval& i) {
m_dep_intervals.set_interval_for_scalar(i, b);
if (wd == e_with_deps::with_deps) {
for (auto p : exp) {
i.get().m_lower_dep = mk_join(i.get().m_lower_dep, mk_leaf(p.second));
i.get().m_lower_dep = mk_join(i.get().m_lower_dep, mk_leaf(p.ci()));
}
i.get().m_upper_dep = i.get().m_lower_dep;
}

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

@ -94,7 +94,7 @@ struct solver::imp {
m_nlsat->get_core(core);
for (auto c : core) {
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
ex.push_justification(idx, rational(1));
ex.push_back(idx);
TRACE("arith", tout << "ex: " << idx << "\n";);
}
nla::new_lemma lemma(m_nla_core, __FUNCTION__);

4
src/math/lp/square_sparse_matrix_def.h
View file

@ -110,7 +110,7 @@ void square_sparse_matrix<T, X>::set_with_no_adjusting_for_row(unsigned row, uns
}
}
// have not found the column between the indices
row_vec.push_back(indexed_value<T>(val, col)); // what about m_other ???
row_vec.push_back(indexed_value<T>(val, col, -1));
}
template <typename T, typename X>
@ -123,7 +123,7 @@ void square_sparse_matrix<T, X>::set_with_no_adjusting_for_col(unsigned row, uns
}
}
// have not found the column between the indices
col_vec.push_back(indexed_value<T>(val, row)); // what about m_other ???
col_vec.push_back(indexed_value<T>(val, row, -1));
}

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

@ -43,7 +43,7 @@ public:
void explain(lp::explanation& e) const {
for (lpci c : m_cs)
if (c + 1 != 0) // c != -1
e.add(c);
e.push_back(c);
}
};

22
src/smt/theory_lra.cpp
View file

@ -2018,11 +2018,11 @@ public:
}
}
for (auto const& ev : ex) {
lp().constraints().display(out << ev.first << ": ", ev.second);
lp().constraints().display(out << ev.coeff() << ": ", ev.ci());
}
expr_ref_vector fmls(m);
for (auto const& ev : ex) {
fmls.push_back(constraint2fml(ev.second));
fmls.push_back(constraint2fml(ev.ci()));
}
expr_ref t(term2expr(term), m);
if (upper) {
@ -2081,9 +2081,7 @@ public:
// m_explanation implies term <= k
reset_evidence();
for (auto const& ev : m_explanation) {
if (!ev.first.is_zero()) {
set_evidence(ev.second, m_core, m_eqs);
}
set_evidence(ev.ci(), m_core, m_eqs);
}
// The call mk_bound() can set the m_infeasible_column in lar_solver
// so the explanation is safer to take before this call.
@ -2335,7 +2333,7 @@ public:
void consume(rational const& v, lp::constraint_index j) override {
m_imp.set_evidence(j, m_imp.m_core, m_imp.m_eqs);
m_imp.m_explanation.push_justification(j, v);
m_imp.m_explanation.add_with_coeff(j, v);
}
};
@ -3273,9 +3271,7 @@ public:
TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"););
for (auto const& ev : m_explanation) {
if (!ev.first.is_zero()) {
set_evidence(ev.second, m_core, m_eqs);
}
set_evidence(ev.ci(), m_core, m_eqs);
}
// SASSERT(validate_conflict(m_core, m_eqs));
dump_conflict(m_core, m_eqs);
@ -3785,11 +3781,11 @@ public:
void display_evidence(std::ostream& out, lp::explanation const& evidence) {
for (auto const& ev : evidence) {
expr_ref e(m);
SASSERT(!ev.first.is_zero());
if (ev.first.is_zero()) {
SASSERT(!ev.coeff().is_zero());
if (ev.coeff().is_zero()) {
continue;
}
unsigned idx = ev.second;
unsigned idx = ev.ci();
switch (m_constraint_sources.get(idx, null_source)) {
case inequality_source: {
literal lit = m_inequalities[idx];
@ -3816,7 +3812,7 @@ public:
}
}
for (auto const& ev : evidence) {
lp().constraints().display(out << ev.first << ": ", ev.second);
lp().constraints().display(out << ev.coeff() << ": ", ev.ci());
}
}

8
src/test/lp/gomory_test.h
View file

@ -67,7 +67,7 @@ struct gomory_test {
}
k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than
// k += lower_bound(x_j).x * new_a;
expl.push_justification(column_lower_bound_constraint(x_j), new_a);
expl.add_with_coeff(column_lower_bound_constraint(x_j), new_a);
}
else {
lp_assert(at_upper(x_j));
@ -79,7 +79,7 @@ struct gomory_test {
new_a = a / (mpq(1) - f_0);
}
k.addmul(new_a, upper_bound(x_j).x); // k += upper_bound(x_j).x * new_a;
expl.push_justification(column_upper_bound_constraint(x_j), new_a);
expl.add_with_coeff(column_upper_bound_constraint(x_j), new_a);
}
TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << k << "\n";);
pol.add_monomial(new_a, x_j);
@ -107,7 +107,7 @@ struct gomory_test {
new_a = (1 - f_j) / f_0;
}
k.addmul(new_a, lower_bound(x_j).x);
expl.push_justification(column_lower_bound_constraint(x_j), new_a);
expl.add_with_coeff(column_lower_bound_constraint(x_j), new_a);
}
else {
lp_assert(at_upper(x_j));
@ -119,7 +119,7 @@ struct gomory_test {
}
new_a.neg(); // the upper terms are inverted
k.addmul(new_a, upper_bound(x_j).x);
expl.push_justification(column_upper_bound_constraint(x_j), new_a);
expl.add_with_coeff(column_upper_bound_constraint(x_j), new_a);
}
TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << k << "\n";);
t.add_monomial(new_a, x_j);

2
src/test/lp/lp.cpp
View file

@ -78,6 +78,7 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
}
void test_nex_order() {
#if Z3DEBUG
enable_trace("nla_cn");
enable_trace("nla_cn_details");
// enable_trace("nla_cn_details_");
@ -116,6 +117,7 @@ void test_nex_order() {
nex_mul * poly = r.mk_mul(five_a_pl_one, b);
nex * p = r.simplify(poly);
std::cout << "poly = " << *poly << " , p = " << *p << "\n";
#endif
}
void test_simplify() {

10
src/test/lp/nla_solver_test.cpp
View file

@ -218,7 +218,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
}
}
SASSERT(found0 && (found1 || found2));
VERIFY(found0 && (found1 || found2));
}
@ -289,7 +289,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
}
SASSERT(found0 && found1 && found2 && found3);
VERIFY(found0 && found1 && found2 && found3);
}
void test_basic_lemma_for_mon_neutral_from_factors_to_monomial() {
@ -364,7 +364,7 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
}
}
SASSERT(found0 && found1);
VERIFY(found0 && found1);
}
void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
@ -416,7 +416,7 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
}
}
SASSERT(found0 && found1 && found2);
VERIFY(found0 && found1 && found2);
}
@ -488,7 +488,7 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
}
}
SASSERT(found0 && found1);
VERIFY(found0 && found1);
}
void test_horner() {