From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 25 May 2012 13:36:17 +0000 (+0000)
Subject: Remove unnecessary code when cancelling. Thanks to Graeme Gange for pointing this... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5ef633328adb1112c82b8de9da4bee5dd5855b10;p=francis%2Fstp.git

Remove unnecessary code when cancelling. Thanks to Graeme Gange for pointing this out.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1660 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/sat/core_prop/Solver_prop.cc b/src/sat/core_prop/Solver_prop.cc
index 6a89472..5b7f229 100644
--- a/src/sat/core_prop/Solver_prop.cc
+++ b/src/sat/core_prop/Solver_prop.cc
@@ -910,68 +910,37 @@ void Solver_prop::cancelUntil(int level) {
 	    int array_id;
 	};
 
-	vec<index_type> toRep;
-	vec<ArrayAccess*> aaRep;
 
 	vec<ArrayAccess*> toReAdd;
 
         // look through the map, and remove it.
         while ((arrayHistory_stack.size() > 0) && (arrayHistory_stack.last().decisionLevel > level))
         {
-        	ArrayAccess& aa = *(arrayHistory_stack.last().aa);
-                assert(aa.known_index);
-                assert(!aa.isIndexConstant()); // Shouldn't remove known indexes.
-                assert(IndexIsSet(aa));   // The index shouldn't be unset yet.
+          ArrayAccess& aa = *(arrayHistory_stack.last().aa);
+          assert(aa.known_index);
+          assert(!aa.isIndexConstant());
+          // Shouldn't remove known indexes.
+          assert(IndexIsSet(aa));
+          // The index shouldn't be unset yet.
 
-        	// Get the integer.
-                index_type asInt = index_as_int(aa);
-        	assert(val_to_aa[aa.array_id].has(asInt));
+          // Get the integer.
+          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];
+          std::vector<ArrayAccess*>& aaV = val_to_aa[aa.array_id][asInt];
+          assert(aaV.size() >0);
+          assert(aaV.back() == &aa);
 
-        	// We'll remove the zeroeth array access, so need to re-add all of the array axioms.
-                if (aaV[0] == &aa)
-                    {
-                        toRep.push(asInt);
-                        aaRep.push(&aa);
-                    }
-
-                bool found = false;
-                for (int i = 0; i < (int) aaV.size(); i++)
-                    if (aaV[i] == &aa)
-                        {
-                            //Find the same pointer and erase it.
-                            aaV.erase(aaV.begin() + i);
-                            found = true;
-                            break;
-                        }
-                assert(found);
+          aaV.erase(aaV.begin() + (aaV.size() - 1));
 
-                    if (aaV.size() == 0)
-                        val_to_aa[aa.array_id].remove(asInt);
+          if (aaV.size() == 0)
+            val_to_aa[aa.array_id].remove(asInt);
 
-                    aa.known_index = false;
-                    toReAdd.push(&aa);
-                    arrayHistory_stack.shrink(1);
-                }
+          aa.known_index = false;
+          toReAdd.push(&aa);
+          arrayHistory_stack.shrink(1);
+        }
 
-	// The zeroeth of these numbers has been deleted, so we might need to redo the implications.
-	for (int i=0; i < toRep.size(); i++)
-	{
-	        index_type asInt = toRep[i];
-	        ArrayAccess& aa = *aaRep[i];
-
-	        if (val_to_aa[aa.array_id].has(asInt))
-	            {
-
-	                std::vector<ArrayAccess*>& aaV = val_to_aa[aa.array_id][asInt];
-	                for (int j=1;j<(int)aaV.size();j++)
-	                {
-	                        assert(aa.known_index);
-	                        writeOutArrayAxiom(*aaV[j]);
-	                }
-	            }
-	}
 
 	sortAlternateTrail();
         while (alternate_trail.size() > 0 && (alternate_trail.back().decisionLevel > level))