From: trevor_hansen Date: Mon, 28 Nov 2011 02:55:18 +0000 (+0000) Subject: Improvement. Allow 128-bit indices with a compile time flag. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9772a5c8e09f47f97013e559bbb8b60aa9564903;p=francis%2Fstp.git Improvement. Allow 128-bit indices with a compile time flag. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1424 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index df26d6e..87a9d73 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -13,7 +13,11 @@ OPTIMIZE = -O3 -DNDEBUG -march=native -fomit-frame-pointer # Optimization #OPTIMIZE = -O3 -g # Debug -#CFLAGS_M32 = -m32 +# To enable 128-bit indices in the array propagators. Put the INDICES_128BITS +# option into CFLAGS_M32. Weird I know. +#CFLAGS_M32 = -DINDICES_128BITS +#CFLAGS_M32 = -m32 + CFLAGS_BASE += $(OPTIMIZE) ifeq ($(WITHCBITP),yes) diff --git a/src/sat/Makefile b/src/sat/Makefile index 57bb88b..62bbbbd 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -6,7 +6,7 @@ OBJS = $(SRCS:.cpp=.o) LIB = libminisat.a # exported variables override those set in recursive makefiles. -export COPTIMIZE=$(CFLAGS_M32) $(CFLAGS_FPIC) -O3 +export COPTIMIZE=$(CFLAGS_M32) $(CFLAGS_FPIC) -O3 .PHONY:core diff --git a/src/sat/core_prop/Solver_prop.cc b/src/sat/core_prop/Solver_prop.cc index acae00e..bd10986 100644 --- a/src/sat/core_prop/Solver_prop.cc +++ b/src/sat/core_prop/Solver_prop.cc @@ -171,6 +171,18 @@ Solver_prop::addArray(int array_id, const vec& i, const vec& v, const if (!ok) return false; + if (i.size() > INDEX_BIT_WIDTH || ki.size() > INDEX_BIT_WIDTH) + { + printf("The array propagators unfortunately don't do arbitrary precision integers yet. " + "With the INDICES_128BITS compile time flag STP does 128-bits on 64-bit machines compiled with GCC. " + "Currently STP is compiled to use %d bit indices. " + "Unfortunately your problem has array indexes of size %d bits. " + "STP does arbitrary precision indices with the '--oldstyle-refinement' or the '-r' flags.\n", + INDEX_BIT_WIDTH, std::max(i.size(), ki.size())); + exit(1); + } + + bool startOfNewArray = false; if (array_id != last_id) { @@ -179,7 +191,7 @@ Solver_prop::addArray(int array_id, const vec& i, const vec& v, const // Map doesn't have a copy constructor, so we create one on the heap. // Some constant indexes will already have been copied into the val_to_aa map. - Map >* t = new Map > [number_of_arrays]; + Map >* t = new Map > [number_of_arrays]; for (int j=0; j < number_of_arrays-1 ; j++) val_to_aa[j].moveTo(t[j]); @@ -279,14 +291,14 @@ void Solver_prop::startWatchOfIndexVariable(ArrayAccess* iv) // Reads out the array index as an integer. It is completely specified. -uint64_t +index_type Solver_prop::index_as_int(const ArrayAccess& iv) { if (iv.isIndexConstant()) return iv.constantIndex(); - uint64_t t = 0; - assert(64 >= iv.indexSize()); + index_type t = 0; + assert(INDEX_BIT_WIDTH >= iv.indexSize()); for (int i = 0; i < iv.indexSize(); i++) { @@ -514,7 +526,7 @@ Solver_prop::writeOutArrayAxiom(ArrayAccess& iv) { assert(IndexIsSet(iv)); - const uint64_t asInt = index_as_int(iv); + const index_type asInt = index_as_int(iv); if (!val_to_aa[iv.array_id].has(asInt)) val_to_aa[iv.array_id].insert(asInt, std::vector()); @@ -894,11 +906,11 @@ void Solver_prop::cancelUntil(int level) { struct to_re_add { - uint64_t index_value; + index_type index_value; int array_id; }; - vec toRep; + vec toRep; vec aaRep; vec toReAdd; @@ -912,7 +924,7 @@ void Solver_prop::cancelUntil(int level) { assert(IndexIsSet(aa)); // The index shouldn't be unset yet. // Get the integer. - uint64_t asInt = index_as_int(aa); + index_type asInt = index_as_int(aa); assert(val_to_aa[aa.array_id].has(asInt)); std::vector& aaV = val_to_aa[aa.array_id][asInt]; @@ -946,7 +958,7 @@ void Solver_prop::cancelUntil(int level) { // The zeroeth of these numbers has been deleted, so we might need to redo the implications. for (int i=0; i < toRep.size(); i++) { - uint64_t asInt = toRep[i]; + index_type asInt = toRep[i]; ArrayAccess& aa = *aaRep[i]; if (val_to_aa[aa.array_id].has(asInt)) diff --git a/src/sat/core_prop/Solver_prop.h b/src/sat/core_prop/Solver_prop.h index 68b86db..a465932 100644 --- a/src/sat/core_prop/Solver_prop.h +++ b/src/sat/core_prop/Solver_prop.h @@ -31,6 +31,17 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace Minisat { +// Use the GCC extension to use 128-bit indices. +#ifdef INDICES_128BITS + typedef unsigned int uint128_t __attribute__((mode(TI))); + static inline uint32_t hash(uint128_t x){ return (uint32_t)x; } + typedef uint128_t index_type; +#else + typedef uint64_t index_type; +#endif + +#define INDEX_BIT_WIDTH (sizeof(index_type) *8) + //================================================================================================= // Solver -- the main class: @@ -132,7 +143,7 @@ private: const bool is_value_constant; // Whether the value is a constant at the start. const bool is_index_constant; - uint64_t index_constant; + index_type index_constant; public: //The index/value is entirely known in advance. @@ -165,7 +176,7 @@ private: if (is_index_constant) { - assert(index_size <=64); + assert(index_size <=INDEX_BIT_WIDTH); for (int i = 0; i < index_size; i++) { lbool v = constant_index[i]; @@ -175,7 +186,7 @@ private: } } } - uint64_t constantIndex() const + index_type constantIndex() const { assert (is_index_constant); return index_constant; @@ -258,7 +269,7 @@ private: lbool accessIndex(const ArrayAccess& iv, int i); lbool accessValue(const ArrayAccess& iv, int i); - uint64_t index_as_int(const ArrayAccess& iv); + index_type index_as_int(const ArrayAccess& iv); void startWatchOfIndexVariable(ArrayAccess* iv); @@ -287,7 +298,7 @@ private: int top_level_var; int alternate_trail_sorted_to; - Map >* val_to_aa; // Maps from the index value of fixed indexes to the array accesses. + Map >* val_to_aa; // Maps from the index value of fixed indexes to the array accesses. Map > watchedLiterals; // The literals that are watched. vec toAddAtStartup; // These need to be added in at startup. vec arrayHistory_stack; // When the index is fixed it's added into here. diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index 1dc48c1..4e818b6 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -162,10 +162,6 @@ namespace BEEV SATSolver::vec_literals index; Minisat::vec index_constants; const int index_width = arr_it->first.GetValueWidth(); - if (index_width > 64) - FatalError("The array propagators unfortunately don't do arbitary precision integers yet." - " They use 64-bit integers internally to store values. Your problem has array indexes > 64 bits." - " Until this is fixed you need to run STP with the '--oldstyle-refinement' or the '-r' flag."); if (it != nodeToSATVar.end()) { const vector& v = it->second;