From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 26 Jan 2011 23:33:34 +0000 (+0000)
Subject: * Improvement. Add array read refinement to the quick statistics.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=cd34e83d5fc973bf8454618193d8eddd5c568bcb;p=francis%2Fstp.git

* Improvement. Add array read refinement to the quick statistics.
* Speedup. Cache more things when doing array read refinement.


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

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index d08383a..f45610c 100644
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -15,7 +15,7 @@
 #include "RunTimes.h"
 
 // BE VERY CAREFUL> Update the Category Names to match.
-std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation"};
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap", "Sending to SAT Solver", "Counter Example Generation","SAT Simplification", "Constant Bit Propagation","Array Read Refinement"};
 
 namespace BEEV
 {
diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index 59ced64..b27441b 100644
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -30,7 +30,8 @@ public:
       SendingToSAT,
       CounterExampleGeneration,
       SATSimplifying,
-      ConstantBitPropagation
+      ConstantBitPropagation,
+      ArrayReadRefinement
     };
 
   static std::string CategoryNames[];
diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index f868259..36b52bf 100644
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -47,6 +47,10 @@ namespace BEEV
 
 	ASTVec FalseAxiomsVec, RemainingAxiomsVec;
 
+	// NB. Because we stop this timer before entering the SAT solver, the count
+	// it produces isn't the number of times Array Read Refinement was entered.
+	bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement);
+
     //in these loops we try to construct Leibnitz axioms and add it to
     //the solve(). We add only those axioms that are false in the
     //current counterexample. we keep adding the axioms until there
@@ -64,6 +68,17 @@ namespace BEEV
     	// Make a vector of the read symbols.
     	ASTVec read_node_symbols;
     	read_node_symbols.reserve(listOfIndices.size());
+
+    	vector<Kind> jKind;
+    	jKind.reserve(listOfIndices.size());
+
+    	vector<ASTNode> concreteIndexes;
+    	concreteIndexes.reserve(listOfIndices.size());
+
+    	vector<ASTNode> concreteValues;
+    	concreteValues.reserve(listOfIndices.size());
+
+
     	for (int i = 0; i < listOfIndices.size(); i++)
     	{
         	const ASTNode& the_index = listOfIndices[i];
@@ -75,6 +90,10 @@ namespace BEEV
         	assert ((SYMBOL == arrsym.GetKind() || BVCONST == arrsym.GetKind()));
 
         	read_node_symbols.push_back(arrsym);
+        	jKind.push_back(listOfIndices[i].GetKind());
+
+        	concreteIndexes.push_back(TermToConstTermUsingModel(the_index));
+        	concreteValues.push_back(TermToConstTermUsingModel(arrsym));
     	}
 
         //loop over the list of indices for the array and create LA,
@@ -82,6 +101,7 @@ namespace BEEV
         for (int i = 0; i < listOfIndices.size(); i++)
           {
         	const ASTNode& index_i = listOfIndices[i];
+        	const Kind iKind = index_i.GetKind();
 
             // Create all distinct pairs of indexes.
             for (int j = i+1; j < listOfIndices.size(); j++)
@@ -90,14 +110,12 @@ namespace BEEV
 
             	// If the index is a constant, and different, then there's no reason to check.
             	// Sometimes we get the same index stored multiple times in the array. Not sure why...
-            	if (BVCONST == index_i.GetKind() && index_j.GetKind() == BVCONST && index_i != index_j)
+            	if (BVCONST == iKind && jKind[j] == BVCONST && index_i != index_j)
             	{
-            		assert(index_i != index_j);
             		continue;
             	}
 
-
-                //prepare for SAT LOOP
+            	//prepare for SAT LOOP
                 //first construct the antecedent for the LA axiom
                 ASTNode eqOfIndices = 
                   (exprless(index_i, index_j)) ? 
@@ -111,9 +129,12 @@ namespace BEEV
                 //construct appropriate Leibnitz axiom
                 ASTNode LeibnitzAxiom = 
                   bm->CreateNode(IMPLIES, eqOfIndices, eqOfReads);
-                if (ASTFalse == ComputeFormulaUsingModel(LeibnitzAxiom))
+                if (concreteIndexes[i] == concreteIndexes[j] && concreteValues[i] != concreteValues[j])
                   {
                     FalseAxiomsVec.push_back(LeibnitzAxiom);
+                    //cerr << "index:" << index_i << " " <<  index_j;
+                    //cerr << read_node_symbols[i];
+                    //cerr << read_node_symbols[j];
                   }
                 else
                   {
@@ -127,6 +148,7 @@ namespace BEEV
 				  bm->CreateNode(AND, FalseAxiomsVec) : FalseAxiomsVec[0];
 				bm->ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms);
 				SOLVER_RETURN_TYPE res2;
+				bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement);
 				res2 =  CallSAT_ResultCheck(SatSolver,
 									  FalseAxioms,
 									  original_input,
@@ -137,7 +159,8 @@ namespace BEEV
 				  {
 					return res2;
 				  }
-				}
+				bm->GetRunTimes()->start(RunTimes::ArrayReadRefinement);
+            }
           }
       }
     if (RemainingAxiomsVec.size() > 0)
@@ -147,9 +170,11 @@ namespace BEEV
 						RemainingAxiomsVec) : RemainingAxiomsVec[0];
 		bm->ASTNodeStats("adding remaining readaxioms to SAT: ",
 				RemainingAxioms);
+		bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement);
 		return CallSAT_ResultCheck(SatSolver, RemainingAxioms, original_input,
 				tosat);
 	}
+	bm->GetRunTimes()->stop(RunTimes::ArrayReadRefinement);
     return SOLVER_UNDECIDED;
   } //end of SATBased_ArrayReadRefinement