Making some functions ASTNode memberfunctions

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

diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h
index 5e83aa56fa4536e85a509660919f4bd9493f38ab..5fadc30cb031264da5bae72adaebfc9db6113799 100644 (file)
--- a/src/AST/ASTNode.h
+++ b/src/AST/ASTNode.h
@@ -147,6 +147,7 @@ namespace BEEV
        return (k == BVCONST || k == TRUE || k == FALSE);
     }
 
+
     bool isITE() const
        {
                bool result;
@@ -169,6 +170,104 @@ namespace BEEV
                return result;
        }
 
+    bool isAtom() const
+    {
+      bool result;
+
+      const Kind k = GetKind();
+      switch (k)
+        {
+        case TRUE:
+          {
+            result = true;
+            break;
+          }
+        case FALSE:
+          {
+            result = true;
+            break;
+          }
+        case SYMBOL:
+          {
+            result = true;
+            break;
+          }
+        case BVCONST:
+          {
+            result = true;
+            break;
+          }
+        default:
+          {
+            result = false;
+            break;
+          }
+        }
+
+      return result;
+    } //End of isAtom()
+
+    bool isPred() const
+    {
+      bool result;
+
+      const Kind k = GetKind();
+      switch (k)
+        {
+        case BVLT:
+          {
+            result = true;
+            break;
+          }
+        case BVLE:
+          {
+            result = true;
+            break;
+          }
+        case BVGT:
+          {
+            result = true;
+            break;
+          }
+        case BVGE:
+          {
+            result = true;
+            break;
+          }
+        case BVSLT:
+          {
+            result = true;
+            break;
+          }
+        case BVSLE:
+          {
+            result = true;
+            break;
+          }
+        case BVSGT:
+          {
+            result = true;
+            break;
+          }
+        case BVSGE:
+          {
+            result = true;
+            break;
+          }
+        case EQ:
+          {
+            result = true;
+            break;
+          }
+        default:
+          {
+            result = false;
+            break;
+          }
+        }
+      return result;
+    } //End of isPred()
+
 
     // For lisp DAG printing.  Has it been printed already, so we can
     // just print the node number?

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index a7ce3ac3790fc340c53f659afa9645893a3e8e39..62739539bcc3ce6816a2ac0b92ca19b83129434f 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -26,128 +26,6 @@ namespace BEEV
       }
     cllp.clear();
   } //End of DeleteClauseList
-  
-
-  bool CNFMgr::isAtom(const ASTNode& varphi)
-  {
-    bool result;
-    
-    Kind k = varphi.GetKind();
-    switch (k)
-      {
-      case TRUE:
-        {
-          result = true;
-          break;
-        }
-      case FALSE:
-        {
-          result = true;
-          break;
-        }
-      case SYMBOL:
-        {
-          result = true;
-          break;
-        }
-      case BVCONST:
-        {
-          result = true;
-          break;
-        }
-      default:
-        {
-          result = false;
-          break;
-        }
-      }
-    
-    return result;
-  } //End of isAtom()
-  
-  bool CNFMgr::isPred(const ASTNode& varphi)
-  {
-    bool result;
-    
-    Kind k = varphi.GetKind();
-    switch (k)
-      {
-      case BVLT:
-        {
-          result = true;
-          break;
-        }
-      case BVLE:
-        {
-          result = true;
-          break;
-        }
-      case BVGT:
-        {
-          result = true;
-          break;
-        }
-      case BVGE:
-        {
-          result = true;
-          break;
-        }
-      case BVSLT:
-        {
-          result = true;
-          break;
-        }
-      case BVSLE:
-        {
-          result = true;
-          break;
-        }
-      case BVSGT:
-        {
-          result = true;
-          break;
-        }
-      case BVSGE:
-        {
-          result = true;
-          break;
-        }
-      case EQ:
-        {
-          result = true;
-          break;
-        }
-      default:
-        {
-          result = false;
-          break;
-        }
-      }
-    
-    return result;
-  } //End of isPred()
-
-  bool CNFMgr::isITE(const ASTNode& varphi)
-  {
-    bool result;
-    
-    Kind k = varphi.GetKind();
-    switch (k)
-      {
-      case ITE:
-        {
-          result = true;
-          break;
-        }
-      default:
-        {
-          result = false;
-          break;
-        }
-      }
-    
-    return result;
-  } //End of isITE()
 
   bool CNFMgr::onChildDoPos(const ASTNode& varphi, unsigned int idx)
   {
@@ -524,11 +402,11 @@ namespace BEEV
     // step 4, recurse over children
     //########################################
     
-    if (isAtom(varphi))
+    if (varphi.isAtom())
       {
         return;
       }
-    else if (isPred(varphi))
+    else if (varphi.isPred())
       {
         for (unsigned int i = 0; i < varphi.GetChildren().size(); i++)
           {
@@ -592,11 +470,11 @@ namespace BEEV
     // step 4, recurse over children
     //########################################
     
-    if (isAtom(varphi))
+    if (varphi.isAtom())
       {
         return;
       }
-    else if (isITE(varphi))
+    else if (varphi.isITE())
       {
         scanFormula(varphi[0], true, false);
         scanFormula(varphi[0], false, false);
@@ -724,14 +602,14 @@ namespace BEEV
     // step 2, ITE's always get renamed
     //########################################
     
-    if (isITE(varphi))
+    if (varphi.isITE())
       {
         x->termforcnf = doRenameITE(varphi, defs);
         reduceMemoryFootprintPos(varphi[0]);
         reduceMemoryFootprintNeg(varphi[0]);
         
       }
-    else if (isAtom(varphi))
+    else if (varphi.isAtom())
       {
         x->termforcnf = ASTNodeToASTNodePtr(varphi);
       }
@@ -941,7 +819,7 @@ namespace BEEV
   void CNFMgr::convertFormulaToCNFPosCases(const ASTNode& varphi, 
                                            ClauseList* defs)
   {
-    if (isPred(varphi))
+    if (varphi.isPred())
       {
         convertFormulaToCNFPosPred(varphi, defs);
         return;
@@ -1023,7 +901,7 @@ namespace BEEV
                                            ClauseList* defs)
   {
 
-    if (isPred(varphi))
+    if (varphi.isPred())
       {
         convertFormulaToCNFNegPred(varphi, defs);
         return;

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index 76afc0c8961a55cd9747a63cef117127775d57d1..a4631c63f74ab4f3b258c1c99a145e57c88f0b06 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -73,12 +73,6 @@ namespace BEEV
     //########################################
     // utility predicates
 
-    bool isAtom(const ASTNode& varphi);
-
-    bool isPred(const ASTNode& varphi);
-
-    bool isITE(const ASTNode& varphi);
-    
     bool onChildDoPos(const ASTNode& varphi, unsigned int idx);
     
     bool onChildDoNeg(const ASTNode& varphi, unsigned int idx);