mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-12-30 16:10:11 -08:00
parent 523578e3f6
commit 5da71dc847
1 changed files with 15 additions and 16 deletions

31
src/test/egraph.cpp
View file

@ -37,10 +37,10 @@ static void test1() {
expr_ref fa = mk_app("f", a, S);
expr_ref ffa = mk_app("f", fa, S);
expr_ref fffa = mk_app("f", ffa, S);
euf::enode* na = g.mk(a, 0, nullptr);
euf::enode* nfa = g.mk(fa, 1, &na);
euf::enode* nffa = g.mk(ffa, 1, &nfa);
euf::enode* nfffa = g.mk(fffa, 1, &nffa);
euf::enode* na = g.mk(a, 0, 0, nullptr);
euf::enode* nfa = g.mk(fa, 0, 1, &na);
euf::enode* nffa = g.mk(ffa, 0, 1, &nfa);
euf::enode* nfffa = g.mk(fffa, 0, 1, &nffa);
std::cout << g << "\n";
g.merge(na, nffa, nullptr);
g.merge(na, nfffa, nullptr);
@ -61,13 +61,13 @@ static void test2() {
std::string xn("x");
xn += std::to_string(i);
expr_ref x = mk_const(m, xn.c_str(), S);
euf::enode* n = g.mk(x, 0, nullptr);
euf::enode* n = g.mk(x, 0, 0, nullptr);
nodes.push_back(n);
for (unsigned j = 0; j < d; ++j) {
std::string f("f");
f += std::to_string(j);
x = mk_app(f.c_str(), x, S);
n = g.mk(x, 1, &n);
n = g.mk(x, 0, 1, &n);
}
top_nodes.push_back(n);
pinned.push_back(x);
@ -101,14 +101,14 @@ static void test3() {
expr_ref u = mk_const(m, "u", I);
expr_ref fx = mk_app("f", x, I);
expr_ref fy = mk_app("f", y, I);
euf::enode* nx = g.mk(x, 0, nullptr);
euf::enode* ny = g.mk(y, 0, nullptr);
euf::enode* nz = g.mk(z, 0, nullptr);
euf::enode* nu = g.mk(u, 0, nullptr);
euf::enode* n0 = g.mk(zero, 0, nullptr);
euf::enode* n1 = g.mk(one, 0, nullptr);
euf::enode* nfx = g.mk(fx, 1, &nx);
euf::enode* nfy = g.mk(fy, 1, &ny);
euf::enode* nx = g.mk(x, 0, 0, nullptr);
euf::enode* ny = g.mk(y, 0, 0, nullptr);
euf::enode* nz = g.mk(z, 0, 0, nullptr);
euf::enode* nu = g.mk(u, 0, 0, nullptr);
euf::enode* n0 = g.mk(zero, 0, 0, nullptr);
euf::enode* n1 = g.mk(one, 0, 0, nullptr);
euf::enode* nfx = g.mk(fx, 0, 1, &nx);
euf::enode* nfy = g.mk(fy, 0, 1, &ny);
int justifications[5] = { 1, 2, 3, 4, 5 };
g.merge(nfx, n0, justifications + 0);
g.merge(nfy, n1, justifications + 1);
@ -125,9 +125,8 @@ static void test3() {
g.begin_explain();
g.explain<int>(js);
g.end_explain();
for (int* j : js) {
for (int* j : js)
std::cout << "conflict: " << *j << "\n";
}
}
void tst_egraph() {