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

add sort stumps for expressions

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-24 17:13:53 -07:00
parent 27a27f16ff
commit 705607fba0
8 changed files with 195 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/math/lp/cross_nested.h
View file

@ -26,15 +26,17 @@ namespace nla {
class cross_nested {
// fields
nex * m_e;
std::function<bool (const nex*)> m_call_on_result;
std::function<bool (unsigned)> m_var_is_fixed;
std::function<unsigned ()> m_random;
bool m_done;
ptr_vector<nex> m_b_split_vec;
int m_reported;
bool m_random_bit;
nex_creator m_nex_creator;
nex * m_e;
std::function<bool (const nex*)> m_call_on_result;
std::function<bool (unsigned)> m_var_is_fixed;
std::function<unsigned ()> m_random;
bool m_done;
ptr_vector<nex> m_b_split_vec;
int m_reported;
bool m_random_bit;
nex_creator m_nex_creator;
std::function<bool (const nex*, const nex*)> m_lt;
#ifdef Z3DEBUG
nex* m_e_clone;
#endif
@ -44,13 +46,14 @@ public:
cross_nested(std::function<bool (const nex*)> call_on_result,
std::function<bool (unsigned)> var_is_fixed,
std::function<unsigned ()> random):
std::function<unsigned ()> random,
std::function<bool (const nex*, const nex*)> lt):
m_call_on_result(call_on_result),
m_var_is_fixed(var_is_fixed),
m_random(random),
m_done(false),
m_reported(0)
{}
m_reported(0),
m_nex_creator(lt) {}
void run(nex *e) {
@ -124,7 +127,7 @@ public:
}
nex* c_over_f = m_nex_creator.mk_div(*c, f);
to_sum(c_over_f)->simplify(&c_over_f);
to_sum(c_over_f)->simplify(&c_over_f, m_lt);
nex_mul* cm;
*c = cm = m_nex_creator.mk_mul(f, c_over_f);
TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";);
@ -389,7 +392,7 @@ public:
TRACE("nla_cn_details", tout << "a = " << *a << "\n";);
SASSERT(a->children().size() >= 2 && m_b_split_vec.size());
nex* f;
a->simplify(&f);
a->simplify(&f, m_lt);
if (m_b_split_vec.size() == 1) {
b = m_b_split_vec[0];
@ -518,7 +521,7 @@ public:
a->children()[j] = normalize(a->children()[j]);
}
nex *r;
a->simplify(&r);
a->simplify(&r, m_lt);
return r;
}

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

