Fixes / Improvements.

* Fix. No longer create NOT(NOT(..)) nodes because their node numbers aren't unique.
* Improvement. Change the AlwaysTrueFormMap (which was a set), to use node numbers ---which allows the nodes to be garbage collected.

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

diff --git a/src/AST/NodeFactory/HashingNodeFactory.cpp b/src/AST/NodeFactory/HashingNodeFactory.cpp
index e584ac779305c2ec489570685aba444899c9abbb..198b1fa6cbea9a77f17983fec3441e252b3f1485 100644 (file)
--- a/src/AST/NodeFactory/HashingNodeFactory.cpp
+++ b/src/AST/NodeFactory/HashingNodeFactory.cpp
@@ -26,6 +26,12 @@ BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind,        const BEEV::ASTVec
                SortByArith(children);
        }
 
+       // We can't create NOT(NOT (..)) nodes because of how the numbering scheme we use works.
+       // So you can't trust the hashiing node factory even to return nodes of the same kind that
+       // you ask for.
+       if (kind == BEEV::NOT && children[0].GetKind() == BEEV::NOT)
+         return children[0][0];
+
        // insert all of children at end of new_children.
        ASTNode n(bm.CreateInteriorNode(kind, n_ptr, children));
        return n;

diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 31c1527bd573e1abb67de6cdef42b6b3e465b45c..dd8c134c3ab747e96deecbcf2ced2ac25c04c643 100644 (file)
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -27,7 +27,11 @@ namespace BEEV
         // have alpha.nodenum + 1.
         if (n_ptr->GetKind() == NOT)
           {
-            n_ptr->SetNodeNum(n_ptr->GetChildren()[0].GetNodeNum() + 1);
+               // The internal node can't be a NOT, because then we'd add
+               // 1 to the NOT's node number, meaning we'd hit an even number,
+               // which could duplicate the next newNodeNum().
+               assert(n_ptr->GetChildren()[0].GetKind() != NOT);
+                       n_ptr->SetNodeNum(n_ptr->GetChildren()[0].GetNodeNum() + 1);
           }
         else
           {

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index a6e2565f599c662c57917518736c3f6f964604a5..932811dd5f1b8d6767a0d04dd30c07bacd9d5e67 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -74,6 +74,12 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
   if (CheckSubstitutionMap(a, output))
     return output;
 
+  if (!alreadyVisited.insert(a.GetNodeNum()).second)
+  {
+    return a;
+  }
+
+
   //traverse a and populate the SubstitutionMap
   const Kind k = a.GetKind();
   if (SYMBOL == k && BOOLEAN_TYPE == a.GetType())
@@ -162,7 +168,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
              it = c.begin(), itend = c.end();
            it != itend; it++)
         {
-          simp->UpdateAlwaysTrueFormMap(*it);
+          simp->UpdateAlwaysTrueFormSet(*it);
           ASTNode aaa = CreateSubstitutionMap(*it,at);
 
           if (ASTTrue != aaa)

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 5c2bac1912721727619cb0e9b1bb843162b20bbe..ad40590640fb440149235a9b72dd5d9d1a64464b 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -31,6 +31,7 @@ class SubstitutionMap {
        ASTNodeSet rhs; // All the rhs that have been seeen.
        set<ASTNodeSet*> rhsAlreadyAdded;
        VariablesInExpression::SymbolPtrSet rhs_visited; // the rhs contains all the variables in here already.
+       HASHSET<int> alreadyVisited;
 
        int loopCount;
 
@@ -68,6 +69,7 @@ public:
        {
                SolverMap->clear();
                haveAppliedSubstitutionMap();
+               alreadyVisited.clear();
        }
 
        virtual ~SubstitutionMap();
@@ -83,7 +85,6 @@ public:
                return false;
        }
 
-
        //update solvermap with (key,value) pair
        bool UpdateSolverMap(const ASTNode& key, const ASTNode& value) {
                ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key;

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 1cffce5da3663baf56a7e7143595879d13dbb02d..a2d18991435fe4ce462cb97b2c47cc099c0565e2 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -180,24 +180,17 @@ namespace BEEV
     MultInverseMap[key] = value;
   }
 
-  bool Simplifier::CheckAlwaysTrueFormMap(const ASTNode& key)
+  bool Simplifier::CheckAlwaysTrueFormSet(const ASTNode& key)
   {
-    ASTNodeSet::iterator it = AlwaysTrueFormMap.find(key);
-    ASTNodeSet::iterator itend = AlwaysTrueFormMap.end();
+    HASHSET<int>::const_iterator it2 = AlwaysTrueHashSet.find(key.GetNodeNum());
+    HASHSET<int>::const_iterator it_end_2 = AlwaysTrueHashSet.end();
 
-    if (it != itend)
-      {
-        //cerr << "found:" << *it << endl;
-        CountersAndStats("Successful_CheckAlwaysTrueFormMap", _bm);
-        return true;
-      }
-
-    return false;
+    return  it2 != it_end_2;
   }
 
-  void Simplifier::UpdateAlwaysTrueFormMap(const ASTNode& key)
+  void Simplifier::UpdateAlwaysTrueFormSet(const ASTNode& key)
   {
-    AlwaysTrueFormMap.insert(key);
+         AlwaysTrueHashSet.insert(key.GetNodeNum());
   }
 
   ASTNode 
@@ -1050,13 +1043,13 @@ namespace BEEV
       return t2;
     if (t1 == t2)
       return t1;
-    if (CheckAlwaysTrueFormMap(t0))
+    if (CheckAlwaysTrueFormSet(t0))
       {
         return t1;
       }
-    if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, t0))
+    if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0))
         || (NOT == t0.GetKind() 
-            && CheckAlwaysTrueFormMap(t0[0])))
+            && CheckAlwaysTrueFormSet(t0[0])))
       {
         return t2;
       }
