Improvement. Add another form of Ackermannisation. Not currently enabled.

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

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index f442c33bc35d7d8d04369c7083ee48aef672a936..565b0bc6d13114530534b04d40161f62435a2ffe 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -138,6 +138,10 @@ namespace BEEV
                                  const ASTNode& original_input,
                                  ToSATBase* tosat);
 
+    void
+    applyAllCongruenceConstraints(SATSolver & SatSolver, ToSATBase *tosat);
+
+
 #if 0
     SOLVER_RETURN_TYPE 
     SATBased_ArrayWriteRefinement(SATSolver& newS,

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 3209b6e4fa4fc93606a21903c31da9c6a2879ad4..9b4cdf9fcb37fd0b5b85f3e79d61ee2aeb772f8a 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -501,4 +501,90 @@ namespace BEEV
     return arraywrite_axiom;
   }//end of Create_ArrayWriteAxioms()
 #endif
+
+  // This is another way of performing Ackermannisation.
+  void
+  AbsRefine_CounterExample::applyAllCongruenceConstraints(SATSolver & SatSolver, ToSATBase *tosat)
+  {
+    //if (bm->UserFlags.stats_flag)
+      cerr << "~CNF~" << endl;
+
+    vector<pair<ASTNode, ArrayTransformer::arrTypeMap> > arrayToIndex;
+    arrayToIndex.insert(arrayToIndex.begin(), ArrayTransform->arrayToIndexToRead.begin(),
+        ArrayTransform->arrayToIndexToRead.end());
+
+    ToSATBase::ASTNodeToSATVar & satVar = tosat->SATVar_to_SymbolIndexMap();
+
+    //for each array, fetch its list of indices seen so far
+    for (vector<pair<ASTNode, ArrayTransformer::arrTypeMap> >::const_iterator iset = arrayToIndex.begin(), iset_end =
+        arrayToIndex.end(); iset != iset_end; iset++)
+      {
+      //const ASTNode& ArrName = iset->first;
+      const map<ASTNode, ArrayTransformer::ArrayRead>& mapper = iset->second;
+
+      vector<ASTNode> listOfIndices;
+      listOfIndices.reserve(mapper.size());
+
+      // Make a vector of the read symbols.
+      ASTVec read_node_symbols;
+      read_node_symbols.reserve(listOfIndices.size());
+
+      vector<Kind> jKind;
+      jKind.reserve(mapper.size());
+
+      ASTVec index_symbols;
+      index_symbols.reserve(mapper.size());
+
+      for (map<ASTNode, ArrayTransformer::ArrayRead>::const_iterator it = mapper.begin();
+          it != mapper.end(); it++)
+        {
+        const ASTNode& the_index = it->first;
+        listOfIndices.push_back(the_index);
+
+        ASTNode arrsym = it->second.symbol;
+        read_node_symbols.push_back(arrsym);
+
+        index_symbols.push_back(it->second.index_symbol);
+
+        assert(read_node_symbols[0].GetValueWidth() == arrsym.GetValueWidth());
+        assert(listOfIndices[0].GetValueWidth() == the_index.GetValueWidth());
+
+        jKind.push_back(the_index.GetKind());
+        }
+
+      assert(listOfIndices.size() == mapper.size());
+
+      //loop over the list of indices for the array and create LA,
+      //and add to inputAlreadyInSAT
+      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++)
+          {
+          const ASTNode& index_j = listOfIndices[j];
+
+          // 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 == iKind && jKind[j] == BVCONST && index_i != index_j)
+            continue;
+
+          if (ASTFalse == simp->CreateSimplifiedEQ(index_i, index_j))
+            continue; // shortcut.
+
+          if (index_i == index_j)
+            cerr << "EQUAL";
+
+          AxiomToBe o(index_symbols[i], index_symbols[j], read_node_symbols[i], read_node_symbols[j]);
+
+          applyAxiomToSAT(SatSolver, o, satVar);
+          }
+        }
+      }
+  }
+
+
+
 };// end of namespace BEEV