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 df26d6e2357aacbb85430e687b2bdc29e5a55d78..87a9d73b4203fabdfeece20f6950f1eb9873442c 100644 (file)
--- 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 57bb88b962e6fff124978e0627d5181794e95b0f..62bbbbd5788a7cda2ad2b2336ffdcff6dc990c28 100644 (file)
--- 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 acae00ebd796c86f82073598ce31f00a0c8ae8ab..bd1098649b5c95fc19d29b08676d717b0da2c541 100644 (file)
--- 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<Lit>& i, const vec<Lit>& 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<Lit>& i, const vec<Lit>& 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<uint64_t, std::vector<ArrayAccess*> >* t = new Map<uint64_t, std::vector<ArrayAccess*>  > [number_of_arrays];
+            Map<index_type, std::vector<ArrayAccess*> >* t = new Map<index_type, std::vector<ArrayAccess*>  > [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<ArrayAccess*>());
@@ -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<uint64_t> toRep;
+       vec<index_type> toRep;
        vec<ArrayAccess*> aaRep;
 
        vec<ArrayAccess*> 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<ArrayAccess*>& 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 68b86db6ad7950d4a0e62a0bc19875da376b9ea1..a465932026df04480f8b85619ae63d82845b2921 100644 (file)
--- 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<uint64_t, std::vector<ArrayAccess*> >* val_to_aa; // Maps from the index value of fixed indexes to the array accesses.
+       Map<index_type, std::vector<ArrayAccess*> >* val_to_aa; // Maps from the index value of fixed indexes to the array accesses.
        Map<Var, std::vector<ArrayAccess*> > watchedLiterals; // The literals that are watched.
        vec<ArrayAccess*> toAddAtStartup;        // These need to be added in at startup.
        vec<ArrayHistory> 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 1dc48c1894a1e8e8e172b3959091e08569338044..4e818b6cf22fe275dace9a97179e9cec056faaf1 100644 (file)
--- 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<Minisat::lbool> 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<unsigned>& v = it->second;