From 30774ec6bc732478cce1a5ceff5f666893c416a6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 May 2014 13:48:25 +0200 Subject: [PATCH] Improved ezsat stand-alone tests --- libs/ezsat/Makefile | 4 +- libs/ezsat/ezsat.h | 2 +- libs/ezsat/puzzle3d.cc | 4 +- libs/ezsat/testbench.cc | 120 ++++++---------------------------------- 4 files changed, 24 insertions(+), 106 deletions(-) diff --git a/libs/ezsat/Makefile b/libs/ezsat/Makefile index da2355a9b..e831cc6f0 100644 --- 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 b0b731d0a..852405566 100644 --- 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 56d293260..aee0044b4 100644 --- a/libs/ezsat/puzzle3d.cc +++ b/libs/ezsat/puzzle3d.cc @@ -260,8 +260,10 @@ int main() std::vector modelExpressions; std::vector 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 8283686e3..8332ad919 100644 --- 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 &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 &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 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 av = sat.vec_const_signed(a, 8); std::vector 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 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 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 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();