Improved ezsat stand-alone tests

diff --git a/libs/ezsat/Makefile b/libs/ezsat/Makefile
index da2355a9b395d6a73563bfc7a37a4463ad8c40af..e831cc6f0bfaec594b01885adf2b72a25c4e2bce 100644 (file)
--- a/libs/ezsat/Makefile
+++ b/libs/ezsat/Makefile
@@ -3,7 +3,7 @@ CC = clang
 CXX = clang
 CXXFLAGS = -MD -Wall -Wextra -ggdb
 CXXFLAGS += -std=c++11 -O0
-LDLIBS = -lminisat -lstdc++
+LDLIBS = -lminisat -lm -lstdc++
 
 all: demo_vec demo_bit demo_cmp testbench puzzle3d
 
@@ -20,7 +20,7 @@ test: all
        ./demo_cmp
 
 clean:
-       rm -f demo_bit demo_vec testbench puzzle3d *.o *.d
+       rm -f demo_bit demo_vec demo_cmp testbench puzzle3d *.o *.d
 
 .PHONY: all test clean
 

diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index b0b731d0a605e86a48497e2b856d553a38dfc102..85240556684e478ed293743ea0c11cce8e81c5ad 100644 (file)
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -168,7 +168,7 @@ public:
                int get(ezSAT *that) {
                        if (name.empty())
                                return id;
-                       return that->literal(name);
+                       return that->frozen_literal(name);
                }
        };
 

diff --git a/libs/ezsat/puzzle3d.cc b/libs/ezsat/puzzle3d.cc
index 56d293260b81fa86926e794eddcb075b83d0b512..aee0044b42c3e76d49176b46136c92e053ef8d22 100644 (file)
--- a/libs/ezsat/puzzle3d.cc
+++ b/libs/ezsat/puzzle3d.cc
@@ -260,8 +260,10 @@ int main()
        std::vector<int> modelExpressions;
        std::vector<bool> modelValues;
 
-       for (auto &it : blockinfo)
+       for (auto &it : blockinfo) {
+               ez.freeze(it.first);
                modelExpressions.push_back(it.first);
+       }
 
        int solution_counter = 0;
        while (1)

