diff options
Diffstat (limited to 'stp/sat')
| -rw-r--r-- | stp/sat/Global.h | 255 | ||||
| -rw-r--r-- | stp/sat/Heap.h | 151 | ||||
| -rw-r--r-- | stp/sat/LICENSE | 20 | ||||
| -rw-r--r-- | stp/sat/Makefile | 19 | ||||
| -rw-r--r-- | stp/sat/Simplifier.cpp | 542 | ||||
| -rw-r--r-- | stp/sat/Solver.cpp | 813 | ||||
| -rw-r--r-- | stp/sat/Solver.h | 356 | ||||
| -rw-r--r-- | stp/sat/SolverTypes.h | 132 | ||||
| -rw-r--r-- | stp/sat/Sort.h | 133 | ||||
| -rw-r--r-- | stp/sat/VarOrder.h | 146 |
10 files changed, 0 insertions, 2567 deletions
diff --git a/stp/sat/Global.h b/stp/sat/Global.h deleted file mode 100644 index deaf8c24..00000000 --- a/stp/sat/Global.h +++ /dev/null @@ -1,255 +0,0 @@ -/****************************************************************************************[Global.h] -MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#ifndef Global_h -#define Global_h - -#include <cassert> -#include <cstdio> -#include <cstdlib> -#include <cstring> -#include <new> - -// PKT: needs to be outside namespace MINISAT or mac os x compilation breaks -#ifdef _MSC_VER -#else -#include <unistd.h> -#endif - -namespace MINISAT { -//================================================================================================= -// Basic Types & Minor Things: - -// DWD: This is needed on darwin. -typedef unsigned int uint; - -#ifdef _MSC_VER - -typedef INT64 int64; -typedef UINT64 uint64; -typedef INT_PTR intp; -typedef UINT_PTR uintp; -#define I64_fmt "I64d" -#else - -typedef long long int64; -typedef unsigned long long uint64; -typedef __PTRDIFF_TYPE__ intp; -typedef unsigned __PTRDIFF_TYPE__ uintp; -#define I64_fmt "lld" -#endif - -template<class T> static inline T min(T x, T y) { return (x < y) ? x : y; } -template<class T> static inline T max(T x, T y) { return (x > y) ? x : y; } - -template <bool> struct STATIC_ASSERTION_FAILURE; -template <> struct STATIC_ASSERTION_FAILURE<true>{}; -#define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE<false>() - - -//================================================================================================= -// 'malloc()'-style memory allocation -- never returns NULL; aborts instead: - - -template<class T> static inline T* xmalloc(size_t size) { - T* tmp = (T*)malloc(size * sizeof(T)); - assert(size == 0 || tmp != NULL); - return tmp; } - -template<class T> static inline T* xrealloc(T* ptr, size_t size) { - T* tmp = (T*)realloc((void*)ptr, size * sizeof(T)); - assert(size == 0 || tmp != NULL); - return tmp; } - -template<class T> static inline void xfree(T *ptr) { - if (ptr != NULL) free((void*)ptr); } - - -//================================================================================================= -// Random numbers: - - -// Returns a random float 0 <= x < 1. Seed must never be 0. -static inline double drand(double& seed) { - seed *= 1389796; - int q = (int)(seed / 2147483647); - seed -= (double)q * 2147483647; - return seed / 2147483647; } - -// Returns a random integer 0 <= x < size. Seed must never be 0. -static inline int irand(double& seed, int size) { - return (int)(drand(seed) * size); } - - -//================================================================================================= -// 'vec' -- automatically resizable arrays (via 'push()' method): - - -// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) - -template<class T> -class vec { - T* data; - int sz; - int cap; - - void init(int size, const T& pad); - void grow(int min_cap); - -public: - // Types: - typedef int Key; - typedef T Datum; - - // Constructors: - vec(void) : data(NULL) , sz(0) , cap(0) { } - vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } - vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } - vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'xfree()') - ~vec(void) { clear(true); } - - // Ownership of underlying array: - T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; } - operator T* (void) { return data; } // (unsafe but convenient) - operator const T* (void) const { return data; } - - // Size operations: - int size (void) const { return sz; } - void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } - void pop (void) { sz--, data[sz].~T(); } - void growTo (int size); - void growTo (int size, const T& pad); - void clear (bool dealloc = false); - void capacity (int size) { grow(size); } - - // Stack interface: - void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; } - void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; } - const T& last (void) const { return data[sz-1]; } - T& last (void) { return data[sz-1]; } - - // Vector interface: - const T& operator [] (int index) const { return data[index]; } - T& operator [] (int index) { return data[index]; } - - // Don't allow copying (error prone): - vec<T>& operator = (vec<T>& other) { TEMPLATE_FAIL; } - vec (vec<T>& other) { TEMPLATE_FAIL; } - - // Duplicatation (preferred instead): - void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); } - void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } -}; - -template<class T> -void vec<T>::grow(int min_cap) { - if (min_cap <= cap) return; - if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2; - else do cap = (cap*3+1) >> 1; while (cap < min_cap); - data = xrealloc(data, cap); } - -template<class T> -void vec<T>::growTo(int size, const T& pad) { - if (sz >= size) return; - grow(size); - for (int i = sz; i < size; i++) new (&data[i]) T(pad); - sz = size; } - -template<class T> -void vec<T>::growTo(int size) { - if (sz >= size) return; - grow(size); - for (int i = sz; i < size; i++) new (&data[i]) T(); - sz = size; } - -template<class T> -void vec<T>::clear(bool dealloc) { - if (data != NULL){ - for (int i = 0; i < sz; i++) data[i].~T(); - sz = 0; - if (dealloc) xfree(data), data = NULL, cap = 0; } } - - -//================================================================================================= -// Useful functions on vectors - - -template<class V, class T> -void remove(V& ts, const T& t) -{ - int j = 0; - for (; j < ts.size() && ts[j] != t; j++) ; - assert(j < ts.size()); - for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; - ts.pop(); -} - - -template<class V, class T> -bool find(V& ts, const T& t) -{ - int j = 0; - for (; j < ts.size() && ts[j] != t; j++) ; - return j < ts.size(); -} - -//================================================================================================= -// Lifted booleans: - - -class lbool { - int value; - explicit lbool(int v) : value(v) { } - -public: - lbool() : value(0) { } - lbool(bool x) : value((int)x*2-1) { } - int toInt(void) const { return value; } - - bool operator == (const lbool& other) const { return value == other.value; } - bool operator != (const lbool& other) const { return value != other.value; } - lbool operator ~ (void) const { return lbool(-value); } - - friend int toInt (lbool l); - friend lbool toLbool(int v); -}; -inline int toInt (lbool l) { return l.toInt(); } -inline lbool toLbool(int v) { return lbool(v); } - -const lbool l_True = toLbool( 1); -const lbool l_False = toLbool(-1); -const lbool l_Undef = toLbool( 0); - - -//================================================================================================= -// Relation operators -- extend definitions from '==' and '<' - - -#ifndef __SGI_STL_INTERNAL_RELOPS // (be aware of SGI's STL implementation...) -#define __SGI_STL_INTERNAL_RELOPS -template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); } -template <class T> static inline bool operator > (const T& x, const T& y) { return y < x; } -template <class T> static inline bool operator <= (const T& x, const T& y) { return !(y < x); } -template <class T> static inline bool operator >= (const T& x, const T& y) { return !(x < y); } -#endif - - -//================================================================================================= -} -#endif diff --git a/stp/sat/Heap.h b/stp/sat/Heap.h deleted file mode 100644 index e3a82dd0..00000000 --- a/stp/sat/Heap.h +++ /dev/null @@ -1,151 +0,0 @@ -/******************************************************************************************[Heap.h] -MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#ifndef Heap_h -#define Heap_h - -#include "../AST/ASTUtil.h" -namespace MINISAT { - -//================================================================================================= - - -static inline int left (int i) { return i+i; } -static inline int right (int i) { return i+i + 1; } -static inline int parent(int i) { return i >> 1; } - -template<class C> -class Heap { - public: - C comp; - vec<int> heap; // heap of ints - vec<int> indices; // int -> index in heap - - inline void percolateUp(int i) - { - int x = heap[i]; - while (parent(i) != 0 && comp(x,heap[parent(i)])){ - heap[i] = heap[parent(i)]; - indices[heap[i]] = i; - i = parent(i); - } - heap [i] = x; - indices[x] = i; - } - - inline void percolateDown(int i) - { - int x = heap[i]; - while (left(i) < heap.size()){ - int child = right(i) < heap.size() && comp(heap[right(i)],heap[left(i)]) ? right(i) : left(i); - if (!comp(heap[child],x)) break; - heap[i] = heap[child]; - indices[heap[i]] = i; - i = child; - } - heap [i] = x; - indices[x] = i; - } - - bool ok(int n) const { - return n >= 0 && n < (int)indices.size(); } - - public: - Heap(C c) : comp(c) { heap.push(-1); } - - void setBounds (int size) { assert(size >= 0); indices.growTo(size,0); } - void increase (int n) { assert(ok(n)); assert(inHeap(n)); percolateUp(indices[n]); } - bool inHeap (int n) const { assert(ok(n)); return indices[n] != 0; } - int size () const { return heap.size()-1; } - bool empty () const { return size() == 0; } - - - void insert(int n) { - assert(!inHeap(n)); - assert(ok(n)); - indices[n] = heap.size(); - heap.push(n); - percolateUp(indices[n]); - } - - - int getmin() { - //printing heap - if(BEEV::print_sat_varorder) { - // fprintf(stderr, "Vijay: heap before getmin: "); - // for (uint i = 1; i < (uint)heap.size(); i++) - // fprintf(stderr, "%d ", heap[i]); - // fprintf(stderr, "\n"); - } - - int r = heap[1]; - heap[1] = heap.last(); - indices[heap[1]] = 1; - indices[r] = 0; - heap.pop(); - if (heap.size() > 1) - percolateDown(1); - return r; - } - - // fool proof variant of insert/increase - void update (int n) { - //fprintf(stderr, "update heap: "); - //for (uint i = 1; i < (uint)heap.size(); i++) - // fprintf(stderr, "%d ", heap[i]); - //fprintf(stderr, "\n"); - setBounds(n+1); - if (!inHeap(n)) - insert(n); - else { - percolateUp(indices[n]); - percolateDown(indices[n]); - } - } - - - bool heapProperty() { - return heapProperty(1); } - - - bool heapProperty(int i) { - return i >= heap.size() - || ((parent(i) == 0 || !comp(heap[i],heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } - - template <class F> void filter(const F& filt) { - int i,j; - for (i = j = 1; i < heap.size(); i++) - if (filt(heap[i])){ - heap[j] = heap[i]; - indices[heap[i]] = j++; - }else - indices[heap[i]] = 0; - - heap.shrink(i - j); - for (int i = heap.size() / 2; i >= 1; i--) - percolateDown(i); - - assert(heapProperty()); - } - -}; - -//================================================================================================= -} -#endif diff --git a/stp/sat/LICENSE b/stp/sat/LICENSE deleted file mode 100644 index 590930bc..00000000 --- a/stp/sat/LICENSE +++ /dev/null @@ -1,20 +0,0 @@ -MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a -copy of this software and associated documentation files (the -"Software"), to deal in the Software without restriction, including -without limitation the rights to use, copy, modify, merge, publish, -distribute, sublicense, and/or sell copies of the Software, and to -permit persons to whom the Software is furnished to do so, subject to -the following conditions: - -The above copyright notice and this permission notice shall be included -in all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS -OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF -MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE -LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION -OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION -WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/stp/sat/Makefile b/stp/sat/Makefile deleted file mode 100644 index 25bb867f..00000000 --- a/stp/sat/Makefile +++ /dev/null @@ -1,19 +0,0 @@ -#===-- stp/sat/Makefile -----------------------------------*- Makefile -*--===# -# -# The KLEE Symbolic Virtual Machine -# -# This file is distributed under the University of Illinois Open Source -# License. See LICENSE.TXT for details. -# -#===------------------------------------------------------------------------===# - -LEVEL=../.. - -LIBRARYNAME=stp_sat -DONT_BUILD_RELINKED=1 -BUILD_ARCHIVE=1 - -include $(LEVEL)/Makefile.common - -# HACK: Force -Wno-deprecated for ext container use. -CXX.Flags += -Wno-deprecated diff --git a/stp/sat/Simplifier.cpp b/stp/sat/Simplifier.cpp deleted file mode 100644 index 2e709066..00000000 --- a/stp/sat/Simplifier.cpp +++ /dev/null @@ -1,542 +0,0 @@ -/************************************************************************************[Simplifier.C] -MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#include "Solver.h" - -namespace MINISAT { - -static const int grow = 0; - -//#define WEAKEN -//#define MATING -//#define ASSYMM - -bool Solver::assymmetricBranching(Clause& c) -{ - assert(decisionLevel() == 0); - - //fprintf(stderr, "assymmetric branching on clause: "); printClause(c); fprintf(stderr, "\n"); - if (satisfied(c)){ - //fprintf(stderr, "subsumed.\n"); - return true; } - - int old; - vec<Lit> copy; for (int i = 0; i < c.size(); i++) copy.push(c[i]); - - do { - assert(copy.size() == c.size()); - - old = copy.size(); - - //fprintf(stderr, "checking that clause is normalized\n"); - //for (int i = 0; i < copy.size(); i++) - // assert(value(copy[i]) == l_Undef); - - for (int i = 0; i < copy.size(); i++){ - trail_lim.push(trail.size()); - //fprintf(stderr, " -- trying to delete literal "); printLit(copy[i]); - for (int j = 0; j < copy.size(); j++) - if (j != i) - check(enqueue(~copy[j])); - - if (propagate() != NULL){ - //fprintf(stderr, " succeeded\n"); - cancelUntil(0); - Lit l = copy[i]; - assert(find(copy, l)); - remove(copy, l); - if (!strengthen(c, l)) - return false; - i--; - - if (c.size() == 1) - return propagate() == NULL; - else - assert(qhead == trail.size()); - } - else - //fprintf(stderr, " failed\n"); - - cancelUntil(0); - } - - //} while (false); - } while (copy.size() < old); - - return true; -} - -// Returns FALSE if clause is always satisfied ('out_clause' should not be used). -//bool Solver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause) -bool Solver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause) -{ - stats.merges++; - - bool ps_smallest = _ps.size() < _qs.size(); - const Clause& ps = ps_smallest ? _qs : _ps; - const Clause& qs = ps_smallest ? _ps : _qs; - - for (int i = 0; i < qs.size(); i++){ - if (var(qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) { - if (ps[j] == ~qs[i]) - return false; - else - goto next; - } - out_clause.push(qs[i]); - } - next:; - } - - for (int i = 0; i < ps.size(); i++) - if (var(ps[i]) != v) - out_clause.push(ps[i]); - - return true; -} - - -void Solver::gather(vec<Clause*>& clauses) -{ - //fprintf(stderr, "Gathering clauses for backwards subsumption\n"); - int ntouched = 0; - assert(touched.size() == occurs.size()); - clauses.clear(); - for (int i = 0; i < touched.size(); i++) - if (touched[i]){ - const vec<Clause*>& cs = getOccurs(i); - ntouched++; - for (int j = 0; j < cs.size(); j++) - if (cs[j]->mark() == 0){ - clauses.push(cs[j]); - cs[j]->mark(2); - } - touched[i] = 0; - } - - //fprintf(stderr, "Touched variables %d of %d yields %d clauses to check\n", ntouched, touched.size(), clauses.size()); - for (int i = 0; i < clauses.size(); i++) - clauses[i]->mark(0); -} - - -/*_________________________________________________________________________________________________ -| -| subsumes : (_c : ClauseId) (c : Clause&) (_d : ClauseId) (d : Clause&) -> bool -| -| Description: -| Checks if c subsumes d, and at the same time, if c can be used to simplify d by subsumption -| resolution. -| -| Input: -| Indices into the 'clauses' vector _c, _d, and references to the corresponding clauses c, d. -| -| Result: -| lit_Error - No subsumption or simplification -| lit_Undef - Clause c subsumes d -| l - The literal l can be deleted from d -|________________________________________________________________________________________________@*/ -inline Lit Solver::subsumes(const Clause& c, const Clause& d) -{ - stats.subsumption_checks++; - if (d.size() < c.size() || (c.abstraction() & ~d.abstraction()) != 0) - return lit_Error; - - Lit ret = lit_Undef; - - for (int i = 0; i < c.size(); i++) { - // search for c[i] or ~c[i] - for (int j = 0; j < d.size(); j++) - if (c[i] == d[j]) - goto ok; - else if (ret == lit_Undef && c[i] == ~d[j]){ - ret = c[i]; - goto ok; - } - - // did not find it - stats.subsumption_misses++; - return lit_Error; - ok:; - } - - return ret; -} - - -// Backward subsumption + backward subsumption resolution -bool Solver::backwardSubsumptionCheck() -{ - while (subsumption_queue.size() > 0 || qhead < trail.size()){ - - // if propagation queue is non empty, take the first literal and - // create a dummy unit clause - if (qhead < trail.size()){ - Lit l = trail[qhead++]; - (*bwdsub_tmpunit)[0] = l; - assert(bwdsub_tmpunit->mark() == 0); - subsumption_queue.push(bwdsub_tmpunit); - } - Clause& c = *subsumption_queue.last(); subsumption_queue.pop(); - - if (c.mark()) - continue; - - if (c.size() == 1 && !enqueue(c[0])) - return false; - - // (1) find best variable to scan - Var best = var(c[0]); - for (int i = 1; i < c.size(); i++) - if (occurs[var(c[i])].size() < occurs[best].size()) - best = var(c[i]); - - // (2) search all candidates - const vec<Clause*>& cs = getOccurs(best); - - for (int j = 0; j < cs.size(); j++) - if (cs[j] != &c){ - if (cs[j]->mark()) - continue; - if (c.mark()) - break; - - //fprintf(stderr, "backward candidate "); printClause(*cs[j]); fprintf(stderr, "\n"); - Lit l = subsumes(c, *cs[j]); - if (l == lit_Undef){ - //fprintf(stderr, "clause backwards subsumed\n"); - //fprintf(stderr, " >> clause %d: ", cs[j]->mark()); printClause(*cs[j]); fprintf(stderr, "\n"); - //fprintf(stderr, " >> clause %d: ", c.mark()); printClause(c); fprintf(stderr, "\n"); - removeClause(*cs[j], false); - }else if (l != lit_Error){ - //fprintf(stderr, "backwards subsumption resolution\n"); - //fprintf(stderr, " >> clause %d: ", cs[j]->mark()); printClause(*cs[j]); fprintf(stderr, "\n"); - //fprintf(stderr, " >> clause %d: ", c.mark()); printClause(c); fprintf(stderr, "\n"); - - assert(cs[j]->size() > 1); - assert(find(*cs[j], ~l)); - - subsumption_queue.push(cs[j]); - if (!strengthen(*cs[j], ~l)) - return false; - - // did current candidate get deleted from cs? then check candidate at index j again - if (var(l) == best) - j--; - } - } - } - - return true; -} - - -bool Solver::eliminateVar(Var v, bool fail) -{ - assert(hasVarProp(v, p_frozen)); - - vec<Clause*> pos, neg; - const vec<Clause*>& cls = getOccurs(v); - - if (value(v) != l_Undef || cls.size() == 0) - return true; - - //fprintf(stderr, "trying to eliminate var %d\n", v+1); - for (int i = 0; i < cls.size(); i++){ - //fprintf(stderr, "clause: "); printClause(*cls[i]); fprintf(stderr, "\n"); - if (find(*cls[i], Lit(v))) - pos.push(cls[i]); - else{ - assert(find(*cls[i], ~Lit(v))); - neg.push(cls[i]); - } - } - -#ifdef WEAKEN - vec<int> posc(pos.size(), 0); - vec<int> negc(neg.size(), 0); -#endif - // check if number of clauses decreases - int cnt = 0; - vec<Lit> resolvent; - for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++){ - resolvent.clear(); - if (merge(*pos[i], *neg[j], v, resolvent)){ - cnt++; -#ifdef WEAKEN - posc[i]++; - negc[j]++; -#endif - } -#ifndef WEAKEN - if (cnt > cls.size() + grow) - return true; -#else -#ifdef MATING - if (cnt > cls.size() + grow) - if (posc[i] > 0) - break; -#endif -#endif - assert(pos.size() <= n_occ[toInt(Lit(v))]); - assert(neg.size() <= n_occ[toInt(~Lit(v))]); - } - -#ifdef WEAKEN -#ifdef MATING - for (int i = 0; i < neg.size(); i++) - if (negc[i] == 0) - for (int j = 0; j < pos.size(); j++){ - resolvent.clear(); - if (merge(*neg[i], *pos[j], v, resolvent)){ - negc[i]++; - break; - } - } -#endif - for (int i = 0; i < pos.size(); i++) - if (posc[i] == 0) - removeClause(*pos[i], false); - - for (int i = 0; i < neg.size(); i++) - if (negc[i] == 0) - removeClause(*neg[i], false); - - if (cnt > cls.size() + grow) - return true; -#endif - //if (pos.size() != n_occ[toInt(Lit(v))]) - // fprintf(stderr, "pos.size() = %d, n_occ[toInt(Lit(v))] = %d\n", pos.size(), n_occ[toInt(Lit(v))]); - assert(pos.size() == n_occ[toInt(Lit(v))]); - //if (neg.size() != n_occ[toInt(~Lit(v))]) - // fprintf(stderr, "neg.size() = %d, n_occ[toInt(Lit(v))] = %d\n", neg.size(), n_occ[toInt(Lit(v))]); - assert(neg.size() == n_occ[toInt(~Lit(v))]); - assert(cnt <= cls.size() + grow); - setVarProp(v, p_decisionvar, false); - - // produce clauses in cross product - int top = clauses.size(); - for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++){ - resolvent.clear(); -#ifdef WEAKEN - if (pos[i]->mark() == 1) - break; - if (neg[j]->mark() == 1) - continue; -#endif - - if (merge(*pos[i], *neg[j], v, resolvent)){ - int i, j; - for (i = j = 0; i < resolvent.size(); i++) - if (value(resolvent[i]) == l_True) - goto next; - else if (value(resolvent[i]) == l_Undef) - resolvent[j++] = resolvent[i]; - resolvent.shrink(i - j); - - if (resolvent.size() == 1){ - if (!enqueue(resolvent[0])) - return false; - }else{ - int apa = clauses.size(); - check(newClause(resolvent, false, true)); - assert(apa + 1 == clauses.size()); - } - } - next:; - } - - if (fail){ - fprintf(stderr, "eliminated var %d, %d <= %d\n", v+1, cnt, cls.size()); - fprintf(stderr, "previous clauses:\n"); - for (int i = 0; i < cls.size(); i++){ - printClause(*cls[i]); - fprintf(stderr, "\n"); - } - - fprintf(stderr, "new clauses:\n"); - for (int i = top; i < clauses.size(); i++){ - printClause(*clauses[i]); - fprintf(stderr, "\n"); - } - - assert(0); } - - //fprintf(stderr, "eliminated var %d, %d <= %d\n", v+1, cnt, cls.size()); - //fprintf(stderr, "previous clauses:\n"); - //for (int i = 0; i < cls.size(); i++){ - // printClause(*cls[i]); - // fprintf(stderr, "\n"); - //} - // - //fprintf(stderr, "new clauses:\n"); - //for (int i = top; i < clauses.size(); i++){ - // printClause(*clauses[i]); - // fprintf(stderr, "\n"); - //} - - // delete + store old clauses - eliminated_var.push(v); - eliminated_lim.push(eliminated.size()); - for (int i = 0; i < cls.size(); i++){ - eliminated.push(Clause_new(*cls[i])); - -#ifdef WEAKEN - if (cls[i]->mark() == 0) -#endif - removeClause(*cls[i], false); - - } - - assert(subsumption_queue.size() == 0); - for (int i = top; i < clauses.size(); i++) -#ifdef ASSYMM - if (clauses[i]->mark() == 0) - if (!assymmetricBranching(*clauses[i])) - return false; - else - subsumption_queue.push(clauses[i]); -#else - if (clauses[i]->mark() == 0) - subsumption_queue.push(clauses[i]); -#endif - - return backwardSubsumptionCheck(); -} - - -void Solver::extendModel() -{ - assert(eliminated_var.size() == eliminated_lim.size()); - for (int i = eliminated_var.size()-1; i >= 0; i--){ - Var v = eliminated_var[i]; - Lit l = lit_Undef; - - //fprintf(stderr, "extending var %d\n", v+1); - - for (int j = eliminated_lim[i]; j < (i+1 >= eliminated_lim.size() ? eliminated.size() : eliminated_lim[i+1]); j++){ - assert(j < eliminated.size()); - Clause& c = *eliminated[j]; - - //fprintf(stderr, "checking clause: "); printClause(c); fprintf(stderr, "\n"); - - for (int k = 0; k < c.size(); k++) - if (var(c[k]) == v) - l = c[k]; - else if (value(c[k]) != l_False) - goto next; - - assert(l != lit_Undef); - //fprintf(stderr, "Fixing var %d to %d\n", v+1, !sign(l)); - - assigns[v] = toInt(lbool(!sign(l))); - break; - - next:; - } - - if (value(v) == l_Undef) - assigns[v] = toInt(l_True); - } -} - - -bool Solver::eliminate() -{ - assert(subsumption); - - int cnt = 0; - //fprintf(stderr, "eliminating variables\n"); - -#ifdef INVARIANTS - // check that all clauses are simplified - fprintf(stderr, "Checking that all clauses are normalized prior to variable elimination\n"); - for (int i = 0; i < clauses.size(); i++) - if (clauses[i]->mark() == 0){ - Clause& c = *clauses[i]; - for (int j = 0; j < c.size(); j++) - assert(value(c[j]) == l_Undef); - } - fprintf(stderr, "done.\n"); -#endif - - for (;;){ - gather(subsumption_queue); - - if (subsumption_queue.size() == 0 && heap.size() == 0) - break; - - //fprintf(stderr, "backwards subsumption: %10d\n", subsumption_queue.size()); - if (!backwardSubsumptionCheck()) - return false; - - //fprintf(stderr, "variable elimination: %10d\n", heap.size()); - cnt = 0; - for (;;){ - assert(!heap.empty() || heap.size() == 0); - if (heap.empty()) - break; - - Var elim = heap.getmin(); - - assert(hasVarProp(elim, p_frozen)); - - //for (int i = 1; i < heap.heap.size(); i++) - // assert(heap.comp(elim, heap.heap[i]) || !heap.comp(elim, heap.heap[i])); - - //if (cnt++ % 100 == 0) - // fprintf(stderr, "left %10d\r", heap.size()); - - if (!eliminateVar(elim)) - return false; - } - } -#ifdef INVARIANTS - // check that no more subsumption is possible - fprintf(stderr, "Checking that no more subsumption is possible\n"); - cnt = 0; - for (int i = 0; i < clauses.size(); i++){ - if (cnt++ % 1000 == 0) - fprintf(stderr, "left %10d\r", clauses.size() - i); - for (int j = 0; j < i; j++) - assert(clauses[i]->mark() || - clauses[j]->mark() || - subsumes(*clauses[i], *clauses[j]) == lit_Error); - } - fprintf(stderr, "done.\n"); - - // check that no more elimination is possible - fprintf(stderr, "Checking that no more elimination is possible\n"); - for (int i = 0; i < nVars(); i++){ - if (hasVarProp(i, p_frozen)) - eliminateVar(i, true); - } - fprintf(stderr, "done.\n"); - -#endif - - assert(qhead == trail.size()); - - return true; -} -} diff --git a/stp/sat/Solver.cpp b/stp/sat/Solver.cpp deleted file mode 100644 index 9761c719..00000000 --- a/stp/sat/Solver.cpp +++ /dev/null @@ -1,813 +0,0 @@ -/****************************************************************************************[Solver.C] -MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#include "Solver.h" -#include "Sort.h" -#include <cmath> - -namespace MINISAT { -//================================================================================================= -// Operations on clauses: - - -/*_________________________________________________________________________________________________ -| -| newClause : (ps : const vec<Lit>&) (learnt : bool) -> [void] -| -| Description: -| Allocate and add a new clause to the SAT solvers clause database. -| -| Input: -| ps - The new clause as a vector of literals. -| learnt - Is the clause a learnt clause? For learnt clauses, 'ps[0]' is assumed to be the -| asserting literal. An appropriate 'enqueue()' operation will be performed on this -| literal. One of the watches will always be on this literal, the other will be set to -| the literal with the highest decision level. -| -| Effect: -| Activity heuristics are updated. -|________________________________________________________________________________________________@*/ -bool Solver::newClause(const vec<Lit>& ps_, bool learnt, bool normalized) -{ - vec<Lit> qs; - if (!learnt && !normalized){ - assert(decisionLevel() == 0); - ps_.copyTo(qs); // Make a copy of the input vector. - - // Remove duplicates: - sortUnique(qs); - - // Check if clause is satisfied: - for (int i = 0; i < qs.size()-1; i++){ - if (qs[i] == ~qs[i+1]) - return true; } - for (int i = 0; i < qs.size(); i++){ - if (value(qs[i]) == l_True) - return true; } - - // Remove false literals: - int i, j; - for (i = j = 0; i < qs.size(); i++) - if (value(qs[i]) != l_False) - qs[j++] = qs[i]; - qs.shrink(i - j); - } - const vec<Lit>& ps = learnt || normalized ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals. - - if (ps.size() == 0) - return false; - else if (ps.size() == 1){ - assert(decisionLevel() == 0); - return enqueue(ps[0]); - }else{ - // Allocate clause: - Clause* c = Clause_new(ps, learnt); - - if (learnt){ - // Put the second watch on the first literal with highest decision level: - // (requires that this method is called at the level where the clause is asserting!) - int i; - for (i = 1; i < ps.size() && position(trailpos[var(ps[i])]) < trail_lim.last(); i++) - ; - (*c)[1] = ps[i]; - (*c)[i] = ps[1]; - - // Bump, enqueue, store clause: - claBumpActivity(*c); // (newly learnt clauses should be considered active) - check(enqueue((*c)[0], c)); - learnts.push(c); - stats.learnts_literals += c->size(); - }else{ - // Store clause: - clauses.push(c); - stats.clauses_literals += c->size(); - - if (subsumption){ - c->calcAbstraction(); - for (int i = 0; i < c->size(); i++){ - assert(!find(occurs[var((*c)[i])], c)); - occurs[var((*c)[i])].push(c); - n_occ[toInt((*c)[i])]++; - touched[var((*c)[i])] = 1; - - if (heap.inHeap(var((*c)[i]))) - updateHeap(var((*c)[i])); - } - } - - } - // Watch clause: - watches[toInt(~(*c)[0])].push(c); - watches[toInt(~(*c)[1])].push(c); - } - - return true; -} - - -// Disposes a clauses and removes it from watcher lists. NOTE! -// Low-level; does NOT change the 'clauses' and 'learnts' vector. -// -void Solver::removeClause(Clause& c, bool dealloc) -{ - //fprintf(stderr, "delete %d: ", _c); printClause(c); fprintf(stderr, "\n"); - assert(c.mark() == 0); - - if (c.size() > 1){ - assert(find(watches[toInt(~c[0])], &c)); - assert(find(watches[toInt(~c[1])], &c)); - remove(watches[toInt(~c[0])], &c); - remove(watches[toInt(~c[1])], &c); } - - if (c.learnt()) stats.learnts_literals -= c.size(); - else stats.clauses_literals -= c.size(); - - if (subsumption && !c.learnt()){ - for (int i = 0; i < c.size(); i++){ - if (dealloc){ - assert(find(occurs[var(c[i])], &c)); - remove(occurs[var(c[i])], &c); - } - n_occ[toInt(c[i])]--; - updateHeap(var(c[i])); - } - } - - if (dealloc) - xfree(&c); - else - c.mark(1); -} - - -bool Solver::satisfied(Clause& c) const -{ - for (int i = 0; i < c.size(); i++) - if (value(c[i]) == l_True) - return true; - return false; } - - -bool Solver::strengthen(Clause& c, Lit l) -{ - assert(decisionLevel() == 0); - assert(c.size() > 1); - assert(c.mark() == 0); - - assert(toInt(~c[0]) < watches.size()); - assert(toInt(~c[1]) < watches.size()); - - assert(find(watches[toInt(~c[0])], &c)); - assert(find(watches[toInt(~c[1])], &c)); - assert(find(c,l)); - - if (c.learnt()) stats.learnts_literals -= 1; - else stats.clauses_literals -= 1; - - if (c[0] == l || c[1] == l){ - assert(find(watches[toInt(~l)], &c)); - remove(c,l); - remove(watches[toInt(~l)], &c); - if (c.size() > 1){ - assert(!find(watches[toInt(~c[1])], &c)); - watches[toInt(~c[1])].push(&c); } - else { - assert(find(watches[toInt(~c[0])], &c)); - remove(watches[toInt(~c[0])], &c); - removeClause(c, false); - } - } - else - remove(c,l); - - assert(c.size() == 1 || find(watches[toInt(~c[0])], &c)); - assert(c.size() == 1 || find(watches[toInt(~c[1])], &c)); - - if (subsumption){ - assert(find(occurs[var(l)], &c)); - remove(occurs[var(l)], &c); - assert(!find(occurs[var(l)], &c)); - - c.calcAbstraction(); - - n_occ[toInt(l)]--; - updateHeap(var(l)); - } - - return c.size() == 1 ? enqueue(c[0]) : true; -} - - -//================================================================================================= -// Minor methods: - - -// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be -// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). -// -Var Solver::newVar(bool polarity, bool dvar) { - int index; - index = nVars(); - watches .push(); // (list for positive literal) - watches .push(); // (list for negative literal) - reason .push(NULL); - assigns .push(toInt(l_Undef)); - trailpos .push(TrailPos(0,0)); - activity .push(0); - order .newVar(polarity,dvar); - seen .push(0); - touched .push(0); - if (subsumption){ - occurs .push(); - n_occ .push(0); - n_occ .push(0); - heap .setBounds(index+1); - } - return index; } - - -// Returns FALSE if immediate conflict. -bool Solver::assume(Lit p) { - trail_lim.push(trail.size()); - return enqueue(p); } - - -// Revert to the state at given level. -void Solver::cancelUntil(int level) { - if (decisionLevel() > level){ - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ - Var x = var(trail[c]); - assigns[x] = toInt(l_Undef); - reason [x] = NULL; - order.undo(x); } - qhead = trail_lim[level]; - trail.shrink(trail.size() - trail_lim[level]); - trail_lim.shrink(trail_lim.size() - level); - } -} - - -//================================================================================================= -// Major methods: - - -/*_________________________________________________________________________________________________ -| -| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void] -| -| Description: -| Analyze conflict and produce a reason clause. -| -| Pre-conditions: -| * 'out_learnt' is assumed to be cleared. -| * Current decision level must be greater than root level. -| -| Post-conditions: -| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. -| -| Effect: -| Will undo part of the trail, upto but not beyond the assumption of the current decision level. -|________________________________________________________________________________________________@*/ -void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel) -{ - int pathC = 0; - int btpos = -1; - Lit p = lit_Undef; - - // Generate conflict clause: - // - out_learnt.push(); // (leave room for the asserting literal) - int index = trail.size()-1; - do{ - assert(confl != NULL); // (otherwise should be UIP) - Clause& c = *confl; - - if (c.learnt()) - claBumpActivity(c); - - for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ - Lit q = c[j]; - if (!seen[var(q)] && position(trailpos[var(q)]) >= trail_lim[0]){ - varBumpActivity(q); - seen[var(q)] = 1; - if (position(trailpos[var(q)]) >= trail_lim.last()) - pathC++; - else{ - out_learnt.push(q); - btpos = max(btpos, position(trailpos[var(q)])); - } - } - } - - // Select next clause to look at: - while (!seen[var(trail[index--])]) ; - p = trail[index+1]; - confl = reason[var(p)]; - seen[var(p)] = 0; - pathC--; - - }while (pathC > 0); - out_learnt[0] = ~p; - - // Find correct backtrack level - for (out_btlevel = trail_lim.size()-1; out_btlevel > 0 && trail_lim[out_btlevel-1] > btpos; out_btlevel--) - ; - - int i, j; - if (expensive_ccmin){ - // Simplify conflict clause (a lot): - // - uint min_level = 0; - for (i = 1; i < out_learnt.size(); i++) - min_level |= abstractLevel(trailpos[var(out_learnt[i])]); // (maintain an abstraction of levels involved in conflict) - - out_learnt.copyTo(analyze_toclear); - for (i = j = 1; i < out_learnt.size(); i++) - if (reason[var(out_learnt[i])] == NULL || !analyze_removable(out_learnt[i], min_level)) - out_learnt[j++] = out_learnt[i]; - }else{ - // Simplify conflict clause (a little): - // - out_learnt.copyTo(analyze_toclear); - for (i = j = 1; i < out_learnt.size(); i++){ - Clause& c = *reason[var(out_learnt[i])]; - for (int k = 1; k < c.size(); k++) - if (!seen[var(c[k])] && position(trailpos[var(c[k])]) >= trail_lim[0]){ - out_learnt[j++] = out_learnt[i]; - break; } - } - } - - stats.max_literals += out_learnt.size(); - out_learnt.shrink(i - j); - stats.tot_literals += out_learnt.size(); - - for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) -} - - -// Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed. -// -bool Solver::analyze_removable(Lit p, uint min_level) -{ - analyze_stack.clear(); analyze_stack.push(p); - int top = analyze_toclear.size(); - while (analyze_stack.size() > 0){ - assert(reason[var(analyze_stack.last())] != NULL); - Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop(); - - for (int i = 1; i < c.size(); i++){ - Lit p = c[i]; - TrailPos tp = trailpos[var(p)]; - if (!seen[var(p)] && position(tp) >= trail_lim[0]){ - if (reason[var(p)] != NULL && (abstractLevel(tp) & min_level) != 0){ - seen[var(p)] = 1; - analyze_stack.push(p); - analyze_toclear.push(p); - }else{ - for (int j = top; j < analyze_toclear.size(); j++) - seen[var(analyze_toclear[j])] = 0; - analyze_toclear.shrink(analyze_toclear.size() - top); - return false; - } - } - } - } - - return true; -} - - -/*_________________________________________________________________________________________________ -| -| analyzeFinal : (p : Lit) -> [void] -| -| Description: -| Specialized analysis procedure to express the final conflict in terms of assumptions. -| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and -| stores the result in 'out_conflict'. -|________________________________________________________________________________________________@*/ -void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) -{ - out_conflict.clear(); - out_conflict.push(p); - - if (decisionLevel() == 0) - return; - - seen[var(p)] = 1; - - int start = position(trailpos[var(p)]); - for (int i = start; i >= trail_lim[0]; i--){ - Var x = var(trail[i]); - if (seen[x]){ - if (reason[x] == NULL){ - assert(position(trailpos[x]) >= trail_lim[0]); - out_conflict.push(~trail[i]); - }else{ - Clause& c = *reason[x]; - for (int j = 1; j < c.size(); j++) - if (position(trailpos[var(c[j])]) >= trail_lim[0]) - seen[var(c[j])] = 1; - } - seen[x] = 0; - } - } -} - - -/*_________________________________________________________________________________________________ -| -| enqueue : (p : Lit) (from : Clause*) -> [bool] -| -| Description: -| Puts a new fact on the propagation queue as well as immediately updating the variable's value. -| Should a conflict arise, FALSE is returned. -| -| Input: -| p - The fact to enqueue -| from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'. -| Default value is NULL (no reason). -| -| Output: -| TRUE if fact was enqueued without conflict, FALSE otherwise. -|________________________________________________________________________________________________@*/ -bool Solver::enqueue(Lit p, Clause* from) -{ - - if (value(p) != l_Undef) - return value(p) != l_False; - else{ - assigns [var(p)] = toInt(lbool(!sign(p))); - trailpos[var(p)] = TrailPos(trail.size(),decisionLevel()); - reason [var(p)] = from; - trail.push(p); - return true; - } -} - - -/*_________________________________________________________________________________________________ -| -| propagate : [void] -> [Clause*] -| -| Description: -| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, -| otherwise NULL. -| -| Post-conditions: -| * the propagation queue is empty, even if there was a conflict. -|________________________________________________________________________________________________@*/ -Clause* Solver::propagate() -{ - if (decisionLevel() == 0 && subsumption) - return backwardSubsumptionCheck() ? NULL : propagate_tmpempty; - - Clause* confl = NULL; - //fprintf(stderr, "propagate, qhead = %d, qtail = %d\n", qhead, qtail); - while (qhead < trail.size()){ - stats.propagations++; - simpDB_props--; - - Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. - vec<Clause*>& ws = watches[toInt(p)]; - Clause **i, **j, **end; - - for (i = j = (Clause**)ws, end = i + ws.size(); i != end;){ - Clause& c = **i++; - - // Make sure the false literal is data[1]: - Lit false_lit = ~p; - if (c[0] == false_lit) - c[0] = c[1], c[1] = false_lit; - - assert(c[1] == false_lit); - - // If 0th watch is true, then clause is already satisfied. - Lit first = c[0]; - if (value(first) == l_True){ - *j++ = &c; - }else{ - // Look for new watch: - for (int k = 2; k < c.size(); k++) - if (value(c[k]) != l_False){ - c[1] = c[k]; c[k] = false_lit; - watches[toInt(~c[1])].push(&c); - goto FoundWatch; } - - // Did not find watch -- clause is unit under assignment: - *j++ = &c; - if (!enqueue(first, &c)){ - confl = &c; - qhead = trail.size(); - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - FoundWatch:; - } - } - ws.shrink(i - j); - } - - return confl; -} - - -/*_________________________________________________________________________________________________ -| -| reduceDB : () -> [void] -| -| Description: -| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked -| clauses are clauses that are reason to some assignment. Binary clauses are never removed. -|________________________________________________________________________________________________@*/ -struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } }; -void Solver::reduceDB() -{ - int i, j; - double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity - - sort(learnts, reduceDB_lt()); - for (i = j = 0; i < learnts.size() / 2; i++){ - if (learnts[i]->size() > 2 && !locked(*learnts[i])) - removeClause(*learnts[i]); - else - learnts[j++] = learnts[i]; - } - for (; i < learnts.size(); i++){ - if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim) - removeClause(*learnts[i]); - else - learnts[j++] = learnts[i]; - } - learnts.shrink(i - j); -} - - -/*_________________________________________________________________________________________________ -| -| simplifyDB : [void] -> [bool] -| -| Description: -| Simplify the clause database according to the current top-level assigment. Currently, the only -| thing done here is the removal of satisfied clauses, but more things can be put here. -|________________________________________________________________________________________________@*/ -bool Solver::simplifyDB(bool expensive) -{ - assert(decisionLevel() == 0); - if (!ok || propagate() != NULL) - return ok = false; - - if (nAssigns() == simpDB_assigns || - (!subsumption && simpDB_props > 0)) // (nothing has changed or preformed a simplification too recently) - return true; - - if (subsumption){ - if (expensive && !eliminate()) - return ok = false; - - // Move this cleanup code to its own method ? - int i , j; - vec<Var> dirty; - for (i = 0; i < clauses.size(); i++) - if (clauses[i]->mark() == 1){ - Clause& c = *clauses[i]; - for (int k = 0; k < c.size(); k++) - if (!seen[var(c[k])]){ - seen[var(c[k])] = 1; - dirty.push(var(c[k])); - } - } - - for (i = 0; i < dirty.size(); i++){ - cleanOcc(dirty[i]); - seen[dirty[i]] = 0; - } - - for (i = j = 0; i < clauses.size(); i++) - if (clauses[i]->mark() == 1) - xfree(clauses[i]); - else - clauses[j++] = clauses[i]; - clauses.shrink(i - j); - } - - // Remove satisfied clauses: - for (int type = 0; type < (subsumption ? 1 : 2); type++){ // (only scan learnt clauses if subsumption is on) - vec<Clause*>& cs = type ? learnts : clauses; - int j = 0; - for (int i = 0; i < cs.size(); i++){ - assert(cs[i]->mark() == 0); - if (satisfied(*cs[i])) - removeClause(*cs[i]); - else - cs[j++] = cs[i]; - } - cs.shrink(cs.size()-j); - } - order.cleanup(); - - simpDB_assigns = nAssigns(); - simpDB_props = stats.clauses_literals + stats.learnts_literals; // (shouldn't depend on 'stats' really, but it will do for now) - - return true; -} - - -/*_________________________________________________________________________________________________ -| -| search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] -| -| Description: -| Search for a model the specified number of conflicts, keeping the number of learnt clauses -| below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to -| indicate infinity. -| -| Output: -| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If -| all variables are decision variables, this means that the clause set is satisfiable. 'l_False' -| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. -|________________________________________________________________________________________________@*/ -lbool Solver::search(int nof_conflicts, int nof_learnts) -{ - assert(ok); - int backtrack_level; - int conflictC = 0; - vec<Lit> learnt_clause; - - stats.starts++; - var_decay = 1 / params.var_decay; - cla_decay = 1 / params.clause_decay; - - for (;;){ - Clause* confl = propagate(); - if (confl != NULL){ - // CONFLICT - stats.conflicts++; conflictC++; - if (decisionLevel() == 0) return l_False; - - learnt_clause.clear(); - analyze(confl, learnt_clause, backtrack_level); - cancelUntil(backtrack_level); - newClause(learnt_clause, true); - varDecayActivity(); - claDecayActivity(); - - }else{ - // NO CONFLICT - - if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ - // Reached bound on number of conflicts: - progress_estimate = progressEstimate(); - cancelUntil(0); - return l_Undef; } - - // Simplify the set of problem clauses: - if (decisionLevel() == 0 && !simplifyDB()) - return l_False; - - if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) - // Reduce the set of learnt clauses: - reduceDB(); - - Lit next = lit_Undef; - - if (decisionLevel() < assumptions.size()){ - // Perform user provided assumption: - next = assumptions[decisionLevel()]; - if (value(next) == l_False){ - analyzeFinal(~next, conflict); - return l_False; } - }else{ - // New variable decision: - stats.decisions++; - next = order.select(params.random_var_freq, decisionLevel()); - } - if (next == lit_Undef) - // Model found: - return l_True; - - check(assume(next)); - } - } -} - - -// Return search-space coverage. Not extremely reliable. -// -double Solver::progressEstimate() -{ - double progress = 0; - double F = 1.0 / nVars(); - - for (int i = 0; i <= decisionLevel(); i++){ - int beg = i == 0 ? 0 : trail_lim[i - 1]; - int end = i == decisionLevel() ? trail.size() : trail_lim[i]; - progress += pow(F, i) * (end - beg); - } - - return progress / nVars(); -} - - -// Divide all variable activities by 1e100. -// -void Solver::varRescaleActivity() -{ - for (int i = 0; i < nVars(); i++) - activity[i] *= 1e-100; - var_inc *= 1e-100; -} - - -// Divide all constraint activities by 1e100. -// -void Solver::claRescaleActivity() -{ - for (int i = 0; i < learnts.size(); i++) - learnts[i]->activity() *= 1e-20; - cla_inc *= 1e-20; -} - - -/*_________________________________________________________________________________________________ -| -| solve : (assumps : const vec<Lit>&) -> [bool] -| -| Description: -| Top-level solve. -|________________________________________________________________________________________________@*/ -bool Solver::solve(const vec<Lit>& assumps) -{ - model.clear(); - conflict.clear(); - - if (!simplifyDB(true)) return false; - - - double nof_conflicts = params.restart_first; - double nof_learnts = nClauses() * params.learntsize_factor; - lbool status = l_Undef; - assumps.copyTo(assumptions); - - if (verbosity >= 1){ - printf("==================================[MINISAT]====================================\n"); - printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); - printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); - printf("===============================================================================\n"); - } - - // Search: - while (status == l_Undef){ - if (verbosity >= 1) - //printf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100); - printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)stats.conflicts, order.size(), nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (double)stats.learnts_literals/nLearnts(), progress_estimate*100); - status = search((int)nof_conflicts, (int)nof_learnts); - nof_conflicts *= params.restart_inc; - nof_learnts *= params.learntsize_inc; - } - - if (verbosity >= 1) { - printf("==============================================================================\n"); - fflush(stdout); - } - - if (status == l_True){ - // Copy model: - extendModel(); -#if 1 - //fprintf(stderr, "Verifying model.\n"); - for (int i = 0; i < clauses.size(); i++) - assert(satisfied(*clauses[i])); - for (int i = 0; i < eliminated.size(); i++) - assert(satisfied(*eliminated[i])); -#endif - model.growTo(nVars()); - for (int i = 0; i < nVars(); i++) model[i] = value(i); - }else{ - assert(status == l_False); - if (conflict.size() == 0) - ok = false; - } - - cancelUntil(0); - return status == l_True; -} -} //end of MINISAT namespace diff --git a/stp/sat/Solver.h b/stp/sat/Solver.h deleted file mode 100644 index 0a6dc87e..00000000 --- a/stp/sat/Solver.h +++ /dev/null @@ -1,356 +0,0 @@ -/****************************************************************************************[Solver.h] -MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#ifndef Solver_h -#define Solver_h - -#include "SolverTypes.h" -#include "VarOrder.h" - -namespace MINISAT { - -//================================================================================================= -// Solver -- the main class: -struct SolverStats { - int64 starts, decisions, propagations, conflicts; - int64 clauses_literals, learnts_literals, max_literals, tot_literals; - int64 subsumption_checks, subsumption_misses, merges; - SolverStats() : - starts(0), decisions(0), propagations(0), conflicts(0) - , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) - , subsumption_checks(0), subsumption_misses(0), merges(0) - { } -}; - - -struct SearchParams { - double var_decay, clause_decay, random_var_freq; - double restart_inc, learntsize_inc, learntsize_factor; - int restart_first; - - SearchParams(double v = 0.95, double c = 0.999, double r = 0.02, - double ri = 1.5, double li = 1.1, double lf = (double)1/(double)3, - int rf = 100) : - var_decay(v), clause_decay(c), random_var_freq(r), - restart_inc(ri), learntsize_inc(li), learntsize_factor(lf), - restart_first(rf) { } -}; - - struct ElimLt { - const vec<int>& n_occ; - - ElimLt(const vec<int>& no) : n_occ(no) {} - int cost (Var x) const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; } - bool operator()(Var x, Var y) const { return cost(x) < cost(y); } - }; - -class Solver { -protected: - // Solver state: - bool ok; // If FALSE,the constraints are already unsatisfiable. - // No part of solver state may be used! - vec<Clause*> clauses; // List of problem clauses. - vec<Clause*> learnts; // List of learnt clauses. - int n_bin_clauses; // Keep track of number of binary clauses "inlined" into the watcher lists (we do this primarily to get identical behavior to the version without the binary clauses trick). - double cla_inc; // Amount to bump next clause with. - double cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. - - vec<double> activity; // A heuristic measurement of the activity of a variable. - double var_inc; // Amount to bump next variable with. - double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. - VarOrder order; // Keeps track of the decision variable order. - vec<char> properties; // TODO: describe!!! - - vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). - vec<char> assigns; // The current assignments (lbool:s stored as char:s). - vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. - vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. - vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. - vec<TrailPos> trailpos; // 'trailpos[var]' contains the position in the trail at wich the assigment was made. - int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). - int simpDB_assigns; // Number of top-level assignments since last execution of 'simplifyDB()'. - int64 simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplifyDB()'. - vec<Lit> assumptions; // Current set of assumptions provided to solve by the user. - - bool subsumption; - vec<char> touched; - vec<vec<Clause*> > occurs; - vec<int> n_occ; - Heap<ElimLt> heap; - vec<Clause*> subsumption_queue; - - vec<Clause*> eliminated; - vec<int> eliminated_lim; - vec<Var> eliminated_var; - - // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is - // used, exept 'seen' wich is used in several places. - // - vec<char> seen; - vec<Lit> analyze_stack; - vec<Lit> analyze_toclear; - Clause* propagate_tmpempty; - Clause* propagate_tmpbin; - Clause* analyze_tmpbin; - Clause* bwdsub_tmpunit; - - vec<Lit> addBinary_tmp; - vec<Lit> addTernary_tmp; - - // Main internal methods: - // - bool assume (Lit p); - void cancelUntil (int level); - void record (const vec<Lit>& clause); - - void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) - bool analyze_removable(Lit p, uint min_level); // (helper method for 'analyze()') - void analyzeFinal (Lit p, vec<Lit>& out_conflict); - bool enqueue (Lit fact, Clause* from = NULL); - Clause* propagate (); - void reduceDB (); - Lit pickBranchLit (); - lbool search (int nof_conflicts, int nof_learnts); - double progressEstimate (); - - // Variable properties: - void setVarProp (Var v, uint prop, bool b) { order.setVarProp(v, prop, b); } - bool hasVarProp (Var v, uint prop) const { return order.hasVarProp(v, prop); } - void updateHeap (Var v) { - if (hasVarProp(v, p_frozen)) - heap.update(v); } - - // Simplification methods: - // - void cleanOcc (Var v) { - assert(subsumption); - vec<Clause*>& occ = occurs[v]; - int i, j; - for (i = j = 0; i < occ.size(); i++) - if (occ[i]->mark() != 1) - occ[j++] = occ[i]; - occ.shrink(i - j); - } - - vec<Clause*>& getOccurs (Var x) { cleanOcc(x); return occurs[x]; } - void gather (vec<Clause*>& clauses); - Lit subsumes (const Clause& c, const Clause& d); - bool assymmetricBranching (Clause& c); - bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause); - - bool backwardSubsumptionCheck (); - bool eliminateVar (Var v, bool fail = false); - bool eliminate (); - void extendModel (); - - // Activity: - // - void varBumpActivity(Lit p) { - if (var_decay < 0) return; // (negative decay means static variable order -- don't bump) - if ( (activity[var(p)] += var_inc) > 1e100 ) varRescaleActivity(); - order.update(var(p)); } - void varDecayActivity () { if (var_decay >= 0) var_inc *= var_decay; } - void varRescaleActivity(); - void claDecayActivity () { cla_inc *= cla_decay; } - void claRescaleActivity(); - - // Operations on clauses: - // - bool newClause(const vec<Lit>& ps, bool learnt = false, bool normalized = false); - void claBumpActivity (Clause& c) { if ( (c.activity() += cla_inc) > 1e20 ) claRescaleActivity(); } - bool locked (const Clause& c) const { return reason[var(c[0])] == &c; } - bool satisfied (Clause& c) const; - bool strengthen (Clause& c, Lit l); - void removeClause (Clause& c, bool dealloc = true); - - int decisionLevel() const { return trail_lim.size(); } - -public: - Solver() : ok (true) - , n_bin_clauses (0) - , cla_inc (1) - , cla_decay (1) - , var_inc (1) - , var_decay (1) - , order (assigns, activity) - , qhead (0) - , simpDB_assigns (-1) - , simpDB_props (0) - , subsumption (true) - , heap (n_occ) - , params () - , expensive_ccmin (true) - , verbosity (0) - , progress_estimate(0) - { - vec<Lit> dummy(2,lit_Undef); - propagate_tmpbin = Clause_new(dummy); - analyze_tmpbin = Clause_new(dummy); - dummy.pop(); - bwdsub_tmpunit = Clause_new(dummy); - dummy.pop(); - propagate_tmpempty = Clause_new(dummy); - addBinary_tmp .growTo(2); - addTernary_tmp.growTo(3); - } - - ~Solver() { - xfree(propagate_tmpbin); - xfree(analyze_tmpbin); - xfree(bwdsub_tmpunit); - xfree(propagate_tmpempty); - for (int i = 0; i < eliminated.size(); i++) xfree(eliminated[i]); - for (int i = 0; i < learnts.size(); i++) xfree(learnts[i]); - for (int i = 0; i < clauses.size(); i++) xfree(clauses[i]); } - - // Helpers: (semi-internal) - // - lbool value(Var x) const { return toLbool(assigns[x]); } - lbool value(Lit p) const { return sign(p) ? ~toLbool(assigns[var(p)]) : toLbool(assigns[var(p)]); } - - int nAssigns() { return trail.size(); } - int nClauses() { return clauses.size(); } - int nLearnts() { return learnts.size(); } - int nConflicts() { return (int)stats.conflicts; } - - // Statistics: (read-only member variable) - // - SolverStats stats; - - // Mode of operation: - // - SearchParams params; // Restart frequency etc. - bool expensive_ccmin; // Controls conflict clause minimization. TRUE by default. - int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - - // Problem specification: - // - Var newVar (bool polarity = true, bool dvar = true); - int nVars () { return assigns.size(); } - bool addUnit (Lit p) { return ok && (ok = enqueue(p)); } - bool addBinary (Lit p, Lit q) { addBinary_tmp [0] = p; addBinary_tmp [1] = q; return addClause(addBinary_tmp); } - bool addTernary(Lit p, Lit q, Lit r) { addTernary_tmp[0] = p; addTernary_tmp[1] = q; addTernary_tmp[2] = r; return addClause(addTernary_tmp); } - bool addClause (const vec<Lit>& ps) { if (ok && !newClause(ps)) ok = false; return ok; } - - // Variable mode: - // - void freezeVar (Var v) { setVarProp(v, p_frozen, true); updateHeap(v); } - - // Solving: - // - bool okay () { return ok; } // FALSE means solver is in a conflicting state - bool simplifyDB (bool expensive = true); - bool solve (const vec<Lit>& assumps); - bool solve () { vec<Lit> tmp; return solve(tmp); } - void turnOffSubsumption() { - subsumption = false; - occurs.clear(true); - n_occ.clear(true); - } - - double progress_estimate; // Set by 'search()'. - vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any). - vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions), this vector represent the conflict clause expressed in the assumptions. - - double returnActivity(int i) { return activity[i];} - void updateInitialActivity(int i, double act) {activity[i] = act; order.heap.update(i);} -}; - - -//================================================================================================= -// Debug: - - -#define L_LIT "%sx%d" -#define L_lit(p) sign(p)?"~":"", var(p) - -// Just like 'assert()' but expression will be evaluated in the release version as well. -inline void check(bool expr) { assert(expr); } - -static void printLit(Lit l) -{ - fprintf(stderr, "%s%d", sign(l) ? "-" : "", var(l)+1); -} - -template<class C> -static void printClause(const C& c) -{ - for (int i = 0; i < c.size(); i++){ - printLit(c[i]); - fprintf(stderr, " "); - } -} - -//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -#ifdef _MSC_VER - -#include <ctime> - -static inline double cpuTime(void) { - return (double)clock() / CLOCKS_PER_SEC; } - -static inline int64 memUsed() { - return 0; } - -//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -#else - -#include <sys/time.h> -#include <sys/resource.h> - -static inline double cpuTime(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } - -#if defined(__linux__) || defined(__CYGWIN__) -static inline int memReadStat(int field) -{ - char name[256]; - pid_t pid = getpid(); - sprintf(name, "/proc/%d/statm", pid); - FILE* in = fopen(name, "rb"); - if (in == NULL) return 0; - int value; - for (; field >= 0; field--) { - int res = fscanf(in, "%d", &value); - (void) res; - } - fclose(in); - return value; -} - -static inline int64 memUsed() { return (int64)memReadStat(0) * (int64)getpagesize(); } -#else -// use this by default. Mac OS X (Darwin) does not define an os type -//defined(__FreeBSD__) - -static inline int64 memUsed(void) { - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - return ru.ru_maxrss*1024; } - -#endif - -//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -#endif - -//================================================================================================= -} -#endif diff --git a/stp/sat/SolverTypes.h b/stp/sat/SolverTypes.h deleted file mode 100644 index fe15a968..00000000 --- a/stp/sat/SolverTypes.h +++ /dev/null @@ -1,132 +0,0 @@ -/***********************************************************************************[SolverTypes.h] -MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - - -#ifndef SolverTypes_h -#define SolverTypes_h - -#include "Global.h" - -namespace MINISAT { - -//================================================================================================= -// Variables, literals, clause IDs: - - -// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, -// so that they can be used as array indices. - -typedef int Var; -#define var_Undef (-1) - - -struct Lit { - int x; - - Lit() : x(2*var_Undef) { } // (lit_Undef) - explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { } -}; - -// Don't use these for constructing/deconstructing literals. Use the normal constructors instead. -inline int toInt (Lit p) { return p.x; } // A "toInt" method that guarantees small, positive integers suitable for array indexing. -inline Lit toLit (int i) { Lit p; p.x = i; return p; } // Inverse of 'toInt()' - -inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } -inline bool sign (Lit p) { return p.x & 1; } -inline int var (Lit p) { return p.x >> 1; } -inline Lit unsign (Lit p) { Lit q; q.x = p.x & ~1; return q; } -inline Lit id (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; } - -inline bool operator == (Lit p, Lit q) { return toInt(p) == toInt(q); } -inline bool operator != (Lit p, Lit q) { return toInt(p) != toInt(q); } -inline bool operator < (Lit p, Lit q) { return toInt(p) < toInt(q); } // '<' guarantees that p, ~p are adjacent in the ordering. - - -const Lit lit_Undef(var_Undef, false); // }- Useful special constants. -const Lit lit_Error(var_Undef, true ); // } - - -//================================================================================================= -// Clause -- a simple class for representing a clause: - -class Clause { - uint size_etc; - union { float act; uint abst; } apa; - Lit data[1]; -public: - // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). - template<class V> - Clause(const V& ps, bool learnt) { - size_etc = (ps.size() << 3) | (uint)learnt; - for (int i = 0; i < ps.size(); i++) data[i] = ps[i]; - if (learnt) apa.act = 0; else apa.abst = 0; } - - // -- use this function instead: - template<class V> - friend Clause* Clause_new(const V& ps, bool learnt = false) { - assert(sizeof(Lit) == sizeof(uint)); - assert(sizeof(float) == sizeof(uint)); - - size_t aux_size = 0; - if (ps.size() > 0) - aux_size = sizeof(uint)*(ps.size() - 1); - - void* mem = xmalloc<char>(sizeof(Clause) + aux_size); - return new (mem) Clause(ps, learnt); } - - int size () const { return size_etc >> 3; } - void shrink (int i) { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); } - void pop () { shrink(1); } - bool learnt () const { return size_etc & 1; } - uint mark () const { return (size_etc >> 1) & 3; } - void mark (uint m) { size_etc = (size_etc & ~6) | ((m & 3) << 1); } - Lit operator [] (int i) const { return data[i]; } - Lit& operator [] (int i) { return data[i]; } - - float& activity () { return apa.act; } - - uint abstraction () const { return apa.abst; } - - void calcAbstraction() { - uint abstraction = 0; - for (int i = 0; i < size(); i++) - abstraction |= 1 << (var(data[i]) & 31); - apa.abst = abstraction; } -}; - - -//================================================================================================= -// TrailPos -- Stores an index into the trail as well as an approximation of a level. This data -// is recorded for each assigment. (Replaces the old level information) - - -class TrailPos { - int tp; - public: - explicit TrailPos(int index, int level) : tp( (index << 5) + (level & 31) ) { } - - friend int abstractLevel(const TrailPos& p) { return 1 << (p.tp & 31); } - friend int position (const TrailPos& p) { return p.tp >> 5; } - - bool operator == (TrailPos other) const { return tp == other.tp; } - bool operator < (TrailPos other) const { return tp < other.tp; } -}; - -} -#endif diff --git a/stp/sat/Sort.h b/stp/sat/Sort.h deleted file mode 100644 index 9def2990..00000000 --- a/stp/sat/Sort.h +++ /dev/null @@ -1,133 +0,0 @@ -/******************************************************************************************[Sort.h] -MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#ifndef Sort_h -#define Sort_h - - -namespace MINISAT { -//================================================================================================= - - -template<class T> -struct LessThan_default { - bool operator () (T x, T y) { return x < y; } -}; - - -//================================================================================================= - - -template <class T, class LessThan> -void selectionSort(T* array, int size, LessThan lt) -{ - int i, j, best_i; - T tmp; - - for (i = 0; i < size-1; i++){ - best_i = i; - for (j = i+1; j < size; j++){ - if (lt(array[j], array[best_i])) - best_i = j; - } - tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; - } -} -template <class T> static inline void selectionSort(T* array, int size) { - selectionSort(array, size, LessThan_default<T>()); } - - -template <class T, class LessThan> -void sort(T* array, int size, LessThan lt, double& seed) -{ - if (size <= 15) - selectionSort(array, size, lt); - - else{ - T pivot = array[irand(seed, size)]; - T tmp; - int i = -1; - int j = size; - - for(;;){ - do i++; while(lt(array[i], pivot)); - do j--; while(lt(pivot, array[j])); - - if (i >= j) break; - - tmp = array[i]; array[i] = array[j]; array[j] = tmp; - } - - sort(array , i , lt, seed); - sort(&array[i], size-i, lt, seed); - } -} -template <class T, class LessThan> void sort(T* array, int size, LessThan lt) { - double seed = 91648253; sort(array, size, lt, seed); } -template <class T> static inline void sort(T* array, int size) { - sort(array, size, LessThan_default<T>()); } - - -template <class T, class LessThan> -void sortUnique(T* array, int& size, LessThan lt) -{ - int i, j; - T last; - - if (size == 0) return; - - sort(array, size, lt); - - i = 1; - last = array[0]; - for (j = 1; j < size; j++){ - if (lt(last, array[j])){ - last = array[i] = array[j]; - i++; } - } - - size = i; -} -template <class T> static inline void sortUnique(T* array, int& size) { - sortUnique(array, size, LessThan_default<T>()); } - - -//================================================================================================= -// For 'vec's: - - -template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) { - sort((T*)v, v.size(), lt); } -template <class T> void sort(vec<T>& v) { - sort(v, LessThan_default<T>()); } - - -template <class T, class LessThan> void sortUnique(vec<T>& v, LessThan lt) { - int size = v.size(); - T* data = v.release(); - sortUnique(data, size, lt); - v.~vec<T>(); - new (&v) vec<T>(data, size); } -template <class T> void sortUnique(vec<T>& v) { - sortUnique(v, LessThan_default<T>()); } - - -//================================================================================================= -} -#endif diff --git a/stp/sat/VarOrder.h b/stp/sat/VarOrder.h deleted file mode 100644 index 6d2a40f0..00000000 --- a/stp/sat/VarOrder.h +++ /dev/null @@ -1,146 +0,0 @@ -/**************************************************************************************[VarOrder.h] -MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ - -#ifndef VarOrder_h -#define VarOrder_h - -#include "SolverTypes.h" -#include "Solver.h" -#include "Heap.h" -#include "../AST/ASTUtil.h" - -namespace MINISAT { - //================================================================================================= - - struct VarOrder_lt { - const vec<double>& activity; - bool operator () (Var x, Var y) { return activity[x] > activity[y]; } - VarOrder_lt(const vec<double>& act) : activity(act) { } - }; - - - enum { p_decisionvar = 0, p_polarity = 1, p_frozen = 2, p_dontcare = 3 }; - - - class VarOrder { - const vec<char>& assigns; // var->val. Pointer to external assignment table. - const vec<double>& activity; // var->act. Pointer to external activity table. - vec<char> properties; - //Heap<VarOrder_lt> heap; - //double random_seed; // For the internal random number generator - - friend class VarFilter; - public: - //FIXME: Vijay: delete after experiments - Heap<VarOrder_lt> heap; - double random_seed; // For the internal random number generator - //FIXME ENDS HERE - - VarOrder(const vec<char>& ass, const vec<double>& act) : - assigns(ass), activity(act), heap(VarOrder_lt(act)), random_seed(2007) - //assigns(ass), activity(act), heap(VarOrder_lt(act)) - { } - - int size () { return heap.size(); } - void setVarProp (Var v, uint prop, bool b) { properties[v] = (properties[v] & ~(1 << prop)) | (b << prop); } - bool hasVarProp (Var v, uint prop) const { return properties[v] & (1 << prop); } - inline void cleanup (); - - inline void newVar(bool polarity, bool dvar); - inline void update(Var x); // Called when variable increased in activity. - inline void undo(Var x); // Called when variable is unassigned and may be selected again. - //Selects a new, unassigned variable (or 'var_Undef' if none exists). - inline Lit select(double random_freq =.0, int decision_level = 0); - }; - - - struct VarFilter { - const VarOrder& o; - VarFilter(const VarOrder& _o) : o(_o) {} - bool operator()(Var v) const { return toLbool(o.assigns[v]) == l_Undef && o.hasVarProp(v, p_decisionvar); } - //bool operator()(Var v) const { return toLbool(o.assigns[v]) == l_Undef; } - }; - - void VarOrder::cleanup() - { - VarFilter f(*this); - heap.filter(f); - } - - void VarOrder::newVar(bool polarity, bool dvar) - { - Var v = assigns.size()-1; - heap.setBounds(v+1); - properties.push(0); - setVarProp(v, p_decisionvar, dvar); - setVarProp(v, p_polarity, polarity); - undo(v); - } - - - void VarOrder::update(Var x) - { - if (heap.inHeap(x)) - heap.increase(x); - } - - - void VarOrder::undo(Var x) - { - if (!heap.inHeap(x) && hasVarProp(x, p_decisionvar)) - heap.insert(x); - } - - - Lit VarOrder::select(double random_var_freq, int decision_level) - { - Var next = var_Undef; - - if (drand(random_seed) < random_var_freq && !heap.empty()) - next = irand(random_seed,assigns.size()); - - // Activity based decision: - while (next == var_Undef || toLbool(assigns[next]) != l_Undef || !hasVarProp(next, p_decisionvar)) - if (heap.empty()){ - next = var_Undef; - break; - }else - next = heap.getmin(); - - //printing - if(BEEV::print_sat_varorder) { - if (next != var_Undef) { - BEEV::Convert_MINISATVar_To_ASTNode_Print(next, - decision_level, - hasVarProp(next, p_polarity)); - // fprintf(stderr,"var = %d, prop = %d, decision = %d, polarity = %d, frozen = %d\n", - // next+1, properties[next], hasVarProp(next, p_decisionvar), - // hasVarProp(next, p_polarity), hasVarProp(next, p_frozen)); - } - else - fprintf(stderr, "var = undef\n"); - } - - return next == var_Undef ? lit_Undef : Lit(next, hasVarProp(next, p_polarity)); - } - - - //================================================================================================= -} -#endif |