Fresh variables created for internal uses, for instance to replace READs during abstr...

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

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index f3b0daebec218b5aa924e3ef7892227b9f7bd729..78c86911f3abe60d27113f1337e1b649e70de722 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -587,7 +587,6 @@ namespace BEEV
                                  "array_" + string(arrName.GetName()));
 
                  Arrayread_SymbolMap[processedTerm] = CurrentSymbol;
-              Introduced_SymbolsSet.insert(CurrentSymbol);
             }
 
           ASTNode ite = CurrentSymbol;

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index c941b43d8fd4860e2a89c03e05e4e5f33af39ad5..c9bf61aade7386000628bfc8d23c9d2422ed3cda 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -55,9 +55,7 @@ namespace BEEV
     // Read(A,j) is replaced with the following ITE: ITE(i=j,v1,v2)
     ASTNodeMap * Arrayread_IteMap;
           
-    // Set of new symbols introduced that replace the array read terms
-    ASTNodeSet Introduced_SymbolsSet;
-    
+
     // Count to keep track of new symbolic constants introduced
     // corresponding to Array Reads
     unsigned int _symbol_count;
@@ -117,7 +115,6 @@ namespace BEEV
     // Constructor
     ArrayTransformer(STPMgr * bm, Simplifier* s) : 
       Arrayread_SymbolMap(),
-      Introduced_SymbolsSet(),
       bm(bm), 
       simp(s), 
       debug_transform(0),
@@ -139,7 +136,6 @@ namespace BEEV
     {
       Arrayread_IteMap->clear();
       delete Arrayread_IteMap;
-      Introduced_SymbolsSet.clear();
       ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin();
       ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end();
       for(;it!=itend;it++)
@@ -175,14 +171,6 @@ namespace BEEV
       return (*Arrayread_IteMap)[arrread];
     } //End of ArrayRead_Ite
 
-    bool FoundIntroducedSymbolSet(const ASTNode& in)
-    {
-      if(Introduced_SymbolsSet.find(in) != Introduced_SymbolsSet.end())
-        {
-          return true;
-        }
-      return false;
-    } // End of IntroduceSymbolSet
 
     void ClearAllTables(void)
     {
@@ -198,7 +186,6 @@ namespace BEEV
       Arrayname_ReadindicesMap->clear();
       Arrayread_SymbolMap.clear();
       Arrayread_IteMap->clear();
-      Introduced_SymbolsSet.clear();
     }
   }; //end of class Transformer
 

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 9273511680faafad564ab15d4c7f9c0a106212cb..d20a787d510fb8add128f743472816a3586599bd 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -639,20 +639,6 @@ namespace BEEV
     return newn;
   }
 
-  //Create a new variable of ValueWidth 'n'
-  ASTNode STPMgr::NewVar(unsigned int n)
-  {
-    std::string c("v");
-    char d[32];
-    sprintf(d, "%d", _symbol_count++);
-    std::string ccc(d);
-    c += "_solver_" + ccc;
-
-    ASTNode CurrentSymbol = CreateSymbol(c.c_str(),0,n);
-    assert(0 !=n);
-    return CurrentSymbol;
-  } //end of NewVar()
-
   bool STPMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
   {
     if (READ == term.GetKind() 

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index da455a87956a700b6c97cb24c164ff3efc06d70d..6e63371048f5e66e5b1f563c88069579157579ef 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -133,6 +133,9 @@ namespace BEEV
     ASTVec ones;
     ASTVec max;
 
+    // Set of new symbols introduced that replace the array read terms
+    ASTNodeSet Introduced_SymbolsSet;
+
   public:
     
     /****************************************************************
@@ -383,18 +386,28 @@ namespace BEEV
     // Print assertions to the input stream
     void printAssertsToStream(ostream &os, int simplify);
 
-    // Create New Variables
-    ASTNode NewVar(unsigned int n);
-
+    // Variables are added automatically to the introduced_symbolset. Variables
+    // in the set aren't printed out as part of the counter example.
     ASTNode CreateFreshVariable(int indexWidth, int valueWidth, std::string prefix)
     {
         char d[32 + prefix.length()];
         sprintf(d, "%s_%d", prefix.c_str(), _symbol_count++);
 
         BEEV::ASTNode CurrentSymbol = CreateSymbol(d,indexWidth,valueWidth);
+        Introduced_SymbolsSet.insert(CurrentSymbol);
         return CurrentSymbol;
     }
 
+    bool FoundIntroducedSymbolSet(const ASTNode& in)
+    {
+      if(Introduced_SymbolsSet.find(in) != Introduced_SymbolsSet.end())
+        {
+          return true;
+        }
+      return false;
+    } // End of IntroduceSymbolSet
+
+
 
     bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
 
@@ -406,6 +419,8 @@ namespace BEEV
       TermsAlreadySeenMap.clear();
     }
 
+    // This is called before SAT solving, so only junk that isn't needed
+    // after SAT solving should be cleaned out.
     void ClearAllTables(void) 
     {
       NodeLetVarMap.clear();

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index ffcc5af49ca6f2562d7b4214f1c982f47e36c76d..dfdf03f5d8b944c632fd9d25daa9f1d187f635e9 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -745,7 +745,7 @@ namespace BEEV
           }
 
         //skip over introduced variables
-        if (f.GetKind() == SYMBOL && (ArrayTransform->FoundIntroducedSymbolSet(
+        if (f.GetKind() == SYMBOL && (bm->FoundIntroducedSymbolSet(
             f)))
           {
             continue;

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index ca2754066de48c9ec4b39bad104b5d455575365d..91e39bedbd75c826466303e941e507ea178d8684 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -457,7 +457,7 @@ namespace BEEV
           //then also add another entry for x = x1@t
           ASTNode var = lhs[0];
           ASTNode newvar = 
-            _bm->NewVar(var.GetValueWidth() - lhs.GetValueWidth());
+            _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs.GetValueWidth(), "v_solver");
           newvar = 
             _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs);
                          assert(BVTypeCheck(newvar));
@@ -528,8 +528,9 @@ namespace BEEV
           if (ChosenVar_Is_Extract)
             {
               const ASTNode& var = lhs[1][0];
+
               ASTNode newvar = 
-                _bm->NewVar(var.GetValueWidth() - lhs[1].GetValueWidth());
+                  _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs[1].GetValueWidth(), "v_solver");
               newvar = 
                 _bm->CreateTerm(BVCONCAT, 
                                 var.GetValueWidth(), 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 20efa8e88944cfc0dccdfe5dd8bf7f27a78c86a2..3961f92b165b005f8766760ffdfffaed64c00852 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -3597,7 +3597,7 @@ namespace BEEV
         ASTNode newVar;
         if (!CheckSimplifyMap(input, newVar, false))
           {
-            newVar = _bm->NewVar(input.GetValueWidth());
+            newVar = _bm->CreateFreshVariable(0,input.GetValueWidth(),"v_solver");
             (*ReadOverWrite_NewName_Map)[input] = newVar;
             NewName_ReadOverWrite_Map[newVar] = input;