mirror of https://github.com/YosysHQ/yosys.git
Added ezSAT library
This commit is contained in:
Clifford Wolf
parent
c32b918681
commit
3371563f2f
25
Makefile
25
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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
@ -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.
|
||||
|
||||
|
|
@ -0,0 +1,71 @@
|
|||
/*
|
||||
* 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;
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,112 @@
|
|||
/*
|
||||
* 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;
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,120 @@
|
|||
/*
|
||||
* 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;
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,46 @@
|
|||
/*
|
||||
* 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
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,313 @@
|
|||
/*
|
||||
* 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
|
||||
|
|
@ -0,0 +1,293 @@
|
|||
/*
|
||||
* 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;
|
||||
}
|
||||
|
||||
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,524 @@
|
|||
/*
|
||||
* 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;
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue