From 3371563f2f14ce0d6bc7798d0fc802b54aae93c8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 7 Jun 2013 10:38:35 +0200 Subject: [PATCH] Added ezSAT library --- Makefile | 25 +- libs/ezsat/Makefile | 26 + libs/ezsat/README | 29 + libs/ezsat/demo_bit.cc | 71 +++ libs/ezsat/demo_vec.cc | 112 ++++ libs/ezsat/ezminisat.cc | 120 ++++ libs/ezsat/ezminisat.h | 46 ++ libs/ezsat/ezsat.cc | 1221 ++++++++++++++++++++++++++++++++++++++ libs/ezsat/ezsat.h | 313 ++++++++++ libs/ezsat/puzzle3d.cc | 293 +++++++++ libs/ezsat/puzzle3d.scad | 82 +++ libs/ezsat/testbench.cc | 524 ++++++++++++++++ 12 files changed, 2854 insertions(+), 8 deletions(-) create mode 100644 libs/ezsat/Makefile create mode 100644 libs/ezsat/README create mode 100644 libs/ezsat/demo_bit.cc create mode 100644 libs/ezsat/demo_vec.cc create mode 100644 libs/ezsat/ezminisat.cc create mode 100644 libs/ezsat/ezminisat.h create mode 100644 libs/ezsat/ezsat.cc create mode 100644 libs/ezsat/ezsat.h create mode 100644 libs/ezsat/puzzle3d.cc create mode 100644 libs/ezsat/puzzle3d.scad create mode 100644 libs/ezsat/testbench.cc diff --git a/Makefile b/Makefile index e1b8bac16..09137f3d4 100644 --- a/Makefile +++ b/Makefile @@ -5,16 +5,10 @@ CONFIG := clang-debug ENABLE_TCL := 1 ENABLE_QT4 := 1 +ENABLE_MINISAT := 1 ENABLE_GPROF := 0 -OBJS = kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/select.o kernel/show.o - -OBJS += libs/bigint/BigIntegerAlgorithms.o libs/bigint/BigInteger.o libs/bigint/BigIntegerUtils.o -OBJS += libs/bigint/BigUnsigned.o libs/bigint/BigUnsignedInABase.o - -OBJS += libs/sha1/sha1.o -OBJS += libs/subcircuit/subcircuit.o - +OBJS = GENFILES = EXTRA_TARGETS = TARGETS = yosys yosys-config @@ -56,6 +50,21 @@ ifeq ($(ENABLE_QT4),1) TARGETS += yosys-svgviewer endif +OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/select.o kernel/show.o + +OBJS += libs/bigint/BigIntegerAlgorithms.o libs/bigint/BigInteger.o libs/bigint/BigIntegerUtils.o +OBJS += libs/bigint/BigUnsigned.o libs/bigint/BigUnsignedInABase.o + +OBJS += libs/sha1/sha1.o +OBJS += libs/subcircuit/subcircuit.o +OBJS += libs/ezsat/ezsat.o + +ifeq ($(ENABLE_MINISAT),1) +CXXFLAGS += -DYOSYS_ENABLE_MINISAT +OBJS += libs/ezsat/ezminisat.o +LDLIBS += -lminisat +endif + include frontends/*/Makefile.inc include passes/*/Makefile.inc include backends/*/Makefile.inc diff --git a/libs/ezsat/Makefile b/libs/ezsat/Makefile new file mode 100644 index 000000000..7a5d5fae4 --- /dev/null +++ b/libs/ezsat/Makefile @@ -0,0 +1,26 @@ + +CC = clang +CXX = clang +CXXFLAGS = -MD -Wall -Wextra -ggdb +CXXFLAGS += -std=c++11 -O0 +LDLIBS = -lminisat -lstdc++ + +all: demo_vec demo_bit testbench puzzle3d + +demo_vec: demo_vec.o ezsat.o ezminisat.o +demo_bit: demo_bit.o ezsat.o ezminisat.o +testbench: testbench.o ezsat.o ezminisat.o +puzzle3d: puzzle3d.o ezsat.o ezminisat.o + +test: all + ./testbench + ./demo_bit + ./demo_vec + +clean: + rm -f demo_bit demo_vec testbench puzzle3d *.o *.d + +.PHONY: all test clean + +-include *.d + diff --git a/libs/ezsat/README b/libs/ezsat/README new file mode 100644 index 000000000..c6745e6cf --- /dev/null +++ b/libs/ezsat/README @@ -0,0 +1,29 @@ + + ************************************************************************** + * * + * The ezSAT C++11 library * + * * + * A simple frontend to SAT solvers with bindings to MiniSAT. * + * by Clifford Wolf * + * * + ************************************************************************** + +============ +Introduction +============ + +This library acts as a frontend to SAT solvers and a helper for generating +CNF for sat solvers. It comes with bindings for MiniSAT (http://minisat.se/). + +Have a look at demo_bit.cc and demo_vec.cc for examples of how to set up +a SAT problem using ezSAT. Have a look at puzzle3d.cc for a more complex +(real-world) example of using ezSAT. + + +C++11 Warning +------------- + +This project is written in C++11. Use appropriate compiler switches to compile +it. Tested with clang version 3.0 and option -std=c++11. Also tested with gcc +version 4.6.3 and option -std=c++0x. + diff --git a/libs/ezsat/demo_bit.cc b/libs/ezsat/demo_bit.cc new file mode 100644 index 000000000..2a5099bf7 --- /dev/null +++ b/libs/ezsat/demo_bit.cc @@ -0,0 +1,71 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "ezminisat.h" +#include + +void print_results(bool satisfiable, const std::vector &modelValues) +{ + if (!satisfiable) { + printf("not satisfiable.\n\n"); + } else { + printf("satisfiable:"); + for (auto val : modelValues) + printf(" %d", val ? 1 : 0); + printf("\n\n"); + } +} + +int main() +{ + ezMiniSAT sat; + + // 3 input AOI-Gate + // 'pos_active' encodes the condition under which the pullup path of the gate is active + // 'neg_active' encodes the condition under which the pulldown path of the gate is active + // 'impossible' encodes the condition that both or none of the above paths is active + int pos_active = sat.AND(sat.NOT("A"), sat.OR(sat.NOT("B"), sat.NOT("C"))); + int neg_active = sat.OR("A", sat.AND("B", "C")); + int impossible = sat.IFF(pos_active, neg_active); + + std::vector modelVars; + std::vector modelValues; + bool satisfiable; + + modelVars.push_back(sat.VAR("A")); + modelVars.push_back(sat.VAR("B")); + modelVars.push_back(sat.VAR("C")); + + printf("\n"); + + printf("pos_active: %s\n", sat.to_string(pos_active).c_str()); + satisfiable = sat.solve(modelVars, modelValues, pos_active); + print_results(satisfiable, modelValues); + + printf("neg_active: %s\n", sat.to_string(neg_active).c_str()); + satisfiable = sat.solve(modelVars, modelValues, neg_active); + print_results(satisfiable, modelValues); + + printf("impossible: %s\n", sat.to_string(impossible).c_str()); + satisfiable = sat.solve(modelVars, modelValues, impossible); + print_results(satisfiable, modelValues); + + return 0; +} + diff --git a/libs/ezsat/demo_vec.cc b/libs/ezsat/demo_vec.cc new file mode 100644 index 000000000..b994f00d6 --- /dev/null +++ b/libs/ezsat/demo_vec.cc @@ -0,0 +1,112 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "ezminisat.h" +#include + +#define INIT_X 123456789 +#define INIT_Y 362436069 +#define INIT_Z 521288629 +#define INIT_W 88675123 + +uint32_t xorshift128() { + static uint32_t x = INIT_X; + static uint32_t y = INIT_Y; + static uint32_t z = INIT_Z; + static uint32_t w = INIT_W; + uint32_t t = x ^ (x << 11); + x = y; y = z; z = w; + w ^= (w >> 19) ^ t ^ (t >> 8); + return w; +} + +void xorshift128_sat(ezSAT &sat, std::vector &x, std::vector &y, std::vector &z, std::vector &w) +{ + std::vector t = sat.vec_xor(x, sat.vec_shl(x, 11)); + x = y; y = z; z = w; + w = sat.vec_xor(sat.vec_xor(w, sat.vec_shr(w, 19)), sat.vec_xor(t, sat.vec_shr(t, 8))); +} + +void find_xorshift128_init_state(uint32_t &x, uint32_t &y, uint32_t &z, uint32_t &w, uint32_t w1, uint32_t w2, uint32_t w3, uint32_t w4) +{ + ezMiniSAT sat; + + std::vector vx = sat.vec_var("x", 32); + std::vector vy = sat.vec_var("y", 32); + std::vector vz = sat.vec_var("z", 32); + std::vector vw = sat.vec_var("w", 32); + + xorshift128_sat(sat, vx, vy, vz, vw); + sat.vec_set_unsigned(vw, w1); + + xorshift128_sat(sat, vx, vy, vz, vw); + sat.vec_set_unsigned(vw, w2); + + xorshift128_sat(sat, vx, vy, vz, vw); + sat.vec_set_unsigned(vw, w3); + + xorshift128_sat(sat, vx, vy, vz, vw); + sat.vec_set_unsigned(vw, w4); + + std::vector modelExpressions; + std::vector modelValues; + + sat.vec_append(modelExpressions, sat.vec_var("x", 32)); + sat.vec_append(modelExpressions, sat.vec_var("y", 32)); + sat.vec_append(modelExpressions, sat.vec_var("z", 32)); + sat.vec_append(modelExpressions, sat.vec_var("w", 32)); + + // sat.printDIMACS(stdout); + + if (!sat.solve(modelExpressions, modelValues)) { + fprintf(stderr, "SAT solver failed to find a model!\n"); + abort(); + } + + x = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("x", 32)); + y = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("y", 32)); + z = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("z", 32)); + w = sat.vec_model_get_unsigned(modelExpressions, modelValues, sat.vec_var("w", 32)); +} + +int main() +{ + uint32_t w1 = xorshift128(); + uint32_t w2 = xorshift128(); + uint32_t w3 = xorshift128(); + uint32_t w4 = xorshift128(); + uint32_t x, y, z, w; + + printf("\n"); + + find_xorshift128_init_state(x, y, z, w, w1, w2, w3, w4); + + printf("x = %9u (%s)\n", (unsigned int)x, x == INIT_X ? "ok" : "ERROR"); + printf("y = %9u (%s)\n", (unsigned int)y, y == INIT_Y ? "ok" : "ERROR"); + printf("z = %9u (%s)\n", (unsigned int)z, z == INIT_Z ? "ok" : "ERROR"); + printf("w = %9u (%s)\n", (unsigned int)w, w == INIT_W ? "ok" : "ERROR"); + + if (x != INIT_X || y != INIT_Y || z != INIT_Z || w != INIT_W) + abort(); + + printf("\n"); + + return 0; +} + diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc new file mode 100644 index 000000000..fbc85c1ff --- /dev/null +++ b/libs/ezsat/ezminisat.cc @@ -0,0 +1,120 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#define __STDC_LIMIT_MACROS 1 + +#include "ezminisat.h" + +#include +#include +#include + +#include "minisat/core/Solver.h" + +ezMiniSAT::ezMiniSAT() : minisatSolver(NULL) +{ + minisatSolver = NULL; + foundContradiction = false; +} + +ezMiniSAT::~ezMiniSAT() +{ + if (minisatSolver != NULL) + delete minisatSolver; +} + +void ezMiniSAT::clear() +{ + if (minisatSolver != NULL) { + delete minisatSolver; + minisatSolver = NULL; + } + foundContradiction = false; + minisatVars.clear(); + ezSAT::clear(); +} + +bool ezMiniSAT::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) +{ + if (0) { +contradiction: + delete minisatSolver; + minisatSolver = NULL; + minisatVars.clear(); + foundContradiction = true; + return false; + } + + if (foundContradiction) { + consumeCnf(); + return false; + } + + std::vector extraClauses, modelIdx; + + for (auto id : assumptions) + extraClauses.push_back(bind(id)); + for (auto id : modelExpressions) + modelIdx.push_back(bind(id)); + + if (minisatSolver == NULL) + minisatSolver = new Minisat::Solver; + + std::vector> cnf; + consumeCnf(cnf); + + while (int(minisatVars.size()) < numCnfVariables()) + minisatVars.push_back(minisatSolver->newVar()); + + for (auto &clause : cnf) { + Minisat::vec ps; + for (auto idx : clause) + if (idx > 0) + ps.push(Minisat::mkLit(minisatVars[idx-1])); + else + ps.push(Minisat::mkLit(minisatVars[-idx-1], true)); + if (!minisatSolver->addClause(ps)) + goto contradiction; + } + + if (cnf.size() > 0 && !minisatSolver->simplify()) + goto contradiction; + + Minisat::vec assumps; + + for (auto idx : extraClauses) + if (idx > 0) + assumps.push(Minisat::mkLit(minisatVars[idx-1])); + else + assumps.push(Minisat::mkLit(minisatVars[-idx-1], true)); + + if (!minisatSolver->solve(assumps)) + return false; + + modelValues.clear(); + modelValues.reserve(modelIdx.size()); + for (auto idx : modelIdx) { + auto value = minisatSolver->modelValue(minisatVars[idx-1]); + // FIXME: Undef values + modelValues.push_back(value == Minisat::lbool(true)); + } + + return true; +} + diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h new file mode 100644 index 000000000..4171985b6 --- /dev/null +++ b/libs/ezsat/ezminisat.h @@ -0,0 +1,46 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#ifndef EZMINISAT_H +#define EZMINISAT_H + +#include "ezsat.h" + +// minisat is using limit macros and format macros in their headers that +// can be the source of some troubles when used from c++11. thefore we +// don't force ezSAT users to use minisat headers.. +namespace Minisat { + class Solver; +} + +class ezMiniSAT : public ezSAT +{ +private: + Minisat::Solver *minisatSolver; + std::vector minisatVars; + bool foundContradiction; + +public: + ezMiniSAT(); + virtual ~ezMiniSAT(); + virtual void clear(); + virtual bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions); +}; + +#endif diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc new file mode 100644 index 000000000..d6ebd678b --- /dev/null +++ b/libs/ezsat/ezsat.cc @@ -0,0 +1,1221 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "ezsat.h" + +#include + +#include +#include + +ezSAT::ezSAT() +{ + literal("TRUE"); + literal("FALSE"); + + assert(literal("TRUE") == TRUE); + assert(literal("FALSE") == FALSE); + + cnfConsumed = false; + cnfVariableCount = 0; +} + +ezSAT::~ezSAT() +{ +} + +int ezSAT::value(bool val) +{ + return val ? TRUE : FALSE; +} + +int ezSAT::literal() +{ + literals.push_back(std::string()); + return literals.size(); +} + +int ezSAT::literal(const std::string &name) +{ + if (literalsCache.count(name) == 0) { + literals.push_back(name); + literalsCache[name] = literals.size(); + } + return literalsCache.at(name); +} + +int ezSAT::expression(OpId op, int a, int b, int c, int d, int e, int f) +{ + std::vector args(6); + args[0] = a, args[1] = b, args[2] = c; + args[3] = d, args[4] = e, args[5] = f; + return expression(op, args); +} + +int ezSAT::expression(OpId op, const std::vector &args) +{ + std::vector myArgs; + myArgs.reserve(args.size()); + bool xorRemovedOddTrues = false; + + for (auto arg : args) + { + if (arg == 0) + continue; + if (op == OpAnd && arg == TRUE) + continue; + if ((op == OpOr || op == OpXor) && arg == FALSE) + continue; + if (op == OpXor && arg == TRUE) { + xorRemovedOddTrues = !xorRemovedOddTrues; + continue; + } + myArgs.push_back(arg); + } + + if (myArgs.size() > 0 && (op == OpAnd || op == OpOr || op == OpXor || op == OpIFF)) { + std::sort(myArgs.begin(), myArgs.end()); + int j = 0; + for (int i = 1; i < int(myArgs.size()); i++) + if (j < 0 || myArgs[j] != myArgs[i]) + myArgs[++j] = myArgs[i]; + else if (op == OpXor) + j--; + myArgs.resize(j+1); + } + + switch (op) + { + case OpNot: + assert(myArgs.size() == 1); + if (myArgs[0] == TRUE) + return FALSE; + if (myArgs[0] == FALSE) + return TRUE; + break; + + case OpAnd: + if (myArgs.size() == 0) + return TRUE; + if (myArgs.size() == 1) + return myArgs[0]; + break; + + case OpOr: + if (myArgs.size() == 0) + return FALSE; + if (myArgs.size() == 1) + return myArgs[0]; + break; + + case OpXor: + if (myArgs.size() == 0) + return xorRemovedOddTrues ? TRUE : FALSE; + if (myArgs.size() == 1) + return myArgs[0]; + break; + + case OpIFF: + assert(myArgs.size() >= 1); + if (myArgs.size() == 1) + return TRUE; + // FIXME: Add proper const folding + break; + + case OpITE: + assert(myArgs.size() == 3); + if (myArgs[0] == TRUE) + return myArgs[1]; + if (myArgs[0] == FALSE) + return myArgs[2]; + break; + + default: + abort(); + } + + std::pair> myExpr(op, myArgs); + int id = 0; + + if (expressionsCache.count(myExpr) > 0) { + id = expressionsCache.at(myExpr); + } else { + id = -(expressions.size() + 1); + expressionsCache[myExpr] = id; + expressions.push_back(myExpr); + } + + return xorRemovedOddTrues ? expression(OpNot, id) : id; +} + +void ezSAT::lookup_literal(int id, std::string &name) const +{ + assert(0 < id && id <= int(literals.size())); + name = literals[id - 1]; +} + +const std::string &ezSAT::lookup_literal(int id) const +{ + assert(0 < id && id <= int(literals.size())); + return literals[id - 1]; +} + +void ezSAT::lookup_expression(int id, OpId &op, std::vector &args) const +{ + assert(0 < -id && -id <= int(expressions.size())); + op = expressions[-id - 1].first; + args = expressions[-id - 1].second; +} + +const std::vector &ezSAT::lookup_expression(int id, OpId &op) const +{ + assert(0 < -id && -id <= int(expressions.size())); + op = expressions[-id - 1].first; + return expressions[-id - 1].second; +} + +int ezSAT::parse_string(const std::string &) +{ + abort(); +} + +std::string ezSAT::to_string(int id) const +{ + std::string text; + + if (id > 0) + { + lookup_literal(id, text); + } + else + { + OpId op; + std::vector args; + lookup_expression(id, op, args); + + switch (op) + { + case OpNot: + text = "not("; + break; + + case OpAnd: + text = "and("; + break; + + case OpOr: + text = "or("; + break; + + case OpXor: + text = "xor("; + break; + + case OpIFF: + text = "iff("; + break; + + case OpITE: + text = "ite("; + break; + + default: + abort(); + } + + for (int i = 0; i < int(args.size()); i++) { + if (i > 0) + text += ", "; + text += to_string(args[i]); + } + + text += ")"; + } + + return text; +} + +int ezSAT::eval(int id, const std::vector &values) const +{ + if (id > 0) { + if (id <= int(values.size()) && (values[id-1] == TRUE || values[id-1] == FALSE || values[id-1] == 0)) + return values[id-1]; + return 0; + } + + OpId op; + const std::vector &args = lookup_expression(id, op); + int a, b; + + switch (op) + { + case OpNot: + assert(args.size() == 1); + a = eval(args[0], values); + if (a == TRUE) + return FALSE; + if (a == FALSE) + return TRUE; + return 0; + case OpAnd: + a = TRUE; + for (auto arg : args) { + b = eval(arg, values); + if (b != TRUE && b != FALSE) + a = 0; + if (b == FALSE) + return FALSE; + } + return a; + case OpOr: + a = FALSE; + for (auto arg : args) { + b = eval(arg, values); + if (b != TRUE && b != FALSE) + a = 0; + if (b == TRUE) + return TRUE; + } + return a; + case OpXor: + a = FALSE; + for (auto arg : args) { + b = eval(arg, values); + if (b != TRUE && b != FALSE) + return 0; + if (b == TRUE) + a = a == TRUE ? FALSE : TRUE; + } + return a; + case OpIFF: + assert(args.size() > 0); + a = eval(args[0], values); + for (auto arg : args) { + b = eval(arg, values); + if (b != TRUE && b != FALSE) + return 0; + if (b != a) + return FALSE; + } + return TRUE; + case OpITE: + assert(args.size() == 3); + a = eval(args[0], values); + if (a == TRUE) + return eval(args[1], values); + if (a == FALSE) + return eval(args[2], values); + return 0; + default: + abort(); + } +} + +void ezSAT::clear() +{ + cnfConsumed = false; + cnfVariableCount = 0; + cnfLiteralVariables.clear(); + cnfExpressionVariables.clear(); + cnfClauses.clear(); + cnfAssumptions.clear(); +} + +void ezSAT::assume(int id) +{ + int idx = bind(id); + cnfClauses.push_back(std::vector(1, idx)); + cnfAssumptions.insert(id); +} + +void ezSAT::add_clause(const std::vector &args) +{ + cnfClauses.push_back(args); +} + +void ezSAT::add_clause(const std::vector &args, bool argsPolarity, int a, int b, int c) +{ + std::vector clause; + for (auto arg : args) + clause.push_back(argsPolarity ? +arg : -arg); + if (a != 0) + clause.push_back(a); + if (b != 0) + clause.push_back(b); + if (c != 0) + clause.push_back(c); + add_clause(clause); +} + +void ezSAT::add_clause(int a, int b, int c) +{ + std::vector clause; + if (a != 0) + clause.push_back(a); + if (b != 0) + clause.push_back(b); + if (c != 0) + clause.push_back(c); + add_clause(clause); +} + +int ezSAT::bind_cnf_not(const std::vector &args) +{ + assert(args.size() == 1); + return -args[0]; +} + +int ezSAT::bind_cnf_and(const std::vector &args) +{ + assert(args.size() >= 2); + + int idx = ++cnfVariableCount; + add_clause(args, false, idx); + + for (auto arg : args) + add_clause(-idx, arg); + + return idx; +} + +int ezSAT::bind_cnf_or(const std::vector &args) +{ + assert(args.size() >= 2); + + int idx = ++cnfVariableCount; + add_clause(args, true, -idx); + + for (auto arg : args) + add_clause(idx, -arg); + + return idx; +} + +int ezSAT::bound(int id) const +{ + if (id > 0 && id <= int(cnfLiteralVariables.size())) + return cnfLiteralVariables[id-1]; + if (-id > 0 && -id <= int(cnfExpressionVariables.size())) + return cnfExpressionVariables[-id-1]; + return 0; +} + +int ezSAT::bind(int id) +{ + if (id >= 0) { + assert(0 < id && id <= int(literals.size())); + cnfLiteralVariables.resize(literals.size()); + if (cnfLiteralVariables[id-1] == 0) { + cnfLiteralVariables[id-1] = ++cnfVariableCount; + if (id == TRUE) + add_clause(+cnfLiteralVariables[id-1]); + if (id == FALSE) + add_clause(-cnfLiteralVariables[id-1]); + } + return cnfLiteralVariables[id-1]; + } + + assert(0 < -id && -id <= int(expressions.size())); + cnfExpressionVariables.resize(expressions.size()); + + if (cnfExpressionVariables[-id-1] == 0) + { + OpId op; + std::vector args; + lookup_expression(id, op, args); + int idx = 0; + + if (op == OpXor) { + while (args.size() > 1) { + std::vector newArgs; + for (int i = 0; i < int(args.size()); i += 2) + if (i+1 == int(args.size())) + newArgs.push_back(args[i]); + else + newArgs.push_back(OR(AND(args[i], NOT(args[i+1])), AND(NOT(args[i]), args[i+1]))); + args.swap(newArgs); + } + idx = bind(args.at(0)); + goto assign_idx; + } + + if (op == OpIFF) { + std::vector invArgs; + for (auto arg : args) + invArgs.push_back(NOT(arg)); + idx = bind(OR(expression(OpAnd, args), expression(OpAnd, invArgs))); + goto assign_idx; + } + + if (op == OpITE) { + idx = bind(OR(AND(args[0], args[1]), AND(NOT(args[0]), args[2]))); + goto assign_idx; + } + + for (int i = 0; i < int(args.size()); i++) + args[i] = bind(args[i]); + + switch (op) + { + case OpNot: idx = bind_cnf_not(args); break; + case OpAnd: idx = bind_cnf_and(args); break; + case OpOr: idx = bind_cnf_or(args); break; + default: abort(); + } + + assign_idx: + assert(idx != 0); + cnfExpressionVariables[-id-1] = idx; + } + + return cnfExpressionVariables[-id-1]; +} + +void ezSAT::consumeCnf() +{ + cnfConsumed = true; + cnfClauses.clear(); +} + +void ezSAT::consumeCnf(std::vector> &cnf) +{ + cnfConsumed = true; + cnf.swap(cnfClauses); + cnfClauses.clear(); +} + +static bool test_bit(uint32_t bitmask, int idx) +{ + if (idx > 0) + return (bitmask & (1 << (+idx-1))) != 0; + else + return (bitmask & (1 << (-idx-1))) == 0; +} + +bool ezSAT::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) +{ + std::vector extraClauses, modelIdx; + std::vector values(numLiterals()); + + for (auto id : assumptions) + extraClauses.push_back(bind(id)); + for (auto id : modelExpressions) + modelIdx.push_back(bind(id)); + + if (cnfVariableCount > 20) { + fprintf(stderr, "*************************************************************************************\n"); + fprintf(stderr, "ERROR: You are trying to use the builtin solver of ezSAT with more than 20 variables!\n"); + fprintf(stderr, "The builtin solver is a dumb brute force solver and only ment for testing and demo\n"); + fprintf(stderr, "purposes. Use a real SAT solve like MiniSAT (e.g. using the ezMiniSAT class) instead.\n"); + fprintf(stderr, "*************************************************************************************\n"); + abort(); + } + + for (uint32_t bitmask = 0; bitmask < (1 << numCnfVariables()); bitmask++) + { + // printf("%07o:", int(bitmask)); + // for (int i = 2; i < numLiterals(); i++) + // if (bound(i+1)) + // printf(" %s=%d", to_string(i+1).c_str(), test_bit(bitmask, bound(i+1))); + // printf(" |"); + // for (int idx = 1; idx <= numCnfVariables(); idx++) + // printf(" %3d", test_bit(bitmask, idx) ? idx : -idx); + // printf("\n"); + + for (auto idx : extraClauses) + if (!test_bit(bitmask, idx)) + goto next; + + for (auto &clause : cnfClauses) { + for (auto idx : clause) + if (test_bit(bitmask, idx)) + goto next_clause; + // printf("failed clause:"); + // for (auto idx2 : clause) + // printf(" %3d", idx2); + // printf("\n"); + goto next; + next_clause:; + // printf("passed clause:"); + // for (auto idx2 : clause) + // printf(" %3d", idx2); + // printf("\n"); + } + + modelValues.resize(modelIdx.size()); + for (int i = 0; i < int(modelIdx.size()); i++) + modelValues[i] = test_bit(bitmask, modelIdx[i]); + + // validate result using eval() + + values[0] = TRUE, values[1] = FALSE; + for (int i = 2; i < numLiterals(); i++) { + int idx = bound(i+1); + values[i] = idx != 0 ? (test_bit(bitmask, idx) ? TRUE : FALSE) : 0; + } + + for (auto id : cnfAssumptions) { + int result = eval(id, values); + if (result != TRUE) { + printInternalState(stderr); + fprintf(stderr, "Variables:"); + for (int i = 0; i < numLiterals(); i++) + fprintf(stderr, " %s=%s", lookup_literal(i+1).c_str(), values[i] == TRUE ? "TRUE" : values[i] == FALSE ? "FALSE" : "UNDEF"); + fprintf(stderr, "\nValidation of solver results failed: got `%d' (%s) for assumption '%d': %s\n", + result, result == FALSE ? "FALSE" : "UNDEF", id, to_string(id).c_str()); + abort(); + } + // printf("OK: %d -> %d\n", id, result); + } + + for (auto id : assumptions) { + int result = eval(id, values); + if (result != TRUE) { + printInternalState(stderr); + fprintf(stderr, "Variables:"); + for (int i = 0; i < numLiterals(); i++) + fprintf(stderr, " %s=%s", lookup_literal(i+1).c_str(), values[i] == TRUE ? "TRUE" : values[i] == FALSE ? "FALSE" : "UNDEF"); + fprintf(stderr, "\nValidation of solver results failed: got `%d' (%s) for assumption '%d': %s\n", + result, result == FALSE ? "FALSE" : "UNDEF", id, to_string(id).c_str()); + abort(); + } + // printf("OK: %d -> %d\n", id, result); + } + + return true; + next:; + } + + return false; +} + +std::vector ezSAT::vec_const_signed(int64_t value, int bits) +{ + std::vector vec; + for (int i = 0; i < bits; i++) + vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE); + return vec; +} + +std::vector ezSAT::vec_const_unsigned(uint64_t value, int bits) +{ + std::vector vec; + for (int i = 0; i < bits; i++) + vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE); + return vec; +} + +std::vector ezSAT::vec_var(std::string name, int bits) +{ + std::vector vec; + for (int i = 0; i < bits; i++) + vec.push_back(VAR(name + "[" + std::to_string(i) + "]")); + return vec; +} + +std::vector ezSAT::vec_cast(const std::vector &vec1, int toBits, bool signExtend) +{ + std::vector vec; + for (int i = 0; i < toBits; i++) + if (i >= int(vec1.size())) + vec.push_back(signExtend ? vec1.back() : FALSE); + else + vec.push_back(vec1[i]); + return vec; +} + +std::vector ezSAT::vec_not(const std::vector &vec1) +{ + std::vector vec; + for (auto bit : vec1) + vec.push_back(NOT(bit)); + return vec; +} + +std::vector ezSAT::vec_and(const std::vector &vec1, const std::vector &vec2) +{ + assert(vec1.size() == vec2.size()); + std::vector vec(vec1.size()); + for (int i = 0; i < int(vec1.size()); i++) + vec[i] = AND(vec1[i], vec2[i]); + return vec; +} + +std::vector ezSAT::vec_or(const std::vector &vec1, const std::vector &vec2) +{ + assert(vec1.size() == vec2.size()); + std::vector vec(vec1.size()); + for (int i = 0; i < int(vec1.size()); i++) + vec[i] = OR(vec1[i], vec2[i]); + return vec; +} + +std::vector ezSAT::vec_xor(const std::vector &vec1, const std::vector &vec2) +{ + assert(vec1.size() == vec2.size()); + std::vector vec(vec1.size()); + for (int i = 0; i < int(vec1.size()); i++) + vec[i] = XOR(vec1[i], vec2[i]); + return vec; +} + +std::vector ezSAT::vec_iff(const std::vector &vec1, const std::vector &vec2) +{ + assert(vec1.size() == vec2.size()); + std::vector vec(vec1.size()); + for (int i = 0; i < int(vec1.size()); i++) + vec[i] = IFF(vec1[i], vec2[i]); + return vec; +} + +std::vector ezSAT::vec_ite(const std::vector &vec1, const std::vector &vec2, const std::vector &vec3) +{ + assert(vec1.size() == vec2.size() && vec2.size() == vec3.size()); + std::vector vec(vec1.size()); + for (int i = 0; i < int(vec1.size()); i++) + vec[i] = ITE(vec1[i], vec2[i], vec3[i]); + return vec; +} + + +std::vector ezSAT::vec_ite(int sel, const std::vector &vec1, const std::vector &vec2) +{ + assert(vec1.size() == vec2.size()); + std::vector vec(vec1.size()); + for (int i = 0; i < int(vec1.size()); i++) + vec[i] = ITE(sel, vec1[i], vec2[i]); + return vec; +} + +// 'y' is the MSB (carry) and x the LSB (sum) output +static void fulladder(ezSAT *that, int a, int b, int c, int &y, int &x) +{ + int tmp = that->XOR(a, b); + int new_x = that->XOR(tmp, c); + int new_y = that->OR(that->AND(a, b), that->AND(c, tmp)); +#if 0 + printf("FULLADD> a=%s, b=%s, c=%s, carry=%s, sum=%s\n", that->to_string(a).c_str(), that->to_string(b).c_str(), + that->to_string(c).c_str(), that->to_string(new_y).c_str(), that->to_string(new_x).c_str()); +#endif + x = new_x, y = new_y; +} + +// 'y' is the MSB (carry) and x the LSB (sum) output +static void halfadder(ezSAT *that, int a, int b, int &y, int &x) +{ + int new_x = that->XOR(a, b); + int new_y = that->AND(a, b); +#if 0 + printf("HALFADD> a=%s, b=%s, carry=%s, sum=%s\n", that->to_string(a).c_str(), that->to_string(b).c_str(), + that->to_string(new_y).c_str(), that->to_string(new_x).c_str()); +#endif + x = new_x, y = new_y; +} + +std::vector ezSAT::vec_count(const std::vector &vec, int bits, bool clip) +{ + std::vector sum = vec_const_unsigned(0, bits); + std::vector carry_vector; + + for (auto bit : vec) { + int carry = bit; + for (int i = 0; i < bits; i++) + halfadder(this, carry, sum[i], carry, sum[i]); + carry_vector.push_back(carry); + } + + if (clip) { + int overflow = vec_reduce_or(carry_vector); + sum = vec_ite(overflow, vec_const_unsigned(~0, bits), sum); + } + +#if 0 + printf("COUNT> vec=["); + for (int i = int(vec.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec[i]).c_str(), i ? ", " : ""); + printf("], result=["); + for (int i = int(sum.size())-1; i >= 0; i--) + printf("%s%s", to_string(sum[i]).c_str(), i ? ", " : ""); + printf("]\n"); +#endif + + return sum; +} + +std::vector ezSAT::vec_add(const std::vector &vec1, const std::vector &vec2) +{ + assert(vec1.size() == vec2.size()); + std::vector vec(vec1.size()); + int carry = FALSE; + for (int i = 0; i < int(vec1.size()); i++) + fulladder(this, vec1[i], vec2[i], carry, carry, vec[i]); + +#if 0 + printf("ADD> vec1=["); + for (int i = int(vec1.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec1[i]).c_str(), i ? ", " : ""); + printf("], vec2=["); + for (int i = int(vec2.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec2[i]).c_str(), i ? ", " : ""); + printf("], result=["); + for (int i = int(vec.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec[i]).c_str(), i ? ", " : ""); + printf("]\n"); +#endif + + return vec; +} + +std::vector ezSAT::vec_sub(const std::vector &vec1, const std::vector &vec2) +{ + assert(vec1.size() == vec2.size()); + std::vector vec(vec1.size()); + int carry = TRUE; + for (int i = 0; i < int(vec1.size()); i++) + fulladder(this, vec1[i], NOT(vec2[i]), carry, carry, vec[i]); + +#if 0 + printf("SUB> vec1=["); + for (int i = int(vec1.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec1[i]).c_str(), i ? ", " : ""); + printf("], vec2=["); + for (int i = int(vec2.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec2[i]).c_str(), i ? ", " : ""); + printf("], result=["); + for (int i = int(vec.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec[i]).c_str(), i ? ", " : ""); + printf("]\n"); +#endif + + return vec; +} + +void ezSAT::vec_cmp(const std::vector &vec1, const std::vector &vec2, int &carry, int &overflow, int &sign, int &zero) +{ + assert(vec1.size() == vec2.size()); + carry = TRUE; + zero = FALSE; + for (int i = 0; i < int(vec1.size()); i++) { + overflow = carry; + fulladder(this, vec1[i], NOT(vec2[i]), carry, carry, sign); + zero = OR(zero, sign); + } + overflow = XOR(overflow, carry); + carry = NOT(carry); + zero = NOT(zero); + +#if 0 + printf("CMP> vec1=["); + for (int i = int(vec1.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec1[i]).c_str(), i ? ", " : ""); + printf("], vec2=["); + for (int i = int(vec2.size())-1; i >= 0; i--) + printf("%s%s", to_string(vec2[i]).c_str(), i ? ", " : ""); + printf("], carry=%s, overflow=%s, sign=%s, zero=%s\n", to_string(carry).c_str(), to_string(overflow).c_str(), to_string(sign).c_str(), to_string(zero).c_str()); +#endif +} + +int ezSAT::vec_lt_signed(const std::vector &vec1, const std::vector &vec2) +{ + int carry, overflow, sign, zero; + vec_cmp(vec1, vec2, carry, overflow, sign, zero); + return OR(AND(NOT(overflow), sign), AND(overflow, NOT(sign))); +} + +int ezSAT::vec_le_signed(const std::vector &vec1, const std::vector &vec2) +{ + int carry, overflow, sign, zero; + vec_cmp(vec1, vec2, carry, overflow, sign, zero); + return OR(AND(NOT(overflow), sign), AND(overflow, NOT(sign)), zero); +} + +int ezSAT::vec_ge_signed(const std::vector &vec1, const std::vector &vec2) +{ + int carry, overflow, sign, zero; + vec_cmp(vec1, vec2, carry, overflow, sign, zero); + return OR(AND(NOT(overflow), NOT(sign)), AND(overflow, sign)); +} + +int ezSAT::vec_gt_signed(const std::vector &vec1, const std::vector &vec2) +{ + int carry, overflow, sign, zero; + vec_cmp(vec1, vec2, carry, overflow, sign, zero); + return AND(OR(AND(NOT(overflow), NOT(sign)), AND(overflow, sign)), NOT(zero)); +} + +int ezSAT::vec_lt_unsigned(const std::vector &vec1, const std::vector &vec2) +{ + int carry, overflow, sign, zero; + vec_cmp(vec1, vec2, carry, overflow, sign, zero); + return carry; +} + +int ezSAT::vec_le_unsigned(const std::vector &vec1, const std::vector &vec2) +{ + int carry, overflow, sign, zero; + vec_cmp(vec1, vec2, carry, overflow, sign, zero); + return OR(carry, zero); +} + +int ezSAT::vec_ge_unsigned(const std::vector &vec1, const std::vector &vec2) +{ + int carry, overflow, sign, zero; + vec_cmp(vec1, vec2, carry, overflow, sign, zero); + return NOT(carry); +} + +int ezSAT::vec_gt_unsigned(const std::vector &vec1, const std::vector &vec2) +{ + int carry, overflow, sign, zero; + vec_cmp(vec1, vec2, carry, overflow, sign, zero); + return AND(NOT(carry), NOT(zero)); +} + +int ezSAT::vec_eq(const std::vector &vec1, const std::vector &vec2) +{ + return vec_reduce_and(vec_iff(vec1, vec2)); +} + +int ezSAT::vec_ne(const std::vector &vec1, const std::vector &vec2) +{ + return NOT(vec_reduce_and(vec_iff(vec1, vec2))); +} + +std::vector ezSAT::vec_shl(const std::vector &vec1, int shift, bool signExtend) +{ + std::vector vec; + for (int i = 0; i < int(vec1.size()); i++) { + int j = i-shift; + if (int(vec1.size()) <= j) + vec.push_back(signExtend ? vec1.back() : FALSE); + else if (0 <= j) + vec.push_back(vec1[j]); + else + vec.push_back(FALSE); + } + return vec; +} + +std::vector ezSAT::vec_srl(const std::vector &vec1, int shift) +{ + std::vector vec; + for (int i = 0; i < int(vec1.size()); i++) { + int j = i-shift; + while (j < 0) + j += vec1.size(); + while (j >= int(vec1.size())) + j -= vec1.size(); + vec.push_back(vec1[j]); + } + return vec; +} + +void ezSAT::vec_append(std::vector &vec, const std::vector &vec1) const +{ + for (auto bit : vec1) + vec.push_back(bit); +} + +void ezSAT::vec_append_signed(std::vector &vec, const std::vector &vec1, int64_t value) +{ + assert(int(vec1.size()) <= 64); + for (int i = 0; i < int(vec1.size()); i++) { + if (((value >> i) & 1) != 0) + vec.push_back(vec1[i]); + else + vec.push_back(NOT(vec1[i])); + } +} + +void ezSAT::vec_append_unsigned(std::vector &vec, const std::vector &vec1, uint64_t value) +{ + assert(int(vec1.size()) <= 64); + for (int i = 0; i < int(vec1.size()); i++) { + if (((value >> i) & 1) != 0) + vec.push_back(vec1[i]); + else + vec.push_back(NOT(vec1[i])); + } +} + +int64_t ezSAT::vec_model_get_signed(const std::vector &modelExpressions, const std::vector &modelValues, const std::vector &vec1) const +{ + int64_t value = 0; + std::map modelMap; + assert(modelExpressions.size() == modelValues.size()); + for (int i = 0; i < int(modelExpressions.size()); i++) + modelMap[modelExpressions[i]] = modelValues[i]; + for (int i = 0; i < 64; i++) { + int j = i < int(vec1.size()) ? i : vec1.size()-1; + if (modelMap.at(vec1[j])) + value |= 1 << i; + } + return value; +} + +uint64_t ezSAT::vec_model_get_unsigned(const std::vector &modelExpressions, const std::vector &modelValues, const std::vector &vec1) const +{ + uint64_t value = 0; + std::map modelMap; + assert(modelExpressions.size() == modelValues.size()); + for (int i = 0; i < int(modelExpressions.size()); i++) + modelMap[modelExpressions[i]] = modelValues[i]; + for (int i = 0; i < int(vec1.size()); i++) + if (modelMap.at(vec1[i])) + value |= 1 << i; + return value; +} + +int ezSAT::vec_reduce_and(const std::vector &vec1) +{ + return expression(OpAnd, vec1); +} + +int ezSAT::vec_reduce_or(const std::vector &vec1) +{ + return expression(OpOr, vec1); +} + +void ezSAT::vec_set(const std::vector &vec1, const std::vector &vec2) +{ + assert(vec1.size() == vec2.size()); + for (int i = 0; i < int(vec1.size()); i++) + SET(vec1[i], vec2[i]); +} + +void ezSAT::vec_set_signed(const std::vector &vec1, int64_t value) +{ + assert(int(vec1.size()) <= 64); + for (int i = 0; i < int(vec1.size()); i++) { + if (((value >> i) & 1) != 0) + assume(vec1[i]); + else + assume(NOT(vec1[i])); + } +} + +void ezSAT::vec_set_unsigned(const std::vector &vec1, uint64_t value) +{ + assert(int(vec1.size()) <= 64); + for (int i = 0; i < int(vec1.size()); i++) { + if (((value >> i) & 1) != 0) + assume(vec1[i]); + else + assume(NOT(vec1[i])); + } +} + +ezSATbit ezSAT::bit(_V a) +{ + return ezSATbit(*this, a); +} + +ezSATvec ezSAT::vec(const std::vector &vec) +{ + return ezSATvec(*this, vec); +} + +void ezSAT::printDIMACS(FILE *f, bool verbose) const +{ + if (cnfConsumed) { + fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!"); + abort(); + } + + int digits = ceil(log10f(cnfVariableCount)) + 2; + + fprintf(f, "c generated by ezSAT\n"); + + if (verbose) + { + fprintf(f, "c\n"); + fprintf(f, "c mapping of variables to literals:\n"); + for (int i = 0; i < int(cnfLiteralVariables.size()); i++) + if (cnfLiteralVariables[i] != 0) + fprintf(f, "c %*d: %s\n", digits, cnfLiteralVariables[i], literals[i].c_str()); + + fprintf(f, "c\n"); + fprintf(f, "c mapping of variables to expressions:\n"); + for (int i = 0; i < int(cnfExpressionVariables.size()); i++) + if (cnfExpressionVariables[i] != 0) + fprintf(f, "c %*d: %s\n", digits, cnfExpressionVariables[i], to_string(-i-1).c_str()); + + fprintf(f, "c\n"); + } + + fprintf(f, "p cnf %d %d\n", cnfVariableCount, int(cnfClauses.size())); + int maxClauseLen = 0; + for (auto &clause : cnfClauses) + maxClauseLen = std::max(int(clause.size()), maxClauseLen); + for (auto &clause : cnfClauses) { + for (auto idx : clause) + fprintf(f, " %*d", digits, idx); + fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0); + } +} + +static std::string expression2str(const std::pair> &data) +{ + std::string text; + switch (data.first) { +#define X(op) case ezSAT::op: text += #op; break; + X(OpNot) + X(OpAnd) + X(OpOr) + X(OpXor) + X(OpIFF) + X(OpITE) + default: + abort(); +#undef X + } + text += ":"; + for (auto it : data.second) + text += " " + std::to_string(it); + return text; +} + +void ezSAT::printInternalState(FILE *f) const +{ + fprintf(f, "--8<-- snip --8<--\n"); + + fprintf(f, "literalsCache:\n"); + for (auto &it : literalsCache) + fprintf(f, " `%s' -> %d\n", it.first.c_str(), it.second); + + fprintf(f, "literals:\n"); + for (int i = 0; i < int(literals.size()); i++) + fprintf(f, " %d: `%s'\n", i+1, literals[i].c_str()); + + fprintf(f, "expressionsCache:\n"); + for (auto &it : expressionsCache) + fprintf(f, " `%s' -> %d\n", expression2str(it.first).c_str(), it.second); + + fprintf(f, "expressions:\n"); + for (int i = 0; i < int(expressions.size()); i++) + fprintf(f, " %d: `%s'\n", -i-1, expression2str(expressions[i]).c_str()); + + fprintf(f, "cnfVariables (count=%d):\n", cnfVariableCount); + for (int i = 0; i < int(cnfLiteralVariables.size()); i++) + if (cnfLiteralVariables[i] != 0) + fprintf(f, " literal %d -> %d (%s)\n", i+1, cnfLiteralVariables[i], to_string(i+1).c_str()); + for (int i = 0; i < int(cnfExpressionVariables.size()); i++) + if (cnfExpressionVariables[i] != 0) + fprintf(f, " expression %d -> %d (%s)\n", -i-1, cnfExpressionVariables[i], to_string(-i-1).c_str()); + + fprintf(f, "cnfClauses:\n"); + for (auto &i1 : cnfClauses) { + for (auto &i2 : i1) + fprintf(f, " %4d", i2); + fprintf(f, "\n"); + } + if (cnfConsumed) + fprintf(f, " *** more clauses consumed via cnfConsume() ***\n"); + + fprintf(f, "--8<-- snap --8<--\n"); +} + +int ezSAT::onehot(const std::vector &vec, bool max_only) +{ + // Mixed one-hot/binary encoding as described by Claessen in Sec. 4.2 of + // "Successful SAT Encoding Techniques. Magnus Bjiirk. 25th July 2009". + // http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf + + std::vector formula; + + // add at-leat-one constraint + if (max_only == false) + formula.push_back(expression(OpOr, vec)); + + // create binary vector + int num_bits = ceil(log2(vec.size())); + std::vector bits; + for (int k = 0; k < num_bits; k++) + bits.push_back(literal()); + + // add at-most-one clauses using binary encoding + for (size_t i = 0; i < vec.size(); i++) + for (int k = 0; k < num_bits; k++) { + std::vector clause; + clause.push_back(NOT(vec[i])); + clause.push_back((i & (1 << k)) != 0 ? bits[k] : NOT(bits[k])); + formula.push_back(expression(OpOr, clause)); + } + + return expression(OpAnd, formula); +} + +int ezSAT::manyhot(const std::vector &vec, int min_hot, int max_hot) +{ + // many-hot encoding using a simple sorting network + + if (max_hot < 0) + max_hot = min_hot; + + std::vector formula; + int M = max_hot+1, N = vec.size(); + std::map, int> x; + + for (int i = -1; i < N; i++) + for (int j = -1; j < M; j++) + x[std::pair(i,j)] = j < 0 ? TRUE : i < 0 ? FALSE : literal(); + + for (int i = 0; i < N; i++) + for (int j = 0; j < M; j++) { + formula.push_back(OR(NOT(vec[i]), x[std::pair(i-1,j-1)], NOT(x[std::pair(i,j)]))); + formula.push_back(OR(NOT(vec[i]), NOT(x[std::pair(i-1,j-1)]), x[std::pair(i,j)])); + formula.push_back(OR(vec[i], x[std::pair(i-1,j)], NOT(x[std::pair(i,j)]))); + formula.push_back(OR(vec[i], NOT(x[std::pair(i-1,j)]), x[std::pair(i,j)])); +#if 0 + // explicit resolution clauses -- in tests it was better to let the sat solver figure those out + formula.push_back(OR(NOT(x[std::pair(i-1,j-1)]), NOT(x[std::pair(i-1,j)]), x[std::pair(i,j)])); + formula.push_back(OR(x[std::pair(i-1,j-1)], x[std::pair(i-1,j)], NOT(x[std::pair(i,j)]))); +#endif + } + + for (int j = 0; j < M; j++) { + if (j+1 <= min_hot) + formula.push_back(x[std::pair(N-1,j)]); + else if (j+1 > max_hot) + formula.push_back(NOT(x[std::pair(N-1,j)])); + } + + return expression(OpAnd, formula); +} + +int ezSAT::ordered(const std::vector &vec1, const std::vector &vec2, bool allow_equal) +{ + std::vector formula; + int last_x = FALSE; + + assert(vec1.size() == vec2.size()); + for (size_t i = 0; i < vec1.size(); i++) + { + int a = vec1[i], b = vec2[i]; + formula.push_back(OR(NOT(a), b, last_x)); + + int next_x = i+1 < vec1.size() ? literal() : allow_equal ? FALSE : TRUE; + formula.push_back(OR(a, b, last_x, NOT(next_x))); + formula.push_back(OR(NOT(a), NOT(b), last_x, NOT(next_x))); + last_x = next_x; + } + + return expression(OpAnd, formula); +} + diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h new file mode 100644 index 000000000..29b7aca71 --- /dev/null +++ b/libs/ezsat/ezsat.h @@ -0,0 +1,313 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#ifndef EZSAT_H +#define EZSAT_H + +#include +#include +#include +#include +#include + +class ezSAT +{ + // each token (terminal or non-terminal) is represented by an interger number + // + // the zero token: + // the number zero is not used as valid token number and is used to encode + // unused parameters for the functions. + // + // positive numbers are literals, with 1 = TRUE and 2 = FALSE; + // + // negative numbers are non-literal expressions. each expression is represented + // by an operator id and a list of expressions (literals or non-literals). + +public: + enum OpId { + OpNot, OpAnd, OpOr, OpXor, OpIFF, OpITE + }; + + const int TRUE = 1; + const int FALSE = 2; + +private: + std::map literalsCache; + std::vector literals; + + std::map>, int> expressionsCache; + std::vector>> expressions; + + bool cnfConsumed; + int cnfVariableCount; + std::vector cnfLiteralVariables, cnfExpressionVariables; + std::vector> cnfClauses; + std::set cnfAssumptions; + + void add_clause(const std::vector &args); + void add_clause(const std::vector &args, bool argsPolarity, int a = 0, int b = 0, int c = 0); + void add_clause(int a, int b = 0, int c = 0); + + int bind_cnf_not(const std::vector &args); + int bind_cnf_and(const std::vector &args); + int bind_cnf_or(const std::vector &args); + +public: + ezSAT(); + virtual ~ezSAT(); + + // manage expressions + + int value(bool val); + int literal(); + int literal(const std::string &name); + int expression(OpId op, int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0); + int expression(OpId op, const std::vector &args); + + void lookup_literal(int id, std::string &name) const; + const std::string &lookup_literal(int id) const; + + void lookup_expression(int id, OpId &op, std::vector &args) const; + const std::vector &lookup_expression(int id, OpId &op) const; + + int parse_string(const std::string &text); + std::string to_string(int id) const; + + int numLiterals() const { return literals.size(); } + int numExpressions() const { return expressions.size(); } + + int eval(int id, const std::vector &values) const; + + // SAT solver interface + // If you are planning on using the solver API (and not simply create a CNF) you must use a child class + // of ezSAT that actually implements a solver backend, such as ezMiniSAT (see ezminisat.h). + + virtual bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions); + + bool solve(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { + return solver(modelExpressions, modelValues, assumptions); + } + + bool solve(const std::vector &modelExpressions, std::vector &modelValues, int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) { + std::vector assumptions; + if (a != 0) assumptions.push_back(a); + if (b != 0) assumptions.push_back(b); + if (c != 0) assumptions.push_back(c); + if (d != 0) assumptions.push_back(d); + if (e != 0) assumptions.push_back(e); + if (f != 0) assumptions.push_back(f); + return solver(modelExpressions, modelValues, assumptions); + } + + bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) { + std::vector assumptions, modelExpressions; + std::vector modelValues; + if (a != 0) assumptions.push_back(a); + if (b != 0) assumptions.push_back(b); + if (c != 0) assumptions.push_back(c); + if (d != 0) assumptions.push_back(d); + if (e != 0) assumptions.push_back(e); + if (f != 0) assumptions.push_back(f); + return solver(modelExpressions, modelValues, assumptions); + } + + // manage CNF (usually only accessed by SAT solvers) + + virtual void clear(); + void assume(int id); + int bind(int id); + + const std::set &assumed() const { return cnfAssumptions; } + int bound(int id) const; + + int numCnfVariables() const { return cnfVariableCount; } + const std::vector> &cnf() const { return cnfClauses; } + + void consumeCnf(); + void consumeCnf(std::vector> &cnf); + + // simple helpers for build expressions easily + + struct _V { + int id; + std::string name; + _V(int id) : id(id) { } + _V(const char *name) : id(0), name(name) { } + _V(const std::string &name) : id(0), name(name) { } + int get(ezSAT *that) { + if (name.empty()) + return id; + return that->literal(name); + } + }; + + int VAR(_V a) { + return a.get(this); + } + + int NOT(_V a) { + return expression(OpNot, a.get(this)); + } + + int AND(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) { + return expression(OpAnd, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this)); + } + + int OR(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) { + return expression(OpOr, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this)); + } + + int XOR(_V a = 0, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) { + return expression(OpXor, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this)); + } + + int IFF(_V a, _V b = 0, _V c = 0, _V d = 0, _V e = 0, _V f = 0) { + return expression(OpIFF, a.get(this), b.get(this), c.get(this), d.get(this), e.get(this), f.get(this)); + } + + int ITE(_V a, _V b, _V c) { + return expression(OpITE, a.get(this), b.get(this), c.get(this)); + } + + void SET(_V a, _V b) { + assume(IFF(a.get(this), b.get(this))); + } + + // simple helpers for building expressions with bit vectors + + std::vector vec_const_signed(int64_t value, int bits); + std::vector vec_const_unsigned(uint64_t value, int bits); + std::vector vec_var(std::string name, int bits); + std::vector vec_cast(const std::vector &vec1, int toBits, bool signExtend = false); + + std::vector vec_not(const std::vector &vec1); + std::vector vec_and(const std::vector &vec1, const std::vector &vec2); + std::vector vec_or(const std::vector &vec1, const std::vector &vec2); + std::vector vec_xor(const std::vector &vec1, const std::vector &vec2); + + std::vector vec_iff(const std::vector &vec1, const std::vector &vec2); + std::vector vec_ite(const std::vector &vec1, const std::vector &vec2, const std::vector &vec3); + std::vector vec_ite(int sel, const std::vector &vec2, const std::vector &vec3); + + std::vector vec_count(const std::vector &vec, int bits, bool clip = true); + std::vector vec_add(const std::vector &vec1, const std::vector &vec2); + std::vector vec_sub(const std::vector &vec1, const std::vector &vec2); + + void vec_cmp(const std::vector &vec1, const std::vector &vec2, int &carry, int &overflow, int &sign, int &zero); + + int vec_lt_signed(const std::vector &vec1, const std::vector &vec2); + int vec_le_signed(const std::vector &vec1, const std::vector &vec2); + int vec_ge_signed(const std::vector &vec1, const std::vector &vec2); + int vec_gt_signed(const std::vector &vec1, const std::vector &vec2); + + int vec_lt_unsigned(const std::vector &vec1, const std::vector &vec2); + int vec_le_unsigned(const std::vector &vec1, const std::vector &vec2); + int vec_ge_unsigned(const std::vector &vec1, const std::vector &vec2); + int vec_gt_unsigned(const std::vector &vec1, const std::vector &vec2); + + int vec_eq(const std::vector &vec1, const std::vector &vec2); + int vec_ne(const std::vector &vec1, const std::vector &vec2); + + std::vector vec_shl(const std::vector &vec1, int shift, bool signExtend = false); + std::vector vec_srl(const std::vector &vec1, int shift); + + std::vector vec_shr(const std::vector &vec1, int shift, bool signExtend = false) { return vec_shl(vec1, -shift, signExtend); } + std::vector vec_srr(const std::vector &vec1, int shift) { return vec_srl(vec1, -shift); } + + void vec_append(std::vector &vec, const std::vector &vec1) const; + void vec_append_signed(std::vector &vec, const std::vector &vec1, int64_t value); + void vec_append_unsigned(std::vector &vec, const std::vector &vec1, uint64_t value); + + int64_t vec_model_get_signed(const std::vector &modelExpressions, const std::vector &modelValues, const std::vector &vec1) const; + uint64_t vec_model_get_unsigned(const std::vector &modelExpressions, const std::vector &modelValues, const std::vector &vec1) const; + + int vec_reduce_and(const std::vector &vec1); + int vec_reduce_or(const std::vector &vec1); + + void vec_set(const std::vector &vec1, const std::vector &vec2); + void vec_set_signed(const std::vector &vec1, int64_t value); + void vec_set_unsigned(const std::vector &vec1, uint64_t value); + + // helpers for generating ezSATbit and ezSATvec objects + + struct ezSATbit bit(_V a); + struct ezSATvec vec(const std::vector &vec); + + // printing CNF and internal state + + void printDIMACS(FILE *f, bool verbose = false) const; + void printInternalState(FILE *f) const; + + // more sophisticated constraints (designed to be used directly with assume(..)) + + int onehot(const std::vector &vec, bool max_only = false); + int manyhot(const std::vector &vec, int min_hot, int max_hot = -1); + int ordered(const std::vector &vec1, const std::vector &vec2, bool allow_equal = true); +}; + +// helper classes for using operator overloading when generating complex expressions + +struct ezSATbit +{ + ezSAT &sat; + int id; + + ezSATbit(ezSAT &sat, ezSAT::_V a) : sat(sat), id(sat.VAR(a)) { } + + ezSATbit operator ~() { return ezSATbit(sat, sat.NOT(id)); } + ezSATbit operator &(const ezSATbit &other) { return ezSATbit(sat, sat.AND(id, other.id)); } + ezSATbit operator |(const ezSATbit &other) { return ezSATbit(sat, sat.OR(id, other.id)); } + ezSATbit operator ^(const ezSATbit &other) { return ezSATbit(sat, sat.XOR(id, other.id)); } + ezSATbit operator ==(const ezSATbit &other) { return ezSATbit(sat, sat.IFF(id, other.id)); } + ezSATbit operator !=(const ezSATbit &other) { return ezSATbit(sat, sat.NOT(sat.IFF(id, other.id))); } + + operator int() const { return id; } + operator ezSAT::_V() const { return ezSAT::_V(id); } + operator std::vector() const { return std::vector(1, id); } +}; + +struct ezSATvec +{ + ezSAT &sat; + std::vector vec; + + ezSATvec(ezSAT &sat, const std::vector &vec) : sat(sat), vec(vec) { } + + ezSATvec operator ~() { return ezSATvec(sat, sat.vec_not(vec)); } + ezSATvec operator &(const ezSATvec &other) { return ezSATvec(sat, sat.vec_and(vec, other.vec)); } + ezSATvec operator |(const ezSATvec &other) { return ezSATvec(sat, sat.vec_or(vec, other.vec)); } + ezSATvec operator ^(const ezSATvec &other) { return ezSATvec(sat, sat.vec_xor(vec, other.vec)); } + + ezSATvec operator +(const ezSATvec &other) { return ezSATvec(sat, sat.vec_add(vec, other.vec)); } + ezSATvec operator -(const ezSATvec &other) { return ezSATvec(sat, sat.vec_sub(vec, other.vec)); } + + ezSATbit operator < (const ezSATvec &other) { return ezSATbit(sat, sat.vec_lt_unsigned(vec, other.vec)); } + ezSATbit operator <=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_le_unsigned(vec, other.vec)); } + ezSATbit operator ==(const ezSATvec &other) { return ezSATbit(sat, sat.vec_eq(vec, other.vec)); } + ezSATbit operator !=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_ne(vec, other.vec)); } + ezSATbit operator >=(const ezSATvec &other) { return ezSATbit(sat, sat.vec_ge_unsigned(vec, other.vec)); } + ezSATbit operator > (const ezSATvec &other) { return ezSATbit(sat, sat.vec_gt_unsigned(vec, other.vec)); } + + ezSATvec operator <<(int shift) { return ezSATvec(sat, sat.vec_shl(vec, shift)); } + ezSATvec operator >>(int shift) { return ezSATvec(sat, sat.vec_shr(vec, shift)); } + + operator std::vector() const { return vec; } +}; + +#endif diff --git a/libs/ezsat/puzzle3d.cc b/libs/ezsat/puzzle3d.cc new file mode 100644 index 000000000..1655e6972 --- /dev/null +++ b/libs/ezsat/puzzle3d.cc @@ -0,0 +1,293 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "ezminisat.h" +#include +#include + +#define DIM_X 5 +#define DIM_Y 5 +#define DIM_Z 5 + +#define NUM_124 6 +#define NUM_223 6 + +ezMiniSAT ez; +int blockidx = 0; +std::map blockinfo; +std::vector grid[DIM_X][DIM_Y][DIM_Z]; + +struct blockgeom_t +{ + int center_x, center_y, center_z; + int size_x, size_y, size_z; + int var; + + void mirror_x() { center_x *= -1; } + void mirror_y() { center_y *= -1; } + void mirror_z() { center_z *= -1; } + + void rotate_x() { int tmp[4] = { center_y, center_z, size_y, size_z }; center_y = tmp[1]; center_z = -tmp[0]; size_y = tmp[3]; size_z = tmp[2]; } + void rotate_y() { int tmp[4] = { center_x, center_z, size_x, size_z }; center_x = tmp[1]; center_z = -tmp[0]; size_x = tmp[3]; size_z = tmp[2]; } + void rotate_z() { int tmp[4] = { center_x, center_y, size_x, size_y }; center_x = tmp[1]; center_y = -tmp[0]; size_x = tmp[3]; size_y = tmp[2]; } + + bool operator< (const blockgeom_t &other) const { + if (center_x != other.center_x) return center_x < other.center_x; + if (center_y != other.center_y) return center_y < other.center_y; + if (center_z != other.center_z) return center_z < other.center_z; + if (size_x != other.size_x) return size_x < other.size_x; + if (size_y != other.size_y) return size_y < other.size_y; + if (size_z != other.size_z) return size_z < other.size_z; + if (var != other.var) return var < other.var; + return false; + } +}; + +// geometry data for spatial symmetry constraints +std::set blockgeom; + +int add_block(int pos_x, int pos_y, int pos_z, int size_x, int size_y, int size_z, int blockidx) +{ + char buffer[1024]; + snprintf(buffer, 1024, "block(%d,%d,%d,%d,%d,%d,%d);", size_x, size_y, size_z, pos_x, pos_y, pos_z, blockidx); + + int var = ez.literal(); + blockinfo[var] = buffer; + + for (int ix = pos_x; ix < pos_x+size_x; ix++) + for (int iy = pos_y; iy < pos_y+size_y; iy++) + for (int iz = pos_z; iz < pos_z+size_z; iz++) + grid[ix][iy][iz].push_back(var); + + blockgeom_t bg; + bg.size_x = 2*size_x; + bg.size_y = 2*size_y; + bg.size_z = 2*size_z; + bg.center_x = (2*pos_x + size_x) - DIM_X; + bg.center_y = (2*pos_y + size_y) - DIM_Y; + bg.center_z = (2*pos_z + size_z) - DIM_Z; + bg.var = var; + + assert(blockgeom.count(bg) == 0); + blockgeom.insert(bg); + + return var; +} + +void add_block_positions_124(std::vector &block_positions_124) +{ + block_positions_124.clear(); + for (int size_x = 1; size_x <= 4; size_x *= 2) + for (int size_y = 1; size_y <= 4; size_y *= 2) + for (int size_z = 1; size_z <= 4; size_z *= 2) { + if (size_x == size_y || size_y == size_z || size_z == size_x) + continue; + for (int ix = 0; ix <= DIM_X-size_x; ix++) + for (int iy = 0; iy <= DIM_Y-size_y; iy++) + for (int iz = 0; iz <= DIM_Z-size_z; iz++) + block_positions_124.push_back(add_block(ix, iy, iz, size_x, size_y, size_z, blockidx++)); + } +} + +void add_block_positions_223(std::vector &block_positions_223) +{ + block_positions_223.clear(); + for (int orientation = 0; orientation < 3; orientation++) { + int size_x = orientation == 0 ? 3 : 2; + int size_y = orientation == 1 ? 3 : 2; + int size_z = orientation == 2 ? 3 : 2; + for (int ix = 0; ix <= DIM_X-size_x; ix++) + for (int iy = 0; iy <= DIM_Y-size_y; iy++) + for (int iz = 0; iz <= DIM_Z-size_z; iz++) + block_positions_223.push_back(add_block(ix, iy, iz, size_x, size_y, size_z, blockidx++)); + } +} + +// use simple built-in random number generator to +// ensure determinism of the program across platforms +uint32_t xorshift32() { + static uint32_t x = 314159265; + x ^= x << 13; + x ^= x >> 17; + x ^= x << 5; + return x; +} + +void condense_exclusives(std::vector &vars) +{ + std::map> exclusive; + + for (int ix = 0; ix < DIM_X; ix++) + for (int iy = 0; iy < DIM_Y; iy++) + for (int iz = 0; iz < DIM_Z; iz++) { + for (int a : grid[ix][iy][iz]) + for (int b : grid[ix][iy][iz]) + if (a != b) + exclusive[a].insert(b); + } + + std::vector> pools; + + for (int a : vars) + { + std::vector candidate_pools; + for (size_t i = 0; i < pools.size(); i++) + { + for (int b : pools[i]) + if (exclusive[a].count(b) == 0) + goto no_candidate_pool; + candidate_pools.push_back(i); + no_candidate_pool:; + } + + if (candidate_pools.size() > 0) { + int p = candidate_pools[xorshift32() % candidate_pools.size()]; + pools[p].push_back(a); + } else { + pools.push_back(std::vector()); + pools.back().push_back(a); + } + } + + std::vector new_vars; + for (auto &pool : pools) + { + std::vector formula; + int var = ez.literal(); + + for (int a : pool) + formula.push_back(ez.OR(ez.NOT(a), var)); + formula.push_back(ez.OR(ez.expression(ezSAT::OpOr, pool), ez.NOT(var))); + + ez.assume(ez.onehot(pool, true)); + ez.assume(ez.expression(ezSAT::OpAnd, formula)); + new_vars.push_back(var); + } + + printf("Condensed %d variables into %d one-hot pools.\n", int(vars.size()), int(new_vars.size())); + vars.swap(new_vars); +} + +int main() +{ + printf("\nCreating SAT encoding..\n"); + + // add 1x2x4 blocks + std::vector block_positions_124; + add_block_positions_124(block_positions_124); + condense_exclusives(block_positions_124); + ez.assume(ez.manyhot(block_positions_124, NUM_124)); + + // add 2x2x3 blocks + std::vector block_positions_223; + add_block_positions_223(block_positions_223); + condense_exclusives(block_positions_223); + ez.assume(ez.manyhot(block_positions_223, NUM_223)); + + // add constraint for max one block per grid element + for (int ix = 0; ix < DIM_X; ix++) + for (int iy = 0; iy < DIM_Y; iy++) + for (int iz = 0; iz < DIM_Z; iz++) { + assert(grid[ix][iy][iz].size() > 0); + ez.assume(ez.onehot(grid[ix][iy][iz], true)); + } + + printf("Found %d possible block positions.\n", int(blockgeom.size())); + + // look for spatial symmetries + std::set> symmetries; + symmetries.insert(blockgeom); + bool keep_running = true; + while (keep_running) { + keep_running = false; + std::set> old_sym; + old_sym.swap(symmetries); + for (auto &old_sym_set : old_sym) + { + std::set mx, my, mz; + std::set rx, ry, rz; + for (auto &bg : old_sym_set) { + blockgeom_t bg_mx = bg, bg_my = bg, bg_mz = bg; + blockgeom_t bg_rx = bg, bg_ry = bg, bg_rz = bg; + bg_mx.mirror_x(), bg_my.mirror_y(), bg_mz.mirror_z(); + bg_rx.rotate_x(), bg_ry.rotate_y(), bg_rz.rotate_z(); + mx.insert(bg_mx), my.insert(bg_my), mz.insert(bg_mz); + rx.insert(bg_rx), ry.insert(bg_ry), rz.insert(bg_rz); + } + if (!old_sym.count(mx) || !old_sym.count(my) || !old_sym.count(mz) || + !old_sym.count(rx) || !old_sym.count(ry) || !old_sym.count(rz)) + keep_running = true; + symmetries.insert(old_sym_set); + symmetries.insert(mx); + symmetries.insert(my); + symmetries.insert(mz); + symmetries.insert(rx); + symmetries.insert(ry); + symmetries.insert(rz); + } + } + + // add constraints to eliminate all the spatial symmetries + std::vector> vecvec; + for (auto &sym : symmetries) { + std::vector vec; + for (auto &bg : sym) + vec.push_back(bg.var); + vecvec.push_back(vec); + } + for (size_t i = 1; i < vecvec.size(); i++) + ez.assume(ez.ordered(vecvec[0], vecvec[1])); + + printf("Found and eliminated %d spatial symmetries.\n", int(symmetries.size())); + printf("Generated %d clauses over %d variables.\n", ez.numCnfVariables(), int(ez.cnf().size())); + + std::vector modelExpressions; + std::vector modelValues; + + for (auto &it : blockinfo) + modelExpressions.push_back(it.first); + + int solution_counter = 0; + while (1) + { + printf("\nSolving puzzle..\n"); + bool ok = ez.solve(modelExpressions, modelValues); + + if (!ok) { + printf("No more solutions found!\n"); + break; + } + + printf("Puzzle solution:\n"); + std::vector constraint; + for (size_t i = 0; i < modelExpressions.size(); i++) + if (modelValues[i]) { + constraint.push_back(ez.NOT(modelExpressions[i])); + printf("%s\n", blockinfo.at(modelExpressions[i]).c_str()); + } + ez.assume(ez.expression(ezSAT::OpOr, constraint)); + solution_counter++; + } + + printf("\nFound %d distinct solutions.\n", solution_counter); + printf("Have a nice day.\n\n"); + + return 0; +} + diff --git a/libs/ezsat/puzzle3d.scad b/libs/ezsat/puzzle3d.scad new file mode 100644 index 000000000..693f8d853 --- /dev/null +++ b/libs/ezsat/puzzle3d.scad @@ -0,0 +1,82 @@ + +gap = 30; +layers = 0; +variant = 1; + +module block(size_x, size_y, size_z, pos_x, pos_y, pos_z, idx) +{ + col = idx % 6 == 0 ? [ 0, 0, 1 ] : + idx % 6 == 1 ? [ 0, 1, 0 ] : + idx % 6 == 2 ? [ 0, 1, 1 ] : + idx % 6 == 3 ? [ 1, 0, 0 ] : + idx % 6 == 4 ? [ 1, 0, 1 ] : + idx % 6 == 5 ? [ 1, 1, 0 ] : [ 0, 0, 0 ]; + translate([-2.5, -2.5, 0] * (100+gap)) difference() { + color(col) translate([pos_x, pos_y, pos_z] * (100 + gap)) + cube([size_x, size_y, size_z] * (100+gap) - [gap, gap, gap], false); + if (layers > 0) + color([0.3, 0.3, 0.3]) translate([0, 0, layers * (100+gap)] - [0.5, 0.5, 0.5] * gap) + cube([5, 5, 5] * (100 + gap), false); + } +} + +if (variant == 1) { + block(1,4,2,0,1,3,47); + block(1,4,2,4,0,0,72); + block(2,1,4,0,0,0,80); + block(2,1,4,3,4,1,119); + block(4,2,1,0,3,0,215); + block(4,2,1,1,0,4,224); + block(3,2,2,0,3,1,253); + block(3,2,2,2,0,2,274); + block(2,3,2,1,2,3,311); + block(2,3,2,2,0,0,312); + block(2,2,3,0,1,0,339); + block(2,2,3,3,2,2,380); +} + +if (variant == 2) { + block(1,2,4,0,0,1,1); + block(1,2,4,4,3,0,38); + block(2,4,1,0,1,0,125); + block(2,4,1,3,0,4,154); + block(4,1,2,0,4,3,179); + block(4,1,2,1,0,0,180); + block(3,2,2,0,2,3,251); + block(3,2,2,2,1,0,276); + block(2,3,2,0,2,1,297); + block(2,3,2,3,0,2,326); + block(2,2,3,1,0,2,350); + block(2,2,3,2,3,0,369); +} + +if (variant == 3) { + block(1,4,2,0,0,3,43); + block(1,4,2,4,1,0,76); + block(2,1,4,0,4,0,88); + block(2,1,4,3,0,1,111); + block(4,2,1,0,0,0,200); + block(4,2,1,1,3,4,239); + block(3,2,2,0,0,1,241); + block(3,2,2,2,3,2,286); + block(2,3,2,1,0,3,303); + block(2,3,2,2,2,0,320); + block(2,2,3,0,2,0,342); + block(2,2,3,3,1,2,377); +} + +if (variant == 4) { + block(1,2,4,0,3,1,7); + block(1,2,4,4,0,0,32); + block(2,4,1,0,0,0,120); + block(2,4,1,3,1,4,159); + block(4,1,2,0,0,3,163); + block(4,1,2,1,4,0,196); + block(3,2,2,0,1,3,247); + block(3,2,2,2,2,0,280); + block(2,3,2,0,0,1,289); + block(2,3,2,3,2,2,334); + block(2,2,3,1,3,2,359); + block(2,2,3,2,0,0,360); +} + diff --git a/libs/ezsat/testbench.cc b/libs/ezsat/testbench.cc new file mode 100644 index 000000000..cc0fe5734 --- /dev/null +++ b/libs/ezsat/testbench.cc @@ -0,0 +1,524 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Clifford Wolf + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "ezminisat.h" +#include + +struct xorshift128 { + uint32_t x, y, z, w; + xorshift128() { + x = 123456789; + y = 362436069; + z = 521288629; + w = 88675123; + } + uint32_t operator()() { + uint32_t t = x ^ (x << 11); + x = y; y = z; z = w; + w ^= (w >> 19) ^ t ^ (t >> 8); + return w; + } +}; + +bool test(ezSAT &sat, int assumption = 0) +{ + for (auto id : sat.assumed()) + printf("%s\n", sat.to_string(id).c_str()); + if (assumption) + printf("%s\n", sat.to_string(assumption).c_str()); + + std::vector modelExpressions; + std::vector modelValues; + + for (int id = 1; id <= sat.numLiterals(); id++) + if (sat.bound(id)) + modelExpressions.push_back(id); + + if (sat.solve(modelExpressions, modelValues, assumption)) { + printf("satisfiable:"); + for (int i = 0; i < int(modelExpressions.size()); i++) + printf(" %s=%d", sat.to_string(modelExpressions[i]).c_str(), int(modelValues[i])); + printf("\n\n"); + return true; + } else { + printf("not satisfiable.\n\n"); + return false; + } +} + +// ------------------------------------------------------------------------------------------------------------ + +void test_simple() +{ + printf("==== %s ====\n\n", __PRETTY_FUNCTION__); + + ezSAT sat; + sat.assume(sat.OR("A", "B")); + sat.assume(sat.NOT(sat.AND("A", "B"))); + test(sat); +} + +// ------------------------------------------------------------------------------------------------------------ + +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; + output_pattern ^= output_pattern << 13; + output_pattern ^= output_pattern >> 17; + output_pattern ^= output_pattern << 5; + + std::vector modelExpressions; + std::vector forwardAssumptions, backwardAssumptions; + std::vector forwardModel, backwardModel; + + sat.vec_append(modelExpressions, sat.vec_var("i", 32)); + sat.vec_append(modelExpressions, sat.vec_var("o", 32)); + + sat.vec_append_unsigned(forwardAssumptions, sat.vec_var("i", 32), input_pattern); + sat.vec_append_unsigned(backwardAssumptions, sat.vec_var("o", 32), output_pattern); + + if (!sat.solve(modelExpressions, backwardModel, backwardAssumptions)) { + printf("backward solving failed!\n"); + abort(); + } + + if (!sat.solve(modelExpressions, forwardModel, forwardAssumptions)) { + printf("forward solving failed!\n"); + abort(); + } + + printf("xorshift32 test with input pattern 0x%08x:\n", input_pattern); + + printf("forward solution: input=0x%08x output=0x%08x\n", + (unsigned int)sat.vec_model_get_unsigned(modelExpressions, forwardModel, sat.vec_var("i", 32)), + (unsigned int)sat.vec_model_get_unsigned(modelExpressions, forwardModel, sat.vec_var("o", 32))); + + printf("backward solution: input=0x%08x output=0x%08x\n", + (unsigned int)sat.vec_model_get_unsigned(modelExpressions, backwardModel, sat.vec_var("i", 32)), + (unsigned int)sat.vec_model_get_unsigned(modelExpressions, backwardModel, sat.vec_var("o", 32))); + + if (forwardModel != backwardModel) { + printf("forward and backward results are inconsistend!\n"); + abort(); + } + + printf("passed.\n\n"); +} + +void test_xorshift32() +{ + printf("==== %s ====\n\n", __PRETTY_FUNCTION__); + + ezMiniSAT sat; + xorshift128 rng; + + std::vector bits = sat.vec_var("i", 32); + + bits = sat.vec_xor(bits, sat.vec_shl(bits, 13)); + bits = sat.vec_xor(bits, sat.vec_shr(bits, 17)); + bits = sat.vec_xor(bits, sat.vec_shl(bits, 5)); + + sat.vec_set(bits, sat.vec_var("o", 32)); + + test_xorshift32_try(sat, 0); + test_xorshift32_try(sat, 314159265); + test_xorshift32_try(sat, rng()); + test_xorshift32_try(sat, rng()); + test_xorshift32_try(sat, rng()); + test_xorshift32_try(sat, rng()); +} + +// ------------------------------------------------------------------------------------------------------------ + +#define CHECK(_expr1, _expr2) check(#_expr1, _expr1, #_expr2, _expr2) + +void check(const char *expr1_str, bool expr1, const char *expr2_str, bool expr2) +{ + if (expr1 == expr2) { + printf("[ %s ] == [ %s ] .. ok (%s == %s)\n", expr1_str, expr2_str, expr1 ? "true" : "false", expr2 ? "true" : "false"); + } else { + printf("[ %s ] != [ %s ] .. ERROR (%s != %s)\n", expr1_str, expr2_str, expr1 ? "true" : "false", expr2 ? "true" : "false"); + abort(); + } +} + +void test_signed(int8_t a, int8_t b, int8_t c) +{ + ezSAT sat; + + std::vector av = sat.vec_const_signed(a, 8); + std::vector bv = sat.vec_const_signed(b, 8); + std::vector cv = sat.vec_const_signed(c, 8); + + printf("Testing signed arithmetic using: a=%+d, b=%+d, c=%+d\n", int(a), int(b), int(c)); + + CHECK(a < b+c, sat.solve(sat.vec_lt_signed(av, sat.vec_add(bv, cv)))); + CHECK(a <= b-c, sat.solve(sat.vec_le_signed(av, sat.vec_sub(bv, cv)))); + + CHECK(a > b+c, sat.solve(sat.vec_gt_signed(av, sat.vec_add(bv, cv)))); + CHECK(a >= b-c, sat.solve(sat.vec_ge_signed(av, sat.vec_sub(bv, cv)))); + + printf("\n"); +} + +void test_unsigned(uint8_t a, uint8_t b, uint8_t c) +{ + ezSAT sat; + + if (b < c) + b ^= c, c ^= b, b ^= c; + + std::vector av = sat.vec_const_unsigned(a, 8); + std::vector bv = sat.vec_const_unsigned(b, 8); + std::vector cv = sat.vec_const_unsigned(c, 8); + + printf("Testing unsigned arithmetic using: a=%d, b=%d, c=%d\n", int(a), int(b), int(c)); + + CHECK(a < b+c, sat.solve(sat.vec_lt_unsigned(av, sat.vec_add(bv, cv)))); + CHECK(a <= b-c, sat.solve(sat.vec_le_unsigned(av, sat.vec_sub(bv, cv)))); + + CHECK(a > b+c, sat.solve(sat.vec_gt_unsigned(av, sat.vec_add(bv, cv)))); + CHECK(a >= b-c, sat.solve(sat.vec_ge_unsigned(av, sat.vec_sub(bv, cv)))); + + printf("\n"); +} + +void test_count(uint32_t x) +{ + ezSAT sat; + + int count = 0; + for (int i = 0; i < 32; i++) + if (((x >> i) & 1) != 0) + count++; + + printf("Testing bit counting using x=0x%08x (%d set bits) .. ", x, count); + + std::vector v = sat.vec_const_unsigned(x, 32); + + std::vector cv6 = sat.vec_const_unsigned(count, 6); + std::vector cv4 = sat.vec_const_unsigned(count <= 15 ? count : 15, 4); + + if (cv6 != sat.vec_count(v, 6, false)) { + fprintf(stderr, "FAILED 6bit-no-clipping test!\n"); + abort(); + } + + if (cv4 != sat.vec_count(v, 4, true)) { + fprintf(stderr, "FAILED 4bit-clipping test!\n"); + abort(); + } + + printf("ok.\n"); +} + +void test_arith() +{ + printf("==== %s ====\n\n", __PRETTY_FUNCTION__); + + xorshift128 rng; + + for (int i = 0; i < 100; i++) + test_signed(rng() % 19 - 10, rng() % 19 - 10, rng() % 19 - 10); + + for (int i = 0; i < 100; i++) + test_unsigned(rng() % 10, rng() % 10, rng() % 10); + + test_count(0x00000000); + test_count(0xffffffff); + for (int i = 0; i < 30; i++) + test_count(rng()); + + printf("\n"); +} + +// ------------------------------------------------------------------------------------------------------------ + +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"); + + std::vector abcd; + abcd.push_back(a); + abcd.push_back(b); + abcd.push_back(c); + abcd.push_back(d); + + ez.assume(ez.onehot(abcd)); + + int solution_counter = 0; + while (1) + { + std::vector modelValues; + bool ok = ez.solve(abcd, modelValues); + + if (!ok) + break; + + printf("Solution: %d %d %d %d\n", int(modelValues[0]), int(modelValues[1]), int(modelValues[2]), int(modelValues[3])); + + int count_hot = 0; + std::vector sol; + for (int i = 0; i < 4; i++) { + if (modelValues[i]) + count_hot++; + sol.push_back(modelValues[i] ? abcd[i] : ez.NOT(abcd[i])); + } + ez.assume(ez.NOT(ez.expression(ezSAT::OpAnd, sol))); + + if (count_hot != 1) { + fprintf(stderr, "Wrong number of hot bits!\n"); + abort(); + } + + solution_counter++; + } + + if (solution_counter != 4) { + fprintf(stderr, "Wrong number of one-hot solutions!\n"); + abort(); + } + + printf("\n"); +} + +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"); + + std::vector abcd; + abcd.push_back(a); + abcd.push_back(b); + abcd.push_back(c); + abcd.push_back(d); + + ez.assume(ez.manyhot(abcd, 1, 2)); + + int solution_counter = 0; + while (1) + { + std::vector modelValues; + bool ok = ez.solve(abcd, modelValues); + + if (!ok) + break; + + printf("Solution: %d %d %d %d\n", int(modelValues[0]), int(modelValues[1]), int(modelValues[2]), int(modelValues[3])); + + int count_hot = 0; + std::vector sol; + for (int i = 0; i < 4; i++) { + if (modelValues[i]) + count_hot++; + sol.push_back(modelValues[i] ? abcd[i] : ez.NOT(abcd[i])); + } + ez.assume(ez.NOT(ez.expression(ezSAT::OpAnd, sol))); + + if (count_hot != 1 && count_hot != 2) { + fprintf(stderr, "Wrong number of hot bits!\n"); + abort(); + } + + solution_counter++; + } + + if (solution_counter != 4 + 4*3/2) { + fprintf(stderr, "Wrong number of one-hot solutions!\n"); + abort(); + } + + printf("\n"); +} + +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 x = ez.literal("x"); + int y = ez.literal("y"); + int z = ez.literal("z"); + + std::vector abc; + abc.push_back(a); + abc.push_back(b); + abc.push_back(c); + + std::vector xyz; + xyz.push_back(x); + xyz.push_back(y); + xyz.push_back(z); + + ez.assume(ez.ordered(abc, xyz)); + + int solution_counter = 0; + + while (1) + { + std::vector modelVariables; + std::vector modelValues; + + modelVariables.push_back(a); + modelVariables.push_back(b); + modelVariables.push_back(c); + + modelVariables.push_back(x); + modelVariables.push_back(y); + modelVariables.push_back(z); + + bool ok = ez.solve(modelVariables, modelValues); + + if (!ok) + break; + + printf("Solution: %d %d %d | %d %d %d\n", + int(modelValues[0]), int(modelValues[1]), int(modelValues[2]), + int(modelValues[3]), int(modelValues[4]), int(modelValues[5])); + + std::vector sol; + for (size_t i = 0; i < modelVariables.size(); i++) + sol.push_back(modelValues[i] ? modelVariables[i] : ez.NOT(modelVariables[i])); + ez.assume(ez.NOT(ez.expression(ezSAT::OpAnd, sol))); + + solution_counter++; + } + + if (solution_counter != 8+7+6+5+4+3+2+1) { + fprintf(stderr, "Wrong number of solutions!\n"); + abort(); + } + + printf("\n"); +} + +// ------------------------------------------------------------------------------------------------------------ + + +int main() +{ + test_simple(); + test_basic_operators(); + test_xorshift32(); + test_arith(); + test_onehot(); + test_manyhot(); + test_ordered(); + printf("Passed all tests.\n\n"); + return 0; +} + -- 2.30.2