mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 03:16:17 +00:00
Code Activity

reverse the order of vars for pdd_grobner, use pdd_grobner.reset()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-28 15:58:02 -08:00
parent b5364b787c
commit 407c8a60db
3 changed files with 87 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -259,7 +259,6 @@ namespace dd {
void reset(unsigned_vector const& level2var); void reset(unsigned_vector const& level2var);
void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; } void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; }
unsigned_vector const& get_level2var() const { return m_level2var; } unsigned_vector const& get_level2var() const { return m_level2var; }
unsigned_vector& get_level2var() { return m_level2var; }
pdd mk_var(unsigned i); pdd mk_var(unsigned i);
pdd mk_val(rational const& r); pdd mk_val(rational const& r);

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

@ -1596,17 +1596,20 @@ void core::set_active_vars_weights(nex_creator& nc) {
void core::set_level2var_for_pdd_grobner() { void core::set_level2var_for_pdd_grobner() {
unsigned n = m_pdd_manager.get_level2var().size(); unsigned n = m_pdd_manager.get_level2var().size();
unsigned_vector level2var(n); unsigned_vector sorted_vars(n);
for (unsigned j = 0; j < n; j++) for (unsigned j = 0; j < n; j++)
level2var[j] = j; sorted_vars[j] = j;
// sort that the larger weights are in beginning // sort that the larger weights are in beginning
std::sort(level2var.begin(), level2var.end(), [this](unsigned a, unsigned b) { std::sort(sorted_vars.begin(), sorted_vars.end(), [this](unsigned a, unsigned b) {
unsigned wa = get_var_weight(a); unsigned wa = get_var_weight(a);
unsigned wb = get_var_weight(b); unsigned wb = get_var_weight(b);
return wa > wb || (wa == wb && a > b); }); return wa < wb || (wa == wb && a < b); });
unsigned_vector& l2v = m_pdd_manager.get_level2var();
unsigned_vector l2v(n);
for (unsigned j = 0; j < n; j++) for (unsigned j = 0; j < n; j++)
l2v[j] = level2var[j]; l2v[j] = sorted_vars[j];
m_pdd_manager.reset(l2v);
} }
unsigned core::get_var_weight(lpvar j) const { unsigned core::get_var_weight(lpvar j) const {

48
src/test/pdd.cpp
View file

@ -1,9 +1,7 @@
#include "math/dd/dd_pdd.h" #include "math/dd/dd_pdd.h"
#include "math/dd/pdd_eval.h"
#include "math/dd/pdd_interval.h"
namespace dd { namespace dd {
static void test1() { static void test1() {
pdd_manager m(3); pdd_manager m(3);
pdd v0 = m.mk_var(0); pdd v0 = m.mk_var(0);
pdd v1 = m.mk_var(1); pdd v1 = m.mk_var(1);
@ -48,9 +46,9 @@ static void test1() {
c2 = (v0*v1*(v2 + v0)) + v2; c2 = (v0*v1*(v2 + v0)) + v2;
c3 = c2.reduce(c1); c3 = c2.reduce(c1);
std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n"; std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n";
} }
static void test2() { static void test2() {
std::cout << "\ntest2\n"; std::cout << "\ntest2\n";
// a(b^2)cd + abc + bcd + bc + cd + 3 reduce by bc // a(b^2)cd + abc + bcd + bc + cd + 3 reduce by bc
pdd_manager m(4); pdd_manager m(4);
@ -67,23 +65,7 @@ static void test2() {
pdd r_fe = m.reduce(f, e); pdd r_fe = m.reduce(f, e);
std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ; std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ;
VERIFY(r_fe == f); VERIFY(r_fe == f);
}
static void test3() {
std::cout << "\ntest3\n";
pdd_manager m(4);
pdd a = m.mk_var(0);
pdd b = m.mk_var(1);
pdd c = m.mk_var(2);
pdd d = m.mk_var(3);
pdd e = a + c;
for (unsigned i = 0; i < 5; i++) {
e = e * e;
} }
e = e * b;
// std::cout << e << "\n";
}
static void test_reset() { static void test_reset() {
std::cout << "\ntest reset\n"; std::cout << "\ntest reset\n";
@ -128,19 +110,25 @@ static void test5() {
SASSERT(e == f); SASSERT(e == f);
} }
static void test6() { static void test_reset() {
std::cout << "\ntest6\n"; std::cout << "\ntest reset\n";
pdd_manager m(5); pdd_manager m(4);
pdd a = m.mk_var(0); pdd a = m.mk_var(0);
pdd b = m.mk_var(1); pdd b = m.mk_var(1);
pdd c = m.mk_var(2); pdd c = m.mk_var(2);
pdd d = m.mk_var(3); pdd d = m.mk_var(3);
pdd e = a * b * b * d + 2*a*b*c + (b*c*d) + (b*c) + (c*d) + 3; std::cout << (a + b)*(c + d) << "\n";
pdd f = a * d * c + a + d;
pdd l = m.zero(); unsigned_vector l2v;
VERIFY(m.try_spoly(e, f, l)); for (unsigned i = 0; i < 4; ++i)
std::cout << "superpose\n" << e << "\nand\n" << f << "\nresult\n" << l << "\n"; l2v.push_back(3 - i);
} m.reset(l2v);
a = m.mk_var(0);
b = m.mk_var(1);
c = m.mk_var(2);
d = m.mk_var(3);
std::cout << (a + b)*(c + d) << "\n";
}
void test_iterator() { void test_iterator() {
std::cout << "test iterator\n"; std::cout << "test iterator\n";