mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 14:25:35 +00:00
Code Activity
z3/src/test/pdd.cpp
Nikolaj Bjorner 4a192850f2 add var_factors 
Add routine to partially factor polynomials. It factors out variables.
2022-07-14 11:06:53 -07:00

398 lines
12 KiB
C++
Raw Blame History

#include "math/dd/dd_pdd.h"
#include <iostream>
namespace dd {
class test {
public :
static void hello_world() {
pdd_manager m(3);
pdd v0 = m.mk_var(0);
pdd v1 = m.mk_var(1);
pdd v2 = m.mk_var(2);
std::cout << v0 << "\n";
std::cout << v1 << "\n";
std::cout << v2 << "\n";
pdd c1 = v0 * v1 * v2;
pdd c2 = v2 * v0 * v1;
std::cout << c1 << "\n";
VERIFY(c1 == c2);
c1 = v0 + v1 + v2;
c2 = v2 + v1 + v0;
std::cout << c1 << "\n";
VERIFY(c1 == c2);
c1 = (v0+v1) * v2;
c2 = (v0*v2) + (v1*v2);
std::cout << c1 << "\n";
VERIFY(c1 == c2);
c1 = (c1 + 3) + 1;
c2 = (c2 + 1) + 3;
std::cout << c1 << "\n";
VERIFY(c1 == c2);
c1 = v0 - v1;
c2 = v1 - v0;
std::cout << c1 << " " << c2 << "\n";
c1 = v1*v2;
c2 = (v0*v2) + (v2*v2);
pdd c3 = m.zero();
VERIFY(m.try_spoly(c1, c2, c3));
std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
c1 = v1*v2;
c2 = (v0*v2) + (v1*v1);
VERIFY(m.try_spoly(c1, c2, c3));
std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n";
c1 = (v0*v1) - (v0*v0);
c2 = (v0*v1*(v2 + v0)) + v2;
c3 = c2.reduce(c1);
std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n";
VERIFY(c3 == c3.reduce(c1));
}
static void reduce() {
std::cout << "\nreduce\n";
// a(b^2)cd + abc + bcd + bc + cd + 3 reduce by bc
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 * b * b * c * d) + (2*a*b*c) + (b*c*d) + (b*c) + (c*d) + 3;
std::cout << e << "\n";
pdd f = b * c;
pdd r_ef = m.reduce(e, f);
m.display(std::cout);
std::cout << "result of reduce " << e << " by " << f << " is " << r_ef << "\n";
VERIFY(r_ef == (c*d) + 3);
pdd r_fe = m.reduce(f, e);
std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ;
VERIFY(r_fe == f);
// test that b*c*d is treated as the leading monomial
f = b*c*d - d*d;
r_ef = m.reduce(e, f);
std::cout << "result of reduce " << e << " by " << f << " is " << r_ef << "\n";
VERIFY(r_ef == (a*b*d*d) + (2*a*b*c) + (d*d) + (b*c) + (c*d) + 3);
pdd k = d*d + 3*b;
VERIFY(m.reduce(f, k) == b*c*d + 3*b);
}
static void large_product() {
std::cout << "\nlarge_product\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 reset() {
std::cout << "\ntest reset\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);
std::cout << (a + b)*(c + d) << "\n";
unsigned_vector l2v;
for (unsigned i = 0; i < 4; ++i)
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";
}
static void canonize() {
std::cout << "\ncanonize\n";
pdd_manager m(2);
pdd a = m.mk_var(0);
pdd b = m.mk_var(1);
pdd e = (a - b) * ( a + b);
pdd f = a * a - b * b;
VERIFY(e == f);
e = (a - b)* (a - b);
f = a * a - 2 * a * b + b * b;
VERIFY(e == f);
e = a - 3;
e = e * e;
f = a * a - 6 * a + 9;
VERIFY(e == f);
e = 2 * a - 3;
e = e * e;
f = 4 * a * a - 12 * a + 9;
VERIFY(e == f);
}
static void iterator() {
std::cout << "test iterator\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 p = (a + b)*(c + 3*d) + 2;
std::cout << p << "\n";
for (auto const& m : p) {
std::cout << m << "\n";
}
}
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";
VERIFY(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
VERIFY(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";
VERIFY(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
VERIFY(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)) {
VERIFY(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;
}
VERIFY(v.size() == 6);
VERIFY(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)) {
VERIFY(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;
}
VERIFY(v.size() == 4);
VERIFY(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";
VERIFY(i != 0 ||( m.vars.size() == 1 && m.vars[0] == vb));
VERIFY(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";
VERIFY(i != 0 ||( m.vars.size() == 6 && m.vars[4] == vb)); // the first one has to be ccbbba
VERIFY(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";
VERIFY(m.lm_lt(p, p0));
VERIFY(m.lm_lt(p0 + a * b, p0 + b * b));
}
/**
* Test polynomials mod 2^2
*/
static void mod4_operations() {
std::cout << "operations mod4\n";
pdd_manager m(4, pdd_manager::mod2N_e, 2);
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";
// should be reduced to 0:
p = a*a*(a*a - 1);
std::cout << p << "\n";
vector<std::pair<unsigned, rational>> sub0, sub1, sub2, sub3;
sub0.push_back(std::make_pair(va, rational(0)));
sub1.push_back(std::make_pair(va, rational(1)));
sub2.push_back(std::make_pair(va, rational(2)));
sub3.push_back(std::make_pair(va, rational(3)));
std::cout << "sub 0 " << p.subst_val(sub0) << "\n";
std::cout << "sub 1 " << p.subst_val(sub1) << "\n";
std::cout << "sub 2 " << p.subst_val(sub2) << "\n";
std::cout << "sub 3 " << p.subst_val(sub3) << "\n";
std::cout << "expect 1 " << (2*a + 1).is_non_zero() << "\n";
std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_non_zero() << "\n";
std::cout << "expect 0 " << (2*a + 2).is_non_zero() << "\n";
SASSERT((2*a + 1).is_non_zero());
SASSERT((2*a + 2*b + 1).is_non_zero());
SASSERT(!(2*a*b + 3*b + 2).is_non_zero());
}
static void factors() {
pdd_manager m(3);
pdd v0 = m.mk_var(0);
pdd v1 = m.mk_var(1);
pdd v2 = m.mk_var(2);
pdd v3 = m.mk_var(3);
pdd v4 = m.mk_var(4);
pdd c1 = v0 * v1 * v2 + v2 * v0 + v1 + 1;
{
auto [vars, p] = c1.var_factors();
VERIFY(p == c1 && vars.empty());
}
{
auto q = c1 * v4;
auto [vars, p] = q.var_factors();
std::cout << p << " " << vars << "\n";
VERIFY(p == c1 && vars.size() == 1 && vars[0] == 4);
}
for (unsigned i = 0; i < 5; ++i) {
auto v = m.mk_var(i);
auto q = c1 * v;
std::cout << i << ": " << q << "\n";
auto [vars, p] = q.var_factors();
std::cout << p << " " << vars << "\n";
VERIFY(p == c1 && vars.size() == 1 && vars[0] == i);
}
for (unsigned i = 0; i < 5; ++i) {
for (unsigned j = 0; j < 5; ++j) {
auto vi = m.mk_var(i);
auto vj = m.mk_var(j);
auto q = c1 * vi * vj;
auto [vars, p] = q.var_factors();
std::cout << p << " " << vars << "\n";
VERIFY(p == c1 && vars.size() == 2);
VERIFY(vars[0] == i || vars[1] == i);
VERIFY(vars[0] == j || vars[1] == j);
}
}
for (unsigned i = 0; i < 5; ++i) {
for (unsigned j = i; j < 5; ++j) {
for (unsigned k = j; k < 5; ++k) {
auto vi = m.mk_var(i);
auto vj = m.mk_var(j);
auto vk = m.mk_var(k);
auto q = c1 * vi * vj * vk;
auto [vars, p] = q.var_factors();
std::cout << p << " " << vars << "\n";
VERIFY(p == c1 && vars.size() == 3);
VERIFY(vars[0] == i || vars[1] == i || vars[2] == i);
VERIFY(vars[0] == j || vars[1] == j || vars[2] == j);
VERIFY(vars[0] == k || vars[1] == k || vars[2] == k);
}
}
}
}
};
}
void tst_pdd() {
dd::test::hello_world();
dd::test::reduce();
dd::test::large_product();
dd::test::canonize();
dd::test::reset();
dd::test::iterator();
dd::test::order();
dd::test::order_lm();
dd::test::mod4_operations();
dd::test::factors();
}
View git blame Copy permalink