@@ -1082,13 +1075,13 @@ namespace BEEV
           return t2;
         if (t1 == t2)
           return t1;
-        if (CheckAlwaysTrueFormMap(t0))
+        if (CheckAlwaysTrueFormSet(t0))
           {
             return t1;
           }
-        if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, t0))
+        if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0))
             || (NOT == t0.GetKind() 
-                && CheckAlwaysTrueFormMap(t0[0])))
+                && CheckAlwaysTrueFormSet(t0[0])))
           {
             return t2;
           }
@@ -1228,7 +1221,7 @@ namespace BEEV
     //pushnegation if there are odd number of NOTs
     bool pn = (NotCount % 2 == 0) ? false : true;
 
-    if (CheckAlwaysTrueFormMap(o))
+    if (CheckAlwaysTrueFormSet(o))
       {
         output = pn ? ASTFalse : ASTTrue;
         return output;
@@ -1393,24 +1386,24 @@ namespace BEEV
           {
             output = ASTTrue;
           }
-        else if (CheckAlwaysTrueFormMap(c0))
+        else if (CheckAlwaysTrueFormSet(c0))
           {
             // c0 AND (~c0 OR c1) <==> c1
             //
             //applying modus ponens
             output = c1;
           }
-        else if (CheckAlwaysTrueFormMap(c1) || 
-                 CheckAlwaysTrueFormMap(nf->CreateNode(NOT, c0)) ||
-                 (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0])))
+        else if (CheckAlwaysTrueFormSet(c1) || 
+                 CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c0)) ||
+                 (NOT == c0.GetKind() && CheckAlwaysTrueFormSet(c0[0])))
           {
             //(~c0 AND (~c0 OR c1)) <==> TRUE
             //
             //(c0 AND ~c0->c1) <==> TRUE
             output = ASTTrue;
           }
-        else if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, c1)) ||
-                 (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0])))
+        else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c1)) ||
+                 (NOT == c1.GetKind() && CheckAlwaysTrueFormSet(c1[0])))
           {
             //(~c1 AND c0->c1) <==> (~c1 AND ~c1->~c0) <==> ~c0
             //(c1 AND c0->~c1) <==> (c1 AND c1->~c0) <==> ~c0
@@ -1481,19 +1474,19 @@ namespace BEEV
       {
         output = ASTFalse;
       }
-    else if (CheckAlwaysTrueFormMap(c0))
+    else if (CheckAlwaysTrueFormSet(c0))
       {
         output = c1;
       }
-    else if (CheckAlwaysTrueFormMap(c1))
+    else if (CheckAlwaysTrueFormSet(c1))
       {
         output = c0;
       }
-    else if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, c0)))
+    else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c0)))
       {
         output = nf->CreateNode(NOT, c1);
       }
