aboutsummaryrefslogtreecommitdiffstats
path: root/libs
diff options
context:
space:
mode:
authorAhmed Irfan <ahmedirfan1983@gmail.com>2014-09-22 11:35:04 +0200
committerAhmed Irfan <ahmedirfan1983@gmail.com>2014-09-22 11:35:04 +0200
commitd3c67ad9b61f602de1100cd264efd227dcacb417 (patch)
tree88c462c53bdab128cd1edbded42483772f82612a /libs
parentb783dbe148e6d246ebd107c0913de2989ab5af48 (diff)
parent13117bb346dd02d2345f716b4403239aebe3d0e2 (diff)
downloadyosys-d3c67ad9b61f602de1100cd264efd227dcacb417.tar.gz
yosys-d3c67ad9b61f602de1100cd264efd227dcacb417.tar.bz2
yosys-d3c67ad9b61f602de1100cd264efd227dcacb417.zip
Merge branch 'master' of https://github.com/cliffordwolf/yosys into btor
added case for memwr cell that is used in muxes (same cell is used more than one time) corrected bug for xnor and logic_not added pmux cell translation Conflicts: backends/btor/btor.cc
Diffstat (limited to 'libs')
-rw-r--r--libs/ezsat/Makefile8
-rw-r--r--libs/ezsat/ezminisat.cc88
-rw-r--r--libs/ezsat/ezminisat.h20
-rw-r--r--libs/ezsat/ezsat.cc322
-rw-r--r--libs/ezsat/ezsat.h38
-rw-r--r--libs/ezsat/puzzle3d.cc4
-rw-r--r--libs/ezsat/testbench.cc131
-rw-r--r--libs/minisat/00_PATCH_mkLit_default_arg.patch20
-rw-r--r--libs/minisat/00_PATCH_remove_zlib.patch38
-rw-r--r--libs/minisat/00_UPDATE.sh17
-rw-r--r--libs/minisat/Alg.h84
-rw-r--r--libs/minisat/Alloc.h131
-rw-r--r--libs/minisat/Dimacs.h87
-rw-r--r--libs/minisat/Heap.h168
-rw-r--r--libs/minisat/IntMap.h106
-rw-r--r--libs/minisat/IntTypes.h42
-rw-r--r--libs/minisat/LICENSE21
-rw-r--r--libs/minisat/Map.h193
-rw-r--r--libs/minisat/Options.cc94
-rw-r--r--libs/minisat/Options.h386
-rw-r--r--libs/minisat/ParseUtils.h119
-rw-r--r--libs/minisat/Queue.h69
-rw-r--r--libs/minisat/Rnd.h67
-rw-r--r--libs/minisat/SimpSolver.cc727
-rw-r--r--libs/minisat/SimpSolver.h222
-rw-r--r--libs/minisat/Solver.cc1068
-rw-r--r--libs/minisat/Solver.h409
-rw-r--r--libs/minisat/SolverTypes.h478
-rw-r--r--libs/minisat/Sort.h98
-rw-r--r--libs/minisat/System.cc171
-rw-r--r--libs/minisat/System.h72
-rw-r--r--libs/minisat/Vec.h134
-rw-r--r--libs/minisat/XAlloc.h45
-rw-r--r--libs/sha1/sha1.cpp455
-rw-r--r--libs/sha1/sha1.h106
-rw-r--r--libs/subcircuit/subcircuit.cc4
-rw-r--r--libs/svgviewer/.gitignore5
-rw-r--r--libs/svgviewer/files/bubbles.svg215
-rw-r--r--libs/svgviewer/files/cubic.svg77
-rw-r--r--libs/svgviewer/files/spheres.svg72
-rw-r--r--libs/svgviewer/main.cpp66
-rw-r--r--libs/svgviewer/mainwindow.cpp205
-rw-r--r--libs/svgviewer/mainwindow.h86
-rw-r--r--libs/svgviewer/svgview.cpp227
-rw-r--r--libs/svgviewer/svgview.h87
-rw-r--r--libs/svgviewer/svgviewer.desktop11
-rw-r--r--libs/svgviewer/svgviewer.pro33
-rw-r--r--libs/svgviewer/svgviewer.qrc6
48 files changed, 5760 insertions, 1572 deletions
diff --git a/libs/ezsat/Makefile b/libs/ezsat/Makefile
index da2355a9b..b1f864160 100644
--- a/libs/ezsat/Makefile
+++ b/libs/ezsat/Makefile
@@ -3,7 +3,8 @@ CC = clang
CXX = clang
CXXFLAGS = -MD -Wall -Wextra -ggdb
CXXFLAGS += -std=c++11 -O0
-LDLIBS = -lminisat -lstdc++
+LDLIBS = ../minisat/Options.cc ../minisat/SimpSolver.cc ../minisat/Solver.cc ../minisat/System.cc -lm -lstdc++
+
all: demo_vec demo_bit demo_cmp testbench puzzle3d
@@ -17,10 +18,11 @@ test: all
./testbench
./demo_bit
./demo_vec
- ./demo_cmp
+ # ./demo_cmp
+ # ./puzzle3d
clean:
- rm -f demo_bit demo_vec testbench puzzle3d *.o *.d
+ rm -f demo_bit demo_vec demo_cmp testbench puzzle3d *.o *.d
.PHONY: all test clean
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index d545834cf..dc4e5d283 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -25,15 +25,20 @@
#include <limits.h>
#include <stdint.h>
-#include <signal.h>
+#include <csignal>
#include <cinttypes>
+#include <unistd.h>
-#include <minisat/core/Solver.h>
+#include "../minisat/Solver.h"
+#include "../minisat/SimpSolver.h"
ezMiniSAT::ezMiniSAT() : minisatSolver(NULL)
{
minisatSolver = NULL;
foundContradiction = false;
+
+ freeze(TRUE);
+ freeze(FALSE);
}
ezMiniSAT::~ezMiniSAT()
@@ -50,9 +55,28 @@ void ezMiniSAT::clear()
}
foundContradiction = false;
minisatVars.clear();
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ cnfFrozenVars.clear();
+#endif
ezSAT::clear();
}
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+void ezMiniSAT::freeze(int id)
+{
+ if (!mode_non_incremental())
+ cnfFrozenVars.insert(bind(id));
+}
+
+bool ezMiniSAT::eliminated(int idx)
+{
+ idx = idx < 0 ? -idx : idx;
+ if (minisatSolver != NULL && idx > 0 && idx <= int(minisatVars.size()))
+ return minisatSolver->isEliminated(minisatVars.at(idx-1));
+ return false;
+}
+#endif
+
ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL;
clock_t ezMiniSAT::alarmHandlerTimeout = 0;
@@ -67,6 +91,8 @@ void ezMiniSAT::alarmHandler(int)
bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
{
+ preSolverCallback();
+
solverTimoutStatus = false;
if (0) {
@@ -90,22 +116,42 @@ contradiction:
for (auto id : modelExpressions)
modelIdx.push_back(bind(id));
- if (minisatSolver == NULL)
- minisatSolver = new Minisat::Solver;
+ if (minisatSolver == NULL) {
+ minisatSolver = new Solver;
+ minisatSolver->verbosity = EZMINISAT_VERBOSITY;
+ }
+#if EZMINISAT_INCREMENTAL
std::vector<std::vector<int>> cnf;
consumeCnf(cnf);
+#else
+ const std::vector<std::vector<int>> &cnf = this->cnf();
+#endif
while (int(minisatVars.size()) < numCnfVariables())
minisatVars.push_back(minisatSolver->newVar());
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ for (auto idx : cnfFrozenVars)
+ minisatSolver->setFrozen(minisatVars.at(idx > 0 ? idx-1 : -idx-1), true);
+ cnfFrozenVars.clear();
+#endif
+
for (auto &clause : cnf) {
Minisat::vec<Minisat::Lit> ps;
- for (auto idx : clause)
+ for (auto idx : clause) {
if (idx > 0)
ps.push(Minisat::mkLit(minisatVars.at(idx-1)));
else
ps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
+#if EZMINISAT_SIMPSOLVER
+ if (minisatSolver->isEliminated(minisatVars.at(idx > 0 ? idx-1 : -idx-1))) {
+ fprintf(stderr, "Assert in %s:%d failed! Missing call to ezsat->freeze(): %s (lit=%d)\n",
+ __FILE__, __LINE__, cnfLiteralInfo(idx).c_str(), idx);
+ abort();
+ }
+#endif
+ }
if (!minisatSolver->addClause(ps))
goto contradiction;
}
@@ -115,20 +161,31 @@ contradiction:
Minisat::vec<Minisat::Lit> assumps;
- for (auto idx : extraClauses)
+ for (auto idx : extraClauses) {
if (idx > 0)
assumps.push(Minisat::mkLit(minisatVars.at(idx-1)));
else
assumps.push(Minisat::mkLit(minisatVars.at(-idx-1), true));
+#if EZMINISAT_SIMPSOLVER
+ if (minisatSolver->isEliminated(minisatVars.at(idx > 0 ? idx-1 : -idx-1))) {
+ fprintf(stderr, "Assert in %s:%d failed! Missing call to ezsat->freeze(): %s\n", __FILE__, __LINE__, cnfLiteralInfo(idx).c_str());
+ abort();
+ }
+#endif
+ }
- sighandler_t old_alarm_sighandler = NULL;
+ struct sigaction sig_action;
+ struct sigaction old_sig_action;
int old_alarm_timeout = 0;
if (solverTimeout > 0) {
+ sig_action.sa_handler = alarmHandler;
+ sigemptyset(&sig_action.sa_mask);
+ sig_action.sa_flags = SA_RESTART;
alarmHandlerThis = this;
alarmHandlerTimeout = clock() + solverTimeout*CLOCKS_PER_SEC;
old_alarm_timeout = alarm(0);
- old_alarm_sighandler = signal(SIGALRM, alarmHandler);
+ sigaction(SIGALRM, &sig_action, &old_sig_action);
alarm(1);
}
@@ -138,12 +195,18 @@ contradiction:
if (alarmHandlerTimeout == 0)
solverTimoutStatus = true;
alarm(0);
- signal(SIGALRM, old_alarm_sighandler);
+ sigaction(SIGALRM, &old_sig_action, NULL);
alarm(old_alarm_timeout);
}
- if (!foundSolution)
+ if (!foundSolution) {
+#if !EZMINISAT_INCREMENTAL
+ delete minisatSolver;
+ minisatSolver = NULL;
+ minisatVars.clear();
+#endif
return false;
+ }
modelValues.clear();
modelValues.resize(modelIdx.size());
@@ -161,6 +224,11 @@ contradiction:
modelValues[i] = (value == Minisat::lbool(refvalue));
}
+#if !EZMINISAT_INCREMENTAL
+ delete minisatSolver;
+ minisatSolver = NULL;
+ minisatVars.clear();
+#endif
return true;
}
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 2919aa2e3..ac9c071c3 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -20,6 +20,10 @@
#ifndef EZMINISAT_H
#define EZMINISAT_H
+#define EZMINISAT_SIMPSOLVER 1
+#define EZMINISAT_VERBOSITY 0
+#define EZMINISAT_INCREMENTAL 1
+
#include "ezsat.h"
#include <time.h>
@@ -28,15 +32,25 @@
// don't force ezSAT users to use minisat headers..
namespace Minisat {
class Solver;
+ class SimpSolver;
}
class ezMiniSAT : public ezSAT
{
private:
- Minisat::Solver *minisatSolver;
+#if EZMINISAT_SIMPSOLVER
+ typedef Minisat::SimpSolver Solver;
+#else
+ typedef Minisat::Solver Solver;
+#endif
+ Solver *minisatSolver;
std::vector<int> minisatVars;
bool foundContradiction;
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ std::set<int> cnfFrozenVars;
+#endif
+
static ezMiniSAT *alarmHandlerThis;
static clock_t alarmHandlerTimeout;
static void alarmHandler(int);
@@ -45,6 +59,10 @@ public:
ezMiniSAT();
virtual ~ezMiniSAT();
virtual void clear();
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ virtual void freeze(int id);
+ virtual bool eliminated(int idx);
+#endif
virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
};
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index dccc00555..13ed112ed 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -19,21 +19,21 @@
#include "ezsat.h"
+#include <cmath>
#include <algorithm>
+#include <cassert>
#include <stdlib.h>
-#include <assert.h>
const int ezSAT::TRUE = 1;
const int ezSAT::FALSE = 2;
ezSAT::ezSAT()
{
- literal("TRUE");
- literal("FALSE");
+ flag_keep_cnf = false;
+ flag_non_incremental = false;
- assert(literal("TRUE") == TRUE);
- assert(literal("FALSE") == FALSE);
+ non_incremental_solve_used_up = false;
cnfConsumed = false;
cnfVariableCount = 0;
@@ -41,6 +41,12 @@ ezSAT::ezSAT()
solverTimeout = 0;
solverTimoutStatus = false;
+
+ literal("TRUE");
+ literal("FALSE");
+
+ assert(literal("TRUE") == TRUE);
+ assert(literal("FALSE") == FALSE);
}
ezSAT::~ezSAT()
@@ -67,6 +73,20 @@ int ezSAT::literal(const std::string &name)
return literalsCache.at(name);
}
+int ezSAT::frozen_literal()
+{
+ int id = literal();
+ freeze(id);
+ return id;
+}
+
+int ezSAT::frozen_literal(const std::string &name)
+{
+ int id = literal(name);
+ freeze(id);
+ return id;
+}
+
int ezSAT::expression(OpId op, int a, int b, int c, int d, int e, int f)
{
std::vector<int> args(6);
@@ -342,13 +362,19 @@ void ezSAT::clear()
cnfLiteralVariables.clear();
cnfExpressionVariables.clear();
cnfClauses.clear();
- cnfAssumptions.clear();
}
-void ezSAT::assume(int id)
+void ezSAT::freeze(int)
+{
+}
+
+bool ezSAT::eliminated(int)
{
- cnfAssumptions.insert(id);
+ return false;
+}
+void ezSAT::assume(int id)
+{
if (id < 0)
{
assert(0 < -id && -id <= int(expressions.size()));
@@ -462,11 +488,32 @@ int ezSAT::bound(int id) const
return 0;
}
-int ezSAT::bind(int id)
+std::string ezSAT::cnfLiteralInfo(int idx) const
+{
+ for (size_t i = 0; i < cnfLiteralVariables.size(); i++) {
+ if (cnfLiteralVariables[i] == idx)
+ return to_string(i+1);
+ if (cnfLiteralVariables[i] == -idx)
+ return "NOT " + to_string(i+1);
+ }
+ for (size_t i = 0; i < cnfExpressionVariables.size(); i++) {
+ if (cnfExpressionVariables[i] == idx)
+ return to_string(-i-1);
+ if (cnfExpressionVariables[i] == -idx)
+ return "NOT " + to_string(-i-1);
+ }
+ return "<unnamed>";
+}
+
+int ezSAT::bind(int id, bool auto_freeze)
{
if (id >= 0) {
assert(0 < id && id <= int(literals.size()));
cnfLiteralVariables.resize(literals.size());
+ if (eliminated(cnfLiteralVariables[id-1])) {
+ fprintf(stderr, "ezSAT: Missing freeze on literal `%s'.\n", to_string(id).c_str());
+ abort();
+ }
if (cnfLiteralVariables[id-1] == 0) {
cnfLiteralVariables[id-1] = ++cnfVariableCount;
if (id == TRUE)
@@ -480,6 +527,17 @@ int ezSAT::bind(int id)
assert(0 < -id && -id <= int(expressions.size()));
cnfExpressionVariables.resize(expressions.size());
+ if (eliminated(cnfExpressionVariables[-id-1]))
+ {
+ cnfExpressionVariables[-id-1] = 0;
+
+ // this will recursively call bind(id). within the recursion
+ // the cnf is pre-set to 0. an idx is allocated there, then it
+ // is frozen, then it returns here with the new idx already set.
+ if (auto_freeze)
+ freeze(id);
+ }
+
if (cnfExpressionVariables[-id-1] == 0)
{
OpId op;
@@ -497,7 +555,7 @@ int ezSAT::bind(int id)
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));
+ idx = bind(args.at(0), false);
goto assign_idx;
}
@@ -505,17 +563,17 @@ int ezSAT::bind(int id)
std::vector<int> invArgs;
for (auto arg : args)
invArgs.push_back(NOT(arg));
- idx = bind(OR(expression(OpAnd, args), expression(OpAnd, invArgs)));
+ idx = bind(OR(expression(OpAnd, args), expression(OpAnd, invArgs)), false);
goto assign_idx;
}
if (op == OpITE) {
- idx = bind(OR(AND(args[0], args[1]), AND(NOT(args[0]), args[2])));
+ idx = bind(OR(AND(args[0], args[1]), AND(NOT(args[0]), args[2])), false);
goto assign_idx;
}
for (int i = 0; i < int(args.size()); i++)
- args[i] = bind(args[i]);
+ args[i] = bind(args[i], false);
switch (op)
{
@@ -535,120 +593,45 @@ int ezSAT::bind(int id)
void ezSAT::consumeCnf()
{
- cnfConsumed = true;
+ if (mode_keep_cnf())
+ cnfClausesBackup.insert(cnfClausesBackup.end(), cnfClauses.begin(), cnfClauses.end());
+ else
+ cnfConsumed = true;
cnfClauses.clear();
}
void ezSAT::consumeCnf(std::vector<std::vector<int>> &cnf)
{
- cnfConsumed = true;
+ if (mode_keep_cnf())
+ cnfClausesBackup.insert(cnfClausesBackup.end(), cnfClauses.begin(), cnfClauses.end());
+ else
+ cnfConsumed = true;
cnf.swap(cnfClauses);
cnfClauses.clear();
}
-static bool test_bit(uint32_t bitmask, int idx)
+void ezSAT::getFullCnf(std::vector<std::vector<int>> &full_cnf) const
{
- if (idx > 0)
- return (bitmask & (1 << (+idx-1))) != 0;
- else
- return (bitmask & (1 << (-idx-1))) == 0;
+ assert(full_cnf.empty());
+ full_cnf.insert(full_cnf.end(), cnfClausesBackup.begin(), cnfClausesBackup.end());
+ full_cnf.insert(full_cnf.end(), cnfClauses.begin(), cnfClauses.end());
}
-bool ezSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
+void ezSAT::preSolverCallback()
{
- 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:;
- }
+ assert(!non_incremental_solve_used_up);
+ if (mode_non_incremental())
+ non_incremental_solve_used_up = true;
+}
- return false;
+bool ezSAT::solver(const std::vector<int>&, std::vector<bool>&, const std::vector<int>&)
+{
+ preSolverCallback();
+ fprintf(stderr, "************************************************************************\n");
+ fprintf(stderr, "ERROR: You are trying to use the solve() method of the ezSAT base class!\n");
+ fprintf(stderr, "Use a dervied class like ezMiniSAT instead.\n");
+ fprintf(stderr, "************************************************************************\n");
+ abort();
}
std::vector<int> ezSAT::vec_const(const std::vector<bool> &bits)
@@ -994,6 +977,96 @@ std::vector<int> ezSAT::vec_srl(const std::vector<int> &vec1, int shift)
return vec;
}
+std::vector<int> ezSAT::vec_shift(const std::vector<int> &vec1, int shift, int extend_left, int extend_right)
+{
+ std::vector<int> vec;
+ for (int i = 0; i < int(vec1.size()); i++) {
+ int j = i+shift;
+ if (j < 0)
+ vec.push_back(extend_right);
+ else if (j >= int(vec1.size()))
+ vec.push_back(extend_left);
+ else
+ vec.push_back(vec1[j]);
+ }
+ return vec;
+}
+
+static int my_clog2(int x)
+{
+ int result = 0;
+ for (x--; x > 0; result++)
+ x >>= 1;
+ return result;
+}
+
+std::vector<int> ezSAT::vec_shift_right(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right)
+{
+ int vec2_bits = std::min(my_clog2(vec1.size()) + (vec2_signed ? 1 : 0), int(vec2.size()));
+
+ std::vector<int> overflow_bits(vec2.begin() + vec2_bits, vec2.end());
+ int overflow_left = FALSE, overflow_right = FALSE;
+
+ if (vec2_signed) {
+ int overflow = FALSE;
+ for (auto bit : overflow_bits)
+ overflow = OR(overflow, XOR(bit, vec2[vec2_bits-1]));
+ overflow_left = AND(overflow, NOT(vec2.back()));
+ overflow_right = AND(overflow, vec2.back());
+ } else
+ overflow_left = vec_reduce_or(overflow_bits);
+
+ std::vector<int> buffer = vec1;
+
+ if (vec2_signed)
+ while (buffer.size() < vec1.size() + (1 << vec2_bits))
+ buffer.push_back(extend_left);
+
+ std::vector<int> overflow_pattern_left(buffer.size(), extend_left);
+ std::vector<int> overflow_pattern_right(buffer.size(), extend_right);
+
+ buffer = vec_ite(overflow_left, overflow_pattern_left, buffer);
+
+ if (vec2_signed)
+ buffer = vec_ite(overflow_right, overflow_pattern_left, buffer);
+
+ for (int i = vec2_bits-1; i >= 0; i--) {
+ std::vector<int> shifted_buffer;
+ if (vec2_signed && i == vec2_bits-1)
+ shifted_buffer = vec_shift(buffer, -(1 << i), extend_left, extend_right);
+ else
+ shifted_buffer = vec_shift(buffer, 1 << i, extend_left, extend_right);
+ buffer = vec_ite(vec2[i], shifted_buffer, buffer);
+ }
+
+ buffer.resize(vec1.size());
+ return buffer;
+}
+
+std::vector<int> ezSAT::vec_shift_left(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right)
+{
+ // vec2_signed is not implemented in vec_shift_left() yet
+ assert(vec2_signed == false);
+
+ int vec2_bits = std::min(my_clog2(vec1.size()), int(vec2.size()));
+
+ std::vector<int> overflow_bits(vec2.begin() + vec2_bits, vec2.end());
+ int overflow = vec_reduce_or(overflow_bits);
+
+ std::vector<int> buffer = vec1;
+ std::vector<int> overflow_pattern_right(buffer.size(), extend_right);
+ buffer = vec_ite(overflow, overflow_pattern_right, buffer);
+
+ for (int i = 0; i < vec2_bits; i++) {
+ std::vector<int> shifted_buffer;
+ shifted_buffer = vec_shift(buffer, -(1 << i), extend_left, extend_right);
+ buffer = vec_ite(vec2[i], shifted_buffer, buffer);
+ }
+
+ buffer.resize(vec1.size());
+ return buffer;
+}
+
void ezSAT::vec_append(std::vector<int> &vec, const std::vector<int> &vec1) const
{
for (auto bit : vec1)
@@ -1124,17 +1197,32 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
if (cnfExpressionVariables[i] != 0)
fprintf(f, "c %*d: %s\n", digits, cnfExpressionVariables[i], to_string(-i-1).c_str());
+ if (mode_keep_cnf()) {
+ fprintf(f, "c\n");
+ fprintf(f, "c %d clauses from backup, %d from current buffer\n",
+ int(cnfClausesBackup.size()), int(cnfClauses.size()));
+ }
+
fprintf(f, "c\n");
}
- fprintf(f, "p cnf %d %d\n", cnfVariableCount, int(cnfClauses.size()));
+ std::vector<std::vector<int>> all_clauses;
+ getFullCnf(all_clauses);
+ assert(cnfClausesCount == int(all_clauses.size()));
+
+ fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount);
int maxClauseLen = 0;
- for (auto &clause : cnfClauses)
+ for (auto &clause : all_clauses)
maxClauseLen = std::max(int(clause.size()), maxClauseLen);
- for (auto &clause : cnfClauses) {
+ if (!verbose)
+ maxClauseLen = std::min(maxClauseLen, 3);
+ for (auto &clause : all_clauses) {
for (auto idx : clause)
fprintf(f, " %*d", digits, idx);
- fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
+ if (maxClauseLen >= int(clause.size()))
+ fprintf(f, " %*d\n", (digits + 1)*int(maxClauseLen - clause.size()) + digits, 0);
+ else
+ fprintf(f, " %*d\n", digits, 0);
}
}
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 547edb93b..c5ef6b0a2 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -48,6 +48,11 @@ public:
static const int FALSE;
private:
+ bool flag_keep_cnf;
+ bool flag_non_incremental;
+
+ bool non_incremental_solve_used_up;
+
std::map<std::string, int> literalsCache;
std::vector<std::string> literals;
@@ -57,8 +62,7 @@ private:
bool cnfConsumed;
int cnfVariableCount, cnfClausesCount;
std::vector<int> cnfLiteralVariables, cnfExpressionVariables;
- std::vector<std::vector<int>> cnfClauses;
- std::set<int> cnfAssumptions;
+ std::vector<std::vector<int>> cnfClauses, cnfClausesBackup;
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);
@@ -68,6 +72,9 @@ private:
int bind_cnf_and(const std::vector<int> &args);
int bind_cnf_or(const std::vector<int> &args);
+protected:
+ void preSolverCallback();
+
public:
int solverTimeout;
bool solverTimoutStatus;
@@ -75,11 +82,19 @@ public:
ezSAT();
virtual ~ezSAT();
+ void keep_cnf() { flag_keep_cnf = true; }
+ void non_incremental() { flag_non_incremental = true; }
+
+ bool mode_keep_cnf() const { return flag_keep_cnf; }
+ bool mode_non_incremental() const { return flag_non_incremental; }
+
// manage expressions
int value(bool val);
int literal();
int literal(const std::string &name);
+ int frozen_literal();
+ int frozen_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);
@@ -141,10 +156,10 @@ public:
// manage CNF (usually only accessed by SAT solvers)
virtual void clear();
+ virtual void freeze(int id);
+ virtual bool eliminated(int idx);
void assume(int id);
- int bind(int id);
-
- const std::set<int> &assumed() const { return cnfAssumptions; }
+ int bind(int id, bool auto_freeze = true);
int bound(int id) const;
int numCnfVariables() const { return cnfVariableCount; }
@@ -154,6 +169,11 @@ public:
void consumeCnf();
void consumeCnf(std::vector<std::vector<int>> &cnf);
+ // use this function to get the full CNF in keep_cnf mode
+ void getFullCnf(std::vector<std::vector<int>> &full_cnf) const;
+
+ std::string cnfLiteralInfo(int idx) const;
+
// simple helpers for build expressions easily
struct _V {
@@ -165,7 +185,7 @@ public:
int get(ezSAT *that) {
if (name.empty())
return id;
- return that->literal(name);
+ return that->frozen_literal(name);
}
};
@@ -217,7 +237,7 @@ public:
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_ite(int sel, const std::vector<int> &vec1, const std::vector<int> &vec2);
std::vector<int> vec_count(const std::vector<int> &vec, int numBits, bool clip = true);
std::vector<int> vec_add(const std::vector<int> &vec1, const std::vector<int> &vec2);
@@ -245,6 +265,10 @@ public:
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); }
+ std::vector<int> vec_shift(const std::vector<int> &vec1, int shift, int extend_left, int extend_right);
+ std::vector<int> vec_shift_right(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right);
+ std::vector<int> vec_shift_left(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right);
+
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);
diff --git a/libs/ezsat/puzzle3d.cc b/libs/ezsat/puzzle3d.cc
index 56d293260..aee0044b4 100644
--- a/libs/ezsat/puzzle3d.cc
+++ b/libs/ezsat/puzzle3d.cc
@@ -260,8 +260,10 @@ int main()
std::vector<int> modelExpressions;
std::vector<bool> modelValues;
- for (auto &it : blockinfo)
+ for (auto &it : blockinfo) {
+ ez.freeze(it.first);
modelExpressions.push_back(it.first);
+ }
int solution_counter = 0;
while (1)
diff --git a/libs/ezsat/testbench.cc b/libs/ezsat/testbench.cc
index cc0fe5734..d20258c37 100644
--- a/libs/ezsat/testbench.cc
+++ b/libs/ezsat/testbench.cc
@@ -38,11 +38,6 @@ struct xorshift128 {
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;
@@ -68,7 +63,8 @@ void test_simple()
{
printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
- ezSAT sat;
+ ezMiniSAT sat;
+ sat.non_incremental();
sat.assume(sat.OR("A", "B"));
sat.assume(sat.NOT(sat.AND("A", "B")));
test(sat);
@@ -76,89 +72,6 @@ void test_simple()
// ------------------------------------------------------------------------------------------------------------
-void test_basic_operators(ezSAT &sat, xorshift128 &rng, int iter, bool buildTrees, bool buildClusters, std::vector<bool> &log)
-{
- int vars[6] = {
- sat.VAR("A"), sat.VAR("B"), sat.VAR("C"),
- sat.NOT("A"), sat.NOT("B"), sat.NOT("C")
- };
- for (int i = 0; i < iter; i++) {
- int assumption = 0, op = rng() % 6, to = rng() % 6;
- int a = vars[rng() % 6], b = vars[rng() % 6], c = vars[rng() % 6];
- // printf("--> %d %d:%s %d:%s %d:%s\n", op, a, sat.to_string(a).c_str(), b, sat.to_string(b).c_str(), c, sat.to_string(c).c_str());
- switch (op)
- {
- case 0:
- assumption = sat.NOT(a);
- break;
- case 1:
- assumption = sat.AND(a, b);
- break;
- case 2:
- assumption = sat.OR(a, b);
- break;
- case 3:
- assumption = sat.XOR(a, b);
- break;
- case 4:
- assumption = sat.IFF(a, b);
- break;
- case 5:
- assumption = sat.ITE(a, b, c);
- break;
- }
- // printf(" --> %d:%s\n", to, sat.to_string(assumption).c_str());
- if (buildTrees)
- vars[to] = assumption;
- if (!buildClusters)
- sat.clear();
- sat.assume(assumption);
- if (sat.numCnfVariables() < 15) {
- printf("%d:\n", int(log.size()));
- log.push_back(test(sat));
- } else {
- // printf("** skipping large problem **\n");
- }
- }
-}
-
-void test_basic_operators(ezSAT &sat, std::vector<bool> &log)
-{
- printf("-- %s --\n\n", __PRETTY_FUNCTION__);
-
- xorshift128 rng;
- test_basic_operators(sat, rng, 1000, false, false, log);
- for (int i = 0; i < 100; i++)
- test_basic_operators(sat, rng, 10, true, false, log);
- for (int i = 0; i < 100; i++)
- test_basic_operators(sat, rng, 10, false, true, log);
-}
-
-void test_basic_operators()
-{
- printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
-
- ezSAT sat;
- ezMiniSAT miniSat;
- std::vector<bool> logSat, logMiniSat;
-
- test_basic_operators(sat, logSat);
- test_basic_operators(miniSat, logMiniSat);
-
- if (logSat != logMiniSat) {
- printf("Differences between logSat and logMiniSat:");
- for (int i = 0; i < int(std::max(logSat.size(), logMiniSat.size())); i++)
- if (i >= int(logSat.size()) || i >= int(logMiniSat.size()) || logSat[i] != logMiniSat[i])
- printf(" %d", i);
- printf("\n");
- abort();
- } else {
- printf("Completed %d tests with identical results with ezSAT and ezMiniSAT.\n\n", int(logSat.size()));
- }
-}
-
-// ------------------------------------------------------------------------------------------------------------
-
void test_xorshift32_try(ezSAT &sat, uint32_t input_pattern)
{
uint32_t output_pattern = input_pattern;
@@ -209,6 +122,8 @@ void test_xorshift32()
printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
ezMiniSAT sat;
+ sat.keep_cnf();
+
xorshift128 rng;
std::vector<int> bits = sat.vec_var("i", 32);
@@ -225,6 +140,9 @@ void test_xorshift32()
test_xorshift32_try(sat, rng());
test_xorshift32_try(sat, rng());
test_xorshift32_try(sat, rng());
+
+ sat.printDIMACS(stdout, true);
+ printf("\n");
}
// ------------------------------------------------------------------------------------------------------------
@@ -243,7 +161,7 @@ void check(const char *expr1_str, bool expr1, const char *expr2_str, bool expr2)
void test_signed(int8_t a, int8_t b, int8_t c)
{
- ezSAT sat;
+ ezMiniSAT sat;
std::vector<int> av = sat.vec_const_signed(a, 8);
std::vector<int> bv = sat.vec_const_signed(b, 8);
@@ -262,7 +180,7 @@ void test_signed(int8_t a, int8_t b, int8_t c)
void test_unsigned(uint8_t a, uint8_t b, uint8_t c)
{
- ezSAT sat;
+ ezMiniSAT sat;
if (b < c)
b ^= c, c ^= b, b ^= c;
@@ -284,7 +202,7 @@ void test_unsigned(uint8_t a, uint8_t b, uint8_t c)
void test_count(uint32_t x)
{
- ezSAT sat;
+ ezMiniSAT sat;
int count = 0;
for (int i = 0; i < 32; i++)
@@ -338,10 +256,10 @@ void test_onehot()
printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
ezMiniSAT ez;
- int a = ez.literal("a");
- int b = ez.literal("b");
- int c = ez.literal("c");
- int d = ez.literal("d");
+ int a = ez.frozen_literal("a");
+ int b = ez.frozen_literal("b");
+ int c = ez.frozen_literal("c");
+ int d = ez.frozen_literal("d");
std::vector<int> abcd;
abcd.push_back(a);
@@ -392,10 +310,10 @@ void test_manyhot()
printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
ezMiniSAT ez;
- int a = ez.literal("a");
- int b = ez.literal("b");
- int c = ez.literal("c");
- int d = ez.literal("d");
+ int a = ez.frozen_literal("a");
+ int b = ez.frozen_literal("b");
+ int c = ez.frozen_literal("c");
+ int d = ez.frozen_literal("d");
std::vector<int> abcd;
abcd.push_back(a);
@@ -446,13 +364,13 @@ void test_ordered()
printf("==== %s ====\n\n", __PRETTY_FUNCTION__);
ezMiniSAT ez;
- int a = ez.literal("a");
- int b = ez.literal("b");
- int c = ez.literal("c");
+ int a = ez.frozen_literal("a");
+ int b = ez.frozen_literal("b");
+ int c = ez.frozen_literal("c");
- int x = ez.literal("x");
- int y = ez.literal("y");
- int z = ez.literal("z");
+ int x = ez.frozen_literal("x");
+ int y = ez.frozen_literal("y");
+ int z = ez.frozen_literal("z");
std::vector<int> abc;
abc.push_back(a);
@@ -512,7 +430,6 @@ void test_ordered()
int main()
{
test_simple();
- test_basic_operators();
test_xorshift32();
test_arith();
test_onehot();
diff --git a/libs/minisat/00_PATCH_mkLit_default_arg.patch b/libs/minisat/00_PATCH_mkLit_default_arg.patch
new file mode 100644
index 000000000..e21683f98
--- /dev/null
+++ b/libs/minisat/00_PATCH_mkLit_default_arg.patch
@@ -0,0 +1,20 @@
+--- SolverTypes.h
++++ SolverTypes.h
+@@ -52,7 +52,7 @@ struct Lit {
+ int x;
+
+ // Use this as a constructor:
+- friend Lit mkLit(Var var, bool sign = false);
++ friend Lit mkLit(Var var, bool sign);
+
+ bool operator == (Lit p) const { return x == p.x; }
+ bool operator != (Lit p) const { return x != p.x; }
+@@ -60,7 +60,7 @@ struct Lit {
+ };
+
+
+-inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
++inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
+ inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
+ inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
+ inline bool sign (Lit p) { return p.x & 1; }
diff --git a/libs/minisat/00_PATCH_remove_zlib.patch b/libs/minisat/00_PATCH_remove_zlib.patch
new file mode 100644
index 000000000..61a36f7e5
--- /dev/null
+++ b/libs/minisat/00_PATCH_remove_zlib.patch
@@ -0,0 +1,38 @@
+--- ParseUtils.h
++++ ParseUtils.h
+@@ -24,8 +24,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
+ #include <stdlib.h>
+ #include <stdio.h>
+
+-#include <zlib.h>
+-
+ #include "XAlloc.h"
+
+ namespace Minisat {
+@@ -36,24 +34,16 @@ namespace Minisat {
+
+
+ class StreamBuffer {
+- gzFile in;
+ unsigned char* buf;
+ int pos;
+ int size;
+
+ enum { buffer_size = 64*1024 };
+
+- void assureLookahead() {
+- if (pos >= size) {
+- pos = 0;
+- size = gzread(in, buf, buffer_size); } }
++ virtual void assureLookahead() = 0;
+
+ public:
+- explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0){
+- buf = (unsigned char*)xrealloc(NULL, buffer_size);
+- assureLookahead();
+- }
+- ~StreamBuffer() { free(buf); }
++ virtual ~StreamBuffer() { }
+
+ int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
+ void operator ++ () { pos++; assureLookahead(); }
diff --git a/libs/minisat/00_UPDATE.sh b/libs/minisat/00_UPDATE.sh
new file mode 100644
index 000000000..96a34ec93
--- /dev/null
+++ b/libs/minisat/00_UPDATE.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+rm -f LICENSE *.cc *.h
+git clone --depth 1 https://github.com/niklasso/minisat minisat_upstream
+rm minisat_upstream/minisat/*/Main.cc
+mv minisat_upstream/LICENSE minisat_upstream/minisat/*/*.{h,cc} .
+rm -rf minisat_upstream
+
+sed -i -e 's,^#include *"minisat/[^/]\+/\?,#include ",' *.cc *.h
+sed -i -e 's/Minisat::memUsedPeak()/Minisat::memUsedPeak(bool)/' System.cc
+sed -i -e 's/PRI[iu]64/ & /' Options.h Solver.cc
+sed -i -e '1 i #define __STDC_LIMIT_MACROS' *.cc
+sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc
+
+patch -p0 < 00_PATCH_mkLit_default_arg.patch
+patch -p0 < 00_PATCH_remove_zlib.patch
+
diff --git a/libs/minisat/Alg.h b/libs/minisat/Alg.h
new file mode 100644
index 000000000..ddb972e77
--- /dev/null
+++ b/libs/minisat/Alg.h
@@ -0,0 +1,84 @@
+/*******************************************************************************************[Alg.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Alg_h
+#define Minisat_Alg_h
+
+#include "Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Useful functions on vector-like types:
+
+//=================================================================================================
+// Removing and searching for elements:
+//
+
+template<class V, class T>
+static inline void remove(V& ts, const T& t)
+{
+ int j = 0;
+ for (; j < (int)ts.size() && ts[j] != t; j++);
+ assert(j < (int)ts.size());
+ for (; j < (int)ts.size()-1; j++) ts[j] = ts[j+1];
+ ts.pop();
+}
+
+
+template<class V, class T>
+static inline bool find(V& ts, const T& t)
+{
+ int j = 0;
+ for (; j < (int)ts.size() && ts[j] != t; j++);
+ return j < (int)ts.size();
+}
+
+
+//=================================================================================================
+// Copying vectors with support for nested vector types:
+//
+
+// Base case:
+template<class T>
+static inline void copy(const T& from, T& to)
+{
+ to = from;
+}
+
+// Recursive case:
+template<class T>
+static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
+{
+ if (!append)
+ to.clear();
+ for (int i = 0; i < from.size(); i++){
+ to.push();
+ copy(from[i], to.last());
+ }
+}
+
+template<class T>
+static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Alloc.h b/libs/minisat/Alloc.h
new file mode 100644
index 000000000..6591dcd55
--- /dev/null
+++ b/libs/minisat/Alloc.h
@@ -0,0 +1,131 @@
+/*****************************************************************************************[Alloc.h]
+Copyright (c) 2008-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+
+#ifndef Minisat_Alloc_h
+#define Minisat_Alloc_h
+
+#include "XAlloc.h"
+#include "Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple Region-based memory allocator:
+
+template<class T>
+class RegionAllocator
+{
+ T* memory;
+ uint32_t sz;
+ uint32_t cap;
+ uint32_t wasted_;
+
+ void capacity(uint32_t min_cap);
+
+ public:
+ // TODO: make this a class for better type-checking?
+ typedef uint32_t Ref;
+ enum { Ref_Undef = UINT32_MAX };
+ enum { Unit_Size = sizeof(T) };
+
+ explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }
+ ~RegionAllocator()
+ {
+ if (memory != NULL)
+ ::free(memory);
+ }
+
+
+ uint32_t size () const { return sz; }
+ uint32_t wasted () const { return wasted_; }
+
+ Ref alloc (int size);
+ void free (int size) { wasted_ += size; }
+
+ // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+ T& operator[](Ref r) { assert(r < sz); return memory[r]; }
+ const T& operator[](Ref r) const { assert(r < sz); return memory[r]; }
+
+ T* lea (Ref r) { assert(r < sz); return &memory[r]; }
+ const T* lea (Ref r) const { assert(r < sz); return &memory[r]; }
+ Ref ael (const T* t) { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
+ return (Ref)(t - &memory[0]); }
+
+ void moveTo(RegionAllocator& to) {
+ if (to.memory != NULL) ::free(to.memory);
+ to.memory = memory;
+ to.sz = sz;
+ to.cap = cap;
+ to.wasted_ = wasted_;
+
+ memory = NULL;
+ sz = cap = wasted_ = 0;
+ }
+
+
+};
+
+template<class T>
+void RegionAllocator<T>::capacity(uint32_t min_cap)
+{
+ if (cap >= min_cap) return;
+
+ uint32_t prev_cap = cap;
+ while (cap < min_cap){
+ // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the
+ // result even by clearing the least significant bit. The resulting sequence of capacities
+ // is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when
+ // using 'uint32_t' as indices so that as much as possible of this space can be used.
+ uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
+ cap += delta;
+
+ if (cap <= prev_cap)
+ throw OutOfMemoryException();
+ }
+ // printf(" .. (%p) cap = %u\n", this, cap);
+
+ assert(cap > 0);
+ memory = (T*)xrealloc(memory, sizeof(T)*cap);
+}
+
+
+template<class T>
+typename RegionAllocator<T>::Ref
+RegionAllocator<T>::alloc(int size)
+{
+ // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
+ assert(size > 0);
+ capacity(sz + size);
+
+ uint32_t prev_sz = sz;
+ sz += size;
+
+ // Handle overflow:
+ if (sz < prev_sz)
+ throw OutOfMemoryException();
+
+ return prev_sz;
+}
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Dimacs.h b/libs/minisat/Dimacs.h
new file mode 100644
index 000000000..ccfa1c013
--- /dev/null
+++ b/libs/minisat/Dimacs.h
@@ -0,0 +1,87 @@
+/****************************************************************************************[Dimacs.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Dimacs_h
+#define Minisat_Dimacs_h
+
+#include <stdio.h>
+
+#include "ParseUtils.h"
+#include "SolverTypes.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// DIMACS Parser:
+
+template<class B, class Solver>
+static void readClause(B& in, Solver& S, vec<Lit>& lits) {
+ int parsed_lit, var;
+ lits.clear();
+ for (;;){
+ parsed_lit = parseInt(in);
+ if (parsed_lit == 0) break;
+ var = abs(parsed_lit)-1;
+ while (var >= S.nVars()) S.newVar();
+ lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
+ }
+}
+
+template<class B, class Solver>
+static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) {
+ vec<Lit> lits;
+ int vars = 0;
+ int clauses = 0;
+ int cnt = 0;
+ for (;;){
+ skipWhitespace(in);
+ if (*in == EOF) break;
+ else if (*in == 'p'){
+ if (eagerMatch(in, "p cnf")){
+ vars = parseInt(in);
+ clauses = parseInt(in);
+ // SATRACE'06 hack
+ // if (clauses > 4000000)
+ // S.eliminate(true);
+ }else{
+ printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
+ }
+ } else if (*in == 'c' || *in == 'p')
+ skipLine(in);
+ else{
+ cnt++;
+ readClause(in, S, lits);
+ S.addClause_(lits); }
+ }
+ if (strictp && cnt != clauses)
+ printf("PARSE ERROR! DIMACS header mismatch: wrong number of clauses\n");
+}
+
+// Inserts problem into solver.
+//
+template<class Solver>
+static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+ StreamBuffer in(input_stream);
+ parse_DIMACS_main(in, S, strictp); }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Heap.h b/libs/minisat/Heap.h
new file mode 100644
index 000000000..057a3cdf2
--- /dev/null
+++ b/libs/minisat/Heap.h
@@ -0,0 +1,168 @@
+/******************************************************************************************[Heap.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Heap_h
+#define Minisat_Heap_h
+
+#include "Vec.h"
+#include "IntMap.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// A heap implementation with support for decrease/increase key.
+
+
+template<class K, class Comp, class MkIndex = MkIndexDefault<K> >
+class Heap {
+ vec<K> heap; // Heap of Keys
+ IntMap<K,int,MkIndex> indices; // Each Key's position (index) in the Heap
+ Comp lt; // The heap is a minimum-heap with respect to this comparator
+
+ // Index "traversal" functions
+ static inline int left (int i) { return i*2+1; }
+ static inline int right (int i) { return (i+1)*2; }
+ static inline int parent(int i) { return (i-1) >> 1; }
+
+
+ void percolateUp(int i)
+ {
+ K x = heap[i];
+ int p = parent(i);
+
+ while (i != 0 && lt(x, heap[p])){
+ heap[i] = heap[p];
+ indices[heap[p]] = i;
+ i = p;
+ p = parent(p);
+ }
+ heap [i] = x;
+ indices[x] = i;
+ }
+
+
+ void percolateDown(int i)
+ {
+ K x = heap[i];
+ while (left(i) < heap.size()){
+ int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
+ if (!lt(heap[child], x)) break;
+ heap[i] = heap[child];
+ indices[heap[i]] = i;
+ i = child;
+ }
+ heap [i] = x;
+ indices[x] = i;
+ }
+
+
+ public:
+ Heap(const Comp& c, MkIndex _index = MkIndex()) : indices(_index), lt(c) {}
+
+ int size () const { return heap.size(); }
+ bool empty () const { return heap.size() == 0; }
+ bool inHeap (K k) const { return indices.has(k) && indices[k] >= 0; }
+ int operator[](int index) const { assert(index < heap.size()); return heap[index]; }
+
+ void decrease (K k) { assert(inHeap(k)); percolateUp (indices[k]); }
+ void increase (K k) { assert(inHeap(k)); percolateDown(indices[k]); }
+
+
+ // Safe variant of insert/decrease/increase:
+ void update(K k)
+ {
+ if (!inHeap(k))
+ insert(k);
+ else {
+ percolateUp(indices[k]);
+ percolateDown(indices[k]); }
+ }
+
+
+ void insert(K k)
+ {
+ indices.reserve(k, -1);
+ assert(!inHeap(k));
+
+ indices[k] = heap.size();
+ heap.push(k);
+ percolateUp(indices[k]);
+ }
+
+
+ void remove(K k)
+ {
+ assert(inHeap(k));
+
+ int k_pos = indices[k];
+ indices[k] = -1;
+
+ if (k_pos < heap.size()-1){
+ heap[k_pos] = heap.last();
+ indices[heap[k_pos]] = k_pos;
+ heap.pop();
+ percolateDown(k_pos);
+ }else
+ heap.pop();
+ }
+
+
+ K removeMin()
+ {
+ K x = heap[0];
+ heap[0] = heap.last();
+ indices[heap[0]] = 0;
+ indices[x] = -1;
+ heap.pop();
+ if (heap.size() > 1) percolateDown(0);
+ return x;
+ }
+
+
+ // Rebuild the heap from scratch, using the elements in 'ns':
+ void build(const vec<K>& ns) {
+ for (int i = 0; i < heap.size(); i++)
+ indices[heap[i]] = -1;
+ heap.clear();
+
+ for (int i = 0; i < ns.size(); i++){
+ // TODO: this should probably call reserve instead of relying on it being reserved already.
+ assert(indices.has(ns[i]));
+ indices[ns[i]] = i;
+ heap.push(ns[i]); }
+
+ for (int i = heap.size() / 2 - 1; i >= 0; i--)
+ percolateDown(i);
+ }
+
+ void clear(bool dispose = false)
+ {
+ // TODO: shouldn't the 'indices' map also be dispose-cleared?
+ for (int i = 0; i < heap.size(); i++)
+ indices[heap[i]] = -1;
+ heap.clear(dispose);
+ }
+};
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/IntMap.h b/libs/minisat/IntMap.h
new file mode 100644
index 000000000..9a66315d1
--- /dev/null
+++ b/libs/minisat/IntMap.h
@@ -0,0 +1,106 @@
+/****************************************************************************************[IntMap.h]
+Copyright (c) 2011, Niklas Sorensson
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_IntMap_h
+#define Minisat_IntMap_h
+
+#include "Vec.h"
+
+namespace Minisat {
+
+ template<class T> struct MkIndexDefault {
+ typename vec<T>::Size operator()(T t) const { return (typename vec<T>::Size)t; }
+ };
+
+ template<class K, class V, class MkIndex = MkIndexDefault<K> >
+ class IntMap {
+ vec<V> map;
+ MkIndex index;
+ public:
+ explicit IntMap(MkIndex _index = MkIndex()) : index(_index){}
+
+ bool has (K k) const { return index(k) < map.size(); }
+
+ const V& operator[](K k) const { assert(has(k)); return map[index(k)]; }
+ V& operator[](K k) { assert(has(k)); return map[index(k)]; }
+
+ const V* begin () const { return &map[0]; }
+ const V* end () const { return &map[map.size()]; }
+ V* begin () { return &map[0]; }
+ V* end () { return &map[map.size()]; }
+
+ void reserve(K key, V pad) { map.growTo(index(key)+1, pad); }
+ void reserve(K key) { map.growTo(index(key)+1); }
+ void insert (K key, V val, V pad){ reserve(key, pad); operator[](key) = val; }
+ void insert (K key, V val) { reserve(key); operator[](key) = val; }
+
+ void clear (bool dispose = false) { map.clear(dispose); }
+ void moveTo (IntMap& to) { map.moveTo(to.map); to.index = index; }
+ void copyTo (IntMap& to) const { map.copyTo(to.map); to.index = index; }
+ };
+
+
+ template<class K, class MkIndex = MkIndexDefault<K> >
+ class IntSet
+ {
+ IntMap<K, char, MkIndex> in_set;
+ vec<K> xs;
+
+ public:
+ // Size operations:
+ int size (void) const { return xs.size(); }
+ void clear (bool free = false){
+ if (free)
+ in_set.clear(true);
+ else
+ for (int i = 0; i < xs.size(); i++)
+ in_set[xs[i]] = 0;
+ xs.clear(free);
+ }
+
+ // Allow inspecting the internal vector:
+ const vec<K>&
+ toVec () const { return xs; }
+
+ // Vector interface:
+ K operator [] (int index) const { return xs[index]; }
+
+
+ void insert (K k) { in_set.reserve(k, 0); if (!in_set[k]) { in_set[k] = 1; xs.push(k); } }
+ bool has (K k) { in_set.reserve(k, 0); return in_set[k]; }
+ };
+
+ #if 0
+ template<class K, class V, V nil, class MkIndex = MkIndexDefault<K> >
+ class IntMapNil {
+ vec<V> map;
+ V nil;
+
+ public:
+ IntMap(){}
+
+ void reserve(K);
+ V& find (K);
+ const V& operator[](K k) const;
+
+ };
+ #endif
+
+//=================================================================================================
+} // namespace Minisat
+#endif
diff --git a/libs/minisat/IntTypes.h b/libs/minisat/IntTypes.h
new file mode 100644
index 000000000..c48816284
--- /dev/null
+++ b/libs/minisat/IntTypes.h
@@ -0,0 +1,42 @@
+/**************************************************************************************[IntTypes.h]
+Copyright (c) 2009-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_IntTypes_h
+#define Minisat_IntTypes_h
+
+#ifdef __sun
+ // Not sure if there are newer versions that support C99 headers. The
+ // needed features are implemented in the headers below though:
+
+# include <sys/int_types.h>
+# include <sys/int_fmtio.h>
+# include <sys/int_limits.h>
+
+#else
+
+# include <stdint.h>
+# include <inttypes.h>
+
+#endif
+
+#include <limits.h>
+
+//=================================================================================================
+
+#endif
diff --git a/libs/minisat/LICENSE b/libs/minisat/LICENSE
new file mode 100644
index 000000000..22816ff39
--- /dev/null
+++ b/libs/minisat/LICENSE
@@ -0,0 +1,21 @@
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+ Copyright (c) 2007-2010 Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a
+copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/libs/minisat/Map.h b/libs/minisat/Map.h
new file mode 100644
index 000000000..a6f832000
--- /dev/null
+++ b/libs/minisat/Map.h
@@ -0,0 +1,193 @@
+/*******************************************************************************************[Map.h]
+Copyright (c) 2006-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Map_h
+#define Minisat_Map_h
+
+#include "IntTypes.h"
+#include "Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Default hash/equals functions
+//
+
+template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
+template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
+
+template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
+template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
+
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
+
+//=================================================================================================
+// Some primes
+//
+
+static const int nprimes = 25;
+static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 };
+
+//=================================================================================================
+// Hash table implementation of Maps
+//
+
+template<class K, class D, class H = Hash<K>, class E = Equal<K> >
+class Map {
+ public:
+ struct Pair { K key; D data; };
+
+ private:
+ H hash;
+ E equals;
+
+ vec<Pair>* table;
+ int cap;
+ int size;
+
+ // Don't allow copying (error prone):
+ Map<K,D,H,E>& operator = (Map<K,D,H,E>& other);
+ Map (Map<K,D,H,E>& other);
+
+ bool checkCap(int new_size) const { return new_size > cap; }
+
+ int32_t index (const K& k) const { return hash(k) % cap; }
+ void _insert (const K& k, const D& d) {
+ vec<Pair>& ps = table[index(k)];
+ ps.push(); ps.last().key = k; ps.last().data = d; }
+
+ void rehash () {
+ const vec<Pair>* old = table;
+
+ int old_cap = cap;
+ int newsize = primes[0];
+ for (int i = 1; newsize <= cap && i < nprimes; i++)
+ newsize = primes[i];
+
+ table = new vec<Pair>[newsize];
+ cap = newsize;
+
+ for (int i = 0; i < old_cap; i++){
+ for (int j = 0; j < old[i].size(); j++){
+ _insert(old[i][j].key, old[i][j].data); }}
+
+ delete [] old;
+
+ // printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);
+ }
+
+
+ public:
+
+ Map () : table(NULL), cap(0), size(0) {}
+ Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}
+ ~Map () { delete [] table; }
+
+ // PRECONDITION: the key must already exist in the map.
+ const D& operator [] (const K& k) const
+ {
+ assert(size != 0);
+ const D* res = NULL;
+ const vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k))
+ res = &ps[i].data;
+ assert(res != NULL);
+ return *res;
+ }
+
+ // PRECONDITION: the key must already exist in the map.
+ D& operator [] (const K& k)
+ {
+ assert(size != 0);
+ D* res = NULL;
+ vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k))
+ res = &ps[i].data;
+ assert(res != NULL);
+ return *res;
+ }
+
+ // PRECONDITION: the key must *NOT* exist in the map.
+ void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }
+ bool peek (const K& k, D& d) const {
+ if (size == 0) return false;
+ const vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k)){
+ d = ps[i].data;
+ return true; }
+ return false;
+ }
+
+ bool has (const K& k) const {
+ if (size == 0) return false;
+ const vec<Pair>& ps = table[index(k)];
+ for (int i = 0; i < ps.size(); i++)
+ if (equals(ps[i].key, k))
+ return true;
+ return false;
+ }
+
+ // PRECONDITION: the key must exist in the map.
+ void remove(const K& k) {
+ assert(table != NULL);
+ vec<Pair>& ps = table[index(k)];
+ int j = 0;
+ for (; j < ps.size() && !equals(ps[j].key, k); j++);
+ assert(j < ps.size());
+ ps[j] = ps.last();
+ ps.pop();
+ size--;
+ }
+
+ void clear () {
+ cap = size = 0;
+ delete [] table;
+ table = NULL;
+ }
+
+ int elems() const { return size; }
+ int bucket_count() const { return cap; }
+
+ // NOTE: the hash and equality objects are not moved by this method:
+ void moveTo(Map& other){
+ delete [] other.table;
+
+ other.table = table;
+ other.cap = cap;
+ other.size = size;
+
+ table = NULL;
+ size = cap = 0;
+ }
+
+ // NOTE: given a bit more time, I could make a more C++-style iterator out of this:
+ const vec<Pair>& bucket(int i) const { return table[i]; }
+};
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Options.cc b/libs/minisat/Options.cc
new file mode 100644
index 000000000..1aff3fab2
--- /dev/null
+++ b/libs/minisat/Options.cc
@@ -0,0 +1,94 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/**************************************************************************************[Options.cc]
+Copyright (c) 2008-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include "Sort.h"
+#include "Options.h"
+#include "ParseUtils.h"
+
+using namespace Minisat;
+
+void Minisat::parseOptions(int& argc, char** argv, bool strict)
+{
+ int i, j;
+ for (i = j = 1; i < argc; i++){
+ const char* str = argv[i];
+ if (match(str, "--") && match(str, Option::getHelpPrefixString()) && match(str, "help")){
+ if (*str == '\0')
+ printUsageAndExit(argc, argv);
+ else if (match(str, "-verb"))
+ printUsageAndExit(argc, argv, true);
+ } else {
+ bool parsed_ok = false;
+
+ for (int k = 0; !parsed_ok && k < Option::getOptionList().size(); k++){
+ parsed_ok = Option::getOptionList()[k]->parse(argv[i]);
+
+ // fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
+ }
+
+ if (!parsed_ok){
+ if (strict && match(argv[i], "-"))
+ fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
+ else
+ argv[j++] = argv[i];
+ }
+ }
+ }
+
+ argc -= (i - j);
+}
+
+
+void Minisat::setUsageHelp (const char* str){ Option::getUsageString() = str; }
+void Minisat::setHelpPrefixStr (const char* str){ Option::getHelpPrefixString() = str; }
+void Minisat::printUsageAndExit (int /*argc*/, char** argv, bool verbose)
+{
+ const char* usage = Option::getUsageString();
+ if (usage != NULL)
+ fprintf(stderr, usage, argv[0]);
+
+ sort(Option::getOptionList(), Option::OptionLt());
+
+ const char* prev_cat = NULL;
+ const char* prev_type = NULL;
+
+ for (int i = 0; i < Option::getOptionList().size(); i++){
+ const char* cat = Option::getOptionList()[i]->category;
+ const char* type = Option::getOptionList()[i]->type_name;
+
+ if (cat != prev_cat)
+ fprintf(stderr, "\n%s OPTIONS:\n\n", cat);
+ else if (type != prev_type)
+ fprintf(stderr, "\n");
+
+ Option::getOptionList()[i]->help(verbose);
+
+ prev_cat = Option::getOptionList()[i]->category;
+ prev_type = Option::getOptionList()[i]->type_name;
+ }
+
+ fprintf(stderr, "\nHELP OPTIONS:\n\n");
+ fprintf(stderr, " --%shelp Print help message.\n", Option::getHelpPrefixString());
+ fprintf(stderr, " --%shelp-verb Print verbose help message.\n", Option::getHelpPrefixString());
+ fprintf(stderr, "\n");
+ exit(0);
+}
+
diff --git a/libs/minisat/Options.h b/libs/minisat/Options.h
new file mode 100644
index 000000000..d602769cf
--- /dev/null
+++ b/libs/minisat/Options.h
@@ -0,0 +1,386 @@
+/***************************************************************************************[Options.h]
+Copyright (c) 2008-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Options_h
+#define Minisat_Options_h
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <math.h>
+#include <string.h>
+
+#include "IntTypes.h"
+#include "Vec.h"
+#include "ParseUtils.h"
+
+namespace Minisat {
+
+//==================================================================================================
+// Top-level option parse/help functions:
+
+
+extern void parseOptions (int& argc, char** argv, bool strict = false);
+extern void printUsageAndExit(int argc, char** argv, bool verbose = false);
+extern void setUsageHelp (const char* str);
+extern void setHelpPrefixStr (const char* str);
+
+
+//==================================================================================================
+// Options is an abstract class that gives the interface for all types options:
+
+
+class Option
+{
+ protected:
+ const char* name;
+ const char* description;
+ const char* category;
+ const char* type_name;
+
+ static vec<Option*>& getOptionList () { static vec<Option*> options; return options; }
+ static const char*& getUsageString() { static const char* usage_str; return usage_str; }
+ static const char*& getHelpPrefixString() { static const char* help_prefix_str = ""; return help_prefix_str; }
+
+ struct OptionLt {
+ bool operator()(const Option* x, const Option* y) {
+ int test1 = strcmp(x->category, y->category);
+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
+ }
+ };
+
+ Option(const char* name_,
+ const char* desc_,
+ const char* cate_,
+ const char* type_) :
+ name (name_)
+ , description(desc_)
+ , category (cate_)
+ , type_name (type_)
+ {
+ getOptionList().push(this);
+ }
+
+ public:
+ virtual ~Option() {}
+
+ virtual bool parse (const char* str) = 0;
+ virtual void help (bool verbose = false) = 0;
+
+ friend void parseOptions (int& argc, char** argv, bool strict);
+ friend void printUsageAndExit (int argc, char** argv, bool verbose);
+ friend void setUsageHelp (const char* str);
+ friend void setHelpPrefixStr (const char* str);
+};
+
+
+//==================================================================================================
+// Range classes with specialization for floating types:
+
+
+struct IntRange {
+ int begin;
+ int end;
+ IntRange(int b, int e) : begin(b), end(e) {}
+};
+
+struct Int64Range {
+ int64_t begin;
+ int64_t end;
+ Int64Range(int64_t b, int64_t e) : begin(b), end(e) {}
+};
+
+struct DoubleRange {
+ double begin;
+ double end;
+ bool begin_inclusive;
+ bool end_inclusive;
+ DoubleRange(double b, bool binc, double e, bool einc) : begin(b), end(e), begin_inclusive(binc), end_inclusive(einc) {}
+};
+
+
+//==================================================================================================
+// Double options:
+
+
+class DoubleOption : public Option
+{
+ protected:
+ DoubleRange range;
+ double value;
+
+ public:
+ DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
+ : Option(n, d, c, "<double>"), range(r), value(def) {
+ // FIXME: set LC_NUMERIC to "C" to make sure that strtof/strtod parses decimal point correctly.
+ }
+
+ operator double (void) const { return value; }
+ operator double& (void) { return value; }
+ DoubleOption& operator=(double x) { value = x; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
+
+ char* end;
+ double tmp = strtod(span, &end);
+
+ if (end == NULL)
+ return false;
+ else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){
+ fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+ exit(1);
+ }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){
+ fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+ exit(1); }
+
+ value = tmp;
+ // fprintf(stderr, "READ VALUE: %g\n", value);
+
+ return true;
+ }
+
+ virtual void help (bool verbose = false){
+ fprintf(stderr, " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
+ name, type_name,
+ range.begin_inclusive ? '[' : '(',
+ range.begin,
+ range.end,
+ range.end_inclusive ? ']' : ')',
+ value);
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+
+
+//==================================================================================================
+// Int options:
+
+
+class IntOption : public Option
+{
+ protected:
+ IntRange range;
+ int32_t value;
+
+ public:
+ IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))
+ : Option(n, d, c, "<int32>"), range(r), value(def) {}
+
+ operator int32_t (void) const { return value; }
+ operator int32_t& (void) { return value; }
+ IntOption& operator= (int32_t x) { value = x; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
+
+ char* end;
+ int32_t tmp = strtol(span, &end, 10);
+
+ if (end == NULL)
+ return false;
+ else if (tmp > range.end){
+ fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+ exit(1);
+ }else if (tmp < range.begin){
+ fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+ exit(1); }
+
+ value = tmp;
+
+ return true;
+ }
+
+ virtual void help (bool verbose = false){
+ fprintf(stderr, " -%-12s = %-8s [", name, type_name);
+ if (range.begin == INT32_MIN)
+ fprintf(stderr, "imin");
+ else
+ fprintf(stderr, "%4d", range.begin);
+
+ fprintf(stderr, " .. ");
+ if (range.end == INT32_MAX)
+ fprintf(stderr, "imax");
+ else
+ fprintf(stderr, "%4d", range.end);
+
+ fprintf(stderr, "] (default: %d)\n", value);
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+
+
+// Leave this out for visual C++ until Microsoft implements C99 and gets support for strtoll.
+#ifndef _MSC_VER
+
+class Int64Option : public Option
+{
+ protected:
+ Int64Range range;
+ int64_t value;
+
+ public:
+ Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range(INT64_MIN, INT64_MAX))
+ : Option(n, d, c, "<int64>"), range(r), value(def) {}
+
+ operator int64_t (void) const { return value; }
+ operator int64_t& (void) { return value; }
+ Int64Option& operator= (int64_t x) { value = x; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
+
+ char* end;
+ int64_t tmp = strtoll(span, &end, 10);
+
+ if (end == NULL)
+ return false;
+ else if (tmp > range.end){
+ fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+ exit(1);
+ }else if (tmp < range.begin){
+ fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+ exit(1); }
+
+ value = tmp;
+
+ return true;
+ }
+
+ virtual void help (bool verbose = false){
+ fprintf(stderr, " -%-12s = %-8s [", name, type_name);
+ if (range.begin == INT64_MIN)
+ fprintf(stderr, "imin");
+ else
+ fprintf(stderr, "%4" PRIi64 , range.begin);
+
+ fprintf(stderr, " .. ");
+ if (range.end == INT64_MAX)
+ fprintf(stderr, "imax");
+ else
+ fprintf(stderr, "%4" PRIi64 , range.end);
+
+ fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+#endif
+
+//==================================================================================================
+// String option:
+
+
+class StringOption : public Option
+{
+ const char* value;
+ public:
+ StringOption(const char* c, const char* n, const char* d, const char* def = NULL)
+ : Option(n, d, c, "<string>"), value(def) {}
+
+ operator const char* (void) const { return value; }
+ operator const char*& (void) { return value; }
+ StringOption& operator= (const char* x) { value = x; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
+
+ value = span;
+ return true;
+ }
+
+ virtual void help (bool verbose = false){
+ fprintf(stderr, " -%-10s = %8s\n", name, type_name);
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+
+
+//==================================================================================================
+// Bool option:
+
+
+class BoolOption : public Option
+{
+ bool value;
+
+ public:
+ BoolOption(const char* c, const char* n, const char* d, bool v)
+ : Option(n, d, c, "<bool>"), value(v) {}
+
+ operator bool (void) const { return value; }
+ operator bool& (void) { return value; }
+ BoolOption& operator=(bool b) { value = b; return *this; }
+
+ virtual bool parse(const char* str){
+ const char* span = str;
+
+ if (match(span, "-")){
+ bool b = !match(span, "no-");
+
+ if (strcmp(span, name) == 0){
+ value = b;
+ return true; }
+ }
+
+ return false;
+ }
+
+ virtual void help (bool verbose = false){
+
+ fprintf(stderr, " -%s, -no-%s", name, name);
+
+ for (uint32_t i = 0; i < 32 - strlen(name)*2; i++)
+ fprintf(stderr, " ");
+
+ fprintf(stderr, " ");
+ fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
+ if (verbose){
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
+ }
+};
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/ParseUtils.h b/libs/minisat/ParseUtils.h
new file mode 100644
index 000000000..04911c70a
--- /dev/null
+++ b/libs/minisat/ParseUtils.h
@@ -0,0 +1,119 @@
+/************************************************************************************[ParseUtils.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_ParseUtils_h
+#define Minisat_ParseUtils_h
+
+#include <stdlib.h>
+#include <stdio.h>
+
+#include "XAlloc.h"
+
+namespace Minisat {
+
+//-------------------------------------------------------------------------------------------------
+// A simple buffered character stream class:
+
+
+
+class StreamBuffer {
+ unsigned char* buf;
+ int pos;
+ int size;
+
+ enum { buffer_size = 64*1024 };
+
+ virtual void assureLookahead() = 0;
+
+public:
+ virtual ~StreamBuffer() { }
+
+ int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
+ void operator ++ () { pos++; assureLookahead(); }
+ int position () const { return pos; }
+};
+
+
+//-------------------------------------------------------------------------------------------------
+// End-of-file detection functions for StreamBuffer and char*:
+
+
+static inline bool isEof(StreamBuffer& in) { return *in == EOF; }
+static inline bool isEof(const char* in) { return *in == '\0'; }
+
+//-------------------------------------------------------------------------------------------------
+// Generic parse functions parametrized over the input-stream type.
+
+
+template<class B>
+static void skipWhitespace(B& in) {
+ while ((*in >= 9 && *in <= 13) || *in == 32)
+ ++in; }
+
+
+template<class B>
+static void skipLine(B& in) {
+ for (;;){
+ if (isEof(in)) return;
+ if (*in == '\n') { ++in; return; }
+ ++in; } }
+
+
+template<class B>
+static int parseInt(B& in) {
+ int val = 0;
+ bool neg = false;
+ skipWhitespace(in);
+ if (*in == '-') neg = true, ++in;
+ else if (*in == '+') ++in;
+ if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
+ while (*in >= '0' && *in <= '9')
+ val = val*10 + (*in - '0'),
+ ++in;
+ return neg ? -val : val; }
+
+
+// String matching: in case of a match the input iterator will be advanced the corresponding
+// number of characters.
+template<class B>
+static bool match(B& in, const char* str) {
+ int i;
+ for (i = 0; str[i] != '\0'; i++)
+ if (in[i] != str[i])
+ return false;
+
+ in += i;
+
+ return true;
+}
+
+// String matching: consumes characters eagerly, but does not require random access iterator.
+template<class B>
+static bool eagerMatch(B& in, const char* str) {
+ for (; *str != '\0'; ++str, ++in)
+ if (*str != *in)
+ return false;
+ return true; }
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Queue.h b/libs/minisat/Queue.h
new file mode 100644
index 000000000..5ba50cd2b
--- /dev/null
+++ b/libs/minisat/Queue.h
@@ -0,0 +1,69 @@
+/*****************************************************************************************[Queue.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Queue_h
+#define Minisat_Queue_h
+
+#include "Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+
+template<class T>
+class Queue {
+ vec<T> buf;
+ int first;
+ int end;
+
+public:
+ typedef T Key;
+
+ Queue() : buf(1), first(0), end(0) {}
+
+ void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
+ int size () const { return (end >= first) ? end - first : end - first + buf.size(); }
+
+ const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+ T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+
+ T peek () const { assert(first != end); return buf[first]; }
+ void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; }
+ void insert(T elem) { // INVARIANT: buf[end] is always unused
+ buf[end++] = elem;
+ if (end == buf.size()) end = 0;
+ if (first == end){ // Resize:
+ vec<T> tmp((buf.size()*3 + 1) >> 1);
+ //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);
+ int i = 0;
+ for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j];
+ for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j];
+ first = 0;
+ end = buf.size();
+ tmp.moveTo(buf);
+ }
+ }
+};
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Rnd.h b/libs/minisat/Rnd.h
new file mode 100644
index 000000000..ccb94c6ce
--- /dev/null
+++ b/libs/minisat/Rnd.h
@@ -0,0 +1,67 @@
+/*******************************************************************************************[Rnd.h]
+Copyright (c) 2012, Niklas Sorensson
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Rnd_h
+#define Minisat_Rnd_h
+
+#include "Vec.h"
+
+namespace Minisat {
+
+// Generate a random double:
+static inline double drand(double& seed)
+{
+ seed *= 1389796;
+ int q = (int)(seed / 2147483647);
+ seed -= (double)q * 2147483647;
+ return seed / 2147483647;
+}
+
+
+// Generate a random integer:
+static inline int irand(double& seed, int size) { return (int)(drand(seed) * size); }
+
+
+// Randomly shuffle the contents of a vector:
+template<class T>
+static void randomShuffle(double& seed, vec<T>& xs)
+{
+ for (int i = 0; i < xs.size(); i++){
+ int pick = i + irand(seed, xs.size() - i);
+ T tmp = xs[i];
+ xs[i] = xs[pick];
+ xs[pick] = tmp;
+ }
+}
+
+// Randomly shuffle a vector of a vector (ugly)
+template<class T>
+static void randomShuffle(double& seed, vec<vec<T> >& xs)
+{
+ for (int i = 0; i < xs.size(); i++){
+ int pick = i + irand(seed, xs.size() - i);
+ vec<T> tmp; xs[i].moveTo(tmp);
+ xs[pick].moveTo(xs[i]);
+ tmp.moveTo(xs[pick]);
+ }
+}
+
+
+//=================================================================================================
+} // namespace Minisat
+#endif
diff --git a/libs/minisat/SimpSolver.cc b/libs/minisat/SimpSolver.cc
new file mode 100644
index 000000000..fd5774e0e
--- /dev/null
+++ b/libs/minisat/SimpSolver.cc
@@ -0,0 +1,727 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/***********************************************************************************[SimpSolver.cc]
+Copyright (c) 2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include "Sort.h"
+#include "SimpSolver.h"
+#include "System.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+// Options:
+
+
+static const char* _cat = "SIMP";
+
+static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false);
+static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false);
+static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true);
+static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
+static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX));
+static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
+static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false));
+
+
+//=================================================================================================
+// Constructor/Destructor:
+
+
+SimpSolver::SimpSolver() :
+ grow (opt_grow)
+ , clause_lim (opt_clause_lim)
+ , subsumption_lim (opt_subsumption_lim)
+ , simp_garbage_frac (opt_simp_garbage_frac)
+ , use_asymm (opt_use_asymm)
+ , use_rcheck (opt_use_rcheck)
+ , use_elim (opt_use_elim)
+ , extend_model (true)
+ , merges (0)
+ , asymm_lits (0)
+ , eliminated_vars (0)
+ , elimorder (1)
+ , use_simplification (true)
+ , occurs (ClauseDeleted(ca))
+ , elim_heap (ElimLt(n_occ))
+ , bwdsub_assigns (0)
+ , n_touched (0)
+{
+ vec<Lit> dummy(1,lit_Undef);
+ ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
+ bwdsub_tmpunit = ca.alloc(dummy);
+ remove_satisfied = false;
+}
+
+
+SimpSolver::~SimpSolver()
+{
+}
+
+
+Var SimpSolver::newVar(lbool upol, bool dvar) {
+ Var v = Solver::newVar(upol, dvar);
+
+ frozen .insert(v, (char)false);
+ eliminated.insert(v, (char)false);
+
+ if (use_simplification){
+ n_occ .insert( mkLit(v), 0);
+ n_occ .insert(~mkLit(v), 0);
+ occurs .init (v);
+ touched .insert(v, 0);
+ elim_heap .insert(v);
+ }
+ return v; }
+
+
+void SimpSolver::releaseVar(Lit l)
+{
+ assert(!isEliminated(var(l)));
+ if (!use_simplification && var(l) >= max_simp_var)
+ // Note: Guarantees that no references to this variable is
+ // left in model extension datastructure. Could be improved!
+ Solver::releaseVar(l);
+ else
+ // Otherwise, don't allow variable to be reused.
+ Solver::addClause(l);
+}
+
+
+lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
+{
+ vec<Var> extra_frozen;
+ lbool result = l_True;
+
+ do_simp &= use_simplification;
+
+ if (do_simp){
+ // Assumptions must be temporarily frozen to run variable elimination:
+ for (int i = 0; i < assumptions.size(); i++){
+ Var v = var(assumptions[i]);
+
+ // If an assumption has been eliminated, remember it.
+ assert(!isEliminated(v));
+
+ if (!frozen[v]){
+ // Freeze and store.
+ setFrozen(v, true);
+ extra_frozen.push(v);
+ } }
+
+ result = lbool(eliminate(turn_off_simp));
+ }
+
+ if (result == l_True)
+ result = Solver::solve_();
+ else if (verbosity >= 1)
+ printf("===============================================================================\n");
+
+ if (result == l_True && extend_model)
+ extendModel();
+
+ if (do_simp)
+ // Unfreeze the assumptions that were frozen:
+ for (int i = 0; i < extra_frozen.size(); i++)
+ setFrozen(extra_frozen[i], false);
+
+ return result;
+}
+
+
+
+bool SimpSolver::addClause_(vec<Lit>& ps)
+{
+#ifndef NDEBUG
+ for (int i = 0; i < ps.size(); i++)
+ assert(!isEliminated(var(ps[i])));
+#endif
+
+ int nclauses = clauses.size();
+
+ if (use_rcheck && implied(ps))
+ return true;
+
+ if (!Solver::addClause_(ps))
+ return false;
+
+ if (use_simplification && clauses.size() == nclauses + 1){
+ CRef cr = clauses.last();
+ const Clause& c = ca[cr];
+
+ // NOTE: the clause is added to the queue immediately and then
+ // again during 'gatherTouchedClauses()'. If nothing happens
+ // in between, it will only be checked once. Otherwise, it may
+ // be checked twice unnecessarily. This is an unfortunate
+ // consequence of how backward subsumption is used to mimic
+ // forward subsumption.
+ subsumption_queue.insert(cr);
+ for (int i = 0; i < c.size(); i++){
+ occurs[var(c[i])].push(cr);
+ n_occ[c[i]]++;
+ touched[var(c[i])] = 1;
+ n_touched++;
+ if (elim_heap.inHeap(var(c[i])))
+ elim_heap.increase(var(c[i]));
+ }
+ }
+
+ return true;
+}
+
+
+void SimpSolver::removeClause(CRef cr)
+{
+ const Clause& c = ca[cr];
+
+ if (use_simplification)
+ for (int i = 0; i < c.size(); i++){
+ n_occ[c[i]]--;
+ updateElimHeap(var(c[i]));
+ occurs.smudge(var(c[i]));
+ }
+
+ Solver::removeClause(cr);
+}
+
+
+bool SimpSolver::strengthenClause(CRef cr, Lit l)
+{
+ Clause& c = ca[cr];
+ assert(decisionLevel() == 0);
+ assert(use_simplification);
+
+ // FIX: this is too inefficient but would be nice to have (properly implemented)
+ // if (!find(subsumption_queue, &c))
+ subsumption_queue.insert(cr);
+
+ if (c.size() == 2){
+ removeClause(cr);
+ c.strengthen(l);
+ }else{
+ detachClause(cr, true);
+ c.strengthen(l);
+ attachClause(cr);
+ remove(occurs[var(l)], cr);
+ n_occ[l]--;
+ updateElimHeap(var(l));
+ }
+
+ return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
+}
+
+
+// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
+{
+ merges++;
+ out_clause.clear();
+
+ bool ps_smallest = _ps.size() < _qs.size();
+ const Clause& ps = ps_smallest ? _qs : _ps;
+ const Clause& qs = ps_smallest ? _ps : _qs;
+
+ for (int i = 0; i < qs.size(); i++){
+ if (var(qs[i]) != v){
+ for (int j = 0; j < ps.size(); j++)
+ if (var(ps[j]) == var(qs[i])){
+ if (ps[j] == ~qs[i])
+ return false;
+ else
+ goto next;
+ }
+ out_clause.push(qs[i]);
+ }
+ next:;
+ }
+
+ for (int i = 0; i < ps.size(); i++)
+ if (var(ps[i]) != v)
+ out_clause.push(ps[i]);
+
+ return true;
+}
+
+
+// Returns FALSE if clause is always satisfied.
+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
+{
+ merges++;
+
+ bool ps_smallest = _ps.size() < _qs.size();
+ const Clause& ps = ps_smallest ? _qs : _ps;
+ const Clause& qs = ps_smallest ? _ps : _qs;
+ const Lit* __ps = (const Lit*)ps;
+ const Lit* __qs = (const Lit*)qs;
+
+ size = ps.size()-1;
+
+ for (int i = 0; i < qs.size(); i++){
+ if (var(__qs[i]) != v){
+ for (int j = 0; j < ps.size(); j++)
+ if (var(__ps[j]) == var(__qs[i])){
+ if (__ps[j] == ~__qs[i])
+ return false;
+ else
+ goto next;
+ }
+ size++;
+ }
+ next:;
+ }
+
+ return true;
+}
+
+
+void SimpSolver::gatherTouchedClauses()
+{
+ if (n_touched == 0) return;
+
+ int i,j;
+ for (i = j = 0; i < subsumption_queue.size(); i++)
+ if (ca[subsumption_queue[i]].mark() == 0)
+ ca[subsumption_queue[i]].mark(2);
+
+ for (i = 0; i < nVars(); i++)
+ if (touched[i]){
+ const vec<CRef>& cs = occurs.lookup(i);
+ for (j = 0; j < cs.size(); j++)
+ if (ca[cs[j]].mark() == 0){
+ subsumption_queue.insert(cs[j]);
+ ca[cs[j]].mark(2);
+ }
+ touched[i] = 0;
+ }
+
+ for (i = 0; i < subsumption_queue.size(); i++)
+ if (ca[subsumption_queue[i]].mark() == 2)
+ ca[subsumption_queue[i]].mark(0);
+
+ n_touched = 0;
+}
+
+
+bool SimpSolver::implied(const vec<Lit>& c)
+{
+ assert(decisionLevel() == 0);
+
+ trail_lim.push(trail.size());
+ for (int i = 0; i < c.size(); i++)
+ if (value(c[i]) == l_True){
+ cancelUntil(0);
+ return true;
+ }else if (value(c[i]) != l_False){
+ assert(value(c[i]) == l_Undef);
+ uncheckedEnqueue(~c[i]);
+ }
+
+ bool result = propagate() != CRef_Undef;
+ cancelUntil(0);
+ return result;
+}
+
+
+// Backward subsumption + backward subsumption resolution
+bool SimpSolver::backwardSubsumptionCheck(bool verbose)
+{
+ int cnt = 0;
+ int subsumed = 0;
+ int deleted_literals = 0;
+ assert(decisionLevel() == 0);
+
+ while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
+
+ // Empty subsumption queue and return immediately on user-interrupt:
+ if (asynch_interrupt){
+ subsumption_queue.clear();
+ bwdsub_assigns = trail.size();
+ break; }
+
+ // Check top-level assignments by creating a dummy clause and placing it in the queue:
+ if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
+ Lit l = trail[bwdsub_assigns++];
+ ca[bwdsub_tmpunit][0] = l;
+ ca[bwdsub_tmpunit].calcAbstraction();
+ subsumption_queue.insert(bwdsub_tmpunit); }
+
+ CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
+ Clause& c = ca[cr];
+
+ if (c.mark()) continue;
+
+ if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
+ printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
+
+ assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
+
+ // Find best variable to scan:
+ Var best = var(c[0]);
+ for (int i = 1; i < c.size(); i++)
+ if (occurs[var(c[i])].size() < occurs[best].size())
+ best = var(c[i]);
+
+ // Search all candidates:
+ vec<CRef>& _cs = occurs.lookup(best);
+ CRef* cs = (CRef*)_cs;
+
+ for (int j = 0; j < _cs.size(); j++)
+ if (c.mark())
+ break;
+ else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
+ Lit l = c.subsumes(ca[cs[j]]);
+
+ if (l == lit_Undef)
+ subsumed++, removeClause(cs[j]);
+ else if (l != lit_Error){
+ deleted_literals++;
+
+ if (!strengthenClause(cs[j], ~l))
+ return false;
+
+ // Did current candidate get deleted from cs? Then check candidate at index j again:
+ if (var(l) == best)
+ j--;
+ }
+ }
+ }
+
+ return true;
+}
+
+
+bool SimpSolver::asymm(Var v, CRef cr)
+{
+ Clause& c = ca[cr];
+ assert(decisionLevel() == 0);
+
+ if (c.mark() || satisfied(c)) return true;
+
+ trail_lim.push(trail.size());
+ Lit l = lit_Undef;
+ for (int i = 0; i < c.size(); i++)
+ if (var(c[i]) != v && value(c[i]) != l_False)
+ uncheckedEnqueue(~c[i]);
+ else
+ l = c[i];
+
+ if (propagate() != CRef_Undef){
+ cancelUntil(0);
+ asymm_lits++;
+ if (!strengthenClause(cr, l))
+ return false;
+ }else
+ cancelUntil(0);
+
+ return true;
+}
+
+
+bool SimpSolver::asymmVar(Var v)
+{
+ assert(use_simplification);
+
+ const vec<CRef>& cls = occurs.lookup(v);
+
+ if (value(v) != l_Undef || cls.size() == 0)
+ return true;
+
+ for (int i = 0; i < cls.size(); i++)
+ if (!asymm(v, cls[i]))
+ return false;
+
+ return backwardSubsumptionCheck();
+}
+
+
+static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
+{
+ elimclauses.push(toInt(x));
+ elimclauses.push(1);
+}
+
+
+static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
+{
+ int first = elimclauses.size();
+ int v_pos = -1;
+
+ // Copy clause to elimclauses-vector. Remember position where the
+ // variable 'v' occurs:
+ for (int i = 0; i < c.size(); i++){
+ elimclauses.push(toInt(c[i]));
+ if (var(c[i]) == v)
+ v_pos = i + first;
+ }
+ assert(v_pos != -1);
+
+ // Swap the first literal with the 'v' literal, so that the literal
+ // containing 'v' will occur first in the clause:
+ uint32_t tmp = elimclauses[v_pos];
+ elimclauses[v_pos] = elimclauses[first];
+ elimclauses[first] = tmp;
+
+ // Store the length of the clause last:
+ elimclauses.push(c.size());
+}
+
+
+
+bool SimpSolver::eliminateVar(Var v)
+{
+ assert(!frozen[v]);
+ assert(!isEliminated(v));
+ assert(value(v) == l_Undef);
+
+ // Split the occurrences into positive and negative:
+ //
+ const vec<CRef>& cls = occurs.lookup(v);
+ vec<CRef> pos, neg;
+ for (int i = 0; i < cls.size(); i++)
+ (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
+
+ // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
+ // clause must exceed the limit on the maximal clause size (if it is set):
+ //
+ int cnt = 0;
+ int clause_size = 0;
+
+ for (int i = 0; i < pos.size(); i++)
+ for (int j = 0; j < neg.size(); j++)
+ if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
+ (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
+ return true;
+
+ // Delete and store old clauses:
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ eliminated_vars++;
+
+ if (pos.size() > neg.size()){
+ for (int i = 0; i < neg.size(); i++)
+ mkElimClause(elimclauses, v, ca[neg[i]]);
+ mkElimClause(elimclauses, mkLit(v));
+ }else{
+ for (int i = 0; i < pos.size(); i++)
+ mkElimClause(elimclauses, v, ca[pos[i]]);
+ mkElimClause(elimclauses, ~mkLit(v));
+ }
+
+ for (int i = 0; i < cls.size(); i++)
+ removeClause(cls[i]);
+
+ // Produce clauses in cross product:
+ vec<Lit>& resolvent = add_tmp;
+ for (int i = 0; i < pos.size(); i++)
+ for (int j = 0; j < neg.size(); j++)
+ if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
+ return false;
+
+ // Free occurs list for this variable:
+ occurs[v].clear(true);
+
+ // Free watchers lists for this variable, if possible:
+ if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
+ if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
+
+ return backwardSubsumptionCheck();
+}
+
+
+bool SimpSolver::substitute(Var v, Lit x)
+{
+ assert(!frozen[v]);
+ assert(!isEliminated(v));
+ assert(value(v) == l_Undef);
+
+ if (!ok) return false;
+
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ const vec<CRef>& cls = occurs.lookup(v);
+
+ vec<Lit>& subst_clause = add_tmp;
+ for (int i = 0; i < cls.size(); i++){
+ Clause& c = ca[cls[i]];
+
+ subst_clause.clear();
+ for (int j = 0; j < c.size(); j++){
+ Lit p = c[j];
+ subst_clause.push(var(p) == v ? x ^ sign(p) : p);
+ }
+
+ removeClause(cls[i]);
+
+ if (!addClause_(subst_clause))
+ return ok = false;
+ }
+
+ return true;
+}
+
+
+void SimpSolver::extendModel()
+{
+ int i, j;
+ Lit x;
+
+ for (i = elimclauses.size()-1; i > 0; i -= j){
+ for (j = elimclauses[i--]; j > 1; j--, i--)
+ if (modelValue(toLit(elimclauses[i])) != l_False)
+ goto next;
+
+ x = toLit(elimclauses[i]);
+ model[var(x)] = lbool(!sign(x));
+ next:;
+ }
+}
+
+
+bool SimpSolver::eliminate(bool turn_off_elim)
+{
+ if (!simplify())
+ return false;
+ else if (!use_simplification)
+ return true;
+
+ // Main simplification loop:
+ //
+ while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
+
+ gatherTouchedClauses();
+ // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
+ if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
+ !backwardSubsumptionCheck(true)){
+ ok = false; goto cleanup; }
+
+ // Empty elim_heap and return immediately on user-interrupt:
+ if (asynch_interrupt){
+ assert(bwdsub_assigns == trail.size());
+ assert(subsumption_queue.size() == 0);
+ assert(n_touched == 0);
+ elim_heap.clear();
+ goto cleanup; }
+
+ // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
+ for (int cnt = 0; !elim_heap.empty(); cnt++){
+ Var elim = elim_heap.removeMin();
+
+ if (asynch_interrupt) break;
+
+ if (isEliminated(elim) || value(elim) != l_Undef) continue;
+
+ if (verbosity >= 2 && cnt % 100 == 0)
+ printf("elimination left: %10d\r", elim_heap.size());
+
+ if (use_asymm){
+ // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
+ bool was_frozen = frozen[elim];
+ frozen[elim] = true;
+ if (!asymmVar(elim)){
+ ok = false; goto cleanup; }
+ frozen[elim] = was_frozen; }
+
+ // At this point, the variable may have been set by assymetric branching, so check it
+ // again. Also, don't eliminate frozen variables:
+ if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
+ ok = false; goto cleanup; }
+
+ checkGarbage(simp_garbage_frac);
+ }
+
+ assert(subsumption_queue.size() == 0);
+ }
+ cleanup:
+
+ // If no more simplification is needed, free all simplification-related data structures:
+ if (turn_off_elim){
+ touched .clear(true);
+ occurs .clear(true);
+ n_occ .clear(true);
+ elim_heap.clear(true);
+ subsumption_queue.clear(true);
+
+ use_simplification = false;
+ remove_satisfied = true;
+ ca.extra_clause_field = false;
+ max_simp_var = nVars();
+
+ // Force full cleanup (this is safe and desirable since it only happens once):
+ rebuildOrderHeap();
+ garbageCollect();
+ }else{
+ // Cheaper cleanup:
+ checkGarbage();
+ }
+
+ if (verbosity >= 1 && elimclauses.size() > 0)
+ printf("| Eliminated clauses: %10.2f Mb |\n",
+ double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+
+ return ok;
+}
+
+
+//=================================================================================================
+// Garbage Collection methods:
+
+
+void SimpSolver::relocAll(ClauseAllocator& to)
+{
+ if (!use_simplification) return;
+
+ // All occurs lists:
+ //
+ for (int i = 0; i < nVars(); i++){
+ occurs.clean(i);
+ vec<CRef>& cs = occurs[i];
+ for (int j = 0; j < cs.size(); j++)
+ ca.reloc(cs[j], to);
+ }
+
+ // Subsumption queue:
+ //
+ for (int i = subsumption_queue.size(); i > 0; i--){
+ CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
+ if (ca[cr].mark()) continue;
+ ca.reloc(cr, to);
+ subsumption_queue.insert(cr);
+ }
+
+ // Temporary clause:
+ //
+ ca.reloc(bwdsub_tmpunit, to);
+}
+
+
+void SimpSolver::garbageCollect()
+{
+ // Initialize the next region to a size corresponding to the estimated utilization degree. This
+ // is not precise but should avoid some unnecessary reallocations for the new region:
+ ClauseAllocator to(ca.size() - ca.wasted());
+
+ to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
+ relocAll(to);
+ Solver::relocAll(to);
+ if (verbosity >= 2)
+ printf("| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ to.moveTo(ca);
+}
diff --git a/libs/minisat/SimpSolver.h b/libs/minisat/SimpSolver.h
new file mode 100644
index 000000000..76d5aca1f
--- /dev/null
+++ b/libs/minisat/SimpSolver.h
@@ -0,0 +1,222 @@
+/************************************************************************************[SimpSolver.h]
+Copyright (c) 2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_SimpSolver_h
+#define Minisat_SimpSolver_h
+
+#include "Queue.h"
+#include "Solver.h"
+
+
+namespace Minisat {
+
+//=================================================================================================
+
+
+class SimpSolver : public Solver {
+ public:
+ // Constructor/Destructor:
+ //
+ SimpSolver();
+ ~SimpSolver();
+
+ // Problem specification:
+ //
+ Var newVar (lbool upol = l_Undef, bool dvar = true);
+ void releaseVar(Lit l);
+ bool addClause (const vec<Lit>& ps);
+ bool addEmptyClause(); // Add the empty clause to the solver.
+ bool addClause (Lit p); // Add a unit clause to the solver.
+ bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r, Lit s); // Add a quaternary clause to the solver.
+ bool addClause_( vec<Lit>& ps);
+ bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
+
+ // Variable mode:
+ //
+ void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
+ bool isEliminated(Var v) const;
+
+ // Alternative freeze interface (may replace 'setFrozen()'):
+ void freezeVar (Var v); // Freeze one variable so it will not be eliminated.
+ void thaw (); // Thaw all frozen variables.
+
+
+ // Solving:
+ //
+ bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+ lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+ bool solve ( bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
+ bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
+
+ // Memory managment:
+ //
+ virtual void garbageCollect();
+
+
+ // Generate a (possibly simplified) DIMACS file:
+ //
+#if 0
+ void toDimacs (const char* file, const vec<Lit>& assumps);
+ void toDimacs (const char* file);
+ void toDimacs (const char* file, Lit p);
+ void toDimacs (const char* file, Lit p, Lit q);
+ void toDimacs (const char* file, Lit p, Lit q, Lit r);
+#endif
+
+ // Mode of operation:
+ //
+ int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
+ int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
+ // -1 means no limit.
+ int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
+ double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
+
+ bool use_asymm; // Shrink clauses by asymmetric branching.
+ bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
+ bool use_elim; // Perform variable elimination.
+ bool extend_model; // Flag to indicate whether the user needs to look at the full model.
+
+ // Statistics:
+ //
+ int merges;
+ int asymm_lits;
+ int eliminated_vars;
+
+ protected:
+
+ // Helper structures:
+ //
+ struct ElimLt {
+ const LMap<int>& n_occ;
+ explicit ElimLt(const LMap<int>& no) : n_occ(no) {}
+
+ // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
+ // 32-bit implementation instead then, but this will have to do for now.
+ uint64_t cost (Var x) const { return (uint64_t)n_occ[mkLit(x)] * (uint64_t)n_occ[~mkLit(x)]; }
+ bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
+
+ // TODO: investigate this order alternative more.
+ // bool operator()(Var x, Var y) const {
+ // int c_x = cost(x);
+ // int c_y = cost(y);
+ // return c_x < c_y || c_x == c_y && x < y; }
+ };
+
+ struct ClauseDeleted {
+ const ClauseAllocator& ca;
+ explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+ bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
+
+ // Solver state:
+ //
+ int elimorder;
+ bool use_simplification;
+ Var max_simp_var; // Max variable at the point simplification was turned off.
+ vec<uint32_t> elimclauses;
+ VMap<char> touched;
+ OccLists<Var, vec<CRef>, ClauseDeleted>
+ occurs;
+ LMap<int> n_occ;
+ Heap<Var,ElimLt> elim_heap;
+ Queue<CRef> subsumption_queue;
+ VMap<char> frozen;
+ vec<Var> frozen_vars;
+ VMap<char> eliminated;
+ int bwdsub_assigns;
+ int n_touched;
+
+ // Temporaries:
+ //
+ CRef bwdsub_tmpunit;
+
+ // Main internal methods:
+ //
+ lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
+ bool asymm (Var v, CRef cr);
+ bool asymmVar (Var v);
+ void updateElimHeap (Var v);
+ void gatherTouchedClauses ();
+ bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
+ bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
+ bool backwardSubsumptionCheck (bool verbose = false);
+ bool eliminateVar (Var v);
+ void extendModel ();
+
+ void removeClause (CRef cr);
+ bool strengthenClause (CRef cr, Lit l);
+ bool implied (const vec<Lit>& c);
+ void relocAll (ClauseAllocator& to);
+};
+
+
+//=================================================================================================
+// Implementation of inline methods:
+
+
+inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
+inline void SimpSolver::updateElimHeap(Var v) {
+ assert(use_simplification);
+ // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+ if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
+ elim_heap.update(v); }
+
+
+inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
+inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, Lit s){ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); add_tmp.push(s); return addClause_(add_tmp); }
+inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
+
+inline void SimpSolver::freezeVar(Var v){
+ if (!frozen[v]){
+ frozen[v] = 1;
+ frozen_vars.push(v);
+ } }
+
+inline void SimpSolver::thaw(){
+ for (int i = 0; i < frozen_vars.size(); i++){
+ Var v = frozen_vars[i];
+ frozen[v] = 0;
+ if (use_simplification)
+ updateElimHeap(v);
+ }
+ frozen_vars.clear(); }
+
+inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
+ budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
+
+inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
+ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Solver.cc b/libs/minisat/Solver.cc
new file mode 100644
index 000000000..ab476853a
--- /dev/null
+++ b/libs/minisat/Solver.cc
@@ -0,0 +1,1068 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/***************************************************************************************[Solver.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include <math.h>
+
+#include "Alg.h"
+#include "Sort.h"
+#include "System.h"
+#include "Solver.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+// Options:
+
+
+static const char* _cat = "CORE";
+
+static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.95, DoubleRange(0, false, 1, false));
+static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false));
+static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
+static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false));
+static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
+static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
+static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false);
+static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true);
+static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX));
+static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false));
+static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false));
+static IntOption opt_min_learnts_lim (_cat, "min-learnts", "Minimum learnt clause limit", 0, IntRange(0, INT32_MAX));
+
+
+//=================================================================================================
+// Constructor/Destructor:
+
+
+Solver::Solver() :
+
+ // Parameters (user settable):
+ //
+ verbosity (0)
+ , var_decay (opt_var_decay)
+ , clause_decay (opt_clause_decay)
+ , random_var_freq (opt_random_var_freq)
+ , random_seed (opt_random_seed)
+ , luby_restart (opt_luby_restart)
+ , ccmin_mode (opt_ccmin_mode)
+ , phase_saving (opt_phase_saving)
+ , rnd_pol (false)
+ , rnd_init_act (opt_rnd_init_act)
+ , garbage_frac (opt_garbage_frac)
+ , min_learnts_lim (opt_min_learnts_lim)
+ , restart_first (opt_restart_first)
+ , restart_inc (opt_restart_inc)
+
+ // Parameters (the rest):
+ //
+ , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
+
+ // Parameters (experimental):
+ //
+ , learntsize_adjust_start_confl (100)
+ , learntsize_adjust_inc (1.5)
+
+ // Statistics: (formerly in 'SolverStats')
+ //
+ , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
+ , dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
+
+ , watches (WatcherDeleted(ca))
+ , order_heap (VarOrderLt(activity))
+ , ok (true)
+ , cla_inc (1)
+ , var_inc (1)
+ , qhead (0)
+ , simpDB_assigns (-1)
+ , simpDB_props (0)
+ , progress_estimate (0)
+ , remove_satisfied (true)
+ , next_var (0)
+
+ // Resource constraints:
+ //
+ , conflict_budget (-1)
+ , propagation_budget (-1)
+ , asynch_interrupt (false)
+{}
+
+
+Solver::~Solver()
+{
+}
+
+
+//=================================================================================================
+// Minor methods:
+
+
+// Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be
+// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
+//
+Var Solver::newVar(lbool upol, bool dvar)
+{
+ Var v;
+ if (free_vars.size() > 0){
+ v = free_vars.last();
+ free_vars.pop();
+ }else
+ v = next_var++;
+
+ watches .init(mkLit(v, false));
+ watches .init(mkLit(v, true ));
+ assigns .insert(v, l_Undef);
+ vardata .insert(v, mkVarData(CRef_Undef, 0));
+ activity .insert(v, rnd_init_act ? drand(random_seed) * 0.00001 : 0);
+ seen .insert(v, 0);
+ polarity .insert(v, true);
+ user_pol .insert(v, upol);
+ decision .reserve(v);
+ trail .capacity(v+1);
+ setDecisionVar(v, dvar);
+ return v;
+}
+
+
+// Note: at the moment, only unassigned variable will be released (this is to avoid duplicate
+// releases of the same variable).
+void Solver::releaseVar(Lit l)
+{
+ if (value(l) == l_Undef){
+ addClause(l);
+ released_vars.push(var(l));
+ }
+}
+
+
+bool Solver::addClause_(vec<Lit>& ps)
+{
+ assert(decisionLevel() == 0);
+ if (!ok) return false;
+
+ // Check if clause is satisfied and remove false/duplicate literals:
+ sort(ps);
+ Lit p; int i, j;
+ for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
+ if (value(ps[i]) == l_True || ps[i] == ~p)
+ return true;
+ else if (value(ps[i]) != l_False && ps[i] != p)
+ ps[j++] = p = ps[i];
+ ps.shrink(i - j);
+
+ if (ps.size() == 0)
+ return ok = false;
+ else if (ps.size() == 1){
+ uncheckedEnqueue(ps[0]);
+ return ok = (propagate() == CRef_Undef);
+ }else{
+ CRef cr = ca.alloc(ps, false);
+ clauses.push(cr);
+ attachClause(cr);
+ }
+
+ return true;
+}
+
+
+void Solver::attachClause(CRef cr){
+ const Clause& c = ca[cr];
+ assert(c.size() > 1);
+ watches[~c[0]].push(Watcher(cr, c[1]));
+ watches[~c[1]].push(Watcher(cr, c[0]));
+ if (c.learnt()) num_learnts++, learnts_literals += c.size();
+ else num_clauses++, clauses_literals += c.size();
+}
+
+
+void Solver::detachClause(CRef cr, bool strict){
+ const Clause& c = ca[cr];
+ assert(c.size() > 1);
+
+ // Strict or lazy detaching:
+ if (strict){
+ remove(watches[~c[0]], Watcher(cr, c[1]));
+ remove(watches[~c[1]], Watcher(cr, c[0]));
+ }else{
+ watches.smudge(~c[0]);
+ watches.smudge(~c[1]);
+ }
+
+ if (c.learnt()) num_learnts--, learnts_literals -= c.size();
+ else num_clauses--, clauses_literals -= c.size();
+}
+
+
+void Solver::removeClause(CRef cr) {
+ Clause& c = ca[cr];
+ detachClause(cr);
+ // Don't leave pointers to free'd memory!
+ if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
+ c.mark(1);
+ ca.free(cr);
+}
+
+
+bool Solver::satisfied(const Clause& c) const {
+ for (int i = 0; i < c.size(); i++)
+ if (value(c[i]) == l_True)
+ return true;
+ return false; }
+
+
+// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
+//
+void Solver::cancelUntil(int level) {
+ if (decisionLevel() > level){
+ for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+ Var x = var(trail[c]);
+ assigns [x] = l_Undef;
+ if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last()))
+ polarity[x] = sign(trail[c]);
+ insertVarOrder(x); }
+ qhead = trail_lim[level];
+ trail.shrink(trail.size() - trail_lim[level]);
+ trail_lim.shrink(trail_lim.size() - level);
+ } }
+
+
+//=================================================================================================
+// Major methods:
+
+
+Lit Solver::pickBranchLit()
+{
+ Var next = var_Undef;
+
+ // Random decision:
+ if (drand(random_seed) < random_var_freq && !order_heap.empty()){
+ next = order_heap[irand(random_seed,order_heap.size())];
+ if (value(next) == l_Undef && decision[next])
+ rnd_decisions++; }
+
+ // Activity based decision:
+ while (next == var_Undef || value(next) != l_Undef || !decision[next])
+ if (order_heap.empty()){
+ next = var_Undef;
+ break;
+ }else
+ next = order_heap.removeMin();
+
+ // Choose polarity based on different polarity modes (global or per-variable):
+ if (next == var_Undef)
+ return lit_Undef;
+ else if (user_pol[next] != l_Undef)
+ return mkLit(next, user_pol[next] == l_True);
+ else if (rnd_pol)
+ return mkLit(next, drand(random_seed) < 0.5);
+ else
+ return mkLit(next, polarity[next]);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
+|
+| Description:
+| Analyze conflict and produce a reason clause.
+|
+| Pre-conditions:
+| * 'out_learnt' is assumed to be cleared.
+| * Current decision level must be greater than root level.
+|
+| Post-conditions:
+| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
+| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
+| rest of literals. There may be others from the same level though.
+|
+|________________________________________________________________________________________________@*/
+void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
+{
+ int pathC = 0;
+ Lit p = lit_Undef;
+
+ // Generate conflict clause:
+ //
+ out_learnt.push(); // (leave room for the asserting literal)
+ int index = trail.size() - 1;
+
+ do{
+ assert(confl != CRef_Undef); // (otherwise should be UIP)
+ Clause& c = ca[confl];
+
+ if (c.learnt())
+ claBumpActivity(c);
+
+ for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
+ Lit q = c[j];
+
+ if (!seen[var(q)] && level(var(q)) > 0){
+ varBumpActivity(var(q));
+ seen[var(q)] = 1;
+ if (level(var(q)) >= decisionLevel())
+ pathC++;
+ else
+ out_learnt.push(q);
+ }
+ }
+
+ // Select next clause to look at:
+ while (!seen[var(trail[index--])]);
+ p = trail[index+1];
+ confl = reason(var(p));
+ seen[var(p)] = 0;
+ pathC--;
+
+ }while (pathC > 0);
+ out_learnt[0] = ~p;
+
+ // Simplify conflict clause:
+ //
+ int i, j;
+ out_learnt.copyTo(analyze_toclear);
+ if (ccmin_mode == 2){
+ for (i = j = 1; i < out_learnt.size(); i++)
+ if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i]))
+ out_learnt[j++] = out_learnt[i];
+
+ }else if (ccmin_mode == 1){
+ for (i = j = 1; i < out_learnt.size(); i++){
+ Var x = var(out_learnt[i]);
+
+ if (reason(x) == CRef_Undef)
+ out_learnt[j++] = out_learnt[i];
+ else{
+ Clause& c = ca[reason(var(out_learnt[i]))];
+ for (int k = 1; k < c.size(); k++)
+ if (!seen[var(c[k])] && level(var(c[k])) > 0){
+ out_learnt[j++] = out_learnt[i];
+ break; }
+ }
+ }
+ }else
+ i = j = out_learnt.size();
+
+ max_literals += out_learnt.size();
+ out_learnt.shrink(i - j);
+ tot_literals += out_learnt.size();
+
+ // Find correct backtrack level:
+ //
+ if (out_learnt.size() == 1)
+ out_btlevel = 0;
+ else{
+ int max_i = 1;
+ // Find the first literal assigned at the next-highest level:
+ for (int i = 2; i < out_learnt.size(); i++)
+ if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
+ max_i = i;
+ // Swap-in this literal at index 1:
+ Lit p = out_learnt[max_i];
+ out_learnt[max_i] = out_learnt[1];
+ out_learnt[1] = p;
+ out_btlevel = level(var(p));
+ }
+
+ for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
+}
+
+
+// Check if 'p' can be removed from a conflict clause.
+bool Solver::litRedundant(Lit p)
+{
+ enum { seen_undef = 0, seen_source = 1, seen_removable = 2, seen_failed = 3 };
+ assert(seen[var(p)] == seen_undef || seen[var(p)] == seen_source);
+ assert(reason(var(p)) != CRef_Undef);
+
+ Clause* c = &ca[reason(var(p))];
+ vec<ShrinkStackElem>& stack = analyze_stack;
+ stack.clear();
+
+ for (uint32_t i = 1; ; i++){
+ if (i < (uint32_t)c->size()){
+ // Checking 'p'-parents 'l':
+ Lit l = (*c)[i];
+
+ // Variable at level 0 or previously removable:
+ if (level(var(l)) == 0 || seen[var(l)] == seen_source || seen[var(l)] == seen_removable){
+ continue; }
+
+ // Check variable can not be removed for some local reason:
+ if (reason(var(l)) == CRef_Undef || seen[var(l)] == seen_failed){
+ stack.push(ShrinkStackElem(0, p));
+ for (int i = 0; i < stack.size(); i++)
+ if (seen[var(stack[i].l)] == seen_undef){
+ seen[var(stack[i].l)] = seen_failed;
+ analyze_toclear.push(stack[i].l);
+ }
+
+ return false;
+ }
+
+ // Recursively check 'l':
+ stack.push(ShrinkStackElem(i, p));
+ i = 0;
+ p = l;
+ c = &ca[reason(var(p))];
+ }else{
+ // Finished with current element 'p' and reason 'c':
+ if (seen[var(p)] == seen_undef){
+ seen[var(p)] = seen_removable;
+ analyze_toclear.push(p);
+ }
+
+ // Terminate with success if stack is empty:
+ if (stack.size() == 0) break;
+
+ // Continue with top element on stack:
+ i = stack.last().i;
+ p = stack.last().l;
+ c = &ca[reason(var(p))];
+
+ stack.pop();
+ }
+ }
+
+ return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+| analyzeFinal : (p : Lit) -> [void]
+|
+| Description:
+| Specialized analysis procedure to express the final conflict in terms of assumptions.
+| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+| stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+void Solver::analyzeFinal(Lit p, LSet& out_conflict)
+{
+ out_conflict.clear();
+ out_conflict.insert(p);
+
+ if (decisionLevel() == 0)
+ return;
+
+ seen[var(p)] = 1;
+
+ for (int i = trail.size()-1; i >= trail_lim[0]; i--){
+ Var x = var(trail[i]);
+ if (seen[x]){
+ if (reason(x) == CRef_Undef){
+ assert(level(x) > 0);
+ out_conflict.insert(~trail[i]);
+ }else{
+ Clause& c = ca[reason(x)];
+ for (int j = 1; j < c.size(); j++)
+ if (level(var(c[j])) > 0)
+ seen[var(c[j])] = 1;
+ }
+ seen[x] = 0;
+ }
+ }
+
+ seen[var(p)] = 0;
+}
+
+
+void Solver::uncheckedEnqueue(Lit p, CRef from)
+{
+ assert(value(p) == l_Undef);
+ assigns[var(p)] = lbool(!sign(p));
+ vardata[var(p)] = mkVarData(from, decisionLevel());
+ trail.push_(p);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+| propagate : [void] -> [Clause*]
+|
+| Description:
+| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
+| otherwise CRef_Undef.
+|
+| Post-conditions:
+| * the propagation queue is empty, even if there was a conflict.
+|________________________________________________________________________________________________@*/
+CRef Solver::propagate()
+{
+ CRef confl = CRef_Undef;
+ int num_props = 0;
+
+ while (qhead < trail.size()){
+ Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
+ vec<Watcher>& ws = watches.lookup(p);
+ Watcher *i, *j, *end;
+ num_props++;
+
+ for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){
+ // Try to avoid inspecting the clause:
+ Lit blocker = i->blocker;
+ if (value(blocker) == l_True){
+ *j++ = *i++; continue; }
+
+ // Make sure the false literal is data[1]:
+ CRef cr = i->cref;
+ Clause& c = ca[cr];
+ Lit false_lit = ~p;
+ if (c[0] == false_lit)
+ c[0] = c[1], c[1] = false_lit;
+ assert(c[1] == false_lit);
+ i++;
+
+ // If 0th watch is true, then clause is already satisfied.
+ Lit first = c[0];
+ Watcher w = Watcher(cr, first);
+ if (first != blocker && value(first) == l_True){
+ *j++ = w; continue; }
+
+ // Look for new watch:
+ for (int k = 2; k < c.size(); k++)
+ if (value(c[k]) != l_False){
+ c[1] = c[k]; c[k] = false_lit;
+ watches[~c[1]].push(w);
+ goto NextClause; }
+
+ // Did not find watch -- clause is unit under assignment:
+ *j++ = w;
+ if (value(first) == l_False){
+ confl = cr;
+ qhead = trail.size();
+ // Copy the remaining watches:
+ while (i < end)
+ *j++ = *i++;
+ }else
+ uncheckedEnqueue(first, cr);
+
+ NextClause:;
+ }
+ ws.shrink(i - j);
+ }
+ propagations += num_props;
+ simpDB_props -= num_props;
+
+ return confl;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+| reduceDB : () -> [void]
+|
+| Description:
+| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
+| clauses are clauses that are reason to some assignment. Binary clauses are never removed.
+|________________________________________________________________________________________________@*/
+struct reduceDB_lt {
+ ClauseAllocator& ca;
+ reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
+ bool operator () (CRef x, CRef y) {
+ return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
+};
+void Solver::reduceDB()
+{
+ int i, j;
+ double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity
+
+ sort(learnts, reduceDB_lt(ca));
+ // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
+ // and clauses with activity smaller than 'extra_lim':
+ for (i = j = 0; i < learnts.size(); i++){
+ Clause& c = ca[learnts[i]];
+ if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
+ removeClause(learnts[i]);
+ else
+ learnts[j++] = learnts[i];
+ }
+ learnts.shrink(i - j);
+ checkGarbage();
+}
+
+
+void Solver::removeSatisfied(vec<CRef>& cs)
+{
+ int i, j;
+ for (i = j = 0; i < cs.size(); i++){
+ Clause& c = ca[cs[i]];
+ if (satisfied(c))
+ removeClause(cs[i]);
+ else{
+ // Trim clause:
+ assert(value(c[0]) == l_Undef && value(c[1]) == l_Undef);
+ for (int k = 2; k < c.size(); k++)
+ if (value(c[k]) == l_False){
+ c[k--] = c[c.size()-1];
+ c.pop();
+ }
+ cs[j++] = cs[i];
+ }
+ }
+ cs.shrink(i - j);
+}
+
+
+void Solver::rebuildOrderHeap()
+{
+ vec<Var> vs;
+ for (Var v = 0; v < nVars(); v++)
+ if (decision[v] && value(v) == l_Undef)
+ vs.push(v);
+ order_heap.build(vs);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+| simplify : [void] -> [bool]
+|
+| Description:
+| Simplify the clause database according to the current top-level assigment. Currently, the only
+| thing done here is the removal of satisfied clauses, but more things can be put here.
+|________________________________________________________________________________________________@*/
+bool Solver::simplify()
+{
+ assert(decisionLevel() == 0);
+
+ if (!ok || propagate() != CRef_Undef)
+ return ok = false;
+
+ if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
+ return true;
+
+ // Remove satisfied clauses:
+ removeSatisfied(learnts);
+ if (remove_satisfied){ // Can be turned off.
+ removeSatisfied(clauses);
+
+ // TODO: what todo in if 'remove_satisfied' is false?
+
+ // Remove all released variables from the trail:
+ for (int i = 0; i < released_vars.size(); i++){
+ assert(seen[released_vars[i]] == 0);
+ seen[released_vars[i]] = 1;
+ }
+
+ int i, j;
+ for (i = j = 0; i < trail.size(); i++)
+ if (seen[var(trail[i])] == 0)
+ trail[j++] = trail[i];
+ trail.shrink(i - j);
+ //printf("trail.size()= %d, qhead = %d\n", trail.size(), qhead);
+ qhead = trail.size();
+
+ for (int i = 0; i < released_vars.size(); i++)
+ seen[released_vars[i]] = 0;
+
+ // Released variables are now ready to be reused:
+ append(released_vars, free_vars);
+ released_vars.clear();
+ }
+ checkGarbage();
+ rebuildOrderHeap();
+
+ simpDB_assigns = nAssigns();
+ simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
+
+ return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+| search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
+|
+| Description:
+| Search for a model the specified number of conflicts.
+| NOTE! Use negative value for 'nof_conflicts' indicate infinity.
+|
+| Output:
+| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
+| all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
+| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
+|________________________________________________________________________________________________@*/
+lbool Solver::search(int nof_conflicts)
+{
+ assert(ok);
+ int backtrack_level;
+ int conflictC = 0;
+ vec<Lit> learnt_clause;
+ starts++;
+
+ for (;;){
+ CRef confl = propagate();
+ if (confl != CRef_Undef){
+ // CONFLICT
+ conflicts++; conflictC++;
+ if (decisionLevel() == 0) return l_False;
+
+ learnt_clause.clear();
+ analyze(confl, learnt_clause, backtrack_level);
+ cancelUntil(backtrack_level);
+
+ if (learnt_clause.size() == 1){
+ uncheckedEnqueue(learnt_clause[0]);
+ }else{
+ CRef cr = ca.alloc(learnt_clause, true);
+ learnts.push(cr);
+ attachClause(cr);
+ claBumpActivity(ca[cr]);
+ uncheckedEnqueue(learnt_clause[0], cr);
+ }
+
+ varDecayActivity();
+ claDecayActivity();
+
+ if (--learntsize_adjust_cnt == 0){
+ learntsize_adjust_confl *= learntsize_adjust_inc;
+ learntsize_adjust_cnt = (int)learntsize_adjust_confl;
+ max_learnts *= learntsize_inc;
+
+ if (verbosity >= 1)
+ printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
+ (int)conflicts,
+ (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
+ (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
+ }
+
+ }else{
+ // NO CONFLICT
+ if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
+ // Reached bound on number of conflicts:
+ progress_estimate = progressEstimate();
+ cancelUntil(0);
+ return l_Undef; }
+
+ // Simplify the set of problem clauses:
+ if (decisionLevel() == 0 && !simplify())
+ return l_False;
+
+ if (learnts.size()-nAssigns() >= max_learnts)
+ // Reduce the set of learnt clauses:
+ reduceDB();
+
+ Lit next = lit_Undef;
+ while (decisionLevel() < assumptions.size()){
+ // Perform user provided assumption:
+ Lit p = assumptions[decisionLevel()];
+ if (value(p) == l_True){
+ // Dummy decision level:
+ newDecisionLevel();
+ }else if (value(p) == l_False){
+ analyzeFinal(~p, conflict);
+ return l_False;
+ }else{
+ next = p;
+ break;
+ }
+ }
+
+ if (next == lit_Undef){
+ // New variable decision:
+ decisions++;
+ next = pickBranchLit();
+
+ if (next == lit_Undef)
+ // Model found:
+ return l_True;
+ }
+
+ // Increase decision level and enqueue 'next'
+ newDecisionLevel();
+ uncheckedEnqueue(next);
+ }
+ }
+}
+
+
+double Solver::progressEstimate() const
+{
+ double progress = 0;
+ double F = 1.0 / nVars();
+
+ for (int i = 0; i <= decisionLevel(); i++){
+ int beg = i == 0 ? 0 : trail_lim[i - 1];
+ int end = i == decisionLevel() ? trail.size() : trail_lim[i];
+ progress += pow(F, i) * (end - beg);
+ }
+
+ return progress / nVars();
+}
+
+/*
+ Finite subsequences of the Luby-sequence:
+
+ 0: 1
+ 1: 1 1 2
+ 2: 1 1 2 1 1 2 4
+ 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
+ ...
+
+
+ */
+
+static double luby(double y, int x){
+
+ // Find the finite subsequence that contains index 'x', and the
+ // size of that subsequence:
+ int size, seq;
+ for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
+
+ while (size-1 != x){
+ size = (size-1)>>1;
+ seq--;
+ x = x % size;
+ }
+
+ return pow(y, seq);
+}
+
+// NOTE: assumptions passed in member-variable 'assumptions'.
+lbool Solver::solve_()
+{
+ model.clear();
+ conflict.clear();
+ if (!ok) return l_False;
+
+ solves++;
+
+ max_learnts = nClauses() * learntsize_factor;
+ if (max_learnts < min_learnts_lim)
+ max_learnts = min_learnts_lim;
+
+ learntsize_adjust_confl = learntsize_adjust_start_confl;
+ learntsize_adjust_cnt = (int)learntsize_adjust_confl;
+ lbool status = l_Undef;
+
+ if (verbosity >= 1){
+ printf("============================[ Search Statistics ]==============================\n");
+ printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n");
+ printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n");
+ printf("===============================================================================\n");
+ }
+
+ // Search:
+ int curr_restarts = 0;
+ while (status == l_Undef){
+ double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
+ status = search(rest_base * restart_first);
+ if (!withinBudget()) break;
+ curr_restarts++;
+ }
+
+ if (verbosity >= 1)
+ printf("===============================================================================\n");
+
+
+ if (status == l_True){
+ // Extend & copy model:
+ model.growTo(nVars());
+ for (int i = 0; i < nVars(); i++) model[i] = value(i);
+ }else if (status == l_False && conflict.size() == 0)
+ ok = false;
+
+ cancelUntil(0);
+ return status;
+}
+
+
+bool Solver::implies(const vec<Lit>& assumps, vec<Lit>& out)
+{
+ trail_lim.push(trail.size());
+ for (int i = 0; i < assumps.size(); i++){
+ Lit a = assumps[i];
+
+ if (value(a) == l_False){
+ cancelUntil(0);
+ return false;
+ }else if (value(a) == l_Undef)
+ uncheckedEnqueue(a);
+ }
+
+ unsigned trail_before = trail.size();
+ bool ret = true;
+ if (propagate() == CRef_Undef){
+ out.clear();
+ for (int j = trail_before; j < trail.size(); j++)
+ out.push(trail[j]);
+ }else
+ ret = false;
+
+ cancelUntil(0);
+ return ret;
+}
+
+//=================================================================================================
+// Writing CNF to DIMACS:
+//
+// FIXME: this needs to be rewritten completely.
+
+static Var mapVar(Var x, vec<Var>& map, Var& max)
+{
+ if (map.size() <= x || map[x] == -1){
+ map.growTo(x+1, -1);
+ map[x] = max++;
+ }
+ return map[x];
+}
+
+
+void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
+{
+ if (satisfied(c)) return;
+
+ for (int i = 0; i < c.size(); i++)
+ if (value(c[i]) != l_False)
+ fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
+ fprintf(f, "0\n");
+}
+
+
+void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
+{
+ FILE* f = fopen(file, "wr");
+ if (f == NULL)
+ fprintf(stderr, "could not open file %s\n", file), exit(1);
+ toDimacs(f, assumps);
+ fclose(f);
+}
+
+
+void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
+{
+ // Handle case when solver is in contradictory state:
+ if (!ok){
+ fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
+ return; }
+
+ vec<Var> map; Var max = 0;
+
+ // Cannot use removeClauses here because it is not safe
+ // to deallocate them at this point. Could be improved.
+ int cnt = 0;
+ for (int i = 0; i < clauses.size(); i++)
+ if (!satisfied(ca[clauses[i]]))
+ cnt++;
+
+ for (int i = 0; i < clauses.size(); i++)
+ if (!satisfied(ca[clauses[i]])){
+ Clause& c = ca[clauses[i]];
+ for (int j = 0; j < c.size(); j++)
+ if (value(c[j]) != l_False)
+ mapVar(var(c[j]), map, max);
+ }
+
+ // Assumptions are added as unit clauses:
+ cnt += assumps.size();
+
+ fprintf(f, "p cnf %d %d\n", max, cnt);
+
+ for (int i = 0; i < assumps.size(); i++){
+ assert(value(assumps[i]) != l_False);
+ fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1);
+ }
+
+ for (int i = 0; i < clauses.size(); i++)
+ toDimacs(f, ca[clauses[i]], map, max);
+
+ if (verbosity > 0)
+ printf("Wrote DIMACS with %d variables and %d clauses.\n", max, cnt);
+}
+
+
+void Solver::printStats() const
+{
+ double cpu_time = cpuTime();
+ double mem_used = memUsedPeak();
+ printf("restarts : %" PRIu64 "\n", starts);
+ printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", conflicts , conflicts /cpu_time);
+ printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time);
+ printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", propagations, propagations/cpu_time);
+ printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
+ if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
+ printf("CPU time : %g s\n", cpu_time);
+}
+
+
+//=================================================================================================
+// Garbage Collection methods:
+
+void Solver::relocAll(ClauseAllocator& to)
+{
+ // All watchers:
+ //
+ watches.cleanAll();
+ for (int v = 0; v < nVars(); v++)
+ for (int s = 0; s < 2; s++){
+ Lit p = mkLit(v, s);
+ vec<Watcher>& ws = watches[p];
+ for (int j = 0; j < ws.size(); j++)
+ ca.reloc(ws[j].cref, to);
+ }
+
+ // All reasons:
+ //
+ for (int i = 0; i < trail.size(); i++){
+ Var v = var(trail[i]);
+
+ // Note: it is not safe to call 'locked()' on a relocated clause. This is why we keep
+ // 'dangling' reasons here. It is safe and does not hurt.
+ if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))){
+ assert(!isRemoved(reason(v)));
+ ca.reloc(vardata[v].reason, to);
+ }
+ }
+
+ // All learnt:
+ //
+ int i, j;
+ for (i = j = 0; i < learnts.size(); i++)
+ if (!isRemoved(learnts[i])){
+ ca.reloc(learnts[i], to);
+ learnts[j++] = learnts[i];
+ }
+ learnts.shrink(i - j);
+
+ // All original:
+ //
+ for (i = j = 0; i < clauses.size(); i++)
+ if (!isRemoved(clauses[i])){
+ ca.reloc(clauses[i], to);
+ clauses[j++] = clauses[i];
+ }
+ clauses.shrink(i - j);
+}
+
+
+void Solver::garbageCollect()
+{
+ // Initialize the next region to a size corresponding to the estimated utilization degree. This
+ // is not precise but should avoid some unnecessary reallocations for the new region:
+ ClauseAllocator to(ca.size() - ca.wasted());
+
+ relocAll(to);
+ if (verbosity >= 2)
+ printf("| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ to.moveTo(ca);
+}
diff --git a/libs/minisat/Solver.h b/libs/minisat/Solver.h
new file mode 100644
index 000000000..44570b0e1
--- /dev/null
+++ b/libs/minisat/Solver.h
@@ -0,0 +1,409 @@
+/****************************************************************************************[Solver.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Solver_h
+#define Minisat_Solver_h
+
+#include "Vec.h"
+#include "Heap.h"
+#include "Alg.h"
+#include "IntMap.h"
+#include "Options.h"
+#include "SolverTypes.h"
+
+
+namespace Minisat {
+
+//=================================================================================================
+// Solver -- the main class:
+
+class Solver {
+public:
+
+ // Constructor/Destructor:
+ //
+ Solver();
+ virtual ~Solver();
+
+ // Problem specification:
+ //
+ Var newVar (lbool upol = l_Undef, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+ void releaseVar(Lit l); // Make literal true and promise to never refer to variable again.
+
+ bool addClause (const vec<Lit>& ps); // Add a clause to the solver.
+ bool addEmptyClause(); // Add the empty clause, making the solver contradictory.
+ bool addClause (Lit p); // Add a unit clause to the solver.
+ bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r, Lit s); // Add a quaternary clause to the solver.
+ bool addClause_( vec<Lit>& ps); // Add a clause to the solver without making superflous internal copy. Will
+ // change the passed vector 'ps'.
+
+ // Solving:
+ //
+ bool simplify (); // Removes already satisfied clauses.
+ bool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
+ lbool solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
+ bool solve (); // Search without assumptions.
+ bool solve (Lit p); // Search for a model that respects a single assumption.
+ bool solve (Lit p, Lit q); // Search for a model that respects two assumptions.
+ bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions.
+ bool okay () const; // FALSE means solver is in a conflicting state
+
+ bool implies (const vec<Lit>& assumps, vec<Lit>& out);
+
+ // Iterate over clauses and top-level assignments:
+ ClauseIterator clausesBegin() const;
+ ClauseIterator clausesEnd() const;
+ TrailIterator trailBegin() const;
+ TrailIterator trailEnd () const;
+
+ void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format.
+ void toDimacs (const char *file, const vec<Lit>& assumps);
+ void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
+
+ // Convenience versions of 'toDimacs()':
+ void toDimacs (const char* file);
+ void toDimacs (const char* file, Lit p);
+ void toDimacs (const char* file, Lit p, Lit q);
+ void toDimacs (const char* file, Lit p, Lit q, Lit r);
+
+ // Variable mode:
+ //
+ void setPolarity (Var v, lbool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
+ void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
+
+ // Read state:
+ //
+ lbool value (Var x) const; // The current value of a variable.
+ lbool value (Lit p) const; // The current value of a literal.
+ lbool modelValue (Var x) const; // The value of a variable in the last model. The last call to solve must have been satisfiable.
+ lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
+ int nAssigns () const; // The current number of assigned literals.
+ int nClauses () const; // The current number of original clauses.
+ int nLearnts () const; // The current number of learnt clauses.
+ int nVars () const; // The current number of variables.
+ int nFreeVars () const;
+ void printStats () const; // Print some current statistics to standard output.
+
+ // Resource constraints:
+ //
+ void setConfBudget(int64_t x);
+ void setPropBudget(int64_t x);
+ void budgetOff();
+ void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
+ void clearInterrupt(); // Clear interrupt indicator flag.
+
+ // Memory managment:
+ //
+ virtual void garbageCollect();
+ void checkGarbage(double gf);
+ void checkGarbage();
+
+ // Extra results: (read-only member variable)
+ //
+ vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
+ LSet conflict; // If problem is unsatisfiable (possibly under assumptions),
+ // this vector represent the final conflict clause expressed in the assumptions.
+
+ // Mode of operation:
+ //
+ int verbosity;
+ double var_decay;
+ double clause_decay;
+ double random_var_freq;
+ double random_seed;
+ bool luby_restart;
+ int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
+ int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
+ bool rnd_pol; // Use random polarities for branching heuristics.
+ bool rnd_init_act; // Initialize variable activities with a small random value.
+ double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
+ int min_learnts_lim; // Minimum number to set the learnts limit to.
+
+ int restart_first; // The initial restart limit. (default 100)
+ double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5)
+ double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3)
+ double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
+
+ int learntsize_adjust_start_confl;
+ double learntsize_adjust_inc;
+
+ // Statistics: (read-only member variable)
+ //
+ uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
+ uint64_t dec_vars, num_clauses, num_learnts, clauses_literals, learnts_literals, max_literals, tot_literals;
+
+protected:
+
+ // Helper structures:
+ //
+ struct VarData { CRef reason; int level; };
+ static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
+
+ struct Watcher {
+ CRef cref;
+ Lit blocker;
+ Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
+ bool operator==(const Watcher& w) const { return cref == w.cref; }
+ bool operator!=(const Watcher& w) const { return cref != w.cref; }
+ };
+
+ struct WatcherDeleted
+ {
+ const ClauseAllocator& ca;
+ WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+ bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
+ };
+
+ struct VarOrderLt {
+ const IntMap<Var, double>& activity;
+ bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
+ VarOrderLt(const IntMap<Var, double>& act) : activity(act) { }
+ };
+
+ struct ShrinkStackElem {
+ uint32_t i;
+ Lit l;
+ ShrinkStackElem(uint32_t _i, Lit _l) : i(_i), l(_l){}
+ };
+
+ // Solver state:
+ //
+ vec<CRef> clauses; // List of problem clauses.
+ vec<CRef> learnts; // List of learnt clauses.
+ vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
+ vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
+ vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
+
+ VMap<double> activity; // A heuristic measurement of the activity of a variable.
+ VMap<lbool> assigns; // The current assignments.
+ VMap<char> polarity; // The preferred polarity of each variable.
+ VMap<lbool> user_pol; // The users preferred polarity of each variable.
+ VMap<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
+ VMap<VarData> vardata; // Stores reason and level for each variable.
+ OccLists<Lit, vec<Watcher>, WatcherDeleted, MkIndexLit>
+ watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+
+ Heap<Var,VarOrderLt>order_heap; // A priority queue of variables ordered with respect to the variable activity.
+
+ bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
+ double cla_inc; // Amount to bump next clause with.
+ double var_inc; // Amount to bump next variable with.
+ int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
+ int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
+ int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
+ double progress_estimate;// Set by 'search()'.
+ bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
+ Var next_var; // Next variable to be created.
+ ClauseAllocator ca;
+
+ vec<Var> released_vars;
+ vec<Var> free_vars;
+
+ // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
+ // used, exept 'seen' wich is used in several places.
+ //
+ VMap<char> seen;
+ vec<ShrinkStackElem>analyze_stack;
+ vec<Lit> analyze_toclear;
+ vec<Lit> add_tmp;
+
+ double max_learnts;
+ double learntsize_adjust_confl;
+ int learntsize_adjust_cnt;
+
+ // Resource constraints:
+ //
+ int64_t conflict_budget; // -1 means no budget.
+ int64_t propagation_budget; // -1 means no budget.
+ bool asynch_interrupt;
+
+ // Main internal methods:
+ //
+ void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
+ Lit pickBranchLit (); // Return the next decision variable.
+ void newDecisionLevel (); // Begins a new decision level.
+ void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined.
+ bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise.
+ CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause.
+ void cancelUntil (int level); // Backtrack until a certain level.
+ void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
+ void analyzeFinal (Lit p, LSet& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
+ bool litRedundant (Lit p); // (helper method for 'analyze()')
+ lbool search (int nof_conflicts); // Search for a given number of conflicts.
+ lbool solve_ (); // Main solve method (assumptions given in 'assumptions').
+ void reduceDB (); // Reduce the set of learnt clauses.
+ void removeSatisfied (vec<CRef>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
+ void rebuildOrderHeap ();
+
+ // Maintaining Variable/Clause activity:
+ //
+ void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
+ void varBumpActivity (Var v, double inc); // Increase a variable with the current 'bump' value.
+ void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
+ void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
+ void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value.
+
+ // Operations on clauses:
+ //
+ void attachClause (CRef cr); // Attach a clause to watcher lists.
+ void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists.
+ void removeClause (CRef cr); // Detach and free a clause.
+ bool isRemoved (CRef cr) const; // Test if a clause has been removed.
+ bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
+ bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
+
+ // Misc:
+ //
+ int decisionLevel () const; // Gives the current decisionlevel.
+ uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
+ CRef reason (Var x) const;
+ int level (Var x) const;
+ double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
+ bool withinBudget () const;
+ void relocAll (ClauseAllocator& to);
+
+ // Static helpers:
+ //
+
+ // Returns a random float 0 <= x < 1. Seed must never be 0.
+ static inline double drand(double& seed) {
+ seed *= 1389796;
+ int q = (int)(seed / 2147483647);
+ seed -= (double)q * 2147483647;
+ return seed / 2147483647; }
+
+ // Returns a random integer 0 <= x < size. Seed must never be 0.
+ static inline int irand(double& seed, int size) {
+ return (int)(drand(seed) * size); }
+};
+
+
+//=================================================================================================
+// Implementation of inline methods:
+
+inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
+inline int Solver::level (Var x) const { return vardata[x].level; }
+
+inline void Solver::insertVarOrder(Var x) {
+ if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
+
+inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
+inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
+inline void Solver::varBumpActivity(Var v, double inc) {
+ if ( (activity[v] += inc) > 1e100 ) {
+ // Rescale:
+ for (int i = 0; i < nVars(); i++)
+ activity[i] *= 1e-100;
+ var_inc *= 1e-100; }
+
+ // Update order_heap with respect to new activity:
+ if (order_heap.inHeap(v))
+ order_heap.decrease(v); }
+
+inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
+inline void Solver::claBumpActivity (Clause& c) {
+ if ( (c.activity() += cla_inc) > 1e20 ) {
+ // Rescale:
+ for (int i = 0; i < learnts.size(); i++)
+ ca[learnts[i]].activity() *= 1e-20;
+ cla_inc *= 1e-20; } }
+
+inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
+inline void Solver::checkGarbage(double gf){
+ if (ca.wasted() > ca.size() * gf)
+ garbageCollect(); }
+
+// NOTE: enqueue does not set the ok flag! (only public methods do)
+inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
+inline bool Solver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
+inline bool Solver::addEmptyClause () { add_tmp.clear(); return addClause_(add_tmp); }
+inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
+inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
+inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline bool Solver::addClause (Lit p, Lit q, Lit r, Lit s){ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); add_tmp.push(s); return addClause_(add_tmp); }
+
+inline bool Solver::isRemoved (CRef cr) const { return ca[cr].mark() == 1; }
+inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
+inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); }
+
+inline int Solver::decisionLevel () const { return trail_lim.size(); }
+inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
+inline lbool Solver::value (Var x) const { return assigns[x]; }
+inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }
+inline lbool Solver::modelValue (Var x) const { return model[x]; }
+inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
+inline int Solver::nAssigns () const { return trail.size(); }
+inline int Solver::nClauses () const { return num_clauses; }
+inline int Solver::nLearnts () const { return num_learnts; }
+inline int Solver::nVars () const { return next_var; }
+// TODO: nFreeVars() is not quite correct, try to calculate right instead of adapting it like below:
+inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
+inline void Solver::setPolarity (Var v, lbool b){ user_pol[v] = b; }
+inline void Solver::setDecisionVar(Var v, bool b)
+{
+ if ( b && !decision[v]) dec_vars++;
+ else if (!b && decision[v]) dec_vars--;
+
+ decision[v] = b;
+ insertVarOrder(v);
+}
+inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
+inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
+inline void Solver::interrupt(){ asynch_interrupt = true; }
+inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
+inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
+inline bool Solver::withinBudget() const {
+ return !asynch_interrupt &&
+ (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
+ (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
+
+// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
+// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
+// all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
+inline bool Solver::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; }
+inline bool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
+inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
+inline bool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }
+inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
+inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
+inline bool Solver::okay () const { return ok; }
+
+inline ClauseIterator Solver::clausesBegin() const { return ClauseIterator(ca, &clauses[0]); }
+inline ClauseIterator Solver::clausesEnd () const { return ClauseIterator(ca, &clauses[clauses.size()]); }
+inline TrailIterator Solver::trailBegin () const { return TrailIterator(&trail[0]); }
+inline TrailIterator Solver::trailEnd () const {
+ return TrailIterator(&trail[decisionLevel() == 0 ? trail.size() : trail_lim[0]]); }
+
+inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
+inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
+inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
+inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
+
+
+//=================================================================================================
+// Debug etc:
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/SolverTypes.h b/libs/minisat/SolverTypes.h
new file mode 100644
index 000000000..a7df57858
--- /dev/null
+++ b/libs/minisat/SolverTypes.h
@@ -0,0 +1,478 @@
+/***********************************************************************************[SolverTypes.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+
+#ifndef Minisat_SolverTypes_h
+#define Minisat_SolverTypes_h
+
+#include <assert.h>
+
+#include "IntTypes.h"
+#include "Alg.h"
+#include "Vec.h"
+#include "IntMap.h"
+#include "Map.h"
+#include "Alloc.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Variables, literals, lifted booleans, clauses:
+
+
+// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
+// so that they can be used as array indices.
+
+typedef int Var;
+#if defined(MINISAT_CONSTANTS_AS_MACROS)
+#define var_Undef (-1)
+#else
+ const Var var_Undef = -1;
+#endif
+
+
+struct Lit {
+ int x;
+
+ // Use this as a constructor:
+ friend Lit mkLit(Var var, bool sign);
+
+ bool operator == (Lit p) const { return x == p.x; }
+ bool operator != (Lit p) const { return x != p.x; }
+ bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering.
+};
+
+
+inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; }
+inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
+inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
+inline bool sign (Lit p) { return p.x & 1; }
+inline int var (Lit p) { return p.x >> 1; }
+
+// Mapping Literals to and from compact integers suitable for array indexing:
+inline int toInt (Var v) { return v; }
+inline int toInt (Lit p) { return p.x; }
+inline Lit toLit (int i) { Lit p; p.x = i; return p; }
+
+//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
+//const Lit lit_Error = mkLit(var_Undef, true ); // }
+
+const Lit lit_Undef = { -2 }; // }- Useful special constants.
+const Lit lit_Error = { -1 }; // }
+
+struct MkIndexLit { vec<Lit>::Size operator()(Lit l) const { return vec<Lit>::Size(l.x); } };
+
+template<class T> class VMap : public IntMap<Var, T>{};
+template<class T> class LMap : public IntMap<Lit, T, MkIndexLit>{};
+class LSet : public IntSet<Lit, MkIndexLit>{};
+
+//=================================================================================================
+// Lifted booleans:
+//
+// NOTE: this implementation is optimized for the case when comparisons between values are mostly
+// between one variable and one constant. Some care had to be taken to make sure that gcc
+// does enough constant propagation to produce sensible code, and this appears to be somewhat
+// fragile unfortunately.
+
+class lbool {
+ uint8_t value;
+
+public:
+ explicit lbool(uint8_t v) : value(v) { }
+
+ lbool() : value(0) { }
+ explicit lbool(bool x) : value(!x) { }
+
+ bool operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }
+ bool operator != (lbool b) const { return !(*this == b); }
+ lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
+
+ lbool operator && (lbool b) const {
+ uint8_t sel = (this->value << 1) | (b.value << 3);
+ uint8_t v = (0xF7F755F4 >> sel) & 3;
+ return lbool(v); }
+
+ lbool operator || (lbool b) const {
+ uint8_t sel = (this->value << 1) | (b.value << 3);
+ uint8_t v = (0xFCFCF400 >> sel) & 3;
+ return lbool(v); }
+
+ friend int toInt (lbool l);
+ friend lbool toLbool(int v);
+};
+inline int toInt (lbool l) { return l.value; }
+inline lbool toLbool(int v) { return lbool((uint8_t)v); }
+
+#if defined(MINISAT_CONSTANTS_AS_MACROS)
+ #define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
+ #define l_False (lbool((uint8_t)1))
+ #define l_Undef (lbool((uint8_t)2))
+#else
+ const lbool l_True ((uint8_t)0);
+ const lbool l_False((uint8_t)1);
+ const lbool l_Undef((uint8_t)2);
+#endif
+
+
+//=================================================================================================
+// Clause -- a simple class for representing a clause:
+
+class Clause;
+typedef RegionAllocator<uint32_t>::Ref CRef;
+
+class Clause {
+ struct {
+ unsigned mark : 2;
+ unsigned learnt : 1;
+ unsigned has_extra : 1;
+ unsigned reloced : 1;
+ unsigned size : 27; } header;
+ union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
+
+ friend class ClauseAllocator;
+
+ // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+ Clause(const vec<Lit>& ps, bool use_extra, bool learnt) {
+ header.mark = 0;
+ header.learnt = learnt;
+ header.has_extra = use_extra;
+ header.reloced = 0;
+ header.size = ps.size();
+
+ for (int i = 0; i < ps.size(); i++)
+ data[i].lit = ps[i];
+
+ if (header.has_extra){
+ if (header.learnt)
+ data[header.size].act = 0;
+ else
+ calcAbstraction();
+ }
+ }
+
+ // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+ Clause(const Clause& from, bool use_extra){
+ header = from.header;
+ header.has_extra = use_extra; // NOTE: the copied clause may lose the extra field.
+
+ for (int i = 0; i < from.size(); i++)
+ data[i].lit = from[i];
+
+ if (header.has_extra){
+ if (header.learnt)
+ data[header.size].act = from.data[header.size].act;
+ else
+ data[header.size].abs = from.data[header.size].abs;
+ }
+ }
+
+public:
+ void calcAbstraction() {
+ assert(header.has_extra);
+ uint32_t abstraction = 0;
+ for (int i = 0; i < size(); i++)
+ abstraction |= 1 << (var(data[i].lit) & 31);
+ data[header.size].abs = abstraction; }
+
+
+ int size () const { return header.size; }
+ void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
+ void pop () { shrink(1); }
+ bool learnt () const { return header.learnt; }
+ bool has_extra () const { return header.has_extra; }
+ uint32_t mark () const { return header.mark; }
+ void mark (uint32_t m) { header.mark = m; }
+ const Lit& last () const { return data[header.size-1].lit; }
+
+ bool reloced () const { return header.reloced; }
+ CRef relocation () const { return data[0].rel; }
+ void relocate (CRef c) { header.reloced = 1; data[0].rel = c; }
+
+ // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
+ // subsumption operations to behave correctly.
+ Lit& operator [] (int i) { return data[i].lit; }
+ Lit operator [] (int i) const { return data[i].lit; }
+ operator const Lit* (void) const { return (Lit*)data; }
+
+ float& activity () { assert(header.has_extra); return data[header.size].act; }
+ uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; }
+
+ Lit subsumes (const Clause& other) const;
+ void strengthen (Lit p);
+};
+
+
+//=================================================================================================
+// ClauseAllocator -- a simple class for allocating memory for clauses:
+
+const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
+class ClauseAllocator
+{
+ RegionAllocator<uint32_t> ra;
+
+ static uint32_t clauseWord32Size(int size, bool has_extra){
+ return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
+
+ public:
+ enum { Unit_Size = RegionAllocator<uint32_t>::Unit_Size };
+
+ bool extra_clause_field;
+
+ ClauseAllocator(uint32_t start_cap) : ra(start_cap), extra_clause_field(false){}
+ ClauseAllocator() : extra_clause_field(false){}
+
+ void moveTo(ClauseAllocator& to){
+ to.extra_clause_field = extra_clause_field;
+ ra.moveTo(to.ra); }
+
+ CRef alloc(const vec<Lit>& ps, bool learnt = false)
+ {
+ assert(sizeof(Lit) == sizeof(uint32_t));
+ assert(sizeof(float) == sizeof(uint32_t));
+ bool use_extra = learnt | extra_clause_field;
+ CRef cid = ra.alloc(clauseWord32Size(ps.size(), use_extra));
+ new (lea(cid)) Clause(ps, use_extra, learnt);
+
+ return cid;
+ }
+
+ CRef alloc(const Clause& from)
+ {
+ bool use_extra = from.learnt() | extra_clause_field;
+ CRef cid = ra.alloc(clauseWord32Size(from.size(), use_extra));
+ new (lea(cid)) Clause(from, use_extra);
+ return cid; }
+
+ uint32_t size () const { return ra.size(); }
+ uint32_t wasted () const { return ra.wasted(); }
+
+ // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+ Clause& operator[](CRef r) { return (Clause&)ra[r]; }
+ const Clause& operator[](CRef r) const { return (Clause&)ra[r]; }
+ Clause* lea (CRef r) { return (Clause*)ra.lea(r); }
+ const Clause* lea (CRef r) const { return (Clause*)ra.lea(r);; }
+ CRef ael (const Clause* t){ return ra.ael((uint32_t*)t); }
+
+ void free(CRef cid)
+ {
+ Clause& c = operator[](cid);
+ ra.free(clauseWord32Size(c.size(), c.has_extra()));
+ }
+
+ void reloc(CRef& cr, ClauseAllocator& to)
+ {
+ Clause& c = operator[](cr);
+
+ if (c.reloced()) { cr = c.relocation(); return; }
+
+ cr = to.alloc(c);
+ c.relocate(cr);
+ }
+};
+
+//=================================================================================================
+// Simple iterator classes (for iterating over clauses and top-level assignments):
+
+class ClauseIterator {
+ const ClauseAllocator& ca;
+ const CRef* crefs;
+public:
+ ClauseIterator(const ClauseAllocator& _ca, const CRef* _crefs) : ca(_ca), crefs(_crefs){}
+
+ void operator++(){ crefs++; }
+ const Clause& operator*() const { return ca[*crefs]; }
+
+ // NOTE: does not compare that references use the same clause-allocator:
+ bool operator==(const ClauseIterator& ci) const { return crefs == ci.crefs; }
+ bool operator!=(const ClauseIterator& ci) const { return crefs != ci.crefs; }
+};
+
+
+class TrailIterator {
+ const Lit* lits;
+public:
+ TrailIterator(const Lit* _lits) : lits(_lits){}
+
+ void operator++() { lits++; }
+ Lit operator*() const { return *lits; }
+
+ bool operator==(const TrailIterator& ti) const { return lits == ti.lits; }
+ bool operator!=(const TrailIterator& ti) const { return lits != ti.lits; }
+};
+
+
+//=================================================================================================
+// OccLists -- a class for maintaining occurence lists with lazy deletion:
+
+template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K> >
+class OccLists
+{
+ IntMap<K, Vec, MkIndex> occs;
+ IntMap<K, char, MkIndex> dirty;
+ vec<K> dirties;
+ Deleted deleted;
+
+ public:
+ OccLists(const Deleted& d, MkIndex _index = MkIndex()) :
+ occs(_index),
+ dirty(_index),
+ deleted(d){}
+
+ void init (const K& idx){ occs.reserve(idx); occs[idx].clear(); dirty.reserve(idx, 0); }
+ Vec& operator[](const K& idx){ return occs[idx]; }
+ Vec& lookup (const K& idx){ if (dirty[idx]) clean(idx); return occs[idx]; }
+
+ void cleanAll ();
+ void clean (const K& idx);
+ void smudge (const K& idx){
+ if (dirty[idx] == 0){
+ dirty[idx] = 1;
+ dirties.push(idx);
+ }
+ }
+
+ void clear(bool free = true){
+ occs .clear(free);
+ dirty .clear(free);
+ dirties.clear(free);
+ }
+};
+
+
+template<class K, class Vec, class Deleted, class MkIndex>
+void OccLists<K,Vec,Deleted,MkIndex>::cleanAll()
+{
+ for (int i = 0; i < dirties.size(); i++)
+ // Dirties may contain duplicates so check here if a variable is already cleaned:
+ if (dirty[dirties[i]])
+ clean(dirties[i]);
+ dirties.clear();
+}
+
+
+template<class K, class Vec, class Deleted, class MkIndex>
+void OccLists<K,Vec,Deleted,MkIndex>::clean(const K& idx)
+{
+ Vec& vec = occs[idx];
+ int i, j;
+ for (i = j = 0; i < vec.size(); i++)
+ if (!deleted(vec[i]))
+ vec[j++] = vec[i];
+ vec.shrink(i - j);
+ dirty[idx] = 0;
+}
+
+
+//=================================================================================================
+// CMap -- a class for mapping clauses to values:
+
+
+template<class T>
+class CMap
+{
+ struct CRefHash {
+ uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
+
+ typedef Map<CRef, T, CRefHash> HashTable;
+ HashTable map;
+
+ public:
+ // Size-operations:
+ void clear () { map.clear(); }
+ int size () const { return map.elems(); }
+
+
+ // Insert/Remove/Test mapping:
+ void insert (CRef cr, const T& t){ map.insert(cr, t); }
+ void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
+ void remove (CRef cr) { map.remove(cr); }
+ bool has (CRef cr, T& t) { return map.peek(cr, t); }
+
+ // Vector interface (the clause 'c' must already exist):
+ const T& operator [] (CRef cr) const { return map[cr]; }
+ T& operator [] (CRef cr) { return map[cr]; }
+
+ // Iteration (not transparent at all at the moment):
+ int bucket_count() const { return map.bucket_count(); }
+ const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
+
+ // Move contents to other map:
+ void moveTo(CMap& other){ map.moveTo(other.map); }
+
+ // TMP debug:
+ void debug(){
+ printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
+};
+
+
+/*_________________________________________________________________________________________________
+|
+| subsumes : (other : const Clause&) -> Lit
+|
+| Description:
+| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
+| by subsumption resolution.
+|
+| Result:
+| lit_Error - No subsumption or simplification
+| lit_Undef - Clause subsumes 'other'
+| p - The literal p can be deleted from 'other'
+|________________________________________________________________________________________________@*/
+inline Lit Clause::subsumes(const Clause& other) const
+{
+ //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
+ //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
+ assert(!header.learnt); assert(!other.header.learnt);
+ assert(header.has_extra); assert(other.header.has_extra);
+ if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
+ return lit_Error;
+
+ Lit ret = lit_Undef;
+ const Lit* c = (const Lit*)(*this);
+ const Lit* d = (const Lit*)other;
+
+ for (unsigned i = 0; i < header.size; i++) {
+ // search for c[i] or ~c[i]
+ for (unsigned j = 0; j < other.header.size; j++)
+ if (c[i] == d[j])
+ goto ok;
+ else if (ret == lit_Undef && c[i] == ~d[j]){
+ ret = c[i];
+ goto ok;
+ }
+
+ // did not find it
+ return lit_Error;
+ ok:;
+ }
+
+ return ret;
+}
+
+inline void Clause::strengthen(Lit p)
+{
+ remove(*this, p);
+ calcAbstraction();
+}
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Sort.h b/libs/minisat/Sort.h
new file mode 100644
index 000000000..cc96486d8
--- /dev/null
+++ b/libs/minisat/Sort.h
@@ -0,0 +1,98 @@
+/******************************************************************************************[Sort.h]
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Sort_h
+#define Minisat_Sort_h
+
+#include "Vec.h"
+
+//=================================================================================================
+// Some sorting algorithms for vec's
+
+
+namespace Minisat {
+
+template<class T>
+struct LessThan_default {
+ bool operator () (T x, T y) { return x < y; }
+};
+
+
+template <class T, class LessThan>
+void selectionSort(T* array, int size, LessThan lt)
+{
+ int i, j, best_i;
+ T tmp;
+
+ for (i = 0; i < size-1; i++){
+ best_i = i;
+ for (j = i+1; j < size; j++){
+ if (lt(array[j], array[best_i]))
+ best_i = j;
+ }
+ tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+ }
+}
+template <class T> static inline void selectionSort(T* array, int size) {
+ selectionSort(array, size, LessThan_default<T>()); }
+
+template <class T, class LessThan>
+void sort(T* array, int size, LessThan lt)
+{
+ if (size <= 15)
+ selectionSort(array, size, lt);
+
+ else{
+ T pivot = array[size / 2];
+ T tmp;
+ int i = -1;
+ int j = size;
+
+ for(;;){
+ do i++; while(lt(array[i], pivot));
+ do j--; while(lt(pivot, array[j]));
+
+ if (i >= j) break;
+
+ tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+ }
+
+ sort(array , i , lt);
+ sort(&array[i], size-i, lt);
+ }
+}
+template <class T> static inline void sort(T* array, int size) {
+ sort(array, size, LessThan_default<T>()); }
+
+
+//=================================================================================================
+// For 'vec's:
+
+
+template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {
+ sort((T*)v, v.size(), lt); }
+template <class T> void sort(vec<T>& v) {
+ sort(v, LessThan_default<T>()); }
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc
new file mode 100644
index 000000000..febe3b40f
--- /dev/null
+++ b/libs/minisat/System.cc
@@ -0,0 +1,171 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/***************************************************************************************[System.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include <signal.h>
+#include <stdio.h>
+
+#include "System.h"
+
+#if defined(__linux__)
+
+#include <stdlib.h>
+
+using namespace Minisat;
+
+static inline int memReadStat(int field)
+{
+ char name[256];
+ pid_t pid = getpid();
+ int value;
+
+ sprintf(name, "/proc/%d/statm", pid);
+ FILE* in = fopen(name, "rb");
+ if (in == NULL) return 0;
+
+ for (; field >= 0; field--)
+ if (fscanf(in, "%d", &value) != 1)
+ printf("ERROR! Failed to parse memory statistics from \"/proc\".\n"), exit(1);
+ fclose(in);
+ return value;
+}
+
+
+static inline int memReadPeak(void)
+{
+ char name[256];
+ pid_t pid = getpid();
+
+ sprintf(name, "/proc/%d/status", pid);
+ FILE* in = fopen(name, "rb");
+ if (in == NULL) return 0;
+
+ // Find the correct line, beginning with "VmPeak:":
+ int peak_kb = 0;
+ while (!feof(in) && fscanf(in, "VmPeak: %d kB", &peak_kb) != 1)
+ while (!feof(in) && fgetc(in) != '\n')
+ ;
+ fclose(in);
+
+ return peak_kb;
+}
+
+double Minisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
+double Minisat::memUsedPeak(bool strictlyPeak) {
+ double peak = memReadPeak() / (double)1024;
+ return peak == 0 && !strictlyPeak ? memUsed() : peak; }
+
+#elif defined(__FreeBSD__) || defined(__FreeBSD_kernel__) || defined(__gnu_hurd__)
+
+double Minisat::memUsed() {
+ struct rusage ru;
+ getrusage(RUSAGE_SELF, &ru);
+ return (double)ru.ru_maxrss / 1024; }
+double Minisat::memUsedPeak(bool) { return memUsed(); }
+
+
+#elif defined(__APPLE__)
+#include <malloc/malloc.h>
+
+double Minisat::memUsed() {
+ malloc_statistics_t t;
+ malloc_zone_statistics(NULL, &t);
+ return (double)t.max_size_in_use / (1024*1024); }
+double Minisat::memUsedPeak(bool) { return memUsed(); }
+
+#else
+double Minisat::memUsed() { return 0; }
+double Minisat::memUsedPeak(bool) { return 0; }
+#endif
+
+
+void Minisat::setX86FPUPrecision()
+{
+#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
+ // Only correct FPU precision on Linux architectures that needs and supports it:
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ printf("WARNING: for repeatability, setting FPU to use double precision\n");
+#endif
+}
+
+
+#if !defined(_MSC_VER) && !defined(__MINGW32__)
+void Minisat::limitMemory(uint64_t max_mem_mb)
+{
+// FIXME: OpenBSD does not support RLIMIT_AS. Not sure how well RLIMIT_DATA works instead.
+#if defined(__OpenBSD__)
+#define RLIMIT_AS RLIMIT_DATA
+#endif
+
+ // Set limit on virtual memory:
+ if (max_mem_mb != 0){
+ rlim_t new_mem_lim = (rlim_t)max_mem_mb * 1024*1024;
+ rlimit rl;
+ getrlimit(RLIMIT_AS, &rl);
+ if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
+ rl.rlim_cur = new_mem_lim;
+ if (setrlimit(RLIMIT_AS, &rl) == -1)
+ printf("WARNING! Could not set resource limit: Virtual memory.\n");
+ }
+ }
+
+#if defined(__OpenBSD__)
+#undef RLIMIT_AS
+#endif
+}
+#else
+void Minisat::limitMemory(uint64_t /*max_mem_mb*/)
+{
+ printf("WARNING! Memory limit not supported on this architecture.\n");
+}
+#endif
+
+
+#if !defined(_MSC_VER) && !defined(__MINGW32__)
+void Minisat::limitTime(uint32_t max_cpu_time)
+{
+ if (max_cpu_time != 0){
+ rlimit rl;
+ getrlimit(RLIMIT_CPU, &rl);
+ if (rl.rlim_max == RLIM_INFINITY || (rlim_t)max_cpu_time < rl.rlim_max){
+ rl.rlim_cur = max_cpu_time;
+ if (setrlimit(RLIMIT_CPU, &rl) == -1)
+ printf("WARNING! Could not set resource limit: CPU-time.\n");
+ }
+ }
+}
+#else
+void Minisat::limitTime(uint32_t /*max_cpu_time*/)
+{
+ printf("WARNING! CPU-time limit not supported on this architecture.\n");
+}
+#endif
+
+
+void Minisat::sigTerm(void handler(int))
+{
+ signal(SIGINT, handler);
+ signal(SIGTERM,handler);
+#ifdef SIGXCPU
+ signal(SIGXCPU,handler);
+#endif
+}
diff --git a/libs/minisat/System.h b/libs/minisat/System.h
new file mode 100644
index 000000000..ee92a6e08
--- /dev/null
+++ b/libs/minisat/System.h
@@ -0,0 +1,72 @@
+/****************************************************************************************[System.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_System_h
+#define Minisat_System_h
+
+#if defined(__linux__)
+#include <fpu_control.h>
+#endif
+
+#include "IntTypes.h"
+
+//-------------------------------------------------------------------------------------------------
+
+namespace Minisat {
+
+static inline double cpuTime(void); // CPU-time in seconds.
+
+extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures).
+extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures).
+
+extern void setX86FPUPrecision(); // Make sure double's are represented with the same precision
+ // in memory and registers.
+
+extern void limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact
+ // semantics varies depending on architecture.
+
+extern void limitTime(uint32_t max_cpu_time); // Set a limit on maximum CPU time. The exact
+ // semantics varies depending on architecture.
+
+extern void sigTerm(void handler(int)); // Set up handling of available termination signals.
+
+}
+
+//-------------------------------------------------------------------------------------------------
+// Implementation of inline functions:
+
+#if defined(_MSC_VER) || defined(__MINGW32__)
+#include <time.h>
+
+static inline double Minisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
+
+#else
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+
+static inline double Minisat::cpuTime(void) {
+ struct rusage ru;
+ getrusage(RUSAGE_SELF, &ru);
+ return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+
+#endif
+
+#endif
diff --git a/libs/minisat/Vec.h b/libs/minisat/Vec.h
new file mode 100644
index 000000000..6e398801f
--- /dev/null
+++ b/libs/minisat/Vec.h
@@ -0,0 +1,134 @@
+/*******************************************************************************************[Vec.h]
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Minisat_Vec_h
+#define Minisat_Vec_h
+
+#include <assert.h>
+#include <limits>
+#include <new>
+
+#include "IntTypes.h"
+#include "XAlloc.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T, class _Size = int>
+class vec {
+public:
+ typedef _Size Size;
+private:
+ T* data;
+ Size sz;
+ Size cap;
+
+ // Don't allow copying (error prone):
+ vec<T>& operator=(vec<T>& other);
+ vec (vec<T>& other);
+
+ static inline Size max(Size x, Size y){ return (x > y) ? x : y; }
+
+public:
+ // Constructors:
+ vec() : data(NULL), sz(0), cap(0) { }
+ explicit vec(Size size) : data(NULL), sz(0), cap(0) { growTo(size); }
+ vec(Size size, const T& pad) : data(NULL), sz(0), cap(0) { growTo(size, pad); }
+ ~vec() { clear(true); }
+
+ // Pointer to first element:
+ operator T* (void) { return data; }
+
+ // Size operations:
+ Size size (void) const { return sz; }
+ void shrink (Size nelems) { assert(nelems <= sz); for (Size i = 0; i < nelems; i++) sz--, data[sz].~T(); }
+ void shrink_ (Size nelems) { assert(nelems <= sz); sz -= nelems; }
+ int capacity (void) const { return cap; }
+ void capacity (Size min_cap);
+ void growTo (Size size);
+ void growTo (Size size, const T& pad);
+ void clear (bool dealloc = false);
+
+ // Stack interface:
+ void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
+ //void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
+ void push (const T& elem) { if (sz == cap) capacity(sz+1); new (&data[sz++]) T(elem); }
+ void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
+ void pop (void) { assert(sz > 0); sz--, data[sz].~T(); }
+ // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
+ // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
+ // happen given the way capacities are calculated (below). Essentially, all capacities are
+ // even, but INT_MAX is odd.
+
+ const T& last (void) const { return data[sz-1]; }
+ T& last (void) { return data[sz-1]; }
+
+ // Vector interface:
+ const T& operator [] (Size index) const { return data[index]; }
+ T& operator [] (Size index) { return data[index]; }
+
+ // Duplicatation (preferred instead):
+ void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (Size i = 0; i < sz; i++) copy[i] = data[i]; }
+ void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
+};
+
+
+template<class T, class _Size>
+void vec<T,_Size>::capacity(Size min_cap) {
+ if (cap >= min_cap) return;
+ Size add = max((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
+ const Size size_max = std::numeric_limits<Size>::max();
+ if ( ((size_max <= std::numeric_limits<int>::max()) && (add > size_max - cap))
+ || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) )
+ throw OutOfMemoryException();
+ }
+
+
+template<class T, class _Size>
+void vec<T,_Size>::growTo(Size size, const T& pad) {
+ if (sz >= size) return;
+ capacity(size);
+ for (Size i = sz; i < size; i++) data[i] = pad;
+ sz = size; }
+
+
+template<class T, class _Size>
+void vec<T,_Size>::growTo(Size size) {
+ if (sz >= size) return;
+ capacity(size);
+ for (Size i = sz; i < size; i++) new (&data[i]) T();
+ sz = size; }
+
+
+template<class T, class _Size>
+void vec<T,_Size>::clear(bool dealloc) {
+ if (data != NULL){
+ for (Size i = 0; i < sz; i++) data[i].~T();
+ sz = 0;
+ if (dealloc) free(data), data = NULL, cap = 0; } }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/XAlloc.h b/libs/minisat/XAlloc.h
new file mode 100644
index 000000000..1da176028
--- /dev/null
+++ b/libs/minisat/XAlloc.h
@@ -0,0 +1,45 @@
+/****************************************************************************************[XAlloc.h]
+Copyright (c) 2009-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+
+#ifndef Minisat_XAlloc_h
+#define Minisat_XAlloc_h
+
+#include <errno.h>
+#include <stdlib.h>
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:
+
+class OutOfMemoryException{};
+static inline void* xrealloc(void *ptr, size_t size)
+{
+ void* mem = realloc(ptr, size);
+ if (mem == NULL && errno == ENOMEM){
+ throw OutOfMemoryException();
+ }else
+ return mem;
+}
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/sha1/sha1.cpp b/libs/sha1/sha1.cpp
index fb7bfed6f..dc86b2ce2 100644
--- a/libs/sha1/sha1.cpp
+++ b/libs/sha1/sha1.cpp
@@ -1,185 +1,270 @@
-/*
- Copyright (c) 2011, Micael Hildenborg
- All rights reserved.
-
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are met:
- * Redistributions of source code must retain the above copyright
- notice, this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright
- notice, this list of conditions and the following disclaimer in the
- documentation and/or other materials provided with the distribution.
- * Neither the name of Micael Hildenborg nor the
- names of its contributors may be used to endorse or promote products
- derived from this software without specific prior written permission.
-
- THIS SOFTWARE IS PROVIDED BY Micael Hildenborg ''AS IS'' AND ANY
- EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
- WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
- DISCLAIMED. IN NO EVENT SHALL Micael Hildenborg BE LIABLE FOR ANY
- DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
- (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
- LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
- ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
- */
-
-/*
- Contributors:
- Gustav
- Several members in the gamedev.se forum.
- Gregory Petrosyan
- */
-
-#include "sha1.h"
-
-namespace sha1
-{
- namespace // local
- {
- // Rotate an integer value to left.
- inline unsigned int rol(const unsigned int value,
- const unsigned int steps)
- {
- return ((value << steps) | (value >> (32 - steps)));
- }
-
- // Sets the first 16 integers in the buffert to zero.
- // Used for clearing the W buffert.
- inline void clearWBuffert(unsigned int* buffert)
- {
- for (int pos = 16; --pos >= 0;)
- {
- buffert[pos] = 0;
- }
- }
-
- void innerHash(unsigned int* result, unsigned int* w)
- {
- unsigned int a = result[0];
- unsigned int b = result[1];
- unsigned int c = result[2];
- unsigned int d = result[3];
- unsigned int e = result[4];
-
- int round = 0;
-
- #define sha1macro(func,val) \
- { \
- const unsigned int t = rol(a, 5) + (func) + e + val + w[round]; \
- e = d; \
- d = c; \
- c = rol(b, 30); \
- b = a; \
- a = t; \
- }
-
- while (round < 16)
- {
- sha1macro((b & c) | (~b & d), 0x5a827999)
- ++round;
- }
- while (round < 20)
- {
- w[round] = rol((w[round - 3] ^ w[round - 8] ^ w[round - 14] ^ w[round - 16]), 1);
- sha1macro((b & c) | (~b & d), 0x5a827999)
- ++round;
- }
- while (round < 40)
- {
- w[round] = rol((w[round - 3] ^ w[round - 8] ^ w[round - 14] ^ w[round - 16]), 1);
- sha1macro(b ^ c ^ d, 0x6ed9eba1)
- ++round;
- }
- while (round < 60)
- {
- w[round] = rol((w[round - 3] ^ w[round - 8] ^ w[round - 14] ^ w[round - 16]), 1);
- sha1macro((b & c) | (b & d) | (c & d), 0x8f1bbcdc)
- ++round;
- }
- while (round < 80)
- {
- w[round] = rol((w[round - 3] ^ w[round - 8] ^ w[round - 14] ^ w[round - 16]), 1);
- sha1macro(b ^ c ^ d, 0xca62c1d6)
- ++round;
- }
-
- #undef sha1macro
-
- result[0] += a;
- result[1] += b;
- result[2] += c;
- result[3] += d;
- result[4] += e;
- }
- } // namespace
-
- void calc(const void* src, const int bytelength, unsigned char* hash)
- {
- // Init the result array.
- unsigned int result[5] = { 0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476, 0xc3d2e1f0 };
-
- // Cast the void src pointer to be the byte array we can work with.
- const unsigned char* sarray = (const unsigned char*) src;
-
- // The reusable round buffer
- unsigned int w[80];
-
- // Loop through all complete 64byte blocks.
- const int endOfFullBlocks = bytelength - 64;
- int endCurrentBlock;
- int currentBlock = 0;
-
- while (currentBlock <= endOfFullBlocks)
- {
- endCurrentBlock = currentBlock + 64;
-
- // Init the round buffer with the 64 byte block data.
- for (int roundPos = 0; currentBlock < endCurrentBlock; currentBlock += 4)
- {
- // This line will swap endian on big endian and keep endian on little endian.
- w[roundPos++] = (unsigned int) sarray[currentBlock + 3]
- | (((unsigned int) sarray[currentBlock + 2]) << 8)
- | (((unsigned int) sarray[currentBlock + 1]) << 16)
- | (((unsigned int) sarray[currentBlock]) << 24);
- }
- innerHash(result, w);
- }
-
- // Handle the last and not full 64 byte block if existing.
- endCurrentBlock = bytelength - currentBlock;
- clearWBuffert(w);
- int lastBlockBytes = 0;
- for (;lastBlockBytes < endCurrentBlock; ++lastBlockBytes)
- {
- w[lastBlockBytes >> 2] |= (unsigned int) sarray[lastBlockBytes + currentBlock] << ((3 - (lastBlockBytes & 3)) << 3);
- }
- w[lastBlockBytes >> 2] |= 0x80 << ((3 - (lastBlockBytes & 3)) << 3);
- if (endCurrentBlock >= 56)
- {
- innerHash(result, w);
- clearWBuffert(w);
- }
- w[15] = bytelength << 3;
- innerHash(result, w);
-
- // Store hash in result pointer, and make sure we get in in the correct order on both endian models.
- for (int hashByte = 20; --hashByte >= 0;)
- {
- hash[hashByte] = (result[hashByte >> 2] >> (((3 - hashByte) & 0x3) << 3)) & 0xff;
- }
- }
-
- void toHexString(const unsigned char* hash, char* hexstring)
- {
- const char hexDigits[] = { "0123456789abcdef" };
-
- for (int hashByte = 20; --hashByte >= 0;)
- {
- hexstring[hashByte << 1] = hexDigits[(hash[hashByte] >> 4) & 0xf];
- hexstring[(hashByte << 1) + 1] = hexDigits[hash[hashByte] & 0xf];
- }
- hexstring[40] = 0;
- }
-} // namespace sha1
+/*
+ sha1.cpp - source code of
+
+ ============
+ SHA-1 in C++
+ ============
+
+ 100% Public Domain.
+
+ Original C Code
+ -- Steve Reid <steve@edmweb.com>
+ Small changes to fit into bglibs
+ -- Bruce Guenter <bruce@untroubled.org>
+ Translation to simpler C++ Code
+ -- Volker Grabsch <vog@notjusthosting.com>
+*/
+
+#include "sha1.h"
+#include <sstream>
+#include <iomanip>
+#include <fstream>
+
+/* Help macros */
+#define SHA1_ROL(value, bits) (((value) << (bits)) | (((value) & 0xffffffff) >> (32 - (bits))))
+#define SHA1_BLK(i) (block[i&15] = SHA1_ROL(block[(i+13)&15] ^ block[(i+8)&15] ^ block[(i+2)&15] ^ block[i&15],1))
+
+/* (R0+R1), R2, R3, R4 are the different operations used in SHA1 */
+#define SHA1_R0(v,w,x,y,z,i) z += ((w&(x^y))^y) + block[i] + 0x5a827999 + SHA1_ROL(v,5); w=SHA1_ROL(w,30);
+#define SHA1_R1(v,w,x,y,z,i) z += ((w&(x^y))^y) + SHA1_BLK(i) + 0x5a827999 + SHA1_ROL(v,5); w=SHA1_ROL(w,30);
+#define SHA1_R2(v,w,x,y,z,i) z += (w^x^y) + SHA1_BLK(i) + 0x6ed9eba1 + SHA1_ROL(v,5); w=SHA1_ROL(w,30);
+#define SHA1_R3(v,w,x,y,z,i) z += (((w|x)&y)|(w&x)) + SHA1_BLK(i) + 0x8f1bbcdc + SHA1_ROL(v,5); w=SHA1_ROL(w,30);
+#define SHA1_R4(v,w,x,y,z,i) z += (w^x^y) + SHA1_BLK(i) + 0xca62c1d6 + SHA1_ROL(v,5); w=SHA1_ROL(w,30);
+
+SHA1::SHA1()
+{
+ reset();
+}
+
+
+void SHA1::update(const std::string &s)
+{
+ std::istringstream is(s);
+ update(is);
+}
+
+
+void SHA1::update(std::istream &is)
+{
+ std::string rest_of_buffer;
+ read(is, rest_of_buffer, BLOCK_BYTES - buffer.size());
+ buffer += rest_of_buffer;
+
+ while (is)
+ {
+ uint32 block[BLOCK_INTS];
+ buffer_to_block(buffer, block);
+ transform(block);
+ read(is, buffer, BLOCK_BYTES);
+ }
+}
+
+
+/*
+ * Add padding and return the message digest.
+ */
+
+std::string SHA1::final()
+{
+ /* Total number of hashed bits */
+ uint64 total_bits = (transforms*BLOCK_BYTES + buffer.size()) * 8;
+
+ /* Padding */
+ buffer += 0x80;
+ unsigned int orig_size = buffer.size();
+ while (buffer.size() < BLOCK_BYTES)
+ {
+ buffer += (char)0x00;
+ }
+
+ uint32 block[BLOCK_INTS];
+ buffer_to_block(buffer, block);
+
+ if (orig_size > BLOCK_BYTES - 8)
+ {
+ transform(block);
+ for (unsigned int i = 0; i < BLOCK_INTS - 2; i++)
+ {
+ block[i] = 0;
+ }
+ }
+
+ /* Append total_bits, split this uint64 into two uint32 */
+ block[BLOCK_INTS - 1] = total_bits;
+ block[BLOCK_INTS - 2] = (total_bits >> 32);
+ transform(block);
+
+ /* Hex std::string */
+ std::ostringstream result;
+ for (unsigned int i = 0; i < DIGEST_INTS; i++)
+ {
+ result << std::hex << std::setfill('0') << std::setw(8);
+ result << (digest[i] & 0xffffffff);
+ }
+
+ /* Reset for next run */
+ reset();
+
+ return result.str();
+}
+
+
+std::string SHA1::from_file(const std::string &filename)
+{
+ std::ifstream stream(filename.c_str(), std::ios::binary);
+ SHA1 checksum;
+ checksum.update(stream);
+ return checksum.final();
+}
+
+
+void SHA1::reset()
+{
+ /* SHA1 initialization constants */
+ digest[0] = 0x67452301;
+ digest[1] = 0xefcdab89;
+ digest[2] = 0x98badcfe;
+ digest[3] = 0x10325476;
+ digest[4] = 0xc3d2e1f0;
+
+ /* Reset counters */
+ transforms = 0;
+ buffer = "";
+}
+
+
+/*
+ * Hash a single 512-bit block. This is the core of the algorithm.
+ */
+
+void SHA1::transform(uint32 block[BLOCK_BYTES])
+{
+ /* Copy digest[] to working vars */
+ uint32 a = digest[0];
+ uint32 b = digest[1];
+ uint32 c = digest[2];
+ uint32 d = digest[3];
+ uint32 e = digest[4];
+
+
+ /* 4 rounds of 20 operations each. Loop unrolled. */
+ SHA1_R0(a,b,c,d,e, 0);
+ SHA1_R0(e,a,b,c,d, 1);
+ SHA1_R0(d,e,a,b,c, 2);
+ SHA1_R0(c,d,e,a,b, 3);
+ SHA1_R0(b,c,d,e,a, 4);
+ SHA1_R0(a,b,c,d,e, 5);
+ SHA1_R0(e,a,b,c,d, 6);
+ SHA1_R0(d,e,a,b,c, 7);
+ SHA1_R0(c,d,e,a,b, 8);
+ SHA1_R0(b,c,d,e,a, 9);
+ SHA1_R0(a,b,c,d,e,10);
+ SHA1_R0(e,a,b,c,d,11);
+ SHA1_R0(d,e,a,b,c,12);
+ SHA1_R0(c,d,e,a,b,13);
+ SHA1_R0(b,c,d,e,a,14);
+ SHA1_R0(a,b,c,d,e,15);
+ SHA1_R1(e,a,b,c,d,16);
+ SHA1_R1(d,e,a,b,c,17);
+ SHA1_R1(c,d,e,a,b,18);
+ SHA1_R1(b,c,d,e,a,19);
+ SHA1_R2(a,b,c,d,e,20);
+ SHA1_R2(e,a,b,c,d,21);
+ SHA1_R2(d,e,a,b,c,22);
+ SHA1_R2(c,d,e,a,b,23);
+ SHA1_R2(b,c,d,e,a,24);
+ SHA1_R2(a,b,c,d,e,25);
+ SHA1_R2(e,a,b,c,d,26);
+ SHA1_R2(d,e,a,b,c,27);
+ SHA1_R2(c,d,e,a,b,28);
+ SHA1_R2(b,c,d,e,a,29);
+ SHA1_R2(a,b,c,d,e,30);
+ SHA1_R2(e,a,b,c,d,31);
+ SHA1_R2(d,e,a,b,c,32);
+ SHA1_R2(c,d,e,a,b,33);
+ SHA1_R2(b,c,d,e,a,34);
+ SHA1_R2(a,b,c,d,e,35);
+ SHA1_R2(e,a,b,c,d,36);
+ SHA1_R2(d,e,a,b,c,37);
+ SHA1_R2(c,d,e,a,b,38);
+ SHA1_R2(b,c,d,e,a,39);
+ SHA1_R3(a,b,c,d,e,40);
+ SHA1_R3(e,a,b,c,d,41);
+ SHA1_R3(d,e,a,b,c,42);
+ SHA1_R3(c,d,e,a,b,43);
+ SHA1_R3(b,c,d,e,a,44);
+ SHA1_R3(a,b,c,d,e,45);
+ SHA1_R3(e,a,b,c,d,46);
+ SHA1_R3(d,e,a,b,c,47);
+ SHA1_R3(c,d,e,a,b,48);
+ SHA1_R3(b,c,d,e,a,49);
+ SHA1_R3(a,b,c,d,e,50);
+ SHA1_R3(e,a,b,c,d,51);
+ SHA1_R3(d,e,a,b,c,52);
+ SHA1_R3(c,d,e,a,b,53);
+ SHA1_R3(b,c,d,e,a,54);
+ SHA1_R3(a,b,c,d,e,55);
+ SHA1_R3(e,a,b,c,d,56);
+ SHA1_R3(d,e,a,b,c,57);
+ SHA1_R3(c,d,e,a,b,58);
+ SHA1_R3(b,c,d,e,a,59);
+ SHA1_R4(a,b,c,d,e,60);
+ SHA1_R4(e,a,b,c,d,61);
+ SHA1_R4(d,e,a,b,c,62);
+ SHA1_R4(c,d,e,a,b,63);
+ SHA1_R4(b,c,d,e,a,64);
+ SHA1_R4(a,b,c,d,e,65);
+ SHA1_R4(e,a,b,c,d,66);
+ SHA1_R4(d,e,a,b,c,67);
+ SHA1_R4(c,d,e,a,b,68);
+ SHA1_R4(b,c,d,e,a,69);
+ SHA1_R4(a,b,c,d,e,70);
+ SHA1_R4(e,a,b,c,d,71);
+ SHA1_R4(d,e,a,b,c,72);
+ SHA1_R4(c,d,e,a,b,73);
+ SHA1_R4(b,c,d,e,a,74);
+ SHA1_R4(a,b,c,d,e,75);
+ SHA1_R4(e,a,b,c,d,76);
+ SHA1_R4(d,e,a,b,c,77);
+ SHA1_R4(c,d,e,a,b,78);
+ SHA1_R4(b,c,d,e,a,79);
+
+ /* Add the working vars back into digest[] */
+ digest[0] += a;
+ digest[1] += b;
+ digest[2] += c;
+ digest[3] += d;
+ digest[4] += e;
+
+ /* Count the number of transformations */
+ transforms++;
+}
+
+
+void SHA1::buffer_to_block(const std::string &buffer, uint32 block[BLOCK_BYTES])
+{
+ /* Convert the std::string (byte buffer) to a uint32 array (MSB) */
+ for (unsigned int i = 0; i < BLOCK_INTS; i++)
+ {
+ block[i] = (buffer[4*i+3] & 0xff)
+ | (buffer[4*i+2] & 0xff)<<8
+ | (buffer[4*i+1] & 0xff)<<16
+ | (buffer[4*i+0] & 0xff)<<24;
+ }
+}
+
+
+void SHA1::read(std::istream &is, std::string &s, int max)
+{
+ char sbuf[max];
+ is.read(sbuf, max);
+ s.assign(sbuf, is.gcount());
+}
+
+
+std::string sha1(const std::string &string)
+{
+ SHA1 checksum;
+ checksum.update(string);
+ return checksum.final();
+}
diff --git a/libs/sha1/sha1.h b/libs/sha1/sha1.h
index 540c156d1..15edee12e 100644
--- a/libs/sha1/sha1.h
+++ b/libs/sha1/sha1.h
@@ -1,49 +1,57 @@
-/*
- Copyright (c) 2011, Micael Hildenborg
- All rights reserved.
-
- Redistribution and use in source and binary forms, with or without
- modification, are permitted provided that the following conditions are met:
- * Redistributions of source code must retain the above copyright
- notice, this list of conditions and the following disclaimer.
- * Redistributions in binary form must reproduce the above copyright
- notice, this list of conditions and the following disclaimer in the
- documentation and/or other materials provided with the distribution.
- * Neither the name of Micael Hildenborg nor the
- names of its contributors may be used to endorse or promote products
- derived from this software without specific prior written permission.
-
- THIS SOFTWARE IS PROVIDED BY Micael Hildenborg ''AS IS'' AND ANY
- EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
- WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
- DISCLAIMED. IN NO EVENT SHALL Micael Hildenborg BE LIABLE FOR ANY
- DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
- (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
- LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
- ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
- SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
- */
-
-#ifndef SHA1_DEFINED
-#define SHA1_DEFINED
-
-namespace sha1
-{
-
- /**
- @param src points to any kind of data to be hashed.
- @param bytelength the number of bytes to hash from the src pointer.
- @param hash should point to a buffer of at least 20 bytes of size for storing the sha1 result in.
- */
- void calc(const void* src, const int bytelength, unsigned char* hash);
-
- /**
- @param hash is 20 bytes of sha1 hash. This is the same data that is the result from the calc function.
- @param hexstring should point to a buffer of at least 41 bytes of size for storing the hexadecimal representation of the hash. A zero will be written at position 40, so the buffer will be a valid zero ended string.
- */
- void toHexString(const unsigned char* hash, char* hexstring);
-
-} // namespace sha1
-
-#endif // SHA1_DEFINED
+/*
+ sha1.h - header of
+
+ ============
+ SHA-1 in C++
+ ============
+
+ 100% Public Domain.
+
+ Original C Code
+ -- Steve Reid <steve@edmweb.com>
+ Small changes to fit into bglibs
+ -- Bruce Guenter <bruce@untroubled.org>
+ Translation to simpler C++ Code
+ -- Volker Grabsch <vog@notjusthosting.com>
+*/
+
+#ifndef SHA1_HPP
+#define SHA1_HPP
+
+
+#include <iostream>
+#include <string>
+
+class SHA1
+{
+public:
+ SHA1();
+ void update(const std::string &s);
+ void update(std::istream &is);
+ std::string final();
+ static std::string from_file(const std::string &filename);
+
+private:
+ typedef unsigned long int uint32; /* just needs to be at least 32bit */
+ typedef unsigned long long uint64; /* just needs to be at least 64bit */
+
+ static const unsigned int DIGEST_INTS = 5; /* number of 32bit integers per SHA1 digest */
+ static const unsigned int BLOCK_INTS = 16; /* number of 32bit integers per SHA1 block */
+ static const unsigned int BLOCK_BYTES = BLOCK_INTS * 4;
+
+ uint32 digest[DIGEST_INTS];
+ std::string buffer;
+ uint64 transforms;
+
+ void reset();
+ void transform(uint32 block[BLOCK_BYTES]);
+
+ static void buffer_to_block(const std::string &buffer, uint32 block[BLOCK_BYTES]);
+ static void read(std::istream &is, std::string &s, int max);
+};
+
+std::string sha1(const std::string &string);
+
+
+
+#endif /* SHA1_HPP */
diff --git a/libs/subcircuit/subcircuit.cc b/libs/subcircuit/subcircuit.cc
index da2638792..84f23d636 100644
--- a/libs/subcircuit/subcircuit.cc
+++ b/libs/subcircuit/subcircuit.cc
@@ -26,8 +26,8 @@
#include <stdio.h>
#ifdef _YOSYS_
-# include "kernel/log.h"
-# define my_printf log
+# include "kernel/yosys.h"
+# define my_printf YOSYS_NAMESPACE_PREFIX log
#else
# define my_printf printf
#endif
diff --git a/libs/svgviewer/.gitignore b/libs/svgviewer/.gitignore
deleted file mode 100644
index b92d91f8b..000000000
--- a/libs/svgviewer/.gitignore
+++ /dev/null
@@ -1,5 +0,0 @@
-Makefile
-moc_mainwindow.cpp
-moc_svgview.cpp
-qrc_svgviewer.cpp
-svgviewer
diff --git a/libs/svgviewer/files/bubbles.svg b/libs/svgviewer/files/bubbles.svg
deleted file mode 100644
index 51730124a..000000000
--- a/libs/svgviewer/files/bubbles.svg
+++ /dev/null
@@ -1,215 +0,0 @@
-<?xml version="1.0" standalone="no"?>
-<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.0//EN" "http://www.w3.org/TR/2001/REC-SVG-20010904/DTD/svg10.dtd">
-<svg width="20cm" height="15cm" viewBox="0 0 800 600"
- xmlns="http://www.w3.org/2000/svg"
- xmlns:xlink="http://www.w3.org/1999/xlink/"
- baseProfile="tiny" version="1.2">
- <title>Spheres</title>
- <desc>Semi-transparent bubbles on a colored background.</desc>
- <defs>
- <!-- Create radial gradients for each bubble. -->
- <radialGradient id="blueBubble" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" stop-opacity="1" />
- <stop offset="25%" stop-color="#cdcdff" stop-opacity=".65" />
- <stop offset="100%" stop-color="#cdaacd" stop-opacity=".75" />
- </radialGradient>
- <radialGradient id="redBubble" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" stop-opacity="1" />
- <stop offset="25%" stop-color="#ffcdcd" stop-opacity=".65" />
- <stop offset="100%" stop-color="#bbbb99" stop-opacity=".75" />
- </radialGradient>
- <radialGradient id="greenBubble" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" stop-opacity="1" />
- <stop offset="25%" stop-color="#cdffcd" stop-opacity=".65" />
- <stop offset="100%" stop-color="#99aaaa" stop-opacity=".75" />
- </radialGradient>
- <radialGradient id="yellowBubble" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" stop-opacity="1" />
- <stop offset="25%" stop-color="#ffffcd" stop-opacity=".65" />
- <stop offset="100%" stop-color="#bbbbaa" stop-opacity=".75" />
- </radialGradient>
- <radialGradient id="background" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="400" fx="250" fy="250">
- <stop offset="0%" stop-color="#ffffee" />
- <stop offset="100%" stop-color="#ccccaa" />
- </radialGradient>
- <linearGradient id="surface" gradientUnits="userSpaceOnUse"
- x1="-100" y1="200" x2="400" y2="200">
- <stop offset="0%" stop-color="#ffffcc" />
- <stop offset="100%" stop-color="#bbbb88" />
- </linearGradient>
-
- <!-- Create radial gradients for each circle to make them look like
- spheres. -->
- <radialGradient id="blueSphere" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" />
- <stop offset="75%" stop-color="blue" />
- <stop offset="100%" stop-color="#222244" />
- </radialGradient>
- <radialGradient id="redSphere" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" />
- <stop offset="75%" stop-color="red" />
- <stop offset="100%" stop-color="#442222" />
- </radialGradient>
- <radialGradient id="greenSphere" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" />
- <stop offset="75%" stop-color="green" />
- <stop offset="100%" stop-color="#113311" />
- </radialGradient>
- <radialGradient id="yellowSphere" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" />
- <stop offset="75%" stop-color="yellow" />
- <stop offset="100%" stop-color="#444422" />
- </radialGradient>
- <radialGradient id="shadowGrad" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="50">
- <stop offset="0%" stop-color="black" stop-opacity="1.0" />
- <stop offset="100%" stop-color="black" stop-opacity="0.0" />
- </radialGradient>
-
- <!-- Define a shadow for each sphere. -->
- <circle id="shadow" fill="url(#shadowGrad)" cx="0" cy="0" r="100" />
- <g id="bubble">
- <circle fill="black" cx="0" cy="0" r="50" />
- <circle fill="#a6ce39" cx="0" cy="0" r="33" />
- <path fill="black" d="M 37,50 L 50,37 L 12,-1 L 22,-11 L 10,-24 L -24,10
- L -11,22 L -1,12 Z" />
- <circle cx="0" cy="0" r="100" />
- </g>
- </defs>
- <g>
- <rect fill="url(#background)" x="0" y="0" width="800" height="600" />
- </g>
-
- <g transform="translate(200,700)">
- <use xlink:href="#bubble" fill="url(#blueBubble)" />
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="1s" dur="10s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(315,700)">
- <g transform="scale(0.5,0.5)">
- <use xlink:href="#bubble" fill="url(#redBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="3s" dur="7s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(80,700)">
- <g transform="scale(0.65,0.65)">
- <use xlink:href="#bubble" fill="url(#greenBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="5s" dur="9s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(255,700)">
- <g transform="scale(0.3,0.3)">
- <use xlink:href="#bubble" fill="url(#yellowBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="2s" dur="6s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(565,700)">
- <g transform="scale(0.4,0.4)">
- <use xlink:href="#bubble" fill="url(#blueBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="4s" dur="8s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(715,700)">
- <g transform="scale(0.6,0.6)">
- <use xlink:href="#bubble" fill="url(#redBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="1s" dur="4s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(645,700)">
- <g transform="scale(0.375,0.375)">
- <use xlink:href="#bubble" fill="url(#greenBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="0s" dur="11s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(555,700)">
- <g transform="scale(0.9,0.9)">
- <use xlink:href="#bubble" fill="url(#yellowBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="3s" dur="7.5s" fill="freeze" repeatCount="indefinite" />
- </g>
-
- <g transform="translate(360,700)">
- <g transform="scale(0.5,0.5)">
- <use xlink:href="#bubble" fill="url(#blueBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="3s" dur="6s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(215,700)">
- <g transform="scale(0.45,0.45)">
- <use xlink:href="#bubble" fill="url(#redBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="5.5s" dur="7s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(420,700)">
- <g transform="scale(0.75,0.75)">
- <use xlink:href="#bubble" fill="url(#greenBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="1s" dur="9s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(815,700)">
- <g transform="scale(0.6,0.6)">
- <use xlink:href="#bubble" fill="url(#yellowBubble)" />
- </g>
- <animateTransform attributeName="transform" type="translate" additive="sum"
- values="0,0; 0,-800" begin="2s" dur="9.5s" fill="freeze" repeatCount="indefinite" />
- </g>
-
- <g transform="translate(225,375)" >
- <g transform="scale(1.0,0.5)" >
- <path d="M 0 0 L 350 0 L 450 450 L -100 450 z"
- fill="url(#surface)" stroke="none" />
- </g>
- </g>
- <g transform="translate(200,0)" >
- <g transform="translate(200,490) scale(2.0,1.0) rotate(45)" >
- <rect fill="#a6ce39" x="-69" y="-69" width="138" height="138" />
- <circle fill="black" cx="0" cy="0" r="50" />
- <circle fill="#a6ce39" cx="0" cy="0" r="33" />
- <path fill="black" d="M 37,50 L 50,37 L 12,-1 L 22,-11 L 10,-24 L -24,10
- L -11,22 L -1,12 Z" />
- <animateTransform attributeName="transform" type="rotate" additive="sum" values="0; 360"
- begin="0s" dur="10s" fill="freeze" repeatCount="indefinite" />
- </g>
- <g transform="translate(200,375)">
- <use xlink:href="#shadow" transform="translate(25,55) scale(1.0,0.5)" />
- <circle fill="url(#blueSphere)" cx="0" cy="0" r="100" />
- </g>
- <g transform="translate(315,440)">
- <g transform="scale(0.5,0.5)">
- <use xlink:href="#shadow" transform="translate(25,55) scale(1.0,0.5)" />
- <circle fill="url(#redSphere)" cx="0" cy="0" r="100" />
- </g>
- </g>
- <g transform="translate(80,475)">
- <g transform="scale(0.65,0.65)">
- <use xlink:href="#shadow" transform="translate(25,55) scale(1.0,0.5)" />
- <circle fill="url(#greenSphere)" cx="0" cy="0" r="100" />
- </g>
- </g>
- <g transform="translate(255,525)">
- <g transform="scale(0.3,0.3)">
- <use xlink:href="#shadow" transform="translate(25,55) scale(1.0,0.5)" />
- <circle fill="url(#yellowSphere)" cx="0" cy="0" r="100" />
- </g>
- </g>
- </g>
-</svg>
diff --git a/libs/svgviewer/files/cubic.svg b/libs/svgviewer/files/cubic.svg
deleted file mode 100644
index 492bb72b8..000000000
--- a/libs/svgviewer/files/cubic.svg
+++ /dev/null
@@ -1,77 +0,0 @@
-<?xml version="1.0" standalone="no"?>
-<svg width="10cm" height="10cm" viewBox="0 0 1000 1000"
- xmlns="http://www.w3.org/2000/svg" version="1.2" baseProfile="tiny">
- <title>Example cubic02 - cubic Bezier commands in path data</title>
- <desc>Picture showing examples of "C" and "S" commands,
- along with annotations showing the control points
- and end points</desc>
-
- <rect fill="none" stroke="blue" stroke-width="1" x="1" y="1" width="998" height="998" />
-
- <!-- Path 1 -->
- <polyline fill="none" stroke="#888888" stroke-width="2" points="100,200 100,100" />
- <polyline fill="none" stroke="#888888" stroke-width="2" points="400,100 400,200" />
- <path fill="none" stroke="red" stroke-width="5" d="M100,200 C100,100 400,100 400,200" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="100" cy="200" r="10" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="400" cy="200" r="10" />
- <circle class="CtlPoint" cx="100" cy="100" r="10" />
- <circle class="CtlPoint" cx="400" cy="100" r="10" />
- <text text-anchor="middle" font-size="22" font-family="Verdana" x="250" y="275">M100,200 C100,100 400,100 400,200</text>
-
- <!-- Path 2 -->
- <polyline fill="none" stroke="#888888" stroke-width="2" points="100,500 25,400" />
- <polyline fill="none" stroke="#888888" stroke-width="2" points="475,400 400,500" />
- <path fill="none" stroke="red" stroke-width="5" d="M100,500 C25,400 475,400 400,500" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="100" cy="500" r="10" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="400" cy="500" r="10" />
- <circle fill="#888888" stroke="none" cx="25" cy="400" r="10" />
- <circle fill="#888888" stroke="none" cx="475" cy="400" r="10" />
- <text text-anchor="middle" font-size="22" font-family="Verdana" x="250" y="575">M100,500 C25,400 475,400 400,500</text>
-
- <!-- Path 3 -->
- <polyline fill="none" stroke="#888888" stroke-width="2" points="100,800 175,700" />
- <polyline fill="none" stroke="#888888" stroke-width="2" points="325,700 400,800" />
- <path fill="none" stroke="red" stroke-width="5" d="M100,800 C175,700 325,700 400,800" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="100" cy="800" r="10" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="400" cy="800" r="10" />
- <circle fill="#888888" stroke="none" cx="175" cy="700" r="10" />
- <circle fill="#888888" stroke="none" cx="325" cy="700" r="10" />
- <text text-anchor="middle" font-size="22" font-family="Verdana" x="250" y="875">M100,800 C175,700 325,700 400,800</text>
-
- <!-- Path 4 -->
- <polyline fill="none" stroke="#888888" stroke-width="2" points="600,200 675,100" />
- <polyline fill="none" stroke="#888888" stroke-width="2" points="975,100 900,200" />
- <path fill="none" stroke="red" stroke-width="5" d="M600,200 C675,100 975,100 900,200" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="600" cy="200" r="10" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="900" cy="200" r="10" />
- <circle fill="#888888" stroke="none" cx="675" cy="100" r="10" />
- <circle fill="#888888" stroke="none" cx="975" cy="100" r="10" />
- <text text-anchor="middle" font-size="22" font-family="Verdana" x="750" y="275">M600,200 C675,100 975,100 900,200</text>
-
- <!-- Path 5 -->
- <polyline fill="none" stroke="#888888" stroke-width="2" points="600,500 600,350" />
- <polyline fill="none" stroke="#888888" stroke-width="2" points="900,650 900,500" />
- <path fill="none" stroke="red" stroke-width="5" d="M600,500 C600,350 900,650 900,500" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="600" cy="500" r="10" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="900" cy="500" r="10" />
- <circle fill="#888888" stroke="none" cx="600" cy="350" r="10" />
- <circle fill="#888888" stroke="none" cx="900" cy="650" r="10" />
- <text text-anchor="middle" font-size="22" font-family="Verdana" x="750" y="575">M600,500 C600,350 900,650 900,500</text>
-
- <!-- Path 6 (C and S command) -->
- <polyline fill="none" stroke="#888888" stroke-width="2" points="600,800 625,700" />
- <polyline fill="none" stroke="#888888" stroke-width="2" points="725,700 750,800" />
- <polyline fill="none" stroke="#888888" stroke-width="2" points="750,800 775,900" />
- <polyline fill="none" stroke="#888888" stroke-width="2" points="875,900 900,800" />
- <path fill="none" stroke="red" stroke-width="5" d="M600,800 C625,700 725,700 750,800
- S875,900 900,800" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="600" cy="800" r="10" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="750" cy="800" r="10" />
- <circle fill="none" stroke="#888888" stroke-width="2" cx="900" cy="800" r="10" />
- <circle fill="#888888" stroke="none" cx="625" cy="700" r="10" />
- <circle fill="#888888" stroke="none" cx="725" cy="700" r="10" />
- <circle fill="#888888" stroke="none" cx="875" cy="900" r="10" />
- <circle fill="none" stroke="blue" stroke-width="4" cx="775" cy="900" r="9" />
- <text text-anchor="middle" font-size="22" font-family="Verdana" x="750" y="945">M600,800 C625,700 725,700 750,800</text>
- <text text-anchor="middle" font-size="22" font-family="Verdana" x="750" y="975">S875,900 900,800</text>
-</svg>
diff --git a/libs/svgviewer/files/spheres.svg b/libs/svgviewer/files/spheres.svg
deleted file mode 100644
index b23164bce..000000000
--- a/libs/svgviewer/files/spheres.svg
+++ /dev/null
@@ -1,72 +0,0 @@
-<?xml version="1.0" standalone="no"?>
-<svg width="8cm" height="8cm" viewBox="0 0 400 400"
- xmlns="http://www.w3.org/2000/svg"
- xmlns:xlink="http://www.w3.org/1999/xlink/"
- baseProfile="tiny" version="1.2">
- <title>Spheres</title>
- <desc>Gradient filled spheres with different colors.</desc>
- <defs>
- <!-- Create radial gradients for each circle to make them look like
- spheres. -->
- <radialGradient id="blueSphere" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" />
- <stop offset="75%" stop-color="blue" />
- <stop offset="100%" stop-color="#222244" />
- </radialGradient>
- <radialGradient id="redSphere" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" />
- <stop offset="75%" stop-color="red" />
- <stop offset="100%" stop-color="#442222" />
- </radialGradient>
- <radialGradient id="greenSphere" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" />
- <stop offset="75%" stop-color="green" />
- <stop offset="100%" stop-color="#113311" />
- </radialGradient>
- <radialGradient id="yellowSphere" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="-50">
- <stop offset="0%" stop-color="white" />
- <stop offset="75%" stop-color="yellow" />
- <stop offset="100%" stop-color="#444422" />
- </radialGradient>
- <radialGradient id="shadowGrad" gradientUnits="userSpaceOnUse"
- cx="0" cy="0" r="100" fx="-50" fy="50">
- <stop offset="0%" stop-color="black" stop-opacity="1.0" />
- <stop offset="100%" stop-color="white" stop-opacity="0.0" />
- </radialGradient>
-
- <!-- Define a shadow for each sphere. -->
- <circle id="shadow" fill="url(#shadowGrad)" cx="0" cy="0" r="100" />
- </defs>
- <g fill="#ffee99" stroke="none" >
- <rect x="0" y="0" width="400" height="400" />
- </g>
- <g fill="white" stroke="none" >
- <rect x="0" y="175" width="400" height="225" />
- </g>
- <g transform="translate(200,175)">
- <use xlink:href="#shadow" transform="translate(25,55) scale(1.0,0.5)" />
- <circle fill="url(#blueSphere)" cx="0" cy="0" r="100" />
- </g>
- <g transform="translate(315,240)">
- <g transform="scale(0.5,0.5)">
- <use xlink:href="#shadow" transform="translate(25,55) scale(1.0,0.5)" />
- <circle fill="url(#redSphere)" cx="0" cy="0" r="100" />
- </g>
- </g>
- <g transform="translate(80,275)">
- <g transform="scale(0.65,0.65)">
- <use xlink:href="#shadow" transform="translate(25,55) scale(1.0,0.5)" />
- <circle fill="url(#greenSphere)" cx="0" cy="0" r="100" />
- </g>
- </g>
- <g transform="translate(255,325)">
- <g transform="scale(0.3,0.3)">
- <use xlink:href="#shadow" transform="translate(25,55) scale(1.0,0.5)" />
- <circle fill="url(#yellowSphere)" cx="0" cy="0" r="100" />
- </g>
- </g>
-</svg>
diff --git a/libs/svgviewer/main.cpp b/libs/svgviewer/main.cpp
deleted file mode 100644
index 34866f854..000000000
--- a/libs/svgviewer/main.cpp
+++ /dev/null
@@ -1,66 +0,0 @@
-/****************************************************************************
-**
-** Copyright (C) 2013 Digia Plc and/or its subsidiary(-ies).
-** Contact: http://www.qt-project.org/legal
-**
-** This file is part of the examples of the Qt Toolkit.
-**
-** $QT_BEGIN_LICENSE:BSD$
-** You may use this file under the terms of the BSD license as follows:
-**
-** "Redistribution and use in source and binary forms, with or without
-** modification, are permitted provided that the following conditions are
-** met:
-** * Redistributions of source code must retain the above copyright
-** notice, this list of conditions and the following disclaimer.
-** * Redistributions in binary form must reproduce the above copyright
-** notice, this list of conditions and the following disclaimer in
-** the documentation and/or other materials provided with the
-** distribution.
-** * Neither the name of Digia Plc and its Subsidiary(-ies) nor the names
-** of its contributors may be used to endorse or promote products derived
-** from this software without specific prior written permission.
-**
-**
-** THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-** "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-** LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-** A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-** OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-** SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-** LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-** DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-** THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-** (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-** OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
-**
-** $QT_END_LICENSE$
-**
-****************************************************************************/
-
-#include <QApplication>
-#include <QString>
-#ifndef QT_NO_OPENGL
-#include <QGLFormat>
-#endif
-
-#include "mainwindow.h"
-
-int main(int argc, char **argv)
-{
- Q_INIT_RESOURCE(svgviewer);
-
- QApplication app(argc, argv);
-
- MainWindow window;
- if (argc == 2)
- window.openFile(argv[1]);
- else
- window.openFile(":/files/bubbles.svg");
-#if defined(Q_OS_SYMBIAN)
- window.showMaximized();
-#else
- window.show();
-#endif
- return app.exec();
-}
diff --git a/libs/svgviewer/mainwindow.cpp b/libs/svgviewer/mainwindow.cpp
deleted file mode 100644
index 70da140eb..000000000
--- a/libs/svgviewer/mainwindow.cpp
+++ /dev/null
@@ -1,205 +0,0 @@
-/****************************************************************************
-**
-** Copyright (C) 2013 Digia Plc and/or its subsidiary(-ies).
-** Contact: http://www.qt-project.org/legal
-**
-** This file is part of the examples of the Qt Toolkit.
-**
-** $QT_BEGIN_LICENSE:BSD$
-** You may use this file under the terms of the BSD license as follows:
-**
-** "Redistribution and use in source and binary forms, with or without
-** modification, are permitted provided that the following conditions are
-** met:
-** * Redistributions of source code must retain the above copyright
-** notice, this list of conditions and the following disclaimer.
-** * Redistributions in binary form must reproduce the above copyright
-** notice, this list of conditions and the following disclaimer in
-** the documentation and/or other materials provided with the
-** distribution.
-** * Neither the name of Digia Plc and its Subsidiary(-ies) nor the names
-** of its contributors may be used to endorse or promote products derived
-** from this software without specific prior written permission.
-**
-**
-** THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-** "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-** LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-** A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-** OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-** SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-** LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-** DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-** THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-** (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-** OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
-**
-** $QT_END_LICENSE$
-**
-****************************************************************************/
-
-#include "mainwindow.h"
-
-#include <QtGui>
-#include <unistd.h>
-#include <QFileSystemWatcher>
-
-#include "svgview.h"
-
-MainWindow::MainWindow()
- : QMainWindow()
- , m_view(new SvgView)
- , m_watcher(NULL)
- , m_filehandle(NULL)
-{
- QMenu *fileMenu = new QMenu(tr("&File"), this);
- QAction *openAction = fileMenu->addAction(tr("&Open..."));
- openAction->setShortcut(QKeySequence(tr("Ctrl+O")));
- QAction *quitAction = fileMenu->addAction(tr("E&xit"));
- quitAction->setShortcuts(QKeySequence::Quit);
-
- menuBar()->addMenu(fileMenu);
-
- QMenu *viewMenu = new QMenu(tr("&View"), this);
-
- m_interactiveAction = viewMenu->addAction(tr("&Interactive"));
- m_interactiveAction->setEnabled(false);
- m_interactiveAction->setCheckable(true);
- m_interactiveAction->setChecked(false);
- connect(m_interactiveAction, SIGNAL(toggled(bool)), m_view, SLOT(setViewInteractive(bool)));
-
- m_backgroundAction = viewMenu->addAction(tr("&Background"));
- m_backgroundAction->setEnabled(false);
- m_backgroundAction->setCheckable(true);
- m_backgroundAction->setChecked(false);
- m_backgroundAction->setVisible(false);
- connect(m_backgroundAction, SIGNAL(toggled(bool)), m_view, SLOT(setViewBackground(bool)));
-
- m_outlineAction = viewMenu->addAction(tr("&Outline"));
- m_outlineAction->setEnabled(false);
- m_outlineAction->setCheckable(true);
- m_outlineAction->setChecked(true);
- connect(m_outlineAction, SIGNAL(toggled(bool)), m_view, SLOT(setViewOutline(bool)));
-
- menuBar()->addMenu(viewMenu);
-
- QMenu *rendererMenu = new QMenu(tr("&Renderer"), this);
- m_nativeAction = rendererMenu->addAction(tr("&Native"));
- m_nativeAction->setCheckable(true);
- m_nativeAction->setChecked(true);
-#ifndef QT_NO_OPENGL
- m_glAction = rendererMenu->addAction(tr("&OpenGL"));
- m_glAction->setCheckable(true);
-#endif
- m_imageAction = rendererMenu->addAction(tr("&Image"));
- m_imageAction->setCheckable(true);
-
-#ifndef QT_NO_OPENGL
- rendererMenu->addSeparator();
- m_highQualityAntialiasingAction = rendererMenu->addAction(tr("&High Quality Antialiasing"));
- m_highQualityAntialiasingAction->setEnabled(false);
- m_highQualityAntialiasingAction->setCheckable(true);
- m_highQualityAntialiasingAction->setChecked(false);
- connect(m_highQualityAntialiasingAction, SIGNAL(toggled(bool)), m_view, SLOT(setHighQualityAntialiasing(bool)));
-#endif
-
- QActionGroup *rendererGroup = new QActionGroup(this);
- rendererGroup->addAction(m_nativeAction);
-#ifndef QT_NO_OPENGL
- rendererGroup->addAction(m_glAction);
-#endif
- rendererGroup->addAction(m_imageAction);
-
- menuBar()->addMenu(rendererMenu);
-
- connect(openAction, SIGNAL(triggered()), this, SLOT(openFile()));
- connect(quitAction, SIGNAL(triggered()), qApp, SLOT(quit()));
- connect(rendererGroup, SIGNAL(triggered(QAction*)),
- this, SLOT(setRenderer(QAction*)));
-
- setCentralWidget(m_view);
- setWindowTitle(tr("Yosys SVG Viewer"));
-}
-
-void MainWindow::openFile(const QString &path, bool reload)
-{
- QString fileName;
- if (path.isNull())
- fileName = QFileDialog::getOpenFileName(this, tr("Open SVG File"),
- m_currentPath, "SVG files (*.svg *.svgz *.svg.gz)");
- else
- fileName = path;
-
- if (m_watcher) {
- delete m_watcher;
- m_watcher = NULL;
- }
- if (m_filehandle) {
- fclose(m_filehandle);
- m_filehandle = NULL;
- }
-
- if (!fileName.isEmpty()) {
- QFile file(fileName);
- if (!file.exists()) {
- QMessageBox::critical(this, tr("Open SVG File"),
- QString("Could not open file '%1'.").arg(fileName));
-
- m_interactiveAction->setEnabled(false);
- m_outlineAction->setEnabled(false);
- m_backgroundAction->setEnabled(false);
- return;
- }
-
- QTransform oldTransform = m_view->transform();
- m_view->openFile(file);
-
- if (!fileName.startsWith(":/"))
- {
- m_currentPath = fileName;
- setWindowTitle(tr("%1 - Yosys SVG Viewer").arg(m_currentPath));
-
- // just keep the file open so this process is found using 'fuser'
- m_filehandle = fopen(fileName.toAscii(), "r");
-
- m_watcher = new QFileSystemWatcher(this);
- m_watcher->addPath(fileName);
- connect(m_watcher, SIGNAL(fileChanged(const QString&)), this, SLOT(reloadFile()));
- }
-
- m_interactiveAction->setEnabled(true);
- m_outlineAction->setEnabled(true);
- m_backgroundAction->setEnabled(true);
-
- if (reload)
- m_view->setTransform(oldTransform);
- else
- resize(m_view->sizeHint() + QSize(80, 80 + menuBar()->height()));
- }
-}
-
-void MainWindow::reloadFile()
-{
- // give the writer ~100 ms to finish writing
- usleep(100000);
- openFile(m_currentPath, true);
-}
-
-void MainWindow::setRenderer(QAction *action)
-{
-#ifndef QT_NO_OPENGL
- m_highQualityAntialiasingAction->setEnabled(false);
-#endif
-
- if (action == m_nativeAction)
- m_view->setRenderer(SvgView::Native);
-#ifndef QT_NO_OPENGL
- else if (action == m_glAction) {
- m_highQualityAntialiasingAction->setEnabled(true);
- m_view->setRenderer(SvgView::OpenGL);
- }
-#endif
- else if (action == m_imageAction) {
- m_view->setRenderer(SvgView::Image);
- }
-}
diff --git a/libs/svgviewer/mainwindow.h b/libs/svgviewer/mainwindow.h
deleted file mode 100644
index dfb5586d4..000000000
--- a/libs/svgviewer/mainwindow.h
+++ /dev/null
@@ -1,86 +0,0 @@
-/****************************************************************************
-**
-** Copyright (C) 2013 Digia Plc and/or its subsidiary(-ies).
-** Contact: http://www.qt-project.org/legal
-**
-** This file is part of the examples of the Qt Toolkit.
-**
-** $QT_BEGIN_LICENSE:BSD$
-** You may use this file under the terms of the BSD license as follows:
-**
-** "Redistribution and use in source and binary forms, with or without
-** modification, are permitted provided that the following conditions are
-** met:
-** * Redistributions of source code must retain the above copyright
-** notice, this list of conditions and the following disclaimer.
-** * Redistributions in binary form must reproduce the above copyright
-** notice, this list of conditions and the following disclaimer in
-** the documentation and/or other materials provided with the
-** distribution.
-** * Neither the name of Digia Plc and its Subsidiary(-ies) nor the names
-** of its contributors may be used to endorse or promote products derived
-** from this software without specific prior written permission.
-**
-**
-** THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-** "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-** LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-** A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-** OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-** SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-** LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-** DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-** THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-** (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-** OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
-**
-** $QT_END_LICENSE$
-**
-****************************************************************************/
-
-#ifndef MAINWINDOW_H
-#define MAINWINDOW_H
-
-#include <QMainWindow>
-#include <QString>
-#include <stdio.h>
-
-class SvgView;
-
-QT_BEGIN_NAMESPACE
-class QAction;
-class QGraphicsView;
-class QGraphicsScene;
-class QGraphicsRectItem;
-class QFileSystemWatcher;
-QT_END_NAMESPACE
-
-class MainWindow : public QMainWindow
-{
- Q_OBJECT
-
-public:
- MainWindow();
-
-public slots:
- void openFile(const QString &path = QString(), bool reload = false);
- void setRenderer(QAction *action);
- void reloadFile();
-
-private:
- QAction *m_nativeAction;
- QAction *m_glAction;
- QAction *m_imageAction;
- QAction *m_highQualityAntialiasingAction;
- QAction *m_interactiveAction;
- QAction *m_backgroundAction;
- QAction *m_outlineAction;
-
- SvgView *m_view;
-
- QString m_currentPath;
- QFileSystemWatcher *m_watcher;
- FILE *m_filehandle;
-};
-
-#endif
diff --git a/libs/svgviewer/svgview.cpp b/libs/svgviewer/svgview.cpp
deleted file mode 100644
index 5a1a5ab29..000000000
--- a/libs/svgviewer/svgview.cpp
+++ /dev/null
@@ -1,227 +0,0 @@
-/****************************************************************************
-**
-** Copyright (C) 2013 Digia Plc and/or its subsidiary(-ies).
-** Contact: http://www.qt-project.org/legal
-**
-** This file is part of the examples of the Qt Toolkit.
-**
-** $QT_BEGIN_LICENSE:BSD$
-** You may use this file under the terms of the BSD license as follows:
-**
-** "Redistribution and use in source and binary forms, with or without
-** modification, are permitted provided that the following conditions are
-** met:
-** * Redistributions of source code must retain the above copyright
-** notice, this list of conditions and the following disclaimer.
-** * Redistributions in binary form must reproduce the above copyright
-** notice, this list of conditions and the following disclaimer in
-** the documentation and/or other materials provided with the
-** distribution.
-** * Neither the name of Digia Plc and its Subsidiary(-ies) nor the names
-** of its contributors may be used to endorse or promote products derived
-** from this software without specific prior written permission.
-**
-**
-** THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-** "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-** LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-** A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-** OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-** SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-** LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-** DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-** THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-** (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-** OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
-**
-** $QT_END_LICENSE$
-**
-****************************************************************************/
-#include "svgview.h"
-
-#include <QFile>
-#include <QWheelEvent>
-#include <QMouseEvent>
-#include <QGraphicsRectItem>
-#include <QGraphicsSvgItem>
-#include <QGraphicsWebView>
-#include <QPaintEvent>
-#include <qmath.h>
-#include <unistd.h>
-
-#ifndef QT_NO_OPENGL
-#include <QGLWidget>
-#endif
-
-SvgView::SvgView(QWidget *parent)
- : QGraphicsView(parent)
- , m_renderer(Native)
- , m_svgItem(0)
- , m_webview(0)
- , m_backgroundItem(0)
- , m_outlineItem(0)
-{
- setScene(new QGraphicsScene(this));
- setTransformationAnchor(AnchorUnderMouse);
- setDragMode(ScrollHandDrag);
- setViewportUpdateMode(FullViewportUpdate);
-
- // Prepare background check-board pattern
- QPixmap tilePixmap(64, 64);
- tilePixmap.fill(Qt::white);
- QPainter tilePainter(&tilePixmap);
- QColor color(220, 220, 220);
- tilePainter.fillRect(0, 0, 32, 32, color);
- tilePainter.fillRect(32, 32, 32, 32, color);
- tilePainter.end();
-
- setBackgroundBrush(tilePixmap);
-}
-
-void SvgView::drawBackground(QPainter *p, const QRectF &)
-{
- p->save();
- p->resetTransform();
- p->drawTiledPixmap(viewport()->rect(), backgroundBrush().texture());
- p->restore();
-}
-
-void SvgView::openFile(const QFile &file)
-{
- if (!file.exists())
- return;
-
- QGraphicsScene *s = scene();
-
- fn = file.fileName();
- if (fn[0] != '/') {
- char cwd_buffer[4096];
- if (getcwd(cwd_buffer, 4096) != NULL)
- fn = cwd_buffer + ("/" + fn);
- }
-
- bool drawBackground = (m_backgroundItem ? m_backgroundItem->isVisible() : false);
- bool drawOutline = (m_outlineItem ? m_outlineItem->isVisible() : true);
- bool useWebview = (m_webview ? m_webview->isVisible() : false);
-
- s->clear();
- resetTransform();
-
- m_svgItem = new QGraphicsSvgItem(file.fileName());
- m_svgItem->setFlags(QGraphicsItem::ItemClipsToShape);
- m_svgItem->setCacheMode(QGraphicsItem::NoCache);
- m_svgItem->setVisible(!useWebview);
- m_svgItem->setZValue(1);
- s->addItem(m_svgItem);
-
- if (useWebview) {
- m_webview = new QGraphicsWebView();
- m_webview->load(QUrl::fromLocalFile(fn));
- m_webview->setResizesToContents(true);
- m_webview->setZoomFactor(0.75);
- m_webview->setVisible(useWebview);
- m_webview->setZValue(1);
- s->addItem(m_webview);
- } else
- m_webview = NULL;
-
- m_backgroundItem = new QGraphicsRectItem(m_svgItem->boundingRect());
- m_backgroundItem->setBrush(Qt::white);
- m_backgroundItem->setPen(Qt::NoPen);
- m_backgroundItem->setVisible(drawBackground);
- m_backgroundItem->setZValue(0);
- s->addItem(m_backgroundItem);
-
- m_outlineItem = new QGraphicsRectItem(m_svgItem->boundingRect());
- QPen outline(Qt::black, 2, Qt::DashLine);
- outline.setCosmetic(true);
- m_outlineItem->setPen(outline);
- m_outlineItem->setBrush(Qt::NoBrush);
- m_outlineItem->setVisible(drawOutline);
- m_outlineItem->setZValue(2);
- s->addItem(m_outlineItem);
-
- s->setSceneRect(m_outlineItem->boundingRect().adjusted(-10, -10, 10, 10));
-}
-
-void SvgView::setRenderer(RendererType type)
-{
- m_renderer = type;
-
- if (m_renderer == OpenGL) {
-#ifndef QT_NO_OPENGL
- setViewport(new QGLWidget(QGLFormat(QGL::SampleBuffers)));
-#endif
- } else {
- setViewport(new QWidget);
- }
-}
-
-void SvgView::setHighQualityAntialiasing(bool highQualityAntialiasing)
-{
-#ifndef QT_NO_OPENGL
- setRenderHint(QPainter::HighQualityAntialiasing, highQualityAntialiasing);
-#else
- Q_UNUSED(highQualityAntialiasing);
-#endif
-}
-
-void SvgView::setViewInteractive(bool enable)
-{
- if (!m_svgItem)
- return;
- if (!m_webview) {
- m_webview = new QGraphicsWebView();
- m_webview->load(QUrl::fromLocalFile(fn));
- m_webview->setResizesToContents(true);
- m_webview->setZoomFactor(0.75);
- m_webview->setVisible(false);
- m_webview->setZValue(1);
- m_svgItem->scene()->addItem(m_webview);
- }
- m_svgItem->setVisible(!enable);
- m_webview->setVisible(enable);
-}
-
-void SvgView::setViewBackground(bool enable)
-{
- if (!m_backgroundItem)
- return;
-
- m_backgroundItem->setVisible(enable);
-}
-
-void SvgView::setViewOutline(bool enable)
-{
- if (!m_outlineItem)
- return;
-
- m_outlineItem->setVisible(enable);
-}
-
-void SvgView::paintEvent(QPaintEvent *event)
-{
- if (m_renderer == Image) {
- if (m_image.size() != viewport()->size()) {
- m_image = QImage(viewport()->size(), QImage::Format_ARGB32_Premultiplied);
- }
-
- QPainter imagePainter(&m_image);
- QGraphicsView::render(&imagePainter);
- imagePainter.end();
-
- QPainter p(viewport());
- p.drawImage(0, 0, m_image);
-
- } else {
- QGraphicsView::paintEvent(event);
- }
-}
-
-void SvgView::wheelEvent(QWheelEvent *event)
-{
- qreal factor = qPow(1.2, event->delta() / 240.0);
- scale(factor, factor);
- event->accept();
-}
-
diff --git a/libs/svgviewer/svgview.h b/libs/svgviewer/svgview.h
deleted file mode 100644
index 833bb52e0..000000000
--- a/libs/svgviewer/svgview.h
+++ /dev/null
@@ -1,87 +0,0 @@
-/****************************************************************************
-**
-** Copyright (C) 2013 Digia Plc and/or its subsidiary(-ies).
-** Contact: http://www.qt-project.org/legal
-**
-** This file is part of the examples of the Qt Toolkit.
-**
-** $QT_BEGIN_LICENSE:BSD$
-** You may use this file under the terms of the BSD license as follows:
-**
-** "Redistribution and use in source and binary forms, with or without
-** modification, are permitted provided that the following conditions are
-** met:
-** * Redistributions of source code must retain the above copyright
-** notice, this list of conditions and the following disclaimer.
-** * Redistributions in binary form must reproduce the above copyright
-** notice, this list of conditions and the following disclaimer in
-** the documentation and/or other materials provided with the
-** distribution.
-** * Neither the name of Digia Plc and its Subsidiary(-ies) nor the names
-** of its contributors may be used to endorse or promote products derived
-** from this software without specific prior written permission.
-**
-**
-** THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-** "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-** LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-** A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-** OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-** SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-** LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-** DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-** THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-** (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-** OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
-**
-** $QT_END_LICENSE$
-**
-****************************************************************************/
-
-#ifndef SVGVIEW_H
-#define SVGVIEW_H
-
-#include <QGraphicsView>
-#include <QGraphicsWebView>
-
-QT_BEGIN_NAMESPACE
-class QWheelEvent;
-class QPaintEvent;
-class QFile;
-QT_END_NAMESPACE
-
-class SvgView : public QGraphicsView
-{
- Q_OBJECT
-
-public:
- enum RendererType { Native, OpenGL, Image };
-
- SvgView(QWidget *parent = 0);
-
- void openFile(const QFile &file);
- void setRenderer(RendererType type = Native);
- void drawBackground(QPainter *p, const QRectF &rect);
-
-public slots:
- void setHighQualityAntialiasing(bool highQualityAntialiasing);
- void setViewInteractive(bool enable);
- void setViewBackground(bool enable);
- void setViewOutline(bool enable);
-
-protected:
- void wheelEvent(QWheelEvent *event);
- void paintEvent(QPaintEvent *event);
-
-private:
- RendererType m_renderer;
-
- QString fn;
- QGraphicsItem *m_svgItem;
- QGraphicsWebView *m_webview;
- QGraphicsRectItem *m_backgroundItem;
- QGraphicsRectItem *m_outlineItem;
-
- QImage m_image;
-};
-#endif // SVGVIEW_H
diff --git a/libs/svgviewer/svgviewer.desktop b/libs/svgviewer/svgviewer.desktop
deleted file mode 100644
index 477ef789d..000000000
--- a/libs/svgviewer/svgviewer.desktop
+++ /dev/null
@@ -1,11 +0,0 @@
-[Desktop Entry]
-Encoding=UTF-8
-Version=1.0
-Type=Application
-Terminal=false
-Name=SVG Viewer
-Exec=/opt/usr/bin/svgviewer
-Icon=svgviewer
-X-Window-Icon=
-X-HildonDesk-ShowInToolbar=true
-X-Osso-Type=application/x-executable
diff --git a/libs/svgviewer/svgviewer.pro b/libs/svgviewer/svgviewer.pro
deleted file mode 100644
index 488c62fd5..000000000
--- a/libs/svgviewer/svgviewer.pro
+++ /dev/null
@@ -1,33 +0,0 @@
-HEADERS = mainwindow.h \
- svgview.h
-RESOURCES = svgviewer.qrc
-SOURCES = main.cpp \
- mainwindow.cpp \
- svgview.cpp
-QT += webkit svg xml
-
-contains(QT_CONFIG, opengl): QT += opengl
-
-CONFIG += console
-
-# install
-target.path = $$[QT_INSTALL_EXAMPLES]/painting/svgviewer
-sources.files = $$SOURCES $$HEADERS $$RESOURCES svgviewer.pro files
-sources.path = $$[QT_INSTALL_EXAMPLES]/painting/svgviewer
-INSTALLS += target sources
-
-wince*: {
- addFiles.files = files\\*.svg
- addFiles.path = "\\My Documents"
- DEPLOYMENT += addFiles
-}
-
-symbian: {
- TARGET.UID3 = 0xA000A64E
- include($$QT_SOURCE_TREE/examples/symbianpkgrules.pri)
- addFiles.files = files\\*.svg
- addFiles.path = .
- DEPLOYMENT += addFiles
-}
-maemo5: include($$QT_SOURCE_TREE/examples/maemo5pkgrules.pri)
-
diff --git a/libs/svgviewer/svgviewer.qrc b/libs/svgviewer/svgviewer.qrc
deleted file mode 100644
index db611f51f..000000000
--- a/libs/svgviewer/svgviewer.qrc
+++ /dev/null
@@ -1,6 +0,0 @@
-<!DOCTYPE RCC><RCC version="1.0">
-<qresource prefix="/">
- <file>files/bubbles.svg</file>
-</qresource>
-</RCC>
-