+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef BITARRAY_H
+#define BITARRAY_H
+
+//#define DEBUG_BITARRAY
+
+#include <string.h>
+#include <assert.h>
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class BitArray
+{
+public:
+ BitArray() :
+ size(0)
+ , mp(NULL)
+ {
+ }
+
+ BitArray(const BitArray& b) :
+ size(b.size)
+ {
+ mp = new uint64_t[size];
+ memcpy(mp, b.mp, sizeof(uint64_t)*size);
+ }
+
+ BitArray& operator=(const BitArray& b)
+ {
+ if (size != b.size) {
+ delete[] mp;
+ size = b.size;
+ mp = new uint64_t[size];
+ }
+ memcpy(mp, b.mp, sizeof(uint64_t)*size);
+
+ return *this;
+ }
+
+ BitArray& operator&=(const BitArray& b)
+ {
+ assert(size == b.size);
+ uint64_t* t1 = mp;
+ uint64_t* t2 = b.mp;
+ for (uint64_t i = 0; i < size; i++) {
+ *t1 &= *t2;
+ t1++;
+ t2++;
+ }
+
+ return *this;
+ }
+
+ const bool nothingInCommon(const BitArray& b) const
+ {
+ assert(size == b.size);
+ const uint64_t* t1 = mp;
+ const uint64_t* t2 = b.mp;
+ for (uint64_t i = 0; i < size; i++) {
+ if ((*t1)&(*t2)) return false;
+ t1++;
+ t2++;
+ }
+
+ return true;
+ }
+
+ BitArray& removeThese(const BitArray& b)
+ {
+ assert(size == b.size);
+ uint64_t* t1 = mp;
+ uint64_t* t2 = b.mp;
+ for (uint64_t i = 0; i < size; i++) {
+ *t1 &= ~(*t2);
+ t1++;
+ t2++;
+ }
+
+ return *this;
+ }
+
+ template<class T>
+ BitArray& removeThese(const T& rem)
+ {
+ for (uint32_t i = 0; i < rem.size(); i++) {
+ clearBit(rem[i]);
+ }
+
+ return *this;
+ }
+
+ void resize(uint _size, const bool fill)
+ {
+ _size = _size/64 + (bool)(_size%64);
+ if (size != _size) {
+ delete[] mp;
+ size = _size;
+ mp = new uint64_t[size];
+ }
+ if (fill) setOne();
+ else setZero();
+ }
+
+ ~BitArray()
+ {
+ delete[] mp;
+ }
+
+ inline const bool isZero() const
+ {
+ const uint64_t* mp2 = (const uint64_t*)mp;
+
+ for (uint i = 0; i < size; i++) {
+ if (mp2[i]) return false;
+ }
+ return true;
+ }
+
+ inline void setZero()
+ {
+ memset(mp, 0, size*sizeof(uint64_t));
+ }
+
+ inline void setOne()
+ {
+ memset(mp, 0, size*sizeof(uint64_t));
+ }
+
+ inline void clearBit(const uint i)
+ {
+ #ifdef DEBUG_BITARRAY
+ assert(size*64 > i);
+ #endif
+
+ mp[i/64] &= ~((uint64_t)1 << (i%64));
+ }
+
+ inline void setBit(const uint i)
+ {
+ #ifdef DEBUG_BITARRAY
+ assert(size*64 > i);
+ #endif
+
+ mp[i/64] |= ((uint64_t)1 << (i%64));
+ }
+
+ inline const bool operator[](const uint& i) const
+ {
+ #ifdef DEBUG_BITARRAY
+ assert(size*64 > i);
+ #endif
+
+ return (mp[i/64] >> (i%64)) & 1;
+ }
+
+ inline const uint getSize() const
+ {
+ return size*64;
+ }
+
+private:
+
+ uint size;
+ uint64_t* mp;
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //BITARRAY_H
+
+/*****************************************************************************************[Queue.h]
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+ 2008 - Gilles Audemard, Laurent Simon
+
+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 BoundedQueue_h
+#define BoundedQueue_h
+
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include "Vec.h"
+
+//=================================================================================================
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+template <class T>
+class bqueue {
+ vec<T> elems;
+ int first;
+ int last;
+ uint64_t sumofqueue;
+ int maxsize;
+ int queuesize; // Number of current elements (must be < maxsize !)
+
+public:
+ bqueue(void) : first(0), last(0), sumofqueue(0), maxsize(0), queuesize(0) { }
+
+ void initSize(int size) {growTo(size);} // Init size of bounded size queue
+
+ void push(T x) {
+ if (queuesize==maxsize) {
+ assert(last==first); // The queue is full, next value to enter will replace oldest one
+ sumofqueue -= elems[last];
+ if ((++last) == maxsize) last = 0;
+ } else
+ queuesize++;
+ sumofqueue += x;
+ elems[first] = x;
+ if ((++first) == maxsize) first = 0;
+ }
+
+ T peek() { assert(queuesize>0); return elems[last]; }
+ void pop() {sumofqueue-=elems[last]; queuesize--; if ((++last) == maxsize) last = 0;}
+
+ uint64_t getsum() const {return sumofqueue;}
+ uint32_t getavg() const {return (uint64_t)sumofqueue/(uint64_t)queuesize;}
+ int isvalid() const {return (queuesize==maxsize);}
+
+ void growTo(int size) {
+ elems.growTo(size);
+ first=0; maxsize=size; queuesize = 0;
+ for(int i=0;i<size;i++) elems[i]=0;
+ }
+
+ void fastclear() {first = 0; last = 0; queuesize=0; sumofqueue=0;} // to be called after restarts... Discard the queue
+
+ int size(void) { return queuesize; }
+
+ void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;}
+};
+
+//=================================================================================================
+
+}; //namespace MINISAT
+
+#endif
+/**************************************************************************************************
+From: Solver.C -- (C) Niklas Een, Niklas Sorensson, 2004
+**************************************************************************************************/
+
+#ifndef CSET_H
+#define CSET_H
+
+#include "Vec.h"
+#include <limits>
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class Clause;
+
+template <class T>
+uint32_t calcAbstraction(const T& ps) {
+ uint32_t abstraction = 0;
+ for (uint32_t i = 0; i != ps.size(); i++)
+ abstraction |= 1 << (ps[i].toInt() & 31);
+ return abstraction;
+}
+
+//#pragma pack(push)
+//#pragma pack(1)
+class ClauseSimp
+{
+ public:
+ ClauseSimp(Clause* c, const uint32_t _index) :
+ clause(c)
+ , index(_index)
+ {}
+
+ Clause* clause;
+ uint32_t index;
+};
+//#pragma pack(pop)
+
+class CSet {
+ vec<uint32_t> where; // Map clause ID to position in 'which'.
+ vec<ClauseSimp> which; // List of clauses (for fast iteration). May contain 'Clause_NULL'.
+ vec<uint32_t> free; // List of positions holding 'Clause_NULL'.
+
+ public:
+ //ClauseSimp& operator [] (uint32_t index) { return which[index]; }
+ void reserve(uint32_t size) { where.reserve(size);}
+ uint32_t size(void) const { return which.size(); }
+ uint32_t nElems(void) const { return which.size() - free.size(); }
+
+ bool add(const ClauseSimp& c) {
+ assert(c.clause != NULL);
+ where.growTo(c.index+1, std::numeric_limits<uint32_t>::max());
+ if (where[c.index] != std::numeric_limits<uint32_t>::max()) {
+ return true;
+ }
+ if (free.size() > 0){
+ where[c.index] = free.last();
+ which[free.last()] = c;
+ free.pop();
+ }else{
+ where[c.index] = which.size();
+ which.push(c);
+ }
+ return false;
+ }
+
+ bool exclude(const ClauseSimp& c) {
+ assert(c.clause != NULL);
+ if (c.index >= where.size() || where[c.index] == std::numeric_limits<uint32_t>::max()) {
+ //not inside
+ return false;
+ }
+ free.push(where[c.index]);
+ which[where[c.index]].clause = NULL;
+ where[c.index] = std::numeric_limits<uint32_t>::max();
+ return true;
+ }
+
+ void clear(void) {
+ for (uint32_t i = 0; i < which.size(); i++) {
+ if (which[i].clause != NULL) {
+ where[which[i].index] = std::numeric_limits<uint32_t>::max();
+ }
+ }
+ which.clear();
+ free.clear();
+ }
+
+ class iterator
+ {
+ public:
+ iterator(ClauseSimp* _it) :
+ it(_it)
+ {}
+
+ void operator++()
+ {
+ it++;
+ }
+
+ const bool operator!=(const iterator& iter) const
+ {
+ return (it != iter.it);;
+ }
+
+ ClauseSimp& operator*() {
+ return *it;
+ }
+
+ ClauseSimp*& operator->() {
+ return it;
+ }
+ private:
+ ClauseSimp* it;
+ };
+
+ iterator begin()
+ {
+ return iterator(which.getData());
+ }
+
+ iterator end()
+ {
+ return iterator(which.getData() + which.size());
+ }
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //CSET_H
\ No newline at end of file
+#include "Clause.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+#ifdef USE_POOLS
+#ifdef USE_4POOLS
+boost::pool<> clausePoolQuad(sizeof(Clause) + 5*sizeof(Lit));
+#endif //USE_4POOLS
+boost::pool<> clausePoolTri(sizeof(Clause) + 3*sizeof(Lit));
+boost::pool<> clausePoolBin(sizeof(Clause) + 2*sizeof(Lit));
+#endif //USE_POOLS
+
+}; //NAMESPACE MINISAT
+/***********************************************************************************[SolverTypes.h]
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+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 CLAUSE_H
+#define CLAUSE_H
+
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include "SmallPtr.h"
+#include <stdint.h>
+#endif //_MSC_VER
+#include <cstdio>
+#include <vector>
+#include <sys/types.h>
+#include "Vec.h"
+#include "SolverTypes.h"
+#include "PackedRow.h"
+#include "constants.h"
+#include "SmallPtr.h"
+#ifdef USE_POOLS
+#include "pool.hpp"
+#endif //USE_POOLS
+#ifndef uint
+#define uint unsigned int
+#endif
+
+//#define USE_4POOLS
+
+using std::vector;
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+//=================================================================================================
+// Clause -- a simple class for representing a clause:
+
+class MatrixFinder;
+
+class Clause
+{
+protected:
+
+ #ifdef STATS_NEEDED
+ uint group;
+ #endif
+
+ uint32_t isLearnt:1;
+ uint32_t strenghtened:1;
+ uint32_t varChanged:1;
+ uint32_t sorted:1;
+ uint32_t invertedXor:1;
+ uint32_t isXorClause:1;
+ uint32_t subsume0Done:1;
+ uint32_t isRemoved:1;
+ #ifdef USE_POOLS
+ uint32_t wasTriOriginallyInt:1;
+ uint32_t wasBinOriginallyInt:1;
+ #ifdef USE_4POOLS
+ uint32_t wasQuadOriginallyInt:1;
+ #endif //USE_4POOLS
+ #endif //USE_POOLS
+ uint32_t mySize:20;
+
+ union {uint32_t act; uint32_t abst;} extra;
+ float oldActivityInter;
+ #ifdef _MSC_VER
+ Lit data[1];
+ #else
+ Lit data[0];
+ #endif //_MSC_VER
+
+#ifdef _MSC_VER
+public:
+#endif //_MSC_VER
+ template<class V>
+ Clause(const V& ps, const uint _group, const bool learnt)
+ {
+ isXorClause = false;
+ strenghtened = false;
+ sorted = false;
+ varChanged = true;
+ subsume0Done = false;
+ mySize = ps.size();
+ isLearnt = learnt;
+ isRemoved = false;
+ setGroup(_group);
+ #ifdef USE_POOLS
+ setAllocSize();
+ #endif //USE_POOLS
+
+ for (uint i = 0; i < ps.size(); i++) data[i] = ps[i];
+ if (learnt) {
+ extra.act = 0;
+ oldActivityInter = 0;
+ } else
+ calcAbstraction();
+ }
+
+public:
+ #ifndef _MSC_VER
+ // -- use this function instead:
+ template<class T>
+ friend Clause* Clause_new(const T& ps, const uint group, const bool learnt = false);
+ friend Clause* Clause_new(Clause& c);
+ #endif //_MSC_VER
+
+ const uint size () const {
+ return mySize;
+ }
+ void resize (const uint size) {
+ mySize = size;
+ }
+ void shrink (const uint i) {
+ assert(i <= size());
+ mySize -= i;
+ }
+ void pop () {
+ shrink(1);
+ }
+ const bool isXor () {
+ return isXorClause;
+ }
+ const bool learnt () const {
+ return isLearnt;
+ }
+ float& oldActivity () {
+ return oldActivityInter;
+ }
+
+ const float& oldActivity () const {
+ return oldActivityInter;
+ }
+
+
+ const bool getStrenghtened() const {
+ return strenghtened;
+ }
+ void setStrenghtened() {
+ strenghtened = true;
+ sorted = false;
+ subsume0Done = false;
+ }
+ void unsetStrenghtened() {
+ strenghtened = false;
+ }
+ const bool getVarChanged() const {
+ return varChanged;
+ }
+ void setVarChanged() {
+ varChanged = true;
+ sorted = false;
+ subsume0Done = false;
+ }
+ void unsetVarChanged() {
+ varChanged = false;
+ }
+ const bool getSorted() const {
+ return sorted;
+ }
+ void setSorted() {
+ sorted = true;
+ }
+ void setUnsorted() {
+ sorted = false;
+ }
+ void subsume0Finished() {
+ subsume0Done = 1;
+ }
+ const bool subsume0IsFinished() {
+ return subsume0Done;
+ }
+
+ Lit& operator [] (uint32_t i) {
+ return data[i];
+ }
+ const Lit& operator [] (uint32_t i) const {
+ return data[i];
+ }
+
+ void setActivity(uint32_t i) {
+ extra.act = i;
+ }
+
+ const uint32_t& activity () const {
+ return extra.act;
+ }
+
+ void makeNonLearnt() {
+ assert(isLearnt);
+ isLearnt = false;
+ calcAbstraction();
+ }
+
+ void makeLearnt(const uint32_t newActivity) {
+ extra.act = newActivity;
+ oldActivityInter = 0;
+ isLearnt = true;
+ }
+
+ inline void strengthen(const Lit p)
+ {
+ remove(*this, p);
+ sorted = false;
+ calcAbstraction();
+ }
+
+ void calcAbstraction() {
+ assert(!learnt());
+ extra.abst = 0;
+ for (uint32_t i = 0; i != size(); i++)
+ extra.abst |= 1 << (data[i].toInt() & 31);
+ }
+
+ uint32_t getAbst()
+ {
+ return extra.abst;
+ }
+
+ const Lit* getData () const {
+ return data;
+ }
+ Lit* getData () {
+ return data;
+ }
+ const Lit* getDataEnd () const {
+ return data+size();
+ }
+ Lit* getDataEnd () {
+ return data+size();
+ }
+ void print(FILE* to = stdout) {
+ plainPrint(to);
+ fprintf(to, "c clause learnt %s group %d act %d oldAct %f\n", (learnt() ? "yes" : "no"), getGroup(), activity(), oldActivity());
+ }
+ void plainPrint(FILE* to = stdout) const {
+ for (uint i = 0; i < size(); i++) {
+ if (data[i].sign()) fprintf(to, "-");
+ fprintf(to, "%d ", data[i].var() + 1);
+ }
+ fprintf(to, "0\n");
+ }
+ #ifdef STATS_NEEDED
+ const uint32_t getGroup() const
+ {
+ return group;
+ }
+ void setGroup(const uint32_t _group)
+ {
+ group = _group;
+ }
+ #else
+ const uint getGroup() const
+ {
+ return 0;
+ }
+ void setGroup(const uint32_t _group)
+ {
+ return;
+ }
+ #endif //STATS_NEEDED
+ void setRemoved() {
+ isRemoved = true;
+ }
+
+ const bool removed() const {
+ return isRemoved;
+ }
+ #ifdef USE_POOLS
+ const bool wasTriOriginally() const
+ {
+ return wasTriOriginallyInt;
+ }
+ const bool wasBinOriginally() const
+ {
+ return wasBinOriginallyInt;
+ }
+ #ifdef USE_4POOLS
+ const bool wasQuadOriginally() const
+ {
+ return wasQuadOriginallyInt;
+ }
+ #endif //USE_4POOLS
+ void setAllocSize()
+ {
+ wasTriOriginallyInt = false;
+ wasBinOriginallyInt = false;
+ #ifdef USE_4POOLS
+ wasQuadOriginallyInt = false;
+ #endif //USE_4POOLS
+ switch(size()) {
+ case 2:
+ wasBinOriginallyInt = true;
+ break;
+ case 3:
+ wasTriOriginallyInt = true;
+ break;
+ #ifdef USE_4POOLS
+ case 4:
+ wasQuadOriginallyInt = true;
+ break;
+ case 5:
+ wasQuadOriginallyInt = true;
+ break;
+ #endif //USE_4POOLS
+ }
+ }
+ #endif //USE_POOLS
+};
+
+class XorClause : public Clause
+{
+
+#ifdef _MSC_VER
+public:
+#else //_MSC_VER
+protected:
+#endif //_MSC_VER
+
+ // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+ template<class V>
+ XorClause(const V& ps, const bool inverted, const uint _group) :
+ Clause(ps, _group, false)
+ {
+ invertedXor = inverted;
+ isXorClause = true;
+ calcXorAbstraction();
+ }
+
+public:
+ #ifndef _MSC_VER
+ // -- use this function instead:
+ template<class V>
+ friend XorClause* XorClause_new(const V& ps, const bool inverted, const uint group);
+ #endif //_MSC_VER
+
+ inline bool xor_clause_inverted() const
+ {
+ return invertedXor;
+ }
+ inline void invert(bool b)
+ {
+ invertedXor ^= b;
+ }
+ void calcXorAbstraction() {
+ extra.abst = 0;
+ for (uint32_t i = 0; i != size(); i++)
+ extra.abst |= 1 << (data[i].var() & 31);
+ }
+
+ void print() {
+ printf("XOR Clause group: %d, size: %d, learnt:%d, lits:\"", getGroup(), size(), learnt());
+ plainPrint();
+ }
+
+ void plainPrint(FILE* to = stdout) const {
+ fprintf(to, "x");
+ if (xor_clause_inverted())
+ printf("-");
+ for (uint i = 0; i < size(); i++) {
+ fprintf(to, "%d ", data[i].var() + 1);
+ }
+ fprintf(to, "0\n");
+ }
+
+ friend class MatrixFinder;
+};
+
+#ifdef USE_POOLS
+extern boost::pool<> clausePoolTri;
+extern boost::pool<> clausePoolBin;
+#ifdef USE_4POOLS
+extern boost::pool<> clausePoolQuad;
+#endif //USE_4POOLS
+#endif //USE_POOLS
+
+template<class T>
+inline void* allocEnough(const T& ps)
+{
+ void* mem;
+ switch(ps.size()) {
+ #ifdef USE_POOLS
+ case 2:
+ mem = clausePoolBin.malloc();
+ break;
+ case 3:
+ mem = clausePoolTri.malloc();
+ break;
+ #ifdef USE_4POOLS
+ case 4:
+ mem = clausePoolQuad.malloc();
+ break;
+ case 5:
+ mem = clausePoolQuad.malloc();
+ break;
+ #endif //USE_4POOLS
+ #endif //USE_POOLS
+ default:
+ mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size()));
+ break;
+ }
+
+ return mem;
+}
+
+template<class T>
+Clause* Clause_new(const T& ps, const uint group, const bool learnt = false)
+{
+ void* mem = allocEnough(ps);
+ Clause* real= new (mem) Clause(ps, group, learnt);
+ return real;
+}
+
+template<class T>
+XorClause* XorClause_new(const T& ps, const bool inverted, const uint group)
+{
+ void* mem = allocEnough(ps);
+ XorClause* real= new (mem) XorClause(ps, inverted, group);
+ return real;
+}
+
+inline Clause* Clause_new(Clause& c)
+{
+ void* mem = allocEnough(c);
+ //Clause* real= new (mem) Clause(ps, group, learnt);
+ memcpy(mem, &c, sizeof(Clause)+sizeof(Lit)*c.size());
+ Clause& c2 = *(Clause*)mem;
+ #ifdef USE_POOLS
+ c2.setAllocSize();
+ #endif //USE_POOLS
+
+ return &c2;
+}
+
+inline void clauseFree(Clause* c)
+{
+ #ifdef USE_POOLS
+ if (c->wasTriOriginally())
+ clausePoolTri.free(c);
+ else if (c->wasBinOriginally())
+ clausePoolBin.free(c);
+ #ifdef USE_4POOLS
+ else if (c->wasQuadOriginally())
+ clausePoolQuad.free(c);
+ #endif //USE_4POOLS
+ else
+ #endif //USE_POOLS
+ free(c);
+}
+
+#ifdef _MSC_VER
+typedef Clause* ClausePtr;
+typedef XorClause* XorClausePtr;
+#else
+typedef sptr<Clause> ClausePtr;
+typedef sptr<XorClause> XorClausePtr;
+#endif //_MSC_VER
+
+#pragma pack(push)
+#pragma pack(1)
+class WatchedBin {
+ public:
+ WatchedBin(Clause *_clause, Lit _impliedLit) : clause(_clause), impliedLit(_impliedLit) {};
+ ClausePtr clause;
+ Lit impliedLit;
+};
+
+class Watched {
+ public:
+ Watched(Clause *_clause, Lit _blockedLit) : clause(_clause), blockedLit(_blockedLit) {};
+ ClausePtr clause;
+ Lit blockedLit;
+};
+#pragma pack(pop)
+
+}; //NAMESPACE MINISAT
+
+#endif //CLAUSE_H
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#include "ClauseCleaner.h"
+#include "VarReplacer.h"
+
+#ifdef _MSC_VER
+#define __builtin_prefetch(a,b,c)
+#endif //_MSC_VER
+
+//#define DEBUG_CLEAN
+//#define VERBOSE_DEBUG
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+ClauseCleaner::ClauseCleaner(Solver& _solver) :
+ solver(_solver)
+{
+ for (uint i = 0; i < 6; i++) {
+ lastNumUnitarySat[i] = solver.get_unitary_learnts_num();
+ lastNumUnitaryClean[i] = solver.get_unitary_learnts_num();
+ }
+}
+
+void ClauseCleaner::removeSatisfied(vec<XorClause*>& cs, ClauseSetType type, const uint limit)
+{
+ #ifdef DEBUG_CLEAN
+ assert(solver.decisionLevel() == 0);
+ #endif
+
+ if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ uint32_t i,j;
+ for (i = j = 0; i < cs.size(); i++) {
+ if (satisfied(*cs[i]))
+ solver.removeClause(*cs[i]);
+ else
+ cs[j++] = cs[i];
+ }
+ cs.shrink(i - j);
+
+ lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
+}
+
+void ClauseCleaner::removeSatisfied(vec<Clause*>& cs, ClauseSetType type, const uint limit)
+{
+ #ifdef DEBUG_CLEAN
+ assert(solver.decisionLevel() == 0);
+ #endif
+
+ if (lastNumUnitarySat[type] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ Clause **i,**j, **end;
+ for (i = j = cs.getData(), end = i + cs.size(); i != end; i++) {
+ if (i+1 != end)
+ __builtin_prefetch(*(i+1), 0, 0);
+ if (satisfied(**i))
+ solver.removeClause(**i);
+ else
+ *j++ = *i;
+ }
+ cs.shrink(i - j);
+
+ lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
+}
+
+void ClauseCleaner::cleanClauses(vec<Clause*>& cs, ClauseSetType type, const uint limit)
+{
+ assert(solver.decisionLevel() == 0);
+ assert(solver.qhead == solver.trail.size());
+
+ if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Cleaning " << (type==binaryClauses ? "binaryClauses" : "normal clauses" ) << std::endl;
+ #endif //VERBOSE_DEBUG
+
+ Clause **s, **ss, **end;
+ for (s = ss = cs.getData(), end = s + cs.size(); s != end;) {
+ if (s+1 != end)
+ __builtin_prefetch(*(s+1), 1, 0);
+ if (cleanClause(*s)) {
+ clauseFree(*s);
+ s++;
+ } else if (type != ClauseCleaner::binaryClauses && (*s)->size() == 2) {
+ solver.binaryClauses.push(*s);
+ solver.becameBinary++;
+ s++;
+ } else {
+ *ss++ = *s++;
+ }
+ }
+ cs.shrink(s-ss);
+
+ lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
+
+ #ifdef VERBOSE_DEBUG
+ cout << "cleanClauses(Clause) useful ?? Removed: " << s-ss << endl;
+ #endif
+}
+
+inline const bool ClauseCleaner::cleanClause(Clause*& cc)
+{
+ Clause& c = *cc;
+
+ Lit origLit1 = c[0];
+ Lit origLit2 = c[1];
+ uint32_t origSize = c.size();
+
+ Lit *i, *j, *end;
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++) {
+ lbool val = solver.value(*i);
+ if (val == l_Undef) {
+ *j++ = *i;
+ continue;
+ }
+
+ if (val == l_True) {
+ solver.detachModifiedClause(origLit1, origLit2, origSize, &c);
+ return true;
+ }
+ }
+ c.shrink(i-j);
+
+ if (i != j) {
+ c.setStrenghtened();
+ if (c.size() == 2) {
+ solver.detachModifiedClause(origLit1, origLit2, origSize, &c);
+ Clause *c2 = Clause_new(c);
+ clauseFree(&c);
+ cc = c2;
+ solver.attachClause(*c2);
+ /*} else if (c.size() == 3) {
+ solver.detachModifiedClause(origLit1, origLit2, origSize, &c);
+ Clause *c2 = Clause_new(c);
+ clauseFree(&c);
+ cc = c2;
+ solver.attachClause(*c2);*/
+ } else {
+ if (c.learnt())
+ solver.learnts_literals -= i-j;
+ else
+ solver.clauses_literals -= i-j;
+ }
+ }
+
+ return false;
+}
+
+void ClauseCleaner::cleanClauses(vec<XorClause*>& cs, ClauseSetType type, const uint limit)
+{
+ assert(solver.decisionLevel() == 0);
+ assert(solver.qhead == solver.trail.size());
+
+ if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ XorClause **s, **ss, **end;
+ for (s = ss = cs.getData(), end = s + cs.size(); s != end; s++) {
+ if (s+1 != end)
+ __builtin_prefetch(*(s+1), 1, 0);
+
+ #ifdef DEBUG_ATTACH
+ assert(find(solver.xorwatches[(**s)[0].var()], *s));
+ assert(find(solver.xorwatches[(**s)[1].var()], *s));
+ if (solver.assigns[(**s)[0].var()]!=l_Undef || solver.assigns[(**s)[1].var()]!=l_Undef) {
+ satisfied(**s);
+ }
+ #endif //DEBUG_ATTACH
+
+ if (cleanClause(**s)) {
+ solver.freeLater.push(*s);
+ (*s)->setRemoved();
+ } else {
+ #ifdef DEBUG_ATTACH
+ assert(find(solver.xorwatches[(**s)[0].var()], *s));
+ assert(find(solver.xorwatches[(**s)[1].var()], *s));
+ #endif //DEBUG_ATTACH
+ *ss++ = *s;
+ }
+ }
+ cs.shrink(s-ss);
+
+ lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
+
+ #ifdef VERBOSE_DEBUG
+ cout << "cleanClauses(XorClause) useful: ?? Removed: " << s-ss << endl;
+ #endif
+}
+
+inline const bool ClauseCleaner::cleanClause(XorClause& c)
+{
+ Lit *i, *j, *end;
+ Var origVar1 = c[0].var();
+ Var origVar2 = c[1].var();
+ uint32_t origSize = c.size();
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++) {
+ const lbool& val = solver.assigns[i->var()];
+ if (val.isUndef()) {
+ *j = *i;
+ j++;
+ } else c.invert(val.getBool());
+ }
+ c.shrink(i-j);
+
+ assert(c.size() != 1);
+ switch (c.size()) {
+ case 0: {
+ solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
+ return true;
+ }
+ case 2: {
+ c[0] = c[0].unsign();
+ c[1] = c[1].unsign();
+ solver.varReplacer->replace(c, c.xor_clause_inverted(), c.getGroup());
+ solver.detachModifiedClause(origVar1, origVar2, origSize, &c);
+ return true;
+ }
+ default: {
+ if (i-j > 0) {
+ c.setStrenghtened();
+ solver.clauses_literals -= i-j;
+ }
+ return false;
+ }
+ }
+
+ assert(false);
+ return false;
+}
+
+void ClauseCleaner::cleanClausesBewareNULL(vec<ClauseSimp>& cs, ClauseCleaner::ClauseSetType type, Subsumer& subs, const uint limit)
+{
+ assert(solver.decisionLevel() == 0);
+ assert(solver.qhead == solver.trail.size());
+
+ if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ ClauseSimp *s, *end;
+ for (s = cs.getData(), end = s + cs.size(); s != end; s++) {
+ if (s+1 != end)
+ __builtin_prefetch((s+1)->clause, 1, 0);
+ if (s->clause == NULL)
+ continue;
+
+ if (cleanClauseBewareNULL(*s, subs)) {
+ continue;
+ } else if (s->clause->size() == 2)
+ solver.becameBinary++;
+ }
+
+ lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
+}
+
+inline const bool ClauseCleaner::cleanClauseBewareNULL(ClauseSimp cc, Subsumer& subs)
+{
+ Clause& c = *cc.clause;
+ vec<Lit> origClause(c.size());
+ memcpy(origClause.getData(), c.getData(), sizeof(Lit)*c.size());
+
+ Lit *i, *j, *end;
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++) {
+ lbool val = solver.value(*i);
+ if (val == l_Undef) {
+ *j++ = *i;
+ continue;
+ }
+
+ if (val == l_True) {
+ subs.unlinkModifiedClause(origClause, cc);
+ clauseFree(cc.clause);
+ return true;
+ }
+ }
+
+ if (i != j) {
+ c.setStrenghtened();
+ if (origClause.size() > 2 && origClause.size()-(i-j) == 2) {
+ subs.unlinkModifiedClause(origClause, cc);
+ subs.clauses[cc.index] = cc;
+ c.shrink(i-j);
+ solver.attachClause(c);
+ subs.linkInAlreadyClause(cc);
+ } else {
+ c.shrink(i-j);
+ subs.unlinkModifiedClauseNoDetachNoNULL(origClause, cc);
+ subs.linkInAlreadyClause(cc);
+ if (c.learnt())
+ solver.learnts_literals -= i-j;
+ else
+ solver.clauses_literals -= i-j;
+ }
+ c.calcAbstraction();
+ subs.updateClause(cc);
+ }
+
+ return false;
+}
+
+void ClauseCleaner::cleanXorClausesBewareNULL(vec<XorClauseSimp>& cs, ClauseCleaner::ClauseSetType type, XorSubsumer& subs, const uint limit)
+{
+ assert(solver.decisionLevel() == 0);
+ assert(solver.qhead == solver.trail.size());
+
+ if (lastNumUnitaryClean[type] + limit >= solver.get_unitary_learnts_num())
+ return;
+
+ XorClauseSimp *s, *end;
+ for (s = cs.getData(), end = s + cs.size(); s != end; s++) {
+ if (s+1 != end)
+ __builtin_prefetch((s+1)->clause, 1, 0);
+ if (s->clause == NULL)
+ continue;
+
+ cleanXorClauseBewareNULL(*s, subs);
+ }
+
+ lastNumUnitaryClean[type] = solver.get_unitary_learnts_num();
+}
+
+inline const bool ClauseCleaner::cleanXorClauseBewareNULL(XorClauseSimp cc, XorSubsumer& subs)
+{
+ XorClause& c = *cc.clause;
+ vec<Lit> origClause(c.size());
+ memcpy(origClause.getData(), c.getData(), sizeof(Lit)*c.size());
+
+ Lit *i, *j, *end;
+ for (i = j = c.getData(), end = i + c.size(); i != end; i++) {
+ const lbool& val = solver.assigns[i->var()];
+ if (val.isUndef()) {
+ *j = *i;
+ j++;
+ } else c.invert(val.getBool());
+ }
+ c.shrink(i-j);
+
+ switch(c.size()) {
+ case 0: {
+ subs.unlinkModifiedClause(origClause, cc);
+ clauseFree(cc.clause);
+ return true;
+ }
+ case 2: {
+ vec<Lit> ps(2);
+ ps[0] = c[0].unsign();
+ ps[1] = c[1].unsign();
+ solver.varReplacer->replace(ps, c.xor_clause_inverted(), c.getGroup());
+ subs.unlinkModifiedClause(origClause, cc);
+ clauseFree(cc.clause);
+ return true;
+ }
+ default:
+ if (i-j > 0) {
+ subs.unlinkModifiedClauseNoDetachNoNULL(origClause, cc);
+ subs.linkInAlreadyClause(cc);
+ c.calcXorAbstraction();
+ }
+ }
+
+ return false;
+}
+
+bool ClauseCleaner::satisfied(const Clause& c) const
+{
+ for (uint i = 0; i != c.size(); i++)
+ if (solver.value(c[i]) == l_True)
+ return true;
+ return false;
+}
+
+bool ClauseCleaner::satisfied(const XorClause& c) const
+{
+ bool final = c.xor_clause_inverted();
+ for (uint k = 0; k != c.size(); k++ ) {
+ const lbool& val = solver.assigns[c[k].var()];
+ if (val.isUndef()) return false;
+ final ^= val.getBool();
+ }
+ return final;
+}
+
+void ClauseCleaner::moveBinClausesToBinClauses()
+{
+ assert(solver.decisionLevel() == 0);
+ assert(solver.qhead == solver.trail.size());
+
+ vec<Clause*>& cs = solver.clauses;
+ Clause **s, **ss, **end;
+ for (s = ss = cs.getData(), end = s + cs.size(); s != end; s++) {
+ if (s+1 != end)
+ __builtin_prefetch(*(s+1), 1, 0);
+
+ if ((**s).size() == 2)
+ solver.binaryClauses.push(*s);
+ else
+ *ss++ = *s;
+ }
+ cs.shrink(s-ss);
+}
+
+}; //NAMESPACE MINISAT
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef CLAUSECLEANER_H
+#define CLAUSECLEANER_H
+
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include "Solver.h"
+#include "Subsumer.h"
+#include "XorSubsumer.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class ClauseCleaner
+{
+ public:
+ ClauseCleaner(Solver& solver);
+
+ enum ClauseSetType {clauses, xorclauses, learnts, binaryClauses, simpClauses, xorSimpClauses};
+
+ void cleanClauses(vec<Clause*>& cs, ClauseSetType type, const uint limit = 0);
+ void cleanClausesBewareNULL(vec<ClauseSimp>& cs, ClauseSetType type, Subsumer& subs, const uint limit = 0);
+ void cleanXorClausesBewareNULL(vec<XorClauseSimp>& cs, ClauseSetType type, XorSubsumer& subs, const uint limit = 0);
+ const bool cleanClauseBewareNULL(ClauseSimp c, Subsumer& subs);
+ const bool cleanXorClauseBewareNULL(XorClauseSimp c, XorSubsumer& subs);
+
+ void cleanClauses(vec<XorClause*>& cs, ClauseSetType type, const uint limit = 0);
+ void removeSatisfied(vec<Clause*>& cs, ClauseSetType type, const uint limit = 0);
+ void removeSatisfied(vec<XorClause*>& cs, ClauseSetType type, const uint limit = 0);
+ void removeAndCleanAll(const bool nolimit = false);
+ bool satisfied(const Clause& c) const;
+ bool satisfied(const XorClause& c) const;
+
+ void moveBinClausesToBinClauses();
+
+ private:
+ const bool cleanClause(XorClause& c);
+ const bool cleanClause(Clause*& c);
+
+ uint lastNumUnitarySat[6];
+ uint lastNumUnitaryClean[6];
+
+ Solver& solver;
+};
+
+inline void ClauseCleaner::removeAndCleanAll(const bool nolimit)
+{
+ //uint limit = std::min((uint)((double)solver.order_heap.size() * PERCENTAGECLEANCLAUSES), FIXCLEANREPLACE);
+ uint limit = (double)solver.order_heap.size() * PERCENTAGECLEANCLAUSES;
+ if (nolimit) limit = 0;
+
+ removeSatisfied(solver.binaryClauses, ClauseCleaner::binaryClauses, limit);
+ cleanClauses(solver.clauses, ClauseCleaner::clauses, limit);
+ cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses, limit);
+ cleanClauses(solver.learnts, ClauseCleaner::learnts, limit);
+}
+
+}; //NAMESPACE MINISAT
+
+#endif //CLAUSECLEANER_H
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#include "Conglomerate.h"
+#include "VarReplacer.h"
+#include "ClauseCleaner.h"
+
+#include <utility>
+#include <algorithm>
+#include <cstring>
+#include "time_mem.h"
+#include <iomanip>
+using std::make_pair;
+
+//#define VERBOSE_DEBUG
+
+#ifdef VERBOSE_DEBUG
+#include <iostream>
+using std::cout;
+using std::endl;
+#endif
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+Conglomerate::Conglomerate(Solver& _solver) :
+ found(0)
+ , solver(_solver)
+{}
+
+Conglomerate::~Conglomerate()
+{
+ for(uint i = 0; i < calcAtFinish.size(); i++)
+ free(calcAtFinish[i]);
+}
+
+void Conglomerate::blockVars()
+{
+ for (Clause *const*it = solver.clauses.getData(), *const*end = it + solver.clauses.size(); it != end; it++) {
+ const Clause& c = **it;
+ for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) {
+ blocked[a->var()] = true;
+ }
+ }
+
+ for (Clause *const*it = solver.binaryClauses.getData(), *const*end = it + solver.binaryClauses.size(); it != end; it++) {
+ const Clause& c = **it;
+ blocked[c[0].var()] = true;
+ blocked[c[1].var()] = true;
+ }
+
+ for (Lit* it = &(solver.trail[0]), *end = it + solver.trail.size(); it != end; it++)
+ blocked[it->var()] = true;
+
+ const vec<Clause*>& clauses = solver.varReplacer->getClauses();
+ for (Clause *const*it = clauses.getData(), *const*end = it + clauses.size(); it != end; it++) {
+ const Clause& c = **it;
+ for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) {
+ blocked[a->var()] = true;
+ }
+ }
+}
+
+void Conglomerate::fillVarToXor()
+{
+ varToXor.clear();
+
+ uint i = 0;
+ for (XorClause* const* it = solver.xorclauses.getData(), *const*end = it + solver.xorclauses.size(); it != end; it++, i++) {
+ const XorClause& c = **it;
+ for (const Lit * a = &c[0], *end = a + c.size(); a != end; a++) {
+ if (!blocked[a->var()])
+ varToXor[a->var()].push_back(make_pair(*it, i));
+ }
+ }
+}
+
+void Conglomerate::removeVar(const Var var)
+{
+ solver.activity[var] = 0.0;
+ solver.order_heap.update(var);
+ removedVars[var] = true;
+ if (solver.decision_var[var]) {
+ madeVarNonDecision.push(var);
+ solver.setDecisionVar(var, false);
+ }
+ found++;
+}
+
+void Conglomerate::processClause(XorClause& x, uint32_t num, Var remove_var)
+{
+ for (const Lit* a = &x[0], *end = a + x.size(); a != end; a++) {
+ Var var = a->var();
+ if (var != remove_var) {
+ varToXorMap::iterator finder = varToXor.find(var);
+ if (finder != varToXor.end()) {
+ vector<pair<XorClause*, uint32_t> >::iterator it =
+ std::find(finder->second.begin(), finder->second.end(), make_pair(&x, num));
+ finder->second.erase(it);
+ }
+ }
+ }
+}
+
+const bool Conglomerate::heuleProcessFull()
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "Heule XOR-ing started" << endl;
+ #endif
+
+ double time = cpuTime();
+ found = 0;
+ uint oldToReplaceVars = solver.varReplacer->getNewToReplaceVars();
+ solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
+ if (solver.ok == false)
+ return false;
+
+ toRemove.clear();
+ toRemove.resize(solver.xorclauses.size(), false);
+ blocked.clear();
+ blocked.resize(solver.nVars(), false);
+ fillVarToXor();
+ if (!heuleProcess())
+ goto end;
+
+ if (solver.verbosity >=1) {
+ std::cout << "c | Heule-processings XORs:" << std::setw(8) << std::setprecision(2) << std::fixed << cpuTime()-time
+ << " Found smaller XOR-s: " << std::setw(6) << found
+ << " New bin anti/eq-s: " << std::setw(3) << solver.varReplacer->getNewToReplaceVars() - oldToReplaceVars
+ << std::setw(0) << " |" << std::endl;
+ }
+
+end:
+
+ clearToRemove();
+
+ return solver.ok;
+}
+
+const bool Conglomerate::conglomerateXorsFull()
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "Finding conglomerate xors started" << endl;
+ #endif
+
+ double time = cpuTime();
+ found = 0;
+ uint32_t origNumClauses = solver.xorclauses.size();
+
+ solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
+ if (solver.ok == false)
+ return false;
+
+ toRemove.clear();
+ toRemove.resize(solver.xorclauses.size(), false);
+ blocked.clear();
+ blocked.resize(solver.nVars(), false);
+ blockVars();
+ fillVarToXor();
+ if (conglomerateXors() == false)
+ goto end;
+
+end:
+
+ clearToRemove();
+ assert(origNumClauses >= solver.xorclauses.size());
+ if (solver.verbosity >=1) {
+ std::cout << "c | Conglomerating XORs:" << std::setw(8) << std::setprecision(2) << std::fixed << cpuTime()-time << " s "
+ << " removed " << std::setw(8) << found << " vars"
+ << " removed " << std::setw(8) << origNumClauses-solver.xorclauses.size() << " clauses"
+ << std::setw(0) << " |" << std::endl;
+ }
+
+ clearLearntsFromToRemove();
+ solver.order_heap.filter(Solver::VarFilter(solver));
+
+ return solver.ok;
+}
+
+void Conglomerate::fillNewSet(vector<vector<Lit> >& newSet, vector<pair<XorClause*, uint32_t> >& clauseSet) const
+{
+ newSet.clear();
+ newSet.resize(clauseSet.size());
+
+ XorClause& firstXorClause = *(clauseSet[0].first);
+ newSet[0].resize(firstXorClause.size());
+ memcpy(&newSet[0][0], firstXorClause.getData(), sizeof(Lit)*firstXorClause.size());
+
+ for (uint i = 1; i < clauseSet.size(); i++) {
+ XorClause& thisXorClause = *clauseSet[i].first;
+ newSet[i] = newSet[0];
+ newSet[i].resize(firstXorClause.size()+thisXorClause.size());
+ memcpy(&newSet[i][firstXorClause.size()], thisXorClause.getData(), sizeof(Lit)*thisXorClause.size());
+ clearDouble(newSet[i]);
+ }
+}
+
+const bool Conglomerate::heuleProcess()
+{
+ vector<vector<Lit> > newSet;
+ while(varToXor.begin() != varToXor.end()) {
+ varToXorMap::iterator it = varToXor.begin();
+ vector<pair<XorClause*, uint32_t> >& clauseSet = it->second;
+ const Var var = it->first;
+
+ if (blocked[var] || clauseSet.size() == 1) {
+ varToXor.erase(it);
+ blocked[var] = true;
+ continue;
+ }
+ blocked[var] = true;
+
+ std::sort(clauseSet.begin(), clauseSet.end(), ClauseSetSorter());
+ fillNewSet(newSet, clauseSet);
+
+ for (uint i = 1; i < newSet.size(); i++) if (newSet[i].size() <= 2) {
+ found++;
+ XorClause& thisXorClause = *clauseSet[i].first;
+ const bool inverted = !clauseSet[0].first->xor_clause_inverted() ^ thisXorClause.xor_clause_inverted();
+ const uint old_group = thisXorClause.getGroup();
+
+ #ifdef VERBOSE_DEBUG
+ cout << "- XOR1:";
+ clauseSet[0].first->plainPrint();
+ cout << "- XOR2:";
+ thisXorClause.plainPrint();
+ #endif
+
+ if (!dealWithNewClause(newSet[i], inverted, old_group))
+ return false;
+ assert(newSet.size() == clauseSet.size());
+ }
+
+ varToXor.erase(it);
+ }
+
+ return (solver.ok = (solver.propagate() == NULL));
+}
+
+const bool Conglomerate::conglomerateXors()
+{
+ vector<vector<Lit> > newSet;
+ while(varToXor.begin() != varToXor.end()) {
+ varToXorMap::iterator it = varToXor.begin();
+ vector<pair<XorClause*, uint32_t> >& clauseSet = it->second;
+ const Var var = it->first;
+
+ //We blocked the var during dealWithNewClause (it was in a 2-long xor-clause)
+ if (blocked[var]) {
+ varToXor.erase(it);
+ continue;
+ }
+
+ if (clauseSet.size() == 0) {
+ removeVar(var);
+ varToXor.erase(it);
+ continue;
+ }
+
+ std::sort(clauseSet.begin(), clauseSet.end(), ClauseSetSorter());
+ fillNewSet(newSet, clauseSet);
+
+ int diff = 0;
+ for (size_t i = 1; i < newSet.size(); i++)
+ diff += (int)newSet[i].size()-(int)clauseSet[i].first->size();
+
+ if (newSet.size() > 2) {
+ blocked[var] = true;
+ varToXor.erase(it);
+ continue;
+ }
+
+ XorClause& firstXorClause = *(clauseSet[0].first);
+ bool first_inverted = !firstXorClause.xor_clause_inverted();
+ removeVar(var);
+
+ #ifdef VERBOSE_DEBUG
+ cout << "--- New conglomerate set ---" << endl;
+ cout << "- Removing: ";
+ firstXorClause.plainPrint();
+ cout << "Adding var " << var+1 << " to calcAtFinish" << endl;
+ #endif
+
+ assert(!toRemove[clauseSet[0].second]);
+ toRemove[clauseSet[0].second] = true;
+ processClause(firstXorClause, clauseSet[0].second, var);
+ solver.detachClause(firstXorClause);
+ calcAtFinish.push(&firstXorClause);
+
+ for (uint i = 1; i < clauseSet.size(); i++) {
+ XorClause& thisXorClause = *clauseSet[i].first;
+ #ifdef VERBOSE_DEBUG
+ cout << "- Removing: ";
+ thisXorClause.plainPrint();
+ #endif
+
+ const uint old_group = thisXorClause.getGroup();
+ const bool inverted = first_inverted ^ thisXorClause.xor_clause_inverted();
+ assert(!toRemove[clauseSet[i].second]);
+ toRemove[clauseSet[i].second] = true;
+ processClause(thisXorClause, clauseSet[i].second, var);
+ solver.removeClause(thisXorClause);
+
+ if (!dealWithNewClause(newSet[i], inverted, old_group))
+ return false;
+ assert(newSet.size() == clauseSet.size());
+ }
+
+ varToXor.erase(it);
+ }
+
+ return (solver.ok = (solver.propagate() == NULL));
+}
+
+bool Conglomerate::dealWithNewClause(vector<Lit>& ps, const bool inverted, const uint old_group)
+{
+ switch(ps.size()) {
+ case 0: {
+ #ifdef VERBOSE_DEBUG
+ cout << "--> xor is 0-long" << endl;
+ #endif
+
+ if (!inverted) {
+ solver.ok = false;
+ return false;
+ }
+ break;
+ }
+ case 1: {
+ #ifdef VERBOSE_DEBUG
+ cout << "--> xor is 1-long, attempting to set variable " << ps[0].var()+1 << endl;
+ #endif
+
+ if (solver.assigns[ps[0].var()] == l_Undef) {
+ assert(solver.decisionLevel() == 0);
+ blocked[ps[0].var()] = true;
+ solver.uncheckedEnqueue(Lit(ps[0].var(), inverted));
+ } else if (solver.assigns[ps[0].var()] != boolToLBool(!inverted)) {
+ #ifdef VERBOSE_DEBUG
+ cout << "Conflict. Aborting.";
+ #endif
+ solver.ok = false;
+ return false;
+ } else {
+ #ifdef VERBOSE_DEBUG
+ cout << "Variable already set to correct value";
+ #endif
+ }
+ break;
+ }
+
+ case 2: {
+ #ifdef VERBOSE_DEBUG
+ cout << "--> xor is 2-long, must later replace variable" << endl;
+ XorClause* newX = XorClause_new(ps, inverted, old_group);
+ newX->plainPrint();
+ free(newX);
+ #endif
+
+ vec<Lit> tmpPS(2);
+ tmpPS[0] = ps[0];
+ tmpPS[1] = ps[1];
+ if (solver.varReplacer->replace(tmpPS, inverted, old_group) == false)
+ return false;
+ blocked[ps[0].var()] = true;
+ blocked[ps[1].var()] = true;
+ break;
+ }
+
+ default: {
+ XorClause* newX = XorClause_new(ps, inverted, old_group);
+
+ #ifdef VERBOSE_DEBUG
+ cout << "- Adding: ";
+ newX->plainPrint();
+ #endif
+
+ solver.xorclauses.push(newX);
+ toRemove.push_back(false);
+ solver.attachClause(*newX);
+ for (const Lit * a = &((*newX)[0]), *end = a + newX->size(); a != end; a++) {
+ if (!blocked[a->var()])
+ varToXor[a->var()].push_back(make_pair(newX, (uint32_t)(toRemove.size()-1)));
+ }
+ break;
+ }
+ }
+
+ return true;
+}
+
+void Conglomerate::clearDouble(vector<Lit>& ps) const
+{
+ std::sort(ps.begin(), ps.end());
+ Lit p;
+ uint32_t i, j;
+ for (i = j = 0, p = lit_Undef; i != ps.size(); i++) {
+ ps[i] = ps[i].unsign();
+ if (ps[i] == p) {
+ //added, but easily removed
+ j--;
+ p = lit_Undef;
+ } else
+ ps[j++] = p = ps[i];
+ }
+ ps.resize(ps.size() - (i - j));
+}
+
+void Conglomerate::clearToRemove()
+{
+ assert(toRemove.size() == solver.xorclauses.size());
+
+ XorClause **a = solver.xorclauses.getData();
+ XorClause **r = a;
+ XorClause **end = a + solver.xorclauses.size();
+ for (uint i = 0; r != end; i++) {
+ if (!toRemove[i])
+ *a++ = *r++;
+ else {
+ r++;
+ }
+ }
+ solver.xorclauses.shrink(r-a);
+}
+
+void Conglomerate::clearLearntsFromToRemove()
+{
+ Clause **a = solver.learnts.getData();
+ Clause **r = a;
+ Clause **end = a + solver.learnts.size();
+ for (; r != end;) {
+ const Clause& c = **r;
+ bool inside = false;
+ if (!solver.locked(c)) {
+ for (uint i = 0; i < c.size(); i++) {
+ if (removedVars[c[i].var()]) {
+ inside = true;
+ break;
+ }
+ }
+ }
+ if (!inside)
+ *a++ = *r++;
+ else {
+ solver.removeClause(**r);
+ r++;
+ }
+ }
+ solver.learnts.shrink(r-a);
+}
+
+void Conglomerate::extendModel(Solver& solver2)
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "Executing doCalcAtFinish" << endl;
+ #endif
+
+ vec<Lit> ps;
+ for (int i = (int)(calcAtFinish.size())-1; i >= 0; i--) {
+ XorClause& c = *calcAtFinish[i];
+ assert(c.size() > 2);
+
+ ps.clear();
+ for (Lit *l = c.getData(), *end = c.getDataEnd(); l != end; l++) {
+ ps.push(l->unsign());
+ }
+
+ solver2.addXorClause(ps, c.xor_clause_inverted(), c.getGroup());
+ assert(solver2.ok);
+ }
+}
+
+const bool Conglomerate::addRemovedClauses()
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "Executing addRemovedClauses" << endl;
+ #endif
+
+ for(XorClause **it = calcAtFinish.getData(), **end = calcAtFinish.getDataEnd(); it != end; it++)
+ {
+ XorClause& c = **it;
+ #ifdef VERBOSE_DEBUG
+ cout << "readding already removed (conglomerated) clause: ";
+ c.plainPrint();
+ #endif
+
+ for(Lit *l = c.getData(), *end2 = c.getDataEnd(); l != end2 ; l++)
+ *l = l->unsign();
+
+ FILE* backup_libraryCNFfile = solver.libraryCNFFile;
+ solver.libraryCNFFile = NULL;
+ if (!solver.addXorClause(c, c.xor_clause_inverted(), c.getGroup())) {
+ for (;it != end; it++) free(*it);
+ calcAtFinish.clear();
+ return false;
+ }
+ solver.libraryCNFFile = backup_libraryCNFfile;
+ free(&c);
+ }
+ calcAtFinish.clear();
+
+ std::fill(removedVars.getData(), removedVars.getDataEnd(), false);
+ for (Var *v = madeVarNonDecision.getData(), *end = madeVarNonDecision.getDataEnd(); v != end; v++) {
+ solver.setDecisionVar(*v, true);
+ }
+ madeVarNonDecision.clear();
+
+ return true;
+}
+
+}; //NAMESPACE MINISAT
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef CONGLOMERATE_H
+#define CONGLOMERATE_H
+
+#include <vector>
+#include <map>
+#include <set>
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include "Clause.h"
+#include "VarReplacer.h"
+#include "Solver.h"
+
+using std::vector;
+using std::pair;
+using std::map;
+using std::set;
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class Solver;
+
+class Conglomerate
+{
+public:
+ Conglomerate(Solver& solver);
+ ~Conglomerate();
+ const bool conglomerateXorsFull();
+ const bool heuleProcessFull();
+ const bool addRemovedClauses(); ///<Add clauses that have been removed. Used if solve() is called multiple times
+ void extendModel(Solver& solver2); ///<Calculate variables removed during conglomeration
+
+ const vec<XorClause*>& getCalcAtFinish() const;
+ vec<XorClause*>& getCalcAtFinish();
+ const vec<bool>& getRemovedVars() const;
+ const bool needCalcAtFinish() const;
+
+ void newVar();
+
+private:
+
+ struct ClauseSetSorter {
+ bool operator () (const pair<XorClause*, uint32_t>& a, const pair<XorClause*, uint32_t>& b) {
+ return a.first->size() < b.first->size();
+ }
+ };
+
+ const bool conglomerateXors();
+ const bool heuleProcess();
+
+ void fillNewSet(vector<vector<Lit> >& newSet, vector<pair<XorClause*, uint32_t> >& clauseSet) const;
+
+ void removeVar(const Var var);
+ void processClause(XorClause& x, uint32_t num, Var remove_var);
+ void blockVars();
+ void fillVarToXor();
+ void clearDouble(vector<Lit>& ps) const;
+ void clearToRemove();
+ void clearLearntsFromToRemove();
+ bool dealWithNewClause(vector<Lit>& ps, const bool inverted, const uint old_group);
+
+ typedef map<uint, vector<pair<XorClause*, uint32_t> > > varToXorMap;
+ varToXorMap varToXor;
+ vector<bool> blocked;
+ vector<bool> toRemove;
+
+ vec<bool> removedVars;
+ vec<Var> madeVarNonDecision;
+
+ vec<XorClause*> calcAtFinish;
+ uint found;
+
+ Solver& solver;
+};
+
+inline void Conglomerate::newVar()
+{
+ removedVars.push(false);
+}
+
+inline const vec<bool>& Conglomerate::getRemovedVars() const
+{
+ return removedVars;
+}
+
+inline const vec<XorClause*>& Conglomerate::getCalcAtFinish() const
+{
+ return calcAtFinish;
+}
+
+inline vec<XorClause*>& Conglomerate::getCalcAtFinish()
+{
+ return calcAtFinish;
+}
+
+inline const bool Conglomerate::needCalcAtFinish() const
+{
+ return calcAtFinish.size();
+}
+
+}; //NAMESPACE MINISAT
+
+#endif //CONGLOMERATE_H
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef DOUBLEPACKEDROW_H
+#define DOUBLEPACKEDROW_H
+
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include <stdlib.h>
+
+#include "SolverTypes.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class DoublePackedRow
+{
+ private:
+ class BitIter {
+ public:
+ inline void operator=(const lbool toSet)
+ {
+ val &= ~((unsigned char)3 << offset);
+ val |= toSet.value << offset;
+ }
+
+ inline operator lbool() const
+ {
+ return lbool((val >> offset) & 3);
+ }
+
+ inline const bool isUndef() const {
+ return ((lbool)*this).isUndef();
+ }
+ inline const bool isDef() const {
+ return ((lbool)*this).isDef();
+ }
+ inline const bool getBool() const {
+ return ((lbool)*this).getBool();
+ }
+ inline const bool operator==(lbool b) const {
+ return ((lbool)*this) == b;
+ }
+ inline const bool operator!=(lbool b) const {
+ return ((lbool)*this) != b;
+ }
+ const lbool operator^(const bool b) const {
+ return ((lbool)*this) ^ b;
+ }
+
+ private:
+ friend class DoublePackedRow;
+ inline BitIter(unsigned char& mp, const uint32_t _offset) :
+ val(mp)
+ , offset(_offset)
+ {}
+
+ unsigned char& val;
+ const uint32_t offset;
+ };
+
+ class BitIterConst {
+ public:
+ inline operator lbool() const
+ {
+ return lbool((val >> offset) & 3);
+ }
+
+ inline const bool isUndef() const {
+ return ((lbool)*this).isUndef();
+ }
+ inline const bool isDef() const {
+ return ((lbool)*this).isDef();
+ }
+ inline const bool getBool() const {
+ return ((lbool)*this).getBool();
+ }
+ inline const bool operator==(lbool b) const {
+ return ((lbool)*this) == b;
+ }
+ inline const bool operator!=(lbool b) const {
+ return ((lbool)*this) != b;
+ }
+ const lbool operator^(const bool b) const {
+ return ((lbool)*this) ^ b;
+ }
+
+
+ private:
+ friend class DoublePackedRow;
+ inline BitIterConst(unsigned char& mp, const uint32_t _offset) :
+ val(mp)
+ , offset(_offset)
+ {}
+
+ const unsigned char& val;
+ const uint32_t offset;
+ };
+
+ public:
+ DoublePackedRow() :
+ numElems(0)
+ , mp(NULL)
+ {}
+
+ uint32_t size() const
+ {
+ return numElems;
+ }
+
+ void growTo(const uint32_t newNumElems)
+ {
+ uint32_t oldSize = numElems/4 + (bool)(numElems % 4);
+ uint32_t newSize = newNumElems/4 + (bool)(newNumElems % 4);
+
+ if (oldSize >= newSize) {
+ numElems = std::max(newNumElems, numElems);
+ return;
+ }
+
+ mp = (unsigned char*)realloc(mp, newSize*sizeof(unsigned char));
+ numElems = newNumElems;
+ }
+
+ inline BitIter operator[](const uint32_t at)
+ {
+ return BitIter(mp[at/4], (at%4)*2);
+ }
+
+ inline const BitIterConst operator[](const uint32_t at) const
+ {
+ return BitIterConst(mp[at/4], (at%4)*2);
+ }
+
+ inline void push(const lbool val)
+ {
+ growTo(numElems+1);
+ (*this)[numElems-1] = val;
+ }
+
+ /*void clear(const uint32_t at)
+ {
+ mp[at/32] &= ~((uint64_t)3 << ((at%32)*2));
+ }*/
+
+ private:
+
+ Var numElems;
+ unsigned char *mp;
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //DOUBLEPACKEDROW_H
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#include "FailedVarSearcher.h"
+
+#include <iomanip>
+#include <utility>
+#include <set>
+using std::make_pair;
+using std::set;
+
+#include "Solver.h"
+#include "ClauseCleaner.h"
+#include "time_mem.h"
+#include "VarReplacer.h"
+#include "ClauseCleaner.h"
+#include "StateSaver.h"
+
+#ifdef _MSC_VER
+#define __builtin_prefetch(a,b,c)
+#endif //_MSC_VER
+
+//#define VERBOSE_DEUBUG
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+FailedVarSearcher::FailedVarSearcher(Solver& _solver):
+ solver(_solver)
+ , tmpPs(2)
+ , finishedLastTimeVar(true)
+ , lastTimeWentUntilVar(0)
+ , finishedLastTimeBin(true)
+ , lastTimeWentUntilBin(0)
+ , numPropsMultiplier(1.0)
+ , lastTimeFoundTruths(0)
+ , numCalls(0)
+{
+}
+
+void FailedVarSearcher::addFromSolver(const vec< XorClause* >& cs)
+{
+ xorClauseSizes.clear();
+ xorClauseSizes.growTo(cs.size());
+ occur.resize(solver.nVars());
+ for (Var var = 0; var < solver.nVars(); var++) {
+ occur[var].clear();
+ }
+
+ uint32_t i = 0;
+ for (XorClause * const*it = cs.getData(), * const*end = it + cs.size(); it != end; it++, i++) {
+ if (it+1 != end)
+ __builtin_prefetch(*(it+1), 0, 0);
+
+ const XorClause& cl = **it;
+ xorClauseSizes[i] = cl.size();
+ for (const Lit *l = cl.getData(), *end2 = l + cl.size(); l != end2; l++) {
+ occur[l->var()].push_back(i);
+ }
+ }
+}
+
+inline void FailedVarSearcher::removeVarFromXors(const Var var)
+{
+ vector<uint32_t>& occ = occur[var];
+ if (occ.empty()) return;
+
+ for (uint32_t *it = &occ[0], *end = it + occ.size(); it != end; it++) {
+ xorClauseSizes[*it]--;
+ if (!xorClauseTouched[*it]) {
+ xorClauseTouched.setBit(*it);
+ investigateXor.push(*it);
+ }
+ }
+}
+
+inline void FailedVarSearcher::addVarFromXors(const Var var)
+{
+ vector<uint32_t>& occ = occur[var];
+ if (occ.empty()) return;
+
+ for (uint32_t *it = &occ[0], *end = it + occ.size(); it != end; it++) {
+ xorClauseSizes[*it]++;
+ }
+}
+
+const TwoLongXor FailedVarSearcher::getTwoLongXor(const XorClause& c)
+{
+ TwoLongXor tmp;
+ uint32_t num = 0;
+ tmp.inverted = c.xor_clause_inverted();
+
+ for(const Lit *l = c.getData(), *end = l + c.size(); l != end; l++) {
+ if (solver.assigns[l->var()] == l_Undef) {
+ assert(num < 2);
+ tmp.var[num] = l->var();
+ num++;
+ } else {
+ tmp.inverted ^= (solver.assigns[l->var()] == l_True);
+ }
+ }
+
+ #ifdef VERBOSE_DEUBUG
+ if (num != 2) {
+ std::cout << "Num:" << num << std::endl;
+ c.plainPrint();
+ }
+ #endif
+
+ std::sort(&tmp.var[0], &tmp.var[0]+2);
+ assert(num == 2);
+ return tmp;
+}
+
+const bool FailedVarSearcher::search(uint64_t numProps)
+{
+ assert(solver.decisionLevel() == 0);
+ solver.testAllClauseAttach();
+ double myTime = cpuTime();
+ uint32_t origHeapSize = solver.order_heap.size();
+ StateSaver savedState(solver);
+ Heap<Solver::VarOrderLt> order_heap_copy(solver.order_heap); //for hyperbin
+ uint64_t origBinClauses = solver.binaryClauses.size();
+
+ if (solver.readdOldLearnts && !readdRemovedLearnts()) goto end;
+
+ //General Stats
+ numFailed = 0;
+ goodBothSame = 0;
+ numCalls++;
+
+ //If failed var searching is going good, do successively more and more of it
+ if (lastTimeFoundTruths > 500 || (double)lastTimeFoundTruths > (double)solver.order_heap.size() * 0.03) std::max(numPropsMultiplier*1.7, 5.0);
+ else numPropsMultiplier = 1.0;
+ numProps = (uint64_t) ((double)numProps * numPropsMultiplier *3);
+
+ //For BothSame
+ propagated.resize(solver.nVars(), 0);
+ propValue.resize(solver.nVars(), 0);
+
+ //For calculating how many variables have really been set
+ origTrailSize = solver.trail.size();
+
+ //For 2-long xor (rule 6 of Equivalent literal propagation in the DLL procedure by Chu-Min Li)
+ toReplaceBefore = solver.varReplacer->getNewToReplaceVars();
+ lastTrailSize = solver.trail.size();
+ binXorFind = true;
+ twoLongXors.clear();
+ if (solver.xorclauses.size() < 5 ||
+ solver.xorclauses.size() > 30000 ||
+ solver.order_heap.size() > 30000 ||
+ solver.nClauses() > 100000)
+ binXorFind = false;
+ if (binXorFind) {
+ solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
+ addFromSolver(solver.xorclauses);
+ }
+ xorClauseTouched.resize(solver.xorclauses.size(), 0);
+ newBinXor = 0;
+
+ //For 2-long xor through Le Berre paper
+ bothInvert = 0;
+
+ //For HyperBin
+ unPropagatedBin.resize(solver.nVars(), 0);
+ myimplies.resize(solver.nVars(), 0);
+ hyperbinProps = 0;
+ if (solver.addExtraBins && !orderLits()) return false;
+ maxHyperBinProps = numProps/8;
+
+ //uint32_t fromBin;
+ uint32_t fromVar;
+ if (finishedLastTimeVar || lastTimeWentUntilVar >= solver.nVars())
+ fromVar = 0;
+ else
+ fromVar = lastTimeWentUntilVar;
+ finishedLastTimeVar = true;
+ lastTimeWentUntilVar = solver.nVars();
+ origProps = solver.propagations;
+ for (Var var = fromVar; var < solver.nVars(); var++) {
+ if (solver.assigns[var] != l_Undef || !solver.decision_var[var])
+ continue;
+ if (solver.propagations - origProps >= numProps) {
+ finishedLastTimeVar = false;
+ lastTimeWentUntilVar = var;
+ break;
+ }
+ if (!tryBoth(Lit(var, false), Lit(var, true)))
+ goto end;
+ }
+
+ numProps = (double)numProps * 1.2;
+ hyperbinProps = 0;
+ while (!order_heap_copy.empty()) {
+ Var var = order_heap_copy.removeMin();
+ if (solver.assigns[var] != l_Undef || !solver.decision_var[var])
+ continue;
+ if (solver.propagations - origProps >= numProps) {
+ finishedLastTimeVar = false;
+ lastTimeWentUntilVar = var;
+ break;
+ }
+ if (!tryBoth(Lit(var, false), Lit(var, true)))
+ goto end;
+ }
+
+ /*if (solver.verbosity >= 1) printResults(myTime);
+ if (finishedLastTimeBin || lastTimeWentUntilBin >= solver.binaryClauses.size())
+ fromBin = 0;
+ else
+ fromBin = lastTimeWentUntilBin;
+ finishedLastTimeBin = true;
+ lastTimeWentUntilBin = solver.nVars();
+ for (uint32_t binCl = 0; binCl < solver.binaryClauses.size(); binCl++) {
+ if ((double)(solver.propagations - origProps) >= 1.1*(double)numProps) {
+ finishedLastTimeBin = false;
+ lastTimeWentUntilBin = binCl;
+ break;
+ }
+
+ Clause& cl = *solver.binaryClauses[binCl];
+ if (solver.value(cl[0]) == l_Undef && solver.value(cl[1]) == l_Undef) {
+ if (!tryBoth(cl[0], cl[1]))
+ goto end;
+ }
+ }*/
+
+ /*for (Clause **it = solver.clauses.getData(), **end = solver.clauses.getDataEnd(); it != end; it++) {
+ Clause& c = **it;
+ for (uint i = 0; i < c.size(); i++) {
+ if (solver.value(c[i]) != l_Undef) goto next;
+ }
+ if (!tryAll(c.getData(), c.getDataEnd()))
+ goto end;
+
+ next:;
+ }
+
+ for (Clause **it = solver.learnts.getData(), **end = solver.learnts.getDataEnd(); it != end; it++) {
+ Clause& c = **it;
+ for (uint i = 0; i < c.size(); i++) {
+ if (solver.value(c[i]) != l_Undef) goto next2;
+ }
+ if (!tryAll(c.getData(), c.getDataEnd()))
+ goto end;
+
+ next2:;
+ }*/
+
+end:
+ bool removedOldLearnts = false;
+ binClauseAdded = solver.binaryClauses.size() - origBinClauses;
+ //Print results
+ if (solver.verbosity >= 1) printResults(myTime);
+
+ solver.order_heap.filter(Solver::VarFilter(solver));
+
+ if (solver.ok && (numFailed || goodBothSame)) {
+ double time = cpuTime();
+ if ((int)origHeapSize - (int)solver.order_heap.size() > (int)origHeapSize/15 && solver.nClauses() + solver.learnts.size() > 500000) {
+ completelyDetachAndReattach();
+ removedOldLearnts = true;
+ } else {
+ solver.clauseCleaner->removeAndCleanAll();
+ }
+ if (solver.verbosity >= 1 && numFailed + goodBothSame > 100) {
+ std::cout << "c | Cleaning up after failed var search: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime() - time << " s "
+ << std::setw(33) << " | " << std::endl;
+ }
+ }
+
+ if (solver.ok && solver.readdOldLearnts && !removedOldLearnts) {
+ if (solver.removedLearnts.size() < 100000) {
+ removeOldLearnts();
+ } else {
+ completelyDetachAndReattach();
+ }
+ }
+
+ lastTimeFoundTruths = solver.trail.size() - origTrailSize;
+
+ savedState.restore();
+
+ solver.testAllClauseAttach();
+ return solver.ok;
+}
+
+void FailedVarSearcher::completelyDetachAndReattach()
+{
+ solver.clauses_literals = 0;
+ solver.learnts_literals = 0;
+ for (uint32_t i = 0; i < solver.nVars(); i++) {
+ solver.binwatches[i*2].clear();
+ solver.binwatches[i*2+1].clear();
+ solver.watches[i*2].clear();
+ solver.watches[i*2+1].clear();
+ solver.xorwatches[i].clear();
+ }
+ solver.varReplacer->reattachInternalClauses();
+ cleanAndAttachClauses(solver.binaryClauses);
+ cleanAndAttachClauses(solver.clauses);
+ cleanAndAttachClauses(solver.learnts);
+ cleanAndAttachClauses(solver.xorclauses);
+}
+
+void FailedVarSearcher::printResults(const double myTime) const
+{
+ std::cout << "c | Flit: "<< std::setw(5) << numFailed <<
+ " Blit: " << std::setw(6) << goodBothSame <<
+ " bXBeca: " << std::setw(4) << newBinXor <<
+ " bXProp: " << std::setw(4) << bothInvert <<
+ " Bins:" << std::setw(7) << binClauseAdded <<
+ " P: " << std::setw(4) << std::fixed << std::setprecision(1) << (double)(solver.propagations - origProps)/1000000.0 << "M"
+ " T: " << std::setw(5) << std::fixed << std::setprecision(2) << cpuTime() - myTime <<
+ std::setw(5) << " |" << std::endl;
+}
+
+const bool FailedVarSearcher::orderLits()
+{
+ uint64_t oldProps = solver.propagations;
+ double myTime = cpuTime();
+ uint32_t numChecked = 0;
+ litDegrees.clear();
+ litDegrees.resize(solver.nVars()*2, 0);
+ BitArray alreadyTested;
+ alreadyTested.resize(solver.nVars()*2, 0);
+ uint32_t i;
+
+ for (i = 0; i < 3*solver.order_heap.size(); i++) {
+ if (solver.propagations - oldProps > 1500000) break;
+ Var var = solver.order_heap[solver.mtrand.randInt(solver.order_heap.size()-1)];
+ if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue;
+
+ Lit randLit(var, solver.mtrand.randInt(1));
+ if (alreadyTested[randLit.toInt()]) continue;
+ alreadyTested.setBit(randLit.toInt());
+
+ numChecked++;
+ solver.newDecisionLevel();
+ solver.uncheckedEnqueueLight(randLit);
+ failed = (solver.propagateBin() != NULL);
+ if (failed) {
+ solver.cancelUntil(0);
+ solver.uncheckedEnqueue(~randLit);
+ solver.ok = (solver.propagate() == NULL);
+ if (!solver.ok) return false;
+ continue;
+ }
+ assert(solver.decisionLevel() > 0);
+ for (int c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) {
+ Lit x = solver.trail[c];
+ litDegrees[x.toInt()]++;
+ }
+ solver.cancelUntil(0);
+ }
+ std::cout << "c binary Degree finding time: " << cpuTime() - myTime << " s num checked: " << numChecked << " i: " << i << " props: " << (solver.propagations - oldProps) << std::endl;
+ solver.propagations = oldProps;
+
+ return true;
+}
+
+void FailedVarSearcher::removeOldLearnts()
+{
+ for (Clause **it = solver.removedLearnts.getData(), **end = solver.removedLearnts.getDataEnd(); it != end; it++) {
+ solver.detachClause(**it);
+ }
+}
+
+struct reduceDB_ltOldLearnt
+{
+ bool operator () (const Clause* x, const Clause* y) {
+ return x->size() > y->size();
+ }
+};
+
+const bool FailedVarSearcher::readdRemovedLearnts()
+{
+ uint32_t toRemove = (solver.removedLearnts.size() > MAX_OLD_LEARNTS) ? (solver.removedLearnts.size() - MAX_OLD_LEARNTS/4) : 0;
+ if (toRemove > 0)
+ std::sort(solver.removedLearnts.getData(), solver.removedLearnts.getDataEnd(), reduceDB_ltOldLearnt());
+
+ Clause **it1, **it2;
+ it1 = it2 = solver.removedLearnts.getData();
+ for (Clause **end = solver.removedLearnts.getDataEnd(); it1 != end; it1++) {
+ if (toRemove > 0) {
+ clauseFree(*it1);
+ toRemove--;
+ continue;
+ }
+
+ Clause* c = solver.addClauseInt(**it1, (**it1).getGroup());
+ clauseFree(*it1);
+ if (c != NULL) {
+ *it2 = c;
+ it2++;
+ }
+ if (!solver.ok) {
+ it1++;
+ for (; it1 != end; it1++) clauseFree(*it1);
+ }
+ }
+ solver.removedLearnts.shrink(it1-it2);
+ //std::cout << "Readded old learnts. New facts:" << (int)origHeapSize - (int)solver.order_heap.size() << std::endl;
+
+ return solver.ok;
+}
+
+#define MAX_REMOVE_BIN_FULL_PROPS 20000000
+#define EXTRATIME_DIVIDER 3
+
+template<bool startUp>
+const bool FailedVarSearcher::removeUslessBinFull()
+{
+ if (!solver.performReplace) return true;
+ while (solver.performReplace && solver.varReplacer->getClauses().size() > 0) {
+ if (!solver.varReplacer->performReplace(true)) return false;
+ solver.clauseCleaner->removeAndCleanAll(true);
+ }
+ assert(solver.varReplacer->getClauses().size() == 0);
+ solver.testAllClauseAttach();
+ if (startUp) {
+ solver.clauseCleaner->moveBinClausesToBinClauses();
+ }
+
+ double myTime = cpuTime();
+ toDeleteSet.clear();
+ toDeleteSet.growTo(solver.nVars()*2, 0);
+ uint32_t origHeapSize = solver.order_heap.size();
+ uint64_t origProps = solver.propagations;
+ bool fixed = false;
+ uint32_t extraTime = solver.binaryClauses.size() / EXTRATIME_DIVIDER;
+
+ uint32_t startFrom = solver.mtrand.randInt(solver.order_heap.size());
+ for (uint32_t i = 0; i != solver.order_heap.size(); i++) {
+ Var var = solver.order_heap[(i+startFrom)%solver.order_heap.size()];
+ if (solver.propagations - origProps + extraTime > MAX_REMOVE_BIN_FULL_PROPS) break;
+ if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue;
+
+ Lit lit(var, true);
+ if (!removeUselessBinaries<startUp>(lit)) {
+ fixed = true;
+ solver.cancelUntil(0);
+ solver.uncheckedEnqueue(~lit);
+ solver.ok = (solver.propagate() == NULL);
+ if (!solver.ok) return false;
+ continue;
+ }
+
+ lit = ~lit;
+ if (!removeUselessBinaries<startUp>(lit)) {
+ fixed = true;
+ solver.cancelUntil(0);
+ solver.uncheckedEnqueue(~lit);
+ solver.ok = (solver.propagate() == NULL);
+ if (!solver.ok) return false;
+ continue;
+ }
+ }
+
+ Clause **i, **j;
+ i = j = solver.binaryClauses.getData();
+ uint32_t num = 0;
+ for (Clause **end = solver.binaryClauses.getDataEnd(); i != end; i++, num++) {
+ if (!(*i)->removed()) {
+ *j++ = *i;
+ } else {
+ clauseFree(*i);
+ }
+ }
+ uint32_t removedUselessBin = i - j;
+ solver.binaryClauses.shrink(i - j);
+
+ if (fixed) solver.order_heap.filter(Solver::VarFilter(solver));
+
+ if (solver.verbosity >= 1) {
+ std::cout
+ << "c Removed useless bin:" << std::setw(8) << removedUselessBin
+ << " fixed: " << std::setw(4) << (origHeapSize - solver.order_heap.size())
+ << " props: " << std::fixed << std::setprecision(2) << std::setw(4) << (double)(solver.propagations - origProps)/1000000.0 << "M"
+ << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << cpuTime() - myTime << std::endl;
+ }
+
+ return true;
+}
+
+const bool FailedVarSearcher::tryBoth(const Lit lit1, const Lit lit2)
+{
+ if (binXorFind) {
+ if (lastTrailSize < solver.trail.size()) {
+ for (uint32_t i = lastTrailSize; i != solver.trail.size(); i++) {
+ removeVarFromXors(solver.trail[i].var());
+ }
+ }
+ lastTrailSize = solver.trail.size();
+ xorClauseTouched.setZero();
+ investigateXor.clear();
+ }
+
+ propagated.setZero();
+ twoLongXors.clear();
+ propagatedVars.clear();
+ unPropagatedBin.setZero();
+ bothSame.clear();
+
+ solver.newDecisionLevel();
+ solver.uncheckedEnqueueLight(lit1);
+ failed = (solver.propagateLight() != NULL);
+ if (failed) {
+ solver.cancelUntil(0);
+ numFailed++;
+ solver.uncheckedEnqueue(~lit1);
+ solver.ok = (solver.propagate(false) == NULL);
+ if (!solver.ok) return false;
+ return true;
+ } else {
+ assert(solver.decisionLevel() > 0);
+ for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) {
+ Var x = solver.trail[c].var();
+ propagated.setBit(x);
+ if (solver.addExtraBins) {
+ unPropagatedBin.setBit(x);
+ propagatedVars.push(x);
+ }
+ if (solver.assigns[x].getBool()) propValue.setBit(x);
+ else propValue.clearBit(x);
+
+ if (binXorFind) removeVarFromXors(x);
+ }
+
+ if (binXorFind) {
+ for (uint32_t *it = investigateXor.getData(), *end = investigateXor.getDataEnd(); it != end; it++) {
+ if (xorClauseSizes[*it] == 2)
+ twoLongXors.insert(getTwoLongXor(*solver.xorclauses[*it]));
+ }
+ for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) {
+ addVarFromXors(solver.trail[c].var());
+ }
+ xorClauseTouched.setZero();
+ investigateXor.clear();
+ }
+
+ solver.cancelUntil(0);
+ }
+
+ if (solver.addExtraBins && hyperbinProps < maxHyperBinProps) addBinClauses(lit1);
+ propagatedVars.clear();
+ unPropagatedBin.setZero();
+
+ solver.newDecisionLevel();
+ solver.uncheckedEnqueueLight(lit2);
+ failed = (solver.propagateLight() != NULL);
+ if (failed) {
+ solver.cancelUntil(0);
+ numFailed++;
+ solver.uncheckedEnqueue(~lit2);
+ solver.ok = (solver.propagate(false) == NULL);
+ if (!solver.ok) return false;
+ return true;
+ } else {
+ assert(solver.decisionLevel() > 0);
+ for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) {
+ Var x = solver.trail[c].var();
+ if (propagated[x]) {
+ if (solver.addExtraBins) {
+ unPropagatedBin.setBit(x);
+ propagatedVars.push(x);
+ }
+ if (propValue[x] == solver.assigns[x].getBool()) {
+ //they both imply the same
+ bothSame.push(Lit(x, !propValue[x]));
+ } else if (c != (int)solver.trail_lim[0]) {
+ bool invert;
+ if (lit1.var() == lit2.var()) {
+ assert(lit1.sign() == false && lit2.sign() == true);
+ tmpPs[0] = Lit(lit1.var(), false);
+ tmpPs[1] = Lit(x, false);
+ invert = propValue[x];
+ } else {
+ tmpPs[0] = Lit(lit1.var(), false);
+ tmpPs[1] = Lit(lit2.var(), false);
+ invert = lit1.sign() ^ lit2.sign();
+ }
+ if (!solver.varReplacer->replace(tmpPs, invert, 0))
+ return false;
+ bothInvert += solver.varReplacer->getNewToReplaceVars() - toReplaceBefore;
+ toReplaceBefore = solver.varReplacer->getNewToReplaceVars();
+ }
+ }
+ if (solver.assigns[x].getBool()) propValue.setBit(x);
+ else propValue.clearBit(x);
+ if (binXorFind) removeVarFromXors(x);
+ }
+
+ if (binXorFind) {
+ if (twoLongXors.size() > 0) {
+ for (uint32_t *it = investigateXor.getData(), *end = it + investigateXor.size(); it != end; it++) {
+ if (xorClauseSizes[*it] == 2) {
+ TwoLongXor tmp = getTwoLongXor(*solver.xorclauses[*it]);
+ if (twoLongXors.find(tmp) != twoLongXors.end()) {
+ tmpPs[0] = Lit(tmp.var[0], false);
+ tmpPs[1] = Lit(tmp.var[1], false);
+ if (!solver.varReplacer->replace(tmpPs, tmp.inverted, solver.xorclauses[*it]->getGroup()))
+ return false;
+ newBinXor += solver.varReplacer->getNewToReplaceVars() - toReplaceBefore;
+ toReplaceBefore = solver.varReplacer->getNewToReplaceVars();
+ }
+ }
+ }
+ }
+ for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) {
+ addVarFromXors(solver.trail[c].var());
+ }
+ }
+
+ solver.cancelUntil(0);
+ }
+
+ if (solver.addExtraBins && hyperbinProps < maxHyperBinProps) addBinClauses(lit2);
+
+ for(uint32_t i = 0; i != bothSame.size(); i++) {
+ solver.uncheckedEnqueue(bothSame[i]);
+ }
+ goodBothSame += bothSame.size();
+ solver.ok = (solver.propagate(false) == NULL);
+ if (!solver.ok) return false;
+
+ return true;
+}
+
+struct litOrder
+{
+ litOrder(const vector<uint32_t>& _litDegrees) :
+ litDegrees(_litDegrees)
+ {}
+
+ bool operator () (const Lit& x, const Lit& y) {
+ return litDegrees[x.toInt()] > litDegrees[y.toInt()];
+ }
+
+ const vector<uint32_t>& litDegrees;
+};
+
+void FailedVarSearcher::addBinClauses(const Lit& lit)
+{
+ uint64_t oldProps = solver.propagations;
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Checking one BTC vs UP" << std::endl;
+ #endif //VERBOSE_DEBUG
+ vec<Lit> toVisit;
+
+ solver.newDecisionLevel();
+ solver.uncheckedEnqueueLight(lit);
+ failed = (solver.propagateBin() != NULL);
+ assert(!failed);
+
+ assert(solver.decisionLevel() > 0);
+ if (propagatedVars.size() - (solver.trail.size()-solver.trail_lim[0]) == 0) {
+ solver.cancelUntil(0);
+ goto end;
+ }
+ for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) {
+ Lit x = solver.trail[c];
+ unPropagatedBin.clearBit(x.var());
+ toVisit.push(x);
+ }
+ solver.cancelUntil(0);
+
+ std::sort(toVisit.getData(), toVisit.getDataEnd(), litOrder(litDegrees));
+ /*************************
+ //To check that the ordering is the right way
+ // --> i.e. to avoid mistake present in Glucose's ordering
+ for (uint32_t i = 0; i < toVisit.size(); i++) {
+ std::cout << "i:" << std::setw(8) << i << " degree:" << litDegrees[toVisit[i].toInt()] << std::endl;
+ }
+ std::cout << std::endl;
+ ***************************/
+
+ //difference between UP and BTC is in unPropagatedBin
+ for (Lit *l = toVisit.getData(), *end = toVisit.getDataEnd(); l != end; l++) {
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Checking visit level " << end-l-1 << std::endl;
+ uint32_t thisLevel = 0;
+ #endif //VERBOSE_DEBUG
+ fillImplies(*l);
+ if (unPropagatedBin.nothingInCommon(myimplies)) goto next;
+ for (const Var *var = propagatedVars.getData(), *end2 = propagatedVars.getDataEnd(); var != end2; var++) {
+ if (unPropagatedBin[*var] && myimplies[*var]) {
+ #ifdef VERBOSE_DEBUG
+ thisLevel++;
+ #endif //VERBOSE_DEBUG
+ addBin(~*l, Lit(*var, !propValue[*var]));
+ unPropagatedBin.removeThese(myImpliesSet);
+ if (unPropagatedBin.isZero()) {
+ myimplies.removeThese(myImpliesSet);
+ myImpliesSet.clear();
+ goto end;
+ }
+ }
+ }
+ next:
+ myimplies.removeThese(myImpliesSet);
+ myImpliesSet.clear();
+ #ifdef VERBOSE_DEBUG
+ if (thisLevel > 0) {
+ std::cout << "Added " << thisLevel << " level diff:" << end-l-1 << std::endl;
+ }
+ #endif //VERBOSE_DEBUG
+ }
+ assert(unPropagatedBin.isZero());
+
+ end:
+ hyperbinProps += solver.propagations - oldProps;
+}
+
+void FailedVarSearcher::fillImplies(const Lit& lit)
+{
+ solver.newDecisionLevel();
+ solver.uncheckedEnqueue(lit);
+ failed = (solver.propagateLight() != NULL);
+ assert(!failed);
+
+ assert(solver.decisionLevel() > 0);
+ for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) {
+ Lit x = solver.trail[c];
+ myimplies.setBit(x.var());
+ myImpliesSet.push(x.var());
+ }
+ solver.cancelUntil(0);
+}
+
+template<bool startUp>
+const bool FailedVarSearcher::fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec<Lit>& wrong)
+{
+ solver.newDecisionLevel();
+ solver.uncheckedEnqueueLight(lit);
+ //if it's a cycle, it doesn't work, so don't propagate origLit
+ failed = (solver.propagateBinExcept<startUp>(origLit) != NULL);
+ if (failed) return false;
+
+ assert(solver.decisionLevel() > 0);
+ int c;
+ extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER;
+ for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) {
+ Lit x = solver.trail[c];
+ if (toDeleteSet[x.toInt()]) {
+ wrong.push(x);
+ toDeleteSet[x.toInt()] = false;
+ };
+ solver.assigns[x.var()] = l_Undef;
+ }
+ solver.assigns[solver.trail[c].var()] = l_Undef;
+
+ solver.qhead = solver.trail_lim[0];
+ solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]);
+ solver.trail_lim.clear();
+ //solver.cancelUntil(0);
+
+ return true;
+}
+
+void FailedVarSearcher::addBin(const Lit& lit1, const Lit& lit2)
+{
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Adding extra bin: ";
+ lit1.print(); std::cout << " "; lit2.printFull();
+ #endif //VERBOSE_DEBUG
+
+ tmpPs[0] = lit1;
+ tmpPs[1] = lit2;
+ solver.addLearntClause(tmpPs, 0, 0);
+ tmpPs.growTo(2);
+ assert(solver.ok);
+}
+
+template<bool startUp>
+const bool FailedVarSearcher::removeUselessBinaries(const Lit& lit)
+{
+ //Nothing can be learnt at this point!
+ //Otherwise, it might happen that the path to X has learnts,
+ //but binary clause to X is not learnt.
+ //So we remove X , then we might remove
+ //the path (since it's learnt) -- removing a FACT!!
+ //[note:removal can be through variable elimination
+ //, and removeWrong() will happily remove it
+ assert(!startUp || solver.learnts.size() == 0);
+
+ solver.newDecisionLevel();
+ solver.uncheckedEnqueueLight(lit);
+ failed = (solver.propagateBinOneLevel<startUp>() != NULL);
+ if (failed) return false;
+ bool ret = true;
+
+ oneHopAway.clear();
+ assert(solver.decisionLevel() > 0);
+ int c;
+ if (solver.trail.size()-solver.trail_lim[0] == 0) {
+ solver.cancelUntil(0);
+ goto end;
+ }
+ extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER;
+ for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) {
+ Lit x = solver.trail[c];
+ toDeleteSet[x.toInt()] = true;
+ oneHopAway.push(x);
+ solver.assigns[x.var()] = l_Undef;
+ }
+ solver.assigns[solver.trail[c].var()] = l_Undef;
+
+ solver.qhead = solver.trail_lim[0];
+ solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]);
+ solver.trail_lim.clear();
+ //solver.cancelUntil(0);
+
+ wrong.clear();
+ for(uint32_t i = 0; i < oneHopAway.size(); i++) {
+ //no need to visit it if it already queued for removal
+ //basically, we check if it's in 'wrong'
+ if (toDeleteSet[oneHopAway[i].toInt()]) {
+ if (!fillBinImpliesMinusLast<startUp>(lit, oneHopAway[i], wrong)) {
+ ret = false;
+ goto end;
+ }
+ }
+ }
+
+ for (uint32_t i = 0; i < wrong.size(); i++) {
+ removeBin(~lit, wrong[i]);
+ }
+
+ end:
+ for(uint32_t i = 0; i < oneHopAway.size(); i++) {
+ toDeleteSet[oneHopAway[i].toInt()] = false;
+ }
+
+ return ret;
+}
+template const bool FailedVarSearcher::removeUselessBinaries <true>(const Lit& lit);
+template const bool FailedVarSearcher::removeUselessBinaries <false>(const Lit& lit);
+template const bool FailedVarSearcher::fillBinImpliesMinusLast <true>(const Lit& origLit, const Lit& lit, vec<Lit>& wrong);
+template const bool FailedVarSearcher::fillBinImpliesMinusLast <false>(const Lit& origLit, const Lit& lit, vec<Lit>& wrong);
+template const bool FailedVarSearcher::removeUslessBinFull <true>();
+template const bool FailedVarSearcher::removeUslessBinFull <false>();
+
+void FailedVarSearcher::removeBin(const Lit& lit1, const Lit& lit2)
+{
+ /*******************
+ Lit litFind1 = lit_Undef;
+ Lit litFind2 = lit_Undef;
+
+ if (solver.binwatches[(~lit1).toInt()].size() < solver.binwatches[(~lit2).toInt()].size()) {
+ litFind1 = lit1;
+ litFind2 = lit2;
+ } else {
+ litFind1 = lit2;
+ litFind2 = lit1;
+ }
+ ********************/
+
+ //Find AND remove from watches
+ vec<WatchedBin>& bwin = solver.binwatches[(~lit1).toInt()];
+ extraTime += bwin.size() / EXTRATIME_DIVIDER;
+ Clause *cl = NULL;
+ WatchedBin *i, *j;
+ i = j = bwin.getData();
+ for (const WatchedBin *end = bwin.getDataEnd(); i != end; i++) {
+ if (i->impliedLit == lit2 && cl == NULL) {
+ cl = i->clause;
+ } else {
+ *j++ = *i;
+ }
+ }
+ bwin.shrink(1);
+ assert(cl != NULL);
+
+ bool found = false;
+ vec<WatchedBin>& bwin2 = solver.binwatches[(~lit2).toInt()];
+ extraTime += bwin2.size() / EXTRATIME_DIVIDER;
+ i = j = bwin2.getData();
+ for (const WatchedBin *end = bwin2.getDataEnd(); i != end; i++) {
+ if (i->clause == cl) {
+ found = true;
+ } else {
+ *j++ = *i;
+ }
+ }
+ bwin2.shrink(1);
+ assert(found);
+
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Removing useless bin: ";
+ cl->plainPrint();
+ #endif //VERBOSE_DEBUG
+
+ cl->setRemoved();
+ solver.clauses_literals -= 2;
+}
+
+template<class T>
+inline void FailedVarSearcher::cleanAndAttachClauses(vec<T*>& cs)
+{
+ T **i = cs.getData();
+ T **j = i;
+ for (T **end = cs.getDataEnd(); i != end; i++) {
+ if (cleanClause(**i)) {
+ solver.attachClause(**i);
+ *j++ = *i;
+ } else {
+ clauseFree(*i);
+ }
+ }
+ cs.shrink(i-j);
+}
+
+inline const bool FailedVarSearcher::cleanClause(Clause& ps)
+{
+ uint32_t origSize = ps.size();
+
+ Lit *i = ps.getData();
+ Lit *j = i;
+ for (Lit *end = ps.getDataEnd(); i != end; i++) {
+ if (solver.value(*i) == l_True) return false;
+ if (solver.value(*i) == l_Undef) {
+ *j++ = *i;
+ }
+ }
+ ps.shrink(i-j);
+ assert(ps.size() > 1);
+
+ if (ps.size() != origSize) ps.setStrenghtened();
+ if (origSize != 2 && ps.size() == 2)
+ solver.becameBinary++;
+
+ return true;
+}
+
+inline const bool FailedVarSearcher::cleanClause(XorClause& ps)
+{
+ uint32_t origSize = ps.size();
+
+ Lit *i = ps.getData(), *j = i;
+ for (Lit *end = ps.getDataEnd(); i != end; i++) {
+ if (solver.assigns[i->var()] == l_True) ps.invert(true);
+ if (solver.assigns[i->var()] == l_Undef) {
+ *j++ = *i;
+ }
+ }
+ ps.shrink(i-j);
+
+ if (ps.size() == 0) return false;
+ assert(ps.size() > 1);
+
+ if (ps.size() != origSize) ps.setStrenghtened();
+ if (ps.size() == 2) {
+ ps[0] = ps[0].unsign();
+ ps[1] = ps[1].unsign();
+ solver.varReplacer->replace(ps, ps.xor_clause_inverted(), ps.getGroup());
+ return false;
+ }
+
+ return true;
+}
+
+/***************
+UNTESTED CODE
+*****************
+const bool FailedVarSearcher::tryAll(const Lit* begin, const Lit* end)
+{
+ propagated.setZero();
+ BitArray propagated2;
+ propagated2.resize(solver.nVars(), 0);
+ propValue.resize(solver.nVars(), 0);
+ bool first = true;
+ bool last = false;
+
+ for (const Lit *it = begin; it != end; it++, first = false) {
+ if (it+1 == end) last = true;
+
+ if (!first && !last) propagated2.setZero();
+ solver.newDecisionLevel();
+ solver.uncheckedEnqueue(*it);
+ failed = (solver.propagate(false) != NULL);
+ if (failed) {
+ solver.cancelUntil(0);
+ numFailed++;
+ solver.uncheckedEnqueue(~(*it));
+ solver.ok = (solver.propagate(false) == NULL);
+ if (!solver.ok) return false;
+ return true;
+ } else {
+ assert(solver.decisionLevel() > 0);
+ for (int c = solver.trail.size()-1; c >= (int)solver.trail_lim[0]; c--) {
+ Var x = solver.trail[c].var();
+ if (last) {
+ if (propagated[x] && propValue[x] == solver.assigns[x].getBool())
+ bothSame.push_back(make_pair(x, !propValue[x]));
+ } else {
+ if (first) {
+ propagated.setBit(x);
+ if (solver.assigns[x].getBool())
+ propValue.setBit(x);
+ else
+ propValue.clearBit(x);
+ } else if (propValue[x] == solver.assigns[x].getBool()) {
+ propagated2.setBit(x);
+ }
+ }
+ }
+ solver.cancelUntil(0);
+ }
+ if (!last && !first) {
+ propagated &= propagated2;
+ if (propagated.isZero()) return true;
+ }
+ }
+
+ for(uint32_t i = 0; i != bothSame.size(); i++) {
+ solver.uncheckedEnqueue(Lit(bothSame[i].first, bothSame[i].second));
+ }
+ goodBothSame += bothSame.size();
+ bothSame.clear();
+ solver.ok = (solver.propagate(false) == NULL);
+ if (!solver.ok) return false;
+
+ return true;
+}
+**************
+Untested code end
+**************/
+
+}; //NAMESPACE MINISAT
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef FAILEDVARSEARCHER_H
+#define FAILEDVARSEARCHER_H
+
+#include <set>
+#include <map>
+using std::map;
+
+#include "SolverTypes.h"
+#include "Clause.h"
+#include "BitArray.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class Solver;
+
+class TwoLongXor
+{
+ public:
+ const bool operator==(const TwoLongXor& other) const
+ {
+ if (var[0] == other.var[0] && var[1] == other.var[1] && inverted == other.inverted)
+ return true;
+ return false;
+ }
+ const bool operator<(const TwoLongXor& other) const
+ {
+ if (var[0] < other.var[0]) return true;
+ if (var[0] > other.var[0]) return false;
+
+ if (var[1] < other.var[1]) return true;
+ if (var[1] > other.var[1]) return false;
+
+ if (inverted < other.inverted) return true;
+ if (inverted > other.inverted) return false;
+
+ return false;
+ }
+
+ Var var[2];
+ bool inverted;
+};
+
+class FailedVarSearcher {
+ public:
+ FailedVarSearcher(Solver& _solver);
+
+ const bool search(uint64_t numProps);
+ template<bool startUp>
+ const bool removeUslessBinFull();
+
+ private:
+ //For 2-long xor
+ const TwoLongXor getTwoLongXor(const XorClause& c);
+ void addFromSolver(const vec<XorClause*>& cs);
+ uint32_t newBinXor;
+
+ //For detach&re-attach (when lots of vars found)
+ template<class T>
+ void cleanAndAttachClauses(vec<T*>& cs);
+ const bool cleanClause(Clause& ps);
+ const bool cleanClause(XorClause& ps);
+ void completelyDetachAndReattach();
+
+ //For re-adding old removed learnt clauses
+ const bool readdRemovedLearnts();
+ void removeOldLearnts();
+
+ //Main
+ const bool tryBoth(const Lit lit1, const Lit lit2);
+ const bool tryAll(const Lit* begin, const Lit* end);
+ void printResults(const double myTime) const;
+
+ Solver& solver;
+
+ //Time
+ uint32_t extraTime;
+
+ //For failure
+ bool failed;
+
+ //bothprop finding
+ BitArray propagated;
+ BitArray propValue;
+ vec<Lit> bothSame;
+
+ //2-long xor-finding
+ vec<uint32_t> xorClauseSizes;
+ vector<vector<uint32_t> > occur;
+ void removeVarFromXors(const Var var);
+ void addVarFromXors(const Var var);
+ BitArray xorClauseTouched;
+ vec<uint32_t> investigateXor;
+ std::set<TwoLongXor> twoLongXors;
+ bool binXorFind;
+ uint32_t lastTrailSize;
+
+ //2-long xor-finding no.2 through
+ // 1) (a->b, ~a->~b) -> a=b
+ // 2) binary clause (a,c): (a->g, c->~g) -> a = ~c
+ uint32_t bothInvert;
+
+ //finding HyperBins
+ void addBinClauses(const Lit& lit);
+ BitArray unPropagatedBin;
+ vec<Var> propagatedVars;
+ void addBin(const Lit& lit1, const Lit& lit2);
+ void fillImplies(const Lit& lit);
+ BitArray myimplies;
+ vec<Var> myImpliesSet;
+ uint64_t hyperbinProps;
+ vector<uint32_t> litDegrees;
+ const bool orderLits();
+ uint64_t maxHyperBinProps;
+ uint64_t binClauseAdded;
+
+ //Remove useless binaries
+ template<bool startUp>
+ const bool fillBinImpliesMinusLast(const Lit& origLit, const Lit& lit, vec<Lit>& wrong);
+ template<bool startUp>
+ const bool removeUselessBinaries(const Lit& lit);
+ void removeBin(const Lit& lit1, const Lit& lit2);
+ vec<char> toDeleteSet;
+ vec<Lit> oneHopAway;
+ vec<Lit> wrong;
+
+ //Temporaries
+ vec<Lit> tmpPs;
+
+ //State for this run
+ uint32_t toReplaceBefore;
+ uint32_t origTrailSize;
+ uint64_t origProps;
+ uint32_t numFailed;
+ uint32_t goodBothSame;
+
+ //State between runs
+ bool finishedLastTimeVar;
+ uint32_t lastTimeWentUntilVar;
+ bool finishedLastTimeBin;
+ uint32_t lastTimeWentUntilBin;
+
+ double numPropsMultiplier;
+ uint32_t lastTimeFoundTruths;
+
+ uint32_t numCalls;
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //FAILEDVARSEARCHER_H
\ No newline at end of file
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#include "FindUndef.h"
+
+#include "Solver.h"
+#include "VarReplacer.h"
+#include <algorithm>
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+FindUndef::FindUndef(Solver& _solver) :
+ solver(_solver)
+ , isPotentialSum(0)
+{
+}
+
+void FindUndef::fillPotential()
+{
+ int trail = solver.decisionLevel()-1;
+
+ while(trail > 0) {
+ assert(trail < (int)solver.trail_lim.size());
+ uint at = solver.trail_lim[trail];
+
+ assert(at > 0);
+ Var v = solver.trail[at].var();
+ if (solver.assigns[v] != l_Undef) {
+ isPotential[v] = true;
+ isPotentialSum++;
+ }
+
+ trail--;
+ }
+
+ for (XorClause** it = solver.xorclauses.getData(), **end = it + solver.xorclauses.size(); it != end; it++) {
+ XorClause& c = **it;
+ for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) {
+ if (isPotential[l->var()]) {
+ isPotential[l->var()] = false;
+ isPotentialSum--;
+ }
+ assert(!solver.value(*l).isUndef());
+ }
+ }
+
+ vector<Var> replacingVars = solver.varReplacer->getReplacingVars();
+ for (Var *it = &replacingVars[0], *end = it + replacingVars.size(); it != end; it++) {
+ if (isPotential[*it]) {
+ isPotential[*it] = false;
+ isPotentialSum--;
+ }
+ }
+}
+
+void FindUndef::unboundIsPotentials()
+{
+ for (uint i = 0; i < isPotential.size(); i++)
+ if (isPotential[i])
+ solver.assigns[i] = l_Undef;
+}
+
+void FindUndef::moveBinToNormal()
+{
+ binPosition = solver.clauses.size();
+ for (uint i = 0; i != solver.binaryClauses.size(); i++)
+ solver.clauses.push(solver.binaryClauses[i]);
+ solver.binaryClauses.clear();
+}
+
+void FindUndef::moveBinFromNormal()
+{
+ for (uint i = binPosition; i != solver.clauses.size(); i++)
+ solver.binaryClauses.push(solver.clauses[i]);
+ solver.clauses.shrink(solver.clauses.size() - binPosition);
+}
+
+const uint FindUndef::unRoll()
+{
+ if (solver.decisionLevel() == 0) return 0;
+
+ moveBinToNormal();
+
+ dontLookAtClause.resize(solver.clauses.size(), false);
+ isPotential.resize(solver.nVars(), false);
+ fillPotential();
+ satisfies.resize(solver.nVars(), 0);
+
+ while(!updateTables()) {
+ assert(isPotentialSum > 0);
+
+ uint32_t maximum = 0;
+ Var v = var_Undef;
+ for (uint i = 0; i < isPotential.size(); i++) {
+ if (isPotential[i] && satisfies[i] >= maximum) {
+ maximum = satisfies[i];
+ v = i;
+ }
+ }
+ assert(v != var_Undef);
+
+ isPotential[v] = false;
+ isPotentialSum--;
+
+ std::fill(satisfies.begin(), satisfies.end(), 0);
+ }
+
+ unboundIsPotentials();
+ moveBinFromNormal();
+
+ return isPotentialSum;
+}
+
+bool FindUndef::updateTables()
+{
+ bool allSat = true;
+
+ uint i = 0;
+ for (Clause** it = solver.clauses.getData(), **end = it + solver.clauses.size(); it != end; it++, i++) {
+ if (dontLookAtClause[i])
+ continue;
+
+ Clause& c = **it;
+ bool definitelyOK = false;
+ Var v = var_Undef;
+ uint numTrue = 0;
+ for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) {
+ if (solver.value(*l) == l_True) {
+ if (!isPotential[l->var()]) {
+ dontLookAtClause[i] = true;
+ definitelyOK = true;
+ break;
+ } else {
+ numTrue ++;
+ v = l->var();
+ }
+ }
+ }
+ if (definitelyOK)
+ continue;
+
+ if (numTrue == 1) {
+ assert(v != var_Undef);
+ isPotential[v] = false;
+ isPotentialSum--;
+ dontLookAtClause[i] = true;
+ continue;
+ }
+
+ //numTrue > 1
+ allSat = false;
+ for (Lit *l = c.getData(), *end = l + c.size(); l != end; l++) {
+ if (solver.value(*l) == l_True)
+ satisfies[l->var()]++;
+ }
+ }
+
+ return allSat;
+}
+
+}; //NAMESPACE MINISAT
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef FINDUNDEF_H
+#define FINDUNDEF_H
+
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+#include <vector>
+using std::vector;
+
+#include "Solver.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class FindUndef {
+ public:
+ FindUndef(Solver& _solver);
+ const uint unRoll();
+
+ private:
+ Solver& solver;
+
+ void moveBinToNormal();
+ void moveBinFromNormal();
+ bool updateTables();
+ void fillPotential();
+ void unboundIsPotentials();
+
+ vector<bool> dontLookAtClause; //If set to TRUE, then that clause already has only 1 lit that is true, so it can be skipped during updateFixNeed()
+ vector<uint32_t> satisfies;
+ vector<bool> isPotential;
+ uint32_t isPotentialSum;
+ uint32_t binPosition;
+
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //
\ No newline at end of file
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#include "Gaussian.h"
+
+#include <iostream>
+#include <iomanip>
+#include "Clause.h"
+#include <algorithm>
+#include "ClauseCleaner.h"
+
+using std::ostream;
+using std::cout;
+using std::endl;
+
+#ifdef VERBOSE_DEBUG
+#include <iterator>
+#endif
+
+namespace MINISAT
+{
+using namespace MINISAT;
+static const uint16_t unassigned_col = std::numeric_limits<uint16_t>::max();
+static const Var unassigned_var = std::numeric_limits<Var>::max();
+
+ostream& operator << (ostream& os, const vec<Lit>& v)
+{
+ for (uint32_t i = 0; i != v.size(); i++) {
+ if (v[i].sign()) os << "-";
+ os << v[i].var()+1 << " ";
+ }
+
+ return os;
+}
+
+Gaussian::Gaussian(Solver& _solver, const GaussianConfig& _config, const uint _matrix_no, const vector<XorClause*>& _xorclauses) :
+ solver(_solver)
+ , config(_config)
+ , matrix_no(_matrix_no)
+ , xorclauses(_xorclauses)
+ , messed_matrix_vars_since_reversal(true)
+ , gauss_last_level(0)
+ , disabled(false)
+ , useful_prop(0)
+ , useful_confl(0)
+ , called(0)
+ , unit_truths(0)
+{
+}
+
+Gaussian::~Gaussian()
+{
+ for (uint i = 0; i < clauses_toclear.size(); i++)
+ clauseFree(clauses_toclear[i].first);
+}
+
+inline void Gaussian::set_matrixset_to_cur()
+{
+ uint level = solver.decisionLevel() / config.only_nth_gauss_save;
+ assert(level <= matrix_sets.size());
+
+ if (level == matrix_sets.size())
+ matrix_sets.push_back(cur_matrixset);
+ else
+ matrix_sets[level] = cur_matrixset;
+}
+
+const bool Gaussian::full_init()
+{
+ assert(solver.ok);
+
+ if (!should_init()) return true;
+ reset_stats();
+ uint32_t last_trail_size = solver.trail.size();
+
+ bool do_again_gauss = true;
+ while (do_again_gauss) {
+ do_again_gauss = false;
+ solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
+ if (!solver.ok) return false;
+ init();
+ Clause* confl;
+ gaussian_ret g = gaussian(confl);
+ switch (g) {
+ case unit_conflict:
+ case conflict:
+ solver.ok = false;
+ return false;
+ case unit_propagation:
+ case propagation:
+ unit_truths += last_trail_size - solver.trail.size();
+ do_again_gauss = true;
+ solver.ok = (solver.propagate() == NULL);
+ if (!solver.ok) return false;
+ break;
+ case nothing:
+ break;
+ }
+ }
+
+ return true;
+}
+
+void Gaussian::init()
+{
+ assert(solver.decisionLevel() == 0);
+
+ fill_matrix(cur_matrixset);
+ if (!cur_matrixset.num_rows || !cur_matrixset.num_cols) {
+ disabled = true;
+ badlevel = 0;
+ return;
+ }
+
+ matrix_sets.clear();
+ matrix_sets.push_back(cur_matrixset);
+ gauss_last_level = solver.trail.size();
+ messed_matrix_vars_since_reversal = false;
+ badlevel = UINT_MAX;
+
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Gaussian init finished." << endl;
+ #endif
+}
+
+uint Gaussian::select_columnorder(vector<uint16_t>& var_to_col, matrixset& origMat)
+{
+ var_to_col.resize(solver.nVars(), unassigned_col);
+
+ uint num_xorclauses = 0;
+ for (uint32_t i = 0; i != xorclauses.size(); i++) {
+ XorClause& c = *xorclauses[i];
+ if (c.removed()) continue;
+ num_xorclauses++;
+
+ for (uint i2 = 0; i2 < c.size(); i2++) {
+ assert(solver.assigns[c[i2].var()].isUndef());
+ var_to_col[c[i2].var()] = unassigned_col - 1;
+ }
+ }
+
+ uint largest_used_var = 0;
+ for (uint i = 0; i < var_to_col.size(); i++)
+ if (var_to_col[i] != unassigned_col)
+ largest_used_var = i;
+ var_to_col.resize(largest_used_var + 1);
+
+ var_is_in.resize(var_to_col.size(), 0);
+ origMat.var_is_set.resize(var_to_col.size(), 0);
+
+ origMat.col_to_var.clear();
+ vector<Var> vars(solver.nVars());
+ if (!config.orderCols) {
+ for (uint32_t i = 0; i < solver.nVars(); i++) {
+ vars.push_back(i);
+ }
+ std::random_shuffle(vars.begin(), vars.end());
+ }
+
+ Heap<Solver::VarOrderLt> order_heap(solver.order_heap);
+ uint32_t iterReduceIt = 0;
+ while ((config.orderCols && !order_heap.empty()) || (!config.orderCols && iterReduceIt < vars.size()))
+ {
+ Var v;
+ if (config.orderCols) v = order_heap.removeMin();
+ else v = vars[iterReduceIt++];
+ if (var_to_col[v] == 1) {
+ #ifdef DEBUG_GAUSS
+ vector<uint>::iterator it =
+ std::find(origMat.col_to_var.begin(), origMat.col_to_var.end(), v);
+ assert(it == origMat.col_to_var.end());
+ #endif
+
+ origMat.col_to_var.push_back(v);
+ var_to_col[v] = origMat.col_to_var.size()-1;
+ var_is_in.setBit(v);
+ }
+ }
+
+ //for the ones that were not in the order_heap, but are marked in var_to_col
+ for (uint v = 0; v != var_to_col.size(); v++) {
+ if (var_to_col[v] == unassigned_col - 1) {
+ origMat.col_to_var.push_back(v);
+ var_to_col[v] = origMat.col_to_var.size() -1;
+ var_is_in.setBit(v);
+ }
+ }
+
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")col_to_var:";
+ std::copy(origMat.col_to_var.begin(), origMat.col_to_var.end(), std::ostream_iterator<uint>(cout, ","));
+ cout << endl;
+ #endif
+
+ return num_xorclauses;
+}
+
+void Gaussian::fill_matrix(matrixset& origMat)
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Filling matrix" << endl;
+ #endif
+
+ vector<uint16_t> var_to_col;
+ origMat.num_rows = select_columnorder(var_to_col, origMat);
+ origMat.num_cols = origMat.col_to_var.size();
+ col_to_var_original = origMat.col_to_var;
+ changed_rows.resize(origMat.num_rows);
+ memset(&changed_rows[0], 0, sizeof(char)*changed_rows.size());
+
+ origMat.last_one_in_col.resize(origMat.num_cols);
+ std::fill(origMat.last_one_in_col.begin(), origMat.last_one_in_col.end(), origMat.num_rows);
+ origMat.first_one_in_row.resize(origMat.num_rows);
+
+ origMat.removeable_cols = 0;
+ origMat.least_column_changed = -1;
+ origMat.matrix.resize(origMat.num_rows, origMat.num_cols);
+
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")matrix size:" << origMat.num_rows << "," << origMat.num_cols << endl;
+ #endif
+
+ uint matrix_row = 0;
+ for (uint32_t i = 0; i != xorclauses.size(); i++) {
+ const XorClause& c = *xorclauses[i];
+ if (c.removed()) continue;
+
+ origMat.matrix.getVarsetAt(matrix_row).set(c, var_to_col, origMat.num_cols);
+ origMat.matrix.getMatrixAt(matrix_row).set(c, var_to_col, origMat.num_cols);
+ matrix_row++;
+ }
+ assert(origMat.num_rows == matrix_row);
+}
+
+void Gaussian::update_matrix_col(matrixset& m, const Var var, const uint col)
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Updating matrix var " << var+1 << " (col " << col << ", m.last_one_in_col[col]: " << m.last_one_in_col[col] << ")" << endl;
+ cout << "m.num_rows:" << m.num_rows << endl;
+ #endif
+
+ #ifdef DEBUG_GAUSS
+ assert(col < m.num_cols);
+ #endif
+
+ m.least_column_changed = std::min(m.least_column_changed, (int)col);
+ PackedMatrix::iterator this_row = m.matrix.beginMatrix();
+ uint row_num = 0;
+
+ if (solver.assigns[var].getBool()) {
+ for (uint end = m.last_one_in_col[col]; row_num != end; ++this_row, row_num++) {
+ if ((*this_row)[col]) {
+ changed_rows[row_num] = true;
+ (*this_row).invert_is_true();
+ (*this_row).clearBit(col);
+ }
+ }
+ } else {
+ for (uint end = m.last_one_in_col[col]; row_num != end; ++this_row, row_num++) {
+ if ((*this_row)[col]) {
+ changed_rows[row_num] = true;
+ (*this_row).clearBit(col);
+ }
+ }
+ }
+
+ #ifdef DEBUG_GAUSS
+ bool c = false;
+ for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = r + m.matrix.getSize(); r != end; ++r)
+ c |= (*r)[col];
+ assert(!c);
+ #endif
+
+ m.removeable_cols++;
+ m.col_to_var[col] = unassigned_var;
+ m.var_is_set.setBit(var);
+}
+
+void Gaussian::update_matrix_by_col_all(matrixset& m)
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Updating matrix." << endl;
+ print_matrix(m);
+ uint num_updated = 0;
+ #endif
+
+ #ifdef DEBUG_GAUSS
+ assert(nothing_to_propagate(cur_matrixset));
+ assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m));
+ #endif
+
+ memset(&changed_rows[0], 0, sizeof(char)*changed_rows.size());
+
+ uint last = 0;
+ uint col = 0;
+ for (const Var *it = &m.col_to_var[0], *end = it + m.num_cols; it != end; col++, it++) {
+ if (*it != unassigned_var && solver.assigns[*it].isDef()) {
+ update_matrix_col(m, *it, col);
+ last++;
+ #ifdef VERBOSE_DEBUG
+ num_updated++;
+ #endif
+ } else
+ last = 0;
+ }
+ m.num_cols -= last;
+
+ #ifdef DEBUG_GAUSS
+ check_matrix_against_varset(m.matrix, m);
+ #endif
+
+ #ifdef VERBOSE_DEBUG
+ cout << "Matrix update finished, updated " << num_updated << " cols" << endl;
+ print_matrix(m);
+ #endif
+
+ /*cout << "num_rows:" << m.num_rows;
+ cout << " num_rows diff:" << origMat.num_rows - m.num_rows << endl;
+ cout << "num_cols:" << col_to_var_original.size();
+ cout << " num_cols diff:" << col_to_var_original.size() - m.col_to_var.size() << endl;
+ cout << "removeable cols:" << m.removeable_cols << endl;*/
+}
+
+inline void Gaussian::update_last_one_in_col(matrixset& m)
+{
+ for (uint16_t* i = &m.last_one_in_col[0]+m.last_one_in_col.size()-1, *end = &m.last_one_in_col[0]-1; i != end && *i >= m.num_rows; i--)
+ *i = m.num_rows;
+}
+
+Gaussian::gaussian_ret Gaussian::gaussian(Clause*& confl)
+{
+ if (solver.decisionLevel() >= badlevel)
+ return nothing;
+
+ if (messed_matrix_vars_since_reversal) {
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")matrix needs copy before update" << endl;
+ #endif
+
+ const uint level = solver.decisionLevel() / config.only_nth_gauss_save;
+ assert(level < matrix_sets.size());
+ cur_matrixset = matrix_sets[level];
+ }
+ update_last_one_in_col(cur_matrixset);
+ update_matrix_by_col_all(cur_matrixset);
+
+ messed_matrix_vars_since_reversal = false;
+ gauss_last_level = solver.trail.size();
+ badlevel = UINT_MAX;
+
+ propagatable_rows.clear();
+ uint conflict_row = UINT_MAX;
+ uint last_row = eliminate(cur_matrixset, conflict_row);
+ #ifdef DEBUG_GAUSS
+ check_matrix_against_varset(cur_matrixset.matrix, cur_matrixset);
+ #endif
+
+ gaussian_ret ret;
+ //There is no early abort, so this is unneeded
+ /*if (conflict_row != UINT_MAX) {
+ uint maxlevel = UINT_MAX;
+ uint size = UINT_MAX;
+ uint best_row = UINT_MAX;
+ analyse_confl(cur_matrixset, conflict_row, maxlevel, size, best_row);
+ ret = handle_matrix_confl(confl, cur_matrixset, size, maxlevel, best_row);
+ } else {*/
+ ret = handle_matrix_prop_and_confl(cur_matrixset, last_row, confl);
+ //}
+ #ifdef DEBUG_GAUSS
+ assert(ret == conflict || nothing_to_propagate(cur_matrixset));
+ #endif
+
+ if (!cur_matrixset.num_cols || !cur_matrixset.num_rows) {
+ badlevel = solver.decisionLevel();
+ return nothing;
+ }
+
+ if (ret == nothing &&
+ solver.decisionLevel() % config.only_nth_gauss_save == 0)
+ set_matrixset_to_cur();
+
+ #ifdef VERBOSE_DEBUG
+ if (ret == nothing)
+ cout << "(" << matrix_no << ")Useless. ";
+ else
+ cout << "(" << matrix_no << ")Useful. ";
+ cout << "(" << matrix_no << ")Useful prop in " << ((double)useful_prop/(double)called)*100.0 << "%" << endl;
+ cout << "(" << matrix_no << ")Useful confl in " << ((double)useful_confl/(double)called)*100.0 << "%" << endl;
+ #endif
+
+ return ret;
+}
+
+uint Gaussian::eliminate(matrixset& m, uint& conflict_row)
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")";
+ cout << "Starting elimination" << endl;
+ cout << "m.least_column_changed:" << m.least_column_changed << endl;
+ print_last_one_in_cols(m);
+
+ uint number_of_row_additions = 0;
+ uint no_exchanged = 0;
+ #endif
+
+ if (m.least_column_changed == INT_MAX) {
+ #ifdef VERBOSE_DEBUG
+ cout << "Nothing to eliminate" << endl;
+ #endif
+
+ return m.num_rows;
+ }
+
+
+ #ifdef DEBUG_GAUSS
+ assert(solver.decisionLevel() == 0 || check_last_one_in_cols(m));
+ #endif
+
+ uint i = 0;
+ uint j = (config.iterativeReduce) ? m.least_column_changed + 1 : 0;
+ PackedMatrix::iterator beginIt = m.matrix.beginMatrix();
+ PackedMatrix::iterator rowIt = m.matrix.beginMatrix();
+
+ #ifdef DEBUG_GAUSS
+ check_first_one_in_row(m, j);
+ #endif
+
+ if (j) {
+ uint16_t until = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows);
+ if (j-1 > m.first_one_in_row[m.num_rows-1])
+ until = m.num_rows;
+ for (;i != until; i++, ++rowIt) if (changed_rows[i] && (*rowIt).popcnt_is_one(m.first_one_in_row[i]))
+ propagatable_rows.push(i);
+ }
+
+ #ifdef VERBOSE_DEBUG
+ cout << "At while() start: i,j = " << i << ", " << j << endl;
+ cout << "num_rows:" << m.num_rows << " num_cols:" << m.num_cols << endl;
+ #endif
+
+ if (j > m.num_cols) {
+ #ifdef VERBOSE_DEBUG
+ cout << "Going straight to finish" << endl;
+ #endif
+ goto finish;
+ }
+
+ #ifdef DEBUG_GAUSS
+ assert(i <= m.num_rows && j <= m.num_cols);
+ #endif
+
+ while (i != m.num_rows && j != m.num_cols) {
+ //Find pivot in column j, starting in row i:
+
+ if (m.col_to_var[j] == unassigned_var) {
+ j++;
+ continue;
+ }
+
+ PackedMatrix::iterator this_matrix_row = rowIt;
+ PackedMatrix::iterator end = beginIt + m.last_one_in_col[j];
+ for (; this_matrix_row != end; ++this_matrix_row) {
+ if ((*this_matrix_row)[j])
+ break;
+ }
+
+ if (this_matrix_row != end) {
+
+ //swap rows i and maxi, but do not change the value of i;
+ if (this_matrix_row != rowIt) {
+ #ifdef VERBOSE_DEBUG
+ no_exchanged++;
+ #endif
+
+ //Would early abort, but would not find the best conflict (and would be expensive)
+ //if (matrix_row_i.is_true() && matrix_row_i.isZero()) {
+ // conflict_row = i;
+ // return 0;
+ //}
+ (*rowIt).swapBoth(*this_matrix_row);
+ }
+ #ifdef DEBUG_GAUSS
+ assert(m.matrix.getMatrixAt(i).popcnt(j) == m.matrix.getMatrixAt(i).popcnt());
+ assert(m.matrix.getMatrixAt(i)[j]);
+ #endif
+
+ if ((*rowIt).popcnt_is_one(j))
+ propagatable_rows.push(i);
+
+ //Now A[i,j] will contain the old value of A[maxi,j];
+ ++this_matrix_row;
+ for (; this_matrix_row != end; ++this_matrix_row) if ((*this_matrix_row)[j]) {
+ //subtract row i from row u;
+ //Now A[u,j] will be 0, since A[u,j] - A[i,j] = A[u,j] -1 = 0.
+ #ifdef VERBOSE_DEBUG
+ number_of_row_additions++;
+ #endif
+
+ (*this_matrix_row).xorBoth(*rowIt);
+ //Would early abort, but would not find the best conflict (and would be expensive)
+ //if (it->is_true() &&it->isZero()) {
+ // conflict_row = i2;
+ // return 0;
+ //}
+ }
+ m.first_one_in_row[i] = j;
+ i++;
+ ++rowIt;
+ m.last_one_in_col[j] = i;
+ } else {
+ m.first_one_in_row[i] = j;
+ m.last_one_in_col[j] = i + 1;
+ }
+ j++;
+ }
+
+ finish:
+
+ m.least_column_changed = INT_MAX;
+
+ #ifdef VERBOSE_DEBUG
+ cout << "Finished elimination" << endl;
+ cout << "Returning with i,j:" << i << ", " << j << "(" << m.num_rows << ", " << m.num_cols << ")" << endl;
+ print_matrix(m);
+ print_last_one_in_cols(m);
+ cout << "(" << matrix_no << ")Exchanged:" << no_exchanged << " row additions:" << number_of_row_additions << endl;
+ #endif
+
+ #ifdef DEBUG_GAUSS
+ assert(check_last_one_in_cols(m));
+ uint row = 0;
+ uint col = 0;
+ for (; col < m.num_cols && row < m.num_rows && row < i ; col++) {
+ assert(m.matrix.getMatrixAt(row).popcnt() == m.matrix.getMatrixAt(row).popcnt(col));
+ assert(!(m.col_to_var[col] == unassigned_var && m.matrix.getMatrixAt(row)[col]));
+ if (m.col_to_var[col] == unassigned_var || !m.matrix.getMatrixAt(row)[col]) {
+ #ifdef VERBOSE_DEBUG
+ cout << "row:" << row << " col:" << col << " m.last_one_in_col[col]-1: " << m.last_one_in_col[col]-1 << endl;
+ #endif
+ assert(m.col_to_var[col] == unassigned_var || std::min((uint16_t)(m.last_one_in_col[col]-1), m.num_rows) == row);
+ continue;
+ }
+ row++;
+ }
+ #endif
+
+ return i;
+}
+
+Gaussian::gaussian_ret Gaussian::handle_matrix_confl(Clause*& confl, const matrixset& m, const uint size, const uint maxlevel, const uint best_row)
+{
+ assert(best_row != UINT_MAX);
+
+ m.matrix.getVarsetAt(best_row).fill(tmp_clause, solver.assigns, col_to_var_original);
+ confl = (Clause*)XorClause_new(tmp_clause, false, solver.learnt_clause_group++);
+ Clause& cla = *confl;
+ #ifdef STATS_NEEDED
+ if (solver.dynamic_behaviour_analysis)
+ solver.logger.set_group_name(confl->getGroup(), "learnt gauss clause");
+ #endif
+
+ if (cla.size() <= 1) {
+ solver.ok = false;
+ return unit_conflict;
+ }
+
+ assert(cla.size() >= 2);
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Found conflict:";
+ cla.plainPrint();
+ #endif
+
+ if (maxlevel != solver.decisionLevel()) {
+ #ifdef STATS_NEEDED
+ if (solver.dynamic_behaviour_analysis)
+ solver.logger.conflict(Logger::gauss_confl_type, maxlevel, confl->getGroup(), *confl);
+ #endif
+ solver.cancelUntil(maxlevel);
+ }
+ const uint curr_dec_level = solver.decisionLevel();
+ assert(maxlevel == curr_dec_level);
+
+ uint maxsublevel = 0;
+ uint maxsublevel_at = UINT_MAX;
+ for (uint i = 0, size = cla.size(); i != size; i++) if (solver.level[cla[i].var()] == (int32_t)curr_dec_level) {
+ uint tmp = find_sublevel(cla[i].var());
+ if (tmp >= maxsublevel) {
+ maxsublevel = tmp;
+ maxsublevel_at = i;
+ }
+ }
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ") || Sublevel of confl: " << maxsublevel << " (due to var:" << cla[maxsublevel_at].var()-1 << ")" << endl;
+ #endif
+
+ Lit tmp(cla[maxsublevel_at]);
+ cla[maxsublevel_at] = cla[1];
+ cla[1] = tmp;
+
+ cancel_until_sublevel(maxsublevel+1);
+ messed_matrix_vars_since_reversal = true;
+ return conflict;
+}
+
+Gaussian::gaussian_ret Gaussian::handle_matrix_prop_and_confl(matrixset& m, uint last_row, Clause*& confl)
+{
+ int32_t maxlevel = std::numeric_limits<int32_t>::max();
+ uint size = UINT_MAX;
+ uint best_row = UINT_MAX;
+
+ for (uint row = last_row; row != m.num_rows; row++) {
+ #ifdef DEBUG_GAUSS
+ assert(m.matrix.getMatrixAt(row).isZero());
+ #endif
+ if (m.matrix.getMatrixAt(row).is_true())
+ analyse_confl(m, row, maxlevel, size, best_row);
+ }
+
+ if (maxlevel != std::numeric_limits<int32_t>::max())
+ return handle_matrix_confl(confl, m, size, maxlevel, best_row);
+
+ #ifdef DEBUG_GAUSS
+ assert(check_no_conflict(m));
+ assert(last_row == 0 || !m.matrix.getMatrixAt(last_row-1).isZero());
+ #endif
+
+ #ifdef VERBOSE_DEBUG
+ cout << "Resizing matrix to num_rows = " << last_row << endl;
+ #endif
+ m.num_rows = last_row;
+ m.matrix.resizeNumRows(m.num_rows);
+
+ gaussian_ret ret = nothing;
+
+ uint num_props = 0;
+ for (const uint* prop_row = propagatable_rows.getData(), *end = prop_row + propagatable_rows.size(); prop_row != end; prop_row++ ) {
+ //this is a "000..1..0000000X" row. I.e. it indicates a propagation
+ ret = handle_matrix_prop(m, *prop_row);
+ num_props++;
+ if (ret == unit_propagation) {
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Unit prop! Breaking from prop examination" << endl;
+ #endif
+ return unit_propagation;
+ }
+ }
+ #ifdef VERBOSE_DEBUG
+ if (num_props > 0) cout << "(" << matrix_no << ")Number of props during gauss:" << num_props << endl;
+ #endif
+
+ return ret;
+}
+
+uint Gaussian::find_sublevel(const Var v) const
+{
+ for (int i = solver.trail.size()-1; i >= 0; i --)
+ if (solver.trail[i].var() == v) return i;
+
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Oooops! Var " << v+1 << " does not have a sublevel!! (so it must be undefined)" << endl;
+ #endif
+
+ assert(false);
+ return 0;
+}
+
+void Gaussian::cancel_until_sublevel(const uint until_sublevel)
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Canceling until sublevel " << until_sublevel << endl;
+ #endif
+
+ for (vector<Gaussian*>::iterator gauss = solver.gauss_matrixes.begin(), end= solver.gauss_matrixes.end(); gauss != end; gauss++)
+ if (*gauss != this) (*gauss)->canceling(until_sublevel);
+
+ for (int sublevel = solver.trail.size()-1; sublevel >= (int)until_sublevel; sublevel--) {
+ Var var = solver.trail[sublevel].var();
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Canceling var " << var+1 << endl;
+ #endif
+
+ #ifdef USE_OLD_POLARITIES
+ solver.polarity[var] = solver.oldPolarity[var];
+ #endif //USE_OLD_POLARITIES
+ solver.assigns[var] = l_Undef;
+ solver.insertVarOrder(var);
+ }
+ solver.trail.shrink(solver.trail.size() - until_sublevel);
+
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Canceling sublevel finished." << endl;
+ #endif
+}
+
+void Gaussian::analyse_confl(const matrixset& m, const uint row, int32_t& maxlevel, uint& size, uint& best_row) const
+{
+ assert(row < m.num_rows);
+
+ //this is a "000...00000001" row. I.e. it indicates we are on the wrong branch
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")matrix conflict found!" << endl;
+ cout << "(" << matrix_no << ")conflict clause's vars: ";
+ print_matrix_row_with_assigns(m.matrix.getVarsetAt(row));
+ cout << endl;
+
+ cout << "(" << matrix_no << ")corresponding matrix's row (should be empty): ";
+ print_matrix_row(m.matrix.getMatrixAt(row));
+ cout << endl;
+ #endif
+
+ int32_t this_maxlevel = 0;
+ unsigned long int var = 0;
+ uint this_size = 0;
+ while (true) {
+ var = m.matrix.getVarsetAt(row).scan(var);
+ if (var == ULONG_MAX) break;
+
+ const Var real_var = col_to_var_original[var];
+ assert(real_var < solver.nVars());
+
+ if (solver.level[real_var] > this_maxlevel)
+ this_maxlevel = solver.level[real_var];
+ var++;
+ this_size++;
+ }
+
+ //the maximum of all lit's level must be lower than the max. level of the current best clause (or this clause must be either empty or unit clause)
+ if (!(
+ (this_maxlevel < maxlevel)
+ || (this_maxlevel == maxlevel && this_size < size)
+ || (this_size <= 1)
+ )) {
+ assert(maxlevel != std::numeric_limits<int32_t>::max());
+
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")Other found conflict just as good or better.";
+ cout << "(" << matrix_no << ") || Old maxlevel:" << maxlevel << " new maxlevel:" << this_maxlevel;
+ cout << "(" << matrix_no << ") || Old size:" << size << " new size:" << this_size << endl;
+ //assert(!(maxlevel != UINT_MAX && maxlevel != this_maxlevel)); //NOTE: only holds if gauss is executed at each level
+ #endif
+
+ return;
+ }
+
+
+ #ifdef VERBOSE_DEBUG
+ if (maxlevel != std::numeric_limits<int32_t>::max())
+ cout << "(" << matrix_no << ")Better conflict found.";
+ else
+ cout << "(" << matrix_no << ")Found a possible conflict.";
+
+ cout << "(" << matrix_no << ") || Old maxlevel:" << maxlevel << " new maxlevel:" << this_maxlevel;
+ cout << "(" << matrix_no << ") || Old size:" << size << " new size:" << this_size << endl;
+ #endif
+
+ maxlevel = this_maxlevel;
+ size = this_size;
+ best_row = row;
+}
+
+Gaussian::gaussian_ret Gaussian::handle_matrix_prop(matrixset& m, const uint row)
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")matrix prop found!" << endl;
+ cout << m.matrix.getMatrixAt(row) << endl;
+ cout << "(" << matrix_no << ")matrix row:";
+ print_matrix_row(m.matrix.getMatrixAt(row));
+ cout << endl;
+ #endif
+
+ m.matrix.getVarsetAt(row).fill(tmp_clause, solver.assigns, col_to_var_original);
+ Clause& cla = *(Clause*)XorClause_new(tmp_clause, false, solver.learnt_clause_group++);
+ #ifdef VERBOSE_DEBUG
+ cout << "(" << matrix_no << ")matrix prop clause: ";
+ cla.plainPrint();
+ cout << endl;
+ #endif
+
+ assert(m.matrix.getMatrixAt(row).is_true() == !cla[0].sign());
+ assert(solver.assigns[cla[0].var()].isUndef());
+ if (cla.size() == 1) {
+ solver.cancelUntil(0);
+ solver.uncheckedEnqueue(cla[0]);
+ clauseFree(&cla);
+ return unit_propagation;
+ }
+
+ clauses_toclear.push_back(std::make_pair(&cla, solver.trail.size()-1));
+ #ifdef STATS_NEEDED
+ if (solver.dynamic_behaviour_analysis)
+ solver.logger.set_group_name(cla.getGroup(), "gauss prop clause");
+ #endif
+ solver.uncheckedEnqueue(cla[0], &cla);
+
+ return propagation;
+}
+
+void Gaussian::disable_if_necessary()
+{
+ if (//nof_conflicts >= 0
+ //&& conflictC >= nof_conflicts/8
+ !config.dontDisable
+ && called > 50
+ && useful_confl*2+useful_prop < (uint)((double)called*0.05) )
+ disabled = true;
+}
+
+llbool Gaussian::find_truths(vec<Lit>& learnt_clause, int& conflictC)
+{
+ Clause* confl;
+
+ disable_if_necessary();
+ if (should_check_gauss(solver.decisionLevel(), solver.starts)) {
+ called++;
+ gaussian_ret g = gaussian(confl);
+
+ switch (g) {
+ case conflict: {
+ useful_confl++;
+ llbool ret = solver.handle_conflict(learnt_clause, confl, conflictC, true);
+ clauseFree(confl);
+
+ if (ret != l_Nothing) return ret;
+ return l_Continue;
+ }
+ case unit_propagation:
+ unit_truths++;
+ case propagation:
+ useful_prop++;
+ return l_Continue;
+ case unit_conflict: {
+ unit_truths++;
+ useful_confl++;
+ if (confl->size() == 0) {
+ clauseFree(confl);
+ return l_False;
+ }
+
+ Lit lit = (*confl)[0];
+ #ifdef STATS_NEEDED
+ if (solver.dynamic_behaviour_analysis)
+ solver.logger.conflict(Logger::gauss_confl_type, 0, confl->getGroup(), *confl);
+ #endif
+
+ solver.cancelUntil(0);
+
+ if (solver.assigns[lit.var()].isDef()) {
+ clauseFree(confl);
+ return l_False;
+ }
+
+ solver.uncheckedEnqueue(lit);
+
+ clauseFree(confl);
+ return l_Continue;
+ }
+ case nothing:
+ break;
+ }
+ }
+
+ return l_Nothing;
+}
+
+template<class T>
+void Gaussian::print_matrix_row(const T& row) const
+{
+ unsigned long int var = 0;
+ while (true) {
+ var = row.scan(var);
+ if (var == ULONG_MAX) break;
+
+ else cout << col_to_var_original[var]+1 << ", ";
+ var++;
+ }
+ cout << "final:" << row.is_true() << endl;;
+}
+
+template<class T>
+void Gaussian::print_matrix_row_with_assigns(const T& row) const
+{
+ unsigned long int col = 0;
+ while (true) {
+ col = row.scan(col);
+ if (col == ULONG_MAX) break;
+
+ else {
+ Var var = col_to_var_original[col];
+ cout << var+1 << "(" << lbool_to_string(solver.assigns[var]) << ")";
+ cout << ", ";
+ }
+ col++;
+ }
+ if (!row.is_true()) cout << "xor_clause_inverted";
+}
+
+const string Gaussian::lbool_to_string(const lbool toprint)
+{
+ if (toprint == l_True)
+ return "true";
+ if (toprint == l_False)
+ return "false";
+ if (toprint == l_Undef)
+ return "undef";
+
+ assert(false);
+ return "";
+}
+
+
+void Gaussian::print_stats() const
+{
+ if (called > 0) {
+ cout.setf(std::ios::fixed);
+ std::cout << " Gauss(" << matrix_no << ") useful";
+ cout << " prop: " << std::setprecision(2) << std::setw(5) << ((double)useful_prop/(double)called)*100.0 << "% ";
+ cout << " confl: " << std::setprecision(2) << std::setw(5) << ((double)useful_confl/(double)called)*100.0 << "% ";
+ if (disabled) std::cout << "disabled";
+ } else
+ std::cout << " Gauss(" << matrix_no << ") not called.";
+}
+
+void Gaussian::print_matrix_stats() const
+{
+ cout << "matrix size: " << cur_matrixset.num_rows << " x " << cur_matrixset.num_cols << endl;
+}
+
+
+void Gaussian::reset_stats()
+{
+ useful_prop = 0;
+ useful_confl = 0;
+ called = 0;
+ disabled = false;
+}
+
+bool Gaussian::check_no_conflict(matrixset& m) const
+{
+ uint row = 0;
+ for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r, ++row) {
+ if ((*r).is_true() && (*r).isZero()) {
+ cout << "Conflict at row " << row << endl;
+ return false;
+ }
+ }
+ return true;
+}
+
+void Gaussian::print_matrix(matrixset& m) const
+{
+ uint row = 0;
+ for (PackedMatrix::iterator it = m.matrix.beginMatrix(); it != m.matrix.endMatrix(); ++it, row++) {
+ cout << *it << " -- row:" << row;
+ if (row >= m.num_rows)
+ cout << " (considered past the end)";
+ cout << endl;
+ }
+}
+
+void Gaussian::print_last_one_in_cols(matrixset& m) const
+{
+ for (uint i = 0; i < m.num_cols; i++) {
+ cout << "last_one_in_col[" << i << "]-1 = " << m.last_one_in_col[i]-1 << endl;
+ }
+}
+
+const bool Gaussian::nothing_to_propagate(matrixset& m) const
+{
+ for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r) {
+ if ((*r).popcnt_is_one()
+ && solver.assigns[m.col_to_var[(*r).scan(0)]].isUndef())
+ return false;
+ }
+ for(PackedMatrix::iterator r = m.matrix.beginMatrix(), end = m.matrix.endMatrix(); r != end; ++r) {
+ if ((*r).isZero() && (*r).is_true())
+ return false;
+ }
+ return true;
+}
+
+const bool Gaussian::check_last_one_in_cols(matrixset& m) const
+{
+ for(uint i = 0; i < m.num_cols; i++) {
+ const uint last = std::min(m.last_one_in_col[i] - 1, (int)m.num_rows);
+ uint real_last = 0;
+ uint i2 = 0;
+ for (PackedMatrix::iterator it = m.matrix.beginMatrix(); it != m.matrix.endMatrix(); ++it, i2++) {
+ if ((*it)[i])
+ real_last = i2;
+ }
+ if (real_last > last)
+ return false;
+ }
+
+ return true;
+}
+
+void Gaussian::check_matrix_against_varset(PackedMatrix& matrix, const matrixset& m) const
+{
+ for (uint i = 0; i < matrix.getSize(); i++) {
+ const PackedRow mat_row = matrix.getMatrixAt(i);
+ const PackedRow var_row = matrix.getVarsetAt(i);
+
+ unsigned long int col = 0;
+ bool final = false;
+ while (true) {
+ col = var_row.scan(col);
+ if (col == ULONG_MAX) break;
+
+ const Var var = col_to_var_original[col];
+ assert(var < solver.nVars());
+
+ if (solver.assigns[var] == l_True) {
+ assert(!mat_row[col]);
+ assert(m.col_to_var[col] == unassigned_var);
+ assert(m.var_is_set[var]);
+ final = !final;
+ } else if (solver.assigns[var] == l_False) {
+ assert(!mat_row[col]);
+ assert(m.col_to_var[col] == unassigned_var);
+ assert(m.var_is_set[var]);
+ } else if (solver.assigns[var] == l_Undef) {
+ assert(m.col_to_var[col] != unassigned_var);
+ assert(!m.var_is_set[var]);
+ assert(mat_row[col]);
+ } else assert(false);
+
+ col++;
+ }
+ if ((final^!mat_row.is_true()) != !var_row.is_true()) {
+ cout << "problem with row:"; print_matrix_row_with_assigns(var_row); cout << endl;
+ assert(false);
+ }
+ }
+}
+
+const void Gaussian::check_first_one_in_row(matrixset& m, const uint j)
+{
+ if (j) {
+ uint16_t until2 = std::min(m.last_one_in_col[m.least_column_changed] - 1, (int)m.num_rows);
+ if (j-1 > m.first_one_in_row[m.num_rows-1]) {
+ until2 = m.num_rows;
+ #ifdef VERBOSE_DEBUG
+ cout << "j-1 > m.first_one_in_row[m.num_rows-1]" << "j:" << j << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl;
+ #endif
+ }
+ for (uint i2 = 0; i2 != until2; i2++) {
+ #ifdef VERBOSE_DEBUG
+ cout << endl << "row " << i2 << " (num rows:" << m.num_rows << ")" << endl;
+ cout << m.matrix.getMatrixAt(i2) << endl;
+ cout << " m.first_one_in_row[m.num_rows-1]:" << m.first_one_in_row[m.num_rows-1] << endl;
+ cout << "first_one_in_row:" << m.first_one_in_row[i2] << endl;
+ cout << "num_cols:" << m.num_cols << endl;
+ cout << "popcnt:" << m.matrix.getMatrixAt(i2).popcnt() << endl;
+ cout << "popcnt_is_one():" << m.matrix.getMatrixAt(i2).popcnt_is_one() << endl;
+ cout << "popcnt_is_one("<< m.first_one_in_row[i2] <<"): " << m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2]) << endl;
+ #endif
+
+ for (uint i3 = 0; i3 < m.first_one_in_row[i2]; i3++) {
+ assert(m.matrix.getMatrixAt(i2)[i3] == 0);
+ }
+ assert(m.matrix.getMatrixAt(i2)[m.first_one_in_row[i2]]);
+ assert(m.matrix.getMatrixAt(i2).popcnt_is_one() ==
+ m.matrix.getMatrixAt(i2).popcnt_is_one(m.first_one_in_row[i2]));
+ }
+ }
+}
+
+//old functions
+
+/*void Gaussian::update_matrix_by_row(matrixset& m) const
+{
+#ifdef VERBOSE_DEBUG
+ cout << "Updating matrix." << endl;
+ uint num_updated = 0;
+#endif
+#ifdef DEBUG_GAUSS
+ assert(nothing_to_propagate(cur_matrixset));
+#endif
+
+ mpz_class toclear, tocount;
+ uint last_col = 0;
+
+ for (uint col = 0; col < m.num_cols; col ++) {
+ Var var = m.col_to_var[col];
+
+ if (var != UINT_MAX && !solver.assigns[var].isUndef()) {
+ toclear.setBit(col);
+ if (solver.assigns[var].getBool()) tocount.setBit(col);
+
+#ifdef DEBUG_GAUSS
+ assert(m.var_to_col[var] < UINT_MAX-1);
+#endif
+ last_col = col;
+ m.least_column_changed = std::min(m.least_column_changed, (int)col);
+
+ m.removeable_cols++;
+ m.col_to_var[col] = UINT_MAX;
+ m.var_to_col[var] = UINT_MAX-1;
+#ifdef VERBOSE_DEBUG
+ num_updated++;
+#endif
+ }
+ }
+
+ toclear.invert();
+ mpz_class tmp;
+ mpz_class* this_row = &m.matrix[0];
+ for(uint i = 0, until = std::min(m.num_rows, m.last_one_in_col[last_col]+1); i < until; i++, this_row++) {
+ mpz_class& r = *this_row;
+ mpz_and(tmp.get_mp(), tocount.get_mp(), r.get_mp());
+ r.invert_is_true(tmp.popcnt() % 2);
+ r &= toclear;
+}
+
+#ifdef VERBOSE_DEBUG
+ cout << "Updated " << num_updated << " matrix cols. Could remove " << m.removeable_cols << " cols " <<endl;
+#endif
+}*/
+
+/*void Gaussian::update_matrix_by_col(matrixset& m, const uint last_level) const
+{
+#ifdef VERBOSE_DEBUG
+ cout << "Updating matrix." << endl;
+ uint num_updated = 0;
+#endif
+#ifdef DEBUG_GAUSS
+ assert(nothing_to_propagate(cur_matrixset));
+#endif
+
+ for (int level = solver.trail.size()-1; level >= last_level; level--){
+ Var var = solver.trail[level].var();
+ const uint col = m.var_to_col[var];
+ if ( col < UINT_MAX-1) {
+ update_matrix_col(m, var, col);
+#ifdef VERBOSE_DEBUG
+ num_updated++;
+#endif
+ }
+ }
+
+#ifdef VERBOSE_DEBUG
+ cout << "Updated " << num_updated << " matrix cols. Could remove " << m.removeable_cols << " cols (out of " << m.num_cols << " )" <<endl;
+#endif
+}*/
+
+}; //NAMESPACE MINISAT
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef GAUSSIAN_H
+#define GAUSSIAN_H
+
+#include <vector>
+#include <limits>
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include "SolverTypes.h"
+#include "Solver.h"
+#include "GaussianConfig.h"
+#include "PackedMatrix.h"
+#include "BitArray.h"
+
+//#define VERBOSE_DEBUG
+//#define DEBUG_GAUSS
+
+#ifdef VERBOSE_DEBUG
+using std::vector;
+using std::cout;
+using std::endl;
+#endif
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class Clause;
+
+class Gaussian
+{
+public:
+ Gaussian(Solver& solver, const GaussianConfig& config, const uint matrix_no, const vector<XorClause*>& xorclauses);
+ ~Gaussian();
+
+ const bool full_init();
+ llbool find_truths(vec<Lit>& learnt_clause, int& conflictC);
+
+ //statistics
+ void print_stats() const;
+ void print_matrix_stats() const;
+ const uint get_called() const;
+ const uint get_useful_prop() const;
+ const uint get_useful_confl() const;
+ const bool get_disabled() const;
+ const uint32_t get_unit_truths() const;
+ void set_disabled(const bool toset);
+
+ //functions used throughout the Solver
+ void canceling(const uint sublevel);
+
+protected:
+ Solver& solver;
+
+ //Gauss high-level configuration
+ const GaussianConfig& config;
+ const uint matrix_no;
+ vector<XorClause*> xorclauses;
+
+ enum gaussian_ret {conflict, unit_conflict, propagation, unit_propagation, nothing};
+ gaussian_ret gaussian(Clause*& confl);
+
+ vector<Var> col_to_var_original; //Matches columns to variables
+ BitArray var_is_in; //variable is part of the the matrix. var_is_in's size is _minimal_ so you should check whether var_is_in.getSize() < var before issuing var_is_in[var]
+ uint badlevel;
+
+ class matrixset
+ {
+ public:
+ PackedMatrix matrix; // The matrix, updated to reflect variable assignements
+ BitArray var_is_set;
+ vector<Var> col_to_var; // col_to_var[COL] tells which variable is at a given column in the matrix. Gives unassigned_var if the COL has been zeroed (i.e. the variable assigned)
+ uint16_t num_rows; // number of active rows in the matrix. Unactive rows are rows that contain only zeros (and if they are conflicting, then the conflict has been treated)
+ uint num_cols; // number of active columns in the matrix. The columns at the end that have all be zeroed are no longer active
+ int least_column_changed; // when updating the matrix, this value contains the smallest column number that has been updated (Gauss elim. can start from here instead of from column 0)
+ vector<uint16_t> last_one_in_col; //last_one_in_col[COL] tells the last row+1 that has a '1' in that column. Used to reduce the burden of Gauss elim. (it only needs to look until that row)
+ vector<uint16_t> first_one_in_row;
+ uint removeable_cols; // the number of columns that have been zeroed out (i.e. assigned)
+ };
+
+ //Saved states
+ vector<matrixset> matrix_sets; // The matrixsets for depths 'decision_from' + 0, 'decision_from' + only_nth_gaussian_save, 'decision_from' + 2*only_nth_gaussian_save, ... 'decision_from' + 'decision_until'.
+ matrixset cur_matrixset; // The current matrixset, i.e. the one we are working on, or the last one we worked on
+
+ //Varibales to keep Gauss state
+ bool messed_matrix_vars_since_reversal;
+ int gauss_last_level;
+ vector<pair<Clause*, uint> > clauses_toclear;
+ bool disabled; // Gauss is disabled
+
+ //State of current elimnation
+ vec<uint> propagatable_rows; //used to store which rows were deemed propagatable during elimination
+ vector<unsigned char> changed_rows; //used to store which rows were deemed propagatable during elimination
+
+ //Statistics
+ uint useful_prop; //how many times Gauss gave propagation as a result
+ uint useful_confl; //how many times Gauss gave conflict as a result
+ uint called; //how many times called the Gauss
+ uint32_t unit_truths; //how many unitary (i.e. decisionLevel 0) truths have been found
+
+ //gauss init functions
+ void init(); // Initalise gauss state
+ void fill_matrix(matrixset& origMat); // Fills the origMat matrix
+ uint select_columnorder(vector<uint16_t>& var_to_col, matrixset& origMat); // Fills var_to_col and col_to_var of the origMat matrix.
+
+ //Main function
+ uint eliminate(matrixset& matrix, uint& conflict_row); //does the actual gaussian elimination
+
+ //matrix update functions
+ void update_matrix_col(matrixset& matrix, const Var x, const uint col); // Update one matrix column
+ void update_matrix_by_col_all(matrixset& m); // Update all columns, column-by-column (and not row-by-row)
+ void set_matrixset_to_cur(); // Save the current matrixset, the cur_matrixset to matrix_sets
+ //void update_matrix_by_row(matrixset& matrix) const;
+ //void update_matrix_by_col(matrixset& matrix, const uint last_level) const;
+
+ //conflict&propagation handling
+ gaussian_ret handle_matrix_prop_and_confl(matrixset& m, uint row, Clause*& confl);
+ void analyse_confl(const matrixset& m, const uint row, int32_t& maxlevel, uint& size, uint& best_row) const; // analyse conflcit to find the best conflict. Gets & returns the best one in 'maxlevel', 'size' and 'best row' (these are all UINT_MAX when calling this function first, i.e. when there is no other possible conflict to compare to the new in 'row')
+ gaussian_ret handle_matrix_confl(Clause*& confl, const matrixset& m, const uint size, const uint maxlevel, const uint best_row);
+ gaussian_ret handle_matrix_prop(matrixset& m, const uint row); // Handle matrix propagation at row 'row'
+ vec<Lit> tmp_clause;
+
+ //propagation&conflict handling
+ void cancel_until_sublevel(const uint until_sublevel); // cancels until sublevel 'until_sublevel'. The var 'until_sublevel' must NOT go over the current level. I.e. this function is ONLY for moving inside the current level
+ uint find_sublevel(const Var v) const; // find the sublevel (i.e. trail[X]) of a given variable
+
+ //helper functions
+ bool at_first_init() const;
+ bool should_init() const;
+ bool should_check_gauss(const uint decisionlevel, const uint starts) const;
+ void disable_if_necessary();
+ void reset_stats();
+ void update_last_one_in_col(matrixset& m);
+
+private:
+
+ //debug functions
+ bool check_no_conflict(matrixset& m) const; // Are there any conflicts that the matrixset 'm' causes?
+ const bool nothing_to_propagate(matrixset& m) const; // Are there any conflicts of propagations that matrixset 'm' clauses?
+ template<class T>
+ void print_matrix_row(const T& row) const; // Print matrix row 'row'
+ template<class T>
+ void print_matrix_row_with_assigns(const T& row) const;
+ void check_matrix_against_varset(PackedMatrix& matrix,const matrixset& m) const;
+ const bool check_last_one_in_cols(matrixset& m) const;
+ const void check_first_one_in_row(matrixset& m, const uint j);
+ void print_matrix(matrixset& m) const;
+ void print_last_one_in_cols(matrixset& m) const;
+ static const string lbool_to_string(const lbool toprint);
+};
+
+inline bool Gaussian::should_init() const
+{
+ return (config.decision_until > 0);
+}
+
+inline bool Gaussian::should_check_gauss(const uint decisionlevel, const uint starts) const
+{
+ return (!disabled
+ && decisionlevel < config.decision_until);
+}
+
+inline void Gaussian::canceling(const uint sublevel)
+{
+ if (disabled)
+ return;
+ uint a = 0;
+ for (int i = clauses_toclear.size()-1; i >= 0 && clauses_toclear[i].second > sublevel; i--) {
+ clauseFree(clauses_toclear[i].first);
+ a++;
+ }
+ clauses_toclear.resize(clauses_toclear.size()-a);
+
+ if (messed_matrix_vars_since_reversal)
+ return;
+ int c = std::min((int)gauss_last_level, (int)(solver.trail.size())-1);
+ for (; c >= (int)sublevel; c--) {
+ Var var = solver.trail[c].var();
+ if (var < var_is_in.getSize()
+ && var_is_in[var]
+ && cur_matrixset.var_is_set[var]) {
+ messed_matrix_vars_since_reversal = true;
+ return;
+ }
+ }
+}
+
+inline const uint32_t Gaussian::get_unit_truths() const
+{
+ return unit_truths;
+}
+
+inline const uint Gaussian::get_called() const
+{
+ return called;
+}
+
+inline const uint Gaussian::get_useful_prop() const
+{
+ return useful_prop;
+}
+
+inline const uint Gaussian::get_useful_confl() const
+{
+ return useful_confl;
+}
+
+inline const bool Gaussian::get_disabled() const
+{
+ return disabled;
+}
+
+inline void Gaussian::set_disabled(const bool toset)
+{
+ disabled = toset;
+}
+
+std::ostream& operator << (std::ostream& os, const vec<Lit>& v);
+
+}; //NAMESPACE MINISAT
+
+#endif //GAUSSIAN_H
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef GAUSSIANCONFIG_H
+#define GAUSSIANCONFIG_H
+
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include "PackedRow.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class GaussianConfig
+{
+ public:
+
+ GaussianConfig() :
+ only_nth_gauss_save(2)
+ , decision_until(0)
+ , dontDisable(false)
+ , noMatrixFind(false)
+ , orderCols(true)
+ , iterativeReduce(true)
+ , maxMatrixRows(1000)
+ , minMatrixRows(20)
+ {
+ }
+
+ //tuneable gauss parameters
+ uint only_nth_gauss_save; //save only every n-th gauss matrix
+ uint decision_until; //do Gauss until this level
+ bool dontDisable; //If activated, gauss elimination is never disabled
+ bool noMatrixFind; //Put all xor-s into one matrix, don't find matrixes
+ bool orderCols; //Order columns according to activity
+ bool iterativeReduce; //Don't minimise matrix work
+ uint32_t maxMatrixRows; //The maximum matrix size -- no. of rows
+ uint32_t minMatrixRows; //The minimum matrix size -- no. of rows
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //GAUSSIANCONFIG_H
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+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 <time.h>
+#include <cstring>
+#include <algorithm>
+#include <vector>
+#include <iostream>
+#include <iomanip>
+#include <fstream>
+#include <sstream>
+#include <limits>
+using std::cout;
+using std::endl;
+using std::ofstream;
+
+#include "Logger.h"
+#include "SolverTypes.h"
+#include "Solver.h"
+#include "Gaussian.h"
+
+#define FST_WIDTH 10
+#define SND_WIDTH 35
+#define TRD_WIDTH 10
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+Logger::Logger(int& _verbosity) :
+ proof_graph_on(false)
+ , mini_proof(false)
+ , statistics_on(false)
+
+ , max_print_lines(20)
+ , uniqueid(1)
+
+ , proof(NULL)
+
+ , sum_conflict_depths(0)
+ , no_conflicts(0)
+ , no_decisions(0)
+ , no_propagations(0)
+ , sum_decisions_on_branches(0)
+ , sum_propagations_on_branches(0)
+
+ , verbosity(_verbosity)
+ , begin_called(false)
+ , proofStarts(0)
+{
+ runid /= 10;
+ runid = time(NULL) % 10000;
+ if (verbosity >= 1) printf("c RunID is: #%d\n",runid);
+}
+
+void Logger::setSolver(const Solver* _s)
+{
+ S = _s;
+}
+
+// Adds a new variable to the knowledge of the logger
+void Logger::new_var(const Var var)
+{
+ if (!statistics_on && !proof_graph_on)
+ return;
+
+ if (varnames.size() <= var) {
+ varnames.resize(var+1, "Noname");
+ times_var_propagated.resize(var+1, 0);
+ times_var_guessed.resize(var+1, 0);
+ depths_of_assigns_for_var.resize(var+1);
+ depths_of_assigns_unit.resize(var+1, false);
+ }
+}
+
+// Resizes the groupnames and other, related vectors to accomodate for a new group
+void Logger::new_group(const uint group)
+{
+ if (groupnames.size() <= group) {
+ groupnames.resize(group+1, "Noname");
+ times_group_caused_conflict.resize(group+1, 0);
+ times_group_caused_propagation.resize(group+1, 0);
+ depths_of_propagations_for_group.resize(group+1);
+ depths_of_propagations_unit.resize(group+1, false);
+ depths_of_conflicts_for_group.resize(group+1);
+ }
+}
+
+string Logger::cut_name_to_size(const string& name) const
+{
+ string ret = name;
+ uint len = name.length();
+ while(len > 0 && (name[len-1] == ' ' || name[len-1] == 0x0A || name[len-1] == 0x0D)) {
+ ret.resize(len-1);
+ len--;
+ }
+
+ if (len > SND_WIDTH-3) {
+ ret[SND_WIDTH-3] = '\0';
+ ret[SND_WIDTH-4] = '.';
+ ret[SND_WIDTH-5] = '.';
+ }
+
+ return ret;
+}
+
+// Adds the new clause group's name to the information stored
+void Logger::set_group_name(const uint group, const char* name_tmp)
+{
+ if (!statistics_on && !proof_graph_on)
+ return;
+
+ string name;
+ if (name_tmp == NULL) return;
+ else name = name_tmp;
+
+ set_group_name(group, name);
+}
+
+void Logger::set_group_name(const uint group, string& name)
+{
+ new_group(group);
+
+ if (name == "Noname") return;
+
+ if (groupnames[group] == "Noname") {
+ groupnames[group] = name;
+ } else if (groupnames[group] != name) {
+ std::cout << "Error! Group no. " << group << "has been named twice. First, as '" << groupnames[group] << "', then second as '" << name << "'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line" << std::endl;
+ exit(-1);
+ }
+}
+
+string Logger::get_group_name(const uint group) const
+{
+ assert(group < groupnames.size());
+ return groupnames[group];
+}
+
+string Logger::get_var_name(const Var var) const
+{
+ if (var >= varnames.size()) return "unknown";
+ return varnames[var];
+}
+
+// sets the variable's name
+void Logger::set_variable_name(const uint var, char* name_tmp)
+{
+ if (!statistics_on && !proof_graph_on)
+ return;
+
+ new_var(var);
+
+ string name;
+ if (name_tmp == NULL)
+ name = "";
+ else
+ name = name_tmp;
+
+ if (varnames[var] == "Noname") {
+ varnames[var] = name;
+ } else if (varnames[var] != name) {
+ printf("Error! Variable no. %d has been named twice. First, as '%s', then second as '%s'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line\n", var+1, varnames[var].c_str(), name.c_str());
+ exit(-1);
+ }
+}
+
+void Logger::first_begin()
+{
+ if (begin_called)
+ return;
+
+ begin();
+}
+
+void Logger::begin()
+{
+ begin_called = true;
+ if (proof_graph_on) {
+ std::stringstream filename;
+ filename << "proofs/" << runid << "-proof" << proofStarts++ << "-" << S->starts << ".dot";
+
+ if (S->starts == 0)
+ history.push_back(uniqueid);
+ else {
+ if (mini_proof)
+ history.resize(S->decisionLevel()+1);
+ else
+ history.resize(S->trail.size()+1);
+ }
+
+ proof = fopen(filename.str().c_str(),"w");
+ if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename.str().c_str()), exit(-1);
+ fprintf(proof, "digraph G {\n");
+ fprintf(proof,"node%d [shape=circle, label=\"BEGIN\", root];\n", history[history.size()-1]);
+ }
+
+ if (statistics_on)
+ reset_statistics();
+}
+
+// For noting conflicts. Updates the proof graph and the statistics.
+template<class T>
+void Logger::conflict(const confl_type type, const uint goback_level, const uint group, const T& learnt_clause)
+{
+ first_begin();
+ assert(!(proof == NULL && proof_graph_on));
+
+ const uint goback_sublevel = S->trail_lim[goback_level];
+
+ if (proof_graph_on) {
+ uniqueid++;
+ fprintf(proof,"node%d [shape=polygon,sides=5,label=\"",uniqueid);
+
+ if (!mini_proof) {
+ for (uint32_t i = 0; i != learnt_clause.size(); i++) {
+ if (learnt_clause[i].sign()) fprintf(proof,"-");
+ int myvar = learnt_clause[i].var();
+ if (varnames[myvar] != "Noname")
+ fprintf(proof,"%s\\n",varnames[myvar].c_str());
+ else
+ fprintf(proof,"Var: %d\\n",myvar);
+ }
+ }
+ fprintf(proof,"\"];\n");
+
+ fprintf(proof,"node%d -> node%d [label=\"",history[history.size()-1],uniqueid);
+ if (type == gauss_confl_type)
+ fprintf(proof,"Gauss\",style=bold");
+ else
+ fprintf(proof,"%s\"", groupnames[group].c_str());
+ fprintf(proof,"];\n");
+
+ if (!mini_proof)
+ history.resize(goback_sublevel+1);
+ else
+ history.resize(goback_level+1);
+ fprintf(proof,"node%d -> node%d [style=dotted];\n",uniqueid,history[history.size()-1]);
+ }
+
+ if (statistics_on) {
+ times_group_caused_conflict[group]++;
+ depths_of_conflicts_for_group[group].sum += S->decisionLevel();
+ depths_of_conflicts_for_group[group].num ++;
+
+ no_conflicts++;
+ sum_conflict_depths += S->trail.size() - S->trail_lim[0];
+ sum_decisions_on_branches += S->decisionLevel();
+ sum_propagations_on_branches += S->trail.size() - S->trail_lim[0] - S->decisionLevel();
+
+ if (branch_depth_distrib.size() <= S->decisionLevel())
+ branch_depth_distrib.resize(S->decisionLevel()+1, 0);
+ branch_depth_distrib[S->decisionLevel()]++;
+ }
+}
+
+template void Logger::conflict(const confl_type type, const uint goback_level, const uint group, const Clause& learnt_clause);
+
+template void Logger::conflict(const confl_type type, const uint goback_level, const uint group, const vec<Lit>& learnt_clause);
+
+// Propagating a literal. Type of literal and the (learned clause's)/(propagating clause's)/(etc) group must be given. Updates the proof graph and the statistics. note: the meaning of the variable 'group' depends on the type
+void Logger::propagation(const Lit lit, Clause* c)
+{
+ first_begin();
+ assert(!(proof == NULL && proof_graph_on));
+
+ uint group;
+ prop_type type;
+ if (c == NULL) {
+ if (S->decisionLevel() == 0)
+ type = add_clause_type;
+ else
+ type = guess_type;
+ group = std::numeric_limits<uint>::max();
+ } else {
+ type = simple_propagation_type;
+ group = c->getGroup();
+ }
+
+ //graph
+ if (proof_graph_on && (!mini_proof || type == guess_type)) {
+ uniqueid++;
+
+ fprintf(proof,"node%d [shape=box, label=\"",uniqueid);;
+ if (lit.sign())
+ fprintf(proof,"-");
+ if (varnames[lit.var()] != "Noname")
+ fprintf(proof,"%s\"];\n",varnames[lit.var()].c_str());
+ else
+ fprintf(proof,"Var: %d\"];\n",lit.var());
+
+ fprintf(proof,"node%d -> node%d [label=\"",history[history.size()-1],uniqueid);
+
+ switch (type) {
+ case simple_propagation_type:
+ fprintf(proof,"%s\"];\n", groupnames[group].c_str());
+ break;
+
+ case add_clause_type:
+ fprintf(proof,"red. from clause\"];\n");
+ break;
+
+ case guess_type:
+ fprintf(proof,"guess\",style=bold];\n");
+ break;
+ }
+ history.push_back(uniqueid);
+ }
+
+ if (statistics_on) {
+ switch (type) {
+ case simple_propagation_type:
+ depths_of_propagations_for_group[group].sum += S->decisionLevel();
+ depths_of_propagations_for_group[group].num ++;
+ if (S->decisionLevel() == 0) depths_of_propagations_unit[group] = true;
+ times_group_caused_propagation[group]++;
+ case add_clause_type:
+ no_propagations++;
+ times_var_propagated[lit.var()]++;
+ depths_of_assigns_for_var[lit.var()].sum += S->decisionLevel();
+ depths_of_assigns_for_var[lit.var()].num ++;
+ if (S->decisionLevel() == 0) depths_of_assigns_unit[lit.var()] = true;
+ break;
+ case guess_type:
+ no_decisions++;
+ times_var_guessed[lit.var()]++;
+
+ depths_of_assigns_for_var[lit.var()].sum += S->decisionLevel();
+ depths_of_assigns_for_var[lit.var()].num ++;
+ break;
+ }
+ }
+}
+
+// Ending of a restart iteration
+void Logger::end(const finish_type finish)
+{
+ first_begin();
+ assert(!(proof == NULL && proof_graph_on));
+
+ if (proof_graph_on) {
+ uniqueid++;
+ switch (finish) {
+ case model_found:
+ fprintf(proof,"node%d [shape=doublecircle, label=\"MODEL\"];\n",uniqueid);
+ break;
+ case unsat_model_found:
+ fprintf(proof,"node%d [shape=doublecircle, label=\"UNSAT\"];\n",uniqueid);
+ break;
+ case restarting:
+ fprintf(proof,"node%d [shape=doublecircle, label=\"Re-starting\\nsearch\"];\n",uniqueid);
+ break;
+ }
+
+ fprintf(proof,"node%d -> node%d;\n",history[history.size()-1],uniqueid);
+ fprintf(proof,"}\n");
+ history.push_back(uniqueid);
+
+ proof = (FILE*)fclose(proof);
+ assert(proof == NULL);
+ }
+
+ if (statistics_on) {
+ printstats();
+ if (finish == restarting)
+ reset_statistics();
+ }
+
+ if (model_found || unsat_model_found)
+ begin_called = false;
+}
+
+void Logger::print_footer() const
+{
+ cout << "+" << std::setfill('-') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << "-" << std::setfill(' ') << "+" << endl;
+}
+
+void Logger::print_assign_var_order() const
+{
+ vector<pair<double, uint> > prop_ordered;
+ for (uint i = 0; i < depths_of_assigns_for_var.size(); i++) {
+ double avg = (double)depths_of_assigns_for_var[i].sum
+ /(double)depths_of_assigns_for_var[i].num;
+ if (depths_of_assigns_for_var[i].num > 0 && !depths_of_assigns_unit[i])
+ prop_ordered.push_back(std::make_pair(avg, i));
+ }
+
+ if (!prop_ordered.empty()) {
+ print_footer();
+ print_simple_line(" Variables are assigned in the following order");
+ print_simple_line(" (unitary clauses not shown)");
+ print_header("var", "var name", "avg order");
+ std::sort(prop_ordered.begin(), prop_ordered.end());
+ print_vars(prop_ordered);
+ }
+}
+
+void Logger::print_prop_order() const
+{
+ vector<pair<double, uint> > prop_ordered;
+ for (uint i = 0; i < depths_of_propagations_for_group.size(); i++) {
+ double avg = (double)depths_of_propagations_for_group[i].sum
+ /(double)depths_of_propagations_for_group[i].num;
+ if (depths_of_propagations_for_group[i].num > 0 && !depths_of_propagations_unit[i])
+ prop_ordered.push_back(std::make_pair(avg, i));
+ }
+
+ if (!prop_ordered.empty()) {
+ print_footer();
+ print_simple_line(" Propagation depth order of clause groups");
+ print_simple_line(" (unitary clauses not shown)");
+ print_header("group", "group name", "avg order");
+ std::sort(prop_ordered.begin(), prop_ordered.end());
+ print_groups(prop_ordered);
+ }
+}
+
+void Logger::print_confl_order() const
+{
+ vector<pair<double, uint> > confl_ordered;
+ for (uint i = 0; i < depths_of_conflicts_for_group.size(); i++) {
+ double avg = (double)depths_of_conflicts_for_group[i].sum
+ /(double)depths_of_conflicts_for_group[i].num;
+ if (depths_of_conflicts_for_group[i].num > 0)
+ confl_ordered.push_back(std::make_pair(avg, i));
+ }
+
+ if (!confl_ordered.empty()) {
+ print_footer();
+ print_simple_line(" Avg. conflict depth order of clause groups");
+ print_header("groupno", "group name", "avg. depth");
+ std::sort(confl_ordered.begin(), confl_ordered.end());
+ print_groups(confl_ordered);
+ }
+}
+
+
+void Logger::print_times_var_guessed() const
+{
+ vector<pair<uint, uint> > times_var_ordered;
+ for (uint32_t i = 0; i != varnames.size(); i++) if (times_var_guessed[i] > 0)
+ times_var_ordered.push_back(std::make_pair(times_var_guessed[i], i));
+
+ if (!times_var_ordered.empty()) {
+ print_footer();
+ print_simple_line(" No. times variable branched on");
+ print_header("var", "var name", "no. times");
+ std::sort(times_var_ordered.rbegin(), times_var_ordered.rend());
+ print_vars(times_var_ordered);
+ }
+}
+
+void Logger::print_times_group_caused_propagation() const
+{
+ vector<pair<uint, uint> > props_group_ordered;
+ for (uint i = 0; i < times_group_caused_propagation.size(); i++)
+ if (times_group_caused_propagation[i] > 0)
+ props_group_ordered.push_back(std::make_pair(times_group_caused_propagation[i], i));
+
+ if (!props_group_ordered.empty()) {
+ print_footer();
+ print_simple_line(" No. propagations made by clause groups");
+ print_header("group", "group name", "no. props");
+ std::sort(props_group_ordered.rbegin(),props_group_ordered.rend());
+ print_groups(props_group_ordered);
+ }
+}
+
+void Logger::print_times_group_caused_conflict() const
+{
+ vector<pair<uint, uint> > confls_group_ordered;
+ for (uint i = 0; i < times_group_caused_conflict.size(); i++)
+ if (times_group_caused_conflict[i] > 0)
+ confls_group_ordered.push_back(std::make_pair(times_group_caused_conflict[i], i));
+
+ if (!confls_group_ordered.empty()) {
+ print_footer();
+ print_simple_line(" No. conflicts made by clause groups");
+ print_header("group", "group name", "no. confl");
+ std::sort(confls_group_ordered.rbegin(), confls_group_ordered.rend());
+ print_groups(confls_group_ordered);
+ }
+}
+
+template<class T>
+void Logger::print_line(const uint& number, const string& name, const T& value) const
+{
+ cout << "|" << std::setw(FST_WIDTH) << number << " " << std::setw(SND_WIDTH) << name << " " << std::setw(TRD_WIDTH) << value << "|" << endl;
+}
+
+void Logger::print_header(const string& first, const string& second, const string& third) const
+{
+ cout << "|" << std::setw(FST_WIDTH) << first << " " << std::setw(SND_WIDTH) << second << " " << std::setw(TRD_WIDTH) << third << "|" << endl;
+ print_footer();
+}
+
+void Logger::print_groups(const vector<pair<double, uint> >& to_print) const
+{
+ uint i = 0;
+ typedef vector<pair<double, uint> >::const_iterator myiterator;
+ for (myiterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) {
+ print_line(it->second+1, cut_name_to_size(groupnames[it->second]), it->first);
+ }
+ print_footer();
+}
+
+void Logger::print_groups(const vector<pair<uint, uint> >& to_print) const
+{
+ uint i = 0;
+ typedef vector<pair<uint, uint> >::const_iterator myiterator;
+ for (myiterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) {
+ print_line(it->second+1, cut_name_to_size(groupnames[it->second]), it->first);
+ }
+ print_footer();
+}
+
+void Logger::print_vars(const vector<pair<double, uint> >& to_print) const
+{
+ uint i = 0;
+ for (vector<pair<double, uint> >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++)
+ print_line(it->second+1, cut_name_to_size(varnames[it->second]), it->first);
+
+ print_footer();
+}
+
+void Logger::print_vars(const vector<pair<uint, uint> >& to_print) const
+{
+ uint i = 0;
+ for (vector<pair<uint, uint> >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) {
+ print_line(it->second+1, cut_name_to_size(varnames[it->second]), it->first);
+ }
+
+ print_footer();
+}
+
+template<class T>
+void Logger::print_line(const string& str, const T& num) const
+{
+ cout << "|" << std::setw(FST_WIDTH+SND_WIDTH+4) << str << std::setw(TRD_WIDTH) << num << "|" << endl;
+}
+
+void Logger::print_simple_line(const string& str) const
+{
+ cout << "|" << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << str << "|" << endl;
+}
+
+void Logger::print_center_line(const string& str) const
+{
+ uint middle = (FST_WIDTH+SND_WIDTH+TRD_WIDTH+4-str.size())/2;
+ int rest = FST_WIDTH+SND_WIDTH+TRD_WIDTH+4-middle*2-str.size();
+ cout << "|" << std::setw(middle) << " " << str << std::setw(middle + rest) << " " << "|" << endl;
+}
+
+void Logger::print_branch_depth_distrib() const
+{
+ //cout << "--- Branch depth stats ---" << endl;
+
+ const uint range = 20;
+ map<uint, uint> range_stat;
+
+ uint i = 0;
+ for (vector<uint>::const_iterator it = branch_depth_distrib.begin(); it != branch_depth_distrib.end(); it++, i++) {
+ range_stat[i/range] += *it;
+ }
+
+ print_footer();
+ print_simple_line(" No. search branches with branch depth between");
+ print_line("Branch depth between", "no. br.-s");
+ print_footer();
+
+ std::stringstream ss;
+ ss << "branch_depths/branch_depth_file" << runid << "-" << S->starts << ".txt";
+ ofstream branch_depth_file;
+ branch_depth_file.open(ss.str().c_str());
+ i = 0;
+
+ for (map<uint, uint>::iterator it = range_stat.begin(); it != range_stat.end(); it++, i++) {
+ std::stringstream ss2;
+ ss2 << it->first*range << " - " << it->first*range + range-1;
+ print_line(ss2.str(), it->second);
+
+ if (branch_depth_file.is_open()) {
+ branch_depth_file << i << "\t" << it->second << "\t";
+ if (i % 5 == 0)
+ branch_depth_file << "\"" << it->first*range << "\"";
+ else
+ branch_depth_file << "\"\"";
+ branch_depth_file << endl;
+ }
+ }
+ if (branch_depth_file.is_open())
+ branch_depth_file.close();
+ print_footer();
+
+}
+
+void Logger::print_learnt_clause_distrib() const
+{
+ map<uint, uint> learnt_sizes;
+ const vec<Clause*>& learnts = S->get_learnts();
+
+ uint maximum = 0;
+
+ for (uint i = 0; i < learnts.size(); i++)
+ {
+ uint size = learnts[i]->size();
+ maximum = std::max(maximum, size);
+
+ map<uint, uint>::iterator it = learnt_sizes.find(size);
+ if (it == learnt_sizes.end())
+ learnt_sizes[size] = 1;
+ else
+ it->second++;
+ }
+
+ learnt_sizes[0] = S->get_unitary_learnts_num();
+
+ uint slice = (maximum+1)/max_print_lines + (bool)((maximum+1)%max_print_lines);
+
+ print_footer();
+ print_simple_line(" Learnt clause length distribution");
+ print_line("Length between", "no. cl.");
+ print_footer();
+
+ uint until = slice;
+ uint from = 0;
+ while(until < maximum+1) {
+ std::stringstream ss2;
+ ss2 << from << " - " << until-1;
+
+ uint sum = 0;
+ for (; from < until; from++) {
+ map<uint, uint>::const_iterator it = learnt_sizes.find(from);
+ if (it != learnt_sizes.end())
+ sum += it->second;
+ }
+
+ print_line(ss2.str(), sum);
+
+ until += slice;
+ }
+
+ print_footer();
+
+ print_leearnt_clause_graph_distrib(maximum, learnt_sizes);
+}
+
+void Logger::print_leearnt_clause_graph_distrib(const uint maximum, const map<uint, uint>& learnt_sizes) const
+{
+ uint no_slices = FST_WIDTH + SND_WIDTH + TRD_WIDTH + 4-3;
+ uint slice = (maximum+1)/no_slices + (bool)((maximum+1)%no_slices);
+ uint until = slice;
+ uint from = 0;
+ vector<uint> slices;
+ uint hmax = 0;
+ while(until < maximum+1) {
+ uint sum = 0;
+ for (; from < until; from++) {
+ map<uint, uint>::const_iterator it = learnt_sizes.find(from);
+ if (it != learnt_sizes.end())
+ sum += it->second;
+ }
+ slices.push_back(sum);
+ until += slice;
+ hmax = std::max(hmax, sum);
+ }
+ slices.resize(no_slices, 0);
+
+ uint height = max_print_lines;
+ uint hslice = (hmax+1)/height + (bool)((hmax+1)%height);
+ if (hslice == 0) return;
+
+ print_simple_line(" Learnt clause distribution in graph form");
+ print_footer();
+ string yaxis = "Number";
+ uint middle = (height-yaxis.size())/2;
+
+ for (int i = height-1; i > 0; i--) {
+ cout << "| ";
+ if (height-1-i >= middle && height-1-i-middle < yaxis.size())
+ cout << yaxis[height-1-i-middle] << " ";
+ else
+ cout << " ";
+ for (uint i2 = 0; i2 != no_slices; i2++) {
+ if (slices[i2]/hslice >= (uint)i) cout << "+";
+ else cout << " ";
+ }
+ cout << "|" << endl;
+ }
+ print_center_line(" Learnt clause size");
+ print_footer();
+}
+
+void Logger::print_general_stats() const
+{
+ print_footer();
+ print_simple_line(" Standard MiniSat stats -- for all restarts until now");
+ print_footer();
+ print_line("Restart number", S->starts);
+ print_line("Number of conflicts", S->conflicts);
+ print_line("Number of decisions", S->decisions);
+ print_line("Number of variables", S->order_heap.size());
+ print_line("Number of clauses", S->nClauses());
+ print_line("Number of literals in clauses",S->clauses_literals);
+ print_line("Avg. literals per learnt clause",(double)S->learnts_literals/(double)S->nLearnts());
+ print_line("Progress estimate (%):", S->progress_estimate*100.0);
+ print_line("All unitary learnts until now", S->get_unitary_learnts_num());
+ print_footer();
+}
+
+void Logger::print_learnt_unitaries(const uint from, const string display) const
+{
+ print_footer();
+ print_simple_line(display);
+ print_header("var", "name", "value");
+ uint32_t until;
+ if (S->decisionLevel() > 0)
+ until = S->trail_lim[0];
+ else
+ until = S->trail.size();
+ for (uint i = from; i < until; i++) {
+ Var var = S->trail[i].var();
+ bool value = !(S->trail[i].sign());
+ print_line(var+1, cut_name_to_size(varnames[var]), value);
+ }
+ print_footer();
+}
+
+
+// Prints statistics on the console
+void Logger::printstats() const
+{
+ assert(statistics_on);
+ assert(varnames.size() == times_var_guessed.size());
+ assert(varnames.size() == times_var_propagated.size());
+
+ const uint fullwidth = FST_WIDTH+SND_WIDTH+TRD_WIDTH+4;
+ cout << endl;
+ cout << "+" << std::setfill('=') << std::setw(fullwidth) << "=" << "+" << endl;
+ std::stringstream tmp;
+ tmp << " STATS FOR RESTART NO. " << std::setw(3) << S->starts << " BEGIN ";
+ uint len = (fullwidth-2)/2-tmp.str().length()/2;
+ uint len2 = len + tmp.str().length()%2 + (fullwidth-2)%2;
+ cout << "||" << std::setfill('*') << std::setw(len) << "*" << tmp.str() << std::setw(len2) << "*" << "||" << endl;
+ cout << "+" << std::setfill('=') << std::setw(fullwidth) << "=" << std::setfill(' ') << "+" << endl;
+
+ cout.setf(std::ios_base::left);
+ cout.precision(2);
+ print_statistics_note();
+ print_times_var_guessed();
+ print_times_group_caused_propagation();
+ print_times_group_caused_conflict();
+ print_prop_order();
+ print_confl_order();
+ print_assign_var_order();
+ print_branch_depth_distrib();
+ print_learnt_clause_distrib();
+ #ifdef USE_GAUSS
+ print_matrix_stats();
+ #endif //USE_GAUSS
+ print_learnt_unitaries(0," Unitary clauses learnt until now");
+ print_learnt_unitaries(last_unitary_learnt_clauses, " Unitary clauses during this restart");
+ print_advanced_stats();
+ print_general_stats();
+}
+
+#ifdef USE_GAUSS
+void Logger::print_matrix_stats() const
+{
+ print_footer();
+ print_simple_line(" Matrix statistics");
+ print_footer();
+
+ uint i = 0;
+ for (vector<Gaussian*>::const_iterator it = S->gauss_matrixes.begin(), end = S->gauss_matrixes.end(); it != end; it++, i++) {
+ std::stringstream s;
+ s << "Matrix " << i << " enabled";
+ std::stringstream tmp;
+ tmp << std::boolalpha << !(*it)->get_disabled();
+ print_line(s.str(), tmp.str());
+
+ s.str("");
+ s << "Matrix " << i << " called";
+ print_line(s.str(), (*it)->get_called());
+
+ s.str("");
+ s << "Matrix " << i << " propagations";
+ print_line(s.str(), (*it)->get_useful_prop());
+
+ s.str("");
+ s << "Matrix " << i << " conflicts";
+ print_line(s.str(), (*it)->get_useful_confl());
+ }
+
+ print_footer();
+}
+#endif //USE_GAUSS
+
+void Logger::print_advanced_stats() const
+{
+ print_footer();
+ print_simple_line(" Advanced statistics - for only this restart");
+ print_footer();
+ print_line("Unitary learnts", S->get_unitary_learnts_num() - last_unitary_learnt_clauses);
+ print_line("No. branches visited", no_conflicts);
+ print_line("Avg. branch depth", (double)sum_conflict_depths/(double)no_conflicts);
+ print_line("No. decisions", no_decisions);
+ print_line("No. propagations",no_propagations);
+
+ //printf("no progatations/no decisions (i.e. one decision gives how many propagations on average *for the whole search graph*): %f\n", (double)no_propagations/(double)no_decisions);
+ //printf("no propagations/sum decisions on branches (if you look at one specific branch, what is the average number of propagations you will find?): %f\n", (double)no_propagations/(double)sum_decisions_on_branches);
+
+ print_simple_line("sum decisions on branches/no. branches");
+ print_simple_line(" (in a given branch, what is the avg.");
+ print_line(" no. of decisions?)",(double)sum_decisions_on_branches/(double)no_conflicts);
+
+ print_simple_line("sum propagations on branches/no. branches");
+ print_simple_line(" (in a given branch, what is the");
+ print_line(" avg. no. of propagations?)",(double)sum_propagations_on_branches/(double)no_conflicts);
+
+ print_footer();
+}
+
+void Logger::print_statistics_note() const
+{
+ print_footer();
+ print_simple_line("Statistics note: If you used CryptoMiniSat as");
+ print_simple_line("a library then vars are all shifted by 1 here");
+ print_simple_line("and in every printed output of the solver.");
+ print_simple_line("This does not apply when you use CryptoMiniSat");
+ print_simple_line("as a stand-alone program.");
+ print_footer();
+}
+
+// resets all stored statistics. Might be useful, to generate statistics for each restart and not for the whole search in general
+void Logger::reset_statistics()
+{
+ assert(S->decisionLevel() == 0);
+ assert(times_var_guessed.size() == times_var_propagated.size());
+ assert(times_group_caused_conflict.size() == times_group_caused_propagation.size());
+
+ typedef vector<uint>::iterator vecit;
+ for (vecit it = times_var_guessed.begin(); it != times_var_guessed.end(); it++)
+ *it = 0;
+
+ for (vecit it = times_var_propagated.begin(); it != times_var_propagated.end(); it++)
+ *it = 0;
+
+ for (vecit it = times_group_caused_conflict.begin(); it != times_group_caused_conflict.end(); it++)
+ *it = 0;
+
+ for (vecit it = times_group_caused_propagation.begin(); it != times_group_caused_propagation.end(); it++)
+ *it = 0;
+
+ for (vecit it = confls_by_group.begin(); it != confls_by_group.end(); it++)
+ *it = 0;
+
+ for (vecit it = props_by_group.begin(); it != props_by_group.end(); it++)
+ *it = 0;
+
+ typedef vector<MyAvg>::iterator avgIt;
+
+ for (avgIt it = depths_of_propagations_for_group.begin(); it != depths_of_propagations_for_group.end(); it++) {
+ it->sum = 0;
+ it->num = 0;
+ }
+
+ for (avgIt it = depths_of_conflicts_for_group.begin(); it != depths_of_conflicts_for_group.end(); it++) {
+ it->sum = 0;
+ it->num = 0;
+ }
+
+ for (avgIt it = depths_of_assigns_for_var.begin(); it != depths_of_assigns_for_var.end(); it++) {
+ it->sum = 0;
+ it->num = 0;
+ }
+ for (uint i = 0; i < depths_of_assigns_unit.size(); i++)
+ depths_of_assigns_unit[i] = false;
+
+ for (uint i = 0; i < depths_of_propagations_unit.size(); i++)
+ depths_of_propagations_unit[i] = false;
+
+ sum_conflict_depths = 0;
+ no_conflicts = 0;
+ no_decisions = 0;
+ no_propagations = 0;
+ sum_decisions_on_branches = 0;
+ sum_propagations_on_branches = 0;
+ branch_depth_distrib.clear();
+ last_unitary_learnt_clauses = S->get_unitary_learnts_num();
+}
+
+}; //NAMESPACE MINISAT
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+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 LOGGER_H
+#define LOGGER_H
+
+#include <stdio.h>
+#include <set>
+#include <vector>
+#include <string>
+#include <map>
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include "Vec.h"
+#include "Heap.h"
+#include "Alg.h"
+#include "SolverTypes.h"
+#include "limits.h"
+#include "Clause.h"
+
+using std::vector;
+using std::pair;
+using std::string;
+using std::map;
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class Solver;
+
+class MyAvg {
+public:
+ MyAvg() :
+ sum(0)
+ , num(0)
+ {}
+
+ uint sum;
+ uint num;
+};
+
+class Logger
+{
+public:
+ Logger(int& vebosity);
+ void setSolver(const Solver* S);
+
+ //types of props, confl, and finish
+ enum prop_type { add_clause_type, guess_type, simple_propagation_type};
+ enum confl_type { simple_confl_type, gauss_confl_type };
+ enum finish_type { model_found, unsat_model_found, restarting};
+
+ //Conflict and propagation(guess is also a proapgation...)
+ template<class T>
+ void conflict(const confl_type type, const uint goback_level, const uint group, const T& learnt_clause);
+ void propagation(const Lit lit, Clause* c);
+
+ //functions to add/name variables
+ void new_var(const Var var);
+ void set_variable_name(const uint var, char* name_tmp);
+
+ //function to name clause groups
+ void set_group_name(const uint group, const char* name_tmp);
+ void set_group_name(const uint group, string& name);
+ string get_group_name(const uint group) const;
+ string get_var_name(const Var var) const;
+
+ void begin();
+ void end(const finish_type finish);
+
+ void newclause(const vec<Lit>& ps, const bool xor_clause, const uint group);
+
+ bool proof_graph_on;
+ bool mini_proof;
+ bool statistics_on;
+
+private:
+ void new_group(const uint group);
+ string cut_name_to_size(const string& name) const;
+
+ void print_groups(const vector<pair<uint, uint> >& to_print) const;
+ void print_groups(const vector<pair<double, uint> >& to_print) const;
+ void print_vars(const vector<pair<uint, uint> >& to_print) const;
+ void print_vars(const vector<pair<double, uint> >& to_print) const;
+ void print_times_var_guessed() const;
+ void print_times_group_caused_propagation() const;
+ void print_times_group_caused_conflict() const;
+ void print_branch_depth_distrib() const;
+ void print_learnt_clause_distrib() const;
+ void print_leearnt_clause_graph_distrib(const uint maximum, const map<uint, uint>& learnt_sizes) const;
+ void print_advanced_stats() const;
+ void print_statistics_note() const;
+ void print_matrix_stats() const;
+ void print_general_stats() const;
+ void print_learnt_unitaries(const uint from, const string display) const;
+
+ uint max_print_lines;
+ template<class T>
+ void print_line(const uint& number, const string& name, const T& value) const;
+ void print_header(const string& first, const string& second, const string& third) const;
+ void print_footer() const;
+ template<class T>
+ void print_line(const string& str, const T& num) const;
+ void print_simple_line(const string& str) const;
+ void print_center_line(const string& str) const;
+
+ void print_confl_order() const;
+ void print_prop_order() const;
+ void print_assign_var_order() const;
+ void printstats() const;
+ void reset_statistics();
+
+ //internal data structures
+ uint uniqueid; //used to store the last unique ID given to a node
+ vector<uint> history; //stores the node uniqueIDs
+
+ //graph drawing
+ FILE* proof; //The file to store the proof
+ uint runid;
+
+ //---------------------
+ //statistics collection
+ //---------------------
+
+ //group and var names
+ vector<string> groupnames;
+ vector<string> varnames;
+
+ //confls and props grouped by clause groups
+ vector<uint> confls_by_group;
+ vector<uint> props_by_group;
+
+ //props and guesses grouped by vars
+ vector<uint> times_var_guessed;
+ vector<uint> times_var_propagated;
+
+ vector<uint> times_group_caused_conflict;
+ vector<uint> times_group_caused_propagation;
+
+ vector<MyAvg> depths_of_propagations_for_group;
+ vector<bool> depths_of_propagations_unit;
+ vector<MyAvg> depths_of_conflicts_for_group;
+ vector<MyAvg> depths_of_assigns_for_var;
+ vector<bool> depths_of_assigns_unit;
+
+ //the distribution of branch depths. first = depth, second = number of occurances
+ vector<uint> branch_depth_distrib;
+
+ uint64_t sum_conflict_depths;
+ uint64_t no_conflicts;
+ uint64_t no_decisions;
+ uint64_t no_propagations;
+ uint64_t sum_decisions_on_branches;
+ uint64_t sum_propagations_on_branches;
+ uint64_t last_unitary_learnt_clauses;
+
+ //message display properties
+ const int& verbosity;
+
+ const Solver* S;
+
+ void first_begin();
+ bool begin_called;
+ uint proofStarts;
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //LOGGER_H
+TOP = ../../..
+include $(TOP)/scripts/Makefile.common
+
+MTL = mtl
+MTRAND = MTRand
+SOURCES = Logger.cpp Solver.cpp PackedRow.cpp \
+ XorFinder.cpp Conglomerate.cpp VarReplacer.cpp \
+ FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp \
+ Clause.cpp FailedVarSearcher.cpp PartFinder.cpp \
+ Subsumer.cpp PartHandler.cpp XorSubsumer.cpp SmallPtr.cpp \
+ Gaussian.cpp MatrixFinder.cpp StateSaver.cpp
+OBJECTS = $(SOURCES:.cpp=.o)
+LIB = libminisat.a
+CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
+EXEC = minisat
+LFLAGS = -lz
+
+all: $(LIB) #$(EXEC)
+lib: $(LIB)
+
+$(LIB): $(OBJECTS)
+ rm -f $@
+ ar cq $@ $(OBJECTS)
+ ranlib $@
+ cp $(LIB) ../
+ cp $(OBJECTS) ../
+
+clean:
+ rm -f $(OBJECTS) $(LIB)
+
+.cpp.o:
+ $(CC) $(CFLAGS) $< -o $@
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#include "MatrixFinder.h"
+
+#include "Solver.h"
+#include "Gaussian.h"
+#include "GaussianConfig.h"
+#include "ClauseCleaner.h"
+#include "time_mem.h"
+
+#include <set>
+#include <map>
+#include <iomanip>
+#include <math.h>
+using std::set;
+using std::map;
+
+//#define VERBOSE_DEBUG
+
+using std::cout;
+using std::endl;
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+//#define PART_FINDING
+
+MatrixFinder::MatrixFinder(Solver& _solver) :
+ solver(_solver)
+{
+}
+
+inline const Var MatrixFinder::fingerprint(const XorClause& c) const
+{
+ Var fingerprint = 0;
+
+ for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++)
+ fingerprint |= a->var();
+
+ return fingerprint;
+}
+
+inline const bool MatrixFinder::firstPartOfSecond(const XorClause& c1, const XorClause& c2) const
+{
+ uint i1, i2;
+ for (i1 = 0, i2 = 0; i1 < c1.size() && i2 < c2.size();) {
+ if (c1[i1].var() != c2[i2].var())
+ i2++;
+ else {
+ i1++;
+ i2++;
+ }
+ }
+
+ return (i1 == c1.size());
+}
+
+const bool MatrixFinder::findMatrixes()
+{
+ table.clear();
+ table.resize(solver.nVars(), var_Undef);
+ reverseTable.clear();
+ matrix_no = 0;
+ double myTime = cpuTime();
+
+ if (solver.xorclauses.size() < MIN_GAUSS_XOR_CLAUSES ||
+ solver.gaussconfig.decision_until <= 0 ||
+ solver.xorclauses.size() > MAX_GAUSS_XOR_CLAUSES
+ )
+ return true;
+
+ solver.clauseCleaner->cleanClauses(solver.xorclauses, ClauseCleaner::xorclauses);
+ if (!solver.ok) return false;
+
+ if (solver.gaussconfig.noMatrixFind) {
+ if (solver.verbosity >=1)
+ cout << "c | Matrix finding disabled through switch. Putting all xors into matrix." << endl;
+ vector<XorClause*> xorclauses;
+ xorclauses.reserve(solver.xorclauses.size());
+ for (uint32_t i = 0; i < solver.xorclauses.size(); i++)
+ xorclauses.push_back(solver.xorclauses[i]);
+ solver.gauss_matrixes.push_back(new Gaussian(solver, solver.gaussconfig, 0, xorclauses));
+ return true;
+ }
+
+ for (XorClause** c = solver.xorclauses.getData(), **end = c + solver.xorclauses.size(); c != end; c++) {
+ set<uint> tomerge;
+ vector<Var> newSet;
+ for (Lit *l = &(**c)[0], *end2 = l + (**c).size(); l != end2; l++) {
+ if (table[l->var()] != var_Undef)
+ tomerge.insert(table[l->var()]);
+ else
+ newSet.push_back(l->var());
+ }
+ if (tomerge.size() == 1) {
+ const uint into = *tomerge.begin();
+ map<uint, vector<Var> >::iterator intoReverse = reverseTable.find(into);
+ for (uint i = 0; i < newSet.size(); i++) {
+ intoReverse->second.push_back(newSet[i]);
+ table[newSet[i]] = into;
+ }
+ continue;
+ }
+
+ for (set<uint>::iterator it = tomerge.begin(); it != tomerge.end(); it++) {
+ newSet.insert(newSet.end(), reverseTable[*it].begin(), reverseTable[*it].end());
+ reverseTable.erase(*it);
+ }
+ for (uint i = 0; i < newSet.size(); i++)
+ table[newSet[i]] = matrix_no;
+ reverseTable[matrix_no] = newSet;
+ matrix_no++;
+ }
+
+ #ifdef VERBOSE_DEBUG
+ for (map<uint, vector<Var> >::iterator it = reverseTable.begin(), end = reverseTable.end(); it != end; it++) {
+ cout << "-- set begin --" << endl;
+ for (vector<Var>::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) {
+ cout << *it2 << ", ";
+ }
+ cout << "-------" << endl;
+ }
+ #endif
+
+ uint32_t numMatrixes = setMatrixes();
+
+ if (solver.verbosity >=1)
+ std::cout << "c | Finding matrixes : " << cpuTime() - myTime << " s (found " << numMatrixes << ") |" << endl;
+
+ for (vector<Gaussian*>::iterator gauss = solver.gauss_matrixes.begin(), end = solver.gauss_matrixes.end(); gauss != end; gauss++) {
+ if (!(*gauss)->full_init()) return false;
+ }
+
+ return true;
+}
+
+const uint MatrixFinder::setMatrixes()
+{
+ vector<pair<uint, uint> > numXorInMatrix;
+ for (uint i = 0; i < matrix_no; i++)
+ numXorInMatrix.push_back(std::make_pair(i, 0));
+
+ vector<uint> sumXorSizeInMatrix(matrix_no, 0);
+ vector<vector<uint> > xorSizesInMatrix(matrix_no);
+ vector<vector<XorClause*> > xorsInMatrix(matrix_no);
+
+ #ifdef PART_FINDING
+ vector<vector<Var> > xorFingerprintInMatrix(matrix_no);
+ #endif
+
+ for (XorClause** c = solver.xorclauses.getData(), **end = c + solver.xorclauses.size(); c != end; c++) {
+ XorClause& x = **c;
+ const uint matrix = table[x[0].var()];
+ assert(matrix < matrix_no);
+
+ //for stats
+ numXorInMatrix[matrix].second++;
+ sumXorSizeInMatrix[matrix] += x.size();
+ xorSizesInMatrix[matrix].push_back(x.size());
+ xorsInMatrix[matrix].push_back(&x);
+
+ #ifdef PART_FINDING
+ xorFingerprintInMatrix[matrix].push_back(fingerprint(x));
+ #endif //PART_FINDING
+ }
+
+ std::sort(numXorInMatrix.begin(), numXorInMatrix.end(), mysorter());
+
+ #ifdef PART_FINDING
+ for (uint i = 0; i < matrix_no; i++)
+ findParts(xorFingerprintInMatrix[i], xorsInMatrix[i]);
+ #endif //PART_FINDING
+
+ uint realMatrixNum = 0;
+ for (int a = matrix_no-1; a != -1; a--) {
+ uint i = numXorInMatrix[a].first;
+
+ if (numXorInMatrix[a].second < 3)
+ continue;
+
+ const uint totalSize = reverseTable[i].size()*numXorInMatrix[a].second;
+ const double density = (double)sumXorSizeInMatrix[i]/(double)totalSize*100.0;
+ double avg = (double)sumXorSizeInMatrix[i]/(double)numXorInMatrix[a].second;
+ double variance = 0.0;
+ for (uint i2 = 0; i2 < xorSizesInMatrix[i].size(); i2++)
+ variance += pow((double)xorSizesInMatrix[i][i2]-avg, 2);
+ variance /= (double)xorSizesInMatrix.size();
+ const double stdDeviation = sqrt(variance);
+
+ if (numXorInMatrix[a].second >= solver.gaussconfig.minMatrixRows
+ && numXorInMatrix[a].second <= solver.gaussconfig.maxMatrixRows
+ && realMatrixNum < 3)
+ {
+ if (solver.verbosity >=1)
+ cout << "c | Matrix no " << std::setw(2) << realMatrixNum;
+ solver.gauss_matrixes.push_back(new Gaussian(solver, solver.gaussconfig, realMatrixNum, xorsInMatrix[i]));
+ realMatrixNum++;
+
+ } else {
+ if (solver.verbosity >=1 /*&& numXorInMatrix[a].second >= 20*/)
+ cout << "c | Unused Matrix ";
+ }
+ if (solver.verbosity >=1 /*&& numXorInMatrix[a].second >= 20*/) {
+ cout << std::setw(7) << numXorInMatrix[a].second << " x" << std::setw(5) << reverseTable[i].size();
+ cout << " density:" << std::setw(5) << std::fixed << std::setprecision(1) << density << "%";
+ cout << " xorlen avg:" << std::setw(5) << std::fixed << std::setprecision(2) << avg;
+ cout << " stdev:" << std::setw(6) << std::fixed << std::setprecision(2) << stdDeviation << " |" << endl;
+ }
+ }
+
+ return realMatrixNum;
+}
+
+void MatrixFinder::findParts(vector<Var>& xorFingerprintInMatrix, vector<XorClause*>& xorsInMatrix)
+{
+ uint ai = 0;
+ for (XorClause **a = &xorsInMatrix[0], **end = a + xorsInMatrix.size(); a != end; a++, ai++) {
+ const Var fingerprint = xorFingerprintInMatrix[ai];
+ uint ai2 = 0;
+ for (XorClause **a2 = &xorsInMatrix[0]; a2 != end; a2++, ai2++) {
+ if (ai == ai2) continue;
+ const Var fingerprint2 = xorFingerprintInMatrix[ai2];
+ if (((fingerprint & fingerprint2) == fingerprint) && firstPartOfSecond(**a, **a2)) {
+ cout << "First part of second:" << endl;
+ (*a)->plainPrint();
+ (*a2)->plainPrint();
+ cout << "END" << endl;
+ }
+ }
+ }
+}
+
+}; //NAMESPACE MINISAT
+/***********************************************************************************
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program. If not, see <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
+#ifndef MATRIXFINDER_H
+#define MATRIXFINDER_H
+
+#include <vector>
+#include <map>
+#ifdef _MSC_VER
+#include <msvc/stdint.h>
+#else
+#include <stdint.h>
+#endif //_MSC_VER
+
+#include "Clause.h"
+#include "Solver.h"
+
+namespace MINISAT
+{
+using namespace MINISAT;
+
+class Solver;
+
+using std::map;
+using std::vector;
+using std::pair;
+
+class MatrixFinder {
+
+ public:
+ MatrixFinder(Solver& solver);
+ const bool findMatrixes();
+
+ private:
+ const uint setMatrixes();
+
+ struct mysorter
+ {
+ bool operator () (const pair<uint, uint>& left, const pair<uint, uint>& right)
+ {
+ return left.second < right.second;
+ }
+ };
+
+ void findParts(vector<Var>& xorFingerprintInMatrix, vector<XorClause*>& xorsInMatrix);
+ inline const Var fingerprint(const XorClause& c) const;
+ inline const bool firstPartOfSecond(const XorClause& c1, const XorClause& c2) const;
+
+ map<uint, vector<Var> > reverseTable; //matrix -> vars
+ vector<Var> table; //var -> matrix
+ uint matrix_no;
+
+ Solver& solver;
+};
+
+}; //NAMESPACE MINISAT
+
+#endif //MATRIXFINDER_H
+// MersenneTwister.h
+// Mersenne Twister random number generator -- a C++ class MTRand
+// Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus
+// Richard J. Wagner v1.0 15 May 2003 rjwagner@writeme.com
+
+// The Mersenne Twister is an algorithm for generating random numbers. It
+// was designed with consideration of the flaws in various other generators.
+// The period, 2^19937-1, and the order of equidistribution, 623 dimensions,
+// are far greater. The generator is also fast; it avoids multiplication and
+// division, and it benefits from caches and pipelines. For more information
+// see the inventors' web page at http://www.math.keio.ac.jp/~matumoto/emt.html
+
+// Reference
+// M. Matsumoto and T. Nishimura, "Mersenne Twister: A 623-Dimensionally
+// Equidistributed Uniform Pseudo-Random Number Generator", ACM Transactions on
+// Modeling and Computer Simulation, Vol. 8, No. 1, January 1998, pp 3-30.
+
+// Copyright (C) 1997 - 2002, Makoto Matsumoto and Takuji Nishimura,
+// Copyright (C) 2000 - 2003, Richard J. Wagner
+// All rights reserved.
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions
+// are met:
+//
+// 1. Redistributions of source code must retain the above copyright
+// notice, this list of conditions and the following disclaimer.
+//
+// 2. 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.
+//
+// 3. The names of its contributors may not 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.
+
+// The original code included the following notice:
+//
+// When you use this, send an email to: matumoto@math.keio.ac.jp
+// with an appropriate reference to your work.
+//
+// It would be nice to CC: rjwagner@writeme.com and Cokus@math.washington.edu
+// when you write.
+
+#ifndef MERSENNETWISTER_H
+#define MERSENNETWISTER_H
+
+#include <iostream>
+#include <limits.h>
+#include <stdio.h>
+#include <time.h>
+#include <math.h>
+
+namespace MINISAT
+{
+
+// Not thread safe (unless auto-initialization is avoided and each thread has
+// its own MTRand object)
+
+class MTRand {
+// Data
+public:
+ typedef unsigned long uint32; // unsigned integer type, at least 32 bits
+
+ enum { N = 624 }; // length of state vector
+ enum { SAVE = N + 1 }; // length of array for save()
+
+protected:
+ enum { M = 397 }; // period parameter
+
+ uint32 state[N]; // internal state
+ uint32 *pNext; // next value to get from state
+ int left; // number of values left before reload needed
+
+
+//Methods
+public:
+ MTRand( const uint32& oneSeed ); // initialize with a simple uint32
+ MTRand( uint32 *const bigSeed, uint32 const seedLength = N ); // or an array
+ MTRand(); // auto-initialize with /dev/urandom or time() and clock()
+
+ // Do NOT use for CRYPTOGRAPHY without securely hashing several returned
+ // values together, otherwise the generator state can be learned after
+ // reading 624 consecutive values.
+
+ // Access to 32-bit random numbers
+ double rand(); // real number in [0,1]
+ double rand( const double& n ); // real number in [0,n]
+ double randExc(); // real number in [0,1)
+ double randExc( const double& n ); // real number in [0,n)
+ double randDblExc(); // real number in (0,1)
+ double randDblExc( const double& n ); // real number in (0,n)
+ uint32 randInt(); // integer in [0,2^32-1]
+ uint32 randInt( const uint32& n ); // integer in [0,n] for n < 2^32
+ double operator()() { return rand(); } // same as rand()
+
+ // Access to 53-bit random numbers (capacity of IEEE double precision)
+ double rand53(); // real number in [0,1)
+
+ // Access to nonuniform random number distributions
+ double randNorm( const double& mean = 0.0, const double& variance = 0.0 );
+
+ // Re-seeding functions with same behavior as initializers
+ void seed( const uint32 oneSeed );
+ void seed( uint32 *const bigSeed, const uint32 seedLength = N );
+ void seed();
+
+ // Saving and loading generator state
+ void save( uint32* saveArray ) const; // to array of size SAVE
+ void load( uint32 *const loadArray ); // from such array
+ friend std::ostream& operator<<( std::ostream& os, const MTRand& mtrand );
+ friend std::istream& operator>>( std::istream& is, MTRand& mtrand );
+
+protected:
+ void initialize( const uint32 oneSeed );
+ void reload();
+ uint32 hiBit( const uint32& u ) const { return u & 0x80000000UL; }
+ uint32 loBit( const uint32& u ) const { return u & 0x00000001UL; }
+ uint32 loBits( const uint32& u ) const { return u & 0x7fffffffUL; }
+ uint32 mixBits( const uint32& u, const uint32& v ) const
+ { return hiBit(u) | loBits(v); }
+ uint32 twist( const uint32& m, const uint32& s0, const uint32& s1 ) const
+ { return m ^ (mixBits(s0,s1)>>1) ^ (-loBit(s1) & 0x9908b0dfUL); }
+ static uint32 hash( time_t t, clock_t c );
+};
+
+
+inline MTRand::MTRand( const uint32& oneSeed )
+ { seed(oneSeed); }
+
+inline MTRand::MTRand( uint32 *const bigSeed, const uint32 seedLength )
+ { seed(bigSeed,seedLength); }
+
+inline MTRand::MTRand()
+ { seed(); }
+
+inline double MTRand::rand()
+ { return double(randInt()) * (1.0/4294967295.0); }
+
+inline double MTRand::rand( const double& n )
+ { return rand() * n; }
+
+inline double MTRand::randExc()
+ { return double(randInt()) * (1.0/4294967296.0); }
+
+inline double MTRand::randExc( const double& n )
+ { return randExc() * n; }
+
+inline double MTRand::randDblExc()
+ { return ( double(randInt()) + 0.5 ) * (1.0/4294967296.0); }
+
+inline double MTRand::randDblExc( const double& n )
+ { return randDblExc() * n; }
+
+inline double MTRand::rand53()
+{
+ uint32 a = randInt() >> 5, b = randInt() >> 6;
+ return ( a * 67108864.0 + b ) * (1.0/9007199254740992.0); // by Isaku Wada
+}
+
+inline double MTRand::randNorm( const double& mean, const double& variance )
+{
+ // Return a real number from a normal (Gaussian) distribution with given
+ // mean and variance by Box-Muller method
+ double r = sqrt( -2.0 * log( 1.0-randDblExc()) ) * variance;
+ double phi = 2.0 * 3.14159265358979323846264338328 * randExc();
+ return mean + r * cos(phi);
+}
+
+inline MTRand::uint32 MTRand::randInt()
+{
+ // Pull a 32-bit integer from the generator state
+ // Every other access function simply transforms the numbers extracted here
+
+ if( left == 0 ) reload();
+ --left;
+
+ register uint32 s1;
+ s1 = *pNext++;
+ s1 ^= (s1 >> 11);
+ s1 ^= (s1 << 7) & 0x9d2c5680UL;
+ s1 ^= (s1 << 15) & 0xefc60000UL;
+ return ( s1 ^ (s1 >> 18) );
+}
+
+inline MTRand::uint32 MTRand::randInt( const uint32& n )
+{
+ // Find which bits are used in n
+ // Optimized by Magnus Jonsson (magnus@smartelectronix.com)
+ uint32 used = n;
+ used |= used >> 1;
+ used |= used >> 2;
+ used |= used >> 4;
+ used |= used >> 8;
+ used |= used >> 16;
+
+ // Draw numbers until one is found in [0,n]
+ uint32 i;
+ do
+ i = randInt() & used; // toss unused bits to shorten search
+ while( i > n );
+ return i;
+}
+
+
+inline void MTRand::seed( const uint32 oneSeed )
+{
+ // Seed the generator with a simple uint32
+ initialize(oneSeed);
+ reload();
+}
+
+
+inline void MTRand::seed( uint32 *const bigSeed, const uint32 seedLength )
+{
+ // Seed the generator with an array of uint32's
+ // There are 2^19937-1 possible initial states. This function allows
+ // all of those to be accessed by providing at least 19937 bits (with a
+ // default seed length of N = 624 uint32's). Any bits above the lower 32
+ // in each element are discarded.
+ // Just call seed() if you want to get array from /dev/urandom
+ initialize(19650218UL);
+ register int i = 1;
+ register uint32 j = 0;
+ register int k = ( N > seedLength ? N : seedLength );
+ for( ; k; --k )
+ {
+ state[i] =
+ state[i] ^ ( (state[i-1] ^ (state[i-1] >> 30)) * 1664525UL );
+ state[i] += ( bigSeed[j] & 0xffffffffUL ) + j;
+ state[i] &= 0xffffffffUL;
+ ++i; ++j;
+ if( i >= N ) { state[0] = state[N-1]; i = 1; }
+ if( j >= seedLength ) j = 0;
+ }
+ for( k = N - 1; k; --k )
+ {
+ state[i] =
+ state[i] ^ ( (state[i-1] ^ (state[i-1] >> 30)) * 1566083941UL );
+ state[i] -= i;
+ state[i] &= 0xffffffffUL;
+ ++i;
+ if( i >= N ) { state[0] = state[N-1]; i = 1; }
+ }
+ state[0] = 0x80000000UL; // MSB is 1, assuring non-zero initial array
+ reload();
+}
+
+
+inline void MTRand::seed()
+{
+ // Seed the generator with an array from /dev/urandom if available
+ // Otherwise use a hash of time() and clock() values
+
+ // First try getting an array from /dev/urandom
+ FILE* urandom = fopen( "/dev/urandom", "rb" );
+ if( urandom )
+ {
+ uint32 bigSeed[N];
+ register uint32 *s = bigSeed;
+ register int i = N;
+ register bool success = true;
+ while( success && i-- )
+ success = fread( s++, sizeof(uint32), 1, urandom );
+ fclose(urandom);
+ if( success ) { seed( bigSeed, N ); return; }
+ }
+
+ // Was not successful, so use time() and clock() instead
+ seed( hash( time(NULL), clock() ) );
+}
+
+
+inline void MTRand::initialize( const uint32 seed )
+{
+ // Initialize generator state with seed
+ // See Knuth TAOCP Vol 2, 3rd Ed, p.106 for multiplier.
+ // In previous versions, most significant bits (MSBs) of the seed affect
+ // only MSBs of the state array. Modified 9 Jan 2002 by Makoto Matsumoto.
+ register uint32 *s = state;
+ register uint32 *r = state;
+ register int i = 1;
+ *s++ = seed & 0xffffffffUL;
+ for( ; i < N; ++i )
+ {
+ *s++ = ( 1812433253UL * ( *r ^ (*r >> 30) ) + i ) & 0xffffffffUL;
+ r++;
+ }
+}
+
+
+inline void MTRand::reload()
+{
+ // Generate N new values in state
+ // Made clearer and faster by Matthew Bellew (matthew.bellew@home.com)
+ register uint32 *p = state;
+ register int i;
+ for( i = N - M; i--; ++p )
+ *p = twist( p[M], p[0], p[1] );
+ for( i = M; --i; ++p )
+ *p = twist( p[M-N], p[0], p[1] );
+ *p = twist( p[M-N], p[0], state[0] );
+
+ left = N, pNext = state;
+}
+
+
+inline MTRand::uint32 MTRand::hash( time_t t, clock_t c )
+{
+ // Get a uint32 from t and c
+ // Better than uint32(x) in case x is floating point in [0,1]
+ // Based on code by Lawrence Kirby (fred@genesis.demon.co.uk)
+
+ static uint32 differ = 0; // guarantee time-based seeds will change
+
+ uint32 h1 = 0;
+ unsigned char *p = (unsigned char *) &t;
+ for( size_t i = 0; i < sizeof(t); ++i )
+ {
+ h1 *= UCHAR_MAX + 2U;
+ h1 += p[i];
+ }
+ uint32 h2 = 0;
+ p = (unsigned char *) &c;
+ for( size_t j = 0; j < sizeof(c); ++j )
+ {
+ h2 *= UCHAR_MAX + 2U;
+ h2 += p[j];
+ }
+ return ( h1 + differ++ ) ^ h2;
+}
+
+
+inline void MTRand::save( uint32* saveArray ) const
+{
+ register uint32 *sa = saveArray;
+ register const uint32 *s = state;
+ register int i = N;
+ for( ; i--; *sa++ = *s++ ) {}
+ *sa = left;
+}
+
+
+inline void MTRand::load( uint32 *const loadArray )
+{
+ register uint32 *s = state;
+ register uint32 *la = loadArray;
+ register int i = N;
+ for( ; i--; *s++ = *la++ ) {}
+ left = *la;
+ pNext = &state[N-left];
+}
+
+
+inline std::ostream& operator<<( std::ostream& os, const MTRand& mtrand )
+{
+ register const MTRand::uint32 *s = mtrand.state;
+ register int i = mtrand.N;
+ for( ; i--; os << *s++ << "\t" ) {}
+ return os << mtrand.left;
+}
+
+
+inline std::istream& operator>>( std::istream& is, MTRand& mtrand )
+{
+ register MTRand::uint32 *s = mtrand.state;
+ register int i = mtrand.N;
+ for( ; i--; is >> *s++ ) {}
+ is >> mtrand.left;
+ mtrand.pNext = &mtrand.state[mtrand.N-mtrand.left];
+ return is;
+}
+};
+
+#endif // MERSENNETWISTER_H
+
+// Change log:
+//
+// v0.1 - First release on 15 May 2000
+// - Based on code by Makoto Matsumoto, Takuji Nishimura, and Shawn Cokus
+// - Translated from C to C++
+// - Made completely ANSI compliant
+// - Designed convenient interface for initialization, seeding, and
+// obtaining numbers in default or user-defined ranges
+// - Added automatic seeding from /dev/urandom or time() and clock()
+// - Provided functions for saving and loading generator state
+//
+// v0.2 - Fixed bug which reloaded generator one step too late
+//
+// v0.3 - Switched to clearer, faster reload() code from Matthew Bellew
+//
+// v0.4 - Removed trailing newline in saved generator format to be consistent
+// with output format of built-in types
+//
+// v0.5 - Improved portability by replacing static const int's with enum's and
+// clarifying return values in seed(); suggested by Eric Heimburg
+// - Removed MAXINT constant; use 0xffffffffUL instead
+//
+// v0.6 - Eliminated seed overflow when uint32 is larger than 32 bits
+// - Changed integer [0,n] generator to give better uniformity
+//
+// v0.7 - Fixed operator precedence ambiguity in reload()
+// - Added access for real numbers in (0,1) and (0,n)
+//
+// v0.8 - Included time.h header to properly support time_t and clock_t
+//
+// v1.0 - Revised seeding to match 26 Jan 2002 update of Nishimura and Matsumoto
+// - Allowed for seeding with arrays of any length
+// - Added access for real numbers in [0,1) with 53-bit resolution
+// - Added access for real numbers from normal (Gaussian) distributions
+// - Increased overall speed by optimizing twist()
+// - Doubled speed of integer [0,n] generation
+// - Fixed out-of-range number generation on 64-bit machines
+// - Improved portability by substituting literal constants for long enum's
+// - Changed license from GNU LGPL to BSD
+/****************************************************************************************[Solver.h]
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+glucose -- Gilles Audemard, Laurent Simon (2008)
+
+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.
+**************************************************************************************************/
+
+#define RATIOREMOVECLAUSES 3
+#define NBCLAUSESBEFOREREDUCE 20000
+#define DYNAMICNBLEVEL
+#define UPDATEVARACTIVITY
+#define FIXCLEANREPLACE 30U
+#define PERCENTAGEPERFORMREPLACE 0.01
+#define PERCENTAGECLEANCLAUSES 0.01
+#define MAX_CLAUSENUM_XORFIND 5000000
+#define BINARY_TO_XOR_APPROX 4.0
+#define FULLRESTART_MULTIPLIER 250
+#define SIMPLIFY_MULTIPLIER 300
+#define FULLRESTART_MULTIPLIER_MULTIPLIER 3.5
+#define RESTART_TYPE_DECIDER_FROM 2
+#define RESTART_TYPE_DECIDER_UNTIL 7
+//#define VERBOSE_DEBUG_XOR
+//#define VERBOSE_DEBUG
+#define USE_GAUSS
+#define MIN_GAUSS_XOR_CLAUSES 5
+#define MAX_GAUSS_XOR_CLAUSES 30000
+#define MAX_OLD_LEARNTS 2000000
+//#define DEBUG_ATTACH
+#define RANDOM_LOOKAROUND_SEARCHSPACE
+//#define USE_OLD_POLARITIES
+//#define DEBUG_VARELIM
+#define BURST_SEARCH
+#define USE_POOLS
projects / francis / stp.git / commitdiff