-    else if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, c1)))
+    else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, c1)))
       {
         output = nf->CreateNode(NOT, c0);
       }
@@ -1572,12 +1565,12 @@ namespace BEEV
       {
         output = nf->CreateNode(AND, t0, t1);
       }
-    else if (CheckAlwaysTrueFormMap(t0))
+    else if (CheckAlwaysTrueFormSet(t0))
       {
         output = t1;
       }
-    else if (CheckAlwaysTrueFormMap(nf->CreateNode(NOT, t0)) ||
-             (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0])))
+    else if (CheckAlwaysTrueFormSet(nf->CreateNode(NOT, t0)) ||
+             (NOT == t0.GetKind() && CheckAlwaysTrueFormSet(t0[0])))
       {
         output = t2;
       }
@@ -3907,7 +3900,7 @@ namespace BEEV
   {
     cerr << "SimplifyMap:" << SimplifyMap->size() << ":" << SimplifyMap->bucket_count() << endl;
     cerr << "SimplifyNegMap:" << SimplifyNegMap->size() << ":" << SimplifyNegMap->bucket_count() << endl;
-    cerr << "AlwaysTrueFormMap" << AlwaysTrueFormMap.size() << ":" << AlwaysTrueFormMap.bucket_count() << endl;
+    cerr << "AlwaysTrueFormSet" << AlwaysTrueHashSet.size() << ":" << AlwaysTrueHashSet.bucket_count() << endl;
     cerr << "MultInverseMap" << MultInverseMap.size() << ":" << MultInverseMap.bucket_count() << endl;
     cerr << "ReadOverWrite_NewName_Map" << ReadOverWrite_NewName_Map->size() << ":" << ReadOverWrite_NewName_Map->bucket_count() << endl;
     cerr << "NewName_ReadOverWrite_Map" << NewName_ReadOverWrite_Map.size() << ":" << NewName_ReadOverWrite_Map.bucket_count() << endl;

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 0e0d640f4b36305282d5b73472c61c1c63901cb9..655da35d696de08e36fe224098865b9dba5f6c20 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -36,7 +36,7 @@ namespace BEEV
     // value is simplified node.
     ASTNodeMap * SimplifyMap;
     ASTNodeMap * SimplifyNegMap;
-    ASTNodeSet AlwaysTrueFormMap;
+    HASHSET<int> AlwaysTrueHashSet;
     ASTNodeMap MultInverseMap;
 
     // For ArrayWrite Abstraction: map from read-over-write term to
@@ -101,8 +101,8 @@ namespace BEEV
     void UpdateSimplifyMap(const ASTNode& key, 
                            const ASTNode& value, 
                            bool pushNeg, ASTNodeMap* VarConstMap=NULL);
-    bool CheckAlwaysTrueFormMap(const ASTNode& key);
-    void UpdateAlwaysTrueFormMap(const ASTNode& val);
+    bool CheckAlwaysTrueFormSet(const ASTNode& key);
+    void UpdateAlwaysTrueFormSet(const ASTNode& val);
     bool CheckMultInverseMap(const ASTNode& key, ASTNode& output);
     void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value);
       
@@ -260,7 +260,7 @@ namespace BEEV
       SimplifyNegMap->clear();
       ReadOverWrite_NewName_Map->clear();
       NewName_ReadOverWrite_Map.clear();
-      AlwaysTrueFormMap.clear();
+      AlwaysTrueHashSet.clear();
       MultInverseMap.clear();
       substitutionMap.clear();
     }
@@ -269,7 +269,7 @@ namespace BEEV
     // These can be cleared (to save memory) without changing the answer.
     void ClearCaches()
     {
-        AlwaysTrueFormMap.clear();
+        AlwaysTrueHashSet.clear();
         MultInverseMap.clear();
         SimplifyMap->clear();
         SimplifyNegMap->clear();