@ -92,7 +92,9 @@ bool horner::lemmas_on_row(const T& row) {
cross_nested cn(
[this](const nex* n) { return check_cross_nested_expr(n); },
[this](unsigned j) { return c().var_is_fixed(j); },
[this]() { return c().random(); }
[this]() { return c().random(); },
[](const nex* a, const nex* b) { return
less_than_nex(a, b, [](lpvar j, lpvar k) { return j < k;}); }
);
SASSERT (row_is_interesting(row));

98
src/math/lp/nex.cpp Normal file
View file

@ -0,0 +1,98 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
--*/
#include "math/lp/nex.h"
namespace nla {
bool ignored_child(nex* e, expr_type t) {
switch(t) {
case expr_type::MUL:
return e->is_scalar() && to_scalar(e)->value().is_one();
case expr_type::SUM:
return e->is_scalar() && to_scalar(e)->value().is_zero();
default: return false;
}
return false;
}
void promote_children_of_sum(ptr_vector<nex> & children,std::function<bool (const nex*, const nex*)> lt ) {
ptr_vector<nex> to_promote;
int skipped = 0;
for(unsigned j = 0; j < children.size(); j++) {
nex** e = &(children[j]);
(*e)->simplify(e, lt);
if ((*e)->is_sum()) {
to_promote.push_back(*e);
} else if (ignored_child(*e, expr_type::SUM)) {
skipped ++;
continue;
} else {
unsigned offset = to_promote.size() + skipped;
if (offset) {
children[j - offset] = *e;
}
}
}
children.shrink(children.size() - to_promote.size() - skipped);
for (nex *e : to_promote) {
for (nex *ee : *(to_sum(e)->children_ptr())) {
if (!ignored_child(ee, expr_type::SUM))
children.push_back(ee);
}
}
}
void promote_children_of_mul(vector<nex_pow> & children, std::function<bool (const nex*, const nex*)> lt) {
TRACE("nla_cn_details", print_vector(children, tout););
vector<nex_pow> to_promote;
int skipped = 0;
for(unsigned j = 0; j < children.size(); j++) {
nex_pow& p = children[j];
(p.e())->simplify(p.ee(), lt);
if ((p.e())->is_mul()) {
to_promote.push_back(p);
} else if (ignored_child(p.e(), expr_type::MUL)) {
skipped ++;
continue;
} else {
unsigned offset = to_promote.size() + skipped;
if (offset) {
children[j - offset] = p;
}
}
}
children.shrink(children.size() - to_promote.size() - skipped);
for (nex_pow & p : to_promote) {
for (nex_pow& pp : to_mul(p.e())->children()) {
SASSERT(!ignored_child(pp.e(), expr_type::MUL));
children.push_back(nex_pow(pp.e(), pp.pow() * p.pow()));
}
}
TRACE("nla_cn_details", print_vector(children, tout););
}
}

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

@ -19,6 +19,7 @@
#pragma once
#include <initializer_list>
#include "math/lp/nla_defs.h"
#include <functional>
namespace nla {
enum class expr_type { VAR, SUM, MUL, SCALAR, UNDEF };
inline std::ostream & operator<<(std::ostream& out, expr_type t) {
@ -42,6 +43,8 @@ inline std::ostream & operator<<(std::ostream& out, expr_type t) {
return out;
}
class nex;
bool less_than_nex_standard(const nex* a, const nex* b);
// This is the class of non-linear expressions
class nex {
@ -68,7 +71,9 @@ public:
virtual ~nex() {}
virtual bool contains(lpvar j) const { return false; }
virtual int get_degree() const = 0;
virtual void simplify(nex** ) = 0;
// simplifies the expression and also assigns the address of "this" to *e
virtual void simplify(nex** e, std::function<bool (const nex*, const nex*)> lt) { *e = this; }
void simplify(nex** e) { return simplify(e, less_than_nex_standard); }
virtual bool is_simplified() const {
return true;
}
@ -100,7 +105,6 @@ public:
bool contains(lpvar j) const { return j == m_j; }
int get_degree() const { return 1; }
virtual void simplify(nex** e) { *e = this; }
bool virtual is_linear() const { return true; }
};
@ -118,7 +122,6 @@ public:
}
int get_degree() const { return 0; }
virtual void simplify(nex** e) { *e = this; }
bool is_linear() const { return true; }
};
@ -126,20 +129,10 @@ public:
const nex_scalar * to_scalar(const nex* a);
class nex_sum;
const nex_sum* to_sum(const nex*a);
static bool ignored_child(nex* e, expr_type t) {
switch(t) {
case expr_type::MUL:
return e->is_scalar() && to_scalar(e)->value().is_one();
case expr_type::SUM:
return e->is_scalar() && to_scalar(e)->value().is_zero();
default: return false;
}
return false;
}
void promote_children_of_sum(ptr_vector<nex> & children);
void promote_children_of_sum(ptr_vector<nex> & children, std::function<bool (const nex*, const nex*)>);
class nex_pow;
void promote_children_of_mul(vector<nex_pow> & children);
void promote_children_of_mul(vector<nex_pow> & children, std::function<bool (const nex*, const nex*)> lt);
class nex_pow {
nex* m_e;
@ -202,6 +195,7 @@ public:
}
void get_powers_from_mul(std::unordered_map<lpvar, unsigned> & r) const {
TRACE("nla_cn_details", tout << "powers of " << *this << "\n";);
r.clear();
for (const auto & c : children()) {
if (!c.e()->is_var()) {
@ -221,13 +215,13 @@ public:
}
return degree;
}
void simplify(nex **e) {
// the second argument is the comparison less than operator
void simplify(nex **e, std::function<bool (const nex*, const nex*)> lt) {
TRACE("nla_cn_details", tout << *this << "\n";);
TRACE("nla_cn_details", tout << "**e = " << **e << "\n";);
*e = this;
TRACE("nla_cn_details", tout << *this << "\n";);
promote_children_of_mul(m_children);
promote_children_of_mul(m_children, lt);
if (size() == 1 && m_children[0].pow() == 1)
*e = m_children[0].e();
TRACE("nla_cn_details", tout << *this << "\n";);
@ -326,12 +320,13 @@ public:
return out;
}
void simplify(nex **e) {
void simplify(nex **e, std::function<bool (const nex*, const nex*)> lt ) {
*e = this;
promote_children_of_sum(m_children);
promote_children_of_sum(m_children, lt);
if (size() == 1)
*e = m_children[0];
}
virtual bool is_simplified() const {
if (size() < 2) return false;
for (nex * e : children()) {
@ -402,6 +397,16 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) {
return e.print(out);
}
inline bool less_than_nex(const nex* a, const nex* b, std::function<bool (lpvar, lpvar)> lt) {
NOT_IMPLEMENTED_YET();
return false;
}
inline bool less_than_nex_standard(const nex* a, const nex* b) {
return less_than_nex(a, b, [](lpvar j, lpvar k) { return j < k; });
}
#if Z3DEBUG
inline bool operator<(const ptr_vector<nex>&a , const ptr_vector<nex>& b) {
@ -420,5 +425,6 @@ inline bool operator<(const ptr_vector<nex>&a , const ptr_vector<nex>& b) {
}
#endif
}

9
src/math/lp/nex_creator.h
View file

@ -38,10 +38,13 @@ struct occ {
class nex_creator {
ptr_vector<nex> m_allocated;
std::unordered_map<lpvar, occ> m_occurences_map;
std::unordered_map<lpvar, unsigned> m_powers;
ptr_vector<nex> m_allocated;
std::unordered_map<lpvar, occ> m_occurences_map;
std::unordered_map<lpvar, unsigned> m_powers;
// the "less than" operator on expressions
std::function<bool (const nex*, const nex*)> m_lt;
public:
nex_creator(std::function<bool (const nex*, const nex*)> lt) {}
const std::unordered_map<lpvar, occ>& occurences_map() const { return m_occurences_map; }
std::unordered_map<lpvar, occ>& occurences_map() { return m_occurences_map; }
const std::unordered_map<lpvar, unsigned> & powers() const { return m_powers; }

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

@ -21,7 +21,13 @@
#include "math/lp/nla_core.h"
#include "math/lp/factorization_factory_imp.h"
namespace nla {
nla_grobner::nla_grobner(core *c) : common(c), m_nl_gb_exhausted(false), m_dep_manager(m_val_manager, m_alloc) {}
nla_grobner::nla_grobner(core *c
) :
common(c),
m_nl_gb_exhausted(false),
m_dep_manager(m_val_manager, m_alloc),
m_nex_creator([this](const nex* a, const nex* b) { return
this->less_than_on_expr(a, b); }) {}
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
// then assert bounds for x, and continue

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

@ -37,7 +37,7 @@ struct grobner_stats {
};
enum class var_weight {
FIXED = 0,
FIXED = 0,
QUOTED_FIXED = 1,
BOUNDED = 2,
QUOTED_BOUNDED = 3,
@ -86,22 +86,23 @@ class nla_grobner : common {
typedef ptr_vector<equation> equation_vector;
// fields
equation_vector m_equations_to_unfreeze;
equation_vector m_equations_to_delete;
lp::int_set m_rows;
lp::int_set m_active_vars;
svector<var_weight> m_active_vars_weights;
unsigned m_num_of_equations;
grobner_stats m_stats;
equation_set m_processed;
equation_set m_to_process;
bool m_nl_gb_exhausted;
ptr_vector<nex> m_allocated;
lp::int_set m_tmp_var_set;
region m_alloc;
ci_value_manager m_val_manager;
ci_dependency_manager m_dep_manager;
nex_creator m_nex_creator;
equation_vector m_equations_to_unfreeze;
equation_vector m_equations_to_delete;
lp::int_set m_rows;
lp::int_set m_active_vars;
svector<var_weight> m_active_vars_weights;
unsigned m_num_of_equations;
grobner_stats m_stats;
equation_set m_processed;
equation_set m_to_process;
bool m_nl_gb_exhausted;
ptr_vector<nex> m_allocated;
lp::int_set m_tmp_var_set;
region m_alloc;
ci_value_manager m_val_manager;
ci_dependency_manager m_dep_manager;
nex_creator m_nex_creator;
std::function<bool (const nex*, const nex*)> m_lt;
public:
nla_grobner(core *core);
void grobner_lemmas();
@ -156,5 +157,22 @@ private:
return static_cast<const nex_scalar*>(a)->value();
return rational(1);
}
bool less_than_on_vars(lpvar a, lpvar b) const {
const auto &aw = m_active_vars_weights[a];
const auto &ab = m_active_vars_weights[b];
if (aw < ab)
return true;
if (aw > ab)
return false;
// aw == ab
return a < b;
}
bool less_than_on_expr(const nex* a, const nex* b) const {
return less_than_nex(a, b, [this](lpvar j, lpvar k) {return less_than_on_vars(j, k);});
}
}; // end of grobner
}

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

@ -96,7 +96,8 @@ void test_cn() {
return false;
} ,
[](unsigned) { return false; },
[]{ return 1; }
[]{ return 1; },
less_than_nex_standard
);
enable_trace("nla_cn");
enable_trace("nla_cn_details");