mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

remove an unused test file

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-03 15:34:00 -07:00
parent 006c53e484
commit d08d381115
1 changed files with 0 additions and 36 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/test/emonomials.cpp
View file

@ -1,36 +0,0 @@
#include "util/lp/emonomials.h"
static void display_mons(nla::emonomials const& em) {
std::cout << em << "\n";
for (auto const& m1 : em) {
std::cout << "factors: " << m1 << ": \n";
for (auto const& m2 : em.get_factors_of(m1)) {
std::cout << m2 << "\n";
}
}
}
void tst_emonomials() {
nla::var_eqs ve;
nla::emonomials em(ve);
unsigned x = 1;
unsigned y = 2;
unsigned z = 3;
unsigned u = 4;
unsigned v1 = 5;
unsigned v2 = 6;
unsigned v3 = 7;
em.add(v1, x, x);
em.add(v2, x, z);
em.add(v3, x, y, x);
display_mons(em);
em.push();
ve.merge_plus(x, y, nla::eq_justification({}));
display_mons(em);
em.push();
ve.merge_plus(x, z, nla::eq_justification({}));
display_mons(em);
em.pop(1);
display_mons(em);
}