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

Nikolaj implemented lm_lt on dd::pdd

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-09 09:57:19 -08:00
parent d1e9998332
commit d6a246777a
5 changed files with 224 additions and 92 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
src/math/dd/dd_pdd.cpp
View file

@ -495,12 +495,9 @@ namespace dd {
}
/*.
* The pdd format makes lexicographic comparison easy: compare based on
* the top variable and descend depending on whether hi(x) == hi(y)
*
* NB. this does not compare leading monomials.
* compare pdds based on leading monomials
*/
bool pdd_manager::lt(pdd const& a, pdd const& b) {
bool pdd_manager::lex_lt(pdd const& a, pdd const& b) {
PDD x = a.root;
PDD y = b.root;
if (x == y) return false;
@ -526,6 +523,48 @@ namespace dd {
}
}
bool pdd_manager::lm_lt(pdd const& a, pdd const& b) {
PDD x = first_leading(a.root);
PDD y = first_leading(b.root);
while (true) {
if (x == y) break;
if (is_val(x) && is_val(y)) break;
if (is_val(x)) return true;
if (is_val(y)) return false;
if (level(x) == level(y)) {
x = next_leading(x);
y = next_leading(y);
}
else {
return level(x) < level(y);
}
}
vector<unsigned_vector> ma, mb;
for (auto const& m : a) {
ma.push_back(m.vars);
}
for (auto const& m : b) {
mb.push_back(m.vars);
}
std::function<bool (unsigned_vector const& a, unsigned_vector const& b)> degree_lex_gt =
[this](unsigned_vector const& a, unsigned_vector const& b) {
unsigned i = 0;
if (a.size() > b.size()) return true;
if (a.size() < b.size()) return false;
for (; i < a.size() && a[i] == b[i]; ++i) {};
return i < a.size() && m_var2level[a[i]] > m_var2level[b[i]];
};
std::sort(ma.begin(), ma.end(), degree_lex_gt);
std::sort(mb.begin(), mb.end(), degree_lex_gt);
auto ita = ma.begin();
auto itb = mb.begin();
for (; ita != ma.end() && itb != mb.end(); ++ita, ++itb) {
if (degree_lex_gt(*itb, *ita)) return true;
if (degree_lex_gt(*ita, *itb)) return false;
}
return ita == ma.end() && itb != mb.end();
}
/**
Compare leading terms of pdds
*/

10
src/math/dd/dd_pdd.h
View file

@ -290,7 +290,12 @@ namespace dd {
// create an spoly r if leading monomials of a and b overlap
bool try_spoly(pdd const& a, pdd const& b, pdd& r);
bool lt(pdd const& a, pdd const& b);
// simple lexicographic comparison
bool lex_lt(pdd const& a, pdd const& b);
// more elaborate comparison based on leading monomials
bool lm_lt(pdd const& a, pdd const& b);
bool different_leading_term(pdd const& a, pdd const& b);
double tree_size(pdd const& p);
unsigned num_vars() const { return m_var2pdd.size(); }
@ -352,9 +357,6 @@ namespace dd {
std::ostream& display(std::ostream& out) const { return m.display(out, *this); }
bool operator==(pdd const& other) const { return root == other.root; }
bool operator!=(pdd const& other) const { return root != other.root; }
bool operator<(pdd const& other) const { return m.lt(*this, other); }
unsigned dag_size() const { return m.dag_size(*this); }
double tree_size() const { return m.tree_size(*this); }

8
src/math/grobner/pdd_solver.cpp
View file

@ -70,9 +70,11 @@ namespace dd {
}
// some of the config fields are set, others are calculated
void solver::set_thresholds() {
IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
if (m_to_simplify.size() == 0)
return;
m_config.m_eqs_threshold = static_cast<unsigned>(10 * ceil(log(m_to_simplify.size()))*m_to_simplify.size());
m_config.m_expr_size_limit = 0;
m_config.m_expr_degree_limit = 0;
for (equation* e: m_to_simplify) {
@ -87,9 +89,9 @@ namespace dd {
verbose_stream() << "set m_config.m_expr_degree_limit to " << m_config.m_expr_degree_limit << "\n";
);
m_config.m_max_steps = 700;
m_config.m_max_simplified = 7000;
m_config.m_max_simplified = 7000;
}
void solver::saturate() {
simplify();
init_saturate();

3
src/math/grobner/pdd_solver.h
View file

@ -55,7 +55,6 @@ public:
unsigned m_max_simplified;
unsigned m_random_seed;
bool m_enable_exlin;
unsigned m_eqs_growth;
config() :
m_eqs_threshold(UINT_MAX),
m_expr_size_limit(UINT_MAX),
@ -154,7 +153,7 @@ private:
bool try_simplify_using(equation& target, equation const& source, bool& changed_leading_term);
bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); }
bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); }
bool is_simpler(equation const& eq1, equation const& eq2) { return m.lm_lt(eq1.poly(), eq2.poly()); }
bool is_conflict(equation const* eq) const { return is_conflict(*eq); }
bool is_conflict(equation const& eq) const { return eq.poly().is_val() && !is_trivial(eq); }
bool check_conflict(equation& eq) { return is_conflict(eq) && (set_conflict(eq), true); }

246
src/test/pdd.cpp
View file

@ -143,90 +143,179 @@ void test_iterator() {
class test {
public :
static void order() {
std::cout << "order\n";
pdd_manager m(4);
unsigned va = 0;
unsigned vb = 1;
unsigned vc = 2;
unsigned vd = 3;
pdd a = m.mk_var(va);
pdd b = m.mk_var(vb);
pdd c = m.mk_var(vc);
pdd d = m.mk_var(vd);
pdd p = a + b;
std::cout << p << "\n";
unsigned i = 0;
for (auto const& m : p) {
std::cout << m << "\n";
SASSERT(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
SASSERT(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
i++;
}
pdd ccbbaa = c*c*b*b*a*a;
pdd ccbbba = c*c*b*b*b*a;
p = ccbbaa + ccbbba;
std::cout << "order\n";
pdd_manager m(4);
unsigned va = 0;
unsigned vb = 1;
unsigned vc = 2;
unsigned vd = 3;
pdd a = m.mk_var(va);
pdd b = m.mk_var(vb);
pdd c = m.mk_var(vc);
pdd d = m.mk_var(vd);
pdd p = a + b;
std::cout << p << "\n";
unsigned i = 0;
for (auto const& m : p) {
std::cout << m << "\n";
SASSERT(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
SASSERT(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
i++;
}
pdd ccbbaa = c*c*b*b*a*a;
pdd ccbbba = c*c*b*b*b*a;
p = ccbbaa + ccbbba;
i = 0;
std::cout << "p = " << p << "\n";
for (auto const& m : p) {
std::cout << m << "\n";
SASSERT(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
SASSERT(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
i++;
}
pdd dcbba = d*c*b*b*a;
pdd dd = d * d;
p = dcbba + ccbbba + dd;
vector<unsigned> v;
std::cout << "p = " << p << "\n";
unsigned k = p.index();
std::cout << "pdd(k) = " << pdd(k, m) << "\n";
k = m.first_leading(k);
do {
if (m.is_val(k)) {
SASSERT(m.val(k).is_one());
break;
i = 0;
std::cout << "p = " << p << "\n";
for (auto const& m : p) {
std::cout << m << "\n";
SASSERT(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
SASSERT(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
i++;
}
v.push_back(m.var(k));
pdd dcbba = d*c*b*b*a;
pdd dd = d * d;
p = dcbba + ccbbba + dd;
vector<unsigned> v;
std::cout << "p = " << p << "\n";
unsigned k = p.index();
std::cout << "pdd(k) = " << pdd(k, m) << "\n";
std::cout << "push v" << m.var(k) << "\n";
k = m.next_leading(k);
} while(true);
auto it = v.begin();
std::cout << "v" << *it;
it++;
for( ; it != v.end(); it ++) {
std::cout << "*v" << *it;
}
SASSERT(v.size() == 6);
SASSERT(v[0] == vc);
std::cout << "\n";
v.reset();
p = d*c*c*d + b*c*c*b + d*d*d;
k = p.index();
std::cout << "pdd(k) = " << pdd(k, m) << "\n";
k = m.first_leading(k);
do {
if (m.is_val(k)) {
SASSERT(m.val(k).is_one());
break;
k = m.first_leading(k);
do {
if (m.is_val(k)) {
SASSERT(m.val(k).is_one());
break;
}
v.push_back(m.var(k));
std::cout << "pdd(k) = " << pdd(k, m) << "\n";
std::cout << "push v" << m.var(k) << "\n";
k = m.next_leading(k);
} while(true);
auto it = v.begin();
std::cout << "v" << *it;
it++;
for( ; it != v.end(); it ++) {
std::cout << "*v" << *it;
}
v.push_back(m.var(k));
SASSERT(v.size() == 6);
SASSERT(v[0] == vc);
std::cout << "\n";
v.reset();
p = d*c*c*d + b*c*c*b + d*d*d;
k = p.index();
std::cout << "pdd(k) = " << pdd(k, m) << "\n";
std::cout << "push v" << m.var(k) << "\n";
k = m.next_leading(k);
} while(true);
it = v.begin();
std::cout << "v" << *it;
it++;
for( ; it != v.end(); it ++) {
std::cout << "*v" << *it;
}
SASSERT(v.size() == 4);
SASSERT(v[0] == vd);
std::cout << "\n";
k = m.first_leading(k);
do {
if (m.is_val(k)) {
SASSERT(m.val(k).is_one());
break;
}
v.push_back(m.var(k));
std::cout << "pdd(k) = " << pdd(k, m) << "\n";
std::cout << "push v" << m.var(k) << "\n";
k = m.next_leading(k);
} while(true);
it = v.begin();
std::cout << "v" << *it;
it++;
for( ; it != v.end(); it ++) {
std::cout << "*v" << *it;
}
SASSERT(v.size() == 4);
SASSERT(v[0] == vd);
std::cout << "\n";
}
}
static void order_lm() {
std::cout << "order_lm\n";
pdd_manager m(4);
unsigned va = 0;
unsigned vb = 1;
unsigned vc = 2;
unsigned vd = 3;
pdd a = m.mk_var(va);
pdd b = m.mk_var(vb);
pdd c = m.mk_var(vc);
pdd d = m.mk_var(vd);
pdd p = a + b;
std::cout << p << "\n";
unsigned i = 0;
for (auto const& m : p) {
std::cout << m << "\n";
SASSERT(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
SASSERT(i != 1 ||( m.vars.size() == 1 && m.vars[0] == va));
i++;
}
pdd ccbbaa = c*c*b*b*a*a;
pdd ccbbba = c*c*b*b*b*a;
p = ccbbaa + ccbbba;
i = 0;
std::cout << "p = " << p << "\n";
for (auto const& m : p) {
std::cout << m << "\n";
SASSERT(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
SASSERT(i != 1 ||( m.vars.size() == 6 && m.vars[4] == va)); // the second one has to be ccbbaa
i++;
}
pdd dcbba = d*c*b*b*a;
pdd dd = d * d;
pdd p0 = p + dd;
std::cout << p0 << " > " << p << "\n";
SASSERT(m.lm_lt(p, p0));
SASSERT(m.lm_lt(p0 + a * b, p0 + b * b));
// vector<unsigned> v;
// std::cout << "p = " << p << "\n";
// unsigned k = p.index();
// std::cout << "pdd(k) = " << pdd(k, m) << "\n";
// k = m.first_leading(k);
// do {
// if (m.is_val(k)) {
// SASSERT(m.val(k).is_one());
// break;
// }
// v.push_back(m.var(k));
// std::cout << "pdd(k) = " << pdd(k, m) << "\n";
// std::cout << "push v" << m.var(k) << "\n";
// k = m.next_leading(k);
// } while(true);
// auto it = v.begin();
// std::cout << "v" << *it;
// it++;
// for( ; it != v.end(); it ++) {
// std::cout << "*v" << *it;
// }
// SASSERT(v.size() == 6);
// SASSERT(v[0] == vc);
// std::cout << "\n";
// v.reset();
// p = d*c*c*d + b*c*c*b + d*d*d;
// k = p.index();
// std::cout << "pdd(k) = " << pdd(k, m) << "\n";
// k = m.first_leading(k);
// do {
// if (m.is_val(k)) {
// SASSERT(m.val(k).is_one());
// break;
// }
// v.push_back(m.var(k));
// std::cout << "pdd(k) = " << pdd(k, m) << "\n";
// std::cout << "push v" << m.var(k) << "\n";
// k = m.next_leading(k);
// } while(true);
// it = v.begin();
// std::cout << "v" << *it;
// it++;
// for( ; it != v.end(); it ++) {
// std::cout << "*v" << *it;
// }
// SASSERT(v.size() == 4);
// SASSERT(v[0] == vd);
// std::cout << "\n";
}
};
}
@ -239,4 +328,5 @@ void tst_pdd() {
dd::test_reset();
dd::test_iterator();
dd::test::order();
dd::test::order_lm();
}