From ff3baffadc2fae694d15d353fe01e316701b2722 Mon Sep 17 00:00:00 2001
From: Mathias Soeken <mathias.soeken@epfl.ch>
Date: Sun, 1 Mar 2020 12:56:17 +0100
Subject: [PATCH] Testcase for npn3_finder.

---
 src/test/CMakeLists.txt |   1 +
 src/test/finder.cpp     | 195 ++++++++++++++++++++++++++++++++++++++++
 src/test/main.cpp       |   1 +
 3 files changed, 197 insertions(+)
 create mode 100644 src/test/finder.cpp

diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index 725bad258..9f44c6f02 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -43,6 +43,7 @@ add_executable(test-z3
   ext_numeral.cpp
   f2n.cpp
   factor_rewriter.cpp
+  finder.cpp
   fixed_bit_vector.cpp
   for_each_file.cpp
   get_consequences.cpp
diff --git a/src/test/finder.cpp b/src/test/finder.cpp
new file mode 100644
index 000000000..488384fa3
--- /dev/null
+++ b/src/test/finder.cpp
@@ -0,0 +1,195 @@
+#include "sat/sat_solver.h"
+#include "sat/sat_npn3_finder.h"
+
+#include <fstream>
+#include <functional>
+#include <iostream>
+
+static void _init_solver(sat::solver& s)
+{
+    s.mk_var();
+    s.mk_var();
+    s.mk_var();
+    s.mk_var();
+}
+
+static void _mk_clause4(sat::solver& s, sat::literal w, sat::literal x, sat::literal y, sat::literal z)
+{
+    sat::literal lits[] = {w, x, y, z};
+    s.mk_clause(4, lits);
+}
+
+template<class CbFn>
+static void _check_finder(sat::solver& s, CbFn&& fn, const std::string& name, unsigned head_exp, unsigned a_exp, unsigned b_exp, unsigned c_exp)
+{
+    using namespace std::placeholders;
+
+    uint32_t found{0u};
+    sat::npn3_finder f_npn(s);
+    fn(f_npn, [&](sat::literal head, sat::literal a, sat::literal b, sat::literal c) {
+        std::cout << "[" << name << "]\n";
+        ENSURE(head.to_uint() == head_exp && a.to_uint() == a_exp && b.to_uint() == b_exp && c.to_uint() == c_exp);
+        ++found;
+    });
+    sat::clause_vector clauses(s.clauses());
+    f_npn(clauses);
+    ENSURE(found == 1u);
+}
+
+static void tst_single_mux() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    s.mk_clause({ 0, true }, { 1, true }, { 3, false });
+    s.mk_clause({ 0, true }, { 1, false }, { 3, true });
+    s.mk_clause({ 0, false }, { 2, true }, { 3, false });
+    s.mk_clause({ 0, false }, { 2, false }, { 3, true });
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_mux), "mux", 7, 0, 3, 5);
+}
+
+static void tst_single_maj() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    s.mk_clause({ 0, false }, { 1, false }, { 3, true });
+    s.mk_clause({ 0, false }, { 2, false }, { 3, true });
+    s.mk_clause({ 1, false }, { 2, false }, { 3, true });
+    s.mk_clause({ 0, true }, { 1, true }, { 3, false });
+    s.mk_clause({ 0, true }, { 2, true }, { 3, false });
+    s.mk_clause({ 1, true }, { 2, true }, { 3, false });
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_maj), "maj", 6, 0, 2, 4);
+}
+
+static void tst_single_orand() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    s.mk_clause({0, false}, {3, true});
+    s.mk_clause({1, false}, {2, false}, {3, true});
+    s.mk_clause({0, true}, {1, true}, {3, false});
+    s.mk_clause({0, true}, {2, true}, {3, false});
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_orand), "orand", 6, 0, 2, 4);
+}
+
+static void tst_single_and() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    sat::literal ls1[] = {{0, true}, {1, true}, {2, true}, {3, false}};
+    s.mk_clause(4, ls1);
+    s.mk_clause({0, false}, {3, true});
+    s.mk_clause({1, false}, {3, true});
+    s.mk_clause({2, false}, {3, true});
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_and), "and", 6, 0, 2, 4);
+}
+
+static void tst_single_xor() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
+    _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false});
+    _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false});
+    _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true});
+    _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true});
+    _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, true});
+    _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, true});
+    _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xor), "xor", 1, 3, 4, 6);
+}
+
+static void tst_single_andxor() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    s.mk_clause({0, true}, {1, false}, {3, true});
+    s.mk_clause({0, true}, {2, false}, {3, true});
+    _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
+    s.mk_clause({0, false}, {1, false}, {3, false});
+    s.mk_clause({0, false}, {2, false}, {3, false});
+    _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true});
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_andxor), "andxor", 0, 6, 2, 4);
+}
+
+static void tst_single_xorand() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    s.mk_clause({0, false}, {3, true});
+    s.mk_clause({1, false}, {2, false}, {3, true});
+    s.mk_clause({1, true}, {2, true}, {3, true});
+    _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, false});
+    _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, false});
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xorand), "xorand", 6, 0, 3, 5);
+}
+
+static void tst_single_gamble() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    s.mk_clause({0, true}, {1, false}, {3, true});
+    s.mk_clause({1, true}, {2, false}, {3, true});
+    s.mk_clause({0, false}, {2, true}, {3, true});
+    _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, false});
+    _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_gamble), "gamble", 6, 0, 2, 4);
+}
+
+static void tst_single_onehot() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    s.mk_clause({0, true}, {1, true}, {3, true});
+    s.mk_clause({0, true}, {2, true}, {3, true});
+    s.mk_clause({1, true}, {2, true}, {3, true});
+    _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true});
+    _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
+    _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false});
+    _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false});
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_onehot), "onehot", 6, 0, 2, 4);
+}
+
+static void tst_single_dot() {
+    reslimit r;
+    sat::solver s({}, r);
+    _init_solver(s);
+
+    s.mk_clause({0, false}, {2, false}, {3, true});
+    s.mk_clause({0, true}, {1, true}, {3, true});
+    s.mk_clause({0, true}, {2, true}, {3, true});
+    s.mk_clause({0, false}, {2, true}, {3, false});
+    _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
+
+    _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_dot), "dot", 6, 0, 2, 4);
+}
+
+void tst_finder() {
+    tst_single_mux();
+    tst_single_maj();
+    tst_single_orand();
+    tst_single_and();
+    tst_single_xor();
+    tst_single_andxor();
+    tst_single_xorand();
+    tst_single_gamble();
+    tst_single_onehot();
+    tst_single_dot();
+}
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 8f3ab52af..05723f63c 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -257,4 +257,5 @@ int main(int argc, char ** argv) {
     TST(pdd_solver);
     TST(solver_pool);
     //TST_ARGV(hs);
+    TST(finder);
 }