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

NB's review

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-12 11:33:18 -10:00
parent 3f442ecef9
commit 882b8ee63b
5 changed files with 80 additions and 125 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/math/lp/nex.h
View file

@ -100,7 +100,7 @@ public:
std::string str() const { std::stringstream ss; print(ss); return ss.str(); }
virtual ~nex() {}
virtual bool contains(lpvar j) const { return false; }
virtual int get_degree() const = 0;
virtual unsigned get_degree() const = 0;
// simplifies the expression and also assigns the address of "this" to *e
virtual const rational& coeff() const { return rational::one(); }
@ -125,7 +125,7 @@ public:
std::ostream & print(std::ostream& out) const override { return out << "v" << m_j; }
bool contains(lpvar j) const { return j == m_j; }
int get_degree() const override { return 1; }
unsigned get_degree() const override { return 1; }
bool is_linear() const override { return true; }
};
@ -139,21 +139,21 @@ public:
rational& value() { return m_v; } // the setter
std::ostream& print(std::ostream& out) const override { return out << m_v; }
int get_degree() const override { return 0; }
unsigned get_degree() const override { return 0; }
bool is_linear() const override { return true; }
};
class nex_pow {
nex* m_e;
int m_power;
unsigned m_power;
public:
explicit nex_pow(nex* e): m_e(e), m_power(1) {}
explicit nex_pow(nex* e, int p): m_e(e), m_power(p) {}
explicit nex_pow(nex* e, unsigned p): m_e(e), m_power(p) {}
const nex * e() const { return m_e; }
nex *& e() { return m_e; }
nex ** ee() { return & m_e; }
int pow() const { return m_power; }
unsigned pow() const { return m_power; }
std::ostream& print(std::ostream& s) const {
if (pow() == 1) {
@ -286,7 +286,7 @@ public:
TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";);
}
int get_degree() const override {
unsigned get_degree() const override {
return get_degree_children(children());
}
@ -316,7 +316,6 @@ public:
ptr_vector<nex>& children() { return m_children;}
const ptr_vector<nex>& children() const { return m_children;}
const ptr_vector<nex>* children_ptr() const { return &m_children;}
ptr_vector<nex>* children_ptr() { return &m_children;}
unsigned size() const override { return m_children.size(); }
@ -369,8 +368,8 @@ public:
return out;
}
int get_degree() const override {
int degree = 0;
unsigned get_degree() const override {
unsigned degree = 0;
for (auto e : *this) {
degree = std::max(degree, e->get_degree());
}

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

@ -561,7 +561,7 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
children.shrink(k);
for (nex *e : to_promote) {
for (nex *ee : *(e->to_sum().children_ptr())) {
for (nex *ee : e->to_sum()) {
if (!is_zero_scalar(ee))
children.push_back(ee);
}

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

@ -54,7 +54,7 @@ bool grobner::internalize_gb_eq(equation* ) {
}
void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) {
SASSERT(!c().active_var_set_contains(j) && !c().var_is_fixed(j));
if (c().active_var_set_contains(j) || c().var_is_fixed(j)) return;
TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";);
const auto& matrix = c().m_lar_solver.A_r();
c().insert_to_active_var_set(j);
@ -62,16 +62,13 @@ void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::qu
for (auto & s : matrix.m_columns[j]) {
unsigned row = s.var();
if (m_rows.contains(row)) continue;
lpvar basic_in_row = core_slv.m_r_basis[row];
if (false && c().var_is_free(basic_in_row)) {
if (false && c().var_is_free(core_slv.m_r_basis[row])) {
TRACE("grobner", tout << "ignore the row " << row << " with the free basic var\n";);
continue; // mimic the behavior of the legacy solver
}
m_rows.insert(row);
for (auto& rc : matrix.m_rows[row]) {
if (c().active_var_set_contains(rc.var()) || c().var_is_fixed(rc.var()))
continue;
q.push(rc.var());
add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
}
}
@ -81,9 +78,7 @@ void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::qu
const monic& m = c().emons()[j];
for (auto fcn : factorization_factory_imp(m, c())) {
for (const factor& fc: fcn) {
lpvar j = var(fc);
if (!c().active_var_set_contains(j) && !c().var_is_fixed(j))
add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
q.push(var(fc));
}
}
}
@ -93,18 +88,12 @@ void grobner::find_nl_cluster() {
std::queue<lpvar> q;
for (lpvar j : c().m_to_refine) {
TRACE("grobner", c().print_monic(c().emons()[j], tout) << "\n";);
if (c().var_is_fixed(j)) {
TRACE("grobner", tout << "skip fixed var " << j << "\n";);
continue;
}
q.push(j);
}
while (!q.empty()) {
unsigned j = q.front();
lpvar j = q.front();
q.pop();
if (c().active_var_set_contains(j))
continue;
add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
}
set_active_vars_weights();
@ -126,13 +115,13 @@ void grobner::display_matrix(std::ostream & out) const {
c().print_term(r, out) << std::endl;
}
}
std::ostream & grobner::display(std::ostream & out) const {
display_equations(out, m_to_superpose, "m_to_superpose:");
display_equations(out, m_to_simplify, "m_to_simplify:");
return out;
}
common::ci_dependency* grobner::dep_from_vector(svector<lp::constraint_index> & cs) {
ci_dependency * d = nullptr;
for (auto c : cs)
@ -143,10 +132,7 @@ common::ci_dependency* grobner::dep_from_vector(svector<lp::constraint_index> &
void grobner::add_row(unsigned i) {
const auto& row = c().m_lar_solver.A_r().m_rows[i];
TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n';
for (auto p : row) {
c().print_var(p.var(), tout) << "\n";
}
);
for (auto p : row) c().print_var(p.var(), tout) << "\n"; );
nex_sum * ns = m_nex_creator.mk_sum();
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);
@ -154,12 +140,6 @@ void grobner::add_row(unsigned i) {
assert_eq_0(e, dep);
}
void grobner::simplify_equations_in_m_to_simplify() {
for (equation *eq : m_to_simplify) {
eq->expr() = m_nex_creator.simplify(eq->expr());
}
}
void grobner::init() {
m_reported = 0;
del_equations(0);
@ -173,7 +153,9 @@ void grobner::init() {
for (unsigned i : m_rows) {
add_row(i);
}
simplify_equations_in_m_to_simplify();
for (equation* eq : m_to_simplify) {
eq->expr() = m_nex_creator.simplify(eq->expr());
}
}
bool grobner::is_trivial(equation* eq) const {
@ -225,24 +207,20 @@ grobner::equation* grobner::simplify_using_to_superpose(equation* eq) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
do {
simplified = false;
for (equation * p : m_to_superpose) {
for (equation* p : m_to_superpose) {
if (simplify_source_target(p, eq)) {
result = true;
result = true;
simplified = true;
}
}
if (canceled()) {
return nullptr;
}
if (eq->expr()->is_scalar())
break;
if (eq->expr()->is_scalar()) {
break;
}
}
if (eq->expr()->is_scalar())
break;
}
while (simplified);
if (result && eq->expr()->is_scalar()) {
TRACE("grobner",);
}
while (simplified && !eq->expr()->is_scalar());
TRACE("grobner", tout << "simplification result: "; display_equation(tout, *eq););
return result ? eq : nullptr;
@ -285,23 +263,22 @@ bool grobner::simplify_target_monomials(equation * source, equation * target) {
return simplify_target_monomials_sum(source, target, targ_sum, high_mon);
}
unsigned grobner::find_divisible(nex_sum* targ_sum,
const nex* high_mon) const {
for (unsigned j = 0; j < targ_sum->size(); j++) {
auto t = (*targ_sum)[j];
unsigned grobner::find_divisible(nex_sum* targ_sum, const nex* high_mon) const {
unsigned j = 0;
for (auto t : *targ_sum) {
if (divide_ignore_coeffs_check_only(t, high_mon)) {
TRACE("grobner", tout << "yes div: " << *t << " / " << *high_mon << "\n";);
return j;
}
++j;
}
TRACE("grobner", tout << "no div: " << *targ_sum << " / " << *high_mon << "\n";);
return -1;
}
bool grobner::simplify_target_monomials_sum(equation * source,
equation * target, nex_sum* targ_sum,
const nex* high_mon) {
equation * target, nex_sum* targ_sum,
const nex* high_mon) {
unsigned j = find_divisible(targ_sum, high_mon);
if (j + 1 == 0)
return false;
@ -333,8 +310,8 @@ bool grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h)
bool p_swallowed = false;
for (; j < t->size() && !p_swallowed; j++) {
auto &tp = (*t)[j];
if (to_var(tp.e())->var() == h_var) {
if (tp.pow() >= static_cast<int>(h->get_child_pow(k))) {
if (tp.e()->to_var().var() == h_var) {
if (tp.pow() >= h->get_child_pow(k)) {
p_swallowed = true;
}
}
@ -345,8 +322,7 @@ bool grobner::divide_ignore_coeffs_check_only_nex_mul(nex_mul* t , const nex* h)
}
}
TRACE("grobner", tout << "division " << *t << " / " << *h << "\n";);
return true;
return true;
}
// return true if h divides t
@ -358,7 +334,7 @@ bool grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
const nex_var * v = to_var(n);
if (h->is_var()) {
return v->var() == to_var(h)->var();
return v->var() == h->to_var().var();
}
if (h->is_mul() || h->is_var()) {
@ -367,7 +343,7 @@ bool grobner::divide_ignore_coeffs_check_only(nex* n , const nex* h) const {
if (h->get_child_pow(0) != 1)
return false;
const nex* e = h->get_child_exp(0);
return e->is_var() && to_var(e)->var() == v->var();
return e->is_var() && e->to_var().var() == v->var();
}
return false;
@ -380,12 +356,13 @@ nex_mul * grobner::divide_ignore_coeffs_perform_nex_mul(nex_mul* t, const nex* h
lpvar h_var = to_var(h->get_child_exp(k))->var();
for (; j < t->size(); j++) {
auto &tp = (*t)[j];
if (to_var(tp.e())->var() == h_var) {
int h_pow = h->get_child_pow(k);
if (tp.e()->to_var().var() == h_var) {
unsigned h_pow = h->get_child_pow(k);
SASSERT(tp.pow() >= h_pow);
j++;
if (tp.pow() > h_pow)
if (tp.pow() > h_pow) {
r->add_child_in_power(tp.e(), tp.pow() - h_pow);
}
break;
} else {
r->add_child_in_power(tp);
@ -429,7 +406,7 @@ void grobner::simplify_target_monomials_sum_j(equation * source, equation *targe
// return true iff simplified
bool 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 << "\nusing: "; display_equation(tout, *source););
TRACE("grobner_d", tout << "simplifying: " << *(target->expr()) << " using " << *(source->expr()) << "\n";);
SASSERT(m_nex_creator.is_simplified(*source->expr()));
SASSERT(m_nex_creator.is_simplified(*target->expr()));
@ -445,15 +422,15 @@ bool grobner::simplify_source_target(equation * source, equation * target) {
bool result = false;
do {
if (simplify_target_monomials(source, target)) {
TRACE("grobner", tout << "simplified target = ";display_equation(tout, *target) << "\n";);
TRACE("grobner", tout << "simplified target = "; display_equation(tout, *target) << "\n";);
result = true;
} else {
break;
}
} while (!canceled());
TRACE("grobner", tout << "result: " << result << "\n"; if (result) display_equation(tout, *target););
if (result) {
target->dep() = m_dep_manager.mk_join(target->dep(), source->dep());
TRACE("grobner", tout << "simplified "; display_equation(tout, *target) << "\n";);
TRACE("grobner_d", tout << "simplified to " << *(target->expr()) << "\n";);
return true;
}
@ -471,7 +448,7 @@ void grobner::process_simplified_target(equation* target, ptr_buffer<equation>&
}
void grobner::check_eq(equation* target) {
if(m_intervals->check_nex(target->expr(), target->dep())) {
if (m_intervals->check_nex(target->expr(), target->dep())) {
TRACE("grobner", tout << "created a lemma for "; display_equation(tout, *target) << "\n";
tout << "vars = \n";
for (lpvar j : get_vars_of_expr(target->expr())) {
@ -488,19 +465,20 @@ bool grobner::simplify_to_superpose_with_eq(equation* eq) {
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
equation_set::iterator it = m_to_superpose.begin();
equation_set::iterator end = m_to_superpose.end();
for (; it != end && !canceled() && !done(); ++it) {
equation * target = *it;
for (equation * target : m_to_superpose) {
if (canceled() || done())
break;
m_changed_leading_term = false;
// if the leading term is simplified, then the equation has to be moved to m_to_simplify
if (simplify_source_target(eq, target)) {
process_simplified_target(target, to_remove);
}
if (is_trivial(target))
if (is_trivial(target)) {
to_delete.push_back(target);
else
}
else {
SASSERT(m_nex_creator.is_simplified(*target->expr()));
}
}
for (equation* eq : to_insert)
insert_to_superpose(eq);
@ -553,17 +531,16 @@ nex * grobner::expr_superpose(nex* e1, nex* e2, const nex* ab, const nex* ac, ne
add_mul_skip_first(r, beta, e1, c);
nex * ret = m_nex_creator.simplify(r);
TRACE("grobner", tout << "e1 = " << *e1 << "\ne2 = " << *e2 <<"\nsuperpose = " << *ret << "\n";);
if (ret->is_scalar()) {
TRACE("grobner",);
}
CTRACE("grobner", ret->is_scalar(), tout << "\n";);
return ret;
}
// let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
void grobner::superpose(equation * eq1, equation * eq2) {
TRACE("grobner", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););
const nex * ab = get_highest_monomial(eq1->expr());
const nex * ac = get_highest_monomial(eq2->expr());
nex_mul *b, *c;
nex_mul *b = nullptr, *c = nullptr;
TRACE("grobner", tout << "ab="; if(ab) { tout << *ab; } else { tout << "null"; };
tout << " , " << " ac="; if(ac) { tout << *ac; } else { tout << "null"; }; tout << "\n";);
if (!find_b_c(ab, ac, b, c)) {
@ -578,7 +555,6 @@ void grobner::superpose(equation * eq1, equation * eq2) {
} else {
insert_to_simplify(eq);
}
}
void grobner::register_report() {
@ -618,8 +594,7 @@ bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) {
break;
}
}
}
}
while (i != ab_size) {
b->add_child_in_power(const_cast<nex*>(ab->get_child_exp(i)), ab->get_child_pow(i));
i++;
@ -631,6 +606,7 @@ bool grobner::find_b_c(const nex* ab, const nex* ac, nex_mul*& b, nex_mul*& c) {
TRACE("nla_grobner", tout << "b=" << *b << ", c=" <<*c << "\n";);
return true;
}
// Finds out if ab and bc have a non-trivial common divider
bool grobner::find_b_c_check_only(const nex* ab, const nex* ac) const {
if (ab == nullptr || ac == nullptr)
@ -658,7 +634,6 @@ bool grobner::find_b_c_check_only(const nex* ab, const nex* ac) const {
return false;
}
void grobner::superpose(equation * eq) {
for (equation * target : m_to_superpose) {
superpose(eq, target);
@ -716,28 +691,14 @@ bool grobner::canceled() const {
return c().lp_settings().get_cancel_flag();
}
bool grobner::done() const {
if (
num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()
||
canceled()
||
m_reported > 0
) {
TRACE("grobner",
tout << "done() is true because of ";
if (num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()) {
tout << "m_num_of_equations = " << num_of_equations() << "\n";
} else if (canceled()) {
tout << "canceled\n";
} else if (m_reported > 0) {
tout << "m_reported = " << m_reported;
}
tout << "\n";);
return true;
}
return false;
CTRACE("grobner", (num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold()),
tout << "m_num_of_equations = " << num_of_equations() << "\n";);
CTRACE("grobner", canceled(), tout << "canceled\n";);
CTRACE("grobner", m_reported > 0, tout << "m_reported = " << m_reported;);
return
num_of_equations() >= c().m_nla_settings.grobner_eqs_threshold() ||
canceled() || m_reported > 0;
}
bool grobner::compute_basis_loop(){
@ -765,7 +726,6 @@ void grobner::update_statistics(){
m_stats.m_gb_compute_basis++;*/
}
bool grobner::push_calculation_forward(ptr_vector<equation>& eqs, unsigned & next_weight) {
return (!m_nl_gb_exhausted) &&
try_to_modify_eqs(eqs, next_weight);
@ -801,6 +761,7 @@ std::ostream& grobner::display_equation(std::ostream & out, const equation & eq)
display_dependency(out, eq.dep());
return out;
}
std::unordered_set<lpvar> grobner::get_vars_of_expr_with_opening_terms(const nex *e ) {
auto ret = get_vars_of_expr(e);
auto & ls = c().m_lar_solver;
@ -840,10 +801,9 @@ void grobner::assert_eq_0(nex* e, ci_dependency * dep) {
}
void grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
unsigned bidx = m_equations_to_delete.size();
eq->m_bidx = bidx;
eq->m_bidx = m_equations_to_delete.size();
eq->dep() = dep;
eq->expr() = e;
eq->expr() = e;
m_equations_to_delete.push_back(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
}
@ -854,18 +814,15 @@ grobner::~grobner() {
std::ostream& grobner::display_dependency(std::ostream& out, ci_dependency* dep) const {
svector<lp::constraint_index> expl;
m_dep_manager.linearize(dep, expl);
{
lp::explanation e(expl);
if (!expl.empty()) {
out << "constraints\n";
m_core->print_explanation(e, out);
out << "\n";
} else {
out << "no deps\n";
}
}
m_dep_manager.linearize(dep, expl);
lp::explanation e(expl);
if (!expl.empty()) {
out << "constraints\n";
m_core->print_explanation(e, out);
out << "\n";
} else {
out << "no deps\n";
}
return out;
}

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

@ -261,17 +261,14 @@ std::ostream & intervals::print_dependencies(ci_dependency* deps , std::ostream&
// 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 << "n = " << *n << "\n";);
m_core->lp_settings().stats().m_cross_nested_forms++;
auto i = interval_of_expr(n, 1);
TRACE("nla_grobner", tout << "callback n = " << *n << "\ni="; display(tout, i) << "\n";);
if (!separated_from_zero(i)) {
reset();
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, initial deps\n"; print_dependencies(initial_deps, tout););
TRACE("grobner", tout << "conflict: interv_wd = "; display(tout, interv_wd ) <<"expr = " << *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;

2
src/smt/smt_context_pp.cpp
View file

@ -496,6 +496,8 @@ namespace smt {
);
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close();
if (m_lemma_id == 1444)
exit(0);
return m_lemma_id;
}