Refactor. Make the TermOrder function a non-member function with the SubstitutionMap...

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

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 23b3bc8577070a646b1eae2f0bf5058e9556be81..cf56ca62bb13e6174afded0e86494d7cdd67d634 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -351,44 +351,4 @@ namespace BEEV
     return true;
   } //End of TypeCheck function
 
-
-  //if a is READ(Arr,const) or SYMBOL, and b is BVCONST then return 1
-  //if b is READ(Arr,const) or SYMBOL, and a is BVCONST then return -1
-  //
-  //else return 0 by default
-  int TermOrder(const ASTNode& a, const ASTNode& b)
-  {
-    Kind k1 = a.GetKind();
-    Kind k2 = b.GetKind();
-
-    //a is of the form READ(Arr,const), and b is const, or
-    //a is of the form var, and b is const
-    if ((k1 == READ 
-         && a[0].GetKind() == SYMBOL 
-         && a[1].GetKind() == BVCONST 
-         && (k2 == BVCONST)))
-      // || k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind()
-      // == BVCONST)))
-      return 1;
-
-    if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2))
-      return 1;
-
-    //b is of the form READ(Arr,const), and a is const, or
-    //b is of the form var, and a is const
-    if ((k1 == BVCONST) 
-        && ((k2 == READ 
-             && b[0].GetKind() == SYMBOL 
-             && b[1].GetKind() == BVCONST)))
-      return -1;
-
-    if (SYMBOL == k2 
-        && (BVCONST == k1 
-            || TRUE == k1 
-            || FALSE == k1))
-      return -1;
-
-    return 0;
-  } //End of TermOrder()
-
 };//end of namespace

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 497669de8961518583521be5a141d9256215abf9..55b6131b386218589b8ccdfd53350b903057f79e 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -791,28 +791,22 @@ namespace BEEV
   void ArrayTransformer::FillUp_ArrReadIndex_Vec(const ASTNode& e0, 
                                                  const ASTNode& e1)
   {
-    int i = TermOrder(e0, e1);
-    if (0 == i)
-      return;
+         assert(e0.GetKind() == READ);
+         assert(e1.GetKind() == BVCONST);
 
-    if (1 == i 
-        && e0.GetKind() != SYMBOL 
-        && !simp->CheckSubstitutionMap(e0))
+         if (e0[0].GetKind() != SYMBOL)
+                 return;
+         if (e0[1].GetKind() != BVCONST)
+                 return;
+
+    if (!simp->CheckSubstitutionMap(e0))
       {
         (*Arrayname_ReadindicesMap)[e0[0]].push_back(e0[1]);
         //e0 is the array read : READ(A,i) and e1 is a bvconst
         Arrayread_SymbolMap[e0] = e1;
         return;
       }
-    if (-1 == i 
-        && e1.GetKind() != SYMBOL 
-        && !simp->CheckSubstitutionMap(e1))
-      {
-        (*Arrayname_ReadindicesMap)[e1[0]].push_back(e1[1]);
-        //e0 is the array read : READ(A,i) and e1 is a bvconst
-        Arrayread_SymbolMap[e1] = e0;
-        return;
-      }
+
   } //End of Fillup
 
 

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 5d29df8a21f5d9650f75e9d3273a277895c7f9a1..b70a15b716859433082fdfd7d05d2d340f37f749 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -16,7 +16,50 @@ SubstitutionMap::~SubstitutionMap()
 }
 
 
-//The big substitution function
+//if a is READ(Arr,const) or SYMBOL, and b is BVCONST then return 1
+//if b is READ(Arr,const) or SYMBOL, and a is BVCONST then return -1
+//
+//else return 0 by default
+int TermOrder(const ASTNode& a, const ASTNode& b)
+{
+  Kind k1 = a.GetKind();
+  Kind k2 = b.GetKind();
+
+  //a is of the form READ(Arr,const), and b is const, or
+  //a is of the form var, and b is const
+  if ((k1 == READ
+       && a[0].GetKind() == SYMBOL
+       && a[1].GetKind() == BVCONST
+       && (k2 == BVCONST)))
+    // || k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind()
+    // == BVCONST)))
+    return 1;
+
+  if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2))
+    return 1;
+
+  //b is of the form READ(Arr,const), and a is const, or
+  //b is of the form var, and a is const
+  if ((k1 == BVCONST)
+      && ((k2 == READ
+           && b[0].GetKind() == SYMBOL
+           && b[1].GetKind() == BVCONST)))
+    return -1;
+
+  if (SYMBOL == k2
+      && (BVCONST == k1
+          || TRUE == k1
+          || FALSE == k1))
+    return -1;
+
+  return 0;
+} //End of TermOrder()
+
+
+//This finds everything which is (= SYMBOL BVCONST) and everything that is (READ SYMBOL BVCONST).
+//i.e. anything that has a termorder of 1 or -1.
+// The bvsolver puts expressions of the form (= SYMBOL TERM) into the solverMap.
+
 ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransformer*at
 )
 {
@@ -67,7 +110,12 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
       ASTVec c = a.GetChildren();
       SortByArith(c);
       ASTNode c1 = simp->SimplifyTerm(c[1]);
-      at->FillUp_ArrReadIndex_Vec(c[0], c1);
+
+      int to;
+      if ((to =TermOrder(c[0],c1))==1 && c[0].GetKind() == READ)
+         at->FillUp_ArrReadIndex_Vec(c[0], c1);
+      else if (to ==-1 && c1.GetKind() == READ)
+               at->FillUp_ArrReadIndex_Vec(c1,c[0]);
 
       if (SYMBOL == c[0].GetKind()
           && bm->VarSeenInTerm(c[0], c1))