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
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
--- /dev/null
+
+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
+
--- /dev/null
+
+ **************************************************************************
+ * *
+ * 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.
+
--- /dev/null
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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 <stdio.h>
+
+void print_results(bool satisfiable, const std::vector<bool> &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<int> modelVars;
+ std::vector<bool> 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;
+}
+
--- /dev/null
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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 <assert.h>
+
+#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<int> &x, std::vector<int> &y, std::vector<int> &z, std::vector<int> &w)
+{
+ std::vector<int> 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<int> vx = sat.vec_var("x", 32);
+ std::vector<int> vy = sat.vec_var("y", 32);
+ std::vector<int> vz = sat.vec_var("z", 32);
+ std::vector<int> 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<int> modelExpressions;
+ std::vector<bool> 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;
+}
+
--- /dev/null
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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 <limits.h>
+#include <stdint.h>
+#include <cinttypes>
+
+#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<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
+{
+ if (0) {
+contradiction:
+ delete minisatSolver;
+ minisatSolver = NULL;
+ minisatVars.clear();
+ foundContradiction = true;
+ return false;
+ }
+
+ if (foundContradiction) {
+ consumeCnf();
+ return false;
+ }
+
+ std::vector<int> 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<std::vector<int>> cnf;
+ consumeCnf(cnf);
+
+ while (int(minisatVars.size()) < numCnfVariables())
+ minisatVars.push_back(minisatSolver->newVar());
+
+ for (auto &clause : cnf) {
+ Minisat::vec<Minisat::Lit> 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<Minisat::Lit> 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;
+}
+
--- /dev/null
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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<int> minisatVars;
+ bool foundContradiction;
+
+public:
+ ezMiniSAT();
+ virtual ~ezMiniSAT();
+ virtual void clear();
+ virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
+};
+
+#endif
--- /dev/null
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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 <algorithm>
+
+#include <stdlib.h>
+#include <assert.h>
+
+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<int> 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<int> &args)
+{
+ std::vector<int> 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<OpId, std::vector<int>> 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<int> &args) const
+{
+ assert(0 < -id && -id <= int(expressions.size()));
+ op = expressions[-id - 1].first;
+ args = expressions[-id - 1].second;
+}
+
+const std::vector<int> &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<int> 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<int> &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<int> &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<int>(1, idx));
+ cnfAssumptions.insert(id);
+}
+
+void ezSAT::add_clause(const std::vector<int> &args)
+{
+ cnfClauses.push_back(args);
+}
+
+void ezSAT::add_clause(const std::vector<int> &args, bool argsPolarity, int a, int b, int c)
+{
+ std::vector<int> 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<int> 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<int> &args)
+{
+ assert(args.size() == 1);
+ return -args[0];
+}
+
+int ezSAT::bind_cnf_and(const std::vector<int> &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<int> &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<int> args;
+ lookup_expression(id, op, args);
+ int idx = 0;
+
+ if (op == OpXor) {
+ while (args.size() > 1) {
+ std::vector<int> 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<int> 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<std::vector<int>> &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<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
+{
+ std::vector<int> extraClauses, modelIdx;
+ std::vector<int> 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<int> ezSAT::vec_const_signed(int64_t value, int bits)
+{
+ std::vector<int> vec;
+ for (int i = 0; i < bits; i++)
+ vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE);
+ return vec;
+}
+
+std::vector<int> ezSAT::vec_const_unsigned(uint64_t value, int bits)
+{
+ std::vector<int> vec;
+ for (int i = 0; i < bits; i++)
+ vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE);
+ return vec;
+}
+
+std::vector<int> ezSAT::vec_var(std::string name, int bits)
+{
+ std::vector<int> vec;
+ for (int i = 0; i < bits; i++)
+ vec.push_back(VAR(name + "[" + std::to_string(i) + "]"));
+ return vec;
+}
+
+std::vector<int> ezSAT::vec_cast(const std::vector<int> &vec1, int toBits, bool signExtend)
+{
+ std::vector<int> 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<int> ezSAT::vec_not(const std::vector<int> &vec1)
+{
+ std::vector<int> vec;
+ for (auto bit : vec1)
+ vec.push_back(NOT(bit));
+ return vec;
+}
+
+std::vector<int> ezSAT::vec_and(const std::vector<int> &vec1, const std::vector<int> &vec2)
+{
+ assert(vec1.size() == vec2.size());
+ std::vector<int> vec(vec1.size());
+ for (int i = 0; i < int(vec1.size()); i++)
+ vec[i] = AND(vec1[i], vec2[i]);
+ return vec;
+}
+
+std::vector<int> ezSAT::vec_or(const std::vector<int> &vec1, const std::vector<int> &vec2)
+{
+ assert(vec1.size() == vec2.size());
+ std::vector<int> vec(vec1.size());
+ for (int i = 0; i < int(vec1.size()); i++)
+ vec[i] = OR(vec1[i], vec2[i]);
+ return vec;
+}
+
+std::vector<int> ezSAT::vec_xor(const std::vector<int> &vec1, const std::vector<int> &vec2)
+{
+ assert(vec1.size() == vec2.size());
+ std::vector<int> vec(vec1.size());
+ for (int i = 0; i < int(vec1.size()); i++)
+ vec[i] = XOR(vec1[i], vec2[i]);
+ return vec;
+}
+
+std::vector<int> ezSAT::vec_iff(const std::vector<int> &vec1, const std::vector<int> &vec2)
+{
+ assert(vec1.size() == vec2.size());
+ std::vector<int> vec(vec1.size());
+ for (int i = 0; i < int(vec1.size()); i++)
+ vec[i] = IFF(vec1[i], vec2[i]);
+ return vec;
+}
+
+std::vector<int> ezSAT::vec_ite(const std::vector<int> &vec1, const std::vector<int> &vec2, const std::vector<int> &vec3)
+{
+ assert(vec1.size() == vec2.size() && vec2.size() == vec3.size());
+ std::vector<int> 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<int> ezSAT::vec_ite(int sel, const std::vector<int> &vec1, const std::vector<int> &vec2)
+{
+ assert(vec1.size() == vec2.size());
+ std::vector<int> 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<int> ezSAT::vec_count(const std::vector<int> &vec, int bits, bool clip)
+{
+ std::vector<int> sum = vec_const_unsigned(0, bits);
+ std::vector<int> 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<int> ezSAT::vec_add(const std::vector<int> &vec1, const std::vector<int> &vec2)
+{
+ assert(vec1.size() == vec2.size());
+ std::vector<int> 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<int> ezSAT::vec_sub(const std::vector<int> &vec1, const std::vector<int> &vec2)
+{
+ assert(vec1.size() == vec2.size());
+ std::vector<int> 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<int> &vec1, const std::vector<int> &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<int> &vec1, const std::vector<int> &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<int> &vec1, const std::vector<int> &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<int> &vec1, const std::vector<int> &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<int> &vec1, const std::vector<int> &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<int> &vec1, const std::vector<int> &vec2)
+{
+ int carry, overflow, sign, zero;
+ vec_cmp(vec1, vec2, carry, overflow, sign, zero);
+ return carry;
+}
+
+int ezSAT::vec_le_unsigned(const std::vector<int> &vec1, const std::vector<int> &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<int> &vec1, const std::vector<int> &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<int> &vec1, const std::vector<int> &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<int> &vec1, const std::vector<int> &vec2)
+{
+ return vec_reduce_and(vec_iff(vec1, vec2));
+}
+
+int ezSAT::vec_ne(const std::vector<int> &vec1, const std::vector<int> &vec2)
+{
+ return NOT(vec_reduce_and(vec_iff(vec1, vec2)));
+}
+
+std::vector<int> ezSAT::vec_shl(const std::vector<int> &vec1, int shift, bool signExtend)
+{
+ std::vector<int> 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<int> ezSAT::vec_srl(const std::vector<int> &vec1, int shift)
+{
+ std::vector<int> 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<int> &vec, const std::vector<int> &vec1) const
+{
+ for (auto bit : vec1)
+ vec.push_back(bit);
+}
+
+void ezSAT::vec_append_signed(std::vector<int> &vec, const std::vector<int> &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<int> &vec, const std::vector<int> &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<int> &modelExpressions, const std::vector<bool> &modelValues, const std::vector<int> &vec1) const
+{
+ int64_t value = 0;
+ std::map<int, bool> 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<int> &modelExpressions, const std::vector<bool> &modelValues, const std::vector<int> &vec1) const
+{
+ uint64_t value = 0;
+ std::map<int, bool> 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<int> &vec1)
+{
+ return expression(OpAnd, vec1);
+}
+
+int ezSAT::vec_reduce_or(const std::vector<int> &vec1)
+{
+ return expression(OpOr, vec1);
+}
+
+void ezSAT::vec_set(const std::vector<int> &vec1, const std::vector<int> &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<int> &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<int> &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<int> &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<ezSAT::OpId, std::vector<int>> &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<int> &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<int> 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<int> 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<int> 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<int> &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<int> formula;
+ int M = max_hot+1, N = vec.size();
+ std::map<std::pair<int,int>, int> x;
+
+ for (int i = -1; i < N; i++)
+ for (int j = -1; j < M; j++)
+ x[std::pair<int,int>(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<int,int>(i-1,j-1)], NOT(x[std::pair<int,int>(i,j)])));
+ formula.push_back(OR(NOT(vec[i]), NOT(x[std::pair<int,int>(i-1,j-1)]), x[std::pair<int,int>(i,j)]));
+ formula.push_back(OR(vec[i], x[std::pair<int,int>(i-1,j)], NOT(x[std::pair<int,int>(i,j)])));
+ formula.push_back(OR(vec[i], NOT(x[std::pair<int,int>(i-1,j)]), x[std::pair<int,int>(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<int,int>(i-1,j-1)]), NOT(x[std::pair<int,int>(i-1,j)]), x[std::pair<int,int>(i,j)]));
+ formula.push_back(OR(x[std::pair<int,int>(i-1,j-1)], x[std::pair<int,int>(i-1,j)], NOT(x[std::pair<int,int>(i,j)])));
+#endif
+ }
+
+ for (int j = 0; j < M; j++) {
+ if (j+1 <= min_hot)
+ formula.push_back(x[std::pair<int,int>(N-1,j)]);
+ else if (j+1 > max_hot)
+ formula.push_back(NOT(x[std::pair<int,int>(N-1,j)]));
+ }
+
+ return expression(OpAnd, formula);
+}
+
+int ezSAT::ordered(const std::vector<int> &vec1, const std::vector<int> &vec2, bool allow_equal)
+{
+ std::vector<int> 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);
+}
+
--- /dev/null
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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 <set>
+#include <map>
+#include <vector>
+#include <string>
+#include <stdio.h>
+
+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<std::string, int> literalsCache;
+ std::vector<std::string> literals;
+
+ std::map<std::pair<OpId, std::vector<int>>, int> expressionsCache;
+ std::vector<std::pair<OpId, std::vector<int>>> expressions;
+
+ bool cnfConsumed;
+ int cnfVariableCount;
+ std::vector<int> cnfLiteralVariables, cnfExpressionVariables;
+ std::vector<std::vector<int>> cnfClauses;
+ std::set<int> cnfAssumptions;
+
+ void add_clause(const std::vector<int> &args);
+ void add_clause(const std::vector<int> &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<int> &args);
+ int bind_cnf_and(const std::vector<int> &args);
+ int bind_cnf_or(const std::vector<int> &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<int> &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<int> &args) const;
+ const std::vector<int> &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<int> &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<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
+
+ bool solve(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) {
+ return solver(modelExpressions, modelValues, assumptions);
+ }
+
+ bool solve(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) {
+ std::vector<int> 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<int> assumptions, modelExpressions;
+ std::vector<bool> 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<int> &assumed() const { return cnfAssumptions; }
+ int bound(int id) const;
+
+ int numCnfVariables() const { return cnfVariableCount; }
+ const std::vector<std::vector<int>> &cnf() const { return cnfClauses; }
+
+ void consumeCnf();
+ void consumeCnf(std::vector<std::vector<int>> &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<int> vec_const_signed(int64_t value, int bits);
+ std::vector<int> vec_const_unsigned(uint64_t value, int bits);
+ std::vector<int> vec_var(std::string name, int bits);
+ std::vector<int> vec_cast(const std::vector<int> &vec1, int toBits, bool signExtend = false);
+
+ std::vector<int> vec_not(const std::vector<int> &vec1);
+ std::vector<int> vec_and(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ std::vector<int> vec_or(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ std::vector<int> vec_xor(const std::vector<int> &vec1, const std::vector<int> &vec2);
+
+ std::vector<int> vec_iff(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ std::vector<int> vec_ite(const std::vector<int> &vec1, const std::vector<int> &vec2, const std::vector<int> &vec3);
+ std::vector<int> vec_ite(int sel, const std::vector<int> &vec2, const std::vector<int> &vec3);
+
+ std::vector<int> vec_count(const std::vector<int> &vec, int bits, bool clip = true);
+ std::vector<int> vec_add(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ std::vector<int> vec_sub(const std::vector<int> &vec1, const std::vector<int> &vec2);
+
+ void vec_cmp(const std::vector<int> &vec1, const std::vector<int> &vec2, int &carry, int &overflow, int &sign, int &zero);
+
+ int vec_lt_signed(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ int vec_le_signed(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ int vec_ge_signed(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ int vec_gt_signed(const std::vector<int> &vec1, const std::vector<int> &vec2);
+
+ int vec_lt_unsigned(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ int vec_le_unsigned(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ int vec_ge_unsigned(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ int vec_gt_unsigned(const std::vector<int> &vec1, const std::vector<int> &vec2);
+
+ int vec_eq(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ int vec_ne(const std::vector<int> &vec1, const std::vector<int> &vec2);
+
+ std::vector<int> vec_shl(const std::vector<int> &vec1, int shift, bool signExtend = false);
+ std::vector<int> vec_srl(const std::vector<int> &vec1, int shift);
+
+ std::vector<int> vec_shr(const std::vector<int> &vec1, int shift, bool signExtend = false) { return vec_shl(vec1, -shift, signExtend); }
+ std::vector<int> vec_srr(const std::vector<int> &vec1, int shift) { return vec_srl(vec1, -shift); }
+
+ void vec_append(std::vector<int> &vec, const std::vector<int> &vec1) const;
+ void vec_append_signed(std::vector<int> &vec, const std::vector<int> &vec1, int64_t value);
+ void vec_append_unsigned(std::vector<int> &vec, const std::vector<int> &vec1, uint64_t value);
+
+ int64_t vec_model_get_signed(const std::vector<int> &modelExpressions, const std::vector<bool> &modelValues, const std::vector<int> &vec1) const;
+ uint64_t vec_model_get_unsigned(const std::vector<int> &modelExpressions, const std::vector<bool> &modelValues, const std::vector<int> &vec1) const;
+
+ int vec_reduce_and(const std::vector<int> &vec1);
+ int vec_reduce_or(const std::vector<int> &vec1);
+
+ void vec_set(const std::vector<int> &vec1, const std::vector<int> &vec2);
+ void vec_set_signed(const std::vector<int> &vec1, int64_t value);
+ void vec_set_unsigned(const std::vector<int> &vec1, uint64_t value);
+
+ // helpers for generating ezSATbit and ezSATvec objects
+
+ struct ezSATbit bit(_V a);
+ struct ezSATvec vec(const std::vector<int> &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<int> &vec, bool max_only = false);
+ int manyhot(const std::vector<int> &vec, int min_hot, int max_hot = -1);
+ int ordered(const std::vector<int> &vec1, const std::vector<int> &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<int>() const { return std::vector<int>(1, id); }
+};
+
+struct ezSATvec
+{
+ ezSAT &sat;
+ std::vector<int> vec;
+
+ ezSATvec(ezSAT &sat, const std::vector<int> &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<int>() const { return vec; }
+};
+
+#endif
--- /dev/null
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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 <stdio.h>
+#include <assert.h>
+
+#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<int, std::string> blockinfo;
+std::vector<int> 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_t> 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<int> &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<int> &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<int> &vars)
+{
+ std::map<int, std::set<int>> 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<std::vector<int>> pools;
+
+ for (int a : vars)
+ {
+ std::vector<int> 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<int>());
+ pools.back().push_back(a);
+ }
+ }
+
+ std::vector<int> new_vars;
+ for (auto &pool : pools)
+ {
+ std::vector<int> 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<int> 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<int> 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<std::set<blockgeom_t>> symmetries;
+ symmetries.insert(blockgeom);
+ bool keep_running = true;
+ while (keep_running) {
+ keep_running = false;
+ std::set<std::set<blockgeom_t>> old_sym;
+ old_sym.swap(symmetries);
+ for (auto &old_sym_set : old_sym)
+ {
+ std::set<blockgeom_t> mx, my, mz;
+ std::set<blockgeom_t> 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<std::vector<int>> vecvec;
+ for (auto &sym : symmetries) {
+ std::vector<int> 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<int> modelExpressions;
+ std::vector<bool> 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<int> 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;
+}
+
--- /dev/null
+
+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);
+}
+
--- /dev/null
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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 <stdio.h>
+
+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<int> modelExpressions;
+ std::vector<bool> 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<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;
+ output_pattern ^= output_pattern << 13;
+ output_pattern ^= output_pattern >> 17;
+ output_pattern ^= output_pattern << 5;
+
+ std::vector<int> modelExpressions;
+ std::vector<int> forwardAssumptions, backwardAssumptions;
+ std::vector<bool> 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<int> 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<int> av = sat.vec_const_signed(a, 8);
+ std::vector<int> bv = sat.vec_const_signed(b, 8);
+ std::vector<int> 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<int> av = sat.vec_const_unsigned(a, 8);
+ std::vector<int> bv = sat.vec_const_unsigned(b, 8);
+ std::vector<int> 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<int> v = sat.vec_const_unsigned(x, 32);
+
+ std::vector<int> cv6 = sat.vec_const_unsigned(count, 6);
+ std::vector<int> 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<int> 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<bool> 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<int> 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<int> 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<bool> 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<int> 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<int> abc;
+ abc.push_back(a);
+ abc.push_back(b);
+ abc.push_back(c);
+
+ std::vector<int> 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<int> modelVariables;
+ std::vector<bool> 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<int> 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;
+}
+
projects / yosys.git / commitdiff