diff --git a/libs/ezsat/testbench.cc b/libs/ezsat/testbench.cc
index 8283686e3bc36c3c3156425505ddc3ebcba89e74..8332ad919ef0233c79ece5c6aea00e9e6f60648b 100644 (file)
--- a/libs/ezsat/testbench.cc
+++ b/libs/ezsat/testbench.cc
@@ -63,7 +63,7 @@ void test_simple()
 {
        printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
 
-       ezSAT sat;
+       ezMiniSAT sat;
        sat.assume(sat.OR("A", "B"));
        sat.assume(sat.NOT(sat.AND("A", "B")));
        test(sat);
@@ -71,89 +71,6 @@ void test_simple()
 
 // ------------------------------------------------------------------------------------------------------------
 
-void test_basic_operators(ezSAT &sat, xorshift128 &rng, int iter, bool buildTrees, bool buildClusters, std::vector<bool> &log)
-{
-       int vars[6] = {
-               sat.VAR("A"), sat.VAR("B"), sat.VAR("C"),
-               sat.NOT("A"), sat.NOT("B"), sat.NOT("C")
-       };
-       for (int i = 0; i < iter; i++) {
-               int assumption = 0, op = rng() % 6, to = rng() % 6;
-               int a = vars[rng() % 6], b = vars[rng() % 6], c = vars[rng() % 6];
-               // printf("--> %d %d:%s %d:%s %d:%s\n", op, a, sat.to_string(a).c_str(), b, sat.to_string(b).c_str(), c, sat.to_string(c).c_str());
-               switch (op)
-               {
-               case 0:
-                       assumption = sat.NOT(a);
-                       break;
-               case 1:
-                       assumption = sat.AND(a, b);
-                       break;
-               case 2:
-                       assumption = sat.OR(a, b);
-                       break;
-               case 3:
-                       assumption = sat.XOR(a, b);
-                       break;
-               case 4:
-                       assumption = sat.IFF(a, b);
-                       break;
-               case 5:
-                       assumption = sat.ITE(a, b, c);
-                       break;
-               }
-               // printf("  --> %d:%s\n", to, sat.to_string(assumption).c_str());
-               if (buildTrees)
-                       vars[to] = assumption;
-               if (!buildClusters)
-                       sat.clear();
-               sat.assume(assumption);
-               if (sat.numCnfVariables() < 15) {
-                       printf("%d:\n", int(log.size()));
-                       log.push_back(test(sat));
-               } else {
-                       // printf("** skipping large problem **\n");
-               }
-       }
-}
-
-void test_basic_operators(ezSAT &sat, std::vector<bool> &log)
-{
-       printf("-- %s --\n\n", __PRETTY_FUNCTION__);
-
-       xorshift128 rng;
-       test_basic_operators(sat, rng, 1000, false, false, log);
-       for (int i = 0; i < 100; i++)
-               test_basic_operators(sat, rng, 10, true, false, log);
-       for (int i = 0; i < 100; i++)
-               test_basic_operators(sat, rng, 10, false, true, log);
-}
-
-void test_basic_operators()
-{
-       printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
-
-       ezSAT sat;
-       ezMiniSAT miniSat;
-       std::vector<bool> logSat, logMiniSat;
-
-       test_basic_operators(sat, logSat);
-       test_basic_operators(miniSat, logMiniSat);
-
-       if (logSat != logMiniSat) {
-               printf("Differences between logSat and logMiniSat:");
-               for (int i = 0; i < int(std::max(logSat.size(), logMiniSat.size())); i++)
-                       if (i >= int(logSat.size()) || i >= int(logMiniSat.size()) || logSat[i] != logMiniSat[i])
-                               printf(" %d", i);
-               printf("\n");
-               abort();
-       } else {
-               printf("Completed %d tests with identical results with ezSAT and ezMiniSAT.\n\n", int(logSat.size()));
-       }
-}
-
-// ------------------------------------------------------------------------------------------------------------
-
 void test_xorshift32_try(ezSAT &sat, uint32_t input_pattern)
 {
        uint32_t output_pattern = input_pattern;
@@ -238,7 +155,7 @@ void check(const char *expr1_str, bool expr1, const char *expr2_str, bool expr2)
 
 void test_signed(int8_t a, int8_t b, int8_t c)
 {
-       ezSAT sat;
+       ezMiniSAT sat;
 
        std::vector<int> av = sat.vec_const_signed(a, 8);
        std::vector<int> bv = sat.vec_const_signed(b, 8);
@@ -257,7 +174,7 @@ void test_signed(int8_t a, int8_t b, int8_t c)
 
 void test_unsigned(uint8_t a, uint8_t b, uint8_t c)
 {
-       ezSAT sat;
+       ezMiniSAT sat;
 
        if (b < c)
                b ^= c, c ^= b, b ^= c;
@@ -279,7 +196,7 @@ void test_unsigned(uint8_t a, uint8_t b, uint8_t c)
 
 void test_count(uint32_t x)
 {
-       ezSAT sat;
+       ezMiniSAT sat;
 
        int count = 0;
        for (int i = 0; i < 32; i++)
@@ -333,10 +250,10 @@ void test_onehot()
        printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
        ezMiniSAT ez;
 
-       int a = ez.literal("a");
-       int b = ez.literal("b");
-       int c = ez.literal("c");
-       int d = ez.literal("d");
+       int a = ez.frozen_literal("a");
+       int b = ez.frozen_literal("b");
+       int c = ez.frozen_literal("c");
+       int d = ez.frozen_literal("d");
 
        std::vector<int> abcd;
        abcd.push_back(a);
@@ -387,10 +304,10 @@ void test_manyhot()
        printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
        ezMiniSAT ez;
 
-       int a = ez.literal("a");
-       int b = ez.literal("b");
-       int c = ez.literal("c");
-       int d = ez.literal("d");
+       int a = ez.frozen_literal("a");
+       int b = ez.frozen_literal("b");
+       int c = ez.frozen_literal("c");
+       int d = ez.frozen_literal("d");
 
        std::vector<int> abcd;
        abcd.push_back(a);
@@ -441,13 +358,13 @@ void test_ordered()
        printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
        ezMiniSAT ez;
 
-       int a = ez.literal("a");
-       int b = ez.literal("b");
-       int c = ez.literal("c");
+       int a = ez.frozen_literal("a");
+       int b = ez.frozen_literal("b");
+       int c = ez.frozen_literal("c");
 
-       int x = ez.literal("x");
-       int y = ez.literal("y");
-       int z = ez.literal("z");
+       int x = ez.frozen_literal("x");
+       int y = ez.frozen_literal("y");
+       int z = ez.frozen_literal("z");
 
        std::vector<int> abc;
        abc.push_back(a);
@@ -507,7 +424,6 @@ void test_ordered()
 int main()
 {
        test_simple();
-       test_basic_operators();
        test_xorshift32();
        test_arith();
        test_onehot();